SMTChecker: Introduce first draft of Z3CHCSmtlib2Interface #15348
Conversation
| response = querySolver(query); | ||
| setupSmtCallback(true); | ||
| if (!boost::starts_with(response, "unsat")) | ||
| return {CheckResult::SATISFIABLE, Expression(true), {}}; |
There was a problem hiding this comment.
If it is not unsat couldn't it also be UNKNOWN or ERROR here?
There was a problem hiding this comment.
If solver for some reason would not return unsat (which is what we expect), then we ignore this second call and just return what we would have returned if we would not want to compute counterexample.
See my response below for the SAT/UNSAT confusion.
blishko
force-pushed
the
smt-z3smtlib-first-draft
branch
from
bb939dd
to
2c38b8b
Compare
| CHCSolverInterface::CexGraph graphFromZ3Answer(std::string const& _proof) const; | ||
| static CHCSolverInterface::CexGraph graphFromSMTLib2Expression( | ||
| smtutil::SMTLib2Expression const& _proof, | ||
| ScopedParser & context |
There was a problem hiding this comment.
| ScopedParser & context | |
| ScopedParser& _context |
|
|
||
| auto const* root = proofStack.top(); | ||
| auto const& derivedRootFact = fact(*root); | ||
| visitedIds.insert({root, nextId++}); |
There was a problem hiding this comment.
| visitedIds.insert({root, nextId++}); | |
| visitedIds.emplace(root, nextId++); |
| auto const* child = &args[i]; | ||
| if (!visitedIds.count(child)) | ||
| { | ||
| visitedIds.insert({child, nextId++}); |
There was a problem hiding this comment.
| visitedIds.insert({child, nextId++}); | |
| visitedIds.emplace(child, nextId++); |
|
Seeing as this is an unused interface, I expect you're going to be making some tweaks in subsequent PR regardless, so please take a glance at the comments, and then we can merge. |
blishko
force-pushed
the
smt-z3smtlib-first-draft
branch
from
2c38b8b
to
441f027
Compare
This commit introduces the interface class without actually using it. The actual switch will be done later, after all things are set up.
blishko
force-pushed
the
smt-z3smtlib-first-draft
branch
from
441f027
to
82a3071
Compare
|
@nikola-matic, I think I addressed all your comments, except the |
Yup, that's fine. |
This commit introduces the interface class without actually using it. The actual switch will be done later, after all things are set up.
This was separated from #15252.