search

stanford-centaur / smt-switch

A generic C++ API for SMT solving. It provides abstract classes which can be implemented by different SMT solvers.
Other
114 stars 43 forks source link

TermTranslator unhelpful rewrite. #326

Open kunalsheth opened 1 year ago

kunalsheth commented 1 year ago

When fed the CVC5 term: (let ((_let_1 (f y))) (let ((_let_2 (f x))) (and (<= 0 _let_2) (<= 0 _let_1) (<= (+ _let_2 _let_1) 1) (not (p 0)) (p _let_1))))

The TermTranslator (to any solver), rewrites it as: (let ((_let_1 (f y))) (let ((_let_2 (f x))) (and (= (ite (<= 0 _let_2) (_ bv1 1) (_ bv0 1)) (_ bv1 1)) (= (ite (<= 0 _let_1) (_ bv1 1) (_ bv0 1)) (_ bv1 1)) (= (ite (<= (+ _let_2 _let_1) 1) (_ bv1 1) (_ bv0 1)) (_ bv1 1)) (= (ite (not (p 0)) (_ bv1 1) (_ bv0 1)) (_ bv1 1)) (= (ite (p _let_1) (_ bv1 1) (_ bv0 1)) (_ bv1 1)))))

We would like the option to disable such a rewrite.

It appears this may be caused by two related bugs:

  1. Because the AND has more than two children, execution goes into the if-statement linked below. We think we would like an option to manually disable this check and/or make smt-switch allow for ANDs to support more than two children. The translated term should have as similar a structure to the original term as possible. https://github.com/stanford-centaur/smt-switch/blob/f2d7d3d6dfccc0b4d6b604563acd34629bac884d/src/term_translator.cpp#L269C12-L269C12
  2. It looks like cast_op and/or cast_term are being called twice upon themselves, leading to a Boolean-to-BV rewrite immediately followed by a BV-to-Boolean rewrite— which I do not think is the intended behavior, and we would also like to turn off.
barrettcw commented 1 year ago

This does look weird. Can you propose a fix and submit a PR?

barrettcw commented 1 year ago

@makaimann - low priority but could you have a look at this and see if you can tell us where the problem is?