[SMTChecker] Fix CHCSmtLib2Interface #11289
Conversation
leonardoalt
force-pushed
the
smt_fix_chcsmtlib2interface
branch
from
a36d55f to
8a444ba
Compare
leonardoalt
force-pushed
the
smt_fix_chcsmtlib2interface
branch
from
8a444ba to
981bca9
Compare
libsmtutil/SolverInterface.h
Outdated
| Expression(s256 const& _number): Expression(_number.str(), {}, SortProvider::sintSort) {} | ||
| Expression(bigint const& _number): Expression(_number.str(), {}, SortProvider::sintSort) {} | ||
| Expression(s256 const& _number): Expression(_number.sign() >= 0 ? _number.str() : "-", _number.sign() >= 0 ? std::vector<Expression>{} : std::vector<Expression>{Expression(size_t(0)), u256(-_number)}, SortProvider::sintSort) {} | ||
| Expression(bigint const& _number): Expression(_number.sign() >= 0 ? _number.str() : "-", _number.sign() >= 0 ? std::vector<Expression>{} : std::vector<Expression>{Expression(size_t(0)), u256(-_number)}, SortProvider::sintSort) {} |
There was a problem hiding this comment.
Not sure about the lines above. The fix is correct but looks kinda ugly. Open to suggestions.
| @@ -118,7 +118,7 @@ SortPointer smtSort(frontend::Type const& _type) | |||
| else | |||
| tupleName = arrayType->baseType()->toString(true); | |||
|
|
|||
| tupleName += "[]"; | |||
| tupleName += "_array"; | |||
There was a problem hiding this comment.
This is needed because smtlib2 doesn't like identifiers with []
| @@ -300,7 +300,7 @@ class Expression | |||
| friend Expression operator/(Expression _a, Expression _b) | |||
| { | |||
| auto intSort = _a.sort; | |||
| return Expression("/", {std::move(_a), std::move(_b)}, intSort); | |||
| return Expression("div", {std::move(_a), std::move(_b)}, intSort); | |||
There was a problem hiding this comment.
Aren't the changes in the commit redundant?
There was a problem hiding this comment.
Because we end up converting "div" to / in both z3interface and cvc4interface. Why do we call it div?
There was a problem hiding this comment.
Because smtlib2 uses the name of the operator when creating the queries. Since we want it to use div, it makes sense for all solvers to read div
There was a problem hiding this comment.
@hrkrshnn only this discussion left to finish I think
There was a problem hiding this comment.
Do we currently use pure smt2 queries?
There was a problem hiding this comment.
It's an option, via SmtLib2Interface or CHCSmtLib2Inteface
leonardoalt
force-pushed
the
smt_fix_chcsmtlib2interface
branch
from
dc919ba to
c570b63
Compare
leonardoalt
force-pushed
the
smt_fix_chcsmtlib2interface
branch
from
c570b63 to
f7b045b
Compare
|
@hrkrshnn updated & rebased |
|
Yea the last commit has parts that would have to into different commits, so I would merge as is since it's not too much. |
Previously CHCSmtLib2Interface was using z3's the
rulelanguage sugar to describe Horn clauses. This PR changes it to the proper smtlib2 Horn logic which other solvers can also understand. That is the main fix and is coded in the first commit.The other commits add other small fixes that I felt were small enough to be just single commits in this same PR:
impliesis not smtlib2,=>is the right operator-10in smtlib2. It needs to be either(- 10)or(0 - 10). Here I went with the latter to avoid overloading the minus operator./is actually Real division, whereas we want Integer division which isdivgasleft()should begasleftbvnatfirstWith these changes, the queries given by CHCSmtLib2Interface can actually be read by any Horn solver that reads smtlib2.
We don't have direct tests for that, because:
t_emsBUT