summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/smt/quant_elim_solver.cpp20
-rw-r--r--src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp18
-rw-r--r--src/theory/quantifiers/instantiate.cpp98
-rw-r--r--src/theory/quantifiers/instantiate.h59
-rw-r--r--src/theory/quantifiers_engine.cpp5
-rw-r--r--src/theory/quantifiers_engine.h5
6 files changed, 115 insertions, 90 deletions
diff --git a/src/smt/quant_elim_solver.cpp b/src/smt/quant_elim_solver.cpp
index 9a0178cfe..ba11319d3 100644
--- a/src/smt/quant_elim_solver.cpp
+++ b/src/smt/quant_elim_solver.cpp
@@ -99,21 +99,11 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as,
Assert(topq.getKind() == FORALL);
Trace("smt-qe") << "Get qe based on preprocessed quantified formula "
<< topq << std::endl;
- std::vector<std::vector<Node>> insts;
- qe->getInstantiationTermVectors(topq, insts);
- std::vector<Node> vars(ne[0].begin(), ne[0].end());
- std::vector<Node> conjs;
- // apply the instantiation on the original body
- for (const std::vector<Node>& inst : insts)
- {
- // note we do not convert to witness form here, since we could be
- // an internal subsolver
- Subs s;
- s.add(vars, inst);
- Node c = s.apply(ne[1].negate());
- conjs.push_back(c);
- }
- ret = nm->mkAnd(conjs);
+ std::vector<Node> insts;
+ qe->getInstantiations(topq, insts);
+ // note we do not convert to witness form here, since we could be
+ // an internal subsolver (SmtEngine::isInternalSubsolver).
+ ret = nm->mkAnd(insts);
Trace("smt-qe") << "QuantElimSolver returned : " << ret << std::endl;
if (q.getKind() == EXISTS)
{
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index 3690cbcac..19821d347 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -473,23 +473,23 @@ Node InstStrategyCegqi::getCounterexampleLiteral(Node q)
bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) {
Assert(!d_curr_quant.isNull());
+ // check if we need virtual term substitution (if used delta or infinity)
+ bool usedVts = d_vtsCache->containsVtsTerm(subs, false);
Instantiate* inst = d_qim.getInstantiate();
//if doing partial quantifier elimination, record the instantiation and set the incomplete flag instead of sending instantiation lemma
if (d_qreg.getQuantAttributes().isQuantElimPartial(d_curr_quant))
{
d_cbqi_set_quant_inactive = true;
d_incomplete_check = true;
- inst->recordInstantiation(d_curr_quant, subs, false, false);
+ inst->recordInstantiation(d_curr_quant, subs, usedVts);
return true;
}
- // check if we need virtual term substitution (if used delta or infinity)
- bool used_vts = d_vtsCache->containsVtsTerm(subs, false);
- if (inst->addInstantiation(d_curr_quant,
- subs,
- InferenceId::QUANTIFIERS_INST_CEGQI,
- false,
- false,
- used_vts))
+ else if (inst->addInstantiation(d_curr_quant,
+ subs,
+ InferenceId::QUANTIFIERS_INST_CEGQI,
+ false,
+ false,
+ usedVts))
{
return true;
}
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index 61c7703ed..b74f4ae0f 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -51,7 +51,7 @@ Instantiate::Instantiate(QuantifiersState& qs,
d_qreg(qr),
d_treg(tr),
d_pnm(pnm),
- d_total_inst_debug(qs.getUserContext()),
+ d_insts(qs.getUserContext()),
d_c_inst_match_trie_dom(qs.getUserContext()),
d_pfInst(pnm ? new CDProof(pnm) : nullptr)
{
@@ -68,24 +68,16 @@ Instantiate::~Instantiate()
bool Instantiate::reset(Theory::Effort e)
{
- if (!d_recorded_inst.empty())
- {
- Trace("quant-engine-debug") << "Removing " << d_recorded_inst.size()
- << " instantiations..." << std::endl;
- // remove explicitly recorded instantiations
- for (std::pair<Node, std::vector<Node> >& r : d_recorded_inst)
- {
- removeInstantiationInternal(r.first, r.second);
- }
- d_recorded_inst.clear();
- }
+ Trace("inst-debug") << "Reset, effort " << e << std::endl;
+ // clear explicitly recorded instantiations
+ d_recordedInst.clear();
return true;
}
void Instantiate::registerQuantifier(Node q) {}
bool Instantiate::checkComplete()
{
- if (!d_recorded_inst.empty())
+ if (!d_recordedInst.empty())
{
Trace("quant-engine-debug")
<< "Set incomplete due to recorded instantiations." << std::endl;
@@ -337,7 +329,10 @@ bool Instantiate::addInstantiation(Node q,
return false;
}
- d_total_inst_debug[q] = d_total_inst_debug[q] + 1;
+ // add to list of instantiations
+ InstLemmaList* ill = getOrMkInstLemmaList(q);
+ ill->d_list.push_back(body);
+ // add to temporary debug statistics (# inst on this round)
d_temp_inst_debug[q]++;
if (Trace.isOn("inst"))
{
@@ -480,12 +475,16 @@ bool Instantiate::addInstantiationExpFail(Node q,
return false;
}
-bool Instantiate::recordInstantiation(Node q,
+void Instantiate::recordInstantiation(Node q,
std::vector<Node>& terms,
- bool modEq,
- bool addedLem)
+ bool doVts)
{
- return recordInstantiationInternal(q, terms, modEq, addedLem);
+ Trace("inst-debug") << "Record instantiation for " << q << std::endl;
+ // get the instantiation list, which ensures that q is marked as a quantified
+ // formula we instantiated, despite only recording an instantiation here
+ getOrMkInstLemmaList(q);
+ Node inst = getInstantiation(q, terms, doVts);
+ d_recordedInst[q].push_back(inst);
}
bool Instantiate::existsInstantiation(Node q,
@@ -562,14 +561,8 @@ Node Instantiate::getInstantiation(Node q, std::vector<Node>& terms, bool doVts)
bool Instantiate::recordInstantiationInternal(Node q,
std::vector<Node>& terms,
- bool modEq,
- bool addedLem)
+ bool modEq)
{
- if (!addedLem)
- {
- // record the instantiation for deletion later
- d_recorded_inst.push_back(std::pair<Node, std::vector<Node> >(q, terms));
- }
if (options::incrementalSolving())
{
Trace("inst-add-debug")
@@ -607,24 +600,13 @@ bool Instantiate::removeInstantiationInternal(Node q, std::vector<Node>& terms)
return d_inst_match_trie[q].removeInstMatch(q, terms);
}
-void Instantiate::getInstantiatedQuantifiedFormulas(std::vector<Node>& qs)
+void Instantiate::getInstantiatedQuantifiedFormulas(std::vector<Node>& qs) const
{
- if (options::incrementalSolving())
- {
- for (context::CDHashSet<Node, NodeHashFunction>::const_iterator it =
- d_c_inst_match_trie_dom.begin();
- it != d_c_inst_match_trie_dom.end();
- ++it)
- {
- qs.push_back(*it);
- }
- }
- else
+ for (NodeInstListMap::const_iterator it = d_insts.begin();
+ it != d_insts.end();
+ ++it)
{
- for (std::pair<const Node, InstMatchTrie>& t : d_inst_match_trie)
- {
- qs.push_back(t.first);
- }
+ qs.push_back(it->first);
}
}
@@ -671,6 +653,20 @@ void Instantiate::getInstantiationTermVectors(
}
}
+void Instantiate::getInstantiations(Node q, std::vector<Node>& insts)
+{
+ Trace("inst-debug") << "get instantiations for " << q << std::endl;
+ InstLemmaList* ill = getOrMkInstLemmaList(q);
+ insts.insert(insts.end(), ill->d_list.begin(), ill->d_list.end());
+ // also include recorded instantations (for qe-partial)
+ std::map<Node, std::vector<Node> >::const_iterator it =
+ d_recordedInst.find(q);
+ if (it != d_recordedInst.end())
+ {
+ insts.insert(insts.end(), it->second.begin(), it->second.end());
+ }
+}
+
bool Instantiate::isProofEnabled() const { return d_pfInst != nullptr; }
void Instantiate::debugPrint(std::ostream& out)
@@ -705,12 +701,11 @@ void Instantiate::debugPrintModel()
{
if (Trace.isOn("inst-per-quant"))
{
- for (NodeUIntMap::iterator it = d_total_inst_debug.begin();
- it != d_total_inst_debug.end();
+ for (NodeInstListMap::iterator it = d_insts.begin(); it != d_insts.end();
++it)
{
- Trace("inst-per-quant")
- << " * " << (*it).second << " for " << (*it).first << std::endl;
+ Trace("inst-per-quant") << " * " << (*it).second->d_list.size() << " for "
+ << (*it).first << std::endl;
}
}
}
@@ -731,6 +726,19 @@ Node Instantiate::ensureType(Node n, TypeNode tn)
return Node::null();
}
+InstLemmaList* Instantiate::getOrMkInstLemmaList(TNode q)
+{
+ NodeInstListMap::iterator it = d_insts.find(q);
+ if (it != d_insts.end())
+ {
+ return it->second.get();
+ }
+ std::shared_ptr<InstLemmaList> ill =
+ std::make_shared<InstLemmaList>(d_qstate.getUserContext());
+ d_insts.insert(q, ill);
+ return ill.get();
+}
+
Instantiate::Statistics::Statistics()
: d_instantiations("Instantiate::Instantiations_Total", 0),
d_inst_duplicate("Instantiate::Duplicate_Inst", 0),
diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h
index be410c2c8..94e16b526 100644
--- a/src/theory/quantifiers/instantiate.h
+++ b/src/theory/quantifiers/instantiate.h
@@ -69,6 +69,15 @@ class InstantiationRewriter
bool doVts) = 0;
};
+/** Context-dependent list of nodes */
+class InstLemmaList
+{
+ public:
+ InstLemmaList(context::Context* c) : d_list(c) {}
+ /** The list */
+ context::CDList<Node> d_list;
+};
+
/** Instantiate
*
* This class is used for generating instantiation lemmas. It maintains an
@@ -90,7 +99,8 @@ class InstantiationRewriter
*/
class Instantiate : public QuantifiersUtil
{
- typedef context::CDHashMap<Node, uint32_t, NodeHashFunction> NodeUIntMap;
+ using NodeInstListMap = context::
+ CDHashMap<Node, std::shared_ptr<InstLemmaList>, NodeHashFunction>;
public:
Instantiate(QuantifiersState& qs,
@@ -187,13 +197,13 @@ class Instantiate : public QuantifiersUtil
bool expFull = true);
/** record instantiation
*
- * Explicitly record that q has been instantiated with terms. This is the
- * same as addInstantiation, but does not enqueue an instantiation lemma.
+ * Explicitly record that q has been instantiated with terms, with virtual
+ * term substitution if doVts is true. This is the same as addInstantiation,
+ * but does not enqueue an instantiation lemma.
*/
- bool recordInstantiation(Node q,
+ void recordInstantiation(Node q,
std::vector<Node>& terms,
- bool modEq = false,
- bool addedLem = true);
+ bool doVts = false);
/** exists instantiation
*
* Returns true if and only if the instantiation already was added or
@@ -240,7 +250,7 @@ class Instantiate : public QuantifiersUtil
* Get the list of quantified formulas that were instantiated in the current
* user context, store them in qs.
*/
- void getInstantiatedQuantifiedFormulas(std::vector<Node>& qs);
+ void getInstantiatedQuantifiedFormulas(std::vector<Node>& qs) const;
/** get instantiation term vectors
*
* Get term vectors corresponding to for all instantiations lemmas added in
@@ -255,6 +265,11 @@ class Instantiate : public QuantifiersUtil
*/
void getInstantiationTermVectors(
std::map<Node, std::vector<std::vector<Node> > >& insts);
+ /**
+ * Get instantiations for quantified formula q. If q is (forall ((x T)) (P
+ * x)), this is a list of the form (P t1) ... (P tn) for ground terms ti.
+ */
+ void getInstantiations(Node q, std::vector<Node>& insts);
//--------------------------------------end user-level interface utilities
/** Are proofs enabled for this object? */
@@ -281,15 +296,12 @@ class Instantiate : public QuantifiersUtil
private:
/** record instantiation, return true if it was not a duplicate
*
- * addedLem : whether an instantiation lemma was added for the vector we are
- * recording. If this is false, we bookkeep the vector.
* modEq : whether to check for duplication modulo equality in instantiation
* tries (for performance),
*/
bool recordInstantiationInternal(Node q,
std::vector<Node>& terms,
- bool modEq = false,
- bool addedLem = true);
+ bool modEq = false);
/** remove instantiation from the cache */
bool removeInstantiationInternal(Node q, std::vector<Node>& terms);
/**
@@ -297,6 +309,8 @@ class Instantiate : public QuantifiersUtil
* if possible.
*/
static Node ensureType(Node n, TypeNode tn);
+ /** Get or make the instantiation list for quantified formula q */
+ InstLemmaList* getOrMkInstLemmaList(TNode q);
/** Reference to the quantifiers state */
QuantifiersState& d_qstate;
@@ -311,8 +325,19 @@ class Instantiate : public QuantifiersUtil
/** instantiation rewriter classes */
std::vector<InstantiationRewriter*> d_instRewrite;
- /** statistics for debugging total instantiations per quantifier */
- NodeUIntMap d_total_inst_debug;
+ /**
+ * The list of all instantiation lemma bodies per quantifier. This is used
+ * for debugging and for quantifier elimination.
+ */
+ NodeInstListMap d_insts;
+ /** explicitly recorded instantiations
+ *
+ * Sometimes an instantiation is recorded internally but not sent out as a
+ * lemma, for instance, for partial quantifier elimination. This is a map
+ * of these instantiations, for each quantified formula. This map is cleared
+ * on presolve, e.g. it is local to a check-sat call.
+ */
+ std::map<Node, std::vector<Node> > d_recordedInst;
/** statistics for debugging total instantiations per quantifier per round */
std::map<Node, uint32_t> d_temp_inst_debug;
@@ -328,14 +353,6 @@ class Instantiate : public QuantifiersUtil
* is valid.
*/
context::CDHashSet<Node, NodeHashFunction> d_c_inst_match_trie_dom;
-
- /** explicitly recorded instantiations
- *
- * Sometimes an instantiation is recorded internally but not sent out as a
- * lemma, for instance, for partial quantifier elimination. This is a map
- * of these instantiations, for each quantified formula.
- */
- std::vector<std::pair<Node, std::vector<Node> > > d_recorded_inst;
/**
* A CDProof storing instantiation steps.
*/
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 8d8f54768..f1ca0dd9f 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -630,6 +630,11 @@ void QuantifiersEngine::getInstantiationTermVectors( std::map< Node, std::vector
d_qim.getInstantiate()->getInstantiationTermVectors(insts);
}
+void QuantifiersEngine::getInstantiations(Node q, std::vector<Node>& insts)
+{
+ d_qim.getInstantiate()->getInstantiations(q, insts);
+}
+
void QuantifiersEngine::printSynthSolution( std::ostream& out ) {
if (d_qmodules->d_synth_e)
{
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 28f162ddd..d05137e80 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -155,6 +155,11 @@ public:
void getInstantiationTermVectors(
std::map<Node, std::vector<std::vector<Node> > >& insts);
/**
+ * Get instantiations for quantified formula q. If q is (forall ((x T)) (P x)),
+ * this is a list of the form (P t1) ... (P tn) for ground terms ti.
+ */
+ void getInstantiations(Node q, std::vector<Node>& insts);
+ /**
* Get skolemization vectors, where for each quantified formula that was
* skolemized, this is the list of skolems that were used to witness the
* negation of that quantified formula.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback