From: Andrew Reynolds Date: Tue, 22 May 2018 18:08:31 +0000 (-0500) Subject: Make sygus infer find function definitions (#1951) X-Git-Tag: cvc5-1.0.0~5025 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=cdf7aacd6b682645cf1a2bc609db005b2f4dafc7;p=cvc5.git Make sygus infer find function definitions (#1951) --- diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 82147c094..36792e3c0 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2701,7 +2701,9 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_mappush_back( f ); } } + if (options::sygusInference()) + { + // try recast as sygus + quantifiers::SygusInference si; + if (si.simplify(d_assertions.ref())) + { + Trace("smt-proc") << "...converted to sygus conjecture." << std::endl; + } + } Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-quant-preprocess" << endl; } @@ -5573,6 +5574,18 @@ void SmtEngine::printSynthSolution( std::ostream& out ) { } } +void SmtEngine::getSynthSolutions(std::map& sol_map) +{ + SmtScope smts(this); + map sol_mapn; + Assert(d_theoryEngine != nullptr); + d_theoryEngine->getSynthSolutions(sol_mapn); + for (std::pair& s : sol_mapn) + { + sol_map[s.first.toExpr()] = s.second.toExpr(); + } +} + Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict) { SmtScope smts(this); diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 83300afc9..dd1d1b88a 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -655,6 +655,22 @@ class CVC4_PUBLIC SmtEngine { */ void printSynthSolution( std::ostream& out ); + /** + * Get synth solution + * + * 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. + * + * Specifically, given a sygus conjecture of the form + * exists x1...xn. forall y1...yn. P( x1...xn, y1...yn ) + * where x1...xn are second order bound variables, we map each xi to + * lambda term in sol_map such that + * forall y1...yn. P( sol_map[x1]...sol_map[xn], y1...yn ) + * is a valid formula. + */ + void getSynthSolutions(std::map& sol_map); + /** * Do quantifier elimination. * diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp index fc7ec8e52..03c39f718 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.cpp +++ b/src/theory/quantifiers/candidate_rewrite_database.cpp @@ -105,7 +105,7 @@ bool CandidateRewriteDatabase::addTerm(Node sol, std::ostream& out) rrChecker.assertFormula(crr.toExpr()); Result r = rrChecker.checkSat(); Trace("rr-check") << "...result : " << r << std::endl; - if (r.asSatisfiabilityResult().isSat()) + if (r.asSatisfiabilityResult().isSat() == Result::SAT) { Trace("rr-check") << "...rewrite does not hold for: " << std::endl; success = false; diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp index 1ca1902a1..f9208599f 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -209,7 +209,7 @@ bool SygusRepairConst::repairSolution(const std::vector& candidates, repcChecker.assertFormula(fo_body.toExpr()); Result r = repcChecker.checkSat(); Trace("sygus-repair-const") << "...got : " << r << std::endl; - if (r.asSatisfiabilityResult().isSat() + if (r.asSatisfiabilityResult().isSat() != Result::UNSAT && !r.asSatisfiabilityResult().isUnknown()) { std::vector sk_sygus_m; diff --git a/src/theory/quantifiers/sygus_inference.cpp b/src/theory/quantifiers/sygus_inference.cpp index cea992f54..dc6ca56a4 100644 --- a/src/theory/quantifiers/sygus_inference.cpp +++ b/src/theory/quantifiers/sygus_inference.cpp @@ -13,6 +13,9 @@ **/ #include "theory/quantifiers/sygus_inference.h" +#include "smt/smt_engine.h" +#include "smt/smt_engine_scope.h" +#include "smt/smt_statistics_registry.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/quantifiers_rewriter.h" @@ -85,6 +88,15 @@ bool SygusInference::simplify(std::vector& assertions) } if (pas.getKind() == FORALL) { + // it must be a standard quantifier + QAttributes qa; + QuantAttributes::computeQuantAttributes(pas, qa); + if (!qa.isStandard()) + { + Trace("sygus-infer") + << "...fail: non-standard top-level quantifier." << std::endl; + return false; + } // infer prefix for (const Node& v : pas[0]) { @@ -170,10 +182,13 @@ bool SygusInference::simplify(std::vector& assertions) // for each free function symbol, make a bound variable of the same type Trace("sygus-infer") << "Do free function substitution..." << std::endl; std::vector ff_vars; + std::map ff_var_to_ff; for (const Node& ff : free_functions) { Node ffv = nm->mkBoundVar(ff.getType()); ff_vars.push_back(ffv); + Trace("sygus-infer") << " synth-fun: " << ff << " as " << ffv << std::endl; + ff_var_to_ff[ffv] = ff; } // substitute free functions -> variables body = body.substitute(free_functions.begin(), @@ -204,17 +219,66 @@ bool SygusInference::simplify(std::vector& assertions) Trace("sygus-infer") << "*** Return sygus inference : " << body << std::endl; - // replace all assertions except the first with true - Node truen = nm->mkConst(true); - for (unsigned i = 0, size = assertions.size(); i < size; i++) + // make a separate smt call + SmtEngine* master_smte = smt::currentSmtEngine(); + SmtEngine rrSygus(nm->toExprManager()); + rrSygus.setLogic(smt::currentSmtEngine()->getLogicInfo()); + rrSygus.assertFormula(body.toExpr()); + Trace("sygus-infer") << "*** Check sat..." << std::endl; + Result r = rrSygus.checkSat(); + Trace("sygus-infer") << "...result : " << r << std::endl; + if (r.asSatisfiabilityResult().isSat() != Result::UNSAT) + { + // failed, conjecture was infeasible + return false; + } + // get the synthesis solutions + std::map synth_sols; + rrSygus.getSynthSolutions(synth_sols); + + std::vector final_ff; + std::vector final_ff_sol; + for (std::map::iterator it = synth_sols.begin(); + it != synth_sols.end(); + ++it) { - if (i == 0) + Node lambda = Node::fromExpr(it->second); + Trace("sygus-infer") << " synth sol : " << it->first << " -> " + << it->second << std::endl; + Node ffv = Node::fromExpr(it->first); + std::map::iterator itffv = ff_var_to_ff.find(ffv); + // all synthesis solutions should correspond to a variable we introduced + Assert(itffv != ff_var_to_ff.end()); + if (itffv != ff_var_to_ff.end()) { - assertions[i] = body; + Node ff = itffv->second; + std::vector args; + for (const Node& v : lambda[0]) + { + args.push_back(v.toExpr()); + } + Trace("sygus-infer") << "Define " << ff << " as " << it->second + << std::endl; + final_ff.push_back(ff); + final_ff_sol.push_back(it->second); + master_smte->defineFunction(ff.toExpr(), args, it->second[1]); } - else + } + + // apply substitution to everything, should result in SAT + for (unsigned i = 0, size = assertions.size(); i < size; i++) + { + Node prev = assertions[i]; + Node curr = assertions[i].substitute(final_ff.begin(), + final_ff.end(), + final_ff_sol.begin(), + final_ff_sol.end()); + if (curr != prev) { - assertions[i] = truen; + curr = Rewriter::rewrite(curr); + Trace("sygus-infer-debug") + << "...rewrote " << prev << " to " << curr << std::endl; + assertions[i] = curr; } } return true; diff --git a/src/theory/quantifiers/sygus_inference.h b/src/theory/quantifiers/sygus_inference.h index a61cebcc0..cdd5a1008 100644 --- a/src/theory/quantifiers/sygus_inference.h +++ b/src/theory/quantifiers/sygus_inference.h @@ -26,8 +26,12 @@ namespace quantifiers { /** SygusInference * - * A preprocessing utility to turn a set of (quantified) assertions into a - * single SyGuS conjecture. + * A preprocessing utility that turns a set of (quantified) assertions into a + * single SyGuS conjecture. If this is possible, we solve for this single Sygus + * conjecture using a separate copy of the SMT engine. If sygus successfully + * solves the conjecture, we plug the synthesis solutions back into the original + * problem, thus obtaining a set of model substitutions under which the + * assertions should simplify to true. */ class SygusInference { @@ -36,8 +40,12 @@ class SygusInference ~SygusInference() {} /** simplify assertions * - * Either replaces assertions with the negation of an equivalent SyGuS - * conjecture and returns true, or otherwise returns false. + * Either replaces all uninterpreted functions in assertions by their + * interpretation in the solution found by a separate call to an SMT engine + * and returns true, or leaves the assertions unmodified and returns false. + * + * We fail if either a sygus conjecture that corresponds to assertions cannot + * be inferred, or the sygus conjecture we infer is infeasible. */ bool simplify(std::vector& assertions); }; diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index 72bf64ac8..ed2390fe5 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1249,6 +1249,7 @@ REG1_TESTS = \ regress1/quantifiers/extract-nproc.smt2 \ regress1/quantifiers/florian-case-ax.smt2 \ regress1/quantifiers/gauss_init_0030.fof.smt2 \ + regress1/quantifiers/horn-simple.smt2 \ regress1/quantifiers/inst-max-level-segf.smt2 \ regress1/quantifiers/inst-prop-simp.smt2 \ regress1/quantifiers/intersection-example-onelane.proof-node22337.smt2 \ diff --git a/test/regress/regress1/quantifiers/horn-simple.smt2 b/test/regress/regress1/quantifiers/horn-simple.smt2 new file mode 100644 index 000000000..a27d8e0d6 --- /dev/null +++ b/test/regress/regress1/quantifiers/horn-simple.smt2 @@ -0,0 +1,13 @@ +; COMMAND-LINE: --sygus-unif --sygus-infer +; EXPECT: sat +(set-logic UFLIA) +(set-info :status sat) +(declare-fun I (Int) Bool) + +(assert (forall ((x Int)) (=> (= x 0) (I x)))) + +(assert (forall ((x Int)) (=> (and (I x) (< x 1)) (I (+ x 1))))) + +(assert (forall ((x Int)) (=> (I x) (<= x 10)))) + +(check-sat)