Does not support InstMatch interfaces anymore, which are spurious.
else
{
// do not run higher-order matching
- return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m);
+ return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m.d_vals);
}
}
if (var_index == d_ho_var_list.size())
{
// we now have an instantiation to try
- return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m);
+ return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m.d_vals);
}
else
{
#include <map>
#include "expr/node_trie.h"
-#include "theory/quantifiers/inst_match_trie.h"
+#include "theory/quantifiers/inst_match.h"
namespace CVC4 {
namespace theory {
uint64_t& addedLemmas)
{
// see if these produce new matches
- d_children_trie[fromChildIndex].addInstMatch(qe->getState(), d_quant, m);
+ d_children_trie[fromChildIndex].addInstMatch(
+ qe->getState(), d_quant, m.d_vals);
// possibly only do the following if we know that new matches will be
// produced? the issue is that instantiations are filtered in quantifiers
// engine, and so there is no guarentee that
#include <vector>
#include "expr/node_trie.h"
#include "theory/quantifiers/ematching/inst_match_generator.h"
+#include "theory/quantifiers/inst_match_trie.h"
namespace CVC4 {
namespace theory {
}
// we do not need the trigger parent for simple triggers (no post-processing
// required)
- if (qe->getInstantiate()->addInstantiation(d_quant, m))
+ if (qe->getInstantiate()->addInstantiation(d_quant, m.d_vals))
{
addedLemmas++;
Debug("simple-trigger") << "-> Produced instantiation " << m << std::endl;
bool Trigger::sendInstantiation(InstMatch& m)
{
- return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m);
+ return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m.d_vals);
}
bool Trigger::mkTriggerTerms(Node q,
Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
triedLemmas++;
//add as instantiation
- if (inst->addInstantiation(f, m, true))
+ if (inst->addInstantiation(f, m.d_vals, true))
{
addedLemmas++;
if (d_qstate.isInConflict())
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
- ** \brief Implementation of inst match class
+ ** \brief Implementation of inst match trie class
**/
#include "theory/quantifiers/inst_match_trie.h"
namespace theory {
namespace inst {
+bool InstMatchTrie::existsInstMatch(quantifiers::QuantifiersState& qs,
+ Node q,
+ const std::vector<Node>& m,
+ bool modEq,
+ ImtIndexOrder* imtio,
+ unsigned index)
+{
+ return !addInstMatch(qs, q, m, modEq, imtio, true, index);
+}
+
bool InstMatchTrie::addInstMatch(quantifiers::QuantifiersState& qs,
Node f,
- std::vector<Node>& m,
+ const std::vector<Node>& m,
bool modEq,
ImtIndexOrder* imtio,
bool onlyExist,
}
bool InstMatchTrie::removeInstMatch(Node q,
- std::vector<Node>& m,
+ const std::vector<Node>& m,
ImtIndexOrder* imtio,
unsigned index)
{
void InstMatchTrie::print(std::ostream& out,
Node q,
- std::vector<TNode>& terms,
- bool useActive,
- std::vector<Node>& active) const
+ std::vector<TNode>& terms) const
{
if (terms.size() == q[0].getNumChildren())
{
- bool print;
- if (useActive)
+ out << " ( ";
+ for (unsigned i = 0, size = terms.size(); i < size; i++)
{
- if (hasInstLemma())
- {
- Node lem = getInstLemma();
- print = std::find(active.begin(), active.end(), lem) != active.end();
- }
- else
+ if (i > 0)
{
- print = false;
+ out << ", ";
}
+ out << terms[i];
}
- else
- {
- print = true;
- }
- if (print)
- {
- out << " ( ";
- for (unsigned i = 0, size = terms.size(); i < size; i++)
- {
- if (i > 0)
- {
- out << ", ";
- }
- out << terms[i];
- }
- out << " )" << std::endl;
- }
+ out << " )" << std::endl;
}
else
{
for (const std::pair<const Node, InstMatchTrie>& d : d_data)
{
terms.push_back(d.first);
- d.second.print(out, q, terms, useActive, active);
+ d.second.print(out, q, terms);
terms.pop_back();
}
}
}
}
+void InstMatchTrie::clear() { d_data.clear(); }
+
+void InstMatchTrie::print(std::ostream& out, Node q) const
+{
+ std::vector<TNode> terms;
+ print(out, q, terms);
+}
+
CDInstMatchTrie::~CDInstMatchTrie()
{
for (std::pair<const Node, CDInstMatchTrie*>& d : d_data)
d_data.clear();
}
+bool CDInstMatchTrie::existsInstMatch(quantifiers::QuantifiersState& qs,
+ Node q,
+ const std::vector<Node>& m,
+ bool modEq,
+ unsigned index)
+{
+ return !addInstMatch(qs, q, m, modEq, index, true);
+}
+
bool CDInstMatchTrie::addInstMatch(quantifiers::QuantifiersState& qs,
Node f,
- std::vector<Node>& m,
+ const std::vector<Node>& m,
bool modEq,
unsigned index,
bool onlyExist)
}
bool CDInstMatchTrie::removeInstMatch(Node q,
- std::vector<Node>& m,
+ const std::vector<Node>& m,
unsigned index)
{
if (index == q[0].getNumChildren())
void CDInstMatchTrie::print(std::ostream& out,
Node q,
- std::vector<TNode>& terms,
- bool useActive,
- std::vector<Node>& active) const
+ std::vector<TNode>& terms) const
{
if (d_valid.get())
{
if (terms.size() == q[0].getNumChildren())
{
- bool print;
- if (useActive)
- {
- if (hasInstLemma())
- {
- Node lem = getInstLemma();
- print = std::find(active.begin(), active.end(), lem) != active.end();
- }
- else
- {
- print = false;
- }
- }
- else
- {
- print = true;
- }
- if (print)
+ out << " ( ";
+ for (unsigned i = 0; i < terms.size(); i++)
{
- out << " ( ";
- for (unsigned i = 0; i < terms.size(); i++)
- {
- if (i > 0) out << " ";
- out << terms[i];
- }
- out << " )" << std::endl;
+ if (i > 0) out << " ";
+ out << terms[i];
}
+ out << " )" << std::endl;
}
else
{
for (const std::pair<const Node, CDInstMatchTrie*>& d : d_data)
{
terms.push_back(d.first);
- d.second->print(out, q, terms, useActive, active);
+ d.second->print(out, q, terms);
terms.pop_back();
}
}
}
}
+void CDInstMatchTrie::print(std::ostream& out, Node q) const
+{
+ std::vector<TNode> terms;
+ print(out, q, terms);
+}
+
+bool InstMatchTrieOrdered::addInstMatch(quantifiers::QuantifiersState& qs,
+ Node q,
+ const std::vector<Node>& m,
+ bool modEq)
+{
+ return d_imt.addInstMatch(qs, q, m, modEq, d_imtio);
+}
+
+bool InstMatchTrieOrdered::existsInstMatch(quantifiers::QuantifiersState& qs,
+ Node q,
+ const std::vector<Node>& m,
+ bool modEq)
+{
+ return d_imt.existsInstMatch(qs, q, m, modEq, d_imtio);
+}
+
} /* CVC4::theory::inst namespace */
} /* CVC4::theory namespace */
} /* CVC4 namespace */
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
- ** \brief inst match class
+ ** \brief inst match trie class
**/
#include "cvc4_private.h"
#include "context/cdlist.h"
#include "context/cdo.h"
#include "expr/node.h"
-#include "theory/quantifiers/inst_match.h"
namespace CVC4 {
namespace theory {
class QuantifiersEngine;
-namespace {
+namespace quantifiers {
class QuantifiersState;
}
*/
bool existsInstMatch(quantifiers::QuantifiersState& qs,
Node q,
- InstMatch& m,
+ const std::vector<Node>& m,
bool modEq = false,
- ImtIndexOrder* imtio = NULL,
- unsigned index = 0)
- {
- return !addInstMatch(qs, q, m, modEq, imtio, true, index);
- }
- /** exists inst match, vector version */
- bool existsInstMatch(quantifiers::QuantifiersState& qs,
- Node q,
- std::vector<Node>& m,
- bool modEq = false,
- ImtIndexOrder* imtio = NULL,
- unsigned index = 0)
- {
- return !addInstMatch(qs, q, m, modEq, imtio, true, index);
- }
+ ImtIndexOrder* imtio = nullptr,
+ unsigned index = 0);
/** add inst match
*
* This method adds (the suffix of) m starting at the given index to this
* If modEq is true, we check for duplication modulo equality the current
* equalities in the equality engine of qs.
*/
- bool addInstMatch(quantifiers::QuantifiersState& qs,
- Node q,
- InstMatch& m,
- bool modEq = false,
- ImtIndexOrder* imtio = NULL,
- bool onlyExist = false,
- unsigned index = 0)
- {
- return addInstMatch(qs, q, m.d_vals, modEq, imtio, onlyExist, index);
- }
- /** add inst match, vector version */
bool addInstMatch(quantifiers::QuantifiersState& qs,
Node f,
- std::vector<Node>& m,
+ const std::vector<Node>& m,
bool modEq = false,
- ImtIndexOrder* imtio = NULL,
+ ImtIndexOrder* imtio = nullptr,
bool onlyExist = false,
unsigned index = 0);
/** remove inst match
* The domain of m is the bound variables of quantified formula q.
*/
bool removeInstMatch(Node f,
- std::vector<Node>& m,
- ImtIndexOrder* imtio = NULL,
+ const std::vector<Node>& m,
+ ImtIndexOrder* imtio = nullptr,
unsigned index = 0);
/**
* Adds the instantiations for q into insts.
void getInstantiations(Node q, std::vector<std::vector<Node>>& insts) const;
/** clear the data of this class */
- void clear() { d_data.clear(); }
+ void clear();
/** print this class */
- void print(std::ostream& out,
- Node q,
- bool useActive,
- std::vector<Node>& active) const
- {
- std::vector<TNode> terms;
- print(out, q, terms, useActive, active);
- }
+ void print(std::ostream& out, Node q) const;
/** the data */
std::map<Node, InstMatchTrie> d_data;
/** helper for print
* terms accumulates the path we are on in the trie.
*/
- void print(std::ostream& out,
- Node q,
- std::vector<TNode>& terms,
- bool useActive,
- std::vector<Node>& active) const;
- /** set instantiation lemma at this node in the trie */
- void setInstLemma(Node n)
- {
- d_data.clear();
- d_data[n].clear();
- }
- /** does this node of the trie store an instantiation lemma? */
- bool hasInstLemma() const { return !d_data.empty(); }
- /** get the instantiation lemma stored in this node of the trie */
- Node getInstLemma() const { return d_data.begin()->first; }
+ void print(std::ostream& out, Node q, std::vector<TNode>& terms) const;
};
/** trie for InstMatch objects
*/
bool existsInstMatch(quantifiers::QuantifiersState& qs,
Node q,
- InstMatch& m,
+ const std::vector<Node>& m,
bool modEq = false,
- unsigned index = 0)
- {
- return !addInstMatch(qs, q, m, modEq, index, true);
- }
- /** exists inst match, vector version */
- bool existsInstMatch(quantifiers::QuantifiersState& qs,
- Node q,
- std::vector<Node>& m,
- bool modEq = false,
- unsigned index = 0)
- {
- return !addInstMatch(qs, q, m, modEq, index, true);
- }
+ unsigned index = 0);
/** add inst match
*
* This method adds (the suffix of) m starting at the given index to this
*/
bool addInstMatch(quantifiers::QuantifiersState& qs,
Node q,
- InstMatch& m,
- bool modEq = false,
- unsigned index = 0,
- bool onlyExist = false)
- {
- return addInstMatch(qs, q, m.d_vals, modEq, index, onlyExist);
- }
- /** add inst match, vector version */
- bool addInstMatch(quantifiers::QuantifiersState& qs,
- Node q,
- std::vector<Node>& m,
+ const std::vector<Node>& m,
bool modEq = false,
unsigned index = 0,
bool onlyExist = false);
* It returns true if and only if this entry existed in this trie.
* The domain of m is the bound variables of quantified formula q.
*/
- bool removeInstMatch(Node q, std::vector<Node>& m, unsigned index = 0);
+ bool removeInstMatch(Node q, const std::vector<Node>& m, unsigned index = 0);
/**
* Adds the instantiations for q into insts.
*/
void getInstantiations(Node q, std::vector<std::vector<Node>>& insts) const;
/** print this class */
- void print(std::ostream& out,
- Node q,
- bool useActive,
- std::vector<Node>& active) const
- {
- std::vector<TNode> terms;
- print(out, q, terms, useActive, active);
- }
+ void print(std::ostream& out, Node q) const;
private:
/** Helper for getInstantiations.*/
void getInstantiations(Node q,
std::vector<std::vector<Node>>& insts,
std::vector<Node>& terms) const;
+ /** helper for print
+ * terms accumulates the path we are on in the trie.
+ */
+ void print(std::ostream& out, Node q, std::vector<TNode>& terms) const;
/** the data */
std::map<Node, CDInstMatchTrie*> d_data;
/** is valid */
context::CDO<bool> d_valid;
- /** helper for print
- * terms accumulates the path we are on in the trie.
- */
- void print(std::ostream& out,
- Node q,
- 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 explanation for inst lemma
- * 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)
- {
- d_data.clear();
- d_data[n] = NULL;
- }
- /** does this node of the trie store an instantiation lemma? */
- bool hasInstLemma() const { return !d_data.empty(); }
- /** get the instantiation lemma stored in this node of the trie */
- Node getInstLemma() const { return d_data.begin()->first; }
};
/** inst match trie ordered
*/
bool addInstMatch(quantifiers::QuantifiersState& qs,
Node q,
- InstMatch& m,
- bool modEq = false)
- {
- return d_imt.addInstMatch(qs, q, m, modEq, d_imtio);
- }
+ const std::vector<Node>& m,
+ bool modEq = false);
/** returns true if this trie contains m
*
* This method returns true if the match m exists in this
*/
bool existsInstMatch(quantifiers::QuantifiersState& qs,
Node q,
- InstMatch& m,
- bool modEq = false)
- {
- return d_imt.existsInstMatch(qs, q, m, modEq, d_imtio);
- }
+ const std::vector<Node>& m,
+ bool modEq = false);
private:
/** the ordering */
d_instRewrite.push_back(ir);
}
-bool Instantiate::addInstantiation(
- Node q, InstMatch& m, bool mkRep, bool modEq, bool doVts)
-{
- Assert(q[0].getNumChildren() == m.d_vals.size());
- return addInstantiation(q, m.d_vals, mkRep, modEq, doVts);
-}
-
bool Instantiate::addInstantiation(
Node q, std::vector<Node>& terms, bool mkRep, bool modEq, bool doVts)
{
}
#ifdef CVC4_ASSERTIONS
bool bad_inst = false;
- if (quantifiers::TermUtil::containsUninterpretedConstant(terms[i]))
+ if (TermUtil::containsUninterpretedConstant(terms[i]))
{
Trace("inst") << "***& inst contains uninterpreted constant : "
<< terms[i] << std::endl;
}
else if (options::cegqi())
{
- Node icf = quantifiers::TermUtil::getInstConstAttr(terms[i]);
+ Node icf = TermUtil::getInstConstAttr(terms[i]);
if (!icf.isNull())
{
if (icf == q)
Node body = getInstantiation(q, d_qreg.d_vars[q], terms, doVts, pfTmp.get());
Node orig_body = body;
// now preprocess, storing the trust node for the rewrite
- TrustNode tpBody = quantifiers::QuantifiersRewriter::preprocess(body, true);
+ TrustNode tpBody = QuantifiersRewriter::preprocess(body, true);
if (!tpBody.isNull())
{
Assert(tpBody.getKind() == TrustNodeKind::REWRITE);
return body;
}
-Node Instantiate::getInstantiation(Node q, InstMatch& m, bool doVts)
-{
- Assert(d_qreg.d_vars.find(q) != d_qreg.d_vars.end());
- Assert(m.d_vals.size() == q[0].getNumChildren());
- return getInstantiation(q, d_qreg.d_vars[q], m.d_vals, doVts);
-}
-
Node Instantiate::getInstantiation(Node q, std::vector<Node>& terms, bool doVts)
{
Assert(d_qreg.d_vars.find(q) != d_qreg.d_vars.end());
/** do instantiation specified by m
*
* This function returns true if the instantiation lemma for quantified
- * formula q for the substitution specified by m is successfully enqueued
+ * formula q for the substitution specified by terms is successfully enqueued
* via a call to QuantifiersInferenceManager::addPendingLemma.
* mkRep : whether to take the representatives of the terms in the range of
* the substitution m,
* (5) The instantiation lemma is a duplicate of previously added lemma.
*
*/
- bool addInstantiation(Node q,
- InstMatch& m,
- bool mkRep = false,
- bool modEq = false,
- bool doVts = false);
- /** add instantiation
- *
- * Same as above, but the substitution we are considering maps the variables
- * of q to the vector terms, in order.
- */
bool addInstantiation(Node q,
std::vector<Node>& terms,
bool mkRep = false,
bool modEq = false,
bool doVts = false);
- /** remove pending instantiation
- *
- * Removes the instantiation lemma lem from the instantiation trie.
- */
- bool removeInstantiation(Node q, Node lem, std::vector<Node>& terms);
/** record instantiation
*
* Explicitly record that q has been instantiated with terms. This is the
std::vector<Node>& terms,
bool doVts = false,
LazyCDProof* pf = nullptr);
- /** get instantiation
- *
- * Same as above, but with vars/terms specified by InstMatch m.
- */
- Node getInstantiation(Node q, InstMatch& m, bool doVts = false);
/** get instantiation
*
* Same as above but with vars equal to the bound variables of q.
projects / cvc5.git / commitdiff