This refactors quantifiers so that it uses the standard interfaces for setting up an equality engine and using it via TheoryState.
This eliminates the need for several special interfaces including getMasterEqualityEngine, CombinationEngine::getCoreEqualityEngine, and most uses of EqualityQuery.
return d_eemanager->getEeTheoryInfo(tid);
}
-eq::EqualityEngine* CombinationEngine::getCoreEqualityEngine()
-{
- return d_eemanager->getCoreEqualityEngine();
-}
-
void CombinationEngine::resetModel() { d_mmanager->resetModel(); }
void CombinationEngine::postProcessModel(bool incomplete)
{
- // should have a consistent core equality engine
- eq::EqualityEngine* mee = d_eemanager->getCoreEqualityEngine();
- if (mee != nullptr)
- {
- AlwaysAssert(mee->consistent());
- }
+ d_eemanager->notifyModel(incomplete);
// postprocess with the model
d_mmanager->postProcessModel(incomplete);
}
/** Finish initialization */
void finishInit();
- //-------------------------- equality engine
/** Get equality engine theory information for theory with identifier tid. */
const EeTheoryInfo* getEeTheoryInfo(TheoryId tid) const;
- /**
- * Get the "core" equality engine. This is the equality engine that
- * quantifiers should use.
- */
- eq::EqualityEngine* getCoreEqualityEngine();
- //-------------------------- end equality engine
//-------------------------- model
/**
* Reset the model maintained by this class. This resets all local information
* Get the equality engine theory information for theory with the given id.
*/
const EeTheoryInfo* getEeTheoryInfo(TheoryId tid) const;
- /**
- * Get the core equality engine, which is the equality engine that the
- * quantifiers engine should use. This corresponds to the master equality
- * engine if eeMode is distributed, or the central equality engine if eeMode
- * is central.
- */
- virtual eq::EqualityEngine* getCoreEqualityEngine() = 0;
/** Allocate equality engine that is context-dependent on c with info esi */
eq::EqualityEngine* allocateEqualityEngine(EeSetupInfo& esi,
context::Context* c);
+ /**
+ * Notify this class that we are about to terminate with a model. This method
+ * is for debugging only.
+ *
+ * @param incomplete Whether we are answering "unknown" instead of "sat".
+ */
+ virtual void notifyModel(bool incomplete) {}
protected:
/** Reference to the theory engine */
Unhandled() << "Expected shared solver to use equality engine";
}
+ const LogicInfo& logicInfo = d_te.getLogicInfo();
+ if (logicInfo.isQuantified())
+ {
+ // construct the master equality engine
+ Assert(d_masterEqualityEngine == nullptr);
+ QuantifiersEngine* qe = d_te.getQuantifiersEngine();
+ Assert(qe != nullptr);
+ d_masterEENotify.reset(new MasterNotifyClass(qe));
+ d_masterEqualityEngine.reset(new eq::EqualityEngine(*d_masterEENotify.get(),
+ d_te.getSatContext(),
+ "theory::master",
+ false));
+ }
// allocate equality engines per theory
for (TheoryId theoryId = theory::THEORY_FIRST;
theoryId != theory::THEORY_LAST;
EeSetupInfo esi;
if (!t->needsEqualityEngine(esi))
{
- // theory said it doesn't need an equality engine, skip
+ // the theory said it doesn't need an equality engine, skip
+ continue;
+ }
+ if (esi.d_useMaster)
+ {
+ // the theory said it wants to use the master equality engine
+ eet.d_usedEe = d_masterEqualityEngine.get();
continue;
}
// allocate the equality engine
eet.d_allocEe.reset(allocateEqualityEngine(esi, c));
// the theory uses the equality engine
eet.d_usedEe = eet.d_allocEe.get();
+ // if there is a master equality engine
+ if (d_masterEqualityEngine != nullptr)
+ {
+ // set the master equality engine of the theory's equality engine
+ eet.d_allocEe->setMasterEqualityEngine(d_masterEqualityEngine.get());
+ }
}
+}
- const LogicInfo& logicInfo = d_te.getLogicInfo();
- if (logicInfo.isQuantified())
+void EqEngineManagerDistributed::notifyModel(bool incomplete)
+{
+ // should have a consistent master equality engine
+ if (d_masterEqualityEngine.get() != nullptr)
{
- // construct the master equality engine
- Assert(d_masterEqualityEngine == nullptr);
- QuantifiersEngine* qe = d_te.getQuantifiersEngine();
- Assert(qe != nullptr);
- d_masterEENotify.reset(new MasterNotifyClass(qe));
- d_masterEqualityEngine.reset(new eq::EqualityEngine(*d_masterEENotify.get(),
- d_te.getSatContext(),
- "theory::master",
- false));
-
- for (TheoryId theoryId = theory::THEORY_FIRST;
- theoryId != theory::THEORY_LAST;
- ++theoryId)
- {
- Theory* t = d_te.theoryOf(theoryId);
- if (t == nullptr)
- {
- // theory not active, skip
- continue;
- }
- EeTheoryInfo& eet = d_einfo[theoryId];
- // Get the allocated equality engine, and connect it to the master
- // equality engine.
- eq::EqualityEngine* eeAlloc = eet.d_allocEe.get();
- if (eeAlloc != nullptr)
- {
- // set the master equality engine of the theory's equality engine
- eeAlloc->setMasterEqualityEngine(d_masterEqualityEngine.get());
- }
- }
+ AlwaysAssert(d_masterEqualityEngine->consistent());
}
}
d_quantEngine->eqNotifyNewClass(t);
}
-eq::EqualityEngine* EqEngineManagerDistributed::getCoreEqualityEngine()
-{
- return d_masterEqualityEngine.get();
-}
-
} // namespace theory
} // namespace CVC4
* per theories and connects them to a master equality engine.
*/
void initializeTheories() override;
- /** get the core equality engine */
- eq::EqualityEngine* getCoreEqualityEngine() override;
+ /** Notify model */
+ void notifyModel(bool incomplete) override;
+
private:
/** notify class for master equality engine */
class MasterNotifyClass : public theory::eq::EqualityEngineNotify
*/
struct EeSetupInfo
{
- EeSetupInfo() : d_notify(nullptr), d_constantsAreTriggers(true) {}
+ EeSetupInfo()
+ : d_notify(nullptr), d_constantsAreTriggers(true), d_useMaster(false)
+ {
+ }
/** The notification class of the theory */
eq::EqualityEngineNotify* d_notify;
/** The name of the equality engine */
std::string d_name;
/** Constants are triggers */
bool d_constantsAreTriggers;
+ /**
+ * Whether we want our state to use the master equality engine. This should
+ * be true exclusively for the theory of quantifiers.
+ */
+ bool d_useMaster;
};
} // namespace theory
TypeNode pvtn = pv.getType();
TypeNode pvtnb = pvtn.getBaseType();
Node pvr = pv;
- if (d_qe->getMasterEqualityEngine()->hasTerm(pv))
+ eq::EqualityEngine* ee = d_qe->getState().getEqualityEngine();
+ if (ee->hasTerm(pv))
{
- pvr = d_qe->getMasterEqualityEngine()->getRepresentative(pv);
+ pvr = ee->getRepresentative(pv);
}
Trace("cegqi-inst-debug") << "[Find instantiation for " << pv
<< "], rep=" << pvr << ", instantiator is "
d_curr_type_eqc.clear();
// must use master equality engine to avoid value instantiations
- eq::EqualityEngine* ee = d_qe->getMasterEqualityEngine();
+ eq::EqualityEngine* ee = d_qe->getState().getEqualityEngine();
//for each variable
for( unsigned i=0; i<d_vars.size(); i++ ){
if( isExcludedEqc( eqc ) ){
d_mode = cand_term_none;
}else{
- eq::EqualityEngine* ee = d_qe->getEqualityQuery()->getEngine();
+ eq::EqualityEngine* ee = d_qe->getState().getEqualityEngine();
if( ee->hasTerm( eqc ) ){
TNodeTrie* tat = d_qe->getTermDatabase()->getTermArgTrie(eqc, op);
if( tat ){
Node CandidateGeneratorQE::getNextCandidateInternal()
{
if( d_mode==cand_term_db ){
+ eq::EqualityEngine* ee = d_qe->getState().getEqualityEngine();
Debug("cand-gen-qe") << "...get next candidate in tbd" << std::endl;
//get next candidate term in the uf term database
while( d_term_iter<d_term_iter_limit ){
if( d_exclude_eqc.empty() ){
return n;
}else{
- Node r = d_qe->getEqualityQuery()->getRepresentative( n );
+ Node r = ee->getRepresentative(n);
if( d_exclude_eqc.find( r )==d_exclude_eqc.end() ){
Debug("cand-gen-qe") << "...returning " << n << std::endl;
return n;
}
void CandidateGeneratorQELitDeq::reset( Node eqc ){
- Node false_term = d_qe->getEqualityQuery()->getEngine()->getRepresentative( NodeManager::currentNM()->mkConst<bool>(false) );
- d_eqc_false = eq::EqClassIterator( false_term, d_qe->getEqualityQuery()->getEngine() );
+ eq::EqualityEngine* ee = d_qe->getState().getEqualityEngine();
+ Node falset = NodeManager::currentNM()->mkConst(false);
+ d_eqc_false = eq::EqClassIterator(falset, ee);
}
Node CandidateGeneratorQELitDeq::getNextCandidate(){
}
void CandidateGeneratorQEAll::reset( Node eqc ) {
- d_eq = eq::EqClassesIterator( d_qe->getEqualityQuery()->getEngine() );
+ d_eq = eq::EqClassesIterator(d_qe->getState().getEqualityEngine());
d_firstTime = true;
}
d_lchildren.clear();
d_arg_to_arg_rep.clear();
d_arg_vector.clear();
- EqualityQuery* eq = d_quantEngine->getEqualityQuery();
+ quantifiers::QuantifiersState& qs = d_quantEngine->getState();
for (std::pair<const TNode, std::vector<Node> >& ha : ho_var_apps_subs)
{
TNode var = ha.first;
}
else if (!itf->second.isNull())
{
- if (!eq->areEqual(itf->second, args[k]))
+ if (!qs.areEqual(itf->second, args[k]))
{
if (!d_quantEngine->getTermDatabase()->isEntailed(
- itf->second.eqNode(args[k]), true, eq))
+ itf->second.eqNode(args[k]), true))
{
fixed_vals[k] = Node::null();
}
{
if (!itf->second.isNull())
{
- Node r = eq->getRepresentative(itf->second);
+ Node r = qs.getRepresentative(itf->second);
std::map<Node, unsigned>::iterator itfr = arg_to_rep.find(r);
if (itfr != arg_to_rep.end())
{
#include "theory/quantifiers/ematching/trigger.h"
#include "theory/quantifiers/ematching/var_match_generator.h"
#include "theory/quantifiers/instantiate.h"
+#include "theory/quantifiers/quantifiers_state.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers_engine.h"
Trace("matching-fail") << "Internal error for match generator." << std::endl;
return -2;
}
- EqualityQuery* q = qe->getEqualityQuery();
+ quantifiers::QuantifiersState& qs = qe->getState();
bool success = true;
std::vector<int> prev;
// if t is null
Trace("matching-debug2")
<< "Setting " << ct << " to " << t[i] << "..." << std::endl;
bool addToPrev = m.get(ct).isNull();
- if (!m.set(q, ct, t[i]))
+ if (!m.set(qs, ct, t[i]))
{
// match is in conflict
Trace("matching-fail")
}
else if (ct == -1)
{
- if (!q->areEqual(d_match_pattern[i], t[i]))
+ if (!qs.areEqual(d_match_pattern[i], t[i]))
{
Trace("matching-fail") << "Match fail arg: " << d_match_pattern[i]
<< " and " << t[i] << std::endl;
if (d_match_pattern.getKind() == INST_CONSTANT)
{
bool addToPrev = m.get(d_children_types[0]).isNull();
- if (!m.set(q, d_children_types[0], t))
+ if (!m.set(qs, d_children_types[0], t))
{
success = false;
}
{
if (t.getType().isBoolean())
{
- t_match = nm->mkConst(!q->areEqual(nm->mkConst(true), t));
+ t_match = nm->mkConst(!qs.areEqual(nm->mkConst(true), t));
}
else
{
if (!t_match.isNull())
{
bool addToPrev = m.get(v).isNull();
- if (!m.set(q, v, t_match))
+ if (!m.set(qs, v, t_match))
{
success = false;
}
// we did not properly initialize the candidate generator, thus we fail
return false;
}
- eqc = qe->getEqualityQuery()->getRepresentative( eqc );
+ eqc = qe->getState().getRepresentative(eqc);
Trace("matching-debug2") << this << " reset " << eqc << "." << std::endl;
if( !d_eq_class_rel.isNull() && d_eq_class_rel.getKind()!=INST_CONSTANT ){
d_eq_class = d_eq_class_rel;
Node t = d_curr_first_candidate;
do{
Trace("matching-debug2") << "Matching candidate : " << t << std::endl;
- Assert(!qe->inConflict());
+ Assert(!qe->getState().isInConflict());
//if t not null, try to fit it into match m
if( !t.isNull() ){
if( d_curr_exclude_match.find( t )==d_curr_exclude_match.end() ){
}
//get the next candidate term t
if( success<0 ){
- t = qe->inConflict() ? Node::null() : d_cg->getNextCandidate();
+ t = qe->getState().isInConflict() ? Node::null()
+ : d_cg->getNextCandidate();
}else{
d_curr_first_candidate = d_cg->getNextCandidate();
}
if (sendInstantiation(tparent, m))
{
addedLemmas++;
- if( qe->inConflict() ){
+ if (qe->getState().isInConflict())
+ {
break;
}
}
}else{
addedLemmas++;
- if( qe->inConflict() ){
+ if (qe->getState().isInConflict())
+ {
break;
}
}
#include "theory/quantifiers/ematching/inst_match_generator_multi.h"
+#include "theory/quantifiers/quantifiers_state.h"
#include "theory/quantifiers_engine.h"
using namespace CVC4::kind;
<< "...processing " << j << " / " << newMatches.size()
<< ", #lemmas = " << addedLemmas << std::endl;
processNewMatch(qe, tparent, newMatches[j], i, addedLemmas);
- if (qe->inConflict())
+ if (qe->getState().isInConflict())
{
return addedLemmas;
}
size_t endChildIndex,
bool modEq)
{
- Assert(!qe->inConflict());
+ Assert(!qe->getState().isInConflict());
if (childIndex == endChildIndex)
{
// m is an instantiation
childIndex,
endChildIndex,
modEq);
- if (qe->inConflict())
+ if (qe->getState().isInConflict())
{
break;
}
{
return;
}
- eq::EqualityEngine* ee = qe->getEqualityQuery()->getEngine();
+ quantifiers::QuantifiersState& qs = qe->getState();
// check modulo equality for other possible instantiations
- if (!ee->hasTerm(n))
+ if (!qs.hasTerm(n))
{
return;
}
- eq::EqClassIterator eqc(ee->getRepresentative(n), ee);
+ eq::EqClassIterator eqc(qs.getRepresentative(n), qs.getEqualityEngine());
while (!eqc.isFinished())
{
Node en = (*eqc);
childIndex,
endChildIndex,
modEq);
- if (qe->inConflict())
+ if (qe->getState().isInConflict())
{
break;
}
QuantifiersEngine* qe,
Trigger* tparent)
{
+ quantifiers::QuantifiersState& qs = qe->getState();
uint64_t addedLemmas = 0;
TNodeTrie* tat;
if (d_eqc.isNull())
{
// iterate over all classes except r
tat = qe->getTermDatabase()->getTermArgTrie(Node::null(), d_op);
- if (tat && !qe->inConflict())
+ if (tat && !qs.isInConflict())
{
- Node r = qe->getEqualityQuery()->getRepresentative(d_eqc);
+ Node r = qs.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));
- if (qe->inConflict())
+ if (qs.isInConflict())
{
break;
}
Debug("simple-trigger-debug")
<< "Adding instantiations based on " << tat << " from " << d_op << " "
<< d_eqc << std::endl;
- if (tat && !qe->inConflict())
+ if (tat && !qs.isInConflict())
{
InstMatch m(q);
addInstantiations(m, qe, addedLemmas, 0, tat);
}
return;
}
+ quantifiers::QuantifiersState& qs = qe->getState();
if (d_match_pattern[argIndex].getKind() == INST_CONSTANT)
{
int v = d_var_num[argIndex];
m.setValue(v, t);
addInstantiations(m, qe, addedLemmas, argIndex + 1, &(tt.second));
m.setValue(v, prev);
- if (qe->inConflict())
+ if (qs.isInConflict())
{
break;
}
}
// inst constant from another quantified formula, treat as ground term?
}
- Node r = qe->getEqualityQuery()->getRepresentative(d_match_pattern[argIndex]);
+ Node r = qs.getRepresentative(d_match_pattern[argIndex]);
std::map<TNode, TNodeTrie>::iterator it = tat->d_data.find(r);
if (it != tat->d_data.end())
{
Trace("inst-engine-debug")
<< " -> unfinished= "
<< (quantStatus == InstStrategyStatus::STATUS_UNFINISHED)
- << ", conflict=" << d_quantEngine->inConflict() << std::endl;
- if( d_quantEngine->inConflict() ){
+ << ", conflict=" << d_qstate.isInConflict() << std::endl;
+ if (d_qstate.isInConflict())
+ {
return;
}
else if (quantStatus == InstStrategyStatus::STATUS_UNFINISHED)
{
unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting();
doInstantiationRound(e);
- if (d_quantEngine->inConflict())
+ if (d_qstate.isInConflict())
{
Assert(d_quantEngine->getNumLemmasWaiting() > lastWaiting);
Trace("inst-engine") << "Conflict, added lemmas = "
{
// for each ground term t that does not exist in the equality engine, we
// add a purification lemma of the form (k = t).
- eq::EqualityEngine* ee = d_quantEngine->getEqualityQuery()->getEngine();
+ eq::EqualityEngine* ee = d_quantEngine->getState().getEqualityEngine();
for (const Node& gt : d_groundTerms)
{
if (!ee->hasTerm(gt))
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->getEqualityQuery(), d_children_types[0], s))
+ if (!m.set(qe->getState(), d_children_types[0], s))
{
return -1;
}
EqualityQueryQuantifiersEngine::EqualityQueryQuantifiersEngine(
QuantifiersState& qs, QuantifiersEngine* qe)
- : d_qe(qe), d_eqi_counter(qs.getSatContext()), d_reset_count(0)
+ : d_qe(qe),
+ d_qstate(qs),
+ d_eqi_counter(qs.getSatContext()),
+ d_reset_count(0)
{
}
return true;
}
-bool EqualityQueryQuantifiersEngine::hasTerm( Node a ){
- return getEngine()->hasTerm( a );
-}
-
-Node EqualityQueryQuantifiersEngine::getRepresentative( Node a ){
- eq::EqualityEngine* ee = getEngine();
- if( ee->hasTerm( a ) ){
- return ee->getRepresentative( a );
- }else{
- return a;
- }
-}
-
-bool EqualityQueryQuantifiersEngine::areEqual( Node a, Node b ){
- if( a==b ){
- return true;
- }else{
- eq::EqualityEngine* ee = getEngine();
- if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
- return ee->areEqual( a, b );
- }else{
- return false;
- }
- }
-}
-
-bool EqualityQueryQuantifiersEngine::areDisequal( Node a, Node b ){
- if( a==b ){
- return false;
- }else{
- eq::EqualityEngine* ee = getEngine();
- if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
- return ee->areDisequal( a, b, false );
- }else{
- return a.isConst() && b.isConst();
- }
- }
-}
-
Node EqualityQueryQuantifiersEngine::getInternalRepresentative(Node a,
Node q,
int index)
{
Assert(q.isNull() || q.getKind() == FORALL);
- Node r = getRepresentative( a );
+ Node r = d_qstate.getRepresentative(a);
if( options::finiteModelFind() ){
if( r.isConst() && quantifiers::TermUtil::containsUninterpretedConstant( r ) ){
//map back from values assigned by model, if any
if (!tr.isNull())
{
r = tr;
- r = getRepresentative( r );
+ r = d_qstate.getRepresentative(r);
}else{
if( r.getType().isSort() ){
Trace("internal-rep-warn") << "No representative for UF constant." << std::endl;
// find best selection for representative
Node r_best;
std::vector<Node> eqc;
- getEquivalenceClass(r, eqc);
+ d_qstate.getEquivalenceClass(r, eqc);
Trace("internal-rep-select")
<< "Choose representative for equivalence class : " << eqc
<< ", type = " << v_tn << std::endl;
return r_best;
}
-eq::EqualityEngine* EqualityQueryQuantifiersEngine::getEngine(){
- return d_qe->getMasterEqualityEngine();
-}
-
-void EqualityQueryQuantifiersEngine::getEquivalenceClass( Node a, std::vector< Node >& eqc ){
- eq::EqualityEngine* ee = getEngine();
- if( ee->hasTerm( a ) ){
- Node rep = ee->getRepresentative( a );
- eq::EqClassIterator eqc_iter( rep, ee );
- while( !eqc_iter.isFinished() ){
- eqc.push_back( *eqc_iter );
- eqc_iter++;
- }
- }else{
- eqc.push_back( a );
- }
- //a should be in its equivalence class
- Assert(std::find(eqc.begin(), eqc.end(), a) != eqc.end());
-}
-
-TNode EqualityQueryQuantifiersEngine::getCongruentTerm( Node f, std::vector< TNode >& args ) {
- return d_qe->getTermDatabase()->getCongruentTerm( f, args );
-}
-
//helper functions
Node EqualityQueryQuantifiersEngine::getInstance( Node n, const std::vector< Node >& eqc, std::unordered_map<TNode, Node, TNodeHashFunction>& cache ){
/** EqualityQueryQuantifiersEngine class
*
- * This is a wrapper class around an equality engine that is used for
- * queries required by algorithms in the quantifiers theory. It uses an equality
- * engine, as determined by the quantifiers engine it points to.
- *
- * The main extension of this class wrt EqualityQuery is the function
+ * The main method of this class is the function
* getInternalRepresentative, which is used by instantiation-based methods
* that are agnostic with respect to choosing terms within an equivalence class.
* Examples of such methods are finite model finding and enumerative
* representative based on the internal heuristic, which is currently based on
* choosing the term that was previously chosen as a representative earliest.
*/
-class EqualityQueryQuantifiersEngine : public EqualityQuery
+class EqualityQueryQuantifiersEngine : public QuantifiersUtil
{
public:
EqualityQueryQuantifiersEngine(QuantifiersState& qs, QuantifiersEngine* qe);
void registerQuantifier(Node q) override {}
/** identify */
std::string identify() const override { return "EqualityQueryQE"; }
- /** does the equality engine have term a */
- bool hasTerm(Node a) override;
- /** get the representative of a */
- Node getRepresentative(Node a) override;
- /** are a and b equal? */
- bool areEqual(Node a, Node b) override;
- /** are a and b disequal? */
- bool areDisequal(Node a, Node b) override;
- /** get equality engine
- * This may either be the master equality engine or the model's equality
- * engine.
- */
- eq::EqualityEngine* getEngine() override;
- /** get list of members in the equivalence class of a */
- void getEquivalenceClass(Node a, std::vector<Node>& eqc) override;
- /** get congruent term
- * If possible, returns a term n such that:
- * (1) n is a term in the equality engine from getEngine().
- * (2) n is of the form f( t1, ..., tk ) where ti is in the equivalence class
- * of args[i] for i=1...k
- * Otherwise, returns the null node.
- *
- * Notice that f should be a "match operator", returned by
- * TermDb::getMatchOperator.
- */
- TNode getCongruentTerm(Node f, std::vector<TNode>& args) override;
/** gets the current best representative in the equivalence
* class of a, based on some heuristic. Currently, the default heuristic
* chooses terms that were previously chosen as representatives
private:
/** pointer to theory engine */
QuantifiersEngine* d_qe;
+ /** the quantifiers state */
+ QuantifiersState& d_qstate;
/** quantifiers equality inference */
context::CDO< unsigned > d_eqi_counter;
/** internal representatives */
Node r = fm->getRepresentative( it->second[a] );
if( Trace.isOn("fmc-model-debug") ){
std::vector< Node > eqc;
- d_qe->getEqualityQuery()->getEquivalenceClass( r, eqc );
+ d_qstate.getEquivalenceClass(r, eqc);
Trace("fmc-model-debug") << " " << (it->second[a]==r);
Trace("fmc-model-debug") << " : " << it->second[a] << " : " << r << " : ";
//Trace("fmc-model-debug") << r2 << " : " << ir << " : ";
if( !riter.isIncomplete() ){
int triedLemmas = 0;
int addedLemmas = 0;
- EqualityQuery* qy = d_quantEngine->getEqualityQuery();
Instantiate* inst = d_quantEngine->getInstantiate();
while( !riter.isFinished() && ( addedLemmas==0 || !options::fmfOneInstPerRound() ) ){
//instantiation was not shown to be true, construct the match
InstMatch m( f );
for (unsigned i = 0; i < riter.getNumTerms(); i++)
{
- m.set(qy, i, riter.getCurrentTerm(i));
+ m.set(d_qstate, i, riter.getCurrentTerm(i));
}
Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
triedLemmas++;
}
}
-bool InstMatch::merge( EqualityQuery* q, InstMatch& m ){
- Assert(d_vals.size() == m.d_vals.size());
- for (unsigned i = 0, size = d_vals.size(); i < size; i++)
- {
- if( !m.d_vals[i].isNull() ){
- if( d_vals[i].isNull() ){
- d_vals[i] = m.d_vals[i];
- }else{
- if( !q->areEqual( d_vals[i], m.d_vals[i]) ){
- clear();
- return false;
- }
- }
- }
- }
- return true;
-}
-
void InstMatch::debugPrint( const char* c ){
for (unsigned i = 0, size = d_vals.size(); i < size; i++)
{
Assert(i < d_vals.size());
d_vals[i] = n;
}
-bool InstMatch::set(EqualityQuery* q, size_t i, TNode n)
+bool InstMatch::set(quantifiers::QuantifiersState& qs, size_t i, TNode n)
{
Assert(i < d_vals.size());
if( !d_vals[i].isNull() ){
- if (q->areEqual(d_vals[i], n))
- {
- return true;
- }else{
- return false;
- }
- }else{
- d_vals[i] = n;
- return true;
+ return qs.areEqual(d_vals[i], n);
}
+ d_vals[i] = n;
+ return true;
}
}/* CVC4::theory::inst namespace */
namespace CVC4 {
namespace theory {
-class EqualityQuery;
+namespace quantifiers {
+class QuantifiersState;
+}
namespace inst {
* not already initialized in this match.
*/
void add(InstMatch& m);
- /** merge with match m
- *
- * This method returns true if the merge was successful, that is, all jointly
- * initialized fields of this class and m are equivalent modulo the equalities
- * given by q.
- */
- bool merge( EqualityQuery* q, InstMatch& m );
/** is this complete, i.e. are all fields non-null? */
bool isComplete();
/** is this empty, i.e. are all fields the null node? */
* This method returns true if the i^th field was previously uninitialized,
* or is equivalent to n modulo the equalities given by q.
*/
- bool set(EqualityQuery* q, size_t i, TNode n);
+ bool set(quantifiers::QuantifiersState& qs, size_t i, TNode n);
};
inline std::ostream& operator<<(std::ostream& out, const InstMatch& m) {
}
if (modEq)
{
+ quantifiers::QuantifiersState& qs = qe->getState();
// check modulo equality if any other instantiation match exists
- if (!n.isNull() && qe->getEqualityQuery()->getEngine()->hasTerm(n))
+ if (!n.isNull() && qs.hasTerm(n))
{
- eq::EqClassIterator eqc(
- qe->getEqualityQuery()->getEngine()->getRepresentative(n),
- qe->getEqualityQuery()->getEngine());
+ eq::EqClassIterator eqc(qs.getRepresentative(n), qs.getEqualityEngine());
while (!eqc.isFinished())
{
Node en = (*eqc);
if (modEq)
{
// check modulo equality if any other instantiation match exists
- if (!n.isNull() && qe->getEqualityQuery()->getEngine()->hasTerm(n))
+ quantifiers::QuantifiersState& qs = qe->getState();
+ if (!n.isNull() && qs.hasTerm(n))
{
- eq::EqClassIterator eqc(
- qe->getEqualityQuery()->getEngine()->getRepresentative(n),
- qe->getEqualityQuery()->getEngine());
+ eq::EqClassIterator eqc(qs.getRepresentative(n), qs.getEqualityEngine());
while (!eqc.isFinished())
{
Node en = (*eqc);
namespace theory {
class QuantifiersEngine;
-class EqualityQuery;
namespace inst {
std::map<TypeNode, std::vector<Node> > term_db_list;
std::vector<TypeNode> ftypes;
TermDb* tdb = d_quantEngine->getTermDatabase();
- EqualityQuery* qy = d_quantEngine->getEqualityQuery();
+ QuantifiersState& qs = d_quantEngine->getState();
// iterate over substitutions for variables
for (unsigned i = 0; i < f[0].getNumChildren(); i++)
{
Node gt = tdb->getTypeGroundTerm(ftypes[i], j);
if (!options::cegqi() || !quantifiers::TermUtil::hasInstConstAttr(gt))
{
- Node rep = qy->getRepresentative(gt);
+ Node rep = qs.getRepresentative(gt);
if (reps_found.find(rep) == reps_found.end())
{
reps_found[rep] = gt;
p->d_quantEngine->getInstantiate()->getInstantiation(d_q, terms);
inst = Rewriter::rewrite(inst);
Node inst_eval = p->getTermDatabase()->evaluateTerm(
- inst, nullptr, options::qcfTConstraint(), true);
+ inst, options::qcfTConstraint(), true);
if( Trace.isOn("qcf-instance-check") ){
Trace("qcf-instance-check") << "Possible propagating instance for " << d_q << " : " << std::endl;
for( unsigned i=0; i<terms.size(); i++ ){
eq::EqualityEngine* QuantifiersModule::getEqualityEngine() const
{
- return d_quantEngine->getMasterEqualityEngine();
+ return d_qstate.getEqualityEngine();
}
bool QuantifiersModule::areEqual(TNode n1, TNode n2) const
{
- return d_quantEngine->getEqualityQuery()->areEqual( n1, n2 );
+ return d_qstate.areEqual(n1, n2);
}
bool QuantifiersModule::areDisequal(TNode n1, TNode n2) const
{
- return d_quantEngine->getEqualityQuery()->areDisequal( n1, n2 );
+ return d_qstate.areDisequal(n1, n2);
}
TNode QuantifiersModule::getRepresentative(TNode n) const
{
- return d_quantEngine->getEqualityQuery()->getRepresentative( n );
+ return d_qstate.getRepresentative(n);
}
QuantifiersEngine* QuantifiersModule::getQuantifiersEngine() const
static void getEntailPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol );
};
-/** EqualityQuery
-* This is a wrapper class around equality engine.
-*/
-class EqualityQuery : public QuantifiersUtil {
-public:
- EqualityQuery(){}
- virtual ~EqualityQuery(){};
- /** extends engine */
- virtual bool extendsEngine() { return false; }
- /** contains term */
- virtual bool hasTerm( Node a ) = 0;
- /** get the representative of the equivalence class of a */
- virtual Node getRepresentative( Node a ) = 0;
- /** returns true if a and b are equal in the current context */
- virtual bool areEqual( Node a, Node b ) = 0;
- /** returns true is a and b are disequal in the current context */
- virtual bool areDisequal( Node a, Node b ) = 0;
- /** get the equality engine associated with this query */
- virtual eq::EqualityEngine* getEngine() = 0;
- /** get the equivalence class of a */
- virtual void getEquivalenceClass( Node a, std::vector< Node >& eqc ) = 0;
- /** get the term that exists in EE that is congruent to f with args (f is
- * returned by TermDb::getMatchOperator(...)) */
- virtual TNode getCongruentTerm( Node f, std::vector< TNode >& args ) = 0;
-};/* class EqualityQuery */
-
/** Types of bounds that can be inferred for quantified formulas */
enum BoundVarType
{
}
}
-void RelevantDomain::RDomain::removeRedundantTerms( QuantifiersEngine * qe ) {
+void RelevantDomain::RDomain::removeRedundantTerms(QuantifiersState& qs)
+{
std::map< Node, Node > rterms;
for( unsigned i=0; i<d_terms.size(); i++ ){
Node r = d_terms[i];
if( !TermUtil::hasInstConstAttr( d_terms[i] ) ){
- r = qe->getEqualityQuery()->getRepresentative( d_terms[i] );
+ r = qs.getRepresentative(d_terms[i]);
}
if( rterms.find( r )==rterms.end() ){
rterms[r] = d_terms[i];
RDomain * r = it2->second;
RDomain * rp = r->getParent();
if( r==rp ){
- r->removeRedundantTerms( d_qe );
+ r->removeRedundantTerms(d_qe->getState());
for( unsigned i=0; i<r->d_terms.size(); i++ ){
Trace("rel-dom") << r->d_terms[i] << " ";
}
/** remove redundant terms for d_terms, removes
* duplicates modulo equality.
*/
- void removeRedundantTerms( QuantifiersEngine * qe );
+ void removeRedundantTerms(QuantifiersState& qs);
/** is n in this relevant domain? */
bool hasTerm( Node n ) { return std::find( d_terms.begin(), d_terms.end(), n )!=d_terms.end(); }
void TermDb::computeArgReps( TNode n ) {
if (d_arg_reps.find(n) == d_arg_reps.end())
{
- eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
+ eq::EqualityEngine* ee = d_qstate.getEqualityEngine();
for (const TNode& nc : n)
{
TNode r = ee->hasTerm(nc) ? ee->getRepresentative(nc) : nc;
{
ops.insert(ops.end(), d_ho_op_slaves[f].begin(), d_ho_op_slaves[f].end());
}
- eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
+ eq::EqualityEngine* ee = d_qstate.getEqualityEngine();
for (TNode ff : ops)
{
for (const Node& n : d_op_map[ff])
unsigned nonCongruentCount = 0;
unsigned alreadyCongruentCount = 0;
unsigned relevantCount = 0;
- eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
NodeManager* nm = NodeManager::currentNM();
for (TNode ff : ops)
{
for (const Node& n : it->second)
{
// to be added to term index, term must be relevant, and exist in EE
- if (!hasTermCurrent(n) || !ee->hasTerm(n))
+ if (!hasTermCurrent(n) || !d_qstate.hasTerm(n))
{
Trace("term-db-debug") << n << " is not relevant." << std::endl;
continue;
}
}
Trace("term-db-debug") << std::endl;
- Assert(ee->hasTerm(n));
- Trace("term-db-debug") << " and value : " << ee->getRepresentative(n)
- << std::endl;
+ Assert(d_qstate.hasTerm(n));
+ Trace("term-db-debug")
+ << " and value : " << d_qstate.getRepresentative(n) << std::endl;
Node at = d_func_map_trie[f].addOrGetTerm(n, d_arg_reps[n]);
- Assert(ee->hasTerm(at));
+ Assert(d_qstate.hasTerm(at));
Trace("term-db-debug2") << "...add term returned " << at << std::endl;
- if (at != n && ee->areEqual(at, n))
+ if (at != n && d_qstate.areEqual(at, n))
{
setTermInactive(n);
Trace("term-db-debug") << n << " is redundant." << std::endl;
congruentCount++;
continue;
}
- if (ee->areDisequal(at, n, false))
+ if (d_qstate.areDisequal(at, n))
{
std::vector<Node> lits;
lits.push_back(nm->mkNode(EQUAL, at, n));
f = getOperatorRepresentative( f );
}
computeUfTerms( f );
- Assert(!d_quantEngine->getMasterEqualityEngine()->hasTerm(r)
- || d_quantEngine->getMasterEqualityEngine()->getRepresentative(r)
- == r);
+ Assert(!d_qstate.getEqualityEngine()->hasTerm(r)
+ || d_qstate.getEqualityEngine()->getRepresentative(r) == r);
std::map< Node, std::map< unsigned, std::vector< Node > > >::iterator it = d_func_map_rel_dom.find( f );
if( it != d_func_map_rel_dom.end() ){
std::map< unsigned, std::vector< Node > >::iterator it2 = it->second.find( i );
Node TermDb::evaluateTerm2(TNode n,
std::map<TNode, Node>& visited,
std::vector<Node>& exp,
- EqualityQuery* qy,
bool useEntailmentTests,
bool computeExp,
bool reqHasTerm)
if( n.getKind()==FORALL || n.getKind()==BOUND_VARIABLE ){
//do nothing
}
- else if (qy->hasTerm(n))
+ else if (d_qstate.hasTerm(n))
{
Trace("term-db-eval") << "...exists in ee, return rep" << std::endl;
- ret = qy->getRepresentative(n);
+ ret = d_qstate.getRepresentative(n);
if (computeExp)
{
if (n != ret)
TNode c = evaluateTerm2(n[i],
visited,
tempExp,
- qy,
useEntailmentTests,
computeExp,
reqHasTerm);
ret = evaluateTerm2(n[c == d_true ? 1 : 2],
visited,
tempExp,
- qy,
useEntailmentTests,
computeExp,
reqHasTerm);
if (!f.isNull())
{
// if f is congruent to a term indexed by this class
- TNode nn = qy->getCongruentTerm(f, args);
+ TNode nn = getCongruentTerm(f, args);
Trace("term-db-eval") << " got congruent term " << nn
<< " from DB for " << n << std::endl;
if (!nn.isNull())
}
}
}
- ret = qy->getRepresentative(nn);
+ ret = d_qstate.getRepresentative(nn);
Trace("term-db-eval") << "return rep" << std::endl;
ret_set = true;
reqHasTerm = false;
ret = Rewriter::rewrite(ret);
if (ret.getKind() == EQUAL)
{
- if (qy->areDisequal(ret[0], ret[1]))
+ if (d_qstate.areDisequal(ret[0], ret[1]))
{
ret = d_false;
}
if (k != OR && k != AND && k != EQUAL && k != ITE && k != NOT
&& k != FORALL)
{
- if (!qy->hasTerm(ret))
+ if (!d_qstate.hasTerm(ret))
{
ret = Node::null();
}
return ret;
}
-
-TNode TermDb::getEntailedTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, EqualityQuery * qy ) {
- Assert(!qy->extendsEngine());
+TNode TermDb::getEntailedTerm2(TNode n,
+ std::map<TNode, TNode>& subs,
+ bool subsRep,
+ bool hasSubs)
+{
Trace("term-db-entail") << "get entailed term : " << n << std::endl;
- if( qy->getEngine()->hasTerm( n ) ){
+ if (d_qstate.hasTerm(n))
+ {
Trace("term-db-entail") << "...exists in ee, return rep " << std::endl;
return n;
}else if( n.getKind()==BOUND_VARIABLE ){
if( it!=subs.end() ){
Trace("term-db-entail") << "...substitution is : " << it->second << std::endl;
if( subsRep ){
- Assert(qy->getEngine()->hasTerm(it->second));
- Assert(qy->getEngine()->getRepresentative(it->second) == it->second);
+ Assert(d_qstate.hasTerm(it->second));
+ Assert(d_qstate.getRepresentative(it->second) == it->second);
return it->second;
- }else{
- return getEntailedTerm2( it->second, subs, subsRep, hasSubs, qy );
}
+ return getEntailedTerm2(it->second, subs, subsRep, hasSubs);
}
}
}else if( n.getKind()==ITE ){
for( unsigned i=0; i<2; i++ ){
- if( isEntailed2( n[0], subs, subsRep, hasSubs, i==0, qy ) ){
- return getEntailedTerm2( n[ i==0 ? 1 : 2 ], subs, subsRep, hasSubs, qy );
+ if (isEntailed2(n[0], subs, subsRep, hasSubs, i == 0))
+ {
+ return getEntailedTerm2(n[i == 0 ? 1 : 2], subs, subsRep, hasSubs);
}
}
}else{
if( !f.isNull() ){
std::vector< TNode > args;
for( unsigned i=0; i<n.getNumChildren(); i++ ){
- TNode c = getEntailedTerm2( n[i], subs, subsRep, hasSubs, qy );
+ TNode c = getEntailedTerm2(n[i], subs, subsRep, hasSubs);
if( c.isNull() ){
return TNode::null();
}
- c = qy->getEngine()->getRepresentative( c );
+ c = d_qstate.getRepresentative(c);
Trace("term-db-entail") << " child " << i << " : " << c << std::endl;
args.push_back( c );
}
- TNode nn = qy->getCongruentTerm( f, args );
+ TNode nn = getCongruentTerm(f, args);
Trace("term-db-entail") << " got congruent term " << nn << " for " << n << std::endl;
return nn;
}
}
Node TermDb::evaluateTerm(TNode n,
- EqualityQuery* qy,
bool useEntailmentTests,
bool reqHasTerm)
{
- if( qy==NULL ){
- qy = d_quantEngine->getEqualityQuery();
- }
std::map< TNode, Node > visited;
std::vector<Node> exp;
- return evaluateTerm2(
- n, visited, exp, qy, useEntailmentTests, false, reqHasTerm);
+ return evaluateTerm2(n, visited, exp, useEntailmentTests, false, reqHasTerm);
}
Node TermDb::evaluateTerm(TNode n,
std::vector<Node>& exp,
- EqualityQuery* qy,
bool useEntailmentTests,
bool reqHasTerm)
{
- if (qy == NULL)
- {
- qy = d_quantEngine->getEqualityQuery();
- }
std::map<TNode, Node> visited;
- return evaluateTerm2(
- n, visited, exp, qy, useEntailmentTests, true, reqHasTerm);
+ return evaluateTerm2(n, visited, exp, useEntailmentTests, true, reqHasTerm);
}
-TNode TermDb::getEntailedTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep, EqualityQuery * qy ) {
- if( qy==NULL ){
- qy = d_quantEngine->getEqualityQuery();
- }
- return getEntailedTerm2( n, subs, subsRep, true, qy );
+TNode TermDb::getEntailedTerm(TNode n,
+ std::map<TNode, TNode>& subs,
+ bool subsRep)
+{
+ return getEntailedTerm2(n, subs, subsRep, true);
}
-TNode TermDb::getEntailedTerm( TNode n, EqualityQuery * qy ) {
- if( qy==NULL ){
- qy = d_quantEngine->getEqualityQuery();
- }
+TNode TermDb::getEntailedTerm(TNode n)
+{
std::map< TNode, TNode > subs;
- return getEntailedTerm2( n, subs, false, false, qy );
+ return getEntailedTerm2(n, subs, false, false);
}
-bool TermDb::isEntailed2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol, EqualityQuery * qy ) {
- Assert(!qy->extendsEngine());
+bool TermDb::isEntailed2(
+ TNode n, std::map<TNode, TNode>& subs, bool subsRep, bool hasSubs, bool pol)
+{
Trace("term-db-entail") << "Check entailed : " << n << ", pol = " << pol << std::endl;
Assert(n.getType().isBoolean());
if( n.getKind()==EQUAL && !n[0].getType().isBoolean() ){
- TNode n1 = getEntailedTerm2( n[0], subs, subsRep, hasSubs, qy );
+ TNode n1 = getEntailedTerm2(n[0], subs, subsRep, hasSubs);
if( !n1.isNull() ){
- TNode n2 = getEntailedTerm2( n[1], subs, subsRep, hasSubs, qy );
+ TNode n2 = getEntailedTerm2(n[1], subs, subsRep, hasSubs);
if( !n2.isNull() ){
if( n1==n2 ){
return pol;
}else{
- Assert(qy->getEngine()->hasTerm(n1));
- Assert(qy->getEngine()->hasTerm(n2));
+ Assert(d_qstate.hasTerm(n1));
+ Assert(d_qstate.hasTerm(n2));
if( pol ){
- return qy->getEngine()->areEqual( n1, n2 );
+ return d_qstate.areEqual(n1, n2);
}else{
- return qy->getEngine()->areDisequal( n1, n2, false );
+ return d_qstate.areDisequal(n1, n2);
}
}
}
}
}else if( n.getKind()==NOT ){
- return isEntailed2( n[0], subs, subsRep, hasSubs, !pol, qy );
+ return isEntailed2(n[0], subs, subsRep, hasSubs, !pol);
}else if( n.getKind()==OR || n.getKind()==AND ){
bool simPol = ( pol && n.getKind()==OR ) || ( !pol && n.getKind()==AND );
for( unsigned i=0; i<n.getNumChildren(); i++ ){
- if( isEntailed2( n[i], subs, subsRep, hasSubs, pol, qy ) ){
+ if (isEntailed2(n[i], subs, subsRep, hasSubs, pol))
+ {
if( simPol ){
return true;
}
//Boolean equality here
}else if( n.getKind()==EQUAL || n.getKind()==ITE ){
for( unsigned i=0; i<2; i++ ){
- if( isEntailed2( n[0], subs, subsRep, hasSubs, i==0, qy ) ){
+ if (isEntailed2(n[0], subs, subsRep, hasSubs, i == 0))
+ {
unsigned ch = ( n.getKind()==EQUAL || i==0 ) ? 1 : 2;
bool reqPol = ( n.getKind()==ITE || i==0 ) ? pol : !pol;
- return isEntailed2( n[ch], subs, subsRep, hasSubs, reqPol, qy );
+ return isEntailed2(n[ch], subs, subsRep, hasSubs, reqPol);
}
}
}else if( n.getKind()==APPLY_UF ){
- TNode n1 = getEntailedTerm2( n, subs, subsRep, hasSubs, qy );
+ TNode n1 = getEntailedTerm2(n, subs, subsRep, hasSubs);
if( !n1.isNull() ){
- Assert(qy->hasTerm(n1));
+ Assert(d_qstate.hasTerm(n1));
if( n1==d_true ){
return pol;
}else if( n1==d_false ){
return !pol;
}else{
- return qy->getEngine()->getRepresentative( n1 ) == ( pol ? d_true : d_false );
+ return d_qstate.getRepresentative(n1) == (pol ? d_true : d_false);
}
}
}else if( n.getKind()==FORALL && !pol ){
- return isEntailed2( n[1], subs, subsRep, hasSubs, pol, qy );
+ return isEntailed2(n[1], subs, subsRep, hasSubs, pol);
}
return false;
}
-bool TermDb::isEntailed( TNode n, bool pol, EqualityQuery * qy ) {
- if( qy==NULL ){
- Assert(d_consistent_ee);
- qy = d_quantEngine->getEqualityQuery();
- }
+bool TermDb::isEntailed(TNode n, bool pol)
+{
+ Assert(d_consistent_ee);
std::map< TNode, TNode > subs;
- return isEntailed2( n, subs, false, false, pol, qy );
+ return isEntailed2(n, subs, false, false, pol);
}
-bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol, EqualityQuery * qy ) {
- if( qy==NULL ){
- Assert(d_consistent_ee);
- qy = d_quantEngine->getEqualityQuery();
- }
- return isEntailed2( n, subs, subsRep, true, pol, qy );
+bool TermDb::isEntailed(TNode n,
+ std::map<TNode, TNode>& subs,
+ bool subsRep,
+ bool pol)
+{
+ Assert(d_consistent_ee);
+ return isEntailed2(n, subs, subsRep, true, pol);
}
bool TermDb::isTermActive( Node n ) {
std::map< Node, Node >::iterator it = d_term_elig_eqc.find( r );
if( it==d_term_elig_eqc.end() ){
Node h;
- eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
- eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
+ eq::EqualityEngine* ee = d_qstate.getEqualityEngine();
+ eq::EqClassIterator eqc_i = eq::EqClassIterator(r, ee);
while (!eqc_i.isFinished())
{
TNode n = (*eqc_i);
d_func_map_rel_dom.clear();
d_consistent_ee = true;
- eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
+ eq::EqualityEngine* ee = d_qstate.getEqualityEngine();
Assert(ee->consistent());
// if higher-order, add equalities for the purification terms now
bool addedFirst = false;
Node first;
//TODO: ignoring singleton eqc isn't enough, need to ensure eqc are relevant
- eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
+ eq::EqClassIterator eqc_i = eq::EqClassIterator(r, ee);
while( !eqc_i.isFinished() ){
TNode n = (*eqc_i);
if( first.isNull() ){
//explicitly add inst closure terms to the equality engine to ensure only EE terms are indexed
for (const Node& n : d_iclosure_processed)
{
- if( !ee->hasTerm( n ) ){
- ee->addTerm( n );
+ if (!ee->hasTerm(n))
+ {
+ ee->addTerm(n);
}
}
if( r.getType().isFunction() ){
Trace("quant-ho") << " process function eqc " << r << std::endl;
Node first;
- eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
+ eq::EqClassIterator eqc_i = eq::EqClassIterator(r, ee);
while( !eqc_i.isFinished() ){
TNode n = (*eqc_i);
Node n_use;
class QuantifiersEngine;
-namespace inst{
- class Trigger;
- class HigherOrderTrigger;
-}
-
namespace quantifiers {
-namespace fmcheck {
- class FullModelChecker;
-}
-
-class TermDbSygus;
-class QuantConflictFind;
-class RelevantDomain;
class ConjectureGenerator;
-class TermGenerator;
class TermGenEnv;
/** Term Database
/** evaluate term
*
* Returns a term n' such that n = n' is entailed based on the equality
- * information qy. This function may generate new terms. In particular,
+ * information ee. This function may generate new terms. In particular,
* we typically rewrite subterms of n of maximal size to terms that exist in
- * the equality engine specified by qy.
+ * the equality engine specified by ee.
*
* useEntailmentTests is whether to call the theory engine's entailmentTest
* on literals n for which this call fails to find a term n' that is
*/
Node evaluateTerm(TNode n,
std::vector<Node>& exp,
- EqualityQuery* qy = NULL,
bool useEntailmentTests = false,
bool reqHasTerm = false);
/** same as above, without exp */
Node evaluateTerm(TNode n,
- EqualityQuery* qy = NULL,
bool useEntailmentTests = false,
bool reqHasTerm = false);
/** get entailed term
*
- * If possible, returns a term n' such that:
- * (1) n' exists in the current equality engine (as specified by qy),
- * (2) n = n' is entailed in the current context.
- * It returns null if no such term can be found.
- * Wrt evaluateTerm, this version does not construct new terms, and
- * thus is less aggressive.
- */
- TNode getEntailedTerm(TNode n, EqualityQuery* qy = NULL);
+ * If possible, returns a term n' such that:
+ * (1) n' exists in the current equality engine (as specified by the state),
+ * (2) n = n' is entailed in the current context.
+ * It returns null if no such term can be found.
+ * Wrt evaluateTerm, this version does not construct new terms, and
+ * thus is less aggressive.
+ */
+ TNode getEntailedTerm(TNode n);
/** get entailed term
*
- * If possible, returns a term n' such that:
- * (1) n' exists in the current equality engine (as specified by qy),
- * (2) n * subs = n' is entailed in the current context, where * is denotes
- * substitution application.
- * It returns null if no such term can be found.
- * subsRep is whether the substitution maps to terms that are representatives
- * according to qy.
- * Wrt evaluateTerm, this version does not construct new terms, and
- * thus is less aggressive.
- */
- TNode getEntailedTerm(TNode n,
- std::map<TNode, TNode>& subs,
- bool subsRep,
- EqualityQuery* qy = NULL);
+ * If possible, returns a term n' such that:
+ * (1) n' exists in the current equality engine (as specified by the state),
+ * (2) n * subs = n' is entailed in the current context, where * denotes
+ * substitution application.
+ * It returns null if no such term can be found.
+ * subsRep is whether the substitution maps to terms that are representatives
+ * according to the quantifiers state.
+ * Wrt evaluateTerm, this version does not construct new terms, and
+ * thus is less aggressive.
+ */
+ TNode getEntailedTerm(TNode n, std::map<TNode, TNode>& subs, bool subsRep);
/** is entailed
- * Checks whether the current context entails n with polarity pol, based on the
- * equality information qy.
- * Returns true if the entailment can be successfully shown.
- */
- bool isEntailed(TNode n, bool pol, EqualityQuery* qy = NULL);
+ * Checks whether the current context entails n with polarity pol, based on
+ * the equality information in the quantifiers state. Returns true if the
+ * entailment can be successfully shown.
+ */
+ bool isEntailed(TNode n, bool pol);
/** is entailed
*
- * Checks whether the current context entails ( n * subs ) with polarity pol,
- * based on the equality information qy,
- * where * denotes substitution application.
- * subsRep is whether the substitution maps to terms that are representatives
- * according to qy.
- */
+ * Checks whether the current context entails ( n * subs ) with polarity pol,
+ * based on the equality information in the quantifiers state,
+ * where * denotes substitution application.
+ * subsRep is whether the substitution maps to terms that are representatives
+ * according to in the quantifiers state.
+ */
bool isEntailed(TNode n,
std::map<TNode, TNode>& subs,
bool subsRep,
- bool pol,
- EqualityQuery* qy = NULL);
+ bool pol);
/** is the term n active in the current context?
*
* By default, all terms are active. A term is inactive if:
Node evaluateTerm2(TNode n,
std::map<TNode, Node>& visited,
std::vector<Node>& exp,
- EqualityQuery* qy,
bool useEntailmentTests,
bool computeExp,
bool reqHasTerm);
/** helper for get entailed term */
- TNode getEntailedTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, EqualityQuery * qy );
+ TNode getEntailedTerm2(TNode n,
+ std::map<TNode, TNode>& subs,
+ bool subsRep,
+ bool hasSubs);
/** helper for is entailed */
- bool isEntailed2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol, EqualityQuery * qy );
+ bool isEntailed2(TNode n,
+ std::map<TNode, TNode>& subs,
+ bool subsRep,
+ bool hasSubs,
+ bool pol);
/** compute uf eqc terms :
* Ensure entries for f are in d_func_map_eqc_trie for all equivalence classes
*/
d_valuation.setUnevaluatedKind(WITNESS);
}
+bool TheoryQuantifiers::needsEqualityEngine(EeSetupInfo& esi)
+{
+ // use the master equality engine
+ esi.d_useMaster = true;
+ return true;
+}
+
void TheoryQuantifiers::preRegisterTerm(TNode n)
{
if (n.getKind() != FORALL)
getQuantifiersEngine()->addTermToDatabase(atom[0], false, true);
if (!options::lteRestrictInstClosure())
{
- getQuantifiersEngine()->getMasterEqualityEngine()->addTerm(atom[0]);
+ d_qstate.getEqualityEngine()->addTerm(atom[0]);
}
}
else
TheoryRewriter* getTheoryRewriter() override;
/** finish initialization */
void finishInit() override;
+ /** needs equality engine */
+ bool needsEqualityEngine(EeSetupInfo& esi) override;
//--------------------------------- end initialization
void preRegisterTerm(TNode n) override;
d_qim(qim),
d_te(nullptr),
d_decManager(nullptr),
- d_masterEqualityEngine(nullptr),
d_eq_query(new quantifiers::EqualityQueryQuantifiersEngine(qstate, this)),
d_tr_trie(new inst::TriggerTrie),
d_model(nullptr),
QuantifiersEngine::~QuantifiersEngine() {}
-void QuantifiersEngine::finishInit(TheoryEngine* te,
- DecisionManager* dm,
- eq::EqualityEngine* mee)
+void QuantifiersEngine::finishInit(TheoryEngine* te, DecisionManager* dm)
{
d_te = te;
d_decManager = dm;
- d_masterEqualityEngine = mee;
// Initialize the modules and the utilities here.
d_qmodules.reset(new quantifiers::QuantifiersModules);
d_qmodules->initialize(this, d_qstate, d_qim, d_modules);
{
return d_te->theoryOf(THEORY_QUANTIFIERS)->getOutputChannel();
}
-/** get default valuation for the quantifiers engine */
Valuation& QuantifiersEngine::getValuation() { return d_qstate.getValuation(); }
-EqualityQuery* QuantifiersEngine::getEqualityQuery() const
+quantifiers::QuantifiersState& QuantifiersEngine::getState()
{
- return d_eq_query.get();
+ return d_qstate;
+}
+quantifiers::QuantifiersInferenceManager&
+QuantifiersEngine::getInferenceManager()
+{
+ return d_qim;
}
quantifiers::QModelBuilder* QuantifiersEngine::getModelBuilder() const
{
void QuantifiersEngine::check( Theory::Effort e ){
CodeTimer codeTimer(d_statistics.d_time);
-
- if (!getMasterEqualityEngine()->consistent())
+ Assert(d_qstate.getEqualityEngine() != nullptr);
+ if (!d_qstate.getEqualityEngine()->consistent())
{
Trace("quant-engine-debug") << "Master equality engine not consistent, return." << std::endl;
return;
return !d_lemmas_waiting.empty() || d_hasAddedLemma;
}
-bool QuantifiersEngine::inConflict() const { return d_qstate.isInConflict(); }
-
bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) {
Trace("quant-engine-debug2") << "Get inst when needs check, counts=" << d_ierCounter << ", " << d_ierCounter_lc << std::endl;
//determine if we should perform check, based on instWhenMode
smtStatisticsRegistry()->unregisterStat(&d_instantiations_rr);
}
-eq::EqualityEngine* QuantifiersEngine::getMasterEqualityEngine() const
-{
- return d_masterEqualityEngine;
-}
-
Node QuantifiersEngine::getInternalRepresentative( Node a, Node q, int index ){
return d_eq_query->getInternalRepresentative(a, q, index);
}
}
void QuantifiersEngine::debugPrintEqualityEngine( const char * c ) {
- eq::EqualityEngine* ee = getMasterEqualityEngine();
+ eq::EqualityEngine* ee = d_qstate.getEqualityEngine();
eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
std::map< TypeNode, int > typ_num;
while( !eqcs_i.isFinished() ){
OutputChannel& getOutputChannel();
/** get default valuation for the quantifiers engine */
Valuation& getValuation();
+ /** The quantifiers state object */
+ quantifiers::QuantifiersState& getState();
+ /** The quantifiers inference manager */
+ quantifiers::QuantifiersInferenceManager& getInferenceManager();
//---------------------- end external interface
//---------------------- utilities
- /** get the master equality engine */
- eq::EqualityEngine* getMasterEqualityEngine() const;
- /** get equality query */
- EqualityQuery* getEqualityQuery() const;
/** get the model builder */
quantifiers::QModelBuilder* getModelBuilder() const;
/** get model */
*
* @param te The theory engine
* @param dm The decision manager of the theory engine
- * @param mee The master equality engine of the theory engine
*/
- void finishInit(TheoryEngine* te,
- DecisionManager* dm,
- eq::EqualityEngine* mee);
+ void finishInit(TheoryEngine* te, DecisionManager* dm);
//---------------------- end private initialization
/**
* Maps quantified formulas to the module that owns them, if any module has
void markRelevant(Node q);
/** has added lemma */
bool hasAddedLemma() const;
- /** is in conflict */
- bool inConflict() const;
/** get current q effort */
QuantifiersModule::QEffort getCurrentQEffort() { return d_curr_effort_level; }
/** get number of waiting lemmas */
TheoryEngine* d_te;
/** Reference to the decision manager of the theory engine */
DecisionManager* d_decManager;
- /** Pointer to the master equality engine */
- eq::EqualityEngine* d_masterEqualityEngine;
/** vector of utilities for quantifiers */
std::vector<QuantifiersUtil*> d_util;
/** vector of modules for quantifiers */
// finish initializing the quantifiers engine
if (d_logicInfo.isQuantified())
{
- d_quantEngine->finishInit(
- this, d_decManager.get(), d_tc->getCoreEqualityEngine());
+ d_quantEngine->finishInit(this, d_decManager.get());
}
// finish initializing the theories by linking them with the appropriate
return d_ee->areDisequal(a, b, false);
}
+void TheoryState::getEquivalenceClass(Node a, std::vector<Node>& eqc) const
+{
+ if (d_ee->hasTerm(a))
+ {
+ Node rep = d_ee->getRepresentative(a);
+ eq::EqClassIterator eqc_iter(rep, d_ee);
+ while (!eqc_iter.isFinished())
+ {
+ eqc.push_back(*eqc_iter);
+ eqc_iter++;
+ }
+ }
+ else
+ {
+ eqc.push_back(a);
+ }
+ // a should be in its equivalence class
+ Assert(std::find(eqc.begin(), eqc.end(), a) != eqc.end());
+}
+
eq::EqualityEngine* TheoryState::getEqualityEngine() const { return d_ee; }
void TheoryState::notifyInConflict() { d_conflict = true; }
* returns true if the representative of a and b are distinct constants.
*/
virtual bool areDisequal(TNode a, TNode b) const;
+ /** get list of members in the equivalence class of a */
+ virtual void getEquivalenceClass(Node a, std::vector<Node>& eqc) const;
/** get equality engine */
eq::EqualityEngine* getEqualityEngine() const;
//-------------------------------------- end equality information
projects / cvc5.git / commitdiff