From 2e1b546811778f2c95f07b70f42e458b0552fab0 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 1 Oct 2019 01:56:57 -0500 Subject: [PATCH] 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. --- src/theory/quantifiers/quantifiers_rewriter.h | 73 ++++++---- .../sygus/ce_guided_single_inv.cpp | 126 +++++++++++++++--- .../quantifiers/sygus/ce_guided_single_inv.h | 14 ++ test/regress/CMakeLists.txt | 2 + .../sygus/cegqi-si-string-triv-2fun.sy | 14 ++ .../regress0/sygus/cegqi-si-string-triv.sy | 12 ++ 6 files changed, 191 insertions(+), 50 deletions(-) create mode 100644 test/regress/regress0/sygus/cegqi-si-string-triv-2fun.sy create mode 100644 test/regress/regress0/sygus/cegqi-si-string-triv.sy 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& args, - std::map& activeMap, - Node n, - std::map& visited); - static void computeArgVec(const std::vector& args, - std::vector& activeArgs, - Node n); - static void computeArgVec2(const std::vector& args, - std::vector& 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& 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& bounds, std::vector& subs, QAttributes& qa); + //-------------------------------------end variable elimination utilities + private: + static int getPurifyIdLit2(Node n, std::map& visited); + static bool addCheckElimChild(std::vector& children, + Node c, + Kind k, + std::map& lit_pol, + bool& childrenChanged); + static void addNodeToOrBuilder(Node n, NodeBuilder<>& t); + static void computeArgs(const std::vector& args, + std::map& activeMap, + Node n, + std::map& visited); + static void computeArgVec(const std::vector& args, + std::vector& activeArgs, + Node n); + static void computeArgVec2(const std::vector& args, + std::vector& activeArgs, + Node n, + Node ipl); + static Node computeProcessTerms2(Node body, + bool hasPol, + bool pol, + std::map& currCond, + int nCurrCond, + std::map& cache, + std::map& icache, + std::vector& new_vars, + std::vector& new_conds, + bool elimExtArith); + static void computeDtTesterIteSplit( + Node n, + std::map& pcons, + std::map >& ncons, + std::vector& 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& 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 args(q[0].begin(), q[0].end()); + // keep solving for variables until a fixed point is reached + std::vector vars; + std::vector subs; + Node body = q[1]; + Node prev; + while (prev != body && !args.empty()) + { + prev = body; + + std::vector varsTmp; + std::vector 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 imap; + for (size_t j = 0, vsize = vars.size(); j < vsize; j++) + { + imap[vars[j]] = subs[j]; + } + std::vector 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 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 */ diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index b47d22492..ca33b45c5 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -887,6 +887,8 @@ set(regress_0_tests regress0/sygus/array-grammar-store.sy regress0/sygus/c100.sy regress0/sygus/ccp16.lus.sy + regress0/sygus/cegqi-si-string-triv.sy + regress0/sygus/cegqi-si-string-triv-2fun.sy regress0/sygus/check-generic-red.sy regress0/sygus/const-var-test.sy regress0/sygus/dt-no-syntax.sy diff --git a/test/regress/regress0/sygus/cegqi-si-string-triv-2fun.sy b/test/regress/regress0/sygus/cegqi-si-string-triv-2fun.sy new file mode 100644 index 000000000..fc8864f55 --- /dev/null +++ b/test/regress/regress0/sygus/cegqi-si-string-triv-2fun.sy @@ -0,0 +1,14 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic ALL) + +(synth-fun f ((x String) (y String)) String) +(synth-fun g ((x String) (y String)) String) + +(declare-var x String) +(declare-var y String) + +(constraint (= (f x y) (str.replace (str.++ x y) "A" "ABCD"))) +(constraint (= (g x y) (str.replace (f x y) "B" "CDE"))) + +(check-synth) diff --git a/test/regress/regress0/sygus/cegqi-si-string-triv.sy b/test/regress/regress0/sygus/cegqi-si-string-triv.sy new file mode 100644 index 000000000..86a68574f --- /dev/null +++ b/test/regress/regress0/sygus/cegqi-si-string-triv.sy @@ -0,0 +1,12 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic ALL) + +(synth-fun f ((x String) (y String)) String) + +(declare-var x String) +(declare-var y String) + +(constraint (= (f x y) (str.replace (str.++ x y) "A" "ABCD"))) + +(check-synth) -- 2.30.2