From 73a92766063e76e6c6f2507f126fb8f84ed3e432 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Fri, 2 Feb 2018 15:34:44 -0600 Subject: [PATCH] Option to check solutions produced by SyGuS solver (#1553) --- src/options/quantifiers_options | 4 +- src/options/smt_options | 3 + src/smt/smt_engine.cpp | 112 +++++++++++++++++- src/smt/smt_engine.h | 10 ++ src/theory/quantifiers_engine.cpp | 5 + src/theory/quantifiers_engine.h | 12 ++ src/theory/theory_engine.cpp | 5 + src/theory/theory_engine.h | 11 ++ test/regress/regress0/sygus/General_plus10.sy | 2 +- test/regress/regress0/sygus/array_search_2.sy | 2 +- test/regress/regress0/sygus/const-var-test.sy | 2 +- test/regress/regress0/sygus/max.sy | 2 +- test/regress/run_regression | 8 ++ 13 files changed, 168 insertions(+), 10 deletions(-) diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 9d717c0ba..96d73feeb 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -294,10 +294,10 @@ option sygusCRefEval --sygus-cref-eval bool :default true direct evaluation of refinement lemmas for conflict analysis option sygusCRefEvalMinExp --sygus-cref-eval-min-exp bool :default true use min explain for direct evaluation of refinement lemmas for conflict analysis - + option sygusStream --sygus-stream bool :read-write :default false enumerate a stream of solutions instead of terminating after the first one - + # internal uses of sygus option sygusRewSynth --sygus-rr-synth bool :default false use sygus to enumerate candidate rewrite rules via sampling diff --git a/src/options/smt_options b/src/options/smt_options index fa6c3ae4e..b19420060 100644 --- a/src/options/smt_options +++ b/src/options/smt_options @@ -54,6 +54,9 @@ option dumpUnsatCores --dump-unsat-cores bool :default false :link --produce-uns option dumpUnsatCoresFull dump-unsat-cores-full --dump-unsat-cores-full bool :default false :link --dump-unsat-cores :link-smt dump-unsat-cores :notify notifyBeforeSearch dump the full unsat core, including unlabeled assertions +option checkSynthSol --check-synth-sol bool :default false + checks whether produced solutions to functions-to-synthesize satisfy the conjecture + option produceAssignments produce-assignments --produce-assignments bool :default false :notify notifyBeforeSearch support the get-assignment command diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 0c8723ff6..6af5e38d5 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1353,13 +1353,13 @@ void SmtEngine::setDefaults() { */ } - if(options::checkModels()) { - if(! options::produceAssertions()) { + if ((options::checkModels() || options::checkSynthSol()) + && !options::produceAssertions()) + { Notice() << "SmtEngine: turning on produce-assertions to support " - << "check-models." << endl; + << "check-models or check-synth-sol." << endl; setOption("produce-assertions", SExpr("true")); } - } if(options::unsatCores()) { if(options::simplificationMode() != SIMPLIFICATION_MODE_NONE) { @@ -4801,6 +4801,12 @@ Result SmtEngine::checkSatisfiability(const Expr& ex, bool inUnsatCore, bool isQ checkUnsatCore(); } } + // Check that synthesis solutions satisfy the conjecture + if (options::checkSynthSol() + && r.asSatisfiabilityResult().isSat() == Result::UNSAT) + { + checkSynthSolution(); + } return r; } catch (UnsafeInterruptException& e) { @@ -5488,6 +5494,104 @@ void SmtEngine::checkModel(bool hardFailure) { Notice() << "SmtEngine::checkModel(): all assertions checked out OK !" << endl; } +void SmtEngine::checkSynthSolution() +{ + NodeManager* nm = NodeManager::currentNM(); + Notice() << "SmtEngine::checkSynthSolution(): checking synthesis solution" << endl; + map sol_map; + /* Get solutions and build auxiliary vectors for substituting */ + d_theoryEngine->getSynthSolutions(sol_map); + Trace("check-synth-sol") << "Got solution map:\n"; + std::vector function_vars, function_sols; + for (const auto& pair : sol_map) + { + Trace("check-synth-sol") << pair.first << " --> " << pair.second << "\n"; + function_vars.push_back(pair.first); + function_sols.push_back(pair.second); + } + Trace("check-synth-sol") << "Starting new SMT Engine\n"; + /* Start new SMT engine to check solutions */ + SmtEngine solChecker(d_exprManager); + solChecker.setLogic(getLogicInfo()); + setOption("check-synth-sol", SExpr("false")); + + Trace("check-synth-sol") << "Retrieving assertions\n"; + // Build conjecture from original assertions + if (d_assertionList == NULL) + { + Trace("check-synth-sol") << "No assertions to check\n"; + return; + } + for (AssertionList::const_iterator i = d_assertionList->begin(); + i != d_assertionList->end(); + ++i) + { + Notice() << "SmtEngine::checkSynthSolution(): checking assertion " << *i << endl; + Trace("check-synth-sol") << "Retrieving assertion " << *i << "\n"; + Node conj = Node::fromExpr(*i); + // Apply any define-funs from the problem. + { + unordered_map cache; + conj = d_private->expandDefinitions(conj, cache); + } + Notice() << "SmtEngine::checkSynthSolution(): -- expands to " << conj << endl; + Trace("check-synth-sol") << "Expanded assertion " << conj << "\n"; + + // Apply solution map to conjecture body + Node conjBody; + /* Whether property is quantifier free */ + if (conj[1].getKind() != kind::EXISTS) + { + conjBody = conj[1].substitute(function_vars.begin(), + function_vars.end(), + function_sols.begin(), + function_sols.end()); + } + else + { + conjBody = conj[1][1].substitute(function_vars.begin(), + function_vars.end(), + function_sols.begin(), + function_sols.end()); + + /* Skolemize property */ + std::vector vars, skos; + for (unsigned j = 0, size = conj[1][0].getNumChildren(); j < size; ++j) + { + vars.push_back(conj[1][0][j]); + std::stringstream ss; + ss << "sk_" << j; + skos.push_back(nm->mkSkolem(ss.str(), conj[1][0][j].getType())); + Trace("check-synth-sol") << "\tSkolemizing " << conj[1][0][j] << " to " + << skos.back() << "\n"; + } + conjBody = conjBody.substitute( + vars.begin(), vars.end(), skos.begin(), skos.end()); + } + Notice() << "SmtEngine::checkSynthSolution(): -- body substitutes to " + << conjBody << endl; + Trace("check-synth-sol") << "Substituted body of assertion to " << conjBody + << "\n"; + solChecker.assertFormula(conjBody.toExpr()); + Result r = solChecker.checkSat(); + Notice() << "SmtEngine::checkSynthSolution(): result is " << r << endl; + Trace("check-synth-sol") << "Satsifiability check: " << r << "\n"; + if (r.asSatisfiabilityResult().isUnknown()) + { + InternalError( + "SmtEngine::checkSynthSolution(): could not check solution, result " + "unknown."); + } + else if (r.asSatisfiabilityResult().isSat()) + { + InternalError( + "SmtEngine::checkSynhtSol(): produced solution allows satisfiable " + "negated conjecture."); + } + solChecker.resetAssertions(); + } +} + // TODO(#1108): Simplify the error reporting of this method. UnsatCore SmtEngine::getUnsatCore() { Trace("smt") << "SMT getUnsatCore()" << endl; diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 0501a6e8f..e768bf826 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -286,6 +286,16 @@ class CVC4_PUBLIC SmtEngine { */ void checkModel(bool hardFailure = true); + /** + * Check that a solution to a synthesis conjecture is indeed a solution. + * + * The check is made by determining if the negation of the synthesis + * conjecture in which the functions-to-synthesize have been replaced by the + * synthesized solutions, which is a quantifier-free formula, is + * unsatisfiable. If not, then the found solutions are wrong. + */ + void checkSynthSolution(); + /** * Postprocess a value for output to the user. Involves doing things * like turning datatypes back into tuples, length-1-bitvectors back diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 34dde7fc8..a0efe80f9 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -1195,6 +1195,11 @@ Node QuantifiersEngine::getInternalRepresentative( Node a, Node q, int index ){ return ret; } +void QuantifiersEngine::getSynthSolutions(std::map& sol_map) +{ + d_ceg_inst->getSynthSolutions(sol_map); +} + void QuantifiersEngine::debugPrintEqualityEngine( const char * c ) { eq::EqualityEngine* ee = getActiveEqualityEngine(); eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 3cd4e8ef9..3716fc497 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -399,6 +399,18 @@ public: void getExplanationForInstLemmas(const std::vector& lems, std::map& quant, std::map >& tvec); + + /** get synth solutions + * + * This function adds entries to sol_map that map functions-to-synthesize with + * their solutions, for all active conjectures. This should be called + * immediately after the solver answers unsat for sygus input. + * + * For details on what is added to sol_map, see + * CegConjecture::getSynthSolutions. + */ + void getSynthSolutions(std::map& sol_map); + //----------end user interface for instantiations /** statistics class */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 435dadce7..edbd768d7 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -902,6 +902,11 @@ TheoryModel* TheoryEngine::getModel() { return d_curr_model; } +void TheoryEngine::getSynthSolutions(std::map& sol_map) +{ + d_quantEngine->getSynthSolutions(sol_map); +} + bool TheoryEngine::presolve() { // Reset the interrupt flag d_interrupted = false; diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 22e269409..7bc95b097 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -715,6 +715,17 @@ public: */ theory::TheoryModel* getModel(); + /** get synth solutions + * + * This function adds entries to sol_map that map functions-to-synthesize with + * their solutions, for all active conjectures. This should be called + * immediately after the solver answers unsat for sygus input. + * + * For details on what is added to sol_map, see + * CegConjecture::getSynthSolutions. + */ + void getSynthSolutions(std::map& sol_map); + /** * Get the model builder */ diff --git a/test/regress/regress0/sygus/General_plus10.sy b/test/regress/regress0/sygus/General_plus10.sy index 1792749e2..33552f9e2 100755 --- a/test/regress/regress0/sygus/General_plus10.sy +++ b/test/regress/regress0/sygus/General_plus10.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=all --sygus-out=status +; COMMAND-LINE: --cegqi-si=all --sygus-out=status --no-check-synth-sol (set-logic LIA) (synth-fun fb () Int ((Start Int ((Constant Int))))) diff --git a/test/regress/regress0/sygus/array_search_2.sy b/test/regress/regress0/sygus/array_search_2.sy index 41346e655..5786eb649 100644 --- a/test/regress/regress0/sygus/array_search_2.sy +++ b/test/regress/regress0/sygus/array_search_2.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=all --sygus-out=status +; COMMAND-LINE: --cegqi-si=all --sygus-out=status --no-check-synth-sol (set-logic LIA) (synth-fun findIdx ( (y1 Int) (y2 Int) (k1 Int)) Int ((Start Int ( 0 1 2 y1 y2 k1 (ite BoolExpr Start Start))) (BoolExpr Bool ((< Start Start) (<= Start Start) (> Start Start) (>= Start Start))))) (declare-var x1 Int) diff --git a/test/regress/regress0/sygus/const-var-test.sy b/test/regress/regress0/sygus/const-var-test.sy index 305f5783a..af2d8b25b 100644 --- a/test/regress/regress0/sygus/const-var-test.sy +++ b/test/regress/regress0/sygus/const-var-test.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=all --sygus-out=status +; COMMAND-LINE: --cegqi-si=all --sygus-out=status --no-check-synth-sol (set-logic LIA) diff --git a/test/regress/regress0/sygus/max.sy b/test/regress/regress0/sygus/max.sy index 37ed848ef..cbe2bccea 100644 --- a/test/regress/regress0/sygus/max.sy +++ b/test/regress/regress0/sygus/max.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=all --sygus-out=status +; COMMAND-LINE: --cegqi-si=all --sygus-out=status --no-check-synth-sol (set-logic LIA) (synth-fun max ((x Int) (y Int)) Int diff --git a/test/regress/run_regression b/test/regress/run_regression index 5d4165597..e236234e1 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -262,6 +262,13 @@ else echo "$expected_output" >"$expoutfile" fi +if [ "$lang" = sygus ]; then + if ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--check-synth-sol' &>/dev/null && + ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--no-check-synth-sol' &>/dev/null; then + # later on, we'll run another test with --check-models on + command_line="$command_line --check-synth-sol" + fi +fi check_models=false if grep '^sat$' "$expoutfile" &>/dev/null || grep '^invalid$' "$expoutfile" &>/dev/null || grep '^unknown$' "$expoptfile" &>/dev/null; then if ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--check-models' &>/dev/null && @@ -407,4 +414,5 @@ if $check_models || $check_proofs || $check_unsat_cores; then fi fi + exit $exitcode -- 2.30.2