From 47b910a85de71b6617e4d1d210dcb57de597961b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 13 Aug 2019 10:39:45 -0500 Subject: [PATCH] Implement check abduct feature (#3152) --- src/options/smt_options.toml | 9 +++++ src/smt/smt_engine.cpp | 71 ++++++++++++++++++++++++++++++++++ src/smt/smt_engine.h | 14 +++++++ test/regress/run_regression.py | 4 ++ 4 files changed, 98 insertions(+) diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 733819780..394875fae 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -634,3 +634,12 @@ header = "options/smt_options.h" default = "false" read_only = true help = "support the get-abduct command" + +[[option]] + name = "checkAbducts" + category = "regular" + long = "check-abducts" + type = "bool" + default = "false" + read_only = true + help = "checks whether produced solutions to get-abduct are correct" diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index b66d230b7..e9c3f06ae 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -4919,6 +4919,70 @@ void SmtEngine::checkSynthSolution() } } +void SmtEngine::checkAbduct(Expr a) +{ + Assert(a.getType().isBoolean()); + Trace("check-abduct") << "SmtEngine::checkAbduct: get expanded assertions" + << std::endl; + + std::vector asserts = getExpandedAssertions(); + asserts.push_back(a); + + // two checks: first, consistent with assertions, second, implies negated goal + // is unsatisfiable. + for (unsigned j = 0; j < 2; j++) + { + Trace("check-abduct") << "SmtEngine::checkAbduct: phase " << j + << ": make new SMT engine" << std::endl; + // Start new SMT engine to check solution + SmtEngine abdChecker(d_exprManager); + abdChecker.setLogic(getLogicInfo()); + Trace("check-abduct") << "SmtEngine::checkAbduct: phase " << j + << ": asserting formulas" << std::endl; + for (const Expr& e : asserts) + { + abdChecker.assertFormula(e); + } + Trace("check-abduct") << "SmtEngine::checkAbduct: phase " << j + << ": check the assertions" << std::endl; + Result r = abdChecker.checkSat(); + Trace("check-abduct") << "SmtEngine::checkAbduct: phase " << j + << ": result is " << r << endl; + std::stringstream serr; + bool isError = false; + if (j == 0) + { + if (r.asSatisfiabilityResult().isSat() != Result::SAT) + { + isError = true; + serr << "SmtEngine::checkAbduct(): produced solution cannot be shown " + "to be consisconsistenttent with assertions, result was " + << r; + } + Trace("check-abduct") + << "SmtEngine::checkAbduct: goal is " << d_abdConj << std::endl; + // add the goal to the set of assertions + Assert(!d_abdConj.isNull()); + asserts.push_back(d_abdConj); + } + else + { + if (r.asSatisfiabilityResult().isSat() != Result::UNSAT) + { + isError = true; + serr << "SmtEngine::checkAbduct(): negated goal cannot be shown " + "unsatisfiable with produced solution, result was " + << r; + } + } + // did we get an unexpected result? + if (isError) + { + InternalError(serr.str().c_str()); + } + } +} + // TODO(#1108): Simplify the error reporting of this method. UnsatCore SmtEngine::getUnsatCore() { Trace("smt") << "SMT getUnsatCore()" << endl; @@ -5081,6 +5145,7 @@ bool SmtEngine::getAbduct(const Expr& conj, const Type& grammarType, Expr& abd) std::vector asserts(axioms.begin(), axioms.end()); // negate the conjecture Node conjn = Node::fromExpr(conj).negate(); + d_abdConj = conjn.toExpr(); asserts.push_back(conjn); d_sssfVarlist.clear(); d_sssfSyms.clear(); @@ -5153,6 +5218,12 @@ bool SmtEngine::getAbductInternal(Expr& abd) // convert to expression abd = abdn.toExpr(); + + // if check abducts option is set, we check the correctness + if (options::checkAbducts()) + { + checkAbduct(abd); + } return true; } Trace("sygus-abduct") << "SmtEngine::getAbduct: could not find solution!" diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index ead337862..f783b0a33 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -175,6 +175,11 @@ class CVC4_PUBLIC SmtEngine { */ std::vector d_sssfVarlist; std::vector d_sssfSyms; + /** + * The conjecture of the current abduction problem. This expression is only + * valid while we are in mode SMT_MODE_ABDUCT. + */ + Expr d_abdConj; /** recursive function definition abstractions for --fmf-fun */ std::map< Node, TypeNode > d_fmfRecFunctionsAbs; std::map< Node, std::vector< Node > > d_fmfRecFunctionsConcrete; @@ -360,6 +365,15 @@ class CVC4_PUBLIC SmtEngine { * unsatisfiable. If not, then the found solutions are wrong. */ void checkSynthSolution(); + /** + * Check that a solution to an abduction conjecture is indeed a solution. + * + * The check is made by determining that the assertions conjoined with the + * solution to the abduction problem (a) is SAT, and the assertions conjoined + * with the abduct and the goal is UNSAT. If these criteria are not met, an + * internal error is thrown. + */ + void checkAbduct(Expr a); /** * Postprocess a value for output to the user. Involves doing things diff --git a/test/regress/run_regression.py b/test/regress/run_regression.py index 8918c75c1..61b89d9c5 100755 --- a/test/regress/run_regression.py +++ b/test/regress/run_regression.py @@ -293,6 +293,10 @@ def run_regression(unsat_cores, proofs, dump, use_skip_return_code, wrapper, '--unconstrained-simp' not in all_args and \ not cvc4_binary.endswith('pcvc4'): extra_command_line_args += ['--check-unsat-cores'] + if '--no-check-abducts' not in all_args and \ + '--check-abducts' not in all_args and \ + not cvc4_binary.endswith('pcvc4'): + extra_command_line_args += ['--check-abducts'] if extra_command_line_args: command_line_args_configs.append(all_args + extra_command_line_args) -- 2.30.2