cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Double SAT run for cex

Browse Source
This commit is contained in:
Leonardo Alt 2020-07-13 20:56:12 +02:00
parent 694ec92688
commit 51721c3080
3 changed files with 64 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

55
libsmtutil/Z3CHCInterface.cpp
View File

@ -36,18 +36,7 @@ Z3CHCInterface::Z3CHCInterface():
z3::set_param("rewriter.pull_cheap_ite", true);
z3::set_param("rlimit", Z3Interface::resourceLimit);
// Spacer options.
// These needs to be set in the solver.
// https://github.com/Z3Prover/z3/blob/master/src/muz/base/fp_params.pyg
z3::params p(*m_context);
// These are useful for solving problems with arrays and loops.
// Use quantified lemma generalizer.
p.set("fp.spacer.q3.use_qgen", true);
p.set("fp.spacer.mbqi", false);
// Ground pobs by using values from a model.
p.set("fp.spacer.ground_pobs", false);
m_solver.set(p);
enablePreProcessing();
}
void Z3CHCInterface::declareVariable(string const& _name, SortPointer const& _sort)
@ -115,6 +104,48 @@ pair<CheckResult, CHCSolverInterface::CexGraph> Z3CHCInterface::query(Expression
return {result, cex};
}
void Z3CHCInterface::enablePreProcessing()
{
// Spacer options.
// These needs to be set in the solver.
// https://github.com/Z3Prover/z3/blob/master/src/muz/base/fp_params.pyg
z3::params p(*m_context);
// These are useful for solving problems with arrays and loops.
// Use quantified lemma generalizer.
p.set("fp.spacer.q3.use_qgen", true);
p.set("fp.spacer.mbqi", false);
// Ground pobs by using values from a model.
p.set("fp.spacer.ground_pobs", false);
// Enable Spacer optimization for better solving.
p.set("fp.xform.slice", true);
p.set("fp.xform.inline_linear", true);
p.set("fp.xform.inline_eager", true);
m_solver.set(p);
}
void Z3CHCInterface::disablePreProcessing()
{
// Spacer options.
// These needs to be set in the solver.
// https://github.com/Z3Prover/z3/blob/master/src/muz/base/fp_params.pyg
z3::params p(*m_context);
// These are useful for solving problems with arrays and loops.
// Use quantified lemma generalizer.
p.set("fp.spacer.q3.use_qgen", true);
p.set("fp.spacer.mbqi", false);
// Ground pobs by using values from a model.
p.set("fp.spacer.ground_pobs", false);
// Disable Spacer optimization for counterexample generation.
p.set("fp.xform.slice", false);
p.set("fp.xform.inline_linear", false);
p.set("fp.xform.inline_eager", false);
m_solver.set(p);
}
/**
Convert a ground refutation into a linear or nonlinear counterexample.
The counterexample is given as an implication graph of the form

3
libsmtutil/Z3CHCInterface.h
View File

@ -46,6 +46,9 @@ public:
Z3Interface* z3Interface() const { return m_z3Interface.get(); }
void enablePreProcessing();
void disablePreProcessing();
private:
/// Constructs a nonlinear counterexample graph from the refutation.
CHCSolverInterface::CexGraph cexGraph(z3::expr const& _proof);

18
libsolidity/formal/CHC.cpp
View File

@ -1128,7 +1128,25 @@ pair<smtutil::CheckResult, CHCSolverInterface::CexGraph> CHC::query(smtutil::Exp
switch (result)
{
case smtutil::CheckResult::SATISFIABLE:
{
#ifdef HAVE_Z3
// Even though the problem is SAT, Spacer's pre processing makes counterexamples incomplete.
// We now disable those optimizations and check whether we can still solve the problem.
auto* spacer = dynamic_cast<Z3CHCInterface*>(m_interface.get());
solAssert(spacer, "");
spacer->disablePreProcessing();
smtutil::CheckResult resultNoOpt;
CHCSolverInterface::CexGraph cexNoOpt;
tie(resultNoOpt, cexNoOpt) = m_interface->query(_query);
if (resultNoOpt == smtutil::CheckResult::SATISFIABLE)
cex = move(cexNoOpt);
spacer->enablePreProcessing();
#endif
break;
}
case smtutil::CheckResult::UNSATISFIABLE:
break;
case smtutil::CheckResult::UNKNOWN: