diff options
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 */ |