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

Generic solver fails SortingNetwork test #240

Open makaimann opened 3 years ago

makaimann commented 3 years ago

This can be reproduced by changing https://github.com/makaimann/smt-switch/blob/3ba9442aef2def27faeb79185065ac1d481d26f7/tests/test-sorting-network.cpp#L104 to include generic solvers. Then configuring, building and running with:

./configure.sh --debug --cvc4
cd build
make
./tests/test-sorting-network
makaimann commented 3 years ago

@yoni206 would you be willing to look into this?

makaimann commented 3 years ago

Oh wait, @yoni206, I looked at it again and figured out the problem. It's because I build a term after calling check-sat. If I move this line https://github.com/makaimann/smt-switch/blob/3ba9442aef2def27faeb79185065ac1d481d26f7/tests/test-sorting-network.cpp#L79 before the call to check-sat, then it passes.

But I'm wondering if it has to be that way? Other solvers don't behave that way in the API at least.

yoni206 commented 3 years ago

from page 52 of: http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf image

In the generic solver, we use a define-fun for every make_term. According to this diagram, define-fun cannot be used right after check-sat when using the textual smtlib interface. Since other APIs don't fail for this, the generic solver should support this too. This can be fixed by, for example, calling define-fun lazily, only before assertions that use the created terms, but there could be other solutions.

yoni206 commented 3 years ago

image (from the same page)

I wasn't accurate -- it is ok to do a define-fun right after check-sat, but it moves you to Assert mode, in which you are not allowed to do get-value. BTW z3's smtlib interface does not complain.