d_theoryEngine->setPropEngine(d_propEngine);
d_theoryEngine->setDecisionEngine(d_decisionEngine);
+ d_theoryEngine->finishInit();
// [MGD 10/20/2011] keep around in incremental mode, due to a
// cleanup ordering issue and Nodes/TNodes. If SAT is popped
StatisticsRegistry::unregisterStat(&d_conflicts);
}
+void ArithCongruenceManager::setMasterEqualityEngine(eq::EqualityEngine* eq) {
+ d_ee.setMasterEqualityEngine(eq);
+}
+
void ArithCongruenceManager::watchedVariableIsZero(Constraint lb, Constraint ub){
Assert(lb->isLowerBound());
Assert(ub->isUpperBound());
return d_explanationMap.find(n) != d_explanationMap.end();
}
+ void setMasterEqualityEngine(eq::EqualityEngine* eq);
+
private:
Node externalToInternal(TNode n) const{
Assert(canExplain(n));
TheoryArith::~TheoryArith(){}
+void TheoryArith::setMasterEqualityEngine(eq::EqualityEngine* eq) {
+ d_congruenceManager.setMasterEqualityEngine(eq);
+}
+
Node skolemFunction(const std::string& name, TypeNode dom, TypeNode range){
NodeManager* currNM = NodeManager::currentNM();
TypeNode functionType = currNM->mkFunctionType(dom, range);
*/
void preRegisterTerm(TNode n);
+ void setMasterEqualityEngine(eq::EqualityEngine* eq);
+
void check(Effort e);
void propagate(Effort e);
Node explain(TNode n);
}
}
-
TheoryArrays::~TheoryArrays() {
StatisticsRegistry::unregisterStat(&d_numRow);
}
+void TheoryArrays::setMasterEqualityEngine(eq::EqualityEngine* eq) {
+ d_equalityEngine.setMasterEqualityEngine(eq);
+}
+
/////////////////////////////////////////////////////////////////////////////
// PREPROCESSING
TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe);
~TheoryArrays();
+ void setMasterEqualityEngine(eq::EqualityEngine* eq);
+
std::string identify() const { return std::string("TheoryArrays"); }
/////////////////////////////////////////////////////////////////////////////
}
}
+void EqualitySolver::setMasterEqualityEngine(eq::EqualityEngine* eq) {
+ d_equalityEngine.setMasterEqualityEngine(eq);
+}
+
void EqualitySolver::preRegister(TNode node) {
if (!d_useEqualityEngine)
return;
public:
EqualitySolver(context::Context* c, TheoryBV* bv);
-
+ void setMasterEqualityEngine(eq::EqualityEngine* eq);
void preRegister(TNode node);
bool addAssertions(const std::vector<TNode>& assertions, Theory::Effort e);
void explain(TNode literal, std::vector<TNode>& assumptions);
TheoryBV::~TheoryBV() {}
+
+void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) {
+ d_equalitySolver.setMasterEqualityEngine(eq);
+}
+
TheoryBV::Statistics::Statistics():
d_avgConflictSize("theory::bv::AvgBVConflictSize"),
d_solveSubstitutions("theory::bv::NumberOfSolveSubstitutions", 0),
TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe);
~TheoryBV();
+ void setMasterEqualityEngine(eq::EqualityEngine* eq);
+
void preRegisterTerm(TNode n);
void check(Effort e);
TheoryDatatypes::~TheoryDatatypes() {
}
+void TheoryDatatypes::setMasterEqualityEngine(eq::EqualityEngine* eq) {
+ d_equalityEngine.setMasterEqualityEngine(eq);
+}
+
TheoryDatatypes::EqcInfo* TheoryDatatypes::getOrMakeEqcInfo( Node n, bool doMake ){
std::map< Node, EqcInfo* >::iterator eqc_i = d_eqc_info.find( n );
if( !hasEqcInfo( n ) ){
TheoryDatatypes(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation,
const LogicInfo& logicInfo, QuantifiersEngine* qe);
~TheoryDatatypes();
+
+ void setMasterEqualityEngine(eq::EqualityEngine* eq);
+
/** propagate */
void propagate(Effort effort);
/** propagate */
TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) :
Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo, qe),
- d_numRestarts(0){
+ d_numRestarts(0),
+ d_masterEqualityEngine(0)
+{
d_numInstantiations = 0;
d_baseDecLevel = -1;
out.handleUserAttribute( "axiom", this );
out.handleUserAttribute( "conjecture", this );
}
-
TheoryQuantifiers::~TheoryQuantifiers() {
}
+void TheoryQuantifiers::setMasterEqualityEngine(eq::EqualityEngine* eq) {
+ d_masterEqualityEngine = eq;
+}
+
void TheoryQuantifiers::addSharedTerm(TNode t) {
Debug("quantifiers-other") << "TheoryQuantifiers::addSharedTerm(): "
<< t << endl;
class TheoryEngine;
namespace theory {
+
namespace quantifiers {
class ModelEngine;
KEEP_STATISTIC(TimerStat, d_theoryTime, "theory::quantifiers::theoryTime");
+ eq::EqualityEngine* d_masterEqualityEngine;
+
public:
TheoryQuantifiers(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe);
~TheoryQuantifiers();
+ void setMasterEqualityEngine(eq::EqualityEngine* eq);
+
void addSharedTerm(TNode t);
void notifyEq(TNode lhs, TNode rhs);
void preRegisterTerm(TNode n);
class CandidateGenerator;
}
+namespace eq {
+class EqualityEngine;
+}
+
/**
* Information about an assertion for the theories.
*/
* Construct a Theory.
*/
Theory(TheoryId id, context::Context* satContext, context::UserContext* userContext,
- OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) throw()
+ OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo,
+ QuantifiersEngine* qe, eq::EqualityEngine* master = 0) throw()
: d_id(id)
, d_satContext(satContext)
, d_userContext(userContext)
*/
virtual void addSharedTerm(TNode n) { }
+ /**
+ * Called to set the master equality engine.
+ */
+ virtual void setMasterEqualityEngine(eq::EqualityEngine* eq) { }
+
/**
* Return the current theory care graph. Theories should overload computeCareGraph to do
* the actual computation, and use addCarePair to add pairs to the care graph.
#include "theory/quantifiers/model_engine.h"
#include "theory/quantifiers/first_order_model.h"
+#include "theory/uf/equality_engine.h"
using namespace std;
using namespace CVC4;
using namespace CVC4::theory;
+void TheoryEngine::finishInit() {
+ if (d_logicInfo.isQuantified()) {
+ Assert(d_masterEqualityEngine == 0);
+ d_masterEqualityEngine = new eq::EqualityEngine(getSatContext(), "theory::master");
+
+ for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) {
+ if (d_theoryTable[theoryId]) {
+ d_theoryTable[theoryId]->setMasterEqualityEngine(d_masterEqualityEngine);
+ }
+ }
+ }
+}
+
TheoryEngine::TheoryEngine(context::Context* context,
context::UserContext* userContext,
RemoveITE& iteRemover,
d_userContext(userContext),
d_logicInfo(logicInfo),
d_sharedTerms(this, context),
+ d_masterEqualityEngine(NULL),
d_quantEngine(NULL),
d_curr_model(NULL),
d_curr_model_builder(NULL),
delete d_quantEngine;
+ delete d_masterEqualityEngine;
+
StatisticsRegistry::unregisterStat(&d_combineTheoriesTime);
}
}
}
-
-template<typename T, bool doAssert>
-class scoped_vector_clear {
- vector<T>& d_v;
-public:
- scoped_vector_clear(vector<T>& v)
- : d_v(v) {
- Assert(!doAssert || d_v.empty());
- }
- ~scoped_vector_clear() {
- d_v.clear();
- }
-
-};
-
/**
* Check all (currently-active) theories for conflicts.
* @param effort the effort level to use
class Instantiator;
class TheoryModel;
class TheoryEngineModelBuilder;
+
+ namespace eq {
+ class EqualityEngine;
+ }
}/* CVC4::theory namespace */
+
class DecisionEngine;
/**
*/
SharedTermsDatabase d_sharedTerms;
+ /**
+ * Master equality engine, to share with theories.
+ */
+ theory::eq::EqualityEngine* d_masterEqualityEngine;
+
/**
* The quantifiers engine
*/
d_decisionEngine = decisionEngine;
}
+ /** Called when all initialization of options/logic is done */
+ void finishInit();
+
/**
* Get a pointer to the underlying propositional engine.
*/
}
-EqualityEngine::EqualityEngine(context::Context* context, std::string name)
+EqualityEngine::EqualityEngine(context::Context* context, std::string name)
: ContextNotifyObj(context)
+, d_masterEqualityEngine(0)
, d_context(context)
, d_done(context, false)
, d_performNotify(true)
EqualityEngine::EqualityEngine(EqualityEngineNotify& notify, context::Context* context, std::string name)
: ContextNotifyObj(context)
+, d_masterEqualityEngine(0)
, d_context(context)
, d_done(context, false)
, d_performNotify(true)
init();
}
+void EqualityEngine::setMasterEqualityEngine(EqualityEngine* master) {
+ Assert(d_masterEqualityEngine == 0);
+ d_masterEqualityEngine = master;
+}
+
void EqualityEngine::enqueue(const MergeCandidate& candidate, bool back) {
Debug("equality") << d_name << "::eq::enqueue(" << d_nodes[candidate.t1Id] << ", " << d_nodes[candidate.t2Id] << ", " << candidate.type << ")" << std::endl;
if (back) {
d_nodeIndividualTrigger[tId] = newTriggerTermSet();
}
+ // If this is not an internal node, add it to the master
+ if (d_masterEqualityEngine && !d_isInternal[result]) {
+ d_masterEqualityEngine->addTerm(t);
+ }
+
propagate();
Debug("equality") << d_name << "::eq::addTerm(" << t << ") => " << result << std::endl;
continue;
}
- // Depending on the merge preference (such as size, or being a constant), merge them
+ // Vector to collect the triggered events
std::vector<TriggerId> triggers;
- if ((node2.getSize() > node1.getSize() && !d_isConstant[t1classId]) || d_isConstant[t2classId]) {
+
+ // Figure out the merge preference
+ EqualityNodeId mergeInto = t1classId;
+ if (d_isInternal[t2classId] != d_isInternal[t1classId]) {
+ // We always keep non-internal nodes as representatives: if any node in
+ // the class is non-internal, then the representative will be non-internal
+ if (d_isInternal[t1classId]) {
+ mergeInto = t2classId;
+ } else {
+ mergeInto = t1classId;
+ }
+ } else if (d_isConstant[t2classId] != d_isConstant[t1classId]) {
+ // We always keep constants as representatives: if any (at most one) node
+ // in the class in a constant, then the representative will be a constant
+ if (d_isConstant[t2classId]) {
+ mergeInto = t2classId;
+ } else {
+ mergeInto = t1classId;
+ }
+ } else if (node2.getSize() > node1.getSize()) {
+ // We always merge into the bigger class to reduce the amount of traversing
+ // we need to do
+ mergeInto = t2classId;
+ }
+
+ if (mergeInto == t2classId) {
Debug("equality") << d_name << "::eq::propagate(): merging " << d_nodes[current.t1Id]<< " into " << d_nodes[current.t2Id] << std::endl;
d_assertedEqualities.push_back(Equality(t2classId, t1classId));
d_assertedEqualitiesCount = d_assertedEqualitiesCount + 1;
}
}
+ // If not merging internal nodes, notify the master
+ if (d_masterEqualityEngine && !d_isInternal[mergeInto]) {
+ d_masterEqualityEngine->assertEqualityInternal(d_nodes[t1classId], d_nodes[t2classId], TNode::null());
+ d_masterEqualityEngine->propagate();
+ }
+
// Notify the triggers
if (d_performNotify && !d_done) {
for (size_t trigger_i = 0, trigger_end = triggers.size(); trigger_i < trigger_end && !d_done; ++ trigger_i) {
/** Default implementation of the notification object */
static EqualityEngineNotifyNone s_notifyNone;
+ /**
+ * Master equality engine that gets all the equality information from
+ * this one, or null if none.
+ */
+ EqualityEngine* d_masterEqualityEngine;
+
public:
+ /**
+ * Initialize the equality engine, given the notification class.
+ */
+ EqualityEngine(EqualityEngineNotify& notify, context::Context* context, std::string name);
+
+ /**
+ * Initialize the equality engine with no notification class.
+ */
+ EqualityEngine(context::Context* context, std::string name);
+
+ /**
+ * Just a destructor.
+ */
+ virtual ~EqualityEngine() throw(AssertionException);
+
+ /**
+ * Set the master equality engine for this one. Master engine will get copies of all
+ * the terms and equalities from this engine.
+ */
+ void setMasterEqualityEngine(EqualityEngine* master);
+
/** Statistics about the equality engine instance */
struct Statistics {
/** Total number of merges */
public:
- /**
- * Initialize the equality engine, given the notification class.
- */
- EqualityEngine(EqualityEngineNotify& notify, context::Context* context, std::string name);
-
- /**
- * Initialize the equality engine with no notification class.
- */
- EqualityEngine(context::Context* context, std::string name);
-
- /**
- * Just a destructor.
- */
- virtual ~EqualityEngine() throw(AssertionException);
-
/**
* Adds a term to the term database.
*/
d_equalityEngine.addFunctionKind(kind::APPLY_UF);
}
+void TheoryUF::setMasterEqualityEngine(eq::EqualityEngine* eq) {
+ d_equalityEngine.setMasterEqualityEngine(eq);
+}
+
static Node mkAnd(const std::vector<TNode>& conjunctions) {
Assert(conjunctions.size() > 0);
}
}
+ void setMasterEqualityEngine(eq::EqualityEngine* eq);
+
void check(Effort);
void preRegisterTerm(TNode term);
Node explain(TNode n);
projects / cvc5.git / commitdiff