This was used in the old method for unsat core tracking for instantiation lemmas, which will soon be subsumed.
This is also work towards eliminating the dependencies on quantifiers engine from Instantiate.
read_only = false
help = "use store axiom during ho-elim"
-### Proof options
-
-[[option]]
- name = "trackInstLemmas"
- category = "regular"
- long = "track-inst-lemmas"
- type = "bool"
- default = "false"
- help = "track instantiation lemmas (for proofs, unsat cores, qe and synthesis minimization)"
-
### Output options
[[option]]
<< std::endl;
options::cegqi.set(false);
}
- // Do we need to track instantiations?
- if (options::unsatCores() && !options::trackInstLemmas.wasSetByUser())
- {
- options::trackInstLemmas.set(true);
- }
if ((options::fmfBoundLazy.wasSetByUser() && options::fmfBoundLazy())
|| (options::fmfBoundInt.wasSetByUser() && options::fmfBoundInt()))
return false;
}
-bool InstMatchTrie::recordInstLemma(Node q,
- std::vector<Node>& m,
- Node lem,
- ImtIndexOrder* imtio,
- unsigned index)
-{
- if (index == q[0].getNumChildren()
- || (imtio && index == imtio->d_order.size()))
- {
- setInstLemma(lem);
- return true;
- }
- unsigned i_index = imtio ? imtio->d_order[index] : index;
- std::map<Node, InstMatchTrie>::iterator it = d_data.find(m[i_index]);
- if (it != d_data.end())
- {
- return it->second.recordInstLemma(q, m, lem, imtio, index + 1);
- }
- return false;
-}
-
void InstMatchTrie::print(std::ostream& out,
Node q,
std::vector<TNode>& terms,
}
}
-void InstMatchTrie::getInstantiations(std::vector<Node>& insts,
- Node q,
- std::vector<Node>& terms,
- QuantifiersEngine* qe,
- bool useActive,
- std::vector<Node>& active) const
-{
- if (terms.size() == q[0].getNumChildren())
- {
- if (useActive)
- {
- if (hasInstLemma())
- {
- Node lem = getInstLemma();
- if (std::find(active.begin(), active.end(), lem) != active.end())
- {
- insts.push_back(lem);
- }
- }
- }
- else
- {
- if (hasInstLemma())
- {
- insts.push_back(getInstLemma());
- }
- else if (!options::trackInstLemmas())
- {
- // If we are tracking instantiation lemmas, then hasInstLemma()
- // corresponds exactly to when the lemma was successfully added.
- // Hence the above condition guards the case where the instantiation
- // was recorded but not sent out as a lemma.
- insts.push_back(qe->getInstantiate()->getInstantiation(q, terms, true));
- }
- }
- }
- else
- {
- for (const std::pair<const Node, InstMatchTrie>& d : d_data)
- {
- terms.push_back(d.first);
- d.second.getInstantiations(insts, q, terms, qe, useActive, active);
- terms.pop_back();
- }
- }
-}
-
-void InstMatchTrie::getExplanationForInstLemmas(
- Node q,
- std::vector<Node>& terms,
- const std::vector<Node>& lems,
- std::map<Node, Node>& quant,
- std::map<Node, std::vector<Node> >& tvec) const
-{
- if (terms.size() == q[0].getNumChildren())
- {
- if (hasInstLemma())
- {
- Node lem = getInstLemma();
- if (std::find(lems.begin(), lems.end(), lem) != lems.end())
- {
- quant[lem] = q;
- tvec[lem].clear();
- tvec[lem].insert(tvec[lem].end(), terms.begin(), terms.end());
- }
- }
- }
- else
- {
- for (const std::pair<const Node, InstMatchTrie>& d : d_data)
- {
- terms.push_back(d.first);
- d.second.getExplanationForInstLemmas(q, terms, lems, quant, tvec);
- terms.pop_back();
- }
- }
-}
-
void InstMatchTrie::getInstantiations(
Node q, std::vector<std::vector<Node>>& insts) const
{
return false;
}
-bool CDInstMatchTrie::recordInstLemma(Node q,
- std::vector<Node>& m,
- Node lem,
- unsigned index)
-{
- if (index == q[0].getNumChildren())
- {
- if (d_valid.get())
- {
- setInstLemma(lem);
- return true;
- }
- return false;
- }
- std::map<Node, CDInstMatchTrie*>::iterator it = d_data.find(m[index]);
- if (it != d_data.end())
- {
- return it->second->recordInstLemma(q, m, lem, index + 1);
- }
- return false;
-}
-
void CDInstMatchTrie::print(std::ostream& out,
Node q,
std::vector<TNode>& terms,
}
}
-void CDInstMatchTrie::getInstantiations(std::vector<Node>& insts,
- Node q,
- std::vector<Node>& terms,
- QuantifiersEngine* qe,
- bool useActive,
- std::vector<Node>& active) const
-{
- if (d_valid.get())
- {
- if (terms.size() == q[0].getNumChildren())
- {
- if (useActive)
- {
- if (hasInstLemma())
- {
- Node lem = getInstLemma();
- if (std::find(active.begin(), active.end(), lem) != active.end())
- {
- insts.push_back(lem);
- }
- }
- }
- else
- {
- if (hasInstLemma())
- {
- insts.push_back(getInstLemma());
- }
- else if (!options::trackInstLemmas())
- {
- // Like in the context-independent case, hasInstLemma()
- // corresponds exactly to when the lemma was successfully added when
- // trackInstLemmas() is true.
- insts.push_back(
- qe->getInstantiate()->getInstantiation(q, terms, true));
- }
- }
- }
- else
- {
- for (const std::pair<const Node, CDInstMatchTrie*>& d : d_data)
- {
- terms.push_back(d.first);
- d.second->getInstantiations(insts, q, terms, qe, useActive, active);
- terms.pop_back();
- }
- }
- }
-}
-
-void CDInstMatchTrie::getExplanationForInstLemmas(
- Node q,
- std::vector<Node>& terms,
- const std::vector<Node>& lems,
- std::map<Node, Node>& quant,
- std::map<Node, std::vector<Node> >& tvec) const
-{
- if (d_valid.get())
- {
- if (terms.size() == q[0].getNumChildren())
- {
- if (hasInstLemma())
- {
- Node lem;
- if (std::find(lems.begin(), lems.end(), lem) != lems.end())
- {
- quant[lem] = q;
- tvec[lem].clear();
- tvec[lem].insert(tvec[lem].end(), terms.begin(), terms.end());
- }
- }
- }
- else
- {
- for (const std::pair<const Node, CDInstMatchTrie*>& d : d_data)
- {
- terms.push_back(d.first);
- d.second->getExplanationForInstLemmas(q, terms, lems, quant, tvec);
- terms.pop_back();
- }
- }
- }
-}
-
void CDInstMatchTrie::getInstantiations(
Node q, std::vector<std::vector<Node>>& insts) const
{
std::vector<Node>& m,
ImtIndexOrder* imtio = NULL,
unsigned index = 0);
- /** record instantiation lemma
- *
- * This records that the instantiation lemma lem corresponds to the entry
- * given by (the suffix of) m starting at the given index.
- */
- bool recordInstLemma(Node q,
- std::vector<Node>& m,
- Node lem,
- ImtIndexOrder* imtio = NULL,
- unsigned index = 0);
/**
* Adds the instantiations for q into insts.
*/
void getInstantiations(Node q, std::vector<std::vector<Node>>& insts) const;
- /** get instantiations
- *
- * This gets the set of instantiation lemmas that were recorded in this trie
- * via calls to recordInstLemma. If useActive is true, we only add
- * instantiations that occur in active.
- */
- void getInstantiations(std::vector<Node>& insts,
- Node q,
- QuantifiersEngine* qe,
- bool useActive,
- std::vector<Node>& active)
- {
- std::vector<Node> terms;
- getInstantiations(insts, q, terms, qe, useActive, active);
- }
- /** get explanation for inst lemmas
- *
- * This gets the explanation for the instantiation lemmas in lems for
- * quantified formula q, for which this trie stores instantiation matches for.
- * For each instantiation lemma lem recording in this trie via calls to
- * recordInstLemma, we map lem to q in map quant, and lem to its corresponding
- * vector of terms in tvec.
- */
- void getExplanationForInstLemmas(
- Node q,
- const std::vector<Node>& lems,
- std::map<Node, Node>& quant,
- std::map<Node, std::vector<Node> >& tvec) const
- {
- std::vector<Node> terms;
- getExplanationForInstLemmas(q, terms, lems, quant, tvec);
- }
-
/** clear the data of this class */
void clear() { d_data.clear(); }
/** print this class */
std::vector<TNode>& terms,
bool useActive,
std::vector<Node>& active) const;
- /** helper for get instantiations
- * terms accumulates the path we are on in the trie.
- */
- void getInstantiations(std::vector<Node>& insts,
- Node q,
- std::vector<Node>& terms,
- QuantifiersEngine* qe,
- bool useActive,
- std::vector<Node>& active) const;
- /** helper for get explantaion for inst lemmas
- * terms accumulates the path we are on in the trie.
- */
- void getExplanationForInstLemmas(
- Node q,
- std::vector<Node>& terms,
- const std::vector<Node>& lems,
- std::map<Node, Node>& quant,
- std::map<Node, std::vector<Node> >& tvec) const;
/** set instantiation lemma at this node in the trie */
void setInstLemma(Node n)
{
* The domain of m is the bound variables of quantified formula q.
*/
bool removeInstMatch(Node q, std::vector<Node>& m, unsigned index = 0);
- /** record instantiation lemma
- *
- * This records that the instantiation lemma lem corresponds to the entry
- * given by (the suffix of) m starting at the given index.
- */
- bool recordInstLemma(Node q,
- std::vector<Node>& m,
- Node lem,
- unsigned index = 0);
/**
* Adds the instantiations for q into insts.
*/
void getInstantiations(Node q, std::vector<std::vector<Node>>& insts) const;
- /** get instantiations
- *
- * This gets the set of instantiation lemmas that were recorded in this class
- * via calls to recordInstLemma. If useActive is true, we only add
- * instantiations that occur in active.
- */
- void getInstantiations(std::vector<Node>& insts,
- Node q,
- QuantifiersEngine* qe,
- bool useActive,
- std::vector<Node>& active)
- {
- std::vector<Node> terms;
- getInstantiations(insts, q, terms, qe, useActive, active);
- }
- /** get explanation for inst lemmas
- *
- * This gets the explanation for the instantiation lemmas in lems for
- * quantified formula q, for which this trie stores instantiation matches for.
- * For each instantiation lemma lem recording in this trie via calls to
- * recordInstLemma, we map lem to q in map quant, and lem to its corresponding
- * vector of terms in tvec.
- */
- void getExplanationForInstLemmas(
- Node q,
- const std::vector<Node>& lems,
- std::map<Node, Node>& quant,
- std::map<Node, std::vector<Node> >& tvec) const
- {
- std::vector<Node> terms;
- getExplanationForInstLemmas(q, terms, lems, quant, tvec);
- }
-
/** print this class */
void print(std::ostream& out,
Node q,
orig_body, q[1], maxInstLevel + 1);
}
}
- if (options::trackInstLemmas())
- {
- if (options::incrementalSolving())
- {
- recorded = d_c_inst_match_trie[q]->recordInstLemma(q, terms, lem);
- }
- else
- {
- recorded = d_inst_match_trie[q].recordInstLemma(q, terms, lem);
- }
- Trace("inst-add-debug") << "...was recorded : " << recorded << std::endl;
- Assert(recorded);
- }
Trace("inst-add-debug") << " --> Success." << std::endl;
++(d_statistics.d_instantiations);
return true;
}
}
-bool Instantiate::getUnsatCoreLemmas(std::vector<Node>& active_lemmas)
-{
- // only if unsat core available
- if (options::unsatCores() && !isProofEnabled())
- {
- if (!ProofManager::currentPM()->unsatCoreAvailable())
- {
- return false;
- }
- }
- else
- {
- return false;
- }
-
- Trace("inst-unsat-core") << "Get instantiations in unsat core..."
- << std::endl;
- ProofManager::currentPM()->getLemmasInUnsatCore(active_lemmas);
- if (Trace.isOn("inst-unsat-core"))
- {
- Trace("inst-unsat-core") << "Quantifiers lemmas in unsat core: "
- << std::endl;
- for (const Node& lem : active_lemmas)
- {
- Trace("inst-unsat-core") << " " << lem << std::endl;
- }
- Trace("inst-unsat-core") << std::endl;
- }
- return true;
-}
-
void Instantiate::getInstantiationTermVectors(
Node q, std::vector<std::vector<Node> >& tvecs)
{
- // if track instantiations is true, we use the instantiation + explanation
- // methods for doing minimization based on unsat cores.
- if (options::trackInstLemmas())
- {
- std::vector<Node> lemmas;
- getInstantiations(q, lemmas);
- std::map<Node, Node> quant;
- std::map<Node, std::vector<Node> > tvec;
- getExplanationForInstLemmas(lemmas, quant, tvec);
- for (std::pair<const Node, std::vector<Node> >& t : tvec)
- {
- tvecs.push_back(t.second);
- }
- return;
- }
if (options::incrementalSolving())
{
}
}
-void Instantiate::getExplanationForInstLemmas(
- const std::vector<Node>& lems,
- std::map<Node, Node>& quant,
- std::map<Node, std::vector<Node> >& tvec)
-{
- if (!options::trackInstLemmas())
- {
- std::stringstream msg;
- msg << "Cannot get explanation for instantiations when --track-inst-lemmas "
- "is false.";
- throw OptionException(msg.str());
- }
- if (options::incrementalSolving())
- {
- for (std::pair<const Node, inst::CDInstMatchTrie*>& t : d_c_inst_match_trie)
- {
- t.second->getExplanationForInstLemmas(t.first, lems, quant, tvec);
- }
- }
- else
- {
- for (std::pair<const Node, inst::InstMatchTrie>& t : d_inst_match_trie)
- {
- t.second.getExplanationForInstLemmas(t.first, lems, quant, tvec);
- }
- }
-#ifdef CVC4_ASSERTIONS
- for (unsigned j = 0; j < lems.size(); j++)
- {
- Assert(quant.find(lems[j]) != quant.end());
- Assert(tvec.find(lems[j]) != tvec.end());
- }
-#endif
-}
-
bool Instantiate::isProofEnabled() const { return d_pfInst != nullptr; }
-void Instantiate::getInstantiations(std::map<Node, std::vector<Node> >& insts)
-{
- if (!options::trackInstLemmas())
- {
- std::stringstream msg;
- msg << "Cannot get instantiations when --track-inst-lemmas is false.";
- throw OptionException(msg.str());
- }
- std::vector<Node> active_lemmas;
- bool useUnsatCore = getUnsatCoreLemmas(active_lemmas);
-
- if (options::incrementalSolving())
- {
- for (std::pair<const Node, inst::CDInstMatchTrie*>& t : d_c_inst_match_trie)
- {
- t.second->getInstantiations(
- insts[t.first], t.first, d_qe, useUnsatCore, active_lemmas);
- }
- }
- else
- {
- for (std::pair<const Node, inst::InstMatchTrie>& t : d_inst_match_trie)
- {
- t.second.getInstantiations(
- insts[t.first], t.first, d_qe, useUnsatCore, active_lemmas);
- }
- }
-}
-
-void Instantiate::getInstantiations(Node q, std::vector<Node>& insts)
-{
- if (options::incrementalSolving())
- {
- std::map<Node, inst::CDInstMatchTrie*>::iterator it =
- d_c_inst_match_trie.find(q);
- if (it != d_c_inst_match_trie.end())
- {
- std::vector<Node> active_lemmas;
- it->second->getInstantiations(
- insts, it->first, d_qe, false, active_lemmas);
- }
- }
- else
- {
- std::map<Node, inst::InstMatchTrie>::iterator it =
- d_inst_match_trie.find(q);
- if (it != d_inst_match_trie.end())
- {
- std::vector<Node> active_lemmas;
- it->second.getInstantiations(
- insts, it->first, d_qe, false, active_lemmas);
- }
- }
-}
-
-Node Instantiate::getInstantiatedConjunction(Node q)
-{
- Assert(q.getKind() == FORALL);
- std::vector<Node> insts;
- getInstantiations(q, insts);
- if (insts.empty())
- {
- return NodeManager::currentNM()->mkConst(true);
- }
- Node ret;
- if (insts.size() == 1)
- {
- ret = insts[0];
- }
- else
- {
- ret = NodeManager::currentNM()->mkNode(kind::AND, insts);
- }
- // have to remove q
- // may want to do this in a better way
- TNode tq = q;
- TNode tt = NodeManager::currentNM()->mkConst(true);
- ret = ret.substitute(tq, tt);
- return ret;
-}
-
void Instantiate::debugPrint(std::ostream& out)
{
// debug information
* user context, store them in qs.
*/
void getInstantiatedQuantifiedFormulas(std::vector<Node>& qs);
- /** get instantiations
- *
- * Get the body of all instantiation lemmas added in the current user context
- * for quantified formula q, store them in insts.
- */
- void getInstantiations(Node q, std::vector<Node>& insts);
- /** get instantiations
- *
- * Get the body of all instantiation lemmas added in the current user context
- * for all quantified formulas stored in the domain of insts, store them in
- * the range of insts.
- */
- void getInstantiations(std::map<Node, std::vector<Node> >& insts);
/** 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 instantiated conjunction
- *
- * This gets a conjunction of the bodies of instantiation lemmas added in the
- * current user context for quantified formula q. For example, if we added:
- * ~forall x. P( x ) V P( a )
- * ~forall x. P( x ) V P( b )
- * Then, this method returns P( a ) ^ P( b ).
- */
- Node getInstantiatedConjunction(Node q);
- /** get unsat core lemmas
- *
- * If this method returns true, then it appends to activeLemmas all lemmas
- * that are in the unsat core that originated from the theory of quantifiers.
- * This method returns false if the unsat core is not available.
- */
- bool getUnsatCoreLemmas(std::vector<Node>& activeLemmas);
- /** get explanation for instantiation lemmas
- *
- *
- */
- void getExplanationForInstLemmas(const std::vector<Node>& lems,
- std::map<Node, Node>& quant,
- std::map<Node, std::vector<Node> >& tvec);
//--------------------------------------end user-level interface utilities
/** Are proofs enabled for this object? */
projects / cvc5.git / commitdiff