diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-10-01 01:56:57 -0500 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-09-30 23:56:57 -0700 |
commit | 2e1b546811778f2c95f07b70f42e458b0552fab0 (patch) | |
tree | e819e393153d339128914477b9bbf0e458bcf4ed /src/theory | |
parent | 8182ab9f7d8d6c732202371c24bafd721ef6cfcc (diff) |
Trivial solve method for single invocation sygus (#3328)
This short circuits CEGQI when the conjecture is solvable by simple equality reasoning. It adds two examples where we previously would have fallen back on enumeration due to not having an instantiation technique for strings, despite the conjectures being trivially solvable.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.h | 73 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/ce_guided_single_inv.cpp | 126 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/ce_guided_single_inv.h | 14 |
3 files changed, 163 insertions, 50 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 7703f01fd..5d5e23c75 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -28,36 +28,9 @@ namespace quantifiers { struct QAttributes; class QuantifiersRewriter { -private: - static int getPurifyIdLit2( Node n, std::map< Node, int >& visited ); public: static bool isLiteral( Node n ); -private: - static bool addCheckElimChild( std::vector< Node >& children, Node c, Kind k, std::map< Node, bool >& lit_pol, bool& childrenChanged ); - static void addNodeToOrBuilder( Node n, NodeBuilder<>& t ); - static void computeArgs(const std::vector<Node>& args, - std::map<Node, bool>& activeMap, - Node n, - std::map<Node, bool>& visited); - static void computeArgVec(const std::vector<Node>& args, - std::vector<Node>& activeArgs, - Node n); - static void computeArgVec2(const std::vector<Node>& args, - std::vector<Node>& activeArgs, - Node n, - Node ipl); - static Node computeProcessTerms2( Node body, bool hasPol, bool pol, std::map< Node, bool >& currCond, int nCurrCond, - std::map< Node, Node >& cache, std::map< Node, Node >& icache, - std::vector< Node >& new_vars, std::vector< Node >& new_conds, bool elimExtArith ); - static void computeDtTesterIteSplit( Node n, std::map< Node, Node >& pcons, std::map< Node, std::map< int, Node > >& ncons, std::vector< Node >& conj ); - /** datatype expand - * - * If v occurs in args and has a datatype type whose index^th constructor is - * C, this method returns a node of the form C( x1, ..., xn ), removes v from - * args and adds x1...xn to args. - */ - static Node datatypeExpand(unsigned index, Node v, std::vector<Node>& args); - //-------------------------------------variable elimination + //-------------------------------------variable elimination utilities /** is variable elimination * * Returns true if v is not a subterm of s, and the type of s is a subtype of @@ -127,6 +100,50 @@ private: std::vector<Node>& bounds, std::vector<Node>& subs, QAttributes& qa); + //-------------------------------------end variable elimination utilities + private: + static int getPurifyIdLit2(Node n, std::map<Node, int>& visited); + static bool addCheckElimChild(std::vector<Node>& children, + Node c, + Kind k, + std::map<Node, bool>& lit_pol, + bool& childrenChanged); + static void addNodeToOrBuilder(Node n, NodeBuilder<>& t); + static void computeArgs(const std::vector<Node>& args, + std::map<Node, bool>& activeMap, + Node n, + std::map<Node, bool>& visited); + static void computeArgVec(const std::vector<Node>& args, + std::vector<Node>& activeArgs, + Node n); + static void computeArgVec2(const std::vector<Node>& args, + std::vector<Node>& activeArgs, + Node n, + Node ipl); + static Node computeProcessTerms2(Node body, + bool hasPol, + bool pol, + std::map<Node, bool>& currCond, + int nCurrCond, + std::map<Node, Node>& cache, + std::map<Node, Node>& icache, + std::vector<Node>& new_vars, + std::vector<Node>& new_conds, + bool elimExtArith); + static void computeDtTesterIteSplit( + Node n, + std::map<Node, Node>& pcons, + std::map<Node, std::map<int, Node> >& ncons, + std::vector<Node>& conj); + /** datatype expand + * + * If v occurs in args and has a datatype type whose index^th constructor is + * C, this method returns a node of the form C( x1, ..., xn ), removes v from + * args and adds x1...xn to args. + */ + static Node datatypeExpand(unsigned index, Node v, std::vector<Node>& args); + + //-------------------------------------variable elimination /** compute variable elimination * * This computes variable elimination rewrites for a body of a quantified diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index c3b9fc28b..96c79e69d 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -20,25 +20,25 @@ #include "smt/smt_statistics_registry.h" #include "theory/arith/arith_msum.h" #include "theory/quantifiers/quantifiers_attributes.h" +#include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/sygus/sygus_grammar_cons.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_enumeration.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" -using namespace CVC4; using namespace CVC4::kind; -using namespace CVC4::theory; -using namespace CVC4::theory::quantifiers; -using namespace std; namespace CVC4 { +namespace theory { +namespace quantifiers { CegSingleInv::CegSingleInv(QuantifiersEngine* qe, SynthConjecture* p) : d_qe(qe), d_parent(p), d_sip(new SingleInvocationPartition), d_sol(new CegSingleInvSol(qe)), + d_isSolved(false), d_single_invocation(false) { @@ -317,7 +317,11 @@ void CegSingleInv::finishInit(bool syntaxRestricted) CegHandledStatus status = CEG_HANDLED; if (d_single_inv.getKind() == FORALL) { - status = CegInstantiator::isCbqiQuant(d_single_inv); + // if the conjecture is not trivially solvable + if (!solveTrivial(d_single_inv)) + { + status = CegInstantiator::isCbqiQuant(d_single_inv); + } } Trace("cegqi-si") << "CegHandledStatus is " << status << std::endl; if (status < CEG_HANDLED) @@ -329,21 +333,8 @@ void CegSingleInv::finishInit(bool syntaxRestricted) d_single_invocation = false; d_single_inv = Node::null(); } - // If we succeeded, mark the quantified formula with the quantifier - // elimination attribute to ensure its structure is preserved - if (!d_single_inv.isNull() && d_single_inv.getKind() == FORALL) - { - Node n_attr = - nm->mkSkolem("qe_si", - nm->booleanType(), - "Auxiliary variable for qe attr for single invocation."); - QuantElimAttribute qea; - n_attr.setAttribute(qea, true); - n_attr = nm->mkNode(INST_ATTRIBUTE, n_attr); - n_attr = nm->mkNode(INST_PATTERN_LIST, n_attr); - d_single_inv = nm->mkNode(FORALL, d_single_inv[0], d_single_inv[1], n_attr); - } } + bool CegSingleInv::solve() { if (d_single_inv.isNull()) @@ -351,12 +342,32 @@ bool CegSingleInv::solve() // not using single invocation techniques return false; } + if (d_isSolved) + { + // already solved, probably via a call to solveTrivial. + return true; + } Trace("cegqi-si") << "Solve using single invocation..." << std::endl; NodeManager* nm = NodeManager::currentNM(); + // Mark the quantified formula with the quantifier elimination attribute to + // ensure its structure is preserved in the query below. + Node siq = d_single_inv; + if (siq.getKind() == FORALL) + { + Node n_attr = + nm->mkSkolem("qe_si", + nm->booleanType(), + "Auxiliary variable for qe attr for single invocation."); + QuantElimAttribute qea; + n_attr.setAttribute(qea, true); + n_attr = nm->mkNode(INST_ATTRIBUTE, n_attr); + n_attr = nm->mkNode(INST_PATTERN_LIST, n_attr); + siq = nm->mkNode(FORALL, siq[0], siq[1], n_attr); + } // solve the single invocation conjecture using a fresh copy of SMT engine SmtEngine siSmt(nm->toExprManager()); siSmt.setLogic(smt::currentSmtEngine()->getLogicInfo()); - siSmt.assertFormula(d_single_inv.toExpr()); + siSmt.assertFormula(siq.toExpr()); Result r = siSmt.checkSat(); Trace("cegqi-si") << "Result: " << r << std::endl; if (r.asSatisfiabilityResult().isSat() != Result::UNSAT) @@ -405,6 +416,7 @@ bool CegSingleInv::solve() Trace("cegqi-si") << " Instantiation Lemma: " << ilem << std::endl; } } + d_isSolved = true; return true; } @@ -606,5 +618,75 @@ Node CegSingleInv::reconstructToSyntax(Node s, } void CegSingleInv::preregisterConjecture(Node q) { d_orig_conjecture = q; } - -} //namespace CVC4 + +bool CegSingleInv::solveTrivial(Node q) +{ + Assert(!d_isSolved); + Assert(d_inst.empty()); + Assert(q.getKind() == FORALL); + // If the conjecture is forall x1...xn. ~(x1 = t1 ^ ... xn = tn), it is + // trivially solvable. + std::vector<Node> args(q[0].begin(), q[0].end()); + // keep solving for variables until a fixed point is reached + std::vector<Node> vars; + std::vector<Node> subs; + Node body = q[1]; + Node prev; + while (prev != body && !args.empty()) + { + prev = body; + + std::vector<Node> varsTmp; + std::vector<Node> subsTmp; + QuantifiersRewriter::getVarElim(body, false, args, varsTmp, subsTmp); + // if we eliminated a variable, update body and reprocess + if (!varsTmp.empty()) + { + Assert(varsTmp.size() == subsTmp.size()); + // remake with eliminated nodes + body = body.substitute( + varsTmp.begin(), varsTmp.end(), subsTmp.begin(), subsTmp.end()); + body = Rewriter::rewrite(body); + // apply to subs + // this ensures we behave correctly if we solve x before y in + // x = y+1 ^ y = 2. + for (size_t i = 0, ssize = subs.size(); i < ssize; i++) + { + subs[i] = subs[i].substitute( + varsTmp.begin(), varsTmp.end(), subsTmp.begin(), subsTmp.end()); + subs[i] = Rewriter::rewrite(subs[i]); + } + vars.insert(vars.end(), varsTmp.begin(), varsTmp.end()); + subs.insert(subs.end(), subsTmp.begin(), subsTmp.end()); + } + } + // if we solved all arguments + if (args.empty()) + { + Trace("cegqi-si-trivial-solve") + << q << " is trivially solvable by substitution " << vars << " -> " + << subs << std::endl; + std::map<Node, Node> imap; + for (size_t j = 0, vsize = vars.size(); j < vsize; j++) + { + imap[vars[j]] = subs[j]; + } + std::vector<Node> inst; + for (const Node& v : q[0]) + { + Assert(imap.find(v) != imap.end()); + inst.push_back(imap[v]); + } + d_inst.push_back(inst); + d_instConds.push_back(NodeManager::currentNM()->mkConst(true)); + d_isSolved = true; + return true; + } + Trace("cegqi-si-trivial-solve") + << q << " is not trivially solvable." << std::endl; + return false; +} + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.h b/src/theory/quantifiers/sygus/ce_guided_single_inv.h index 00e3639f8..0d5af327e 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.h +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.h @@ -76,7 +76,9 @@ class CegSingleInv Node d_orig_solution; Node d_solution; Node d_sygus_solution; + public: + //---------------------------------representation of the solution /** * The list of instantiations that suffice to show the first-order equivalent * of the negated synthesis conjecture is unsatisfiable. @@ -87,6 +89,9 @@ class CegSingleInv * first order conjecture for the term vectors above. */ std::vector<Node> d_instConds; + /** is solved */ + bool d_isSolved; + //---------------------------------end representation of the solution private: // conjecture @@ -168,6 +173,15 @@ class CegSingleInv return Node::null(); } } + + private: + /** solve trivial + * + * If this method returns true, it sets d_isSolved to true and adds + * t1 ... tn to d_inst if it can be shown that (forall x1 ... xn. P) is + * unsatisfiable for instantiation {x1 -> t1 ... xn -> tn}. + */ + bool solveTrivial(Node q); }; }/* namespace CVC4::theory::quantifiers */ |