namespace theory {
namespace inst {
-IMGenerator::IMGenerator(quantifiers::QuantifiersState& qs,
- quantifiers::QuantifiersInferenceManager& qim)
- : d_qstate(qs), d_qim(qim)
+IMGenerator::IMGenerator(Trigger* tparent)
+ : d_tparent(tparent), d_qstate(tparent->d_qstate)
{
}
-bool IMGenerator::sendInstantiation(Trigger* tparent,
- InstMatch& m,
- InferenceId id)
+bool IMGenerator::sendInstantiation(InstMatch& m, InferenceId id)
{
- return tparent->sendInstantiation(m, id);
+ return d_tparent->sendInstantiation(m, id);
}
-InstMatchGenerator::InstMatchGenerator(
- Node pat,
- quantifiers::QuantifiersState& qs,
- quantifiers::QuantifiersInferenceManager& qim)
- : IMGenerator(qs, qim)
+QuantifiersEngine* IMGenerator::getQuantifiersEngine()
+{
+ return d_tparent->d_quantEngine;
+}
+
+InstMatchGenerator::InstMatchGenerator(Trigger* tparent, Node pat)
+ : IMGenerator(tparent)
{
d_cg = nullptr;
d_needsReset = true;
}
}
-int InstMatchGenerator::getActiveScore( QuantifiersEngine * qe ) {
+int InstMatchGenerator::getActiveScore()
+{
if( d_match_pattern.isNull() ){
return -1;
}
- else if (TriggerTermInfo::isAtomicTrigger(d_match_pattern))
+ quantifiers::TermDb* tdb = getQuantifiersEngine()->getTermDatabase();
+ if (TriggerTermInfo::isAtomicTrigger(d_match_pattern))
{
- Node f = qe->getTermDatabase()->getMatchOperator( d_match_pattern );
- unsigned ngt = qe->getTermDatabase()->getNumGroundTerms( f );
+ Node f = tdb->getMatchOperator(d_match_pattern);
+ unsigned ngt = tdb->getNumGroundTerms(f);
Trace("trigger-active-sel-debug") << "Number of ground terms for " << f << " is " << ngt << std::endl;
return ngt;
}else if( d_match_pattern.getKind()==INST_CONSTANT ){
TypeNode tn = d_match_pattern.getType();
- unsigned ngtt = qe->getTermDatabase()->getNumTypeGroundTerms( tn );
+ unsigned ngtt = tdb->getNumTypeGroundTerms(tn);
Trace("trigger-active-sel-debug") << "Number of ground terms for " << tn << " is " << ngtt << std::endl;
return ngtt;
}
}
void InstMatchGenerator::initialize(Node q,
- QuantifiersEngine* qe,
std::vector<InstMatchGenerator*>& gens)
{
if (d_pattern.isNull())
d_match_pattern_type = d_match_pattern.getType();
Trace("inst-match-gen") << "Pattern is " << d_pattern << ", match pattern is "
<< d_match_pattern << std::endl;
- d_match_pattern_op = qe->getTermDatabase()->getMatchOperator(d_match_pattern);
+ quantifiers::TermDb* tdb = getQuantifiersEngine()->getTermDatabase();
+ d_match_pattern_op = tdb->getMatchOperator(d_match_pattern);
// now, collect children of d_match_pattern
Kind mpk = d_match_pattern.getKind();
}
else
{
- InstMatchGenerator* cimg =
- getInstMatchGenerator(q, pat, d_qstate, d_qim);
+ InstMatchGenerator* cimg = getInstMatchGenerator(d_tparent, q, pat);
if (cimg)
{
d_children.push_back(cimg);
}
}
+ QuantifiersEngine* qe = getQuantifiersEngine();
// create candidate generator
if (mpk == APPLY_SELECTOR)
{
{
if (d_pattern.getKind() == APPLY_SELECTOR_TOTAL)
{
- Node selectorExpr = qe->getTermDatabase()->getMatchOperator(d_pattern);
+ Node selectorExpr = tdb->getMatchOperator(d_pattern);
size_t selectorIndex = datatypes::utils::cindexOf(selectorExpr);
const DType& dt = datatypes::utils::datatypeOf(selectorExpr);
const DTypeConstructor& c = dt[selectorIndex];
}
/** get match (not modulo equality) */
-int InstMatchGenerator::getMatch(
- Node f, Node t, InstMatch& m, QuantifiersEngine* qe, Trigger* tparent)
+int InstMatchGenerator::getMatch(Node f, Node t, InstMatch& m)
{
Trace("matching") << "Matching " << t << " against pattern " << d_match_pattern << " ("
<< m << ")" << ", " << d_children.size() << ", pattern is " << d_pattern << std::endl;
// we will be requesting candidates for matching terms for each child
for (size_t i = 0, size = d_children.size(); i < size; i++)
{
- if (!d_children[i]->reset(t[d_children_index[i]], qe))
+ if (!d_children[i]->reset(t[d_children_index[i]]))
{
success = false;
break;
if (success)
{
Trace("matching-debug2") << "Continue next " << d_next << std::endl;
- ret_val = continueNextMatch(
- f, m, qe, tparent, InferenceId::QUANTIFIERS_INST_E_MATCHING);
+ ret_val =
+ continueNextMatch(f, m, InferenceId::QUANTIFIERS_INST_E_MATCHING);
}
}
if (ret_val < 0)
int InstMatchGenerator::continueNextMatch(Node q,
InstMatch& m,
- QuantifiersEngine* qe,
- Trigger* tparent,
InferenceId id)
{
if( d_next!=NULL ){
- return d_next->getNextMatch(q, m, qe, tparent);
+ return d_next->getNextMatch(q, m);
}
if (d_active_add)
{
- return sendInstantiation(tparent, m, id) ? 1 : -1;
+ return sendInstantiation(m, id) ? 1 : -1;
}
return 1;
}
/** reset instantiation round */
-void InstMatchGenerator::resetInstantiationRound( QuantifiersEngine* qe ){
+void InstMatchGenerator::resetInstantiationRound()
+{
if( !d_match_pattern.isNull() ){
Trace("matching-debug2") << this << " reset instantiation round." << std::endl;
d_needsReset = true;
}
}
if( d_next ){
- d_next->resetInstantiationRound( qe );
+ d_next->resetInstantiationRound();
}
d_curr_exclude_match.clear();
}
-bool InstMatchGenerator::reset( Node eqc, QuantifiersEngine* qe ){
+bool InstMatchGenerator::reset(Node eqc)
+{
if (d_cg == nullptr)
{
// we did not properly initialize the candidate generator, thus we fail
return !d_curr_first_candidate.isNull();
}
-int InstMatchGenerator::getNextMatch(Node f,
- InstMatch& m,
- QuantifiersEngine* qe,
- Trigger* tparent)
+int InstMatchGenerator::getNextMatch(Node f, InstMatch& m)
{
if( d_needsReset ){
Trace("matching") << "Reset not done yet, must do the reset..." << std::endl;
- reset( d_eq_class, qe );
+ reset(d_eq_class);
}
d_curr_matched = Node::null();
Trace("matching") << this << " " << d_match_pattern << " get next match " << m << " in eq class " << d_eq_class << 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, qe, tparent);
+ success = getMatch(f, t, m);
if( d_independent_gen && success<0 ){
Assert(d_eq_class.isNull() || !d_eq_class_rel.isNull());
d_curr_exclude_match[t] = true;
Trace("matching-summary") << "..." << d_match_pattern << " failed, reset." << std::endl;
Trace("matching") << this << " failed, reset " << d_eq_class << std::endl;
//we failed, must reset
- reset( d_eq_class, qe );
+ reset(d_eq_class);
}else{
Trace("matching-summary") << "..." << d_match_pattern << " success." << std::endl;
}
return success;
}
-uint64_t InstMatchGenerator::addInstantiations(Node f,
- QuantifiersEngine* qe,
- Trigger* tparent)
+uint64_t InstMatchGenerator::addInstantiations(Node f)
{
//try to add instantiation for each match produced
uint64_t addedLemmas = 0;
InstMatch m( f );
- while (getNextMatch(f, m, qe, tparent) > 0)
+ while (getNextMatch(f, m) > 0)
{
if( !d_active_add ){
- if (sendInstantiation(tparent, m, InferenceId::UNKNOWN))
+ if (sendInstantiation(m, InferenceId::UNKNOWN))
{
addedLemmas++;
if (d_qstate.isInConflict())
return addedLemmas;
}
-InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator(
- Node q,
- Node pat,
- quantifiers::QuantifiersState& qs,
- quantifiers::QuantifiersInferenceManager& qim,
- QuantifiersEngine* qe)
+InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator(Trigger* tparent,
+ Node q,
+ Node pat)
{
std::vector< Node > pats;
pats.push_back( pat );
std::map< Node, InstMatchGenerator * > pat_map_init;
- return mkInstMatchGenerator(q, pats, qs, qim, qe, pat_map_init);
+ return mkInstMatchGenerator(tparent, q, pats, pat_map_init);
}
InstMatchGenerator* InstMatchGenerator::mkInstMatchGeneratorMulti(
- Node q,
- std::vector<Node>& pats,
- quantifiers::QuantifiersState& qs,
- quantifiers::QuantifiersInferenceManager& qim,
- QuantifiersEngine* qe)
+ Trigger* tparent, Node q, std::vector<Node>& pats)
{
Assert(pats.size() > 1);
InstMatchGeneratorMultiLinear* imgm =
- new InstMatchGeneratorMultiLinear(q, pats, qs, qim);
+ new InstMatchGeneratorMultiLinear(tparent, q, pats);
std::vector< InstMatchGenerator* > gens;
- imgm->initialize(q, qe, gens);
+ imgm->initialize(q, gens);
Assert(gens.size() == pats.size());
std::vector< Node > patsn;
std::map< Node, InstMatchGenerator * > pat_map_init;
patsn.push_back( pn );
pat_map_init[pn] = g;
}
- //return mkInstMatchGenerator( q, patsn, qe, pat_map_init );
- imgm->d_next = mkInstMatchGenerator(q, patsn, qs, qim, qe, pat_map_init);
+ imgm->d_next = mkInstMatchGenerator(tparent, q, patsn, pat_map_init);
return imgm;
}
InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator(
+ Trigger* tparent,
Node q,
std::vector<Node>& pats,
- quantifiers::QuantifiersState& qs,
- quantifiers::QuantifiersInferenceManager& qim,
- QuantifiersEngine* qe,
std::map<Node, InstMatchGenerator*>& pat_map_init)
{
size_t pCounter = 0;
InstMatchGenerator* init;
std::map< Node, InstMatchGenerator * >::iterator iti = pat_map_init.find( pats[pCounter] );
if( iti==pat_map_init.end() ){
- init = new InstMatchGenerator(pats[pCounter], qs, qim);
+ init = new InstMatchGenerator(tparent, pats[pCounter]);
}else{
init = iti->second;
}
if( prev ){
prev->d_next = curr;
}
- curr->initialize(q, qe, gens);
+ curr->initialize(q, gens);
prev = curr;
counter++;
}
return oinit;
}
-InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator(
- Node q,
- Node n,
- quantifiers::QuantifiersState& qs,
- quantifiers::QuantifiersInferenceManager& qim)
+InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator(Trigger* tparent,
+ Node q,
+ Node n)
{
if (n.getKind() != INST_CONSTANT)
{
{
Node s = PatternTermSelector::getInversion(n, x);
VarMatchGeneratorTermSubs* vmg =
- new VarMatchGeneratorTermSubs(x, s, qs, qim);
+ new VarMatchGeneratorTermSubs(tparent, x, s);
Trace("var-trigger") << "Term substitution trigger : " << n
<< ", var = " << x << ", subs = " << s << std::endl;
return vmg;
}
}
- return new InstMatchGenerator(n, qs, qim);
+ return new InstMatchGenerator(tparent, n);
}
}/* CVC4::theory::inst namespace */
namespace quantifiers {
class QuantifiersState;
-class QuantifiersInferenceManager;
} // namespace quantifiers
namespace inst {
*/
class IMGenerator {
public:
- IMGenerator(quantifiers::QuantifiersState& qs,
- quantifiers::QuantifiersInferenceManager& qim);
+ IMGenerator(Trigger* tparent);
virtual ~IMGenerator() {}
/** Reset instantiation round.
*
* Called once at beginning of an instantiation round.
*/
- virtual void resetInstantiationRound(QuantifiersEngine* qe) {}
+ virtual void resetInstantiationRound() {}
/** Reset.
*
* eqc is the equivalence class to search in (any if eqc=null).
* otherwise. An example of when it returns false is if it can be determined
* that no appropriate matchable terms occur based on eqc.
*/
- virtual bool reset(Node eqc, QuantifiersEngine* qe) { return true; }
+ virtual bool reset(Node eqc) { return true; }
/** Get the next match.
*
* Must call reset( eqc ) before this function. This constructs an
*
* Returns a value >0 if an instantiation was successfully generated
*/
- virtual int getNextMatch(Node q,
- InstMatch& m,
- QuantifiersEngine* qe,
- Trigger* tparent)
- {
- return 0;
- }
- /** add instantiations
+ virtual int getNextMatch(Node q, InstMatch& m) { return 0; }
+ /** add instantiations
*
* This add all available instantiations for q based on the current context
* using the implemented matching algorithm. It typically is implemented as a
* It returns the number of instantiations added using calls to calls to
* Instantiate::addInstantiation(...).
*/
- virtual uint64_t addInstantiations(Node q,
- QuantifiersEngine* qe,
- Trigger* tparent)
- {
- return 0;
- }
- /** get active score
+ virtual uint64_t addInstantiations(Node q) { return 0; }
+ /** get active score
*
* A heuristic value indicating how active this generator is.
*/
- virtual int getActiveScore( QuantifiersEngine * qe ) { return 0; }
- protected:
- /** send instantiation
- *
- * This method sends instantiation, specified by m, 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(Trigger* tparent, InstMatch& m, InferenceId id);
- /** The state of the quantifiers engine */
- quantifiers::QuantifiersState& d_qstate;
- /** The quantifiers inference manager */
- quantifiers::QuantifiersInferenceManager& d_qim;
+ virtual int getActiveScore() { return 0; }
+
+protected:
+ /** send instantiation
+ *
+ * This method sends instantiation, specified by m, 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);
+ /** The parent trigger that owns this */
+ Trigger* d_tparent;
+ /** The state of the quantifiers engine */
+ quantifiers::QuantifiersState& d_qstate;
+ // !!!!!!!!! temporarily available (project #15)
+ QuantifiersEngine* getQuantifiersEngine();
};/* class IMGenerator */
class CandidateGenerator;
~InstMatchGenerator() override;
/** Reset instantiation round. */
- void resetInstantiationRound(QuantifiersEngine* qe) override;
+ void resetInstantiationRound() override;
/** Reset. */
- bool reset(Node eqc, QuantifiersEngine* qe) override;
+ bool reset(Node eqc) override;
/** Get the next match. */
- int getNextMatch(Node q,
- InstMatch& m,
- QuantifiersEngine* qe,
- Trigger* tparent) override;
+ int getNextMatch(Node q, InstMatch& m) override;
/** Add instantiations. */
- uint64_t addInstantiations(Node q,
- QuantifiersEngine* qe,
- Trigger* tparent) override;
+ uint64_t addInstantiations(Node q) override;
/** set active add flag (true by default)
*
*
* See Trigger::getActiveScore for details.
*/
- int getActiveScore(QuantifiersEngine* qe) override;
+ int getActiveScore() override;
/** exclude match
*
* Exclude matching d_match_pattern with Node n on subsequent calls to
void setIndependent() { d_independent_gen = true; }
//-------------------------------construction of inst match generators
/** mkInstMatchGenerator for single triggers, calls the method below */
- static InstMatchGenerator* mkInstMatchGenerator(
- Node q,
- Node pat,
- quantifiers::QuantifiersState& qs,
- quantifiers::QuantifiersInferenceManager& qim,
- QuantifiersEngine* qe);
+ static InstMatchGenerator* mkInstMatchGenerator(Trigger* tparent,
+ Node q,
+ Node pat);
/** mkInstMatchGenerator for the multi trigger case
*
* This linked list of InstMatchGenerator classes with one
* InstMatchGenerators corresponding to each unique subterm of pats with
* free variables.
*/
- static InstMatchGenerator* mkInstMatchGeneratorMulti(
- Node q,
- std::vector<Node>& pats,
- quantifiers::QuantifiersState& qs,
- quantifiers::QuantifiersInferenceManager& qim,
- QuantifiersEngine* qe);
+ static InstMatchGenerator* mkInstMatchGeneratorMulti(Trigger* tparent,
+ Node q,
+ std::vector<Node>& pats);
/** mkInstMatchGenerator
*
* This generates a linked list of InstMatchGenerators for each unique
* It calls initialize(...) for all InstMatchGenerators generated by this call.
*/
static InstMatchGenerator* mkInstMatchGenerator(
+ Trigger* tparent,
Node q,
std::vector<Node>& pats,
- quantifiers::QuantifiersState& qs,
- quantifiers::QuantifiersInferenceManager& qim,
- QuantifiersEngine* qe,
std::map<Node, InstMatchGenerator*>& pat_map_init);
//-------------------------------end construction of inst match generators
* These are intentionally private, and are called during linked list
* construction in mkInstMatchGenerator.
*/
- InstMatchGenerator(Node pat,
- quantifiers::QuantifiersState& qs,
- quantifiers::QuantifiersInferenceManager& qim);
+ InstMatchGenerator(Trigger* tparent, Node pat);
/** The pattern we are producing matches for.
*
* This term and d_match_pattern can be different since this
* 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, QuantifiersEngine* qe, Trigger* tparent);
+ int getMatch(Node q, Node t, InstMatch& m);
/** Initialize this generator.
*
* q is the quantified formula associated with this generator.
* constructed in this way, it adds them to gens.
*/
void initialize(Node q,
- QuantifiersEngine* qe,
std::vector<InstMatchGenerator*>& gens);
/** Continue next match
*
*/
int continueNextMatch(Node q,
InstMatch& m,
- QuantifiersEngine* qe,
- Trigger* tparent,
InferenceId id);
/** Get inst match generator
*
* appropriate matching algorithm for n within q
* within a linked list of InstMatchGenerators.
*/
- static InstMatchGenerator* getInstMatchGenerator(
- Node q,
- Node n,
- quantifiers::QuantifiersState& qs,
- quantifiers::QuantifiersInferenceManager& qim);
+ static InstMatchGenerator* getInstMatchGenerator(Trigger* tparent,
+ Node q,
+ Node n);
};/* class InstMatchGenerator */
}
namespace theory {
namespace inst {
-InstMatchGeneratorMulti::InstMatchGeneratorMulti(
- Node q,
- std::vector<Node>& pats,
- quantifiers::QuantifiersState& qs,
- quantifiers::QuantifiersInferenceManager& qim,
- QuantifiersEngine* qe)
- : IMGenerator(qs, qim), d_quant(q)
+InstMatchGeneratorMulti::InstMatchGeneratorMulti(Trigger* tparent,
+ Node q,
+ std::vector<Node>& pats)
+ : IMGenerator(tparent), d_quant(q)
{
Trace("multi-trigger-cache")
<< "Making smart multi-trigger for " << q << std::endl;
Node n = pats[i];
// make the match generator
InstMatchGenerator* img =
- InstMatchGenerator::mkInstMatchGenerator(q, n, qs, qim, qe);
+ InstMatchGenerator::mkInstMatchGenerator(tparent, q, n);
img->setActiveAdd(false);
d_children.push_back(img);
// compute unique/shared variables
/** reset instantiation round (call this whenever equivalence classes have
* changed) */
-void InstMatchGeneratorMulti::resetInstantiationRound(QuantifiersEngine* qe)
+void InstMatchGeneratorMulti::resetInstantiationRound()
{
for (InstMatchGenerator* c : d_children)
{
- c->resetInstantiationRound(qe);
+ c->resetInstantiationRound();
}
}
/** reset, eqc is the equivalence class to search in (any if eqc=null) */
-bool InstMatchGeneratorMulti::reset(Node eqc, QuantifiersEngine* qe)
+bool InstMatchGeneratorMulti::reset(Node eqc)
{
for (InstMatchGenerator* c : d_children)
{
- if (!c->reset(eqc, qe))
+ if (!c->reset(eqc))
{
// do not return false here
}
return true;
}
-uint64_t InstMatchGeneratorMulti::addInstantiations(Node q,
- QuantifiersEngine* qe,
- Trigger* tparent)
+uint64_t InstMatchGeneratorMulti::addInstantiations(Node q)
{
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, qe, tparent) > 0)
+ while (d_children[i]->getNextMatch(q, m) > 0)
{
// m.makeRepresentative( qe );
newMatches.push_back(InstMatch(&m));
Trace("multi-trigger-cache2")
<< "...processing " << j << " / " << newMatches.size()
<< ", #lemmas = " << addedLemmas << std::endl;
- processNewMatch(qe, tparent, newMatches[j], i, addedLemmas);
- if (qe->getState().isInConflict())
+ processNewMatch(newMatches[j], i, addedLemmas);
+ if (d_qstate.isInConflict())
{
return addedLemmas;
}
return addedLemmas;
}
-void InstMatchGeneratorMulti::processNewMatch(QuantifiersEngine* qe,
- Trigger* tparent,
- InstMatch& m,
+void InstMatchGeneratorMulti::processNewMatch(InstMatch& m,
size_t fromChildIndex,
uint64_t& addedLemmas)
{
// see if these produce new matches
- d_children_trie[fromChildIndex].addInstMatch(
- qe->getState(), d_quant, m.d_vals);
+ d_children_trie[fromChildIndex].addInstMatch(d_qstate, 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
<< "Child " << fromChildIndex << " produced match " << m << std::endl;
// process new instantiations
size_t childIndex = (fromChildIndex + 1) % d_children.size();
- processNewInstantiations(qe,
- tparent,
- m,
+ processNewInstantiations(m,
addedLemmas,
d_children_trie[childIndex].getTrie(),
0,
true);
}
-void InstMatchGeneratorMulti::processNewInstantiations(QuantifiersEngine* qe,
- Trigger* tparent,
- InstMatch& m,
+void InstMatchGeneratorMulti::processNewInstantiations(InstMatch& m,
uint64_t& addedLemmas,
InstMatchTrie* tr,
size_t trieIndex,
size_t endChildIndex,
bool modEq)
{
- Assert(!qe->getState().isInConflict());
+ Assert(!d_qstate.isInConflict());
if (childIndex == endChildIndex)
{
// m is an instantiation
- if (sendInstantiation(
- tparent, m, InferenceId::QUANTIFIERS_INST_E_MATCHING_MT))
+ if (sendInstantiation(m, InferenceId::QUANTIFIERS_INST_E_MATCHING_MT))
{
addedLemmas++;
Trace("multi-trigger-cache-debug")
{
InstMatch mn(&m);
mn.setValue(curr_index, d.first);
- processNewInstantiations(qe,
- tparent,
- mn,
+ processNewInstantiations(mn,
addedLemmas,
&(d.second),
trieIndex + 1,
childIndex,
endChildIndex,
modEq);
- if (qe->getState().isInConflict())
+ if (d_qstate.isInConflict())
{
break;
}
std::map<Node, InstMatchTrie>::iterator it = tr->d_data.find(n);
if (it != tr->d_data.end())
{
- processNewInstantiations(qe,
- tparent,
- m,
+ processNewInstantiations(m,
addedLemmas,
&(it->second),
trieIndex + 1,
{
return;
}
- quantifiers::QuantifiersState& qs = qe->getState();
+ quantifiers::QuantifiersState& qs = d_qstate;
// check modulo equality for other possible instantiations
if (!qs.hasTerm(n))
{
std::map<Node, InstMatchTrie>::iterator itc = tr->d_data.find(en);
if (itc != tr->d_data.end())
{
- processNewInstantiations(qe,
- tparent,
- m,
+ processNewInstantiations(m,
addedLemmas,
&(itc->second),
trieIndex + 1,
childIndex,
endChildIndex,
modEq);
- if (qe->getState().isInConflict())
+ if (d_qstate.isInConflict())
{
break;
}
else
{
size_t newChildIndex = (childIndex + 1) % d_children.size();
- processNewInstantiations(qe,
- tparent,
- m,
+ processNewInstantiations(m,
addedLemmas,
d_children_trie[newChildIndex].getTrie(),
0,
{
public:
/** constructors */
- InstMatchGeneratorMulti(Node q,
- std::vector<Node>& pats,
- quantifiers::QuantifiersState& qs,
- quantifiers::QuantifiersInferenceManager& qim,
- QuantifiersEngine* qe);
+ InstMatchGeneratorMulti(Trigger* tparent, Node q, std::vector<Node>& pats);
/** destructor */
~InstMatchGeneratorMulti() override;
/** Reset instantiation round. */
- void resetInstantiationRound(QuantifiersEngine* qe) override;
+ void resetInstantiationRound() override;
/** Reset. */
- bool reset(Node eqc, QuantifiersEngine* qe) override;
+ bool reset(Node eqc) override;
/** Add instantiations. */
- uint64_t addInstantiations(Node q,
- QuantifiersEngine* qe,
- Trigger* tparent) override;
+ uint64_t addInstantiations(Node q) override;
private:
/** process new match
* addedLemmas is how many instantiations we succesfully send
* via IMGenerator::sendInstantiation(...) calls.
*/
- void processNewMatch(QuantifiersEngine* qe,
- Trigger* tparent,
- InstMatch& m,
+ void processNewMatch(InstMatch& m,
size_t fromChildIndex,
uint64_t& addedLemmas);
/** helper for process new match
* computed by this function returns to.
* modEq is whether we are matching modulo equality.
*/
- void processNewInstantiations(QuantifiersEngine* qe,
- Trigger* tparent,
- InstMatch& m,
+ void processNewInstantiations(InstMatch& m,
uint64_t& addedLemmas,
InstMatchTrie* tr,
size_t trieIndex,
namespace inst {
InstMatchGeneratorMultiLinear::InstMatchGeneratorMultiLinear(
- Node q,
- std::vector<Node>& pats,
- quantifiers::QuantifiersState& qs,
- quantifiers::QuantifiersInferenceManager& qim)
- : InstMatchGenerator(Node::null(), qs, qim)
+ Trigger* tparent, Node q, std::vector<Node>& pats)
+ : InstMatchGenerator(tparent, Node::null())
{
// order patterns to maximize eager matching failures
std::map<Node, std::vector<Node> > var_contains;
{
Node po = pats_ordered[i];
Trace("multi-trigger-linear") << "...make for " << po << std::endl;
- InstMatchGenerator* cimg = getInstMatchGenerator(q, po, qs, qim);
+ InstMatchGenerator* cimg = getInstMatchGenerator(tparent, q, po);
Assert(cimg != nullptr);
d_children.push_back(cimg);
// this could be improved
}
}
-int InstMatchGeneratorMultiLinear::resetChildren(QuantifiersEngine* qe)
+int InstMatchGeneratorMultiLinear::resetChildren()
{
for (InstMatchGenerator* c : d_children)
{
- if (!c->reset(Node::null(), qe))
+ if (!c->reset(Node::null()))
{
return -2;
}
return 1;
}
-bool InstMatchGeneratorMultiLinear::reset(Node eqc, QuantifiersEngine* qe)
+bool InstMatchGeneratorMultiLinear::reset(Node eqc)
{
Assert(eqc.isNull());
if (options::multiTriggerLinear())
{
return true;
}
- return resetChildren(qe) > 0;
+ return resetChildren() > 0;
}
-int InstMatchGeneratorMultiLinear::getNextMatch(Node q,
- InstMatch& m,
- QuantifiersEngine* qe,
- Trigger* tparent)
+int InstMatchGeneratorMultiLinear::getNextMatch(Node q, InstMatch& m)
{
Trace("multi-trigger-linear-debug")
<< "InstMatchGeneratorMultiLinear::getNextMatch : reset " << std::endl;
if (options::multiTriggerLinear())
{
// reset everyone
- int rc_ret = resetChildren(qe);
+ int rc_ret = resetChildren();
if (rc_ret < 0)
{
return rc_ret;
<< "InstMatchGeneratorMultiLinear::getNextMatch : continue match "
<< std::endl;
Assert(d_next != nullptr);
- int ret_val = continueNextMatch(
- q, m, qe, tparent, InferenceId::QUANTIFIERS_INST_E_MATCHING_MTL);
+ int ret_val =
+ continueNextMatch(q, m, InferenceId::QUANTIFIERS_INST_E_MATCHING_MTL);
if (ret_val > 0)
{
Trace("multi-trigger-linear")
public:
/** Reset. */
- bool reset(Node eqc, QuantifiersEngine* qe) override;
+ bool reset(Node eqc) override;
/** Get the next match. */
- int getNextMatch(Node q,
- InstMatch& m,
- QuantifiersEngine* qe,
- Trigger* tparent) override;
+ int getNextMatch(Node q, InstMatch& m) override;
protected:
/** reset the children of this generator */
- int resetChildren(QuantifiersEngine* qe);
+ int resetChildren();
/** constructor */
- InstMatchGeneratorMultiLinear(Node q,
- std::vector<Node>& pats,
- quantifiers::QuantifiersState& qs,
- quantifiers::QuantifiersInferenceManager& qim);
+ InstMatchGeneratorMultiLinear(Trigger* tparent,
+ Node q,
+ std::vector<Node>& pats);
};
} // namespace inst
namespace theory {
namespace inst {
-InstMatchGeneratorSimple::InstMatchGeneratorSimple(
- Node q,
- Node pat,
- quantifiers::QuantifiersState& qs,
- quantifiers::QuantifiersInferenceManager& qim,
- QuantifiersEngine* qe)
- : IMGenerator(qs, qim), d_quant(q), d_match_pattern(pat)
+InstMatchGeneratorSimple::InstMatchGeneratorSimple(Trigger* tparent,
+ Node q,
+ Node pat)
+ : IMGenerator(tparent), d_quant(q), d_match_pattern(pat)
{
if (d_match_pattern.getKind() == NOT)
{
}
d_match_pattern_arg_types.push_back(d_match_pattern[i].getType());
}
- d_op = qe->getTermDatabase()->getMatchOperator(d_match_pattern);
+ quantifiers::TermDb* tdb = getQuantifiersEngine()->getTermDatabase();
+ d_op = tdb->getMatchOperator(d_match_pattern);
}
-void InstMatchGeneratorSimple::resetInstantiationRound(QuantifiersEngine* qe) {}
-uint64_t InstMatchGeneratorSimple::addInstantiations(Node q,
- QuantifiersEngine* qe,
- Trigger* tparent)
+void InstMatchGeneratorSimple::resetInstantiationRound() {}
+uint64_t InstMatchGeneratorSimple::addInstantiations(Node q)
{
- quantifiers::QuantifiersState& qs = qe->getState();
uint64_t addedLemmas = 0;
TNodeTrie* tat;
+ quantifiers::TermDb* tdb = getQuantifiersEngine()->getTermDatabase();
if (d_eqc.isNull())
{
- tat = qe->getTermDatabase()->getTermArgTrie(d_op);
+ tat = tdb->getTermArgTrie(d_op);
}
else
{
if (d_pol)
{
- tat = qe->getTermDatabase()->getTermArgTrie(d_eqc, d_op);
+ tat = tdb->getTermArgTrie(d_eqc, d_op);
}
else
{
// iterate over all classes except r
- tat = qe->getTermDatabase()->getTermArgTrie(Node::null(), d_op);
- if (tat && !qs.isInConflict())
+ tat = tdb->getTermArgTrie(Node::null(), d_op);
+ if (tat && !d_qstate.isInConflict())
{
- Node r = qs.getRepresentative(d_eqc);
+ Node r = d_qstate.getRepresentative(d_eqc);
for (std::pair<const TNode, TNodeTrie>& t : tat->d_data)
{
if (t.first != r)
{
InstMatch m(q);
- addInstantiations(m, qe, addedLemmas, 0, &(t.second), tparent);
- if (qs.isInConflict())
+ addInstantiations(m, addedLemmas, 0, &(t.second));
+ if (d_qstate.isInConflict())
{
break;
}
Debug("simple-trigger-debug")
<< "Adding instantiations based on " << tat << " from " << d_op << " "
<< d_eqc << std::endl;
- if (tat && !qs.isInConflict())
+ if (tat && !d_qstate.isInConflict())
{
InstMatch m(q);
- addInstantiations(m, qe, addedLemmas, 0, tat, tparent);
+ addInstantiations(m, addedLemmas, 0, tat);
}
return addedLemmas;
}
void InstMatchGeneratorSimple::addInstantiations(InstMatch& m,
- QuantifiersEngine* qe,
uint64_t& addedLemmas,
size_t argIndex,
- TNodeTrie* tat,
- Trigger* tparent)
+ TNodeTrie* tat)
{
Debug("simple-trigger-debug")
<< "Add inst " << argIndex << " " << d_match_pattern << std::endl;
}
// we do not need the trigger parent for simple triggers (no post-processing
// required)
- if (sendInstantiation(
- tparent, m, InferenceId::QUANTIFIERS_INST_E_MATCHING_SIMPLE))
+ if (sendInstantiation(m, InferenceId::QUANTIFIERS_INST_E_MATCHING_SIMPLE))
{
addedLemmas++;
Debug("simple-trigger") << "-> Produced instantiation " << m << std::endl;
}
return;
}
- quantifiers::QuantifiersState& qs = qe->getState();
if (d_match_pattern[argIndex].getKind() == INST_CONSTANT)
{
int v = d_var_num[argIndex];
if (prev.isNull() || prev == t)
{
m.setValue(v, t);
- addInstantiations(
- m, qe, addedLemmas, argIndex + 1, &(tt.second), tparent);
+ addInstantiations(m, addedLemmas, argIndex + 1, &(tt.second));
m.setValue(v, prev);
- if (qs.isInConflict())
+ if (d_qstate.isInConflict())
{
break;
}
}
// inst constant from another quantified formula, treat as ground term?
}
- Node r = qs.getRepresentative(d_match_pattern[argIndex]);
+ Node r = d_qstate.getRepresentative(d_match_pattern[argIndex]);
std::map<TNode, TNodeTrie>::iterator it = tat->d_data.find(r);
if (it != tat->d_data.end())
{
- addInstantiations(m, qe, addedLemmas, argIndex + 1, &(it->second), tparent);
+ addInstantiations(m, addedLemmas, argIndex + 1, &(it->second));
}
}
-int InstMatchGeneratorSimple::getActiveScore(QuantifiersEngine* qe)
+int InstMatchGeneratorSimple::getActiveScore()
{
- Node f = qe->getTermDatabase()->getMatchOperator(d_match_pattern);
- size_t ngt = qe->getTermDatabase()->getNumGroundTerms(f);
+ quantifiers::TermDb* tdb = getQuantifiersEngine()->getTermDatabase();
+ Node f = tdb->getMatchOperator(d_match_pattern);
+ size_t ngt = tdb->getNumGroundTerms(f);
Trace("trigger-active-sel-debug") << "Number of ground terms for (simple) "
<< f << " is " << ngt << std::endl;
return static_cast<int>(ngt);
{
public:
/** constructors */
- InstMatchGeneratorSimple(Node q,
- Node pat,
- quantifiers::QuantifiersState& qs,
- quantifiers::QuantifiersInferenceManager& qim,
- QuantifiersEngine* qe);
+ InstMatchGeneratorSimple(Trigger* tparent, Node q, Node pat);
/** Reset instantiation round. */
- void resetInstantiationRound(QuantifiersEngine* qe) override;
+ void resetInstantiationRound() override;
/** Add instantiations. */
- uint64_t addInstantiations(Node q,
- QuantifiersEngine* qe,
- Trigger* tparent) override;
+ uint64_t addInstantiations(Node q) override;
/** Get active score. */
- int getActiveScore(QuantifiersEngine* qe) override;
+ int getActiveScore() override;
private:
/** quantified formula for the trigger term */
* tat is the term index we are currently traversing.
*/
void addInstantiations(InstMatch& m,
- QuantifiersEngine* qe,
uint64_t& addedLemmas,
size_t argIndex,
- TNodeTrie* tat,
- Trigger* tparent);
+ TNodeTrie* tat);
};
} // namespace inst
if( d_nodes.size()==1 ){
if (TriggerTermInfo::isSimpleTrigger(d_nodes[0]))
{
- d_mg = new InstMatchGeneratorSimple(q, d_nodes[0], qs, qim, qe);
+ d_mg = new InstMatchGeneratorSimple(this, q, d_nodes[0]);
++(qe->d_statistics.d_triggers);
}else{
- d_mg =
- InstMatchGenerator::mkInstMatchGenerator(q, d_nodes[0], qs, qim, qe);
+ d_mg = InstMatchGenerator::mkInstMatchGenerator(this, q, d_nodes[0]);
++(qe->d_statistics.d_simple_triggers);
}
}else{
if( options::multiTriggerCache() ){
- d_mg = new InstMatchGeneratorMulti(q, d_nodes, qs, qim, qe);
+ d_mg = new InstMatchGeneratorMulti(this, q, d_nodes);
}else{
- d_mg = InstMatchGenerator::mkInstMatchGeneratorMulti(
- q, d_nodes, qs, qim, qe);
+ d_mg = InstMatchGenerator::mkInstMatchGeneratorMulti(this, q, d_nodes);
}
if (Trace.isOn("multi-trigger"))
{
delete d_mg;
}
-void Trigger::resetInstantiationRound(){
- d_mg->resetInstantiationRound( d_quantEngine );
-}
+void Trigger::resetInstantiationRound() { d_mg->resetInstantiationRound(); }
-void Trigger::reset( Node eqc ){
- d_mg->reset( eqc, d_quantEngine );
-}
+void Trigger::reset(Node eqc) { d_mg->reset(eqc); }
bool Trigger::isMultiTrigger() const { return d_nodes.size() > 1; }
}
}
}
- uint64_t addedLemmas = d_mg->addInstantiations(d_quant, d_quantEngine, this);
+ uint64_t addedLemmas = d_mg->addInstantiations(d_quant);
if (Debug.isOn("inst-trigger"))
{
if (addedLemmas > 0)
return mkTrigger(qe, qs, qim, qr, f, nodes, keepAll, trOption, useNVars);
}
-int Trigger::getActiveScore() {
- return d_mg->getActiveScore( d_quantEngine );
-}
+int Trigger::getActiveScore() { return d_mg->getActiveScore(); }
Node Trigger::ensureGroundTermPreprocessed(Valuation& val,
Node n,
* This example would fail to match when f(a) is not registered.
*/
std::vector<Node> d_groundTerms;
- /** The quantifiers engine associated with this trigger. */
+ // !!!!!!!!!!!!!!!!!! temporarily available (project #15)
QuantifiersEngine* d_quantEngine;
/** Reference to the quantifiers state */
quantifiers::QuantifiersState& d_qstate;
namespace theory {
namespace inst {
-VarMatchGeneratorTermSubs::VarMatchGeneratorTermSubs(
- Node var,
- Node subs,
- quantifiers::QuantifiersState& qs,
- quantifiers::QuantifiersInferenceManager& qim)
- : InstMatchGenerator(Node::null(), qs, qim),
+VarMatchGeneratorTermSubs::VarMatchGeneratorTermSubs(Trigger* tparent,
+ Node var,
+ Node subs)
+ : InstMatchGenerator(tparent, Node::null()),
d_var(var),
d_subs(subs),
d_rm_prev(false)
d_var_type = d_var.getType();
}
-bool VarMatchGeneratorTermSubs::reset(Node eqc, QuantifiersEngine* qe)
+bool VarMatchGeneratorTermSubs::reset(Node eqc)
{
d_eq_class = eqc;
return true;
}
-int VarMatchGeneratorTermSubs::getNextMatch(Node q,
- InstMatch& m,
- QuantifiersEngine* qe,
- Trigger* tparent)
+int VarMatchGeneratorTermSubs::getNextMatch(Node q, InstMatch& m)
{
int ret_val = -1;
if (!d_eq_class.isNull())
d_eq_class = Node::null();
// if( s.getType().isSubtypeOf( d_var_type ) ){
d_rm_prev = m.get(d_children_types[0]).isNull();
- if (!m.set(qe->getState(), d_children_types[0], s))
+ if (!m.set(d_qstate, d_children_types[0], s))
{
return -1;
}
else
{
ret_val = continueNextMatch(
- q, m, qe, tparent, InferenceId::QUANTIFIERS_INST_E_MATCHING_VAR_GEN);
+ q, m, InferenceId::QUANTIFIERS_INST_E_MATCHING_VAR_GEN);
if (ret_val > 0)
{
return ret_val;
class VarMatchGeneratorTermSubs : public InstMatchGenerator
{
public:
- VarMatchGeneratorTermSubs(Node var,
- Node subs,
- quantifiers::QuantifiersState& qs,
- quantifiers::QuantifiersInferenceManager& qim);
+ VarMatchGeneratorTermSubs(Trigger* tparent, Node var, Node subs);
/** Reset */
- bool reset(Node eqc, QuantifiersEngine* qe) override;
+ bool reset(Node eqc) override;
/** Get the next match. */
- int getNextMatch(Node q,
- InstMatch& m,
- QuantifiersEngine* qe,
- Trigger* tparent) override;
+ int getNextMatch(Node q, InstMatch& m) override;
private:
/** variable we are matching (x in the example x+1). */
projects / cvc5.git / commitdiff