diff options
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/candidate_rewrite_database.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_repair_const.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus_inference.cpp | 78 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus_inference.h | 16 |
4 files changed, 85 insertions, 13 deletions
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<Node>& 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<Node> 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<Node>& 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<Node>& 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<Node> ff_vars; + std::map<Node, Node> 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<Node>& 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<Expr, Expr> synth_sols; + rrSygus.getSynthSolutions(synth_sols); + + std::vector<Node> final_ff; + std::vector<Node> final_ff_sol; + for (std::map<Expr, Expr>::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<Node, Node>::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<Expr> 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<Node>& assertions); }; |