We require tracking of instantiation lemmas for quantifier elimination. Recently, this feature was removed in favor of reconstructing instantiations via substitutions. This does not quite work if instantiation lemmas have more complex post-processing, e.g. virtual term substitution.
This PR reimplements a much simpler form of instantiation tracking that simply adds instantiation bodies to a vector, per quantified formula. It uses this vector for quantifier elimination.
Fixes #5899.
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)
{
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;
}
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)
{
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;
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"))
{
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,
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")
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);
}
}
}
}
+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)
{
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;
}
}
}
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),
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
*/
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,
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
* 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
*/
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? */
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);
/**
* 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;
/** 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;
* 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.
*/
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)
{
std::vector<std::vector<Node> >& tvecs);
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
regress1/quantifiers/issue5507-qe.smt2
regress1/quantifiers/issue5658-qe.smt2
regress1/quantifiers/issue5766-wrong-sel-trigger.smt2
+ regress1/quantifiers/issue5899-qe.smt2
regress1/quantifiers/issue993.smt2
regress1/quantifiers/javafe.ast.StmtVec.009.smt2
regress1/quantifiers/lia-witness-div-pp.smt2
--- /dev/null
+; SCRUBBER: sed 's/(.*)/()/g'
+; EXPECT: ()
+; EXIT: 0
+
+
+(set-logic LIRA)
+(define-fun
+ __node_init_HH_4
+ ((HH.usr.x@0 Bool)
+ (HH.usr.y@0 Bool)
+ (HH.res.init_flag@0 Bool))
+ Bool
+ (and
+ (= HH.usr.y@0 HH.usr.x@0)
+ HH.res.init_flag@0))
+;; Success
+
+(define-fun
+ __node_trans_HH_4
+ ((HH.usr.x@1 Bool)
+ (HH.usr.y@1 Bool)
+ (HH.res.init_flag@1 Bool)
+ (HH.usr.x@0 Bool)
+ (HH.usr.y@0 Bool)
+ (HH.res.init_flag@0 Bool))
+ Bool
+ (and
+ (= HH.usr.y@1 (or HH.usr.x@1 HH.usr.y@0))
+ (not HH.res.init_flag@1)))
+;; Success
+
+(define-fun
+ __node_init_FTH_4
+ ((FTH.usr.x@0 Bool)
+ (FTH.usr.r@0 Bool)
+ (FTH.res.init_flag@0 Bool)
+ (FTH.res.abs_0@0 Bool)
+ (FTH.res.inst_1@0 Bool))
+ Bool
+ (and
+ (= FTH.usr.r@0 FTH.usr.x@0)
+ (__node_init_HH_4
+ FTH.usr.x@0
+ FTH.res.abs_0@0
+ FTH.res.inst_1@0)
+ FTH.res.init_flag@0))
+;; Success
+
+(define-fun
+ __node_trans_FTH_4
+ ((FTH.usr.x@1 Bool)
+ (FTH.usr.r@1 Bool)
+ (FTH.res.init_flag@1 Bool)
+ (FTH.res.abs_0@1 Bool)
+ (FTH.res.inst_1@1 Bool)
+ (FTH.usr.x@0 Bool)
+ (FTH.usr.r@0 Bool)
+ (FTH.res.init_flag@0 Bool)
+ (FTH.res.abs_0@0 Bool)
+ (FTH.res.inst_1@0 Bool))
+ Bool
+ (and
+ (=
+ FTH.usr.r@1
+ (and (not FTH.res.abs_0@0) FTH.usr.x@1))
+ (__node_trans_HH_4
+ FTH.usr.x@1
+ FTH.res.abs_0@1
+ FTH.res.inst_1@1
+ FTH.usr.x@0
+ FTH.res.abs_0@0
+ FTH.res.inst_1@0)
+ (not FTH.res.init_flag@1)))
+;; Success
+
+(declare-fun %f137@0 () Bool)
+;; Success
+
+(declare-fun %f144@0 () Bool)
+;; Success
+
+(declare-fun %f145@0 () Real)
+;; Success
+
+(declare-fun %f146@0 () Real)
+;; Success
+
+(declare-fun %f147@0 () Int)
+;; Success
+
+(declare-fun %f148@0 () Real)
+;; Success
+
+(declare-fun %f149@0 () Real)
+;; Success
+
+(declare-fun %f136@0 () Bool)
+;; Success
+
+(declare-fun %f150@0 () Bool)
+;; Success
+
+(declare-fun %f151@0 () Bool)
+;; Success
+
+(declare-fun %f152@0 () Bool)
+;; Success
+
+(declare-fun %f154@0 () Bool)
+;; Success
+
+(declare-fun %f155@0 () Bool)
+;; Success
+
+(declare-fun %f156@0 () Bool)
+;; Success
+
+(declare-fun %f157@0 () Bool)
+;; Success
+
+(declare-fun %f158@0 () Bool)
+;; Success
+
+(declare-fun %f275@0 () Bool)
+;; Success
+
+(declare-fun %f274@0 () Bool)
+;; Success
+
+(declare-fun %f273@0 () Bool)
+;; Success
+
+(declare-fun %f272@0 () Bool)
+;; Success
+
+(declare-fun %f271@0 () Bool)
+;; Success
+
+(declare-fun %f137@1 () Bool)
+;; Success
+
+(declare-fun %f144@1 () Bool)
+;; Success
+
+(declare-fun %f145@1 () Real)
+;; Success
+
+(declare-fun %f146@1 () Real)
+;; Success
+
+(declare-fun %f147@1 () Int)
+;; Success
+
+(declare-fun %f148@1 () Real)
+;; Success
+
+(declare-fun %f149@1 () Real)
+;; Success
+
+(declare-fun %f136@1 () Bool)
+;; Success
+
+(declare-fun %f150@1 () Bool)
+;; Success
+
+(declare-fun %f151@1 () Bool)
+;; Success
+
+(declare-fun %f152@1 () Bool)
+;; Success
+
+(declare-fun %f154@1 () Bool)
+;; Success
+
+(declare-fun %f155@1 () Bool)
+;; Success
+
+(declare-fun %f156@1 () Bool)
+;; Success
+
+(declare-fun %f157@1 () Bool)
+;; Success
+
+(declare-fun %f158@1 () Bool)
+;; Success
+
+(declare-fun %f275@1 () Bool)
+;; Success
+
+(declare-fun %f274@1 () Bool)
+;; Success
+
+(declare-fun %f273@1 () Bool)
+;; Success
+
+(declare-fun %f272@1 () Bool)
+;; Success
+
+(declare-fun %f271@1 () Bool)
+;; Success
+
+(get-qe
+ (exists
+ ((X1 Bool)
+ (X2 Bool)
+ (X3 Bool)
+ (X4 Bool)
+ (X5 Bool)
+ (X6 Bool)
+ (X7 Bool)
+ (X8 Bool)
+ (X9 Bool)
+ (X10 Bool)
+ (X11 Bool)
+ (X12 Bool)
+ (X13 Bool)
+ (X14 Bool)
+ (X15 Real)
+ (X16 Real)
+ (X17 Int)
+ (X18 Real)
+ (X19 Real)
+ (X20 Bool)
+ (X21 Bool))
+ (not
+ (or
+ (and
+ (or X21 (not X20))
+ (or
+ (and
+ (not %f150@0)
+ (or
+ (__node_trans_FTH_4
+ false
+ false
+ false
+ true
+ false
+ false
+ %f154@0
+ %f274@0
+ %f273@0
+ %f272@0)
+ (__node_trans_FTH_4
+ false
+ false
+ false
+ false
+ false
+ false
+ %f154@0
+ %f274@0
+ %f273@0
+ %f272@0))
+ (or
+ (__node_trans_HH_4 false true false false %f151@0 %f275@0)
+ (__node_trans_HH_4 false false false false %f151@0 %f275@0))
+ (or
+ (__node_trans_HH_4 false true false %f156@0 %f157@0 %f271@0)
+ (__node_trans_HH_4
+ false
+ false
+ false
+ %f156@0
+ %f157@0
+ %f271@0)))
+ (and
+ %f150@0
+ (__node_trans_HH_4 true true false %f156@0 %f157@0 %f271@0)
+ (or
+ (__node_trans_FTH_4
+ false
+ false
+ false
+ true
+ false
+ true
+ %f154@0
+ %f274@0
+ %f273@0
+ %f272@0)
+ (__node_trans_FTH_4
+ false
+ false
+ false
+ false
+ false
+ true
+ %f154@0
+ %f274@0
+ %f273@0
+ %f272@0))
+ (or
+ (__node_trans_HH_4 false true false true %f151@0 %f275@0)
+ (__node_trans_HH_4 false false false true %f151@0 %f275@0)))))
+ (and
+ X20
+ (not X21)
+ (or
+ (and
+ (not %f150@0)
+ (__node_trans_HH_4 true true false false %f151@0 %f275@0)
+ (or
+ (and
+ (__node_trans_HH_4
+ false
+ true
+ false
+ %f156@0
+ %f157@0
+ %f271@0)
+ (or
+ (__node_trans_FTH_4
+ true
+ false
+ false
+ true
+ false
+ false
+ %f154@0
+ %f274@0
+ %f273@0
+ %f272@0)
+ (and
+ (= %f148@0 X19)
+ (= %f149@0 X18)
+ (__node_trans_FTH_4
+ true
+ true
+ false
+ true
+ false
+ false
+ %f154@0
+ %f274@0
+ %f273@0
+ %f272@0))))
+ (and
+ (__node_trans_HH_4
+ false
+ false
+ false
+ %f156@0
+ %f157@0
+ %f271@0)
+ (or
+ (__node_trans_FTH_4
+ true
+ true
+ false
+ true
+ false
+ false
+ %f154@0
+ %f274@0
+ %f273@0
+ %f272@0)
+ (__node_trans_FTH_4
+ true
+ false
+ false
+ true
+ false
+ false
+ %f154@0
+ %f274@0
+ %f273@0
+ %f272@0)))))
+ (and
+ %f150@0
+ (__node_trans_HH_4 true true false %f156@0 %f157@0 %f271@0)
+ (__node_trans_HH_4 true true false true %f151@0 %f275@0)
+ (or
+ (__node_trans_FTH_4
+ true
+ false
+ false
+ true
+ false
+ true
+ %f154@0
+ %f274@0
+ %f273@0
+ %f272@0)
+ (and
+ (= %f148@0 X19)
+ (= %f149@0 X18)
+ (__node_trans_FTH_4
+ true
+ true
+ false
+ true
+ false
+ true
+ %f154@0
+ %f274@0
+ %f273@0
+ %f272@0))))))))))
+
+(exit)
+;; NoResponse
+
projects / cvc5.git / commitdiff