InstMatch objects are now fully owned by Triggers. They are passed by reference to InstMatchGenerators.
This also simplifies the interfaces by not passing the quantified formulas.
This is in preparation for making InstMatch objects carry entailment test information.
{
}
-bool IMGenerator::sendInstantiation(InstMatch& m, InferenceId id)
+bool IMGenerator::sendInstantiation(std::vector<Node>& terms, InferenceId id)
{
- return d_tparent->sendInstantiation(m, id);
+ return d_tparent->sendInstantiation(terms, id);
}
} // namespace inst
* instantiation, which it populates in data structure m,
* based on the current context using the implemented matching algorithm.
*
- * q is the quantified formula we are adding instantiations for
- * m is the InstMatch object we are generating
- *
- * Returns a value >0 if an instantiation was successfully generated
+ * @param m the InstMatch object we are generating
+ * @return a value >0 if an instantiation was successfully generated
*/
- virtual int getNextMatch(Node q, InstMatch& m) { return 0; }
+ virtual int getNextMatch(InstMatch& m) { return 0; }
/** add instantiations
*
- * This adds all available instantiations for q based on the current context
- * using the implemented matching algorithm. It typically is implemented as a
- * fixed point of getNextMatch above.
+ * This adds all available instantiations for the quantified formula of m
+ * based on the current context using the implemented matching algorithm. It
+ * typically is implemented as a fixed point of getNextMatch above.
*
* It returns the number of instantiations added using calls to
* Instantiate::addInstantiation(...).
*/
- virtual uint64_t addInstantiations(Node q) { return 0; }
+ virtual uint64_t addInstantiations(InstMatch& m) { return 0; }
/** get active score
*
* A heuristic value indicating how active this generator is.
protected:
/** send instantiation
*
- * This method sends instantiation, specified by m, to the parent trigger
+ * This method sends instantiation, specified by terms, to the parent trigger
* object, which will in turn make a call to
* Instantiate::addInstantiation(...). This method returns true if a
* call to Instantiate::addInstantiation(...) was successfully made,
* indicating that an instantiation was enqueued in the quantifier engine's
* lemma cache.
*/
- bool sendInstantiation(InstMatch& m, InferenceId id);
+ bool sendInstantiation(std::vector<Node>& terms, InferenceId id);
/** The parent trigger that owns this */
Trigger* d_tparent;
/** Reference to the state of the quantifiers engine */
}
/** get match (not modulo equality) */
-int InstMatchGenerator::getMatch(Node f, Node t, InstMatch& m)
+int InstMatchGenerator::getMatch(Node t, InstMatch& m)
{
Trace("matching") << "Matching " << t << " against pattern " << d_match_pattern << " ("
<< m << ")" << ", " << d_children.size() << ", pattern is " << d_pattern << std::endl;
Trace("matching-debug2")
<< "Setting " << ct << " to " << t[i] << "..." << std::endl;
bool addToPrev = m.get(ct).isNull();
- if (!m.set(d_qstate, ct, t[i]))
+ if (!m.set(ct, t[i]))
{
// match is in conflict
Trace("matching-fail")
if (d_match_pattern.getKind() == INST_CONSTANT)
{
bool addToPrev = m.get(d_children_types[0]).isNull();
- if (!m.set(d_qstate, d_children_types[0], t))
+ if (!m.set(d_children_types[0], t))
{
success = false;
}
if (!t_match.isNull())
{
bool addToPrev = m.get(v).isNull();
- if (!m.set(d_qstate, v, t_match))
+ if (!m.set(v, t_match))
{
success = false;
}
if (success)
{
Trace("matching-debug2") << "Continue next " << d_next << std::endl;
- ret_val =
- continueNextMatch(f, m, InferenceId::QUANTIFIERS_INST_E_MATCHING);
+ ret_val = continueNextMatch(m, InferenceId::QUANTIFIERS_INST_E_MATCHING);
}
}
if (ret_val < 0)
return ret_val;
}
-int InstMatchGenerator::continueNextMatch(Node q,
- InstMatch& m,
- InferenceId id)
+int InstMatchGenerator::continueNextMatch(InstMatch& m, InferenceId id)
{
if( d_next!=NULL ){
- return d_next->getNextMatch(q, m);
+ return d_next->getNextMatch(m);
}
if (d_active_add)
{
- return sendInstantiation(m, id) ? 1 : -1;
+ std::vector<Node> mc = m.get();
+ return sendInstantiation(mc, id) ? 1 : -1;
}
return 1;
}
return !d_curr_first_candidate.isNull();
}
-int InstMatchGenerator::getNextMatch(Node f, InstMatch& m)
+int InstMatchGenerator::getNextMatch(InstMatch& m)
{
if( d_needsReset ){
Trace("matching") << "Reset not done yet, must do the reset..." << std::endl;
if( d_curr_exclude_match.find( t )==d_curr_exclude_match.end() ){
Assert(t.getType().isComparableTo(d_match_pattern_type));
Trace("matching-summary") << "Try " << d_match_pattern << " : " << t << std::endl;
- success = getMatch(f, t, m);
+ success = getMatch(t, m);
if( d_independent_gen && success<0 ){
Assert(d_eq_class.isNull() || !d_eq_class_rel.isNull());
d_curr_exclude_match[t] = true;
return success;
}
-uint64_t InstMatchGenerator::addInstantiations(Node f)
+uint64_t InstMatchGenerator::addInstantiations(InstMatch& m)
{
//try to add instantiation for each match produced
uint64_t addedLemmas = 0;
- InstMatch m( f );
- while (getNextMatch(f, m) > 0)
+ m.resetAll();
+ while (getNextMatch(m) > 0)
{
if( !d_active_add ){
- if (sendInstantiation(m, InferenceId::UNKNOWN))
+ std::vector<Node> mc = m.get();
+ if (sendInstantiation(mc, InferenceId::UNKNOWN))
{
addedLemmas++;
if (d_qstate.isInConflict())
break;
}
}
- m.clear();
+ m.resetAll();
}
//return number of lemmas added
return addedLemmas;
/** Reset. */
bool reset(Node eqc) override;
/** Get the next match. */
- int getNextMatch(Node q, InstMatch& m) override;
+ int getNextMatch(InstMatch& m) override;
/** Add instantiations. */
- uint64_t addInstantiations(Node q) override;
+ uint64_t addInstantiations(InstMatch& m) override;
/** set active add flag (true by default)
*
* their match operator (see TermDatabase::getMatchOperator) is the same.
* only valid for use where !d_match_pattern.isNull().
*/
- int getMatch(Node q, Node t, InstMatch& m);
+ int getMatch(Node t, InstMatch& m);
/** Initialize this generator.
*
* q is the quantified formula associated with this generator.
* value >0 if active add is false). Its return value has the same semantics
* as getNextMatch.
*/
- int continueNextMatch(Node q,
- InstMatch& m,
- InferenceId id);
+ int continueNextMatch(InstMatch& m, InferenceId id);
/** Get inst match generator
*
* Gets the InstMatchGenerator that implements the
return true;
}
-uint64_t InstMatchGeneratorMulti::addInstantiations(Node q)
+uint64_t InstMatchGeneratorMulti::addInstantiations(InstMatch& m)
{
uint64_t addedLemmas = 0;
Trace("multi-trigger-cache") << "Process smart multi trigger" << std::endl;
{
Trace("multi-trigger-cache") << "Calculate matches " << i << std::endl;
std::vector<InstMatch> newMatches;
- InstMatch m(q);
- while (d_children[i]->getNextMatch(q, m) > 0)
+ while (d_children[i]->getNextMatch(m) > 0)
{
Trace("multi-trigger-cache2")
<< "...processing new match, #lemmas = " << addedLemmas << std::endl;
{
return addedLemmas;
}
- m.clear();
+ m.resetAll();
}
}
return addedLemmas;
if (childIndex == endChildIndex)
{
// m is an instantiation
- if (sendInstantiation(m, InferenceId::QUANTIFIERS_INST_E_MATCHING_MT))
+ std::vector<Node> mc = m.get();
+ if (sendInstantiation(mc, InferenceId::QUANTIFIERS_INST_E_MATCHING_MT))
{
addedLemmas++;
Trace("multi-trigger-cache-debug")
for (std::pair<const Node, InstMatchTrie>& d : tr->d_data)
{
// try to set
- if (!m.set(qs, curr_index, d.first))
+ if (!m.set(curr_index, d.first))
{
continue;
}
/** Reset. */
bool reset(Node eqc) override;
/** Add instantiations. */
- uint64_t addInstantiations(Node q) override;
+ uint64_t addInstantiations(InstMatch& m) override;
private:
/** process new match
return resetChildren() > 0;
}
-int InstMatchGeneratorMultiLinear::getNextMatch(Node q, InstMatch& m)
+int InstMatchGeneratorMultiLinear::getNextMatch(InstMatch& m)
{
Trace("multi-trigger-linear-debug")
<< "InstMatchGeneratorMultiLinear::getNextMatch : reset " << std::endl;
<< std::endl;
Assert(d_next != nullptr);
int ret_val =
- continueNextMatch(q, m, InferenceId::QUANTIFIERS_INST_E_MATCHING_MTL);
+ continueNextMatch(m, InferenceId::QUANTIFIERS_INST_E_MATCHING_MTL);
if (ret_val > 0)
{
Trace("multi-trigger-linear")
/** Reset. */
bool reset(Node eqc) override;
/** Get the next match. */
- int getNextMatch(Node q, InstMatch& m) override;
+ int getNextMatch(InstMatch& m) override;
protected:
/** reset the children of this generator */
}
void InstMatchGeneratorSimple::resetInstantiationRound() {}
-uint64_t InstMatchGeneratorSimple::addInstantiations(Node q)
+uint64_t InstMatchGeneratorSimple::addInstantiations(InstMatch& m)
{
uint64_t addedLemmas = 0;
TNodeTrie* tat;
{
if (t.first != r)
{
- InstMatch m(q);
+ m.resetAll();
addInstantiations(m, addedLemmas, 0, &(t.second));
if (d_qstate.isInConflict())
{
<< d_eqc << std::endl;
if (tat && !d_qstate.isInConflict())
{
- InstMatch m(q);
+ m.resetAll();
addInstantiations(m, addedLemmas, 0, tat);
}
return addedLemmas;
TNode t = tat->getData();
Trace("simple-trigger") << "Actual term is " << t << std::endl;
// convert to actual used terms
+ std::vector<Node> terms;
+ terms.resize(d_quant[0].getNumChildren());
for (const auto& v : d_var_num)
{
if (v.second >= 0)
Assert(v.first < t.getNumChildren());
Trace("simple-trigger")
<< "...set " << v.second << " " << t[v.first] << std::endl;
- m.setValue(v.second, t[v.first]);
+ terms[v.second] = t[v.first];
}
}
// we do not need the trigger parent for simple triggers (no post-processing
// required)
- if (sendInstantiation(m, InferenceId::QUANTIFIERS_INST_E_MATCHING_SIMPLE))
+ if (sendInstantiation(terms,
+ InferenceId::QUANTIFIERS_INST_E_MATCHING_SIMPLE))
{
addedLemmas++;
- Trace("simple-trigger") << "-> Produced instantiation " << m << std::endl;
+ Trace("simple-trigger")
+ << "-> Produced instantiation " << terms << std::endl;
}
return;
}
for (std::pair<const TNode, TNodeTrie>& tt : tat->d_data)
{
Node t = tt.first;
- Node prev = m.get(v);
// using representatives, just check if equal
Assert(t.getType().isComparableTo(d_match_pattern_arg_types[argIndex]));
- if (prev.isNull() || prev == t)
+ bool wasSet = !m.get(v).isNull();
+ if (!m.set(v, t))
{
- m.setValue(v, t);
- addInstantiations(m, addedLemmas, argIndex + 1, &(tt.second));
- m.setValue(v, prev);
- if (d_qstate.isInConflict())
- {
- break;
- }
+ continue;
+ }
+ addInstantiations(m, addedLemmas, argIndex + 1, &(tt.second));
+ if (!wasSet)
+ {
+ m.reset(v);
+ }
+ if (d_qstate.isInConflict())
+ {
+ break;
}
}
return;
/** Reset instantiation round. */
void resetInstantiationRound() override;
/** Add instantiations. */
- uint64_t addInstantiations(Node q) override;
+ uint64_t addInstantiations(InstMatch& m) override;
/** Get active score. */
int getActiveScore() override;
return true;
}
-int RelationalMatchGenerator::getNextMatch(Node q, InstMatch& m)
+int RelationalMatchGenerator::getNextMatch(InstMatch& m)
{
Trace("relational-match-gen") << "getNextMatch, rel match gen" << std::endl;
// try (up to) two different terms
d_counter++;
Trace("relational-match-gen")
<< "...try set " << s << " for " << checkPol << std::endl;
- if (m.set(d_qstate, d_vindex, s))
+ if (m.set(d_vindex, s))
{
Trace("relational-match-gen") << "...success" << std::endl;
int ret = continueNextMatch(
- q, m, InferenceId::QUANTIFIERS_INST_E_MATCHING_RELATIONAL);
+ m, InferenceId::QUANTIFIERS_INST_E_MATCHING_RELATIONAL);
if (ret > 0)
{
Trace("relational-match-gen") << "...returned " << ret << std::endl;
/** Reset */
bool reset(Node eqc) override;
/** Get the next match. */
- int getNextMatch(Node q, InstMatch& m) override;
+ int getNextMatch(InstMatch& m) override;
private:
/** the variable */
TermRegistry& tr,
Node q,
std::vector<Node>& nodes)
- : EnvObj(env), d_qstate(qs), d_qim(qim), d_qreg(qr), d_treg(tr), d_quant(q)
+ : EnvObj(env),
+ d_qstate(qs),
+ d_qim(qim),
+ d_qreg(qr),
+ d_treg(tr),
+ d_quant(q),
+ d_instMatch(env, qs, tr, q)
{
// We must ensure that the ground subterms of the trigger have been
// preprocessed.
}
}
}
- uint64_t addedLemmas = d_mg->addInstantiations(d_quant);
+ uint64_t addedLemmas = d_mg->addInstantiations(d_instMatch);
if (TraceIsOn("inst-trigger"))
{
if (addedLemmas > 0)
return d_qim.getInstantiate()->addInstantiation(d_quant, m, id, d_trNode);
}
-bool Trigger::sendInstantiation(InstMatch& m, InferenceId id)
-{
- return sendInstantiation(m.get(), id);
-}
-
int Trigger::getActiveScore() { return d_mg->getActiveScore(); }
Node Trigger::ensureGroundTermPreprocessed(Valuation& val,
#include "expr/node.h"
#include "smt/env_obj.h"
#include "theory/inference_id.h"
+#include "theory/quantifiers/inst_match.h"
namespace cvc5::internal {
namespace theory {
-class QuantifiersEngine;
class Valuation;
namespace quantifiers {
+
class QuantifiersState;
class QuantifiersInferenceManager;
class QuantifiersRegistry;
class TermRegistry;
-class InstMatch;
namespace inst {
class IMGenerator;
class InstMatchGenerator;
+
/** A collection of nodes representing a trigger.
*
* This class encapsulates all implementations of E-matching in cvc5.
* Instantiate::addInstantiation(...).
*/
virtual bool sendInstantiation(std::vector<Node>& m, InferenceId id);
- /** inst match version, calls the above method */
- bool sendInstantiation(InstMatch& m, InferenceId id);
/**
* Ensure that all ground subterms of n have been preprocessed. This makes
* calls to the provided valuation to obtain the preprocessed form of these
* algorithm associated with this trigger.
*/
IMGenerator* d_mg;
+ /**
+ * An instantiation match, for building instantiation terms and doing
+ * incremental entailment checking.
+ */
+ InstMatch d_instMatch;
}; /* class Trigger */
} // namespace inst
return true;
}
-int VarMatchGeneratorTermSubs::getNextMatch(Node q, InstMatch& m)
+int VarMatchGeneratorTermSubs::getNextMatch(InstMatch& m)
{
size_t index = d_children_types[0];
int ret_val = -1;
d_eq_class = Node::null();
// if( s.getType().isSubtypeOf( d_var_type ) ){
d_rm_prev = m.get(index).isNull();
- if (!m.set(d_qstate, index, s))
+ if (!m.set(index, s))
{
return -1;
}
else
{
ret_val = continueNextMatch(
- q, m, InferenceId::QUANTIFIERS_INST_E_MATCHING_VAR_GEN);
+ m, InferenceId::QUANTIFIERS_INST_E_MATCHING_VAR_GEN);
if (ret_val > 0)
{
return ret_val;
/** Reset */
bool reset(Node eqc) override;
/** Get the next match. */
- int getNextMatch(Node q, InstMatch& m) override;
+ int getNextMatch(InstMatch& m) override;
private:
/** variable we are matching (x in the example x+1). */
#include "theory/quantifiers/inst_match.h"
+#include "options/quantifiers_options.h"
#include "theory/quantifiers/quantifiers_state.h"
+#include "theory/quantifiers/term_registry.h"
namespace cvc5::internal {
namespace theory {
namespace quantifiers {
-InstMatch::InstMatch(TNode q) : d_quant(q)
+InstMatch::InstMatch(Env& env, QuantifiersState& qs, TermRegistry& tr, TNode q)
+ : EnvObj(env), d_qs(qs), d_tr(tr), d_quant(q)
{
d_vals.resize(q[0].getNumChildren());
Assert(!d_vals.empty());
Assert(d_vals[0].isNull());
}
-void InstMatch::add(InstMatch& m)
-{
- for (unsigned i = 0, size = d_vals.size(); i < size; i++)
- {
- if( d_vals[i].isNull() ){
- d_vals[i] = m.d_vals[i];
- }
- }
-}
-
void InstMatch::debugPrint( const char* c ){
for (unsigned i = 0, size = d_vals.size(); i < size; i++)
{
return true;
}
-void InstMatch::clear() {
- for( unsigned i=0; i<d_vals.size(); i++ ){
+void InstMatch::resetAll()
+{
+ for (size_t i = 0, nvals = d_vals.size(); i < nvals; i++)
+ {
d_vals[i] = Node::null();
}
}
return d_vals[i];
}
-void InstMatch::setValue(size_t i, TNode n)
-{
- Assert(i < d_vals.size());
- d_vals[i] = n;
-}
-
-bool InstMatch::set(QuantifiersState& qs, size_t i, TNode n)
+bool InstMatch::set(size_t i, TNode n)
{
Assert(i < d_vals.size());
if (!d_vals[i].isNull())
{
// if they are equal, we do nothing
- return qs.areEqual(d_vals[i], n);
+ return d_qs.areEqual(d_vals[i], n);
}
// otherwise, we update the value
d_vals[i] = n;
d_vals[i] = Node::null();
}
-std::vector<Node>& InstMatch::get() { return d_vals; }
+const std::vector<Node>& InstMatch::get() const { return d_vals; }
} // namespace quantifiers
} // namespace theory
#include <vector>
#include "expr/node.h"
+#include "smt/env_obj.h"
namespace cvc5::internal {
namespace theory {
namespace quantifiers {
class QuantifiersState;
+class TermRegistry;
/** Inst match
*
* The values of d_vals may be null, which indicate that the field has
* yet to be initialized.
*/
-class InstMatch {
+class InstMatch : protected EnvObj
+{
public:
- InstMatch(TNode q);
- /** add match m
- *
- * This adds the initialized fields of m to this match for each field that is
- * not already initialized in this match.
- */
- void add(InstMatch& m);
+ InstMatch(Env& env, QuantifiersState& qs, TermRegistry& tr, TNode q);
/** is this complete, i.e. are all fields non-null? */
bool isComplete() const;
/** is this empty, i.e. are all fields the null node? */
bool empty() const;
- /** clear the instantiation, i.e. set all fields to the null node */
- void clear();
+ /**
+ * Clear the instantiation, i.e. set all fields to the null node.
+ */
+ void resetAll();
/** debug print method */
void debugPrint(const char* c);
/** to stream */
void toStream(std::ostream& out) const;
/** get the i^th term in the instantiation */
Node get(size_t i) const;
- /** set/overwrites the i^th field in the instantiation with n */
- void setValue(size_t i, TNode n);
/** set the i^th term in the instantiation to n
*
- * This method returns true if the i^th field was previously uninitialized,
- * or is equivalent to n modulo the equalities given by q.
+ * If the d_vals[i] is not null, then this return true iff it is equal to
+ * n based on the quantifiers state.
+ *
+ * If the d_vals[i] is null, then this sets d_vals[i] to n.
+ */
+ bool set(size_t i, TNode n);
+ /**
+ * Resets index i, which sets d_vals[i] to null.
*/
- bool set(QuantifiersState& qs, size_t i, TNode n);
- /** Resets index i */
void reset(size_t i);
/** Get the values */
- std::vector<Node>& get();
+ const std::vector<Node>& get() const;
private:
+ /** Reference to the state */
+ QuantifiersState& d_qs;
+ /** Reference to the term registry */
+ TermRegistry& d_tr;
/**
* Ground terms for each variable of the quantified formula, in order.
* Null nodes indicate the variable has not been set.
projects / cvc5.git / commitdiff