summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/quantifiers/quantifiers_rewriter.h73
-rw-r--r--src/theory/quantifiers/sygus/ce_guided_single_inv.cpp126
-rw-r--r--src/theory/quantifiers/sygus/ce_guided_single_inv.h14
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback