This commit updates Theory so that equality engines are allocated dynamically. The plan is to make this configurable based on the theory combination method.
The fundamental changes include:
- Add `d_equalityEngine` (raw) pointer to Theory, which is the "official" equality engine of the theory.
- Standardize methods for initializing Theory. This is now made more explicit in the documentation in theory.h, and includes a method `finishInitStandalone` for users of Theory that don't have an associated TheoryEngine.
- Refactor TheoryEngine::finishInit, including how Theory is initialized to incorporate the new policy.
- Things related to master equality engine are now specific to EqEngineManagerDistributed and hence can be removed from TheoryEngine. This will be further refactored in forthcoming PRs.
Note that the majority of changes are due to changing `d_equalityEngine.` to `d_equalityEngine->` throughout.
InternalError() << "can't generate theory-proof for "
<< ProofManager::currentPM()->getLogic();
}
+ // must perform initialization on the theory
+ if (th != nullptr)
+ {
+ // finish init, standalone version
+ th->finishInitStandalone();
+ }
Debug("pf::tp") << "TheoryProof::printTheoryLemmaProof - calling th->ProduceProofs()" << std::endl;
th->produceProofs();
d_constraintDatabase(cd),
d_setupLiteral(setup),
d_avariables(avars),
- d_ee(d_notify, c, "theory::arith::ArithCongruenceManager", true)
+ d_ee(nullptr)
{
- d_ee.addFunctionKind(kind::NONLINEAR_MULT);
- d_ee.addFunctionKind(kind::EXPONENTIAL);
- d_ee.addFunctionKind(kind::SINE);
- d_ee.addFunctionKind(kind::IAND);
}
ArithCongruenceManager::~ArithCongruenceManager() {}
+bool ArithCongruenceManager::needsEqualityEngine(EeSetupInfo& esi)
+{
+ esi.d_notify = &d_notify;
+ esi.d_name = "theory::arith::ArithCongruenceManager";
+ return true;
+}
+
+void ArithCongruenceManager::finishInit(eq::EqualityEngine* ee)
+{
+ Assert(ee != nullptr);
+ d_ee = ee;
+ d_ee->addFunctionKind(kind::NONLINEAR_MULT);
+ d_ee->addFunctionKind(kind::EXPONENTIAL);
+ d_ee->addFunctionKind(kind::SINE);
+ d_ee->addFunctionKind(kind::IAND);
+}
+
ArithCongruenceManager::Statistics::Statistics():
d_watchedVariables("theory::arith::congruence::watchedVariables", 0),
d_watchedVariableIsZero("theory::arith::congruence::watchedVariableIsZero", 0),
return d_explanationMap.find(n) != d_explanationMap.end();
}
-void ArithCongruenceManager::setMasterEqualityEngine(eq::EqualityEngine* eq) {
- d_ee.setMasterEqualityEngine(eq);
-}
-
Node ArithCongruenceManager::externalToInternal(TNode n) const{
Assert(canExplain(n));
ExplainMap::const_iterator iter = d_explanationMap.find(n);
void ArithCongruenceManager::explain(TNode literal, std::vector<TNode>& assumptions) {
if (literal.getKind() != kind::NOT) {
- d_ee.explainEquality(literal[0], literal[1], true, assumptions);
+ d_ee->explainEquality(literal[0], literal[1], true, assumptions);
} else {
- d_ee.explainEquality(literal[0][0], literal[0][1], false, assumptions);
+ d_ee->explainEquality(literal[0][0], literal[0][1], false, assumptions);
}
}
Trace("arith-ee") << "Assert " << eq << ", pol " << isEquality << ", reason " << reason << std::endl;
if(isEquality){
- d_ee.assertEquality(eq, true, reason);
+ d_ee->assertEquality(eq, true, reason);
}else{
- d_ee.assertEquality(eq, false, reason);
+ d_ee->assertEquality(eq, false, reason);
}
}
d_keepAlive.push_back(reason);
Trace("arith-ee") << "Assert equalsConstant " << eq << ", reason " << reason << std::endl;
- d_ee.assertEquality(eq, true, reason);
+ d_ee->assertEquality(eq, true, reason);
}
void ArithCongruenceManager::equalsConstant(ConstraintCP lb, ConstraintCP ub){
d_keepAlive.push_back(reason);
Trace("arith-ee") << "Assert equalsConstant2 " << eq << ", reason " << reason << std::endl;
- d_ee.assertEquality(eq, true, reason);
+ d_ee->assertEquality(eq, true, reason);
}
void ArithCongruenceManager::addSharedTerm(Node x){
- d_ee.addTriggerTerm(x, THEORY_ARITH);
+ d_ee->addTriggerTerm(x, THEORY_ARITH);
}
}/* CVC4::theory::arith namespace */
const ArithVariables& d_avariables;
- eq::EqualityEngine d_ee;
+ /** The equality engine being used by this class */
+ eq::EqualityEngine* d_ee;
void raiseConflict(Node conflict);
public:
bool canExplain(TNode n) const;
- void setMasterEqualityEngine(eq::EqualityEngine* eq);
-
private:
Node externalToInternal(TNode n) const;
ArithCongruenceManager(context::Context* satContext, ConstraintDatabase&, SetupLiteralCallBack, const ArithVariables&, RaiseEqualityEngineConflict raiseConflict);
~ArithCongruenceManager();
+ //--------------------------------- initialization
+ /**
+ * Returns true if we need an equality engine, see
+ * Theory::needsEqualityEngine.
+ */
+ bool needsEqualityEngine(EeSetupInfo& esi);
+ /**
+ * Finish initialize. This class is instructed by TheoryArithPrivate to use
+ * the equality engine ee.
+ */
+ void finishInit(eq::EqualityEngine* ee);
+ //--------------------------------- end initialization
+
Node explain(TNode literal);
void explain(TNode lit, NodeBuilder<>& out);
void addSharedTerm(Node x);
-
- eq::EqualityEngine * getEqualityEngine() { return &d_ee; }
-private:
+ private:
class Statistics {
public:
IntStat d_watchedVariables;
return d_internal->getTheoryRewriter();
}
-void TheoryArith::preRegisterTerm(TNode n){
- d_internal->preRegisterTerm(n);
+bool TheoryArith::needsEqualityEngine(EeSetupInfo& esi)
+{
+ return d_internal->needsEqualityEngine(esi);
}
-
void TheoryArith::finishInit()
{
if (getLogicInfo().isTheoryEnabled(THEORY_ARITH)
d_valuation.setUnevaluatedKind(kind::SINE);
d_valuation.setUnevaluatedKind(kind::PI);
}
+ // finish initialize internally
+ d_internal->finishInit();
}
+void TheoryArith::preRegisterTerm(TNode n) { d_internal->preRegisterTerm(n); }
+
TrustNode TheoryArith::expandDefinition(Node node)
{
return d_internal->expandDefinition(node);
}
-void TheoryArith::setMasterEqualityEngine(eq::EqualityEngine* eq) {
- d_internal->setMasterEqualityEngine(eq);
-}
-
void TheoryArith::addSharedTerm(TNode n){
d_internal->addSharedTerm(n);
}
ProofNodeManager* pnm = nullptr);
virtual ~TheoryArith();
+ //--------------------------------- initialization
+ /** get the official theory rewriter of this theory */
TheoryRewriter* getTheoryRewriter() override;
+ /**
+ * Returns true if this theory needs an equality engine, which is assigned
+ * to it (d_equalityEngine) by the equality engine manager during
+ * TheoryEngine::finishInit, prior to calling finishInit for this theory.
+ * If this method returns true, it stores instructions for the notifications
+ * this Theory wishes to receive from its equality engine.
+ */
+ bool needsEqualityEngine(EeSetupInfo& esi) override;
+ /** finish initialization */
+ void finishInit() override;
+ //--------------------------------- end initialization
/**
* Does non-context dependent setup for a node connected to a theory.
*/
void preRegisterTerm(TNode n) override;
- void finishInit() override;
-
TrustNode expandDefinition(Node node) override;
- void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
-
void check(Effort e) override;
bool needsCheckLastEffort() override;
void propagate(Effort e) override;
d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)),
d_attemptSolSimplex(
d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)),
- d_nonlinearExtension(NULL),
+ d_nonlinearExtension(nullptr),
d_pass1SDP(NULL),
d_otherSDP(NULL),
d_lastContextIntegerAttempted(c, -1),
d_statistics(),
d_opElim(pnm, logicInfo)
{
- // only need to create if non-linear logic
- if (logicInfo.isTheoryEnabled(THEORY_ARITH) && !logicInfo.isLinear())
- {
- d_nonlinearExtension = new nl::NonlinearExtension(
- containing, d_congruenceManager.getEqualityEngine());
- }
}
TheoryArithPrivate::~TheoryArithPrivate(){
if(d_nonlinearExtension != NULL) { delete d_nonlinearExtension; }
}
+TheoryRewriter* TheoryArithPrivate::getTheoryRewriter() { return &d_rewriter; }
+bool TheoryArithPrivate::needsEqualityEngine(EeSetupInfo& esi)
+{
+ return d_congruenceManager.needsEqualityEngine(esi);
+}
+void TheoryArithPrivate::finishInit()
+{
+ eq::EqualityEngine* ee = d_containing.getEqualityEngine();
+ Assert(ee != nullptr);
+ d_congruenceManager.finishInit(ee);
+ const LogicInfo& logicInfo = getLogicInfo();
+ // only need to create nonlinear extension if non-linear logic
+ if (logicInfo.isTheoryEnabled(THEORY_ARITH) && !logicInfo.isLinear())
+ {
+ d_nonlinearExtension = new nl::NonlinearExtension(d_containing, ee);
+ }
+}
+
static bool contains(const ConstraintCPVec& v, ConstraintP con){
for(unsigned i = 0, N = v.size(); i < N; ++i){
if(v[i] == con){
// return safeConstructNary(nb);
}
-void TheoryArithPrivate::setMasterEqualityEngine(eq::EqualityEngine* eq) {
- d_congruenceManager.setMasterEqualityEngine(eq);
-}
-
TheoryArithPrivate::ModelException::ModelException(TNode n, const char* msg)
{
stringstream ss;
ProofNodeManager* pnm);
~TheoryArithPrivate();
- TheoryRewriter* getTheoryRewriter() { return &d_rewriter; }
+ //--------------------------------- initialization
+ /** get the official theory rewriter of this theory */
+ TheoryRewriter* getTheoryRewriter();
+ /**
+ * Returns true if we need an equality engine, see
+ * Theory::needsEqualityEngine.
+ */
+ bool needsEqualityEngine(EeSetupInfo& esi);
+ /** finish initialize */
+ void finishInit();
+ //--------------------------------- end initialization
/**
* Does non-context dependent setup for a node connected to a theory.
void preRegisterTerm(TNode n);
TrustNode expandDefinition(Node node);
- void setMasterEqualityEngine(eq::EqualityEngine* eq);
-
void check(Theory::Effort e);
bool needsCheckLastEffort();
void propagate(Theory::Effort e);
d_isPreRegistered(c),
d_mayEqualEqualityEngine(c, name + "theory::arrays::mayEqual", true),
d_notify(*this),
- d_equalityEngine(d_notify, c, name + "theory::arrays", true),
d_conflict(c, false),
d_backtracker(c),
d_infoMap(c, &d_backtracker, name),
d_readTableContext(new context::Context()),
d_arrayMerges(c),
d_inCheckModel(false),
- d_proofReconstruction(&d_equalityEngine),
+ d_proofReconstruction(nullptr),
d_dstrat(new TheoryArraysDecisionStrategy(this)),
d_dstratInit(false)
{
// The preprocessing congruence kinds
d_ppEqualityEngine.addFunctionKind(kind::SELECT);
d_ppEqualityEngine.addFunctionKind(kind::STORE);
-
- // The kinds we are treating as function application in congruence
- d_equalityEngine.addFunctionKind(kind::SELECT);
- if (d_ccStore) {
- d_equalityEngine.addFunctionKind(kind::STORE);
- }
- if (d_useArrTable) {
- d_equalityEngine.addFunctionKind(kind::ARR_TABLE_FUN);
- }
-
- d_reasonRow = d_equalityEngine.getFreshMergeReasonType();
- d_reasonRow1 = d_equalityEngine.getFreshMergeReasonType();
- d_reasonExt = d_equalityEngine.getFreshMergeReasonType();
-
- d_proofReconstruction.setRowMergeTag(d_reasonRow);
- d_proofReconstruction.setRow1MergeTag(d_reasonRow1);
- d_proofReconstruction.setExtMergeTag(d_reasonExt);
-
- d_equalityEngine.addPathReconstructionTrigger(d_reasonRow, &d_proofReconstruction);
- d_equalityEngine.addPathReconstructionTrigger(d_reasonRow1, &d_proofReconstruction);
- d_equalityEngine.addPathReconstructionTrigger(d_reasonExt, &d_proofReconstruction);
}
TheoryArrays::~TheoryArrays() {
smtStatisticsRegistry()->unregisterStat(&d_numSetModelValConflicts);
}
-void TheoryArrays::setMasterEqualityEngine(eq::EqualityEngine* eq) {
- d_equalityEngine.setMasterEqualityEngine(eq);
+TheoryRewriter* TheoryArrays::getTheoryRewriter() { return &d_rewriter; }
+
+bool TheoryArrays::needsEqualityEngine(EeSetupInfo& esi)
+{
+ esi.d_notify = &d_notify;
+ esi.d_name = d_instanceName + "theory::arrays::ee";
+ return true;
+}
+
+void TheoryArrays::finishInit()
+{
+ Assert(d_equalityEngine != nullptr);
+
+ // The kinds we are treating as function application in congruence
+ d_equalityEngine->addFunctionKind(kind::SELECT);
+ if (d_ccStore)
+ {
+ d_equalityEngine->addFunctionKind(kind::STORE);
+ }
+ if (d_useArrTable)
+ {
+ d_equalityEngine->addFunctionKind(kind::ARR_TABLE_FUN);
+ }
+
+ d_proofReconstruction.reset(new ArrayProofReconstruction(d_equalityEngine));
+ d_reasonRow = d_equalityEngine->getFreshMergeReasonType();
+ d_reasonRow1 = d_equalityEngine->getFreshMergeReasonType();
+ d_reasonExt = d_equalityEngine->getFreshMergeReasonType();
+
+ d_proofReconstruction->setRowMergeTag(d_reasonRow);
+ d_proofReconstruction->setRow1MergeTag(d_reasonRow1);
+ d_proofReconstruction->setExtMergeTag(d_reasonExt);
+
+ d_equalityEngine->addPathReconstructionTrigger(d_reasonRow,
+ d_proofReconstruction.get());
+ d_equalityEngine->addPathReconstructionTrigger(d_reasonRow1,
+ d_proofReconstruction.get());
+ d_equalityEngine->addPathReconstructionTrigger(d_reasonExt,
+ d_proofReconstruction.get());
}
/////////////////////////////////////////////////////////////////////////////
//eq::EqProof * eqp = new eq::EqProof;
// eq::EqProof * eqp = NULL;
if (atom.getKind() == kind::EQUAL) {
- d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions, proof);
+ d_equalityEngine->explainEquality(
+ atom[0], atom[1], polarity, assumptions, proof);
} else {
- d_equalityEngine.explainPredicate(atom, polarity, assumptions, proof);
+ d_equalityEngine->explainPredicate(atom, polarity, assumptions, proof);
}
if (Debug.isOn("pf::array"))
{
return node;
}
index2 = d_infoMap.getWeakEquivIndex(node);
- if (index2.isNull() || !d_equalityEngine.areEqual(index, index2)) {
+ if (index2.isNull() || !d_equalityEngine->areEqual(index, index2))
+ {
node = pointer;
}
else {
conjunctions.push_back(reason);
break;
case kind::EQUAL:
- d_equalityEngine.explainEquality(reason[0], reason[1], true, conjunctions);
+ d_equalityEngine->explainEquality(
+ reason[0], reason[1], true, conjunctions);
break;
default:
Unreachable();
index2 = d_infoMap.getWeakEquivIndex(node);
if (index2.isNull()) {
// Null index means these two nodes became equal: explain the equality.
- d_equalityEngine.explainEquality(node, pointer, true, conjunctions);
+ d_equalityEngine->explainEquality(node, pointer, true, conjunctions);
node = pointer;
}
- else if (!d_equalityEngine.areEqual(index, index2)) {
+ else if (!d_equalityEngine->areEqual(index, index2))
+ {
// If indices are not equal in current context, need to add that to the lemma.
Node reason = index.eqNode(index2).notNode();
d_permRef.push_back(reason);
TNode index2 = d_infoMap.getWeakEquivIndex(secondary);
Node reason;
TNode next;
- while (index2.isNull() || !d_equalityEngine.areEqual(index, index2)) {
+ while (index2.isNull() || !d_equalityEngine->areEqual(index, index2))
+ {
next = d_infoMap.getWeakEquivPointer(secondary);
d_infoMap.setWeakEquivSecondary(node, next);
reason = d_infoMap.getWeakEquivSecondaryReason(node);
TNode pointer, indexRep;
if (!index.isNull()) {
index_trail.push_back(index);
- marked.insert(d_equalityEngine.getRepresentative(index));
+ marked.insert(d_equalityEngine->getRepresentative(index));
}
while (arrayFrom != arrayTo) {
index = d_infoMap.getWeakEquivIndex(arrayFrom);
pointer = d_infoMap.getWeakEquivPointer(arrayFrom);
if (!index.isNull()) {
- indexRep = d_equalityEngine.getRepresentative(index);
+ indexRep = d_equalityEngine->getRepresentative(index);
if (marked.find(indexRep) == marked.end() && weakEquivGetRepIndex(arrayFrom, index) != arrayTo) {
weakEquivMakeRepIndex(arrayFrom);
d_infoMap.setWeakEquivSecondary(arrayFrom, arrayTo);
|| !secondary.isNull());
if (!pointer.isNull()) {
if (index.isNull()) {
- Assert(d_equalityEngine.areEqual(n, pointer));
+ Assert(d_equalityEngine->areEqual(n, pointer));
}
else {
Assert(
case kind::EQUAL:
// Add the trigger for equality
// NOTE: note that if the equality is true or false already, it might not be added
- d_equalityEngine.addTriggerEquality(node);
+ d_equalityEngine->addTriggerEquality(node);
break;
case kind::SELECT: {
// Invariant: array terms should be preregistered before being added to the equality engine
- if (d_equalityEngine.hasTerm(node)) {
+ if (d_equalityEngine->hasTerm(node))
+ {
Assert(d_isPreRegistered.find(node) != d_isPreRegistered.end());
return;
}
// Reads
- TNode store = d_equalityEngine.getRepresentative(node[0]);
+ TNode store = d_equalityEngine->getRepresentative(node[0]);
// The may equal needs the store
d_mayEqualEqualityEngine.addTerm(store);
if (node.getType().isArray())
{
d_mayEqualEqualityEngine.addTerm(node);
- d_equalityEngine.addTriggerTerm(node, THEORY_ARRAYS);
+ d_equalityEngine->addTriggerTerm(node, THEORY_ARRAYS);
}
else
{
- d_equalityEngine.addTerm(node);
+ d_equalityEngine->addTerm(node);
}
Assert((d_isPreRegistered.insert(node), true));
- Assert(d_equalityEngine.getRepresentative(store) == store);
+ Assert(d_equalityEngine->getRepresentative(store) == store);
d_infoMap.addIndex(store, node[1]);
// Synchronize d_constReadsContext with SAT context
}
// Record read in sharing data structure
- TNode index = d_equalityEngine.getRepresentative(node[1]);
+ TNode index = d_equalityEngine->getRepresentative(node[1]);
if (!options::arraysWeakEquivalence() && index.isConst()) {
CTNodeList* temp;
CNodeNListMap::iterator it = d_constReads.find(index);
break;
}
case kind::STORE: {
- if (d_equalityEngine.hasTerm(node)) {
+ if (d_equalityEngine->hasTerm(node))
+ {
break;
}
- d_equalityEngine.addTriggerTerm(node, THEORY_ARRAYS);
+ d_equalityEngine->addTriggerTerm(node, THEORY_ARRAYS);
- TNode a = d_equalityEngine.getRepresentative(node[0]);
+ TNode a = d_equalityEngine->getRepresentative(node[0]);
if (node.isConst()) {
// Can't use d_mayEqualEqualityEngine to merge node with a because they are both constants,
TNode v = node[2];
NodeManager* nm = NodeManager::currentNM();
Node ni = nm->mkNode(kind::SELECT, node, i);
- if (!d_equalityEngine.hasTerm(ni)) {
+ if (!d_equalityEngine->hasTerm(ni))
+ {
preRegisterTermInternal(ni);
}
// Apply RIntro1 Rule
- d_equalityEngine.assertEquality(ni.eqNode(v), true, d_true, d_reasonRow1);
+ d_equalityEngine->assertEquality(ni.eqNode(v), true, d_true, d_reasonRow1);
d_infoMap.addStore(node, node);
d_infoMap.addInStore(a, node);
break;
}
case kind::STORE_ALL: {
- if (d_equalityEngine.hasTerm(node)) {
+ if (d_equalityEngine->hasTerm(node))
+ {
break;
}
ArrayStoreAll storeAll = node.getConst<ArrayStoreAll>();
d_infoMap.setConstArr(node, node);
d_mayEqualEqualityEngine.addTerm(node);
Assert(d_mayEqualEqualityEngine.getRepresentative(node) == node);
- d_equalityEngine.addTriggerTerm(node, THEORY_ARRAYS);
+ d_equalityEngine->addTriggerTerm(node, THEORY_ARRAYS);
d_defValues[node] = defaultValue;
break;
}
if (node.getType().isArray()) {
// The may equal needs the node
d_mayEqualEqualityEngine.addTerm(node);
- d_equalityEngine.addTriggerTerm(node, THEORY_ARRAYS);
- Assert(d_equalityEngine.getSize(node) == 1);
+ d_equalityEngine->addTriggerTerm(node, THEORY_ARRAYS);
+ Assert(d_equalityEngine->getSize(node) == 1);
}
else {
- d_equalityEngine.addTerm(node);
+ d_equalityEngine->addTerm(node);
}
break;
}
// Invariant: preregistered terms are exactly the terms in the equality engine
// Disabled, see comment above for kind::EQUAL
- // Assert(d_equalityEngine.hasTerm(node) ||
- // !d_equalityEngine.consistent());
+ // Assert(d_equalityEngine->hasTerm(node) ||
+ // !d_equalityEngine->consistent());
}
// Note: do this here instead of in preRegisterTermInternal to prevent internal select
// terms from being propagated out (as this results in an assertion failure).
if (node.getKind() == kind::SELECT && node.getType().isBoolean()) {
- d_equalityEngine.addTriggerPredicate(node);
+ d_equalityEngine->addTriggerPredicate(node);
}
}
void TheoryArrays::addSharedTerm(TNode t) {
Debug("arrays::sharing") << spaces(getSatContext()->getLevel()) << "TheoryArrays::addSharedTerm(" << t << ")" << std::endl;
- d_equalityEngine.addTriggerTerm(t, THEORY_ARRAYS);
+ d_equalityEngine->addTriggerTerm(t, THEORY_ARRAYS);
if (t.getType().isArray()) {
d_sharedArrays.insert(t);
}
EqualityStatus TheoryArrays::getEqualityStatus(TNode a, TNode b) {
- Assert(d_equalityEngine.hasTerm(a) && d_equalityEngine.hasTerm(b));
- if (d_equalityEngine.areEqual(a, b)) {
+ Assert(d_equalityEngine->hasTerm(a) && d_equalityEngine->hasTerm(b));
+ if (d_equalityEngine->areEqual(a, b))
+ {
// The terms are implied to be equal
return EQUALITY_TRUE;
}
- else if (d_equalityEngine.areDisequal(a, b, false)) {
+ else if (d_equalityEngine->areDisequal(a, b, false))
+ {
// The terms are implied to be dis-equal
return EQUALITY_FALSE;
}
TNode x = r1[1];
TNode y = r2[1];
- Assert(d_equalityEngine.isTriggerTerm(x, THEORY_ARRAYS));
+ Assert(d_equalityEngine->isTriggerTerm(x, THEORY_ARRAYS));
- if (d_equalityEngine.hasTerm(x) && d_equalityEngine.hasTerm(y) &&
- (d_equalityEngine.areEqual(x,y) || d_equalityEngine.areDisequal(x,y,false))) {
+ if (d_equalityEngine->hasTerm(x) && d_equalityEngine->hasTerm(y)
+ && (d_equalityEngine->areEqual(x, y)
+ || d_equalityEngine->areDisequal(x, y, false)))
+ {
Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): equality known, skipping" << std::endl;
return;
}
// If the terms are already known to be equal, we are also in good shape
- if (d_equalityEngine.areEqual(r1, r2)) {
+ if (d_equalityEngine->areEqual(r1, r2))
+ {
Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): equal, skipping" << std::endl;
return;
}
// If arrays are known to be disequal, or cannot become equal, we can continue
Assert(d_mayEqualEqualityEngine.hasTerm(r1[0])
&& d_mayEqualEqualityEngine.hasTerm(r2[0]));
- if (r1[0].getType() != r2[0].getType() ||
- d_equalityEngine.areDisequal(r1[0], r2[0], false)) {
+ if (r1[0].getType() != r2[0].getType()
+ || d_equalityEngine->areDisequal(r1[0], r2[0], false))
+ {
Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): arrays can't be equal, skipping" << std::endl;
return;
}
}
}
- if (!d_equalityEngine.isTriggerTerm(y, THEORY_ARRAYS)) {
+ if (!d_equalityEngine->isTriggerTerm(y, THEORY_ARRAYS))
+ {
Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): not connected to shared terms, skipping" << std::endl;
return;
}
// Get representative trigger terms
- TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_ARRAYS);
- TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_ARRAYS);
+ TNode x_shared =
+ d_equalityEngine->getTriggerTermRepresentative(x, THEORY_ARRAYS);
+ TNode y_shared =
+ d_equalityEngine->getTriggerTermRepresentative(y, THEORY_ARRAYS);
EqualityStatus eqStatusDomain = d_valuation.getEqualityStatus(x_shared, y_shared);
switch (eqStatusDomain) {
case EQUALITY_TRUE_AND_PROPAGATED:
TNode r1 = d_reads[i];
Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): checking read " << r1 << std::endl;
- Assert(d_equalityEngine.hasTerm(r1));
+ Assert(d_equalityEngine->hasTerm(r1));
TNode x = r1[1];
- if (!d_equalityEngine.isTriggerTerm(x, THEORY_ARRAYS)) {
+ if (!d_equalityEngine->isTriggerTerm(x, THEORY_ARRAYS))
+ {
Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): not connected to shared terms, skipping" << std::endl;
continue;
}
- Node x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_ARRAYS);
+ Node x_shared =
+ d_equalityEngine->getTriggerTermRepresentative(x, THEORY_ARRAYS);
// Get the model value of index and find all reads that read from that same model value: these are the pairs we have to check
// Also, insert this read in the list at the proper index
// We don't know the model value for x. Just do brute force examination of all pairs of reads
for (unsigned j = 0; j < size; ++j) {
TNode r2 = d_reads[j];
- Assert(d_equalityEngine.hasTerm(r2));
+ Assert(d_equalityEngine->hasTerm(r2));
checkPair(r1,r2);
}
for (unsigned j = 0; j < d_constReadsList.size(); ++j) {
TNode r2 = d_constReadsList[j];
- Assert(d_equalityEngine.hasTerm(r2));
+ Assert(d_equalityEngine->hasTerm(r2));
checkPair(r1,r2);
}
}
NodeManager* nm = NodeManager::currentNM();
std::vector<Node> arrays;
bool computeRep, isArray;
- eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(&d_equalityEngine);
+ eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(d_equalityEngine);
for (; !eqcs_i.isFinished(); ++eqcs_i) {
Node eqc = (*eqcs_i);
isArray = eqc.getType().isArray();
continue;
}
computeRep = false;
- eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, &d_equalityEngine);
+ eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, d_equalityEngine);
for (; !eqc_i.isFinished(); ++eqc_i) {
Node n = *eqc_i;
// If this EC is an array type and it contains something other than STORE nodes, we have to compute a representative explicitly
bool changed;
do {
changed = false;
- eqcs_i = eq::EqClassesIterator(&d_equalityEngine);
+ eqcs_i = eq::EqClassesIterator(d_equalityEngine);
for (; !eqcs_i.isFinished(); ++eqcs_i) {
Node eqc = (*eqcs_i);
- eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, &d_equalityEngine);
+ eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, d_equalityEngine);
for (; !eqc_i.isFinished(); ++eqc_i) {
Node n = *eqc_i;
if (n.getKind() == kind::SELECT && termSet.find(n) != termSet.end()) {
// Find all terms equivalent to n[0] and get corresponding read terms
- Node array_eqc = d_equalityEngine.getRepresentative(n[0]);
- eq::EqClassIterator array_eqc_i = eq::EqClassIterator(array_eqc, &d_equalityEngine);
+ Node array_eqc = d_equalityEngine->getRepresentative(n[0]);
+ eq::EqClassIterator array_eqc_i =
+ eq::EqClassIterator(array_eqc, d_equalityEngine);
for (; !array_eqc_i.isFinished(); ++array_eqc_i) {
Node arr = *array_eqc_i;
- if (arr.getKind() == kind::STORE &&
- termSet.find(arr) != termSet.end() &&
- !d_equalityEngine.areEqual(arr[1],n[1])) {
+ if (arr.getKind() == kind::STORE
+ && termSet.find(arr) != termSet.end()
+ && !d_equalityEngine->areEqual(arr[1], n[1]))
+ {
Node r = nm->mkNode(kind::SELECT, arr, n[1]);
- if (termSet.find(r) == termSet.end() && d_equalityEngine.hasTerm(r)) {
+ if (termSet.find(r) == termSet.end()
+ && d_equalityEngine->hasTerm(r))
+ {
Trace("arrays::collectModelInfo") << "TheoryArrays::collectModelInfo, adding RIntro2(a) read: " << r << endl;
termSet.insert(r);
changed = true;
}
r = nm->mkNode(kind::SELECT, arr[0], n[1]);
- if (termSet.find(r) == termSet.end() && d_equalityEngine.hasTerm(r)) {
+ if (termSet.find(r) == termSet.end()
+ && d_equalityEngine->hasTerm(r))
+ {
Trace("arrays::collectModelInfo") << "TheoryArrays::collectModelInfo, adding RIntro2(b) read: " << r << endl;
termSet.insert(r);
changed = true;
for(; it < instores->size(); ++it) {
TNode instore = (*instores)[it];
Assert(instore.getKind() == kind::STORE);
- if (termSet.find(instore) != termSet.end() &&
- !d_equalityEngine.areEqual(instore[1],n[1])) {
+ if (termSet.find(instore) != termSet.end()
+ && !d_equalityEngine->areEqual(instore[1], n[1]))
+ {
Node r = nm->mkNode(kind::SELECT, instore, n[1]);
- if (termSet.find(r) == termSet.end() && d_equalityEngine.hasTerm(r)) {
+ if (termSet.find(r) == termSet.end()
+ && d_equalityEngine->hasTerm(r))
+ {
Trace("arrays::collectModelInfo") << "TheoryArrays::collectModelInfo, adding RIntro2(c) read: " << r << endl;
termSet.insert(r);
changed = true;
}
r = nm->mkNode(kind::SELECT, instore[0], n[1]);
- if (termSet.find(r) == termSet.end() && d_equalityEngine.hasTerm(r)) {
+ if (termSet.find(r) == termSet.end()
+ && d_equalityEngine->hasTerm(r))
+ {
Trace("arrays::collectModelInfo") << "TheoryArrays::collectModelInfo, adding RIntro2(d) read: " << r << endl;
termSet.insert(r);
changed = true;
} while (changed);
// Send the equality engine information to the model
- if (!m->assertEqualityEngine(&d_equalityEngine, &termSet))
+ if (!m->assertEqualityEngine(d_equalityEngine, &termSet))
{
return false;
}
Node n = *set_it;
// If this term is a select, record that the EC rep of its store parameter is being read from using this term
if (n.getKind() == kind::SELECT) {
- selects[d_equalityEngine.getRepresentative(n[0])].push_back(n);
+ selects[d_equalityEngine->getRepresentative(n[0])].push_back(n);
}
}
// Compute all default values already in use
//if (fullModel) {
for (size_t i=0; i<arrays.size(); ++i) {
- TNode nrep = d_equalityEngine.getRepresentative(arrays[i]);
+ TNode nrep = d_equalityEngine->getRepresentative(arrays[i]);
d_mayEqualEqualityEngine.addTerm(nrep); // add the term in case it isn't there already
TNode mayRep = d_mayEqualEqualityEngine.getRepresentative(nrep);
it = d_defValues.find(mayRep);
// Loop through all array equivalence classes that need a representative computed
for (size_t i=0; i<arrays.size(); ++i) {
TNode n = arrays[i];
- TNode nrep = d_equalityEngine.getRepresentative(n);
+ TNode nrep = d_equalityEngine->getRepresentative(n);
//if (fullModel) {
// Compute default value for this array - there is one default value for every mayEqual equivalence class
}
else {
skolem = (*it).second;
- if (d_equalityEngine.hasTerm(ref) &&
- d_equalityEngine.hasTerm(skolem) &&
- d_equalityEngine.areEqual(ref, skolem)) {
+ if (d_equalityEngine->hasTerm(ref) && d_equalityEngine->hasTerm(skolem)
+ && d_equalityEngine->areEqual(ref, skolem))
+ {
makeEqual = false;
}
}
if (makeEqual) {
Node d = skolem.eqNode(ref);
Debug("arrays-model-based") << "Asserting skolem equality " << d << endl;
- d_equalityEngine.assertEquality(d, true, d_true);
+ d_equalityEngine->assertEquality(d, true, d_true);
Assert(!d_conflict);
d_skolemAssertions.push_back(d);
d_skolemIndex = d_skolemIndex + 1;
if (!assertion.d_isPreregistered)
{
if (atom.getKind() == kind::EQUAL) {
- if (!d_equalityEngine.hasTerm(atom[0])) {
+ if (!d_equalityEngine->hasTerm(atom[0]))
+ {
Assert(atom[0].isConst());
- d_equalityEngine.addTerm(atom[0]);
+ d_equalityEngine->addTerm(atom[0]);
}
- if (!d_equalityEngine.hasTerm(atom[1])) {
+ if (!d_equalityEngine->hasTerm(atom[1]))
+ {
Assert(atom[1].isConst());
- d_equalityEngine.addTerm(atom[1]);
+ d_equalityEngine->addTerm(atom[1]);
}
}
}
// Do the work
switch (fact.getKind()) {
case kind::EQUAL:
- d_equalityEngine.assertEquality(fact, true, fact);
+ d_equalityEngine->assertEquality(fact, true, fact);
break;
case kind::SELECT:
- d_equalityEngine.assertPredicate(fact, true, fact);
+ d_equalityEngine->assertPredicate(fact, true, fact);
break;
case kind::NOT:
if (fact[0].getKind() == kind::SELECT) {
- d_equalityEngine.assertPredicate(fact[0], false, fact);
- } else if (!d_equalityEngine.areDisequal(fact[0][0], fact[0][1], false)) {
+ d_equalityEngine->assertPredicate(fact[0], false, fact);
+ }
+ else if (!d_equalityEngine->areDisequal(fact[0][0], fact[0][1], false))
+ {
// Assert the dis-equality
- d_equalityEngine.assertEquality(fact[0], false, fact);
+ d_equalityEngine->assertEquality(fact[0], false, fact);
// Apply ArrDiseq Rule if diseq is between arrays
if(fact[0][0].getType().isArray() && !d_conflict) {
// when we output the lemma. However, in replay need the lemma to be propagated, and so we
// preregister manually.
if (d_proofsEnabled) {
- if (!d_equalityEngine.hasTerm(ak)) { preRegisterTermInternal(ak); }
- if (!d_equalityEngine.hasTerm(bk)) { preRegisterTermInternal(bk); }
+ if (!d_equalityEngine->hasTerm(ak))
+ {
+ preRegisterTermInternal(ak);
+ }
+ if (!d_equalityEngine->hasTerm(bk))
+ {
+ preRegisterTermInternal(bk);
+ }
}
- if (options::arraysPropagate() > 0 && d_equalityEngine.hasTerm(ak) && d_equalityEngine.hasTerm(bk)) {
+ if (options::arraysPropagate() > 0 && d_equalityEngine->hasTerm(ak)
+ && d_equalityEngine->hasTerm(bk))
+ {
// Propagate witness disequality - might produce a conflict
d_permRef.push_back(lemma);
Debug("pf::array") << "Asserting to the equality engine:" << std::endl
<< "\teq = " << eq << std::endl
<< "\treason = " << fact << std::endl;
- d_equalityEngine.assertEquality(eq, false, fact, d_reasonExt);
+ d_equalityEngine->assertEquality(eq, false, fact, d_reasonExt);
++d_numProp;
}
// Find the bucket for this read.
mayRep = d_mayEqualEqualityEngine.getRepresentative(r[0]);
- iRep = d_equalityEngine.getRepresentative(r[1]);
+ iRep = d_equalityEngine->getRepresentative(r[1]);
std::pair<TNode, TNode> key(mayRep, iRep);
ReadBucketMap::iterator rbm_it = d_readBucketTable.find(key);
if (rbm_it == d_readBucketTable.end())
const TNode& r2 = *ctnl_it;
Assert(r2.getKind() == kind::SELECT);
Assert(mayRep == d_mayEqualEqualityEngine.getRepresentative(r2[0]));
- Assert(iRep == d_equalityEngine.getRepresentative(r2[1]));
- if (d_equalityEngine.areEqual(r, r2)) {
+ Assert(iRep == d_equalityEngine->getRepresentative(r2[1]));
+ if (d_equalityEngine->areEqual(r, r2))
+ {
continue;
}
if (weakEquivGetRepIndex(r[0], r[1]) == weakEquivGetRepIndex(r2[0], r[1])) {
// add lemma: r[1] = r2[1] /\ cond(r[0],r2[0]) => r = r2
vector<TNode> conjunctions;
- Assert(d_equalityEngine.areEqual(r, Rewriter::rewrite(r)));
- Assert(d_equalityEngine.areEqual(r2, Rewriter::rewrite(r2)));
+ Assert(d_equalityEngine->areEqual(r, Rewriter::rewrite(r)));
+ Assert(d_equalityEngine->areEqual(r2, Rewriter::rewrite(r2)));
Node lemma = Rewriter::rewrite(r).eqNode(Rewriter::rewrite(r2)).negate();
d_permRef.push_back(lemma);
conjunctions.push_back(lemma);
if (r[1] != r2[1]) {
- d_equalityEngine.explainEquality(r[1], r2[1], true, conjunctions);
+ d_equalityEngine->explainEquality(r[1], r2[1], true, conjunctions);
}
// TODO: get smaller lemmas by eliminating shared parts of path
weakEquivBuildCond(r[0], r[1], conjunctions);
// Normally, a is its own representative, but it's possible for a to have
// been merged with another array after it got queued up by the equality engine,
// so we take its representative to be safe.
- a = d_equalityEngine.getRepresentative(a);
- Assert(d_equalityEngine.getRepresentative(b) == a);
+ a = d_equalityEngine->getRepresentative(a);
+ Assert(d_equalityEngine->getRepresentative(b) == a);
Trace("arrays-merge") << spaces(getSatContext()->getLevel()) << "Arrays::merge: (" << a << ", " << b << ")\n";
if (options::arraysOptimizeLinear() && !options::arraysWeakEquivalence()) {
TNode b = a[0];
TNode i = a[1];
- TNode brep = d_equalityEngine.getRepresentative(b);
+ TNode brep = d_equalityEngine->getRepresentative(b);
if (!options::arraysOptimizeLinear() || d_infoMap.isNonLinear(brep)) {
const CTNodeList* js = d_infoMap.getIndices(brep);
d_infoMap.getInfo(a)->print();
}
Assert(a.getType().isArray());
- Assert(d_equalityEngine.getRepresentative(a) == a);
+ Assert(d_equalityEngine->getRepresentative(a) == a);
TNode constArr = d_infoMap.getConstArr(a);
if (!constArr.isNull()) {
ArrayStoreAll storeAll = constArr.getConst<ArrayStoreAll>();
Node defValue = storeAll.getValue();
Node selConst = NodeManager::currentNM()->mkNode(kind::SELECT, constArr, i);
- if (!d_equalityEngine.hasTerm(selConst)) {
+ if (!d_equalityEngine->hasTerm(selConst))
+ {
preRegisterTermInternal(selConst);
}
- d_equalityEngine.assertEquality(selConst.eqNode(defValue), true, d_true);
+ d_equalityEngine->assertEquality(selConst.eqNode(defValue), true, d_true);
}
const CTNodeList* stores = d_infoMap.getStores(a);
for( ; it < i_a->size(); ++it) {
TNode i = (*i_a)[it];
Node selConst = NodeManager::currentNM()->mkNode(kind::SELECT, constArr, i);
- if (!d_equalityEngine.hasTerm(selConst)) {
+ if (!d_equalityEngine->hasTerm(selConst))
+ {
preRegisterTermInternal(selConst);
}
}
std::tie(a, b, i, j) = lem;
Assert(a.getType().isArray() && b.getType().isArray());
- if (d_equalityEngine.areEqual(a,b) ||
- d_equalityEngine.areEqual(i,j)) {
+ if (d_equalityEngine->areEqual(a, b) || d_equalityEngine->areEqual(i, j))
+ {
return;
}
Node bj = nm->mkNode(kind::SELECT, b, j);
// Try to avoid introducing new read terms: track whether these already exist
- bool ajExists = d_equalityEngine.hasTerm(aj);
- bool bjExists = d_equalityEngine.hasTerm(bj);
+ bool ajExists = d_equalityEngine->hasTerm(aj);
+ bool bjExists = d_equalityEngine->hasTerm(bj);
bool bothExist = ajExists && bjExists;
// If propagating, check propagations
int prop = options::arraysPropagate();
if (prop > 0) {
- if (d_equalityEngine.areDisequal(i,j,true) && (bothExist || prop > 1)) {
+ if (d_equalityEngine->areDisequal(i, j, true) && (bothExist || prop > 1))
+ {
Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::queueRowLemma: propagating aj = bj ("<<aj<<", "<<bj<<")\n";
Node aj_eq_bj = aj.eqNode(bj);
Node reason =
if (!bjExists) {
preRegisterTermInternal(bj);
}
- d_equalityEngine.assertEquality(aj_eq_bj, true, reason, d_reasonRow);
+ d_equalityEngine->assertEquality(aj_eq_bj, true, reason, d_reasonRow);
++d_numProp;
return;
}
- if (bothExist && d_equalityEngine.areDisequal(aj,bj,true)) {
+ if (bothExist && d_equalityEngine->areDisequal(aj, bj, true))
+ {
Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::queueRowLemma: propagating i = j ("<<i<<", "<<j<<")\n";
Node reason =
(aj.isConst() && bj.isConst()) ? d_true : aj.eqNode(bj).notNode();
Node i_eq_j = i.eqNode(j);
d_permRef.push_back(reason);
- d_equalityEngine.assertEquality(i_eq_j, true, reason, d_reasonRow);
+ d_equalityEngine->assertEquality(i_eq_j, true, reason, d_reasonRow);
++d_numProp;
return;
}
std::tie(a, b, i, j) = lem;
Assert(a.getType().isArray() && b.getType().isArray());
- if (d_equalityEngine.areEqual(a,b) ||
- d_equalityEngine.areEqual(i,j)) {
+ if (d_equalityEngine->areEqual(a, b) || d_equalityEngine->areEqual(i, j))
+ {
return;
}
Node bj = nm->mkNode(kind::SELECT, b, j);
// Try to avoid introducing new read terms: track whether these already exist
- bool ajExists = d_equalityEngine.hasTerm(aj);
- bool bjExists = d_equalityEngine.hasTerm(bj);
+ bool ajExists = d_equalityEngine->hasTerm(aj);
+ bool bjExists = d_equalityEngine->hasTerm(bj);
bool bothExist = ajExists && bjExists;
// If propagating, check propagations
// If equivalent lemma already exists, don't enqueue this one
if (d_useArrTable) {
Node tableEntry = NodeManager::currentNM()->mkNode(kind::ARR_TABLE_FUN, a, b, i, j);
- if (d_equalityEngine.getSize(tableEntry) != 1) {
+ if (d_equalityEngine->getSize(tableEntry) != 1)
+ {
return;
}
}
// Prefer equality between indexes so as not to introduce new read terms
- if (options::arraysEagerIndexSplitting() && !bothExist && !d_equalityEngine.areDisequal(i,j, false)) {
+ if (options::arraysEagerIndexSplitting() && !bothExist
+ && !d_equalityEngine->areDisequal(i, j, false))
+ {
Node i_eq_j;
if (!d_proofsEnabled) {
i_eq_j = d_valuation.ensureLiteral(i.eqNode(j)); // TODO: think about this
if (!ajExists) {
preRegisterTermInternal(aj);
}
- if (!d_equalityEngine.hasTerm(aj2)) {
+ if (!d_equalityEngine->hasTerm(aj2))
+ {
preRegisterTermInternal(aj2);
}
- d_equalityEngine.assertEquality(aj.eqNode(aj2), true, d_true);
+ d_equalityEngine->assertEquality(aj.eqNode(aj2), true, d_true);
}
Node bj2 = Rewriter::rewrite(bj);
if (bj != bj2) {
if (!bjExists) {
preRegisterTermInternal(bj);
}
- if (!d_equalityEngine.hasTerm(bj2)) {
+ if (!d_equalityEngine->hasTerm(bj2))
+ {
preRegisterTermInternal(bj2);
}
- d_equalityEngine.assertEquality(bj.eqNode(bj2), true, d_true);
+ d_equalityEngine->assertEquality(bj.eqNode(bj2), true, d_true);
}
if (aj2 == bj2) {
return;
Node eq1 = aj2.eqNode(bj2);
Node eq1_r = Rewriter::rewrite(eq1);
if (eq1_r == d_true) {
- if (!d_equalityEngine.hasTerm(aj2)) {
+ if (!d_equalityEngine->hasTerm(aj2))
+ {
preRegisterTermInternal(aj2);
}
- if (!d_equalityEngine.hasTerm(bj2)) {
+ if (!d_equalityEngine->hasTerm(bj2))
+ {
preRegisterTermInternal(bj2);
}
- d_equalityEngine.assertEquality(eq1, true, d_true);
+ d_equalityEngine->assertEquality(eq1, true, d_true);
return;
}
Node eq2 = i.eqNode(j);
Node eq2_r = Rewriter::rewrite(eq2);
if (eq2_r == d_true) {
- d_equalityEngine.assertEquality(eq2, true, d_true);
+ d_equalityEngine->assertEquality(eq2, true, d_true);
return;
}
NodeManager* nm = NodeManager::currentNM();
Node aj = nm->mkNode(kind::SELECT, a, j);
Node bj = nm->mkNode(kind::SELECT, b, j);
- bool ajExists = d_equalityEngine.hasTerm(aj);
- bool bjExists = d_equalityEngine.hasTerm(bj);
+ bool ajExists = d_equalityEngine->hasTerm(aj);
+ bool bjExists = d_equalityEngine->hasTerm(bj);
// Check for redundant lemma
// TODO: more checks possible (i.e. check d_RowAlreadyAdded in context)
- if (!d_equalityEngine.hasTerm(i) || !d_equalityEngine.hasTerm(j) || d_equalityEngine.areEqual(i,j) ||
- !d_equalityEngine.hasTerm(a) || !d_equalityEngine.hasTerm(b) || d_equalityEngine.areEqual(a,b) ||
- (ajExists && bjExists && d_equalityEngine.areEqual(aj,bj))) {
+ if (!d_equalityEngine->hasTerm(i) || !d_equalityEngine->hasTerm(j)
+ || d_equalityEngine->areEqual(i, j) || !d_equalityEngine->hasTerm(a)
+ || !d_equalityEngine->hasTerm(b) || d_equalityEngine->areEqual(a, b)
+ || (ajExists && bjExists && d_equalityEngine->areEqual(aj, bj)))
+ {
continue;
}
if (!ajExists) {
preRegisterTermInternal(aj);
}
- if (!d_equalityEngine.hasTerm(aj2)) {
+ if (!d_equalityEngine->hasTerm(aj2))
+ {
preRegisterTermInternal(aj2);
}
- d_equalityEngine.assertEquality(aj.eqNode(aj2), true, d_true);
+ d_equalityEngine->assertEquality(aj.eqNode(aj2), true, d_true);
}
Node bj2 = Rewriter::rewrite(bj);
if (bj != bj2) {
if (!bjExists) {
preRegisterTermInternal(bj);
}
- if (!d_equalityEngine.hasTerm(bj2)) {
+ if (!d_equalityEngine->hasTerm(bj2))
+ {
preRegisterTermInternal(bj2);
}
- d_equalityEngine.assertEquality(bj.eqNode(bj2), true, d_true);
-
+ d_equalityEngine->assertEquality(bj.eqNode(bj2), true, d_true);
}
if (aj2 == bj2) {
continue;
Node eq1 = aj2.eqNode(bj2);
Node eq1_r = Rewriter::rewrite(eq1);
if (eq1_r == d_true) {
- if (!d_equalityEngine.hasTerm(aj2)) {
+ if (!d_equalityEngine->hasTerm(aj2))
+ {
preRegisterTermInternal(aj2);
}
- if (!d_equalityEngine.hasTerm(bj2)) {
+ if (!d_equalityEngine->hasTerm(bj2))
+ {
preRegisterTermInternal(bj2);
}
- d_equalityEngine.assertEquality(eq1, true, d_true);
+ d_equalityEngine->assertEquality(eq1, true, d_true);
continue;
}
Node eq2 = i.eqNode(j);
Node eq2_r = Rewriter::rewrite(eq2);
if (eq2_r == d_true) {
- d_equalityEngine.assertEquality(eq2, true, d_true);
+ d_equalityEngine->assertEquality(eq2, true, d_true);
continue;
}
std::string name = "");
~TheoryArrays();
- TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
-
- void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
+ //--------------------------------- initialization
+ /** get the official theory rewriter of this theory */
+ TheoryRewriter* getTheoryRewriter() override;
+ /**
+ * Returns true if we need an equality engine. If so, we initialize the
+ * information regarding how it should be setup. For details, see the
+ * documentation in Theory::needsEqualityEngine.
+ */
+ bool needsEqualityEngine(EeSetupInfo& esi) override;
+ /** finish initialization */
+ void finishInit() override;
+ //--------------------------------- end initialization
std::string identify() const override { return std::string("TheoryArrays"); }
/** The notify class for d_equalityEngine */
NotifyClass d_notify;
- /** Equaltity engine */
- eq::EqualityEngine d_equalityEngine;
-
/** Are we in conflict? */
context::CDO<bool> d_conflict;
int d_topLevel;
/** An equality-engine callback for proof reconstruction */
- ArrayProofReconstruction d_proofReconstruction;
+ std::unique_ptr<ArrayProofReconstruction> d_proofReconstruction;
/**
* The decision strategy for the theory of arrays, which calls the
*/
Node getNextDecisionRequest();
- public:
- eq::EqualityEngine* getEqualityEngine() override { return &d_equalityEngine; }
-
};/* class TheoryArrays */
}/* CVC4::theory::arrays namespace */
CoreSolver::CoreSolver(context::Context* c, TheoryBV* bv, ExtTheory* extt)
: SubtheorySolver(c, bv),
d_notify(*this),
- d_equalityEngine(d_notify, c, "theory::bv::ee", true),
d_slicer(new Slicer()),
d_isComplete(c, true),
d_lemmaThreshold(16),
d_useSlicer(false),
d_preregisterCalled(false),
d_checkCalled(false),
+ d_bv(bv),
d_extTheory(extt),
d_reasons(c)
{
- // The kinds we are treating as function application in congruence
- d_equalityEngine.addFunctionKind(kind::BITVECTOR_CONCAT, true);
- // d_equalityEngine.addFunctionKind(kind::BITVECTOR_AND);
- // d_equalityEngine.addFunctionKind(kind::BITVECTOR_OR);
- // d_equalityEngine.addFunctionKind(kind::BITVECTOR_XOR);
- // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOT);
- // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NAND);
- // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOR);
- // d_equalityEngine.addFunctionKind(kind::BITVECTOR_XNOR);
- // d_equalityEngine.addFunctionKind(kind::BITVECTOR_COMP);
- d_equalityEngine.addFunctionKind(kind::BITVECTOR_MULT, true);
- d_equalityEngine.addFunctionKind(kind::BITVECTOR_PLUS, true);
- d_equalityEngine.addFunctionKind(kind::BITVECTOR_EXTRACT, true);
- // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SUB);
- // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NEG);
- // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UDIV);
- // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UREM);
- // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SDIV);
- // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SREM);
- // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SMOD);
- // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SHL);
- // d_equalityEngine.addFunctionKind(kind::BITVECTOR_LSHR);
- // d_equalityEngine.addFunctionKind(kind::BITVECTOR_ASHR);
- // d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULT);
- // d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULE);
- // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGT);
- // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGE);
- // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLT);
- // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLE);
- // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGT);
- // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGE);
- d_equalityEngine.addFunctionKind(kind::BITVECTOR_TO_NAT);
- d_equalityEngine.addFunctionKind(kind::INT_TO_BITVECTOR);
}
CoreSolver::~CoreSolver() {}
-void CoreSolver::setMasterEqualityEngine(eq::EqualityEngine* eq) {
- d_equalityEngine.setMasterEqualityEngine(eq);
+bool CoreSolver::needsEqualityEngine(EeSetupInfo& esi)
+{
+ esi.d_notify = &d_notify;
+ esi.d_name = "theory::bv::ee";
+ return true;
+}
+
+void CoreSolver::finishInit()
+{
+ // use the parent's equality engine, which may be the one we allocated above
+ d_equalityEngine = d_bv->getEqualityEngine();
+
+ // The kinds we are treating as function application in congruence
+ d_equalityEngine->addFunctionKind(kind::BITVECTOR_CONCAT, true);
+ // d_equalityEngine->addFunctionKind(kind::BITVECTOR_AND);
+ // d_equalityEngine->addFunctionKind(kind::BITVECTOR_OR);
+ // d_equalityEngine->addFunctionKind(kind::BITVECTOR_XOR);
+ // d_equalityEngine->addFunctionKind(kind::BITVECTOR_NOT);
+ // d_equalityEngine->addFunctionKind(kind::BITVECTOR_NAND);
+ // d_equalityEngine->addFunctionKind(kind::BITVECTOR_NOR);
+ // d_equalityEngine->addFunctionKind(kind::BITVECTOR_XNOR);
+ // d_equalityEngine->addFunctionKind(kind::BITVECTOR_COMP);
+ d_equalityEngine->addFunctionKind(kind::BITVECTOR_MULT, true);
+ d_equalityEngine->addFunctionKind(kind::BITVECTOR_PLUS, true);
+ d_equalityEngine->addFunctionKind(kind::BITVECTOR_EXTRACT, true);
+ // d_equalityEngine->addFunctionKind(kind::BITVECTOR_SUB);
+ // d_equalityEngine->addFunctionKind(kind::BITVECTOR_NEG);
+ // d_equalityEngine->addFunctionKind(kind::BITVECTOR_UDIV);
+ // d_equalityEngine->addFunctionKind(kind::BITVECTOR_UREM);
+ // d_equalityEngine->addFunctionKind(kind::BITVECTOR_SDIV);
+ // d_equalityEngine->addFunctionKind(kind::BITVECTOR_SREM);
+ // d_equalityEngine->addFunctionKind(kind::BITVECTOR_SMOD);
+ // d_equalityEngine->addFunctionKind(kind::BITVECTOR_SHL);
+ // d_equalityEngine->addFunctionKind(kind::BITVECTOR_LSHR);
+ // d_equalityEngine->addFunctionKind(kind::BITVECTOR_ASHR);
+ // d_equalityEngine->addFunctionKind(kind::BITVECTOR_ULT);
+ // d_equalityEngine->addFunctionKind(kind::BITVECTOR_ULE);
+ // d_equalityEngine->addFunctionKind(kind::BITVECTOR_UGT);
+ // d_equalityEngine->addFunctionKind(kind::BITVECTOR_UGE);
+ // d_equalityEngine->addFunctionKind(kind::BITVECTOR_SLT);
+ // d_equalityEngine->addFunctionKind(kind::BITVECTOR_SLE);
+ // d_equalityEngine->addFunctionKind(kind::BITVECTOR_SGT);
+ // d_equalityEngine->addFunctionKind(kind::BITVECTOR_SGE);
+ d_equalityEngine->addFunctionKind(kind::BITVECTOR_TO_NAT);
+ d_equalityEngine->addFunctionKind(kind::INT_TO_BITVECTOR);
}
void CoreSolver::enableSlicer() {
void CoreSolver::preRegister(TNode node) {
d_preregisterCalled = true;
if (node.getKind() == kind::EQUAL) {
- d_equalityEngine.addTriggerEquality(node);
- if (d_useSlicer) {
- d_slicer->processEquality(node);
- AlwaysAssert(!d_checkCalled);
+ d_equalityEngine->addTriggerEquality(node);
+ if (d_useSlicer)
+ {
+ d_slicer->processEquality(node);
+ AlwaysAssert(!d_checkCalled);
}
} else {
- d_equalityEngine.addTerm(node);
+ d_equalityEngine->addTerm(node);
// Register with the extended theory, for context-dependent simplification.
// Notice we do this for registered terms but not internally generated
// equivalence classes. The two should roughly cooincide. Since ExtTheory is
bool polarity = literal.getKind() != kind::NOT;
TNode atom = polarity ? literal : literal[0];
if (atom.getKind() == kind::EQUAL) {
- d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions);
+ d_equalityEngine->explainEquality(atom[0], atom[1], polarity, assumptions);
} else {
- d_equalityEngine.explainPredicate(atom, polarity, assumptions);
+ d_equalityEngine->explainPredicate(atom, polarity, assumptions);
}
}
TNodeSet constants;
TNodeSet constants_in_eq_engine;
// collect constants in equality engine
- eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(&d_equalityEngine);
+ eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(d_equalityEngine);
while (!eqcs_i.isFinished())
{
TNode repr = *eqcs_i;
if (repr.getKind() == kind::CONST_BITVECTOR)
{
// must check if it's just the constant
- eq::EqClassIterator it(repr, &d_equalityEngine);
+ eq::EqClassIterator it(repr, d_equalityEngine);
if (!(++it).isFinished() || true)
{
constants.insert(repr);
// build repr to value map
- eqcs_i = eq::EqClassesIterator(&d_equalityEngine);
+ eqcs_i = eq::EqClassesIterator(d_equalityEngine);
while (!eqcs_i.isFinished())
{
TNode repr = *eqcs_i;
if (predicate.getKind() == kind::EQUAL) {
if (negated) {
// dis-equality
- d_equalityEngine.assertEquality(predicate, false, reason);
+ d_equalityEngine->assertEquality(predicate, false, reason);
} else {
// equality
- d_equalityEngine.assertEquality(predicate, true, reason);
+ d_equalityEngine->assertEquality(predicate, true, reason);
}
} else {
// Adding predicate if the congruence over it is turned on
- if (d_equalityEngine.isFunctionKind(predicate.getKind())) {
- d_equalityEngine.assertPredicate(predicate, !negated, reason);
+ if (d_equalityEngine->isFunctionKind(predicate.getKind()))
+ {
+ d_equalityEngine->assertPredicate(predicate, !negated, reason);
}
}
}
void CoreSolver::conflict(TNode a, TNode b) {
std::vector<TNode> assumptions;
- d_equalityEngine.explainEquality(a, b, true, assumptions);
+ d_equalityEngine->explainEquality(a, b, true, assumptions);
Node conflict = flattenAnd(assumptions);
d_bv->setConflict(conflict);
}
}
set<Node> termSet;
d_bv->computeRelevantTerms(termSet);
- if (!m->assertEqualityEngine(&d_equalityEngine, &termSet))
+ if (!m->assertEqualityEngine(d_equalityEngine, &termSet))
{
return false;
}
Node CoreSolver::getModelValue(TNode var) {
Debug("bitvector-model") << "CoreSolver::getModelValue (" << var <<")";
Assert(isComplete());
- TNode repr = d_equalityEngine.getRepresentative(var);
+ TNode repr = d_equalityEngine->getRepresentative(var);
Node result = Node();
if (repr.getKind() == kind::CONST_BITVECTOR) {
result = repr;
return result;
}
+void CoreSolver::addSharedTerm(TNode t)
+{
+ d_equalityEngine->addTriggerTerm(t, THEORY_BV);
+}
+
+EqualityStatus CoreSolver::getEqualityStatus(TNode a, TNode b)
+{
+ if (d_equalityEngine->areEqual(a, b))
+ {
+ // The terms are implied to be equal
+ return EQUALITY_TRUE;
+ }
+ if (d_equalityEngine->areDisequal(a, b, false))
+ {
+ // The terms are implied to be dis-equal
+ return EQUALITY_FALSE;
+ }
+ return EQUALITY_UNKNOWN;
+}
+
+bool CoreSolver::hasTerm(TNode node) const
+{
+ return d_equalityEngine->hasTerm(node);
+}
+void CoreSolver::addTermToEqualityEngine(TNode node)
+{
+ d_equalityEngine->addTerm(node);
+}
+
CoreSolver::Statistics::Statistics()
: d_numCallstoCheck("theory::bv::CoreSolver::NumCallsToCheck", 0)
, d_slicerEnabled("theory::bv::CoreSolver::SlicerEnabled", false)
/** The notify class for d_equalityEngine */
NotifyClass d_notify;
- /** Equality engine */
- eq::EqualityEngine d_equalityEngine;
-
/** Store a propagation to the bv solver */
bool storePropagation(TNode literal);
bool d_preregisterCalled;
bool d_checkCalled;
+ /** Pointer to the parent theory solver that owns this */
+ TheoryBV* d_bv;
+ /** Pointer to the equality engine of the parent */
+ eq::EqualityEngine* d_equalityEngine;
/** Pointer to the extended theory module. */
ExtTheory* d_extTheory;
Node getBaseDecomposition(TNode a);
bool isCompleteForTerm(TNode term, TNodeBoolMap& seen);
Statistics d_statistics;
-public:
- CoreSolver(context::Context* c, TheoryBV* bv, ExtTheory* extt);
- ~CoreSolver();
- bool isComplete() override { return d_isComplete; }
- void setMasterEqualityEngine(eq::EqualityEngine* eq);
- void preRegister(TNode node) override;
- bool check(Theory::Effort e) override;
- void explain(TNode literal, std::vector<TNode>& assumptions) override;
- bool collectModelInfo(TheoryModel* m, bool fullModel) override;
- Node getModelValue(TNode var) override;
- void addSharedTerm(TNode t) override
- {
- d_equalityEngine.addTriggerTerm(t, THEORY_BV);
- }
- EqualityStatus getEqualityStatus(TNode a, TNode b) override
- {
- if (d_equalityEngine.areEqual(a, b)) {
- // The terms are implied to be equal
- return EQUALITY_TRUE;
- }
- if (d_equalityEngine.areDisequal(a, b, false)) {
- // The terms are implied to be dis-equal
- return EQUALITY_FALSE;
- }
- return EQUALITY_UNKNOWN;
- }
- bool hasTerm(TNode node) const { return d_equalityEngine.hasTerm(node); }
- void addTermToEqualityEngine(TNode node) { d_equalityEngine.addTerm(node); }
+
+ public:
+ CoreSolver(context::Context* c, TheoryBV* bv, ExtTheory* extt);
+ ~CoreSolver();
+ bool needsEqualityEngine(EeSetupInfo& esi);
+ void finishInit();
+ bool isComplete() override { return d_isComplete; }
+ void preRegister(TNode node) override;
+ bool check(Theory::Effort e) override;
+ void explain(TNode literal, std::vector<TNode>& assumptions) override;
+ bool collectModelInfo(TheoryModel* m, bool fullModel) override;
+ Node getModelValue(TNode var) override;
+ void addSharedTerm(TNode t) override;
+ EqualityStatus getEqualityStatus(TNode a, TNode b) override;
+ bool hasTerm(TNode node) const;
+ void addTermToEqualityEngine(TNode node);
void enableSlicer();
- eq::EqualityEngine * getEqualityEngine() { return &d_equalityEngine; }
};
TheoryBV::~TheoryBV() {}
-void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) {
- if (options::bitblastMode() == options::BitblastMode::EAGER)
+TheoryRewriter* TheoryBV::getTheoryRewriter() { return &d_rewriter; }
+
+bool TheoryBV::needsEqualityEngine(EeSetupInfo& esi)
+{
+ CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
+ if (core)
{
- return;
+ return core->needsEqualityEngine(esi);
}
- if (options::bitvectorEqualitySolver()) {
- dynamic_cast<CoreSolver*>(d_subtheoryMap[SUB_CORE])->setMasterEqualityEngine(eq);
+ // otherwise we don't use an equality engine
+ return false;
+}
+
+void TheoryBV::finishInit()
+{
+ // these kinds are semi-evaluated in getModelValue (applications of this
+ // kind are treated as variables)
+ d_valuation.setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UDIV);
+ d_valuation.setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UREM);
+
+ CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
+ if (core)
+ {
+ // must finish initialization in the core solver
+ core->finishInit();
}
}
Unreachable();
}
-void TheoryBV::finishInit()
-{
- // these kinds are semi-evaluated in getModelValue (applications of this
- // kind are treated as variables)
- TheoryModel* tm = d_valuation.getModel();
- Assert(tm != nullptr);
- tm->setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UDIV);
- tm->setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UREM);
-}
-
TrustNode TheoryBV::expandDefinition(Node node)
{
Debug("bitvector-expandDefinition") << "TheoryBV::expandDefinition(" << node << ")" << std::endl;
}
}
-
-eq::EqualityEngine * TheoryBV::getEqualityEngine() {
- CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
- if( core ){
- return core->getEqualityEngine();
- }else{
- return NULL;
- }
-}
-
bool TheoryBV::getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp ) {
eq::EqualityEngine * ee = getEqualityEngine();
if( ee ){
~TheoryBV();
- TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
-
- void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
-
+ //--------------------------------- initialization
+ /** get the official theory rewriter of this theory */
+ TheoryRewriter* getTheoryRewriter() override;
+ /**
+ * Returns true if we need an equality engine. If so, we initialize the
+ * information regarding how it should be setup. For details, see the
+ * documentation in Theory::needsEqualityEngine.
+ */
+ bool needsEqualityEngine(EeSetupInfo& esi) override;
+ /** finish initialization */
void finishInit() override;
+ //--------------------------------- end initialization
TrustNode expandDefinition(Node node) override;
std::string identify() const override { return std::string("TheoryBV"); }
- /** equality engine */
- eq::EqualityEngine* getEqualityEngine() override;
bool getCurrentSubstitution(int effort,
std::vector<Node>& vars,
std::vector<Node>& subs,
d_infer_exp(c),
d_term_sk(u),
d_notify(*this),
- d_equalityEngine(d_notify, c, "theory::datatypes", true),
d_labels(c),
d_selector_apps(c),
d_conflict(c, false),
d_lemmas_produced_c(u),
d_sygusExtension(nullptr)
{
- // The kinds we are treating as function application in congruence
- d_equalityEngine.addFunctionKind(kind::APPLY_CONSTRUCTOR);
- d_equalityEngine.addFunctionKind(kind::APPLY_SELECTOR_TOTAL);
- //d_equalityEngine.addFunctionKind(kind::DT_SIZE);
- //d_equalityEngine.addFunctionKind(kind::DT_HEIGHT_BOUND);
- d_equalityEngine.addFunctionKind(kind::APPLY_TESTER);
- //d_equalityEngine.addFunctionKind(kind::APPLY_UF);
d_true = NodeManager::currentNM()->mkConst( true );
d_zero = NodeManager::currentNM()->mkConst( Rational(0) );
}
}
-void TheoryDatatypes::setMasterEqualityEngine(eq::EqualityEngine* eq) {
- d_equalityEngine.setMasterEqualityEngine(eq);
+TheoryRewriter* TheoryDatatypes::getTheoryRewriter() { return &d_rewriter; }
+
+bool TheoryDatatypes::needsEqualityEngine(EeSetupInfo& esi)
+{
+ esi.d_notify = &d_notify;
+ esi.d_name = "theory::datatypes::ee";
+ return true;
+}
+
+void TheoryDatatypes::finishInit()
+{
+ Assert(d_equalityEngine != nullptr);
+ // The kinds we are treating as function application in congruence
+ d_equalityEngine->addFunctionKind(kind::APPLY_CONSTRUCTOR);
+ d_equalityEngine->addFunctionKind(kind::APPLY_SELECTOR_TOTAL);
+ d_equalityEngine->addFunctionKind(kind::APPLY_TESTER);
+ // We could but don't do congruence for DT_SIZE and DT_HEIGHT_BOUND here.
+ // It also could make sense in practice to do congruence for APPLY_UF, but
+ // this is not done.
+ if (getQuantifiersEngine() && options::sygus())
+ {
+ d_sygusExtension.reset(
+ new SygusExtension(this, getQuantifiersEngine(), getSatContext()));
+ // do congruence on evaluation functions
+ d_equalityEngine->addFunctionKind(kind::DT_SYGUS_EVAL);
+ }
}
TheoryDatatypes::EqcInfo* TheoryDatatypes::getOrMakeEqcInfo( TNode n, bool doMake ){
do {
d_addedFact = false;
std::map< TypeNode, Node > rec_singletons;
- eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
+ eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(d_equalityEngine);
while( !eqcs_i.isFinished() ){
Node n = (*eqcs_i);
//TODO : avoid irrelevant (pre-registered but not asserted) terms here?
bool polarity = fact.getKind() != kind::NOT;
TNode atom = polarity ? fact : fact[0];
if (atom.getKind() == kind::EQUAL) {
- d_equalityEngine.assertEquality( atom, polarity, exp );
+ d_equalityEngine->assertEquality(atom, polarity, exp);
}else{
- d_equalityEngine.assertPredicate( atom, polarity, exp );
+ d_equalityEngine->assertPredicate(atom, polarity, exp);
}
doPendingMerges();
// could be sygus-specific
switch (n.getKind()) {
case kind::EQUAL:
// Add the trigger for equality
- d_equalityEngine.addTriggerEquality(n);
+ d_equalityEngine->addTriggerEquality(n);
break;
case kind::APPLY_TESTER:
// Get triggered for both equal and dis-equal
- d_equalityEngine.addTriggerPredicate(n);
+ d_equalityEngine->addTriggerPredicate(n);
break;
default:
// Function applications/predicates
- d_equalityEngine.addTerm(n);
+ d_equalityEngine->addTerm(n);
if (d_sygusExtension)
{
std::vector< Node > lemmas;
d_sygusExtension->preRegisterTerm(n, lemmas);
doSendLemmas( lemmas );
}
- //d_equalityEngine.addTriggerTerm(n, THEORY_DATATYPES);
+ // d_equalityEngine->addTriggerTerm(n, THEORY_DATATYPES);
break;
}
flushPendingFacts();
}
-void TheoryDatatypes::finishInit() {
- if (getQuantifiersEngine() && options::sygus())
- {
- d_sygusExtension.reset(
- new SygusExtension(this, getQuantifiersEngine(), getSatContext()));
- // do congruence on evaluation functions
- d_equalityEngine.addFunctionKind(kind::DT_SYGUS_EVAL);
- }
-}
-
TrustNode TheoryDatatypes::expandDefinition(Node n)
{
NodeManager* nm = NodeManager::currentNM();
void TheoryDatatypes::addSharedTerm(TNode t) {
Debug("datatypes") << "TheoryDatatypes::addSharedTerm(): "
<< t << " " << t.getType().isBoolean() << endl;
- d_equalityEngine.addTriggerTerm(t, THEORY_DATATYPES);
+ d_equalityEngine->addTriggerTerm(t, THEORY_DATATYPES);
Debug("datatypes") << "TheoryDatatypes::addSharedTerm() finished" << std::endl;
}
void TheoryDatatypes::explainEquality( TNode a, TNode b, bool polarity, std::vector<TNode>& assumptions ) {
if( a!=b ){
std::vector<TNode> tassumptions;
- d_equalityEngine.explainEquality(a, b, polarity, tassumptions);
+ d_equalityEngine->explainEquality(a, b, polarity, tassumptions);
addAssumptions( assumptions, tassumptions );
}
}
void TheoryDatatypes::explainPredicate( TNode p, bool polarity, std::vector<TNode>& assumptions ) {
std::vector<TNode> tassumptions;
- d_equalityEngine.explainPredicate(p, polarity, tassumptions);
+ d_equalityEngine->explainPredicate(p, polarity, tassumptions);
addAssumptions( assumptions, tassumptions );
}
}
EqualityStatus TheoryDatatypes::getEqualityStatus(TNode a, TNode b){
- Assert(d_equalityEngine.hasTerm(a) && d_equalityEngine.hasTerm(b));
- if (d_equalityEngine.areEqual(a, b)) {
+ Assert(d_equalityEngine->hasTerm(a) && d_equalityEngine->hasTerm(b));
+ if (d_equalityEngine->areEqual(a, b))
+ {
// The terms are implied to be equal
return EQUALITY_TRUE;
}
- if (d_equalityEngine.areDisequal(a, b, false)) {
+ if (d_equalityEngine->areDisequal(a, b, false))
+ {
// The terms are implied to be dis-equal
return EQUALITY_FALSE;
}
for (unsigned k = 0; k < f1.getNumChildren(); ++ k) {
TNode x = f1[k];
TNode y = f2[k];
- Assert(d_equalityEngine.hasTerm(x));
- Assert(d_equalityEngine.hasTerm(y));
+ Assert(d_equalityEngine->hasTerm(x));
+ Assert(d_equalityEngine->hasTerm(y));
Assert(!areDisequal(x, y));
Assert(!areCareDisequal(x, y));
- if( !d_equalityEngine.areEqual( x, y ) ){
+ if (!d_equalityEngine->areEqual(x, y))
+ {
Trace("dt-cg") << "Arg #" << k << " is " << x << " " << y << std::endl;
- if( d_equalityEngine.isTriggerTerm(x, THEORY_DATATYPES) && d_equalityEngine.isTriggerTerm(y, THEORY_DATATYPES) ){
- TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_DATATYPES);
- TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_DATATYPES);
+ if (d_equalityEngine->isTriggerTerm(x, THEORY_DATATYPES)
+ && d_equalityEngine->isTriggerTerm(y, THEORY_DATATYPES))
+ {
+ TNode x_shared = d_equalityEngine->getTriggerTermRepresentative(
+ x, THEORY_DATATYPES);
+ TNode y_shared = d_equalityEngine->getTriggerTermRepresentative(
+ y, THEORY_DATATYPES);
currentPairs.push_back(make_pair(x_shared, y_shared));
}
}
std::map<TNode, TNodeTrie>::iterator it2 = it;
++it2;
for( ; it2 != t1->d_data.end(); ++it2 ){
- if( !d_equalityEngine.areDisequal(it->first, it2->first, false) ){
+ if (!d_equalityEngine->areDisequal(it->first, it2->first, false))
+ {
if( !areCareDisequal(it->first, it2->first) ){
addCarePairs( &it->second, &it2->second, arity, depth+1, n_pairs );
}
{
for (std::pair<const TNode, TNodeTrie>& tt2 : t2->d_data)
{
- if (!d_equalityEngine.areDisequal(tt1.first, tt2.first, false))
+ if (!d_equalityEngine->areDisequal(tt1.first, tt2.first, false))
{
if (!areCareDisequal(tt1.first, tt2.first))
{
unsigned functionTerms = d_functionTerms.size();
for( unsigned i=0; i<functionTerms; i++ ){
TNode f1 = d_functionTerms[i];
- Assert(d_equalityEngine.hasTerm(f1));
+ Assert(d_equalityEngine->hasTerm(f1));
Trace("dt-cg-debug") << "...build for " << f1 << std::endl;
//break into index based on operator, and type of first argument (since some operators are parametric)
Node op = f1.getOperator();
std::vector< TNode > reps;
bool has_trigger_arg = false;
for( unsigned j=0; j<f1.getNumChildren(); j++ ){
- reps.push_back( d_equalityEngine.getRepresentative( f1[j] ) );
- if( d_equalityEngine.isTriggerTerm( f1[j], THEORY_DATATYPES ) ){
+ reps.push_back(d_equalityEngine->getRepresentative(f1[j]));
+ if (d_equalityEngine->isTriggerTerm(f1[j], THEORY_DATATYPES))
+ {
has_trigger_arg = true;
}
}
bool TheoryDatatypes::collectModelInfo(TheoryModel* m)
{
- Trace("dt-cmi") << "Datatypes : Collect model info " << d_equalityEngine.consistent() << std::endl;
+ Trace("dt-cmi") << "Datatypes : Collect model info "
+ << d_equalityEngine->consistent() << std::endl;
Trace("dt-model") << std::endl;
printModelDebug( "dt-model" );
Trace("dt-model") << std::endl;
getRelevantTerms(termSet);
//combine the equality engine
- if (!m->assertEqualityEngine(&d_equalityEngine, &termSet))
+ if (!m->assertEqualityEngine(d_equalityEngine, &termSet))
{
return false;
}
//get all constructors
- eq::EqClassesIterator eqccs_i = eq::EqClassesIterator( &d_equalityEngine );
+ eq::EqClassesIterator eqccs_i = eq::EqClassesIterator(d_equalityEngine);
std::vector< Node > cons;
std::vector< Node > nodes;
std::map< Node, Node > eqc_cons;
bool addCons = false;
TypeNode tt = eqc.getType();
const DType& dt = tt.getDType();
- if( !d_equalityEngine.hasTerm( eqc ) ){
+ if (!d_equalityEngine->hasTerm(eqc))
+ {
Assert(false);
}else{
Trace("dt-cmi") << "NOTICE : Datatypes: no constructor in equivalence class " << eqc << std::endl;
bool cfinite = dt[ i ].isInterpretedFinite( tt );
if( pcons[i] && (r==1)==cfinite ){
neqc = utils::getInstCons(eqc, dt, i);
- //for( unsigned j=0; j<neqc.getNumChildren(); j++ ){
- // //if( sels[i].find( j )==sels[i].end() && neqc[j].getType().isDatatype() ){
- // if( !d_equalityEngine.hasTerm( neqc[j] ) && neqc[j].getType().isDatatype() ){
- // nodes.push_back( neqc[j] );
- // }
- //}
break;
}
}
//Assert( n_ic==Rewriter::rewrite( n_ic ) );
n_ic = Rewriter::rewrite( n_ic );
collectTerms( n_ic );
- d_equalityEngine.addTerm(n_ic);
+ d_equalityEngine->addTerm(n_ic);
Debug("dt-enum") << "Made instantiate cons " << n_ic << std::endl;
}
d_inst_map[n][index] = n_ic;
void TheoryDatatypes::checkCycles() {
Trace("datatypes-cycle-check") << "Check acyclicity" << std::endl;
std::vector< Node > cdt_eqc;
- eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
+ eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(d_equalityEngine);
while( !eqcs_i.isFinished() ){
Node eqc = (*eqcs_i);
TypeNode tn = eqc.getType();
}
}
-bool TheoryDatatypes::hasTerm( TNode a ){
- return d_equalityEngine.hasTerm( a );
-}
+bool TheoryDatatypes::hasTerm(TNode a) { return d_equalityEngine->hasTerm(a); }
bool TheoryDatatypes::areEqual( TNode a, TNode b ){
if( a==b ){
return true;
}else if( hasTerm( a ) && hasTerm( b ) ){
- return d_equalityEngine.areEqual( a, b );
+ return d_equalityEngine->areEqual(a, b);
}else{
return false;
}
if( a==b ){
return false;
}else if( hasTerm( a ) && hasTerm( b ) ){
- return d_equalityEngine.areDisequal( a, b, false );
+ return d_equalityEngine->areDisequal(a, b, false);
}else{
//TODO : constants here?
return false;
}
bool TheoryDatatypes::areCareDisequal( TNode x, TNode y ) {
- Assert(d_equalityEngine.hasTerm(x));
- Assert(d_equalityEngine.hasTerm(y));
- if( d_equalityEngine.isTriggerTerm(x, THEORY_DATATYPES) && d_equalityEngine.isTriggerTerm(y, THEORY_DATATYPES) ){
- TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_DATATYPES);
- TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_DATATYPES);
+ Assert(d_equalityEngine->hasTerm(x));
+ Assert(d_equalityEngine->hasTerm(y));
+ if (d_equalityEngine->isTriggerTerm(x, THEORY_DATATYPES)
+ && d_equalityEngine->isTriggerTerm(y, THEORY_DATATYPES))
+ {
+ TNode x_shared =
+ d_equalityEngine->getTriggerTermRepresentative(x, THEORY_DATATYPES);
+ TNode y_shared =
+ d_equalityEngine->getTriggerTermRepresentative(y, THEORY_DATATYPES);
EqualityStatus eqStatus = d_valuation.getEqualityStatus(x_shared, y_shared);
if( eqStatus==EQUALITY_FALSE_AND_PROPAGATED || eqStatus==EQUALITY_FALSE || eqStatus==EQUALITY_FALSE_IN_MODEL ){
return true;
TNode TheoryDatatypes::getRepresentative( TNode a ){
if( hasTerm( a ) ){
- return d_equalityEngine.getRepresentative( a );
+ return d_equalityEngine->getRepresentative(a);
}else{
return a;
}
}
Trace( c ) << "Datatypes model : " << std::endl;
- eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
+ eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(d_equalityEngine);
while( !eqcs_i.isFinished() ){
Node eqc = (*eqcs_i);
//if( !eqc.getType().isBoolean() ){
Trace( c ) << eqc << " : " << eqc.getType() << " : " << std::endl;
Trace( c ) << " { ";
//add terms to model
- eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
+ eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, d_equalityEngine);
while( !eqc_i.isFinished() ){
if( (*eqc_i)!=eqc ){
Trace( c ) << (*eqc_i) << " ";
<< std::endl;
//also include non-singleton equivalence classes TODO : revisit this
- eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
+ eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(d_equalityEngine);
while( !eqcs_i.isFinished() ){
TNode r = (*eqcs_i);
bool addedFirst = false;
TypeNode rtn = r.getType();
if (!rtn.isBoolean())
{
- eq::EqClassIterator eqc_i = eq::EqClassIterator(r, &d_equalityEngine);
+ eq::EqClassIterator eqc_i = eq::EqClassIterator(r, d_equalityEngine);
while (!eqc_i.isFinished())
{
TNode n = (*eqc_i);
if( atom.getKind()==APPLY_TESTER ){
Node n = atom[0];
if( hasTerm( n ) ){
- Node r = d_equalityEngine.getRepresentative( n );
+ Node r = d_equalityEngine->getRepresentative(n);
EqcInfo * ei = getOrMakeEqcInfo( r, false );
int l_index = getLabelIndex( ei, r );
int t_index = static_cast<int>(utils::indexOf(atom.getOperator()));
private:
/** The notify class */
NotifyClass d_notify;
- /** Equaltity engine */
- eq::EqualityEngine d_equalityEngine;
/** information necessary for equivalence classes */
std::map< Node, EqcInfo* > d_eqc_info;
/** map from nodes to their instantiated equivalent for each constructor type */
ProofNodeManager* pnm = nullptr);
~TheoryDatatypes();
- TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
-
- void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
+ //--------------------------------- initialization
+ /** get the official theory rewriter of this theory */
+ TheoryRewriter* getTheoryRewriter() override;
+ /**
+ * Returns true if we need an equality engine. If so, we initialize the
+ * information regarding how it should be setup. For details, see the
+ * documentation in Theory::needsEqualityEngine.
+ */
+ bool needsEqualityEngine(EeSetupInfo& esi) override;
+ /** finish initialization */
+ void finishInit() override;
+ //--------------------------------- end initialization
/** propagate */
void propagate(Effort effort) override;
void check(Effort e) override;
bool needsCheckLastEffort() override;
void preRegisterTerm(TNode n) override;
- void finishInit() override;
TrustNode expandDefinition(Node n) override;
TrustNode ppRewrite(TNode n) override;
void presolve() override;
{
return std::string("TheoryDatatypes");
}
- /** equality engine */
- eq::EqualityEngine* getEqualityEngine() override { return &d_equalityEngine; }
bool getCurrentSubstitution(int effort,
std::vector<Node>& vars,
std::vector<Node>& subs,
}
// allocate the equality engine
eet.d_allocEe.reset(allocateEqualityEngine(esi, c));
+ eet.d_usedEe = eet.d_allocEe.get();
}
const LogicInfo& logicInfo = d_te.getLogicInfo();
*/
struct EeTheoryInfo
{
+ EeTheoryInfo() : d_usedEe(nullptr) {}
+ /** The equality engine that the theory uses (if it exists) */
+ eq::EqualityEngine* d_usedEe;
/** The equality engine allocated by this theory (if it exists) */
std::unique_ptr<eq::EqualityEngine> d_allocEe;
};
ProofNodeManager* pnm)
: Theory(THEORY_FP, c, u, out, valuation, logicInfo, pnm),
d_notification(*this),
- d_equalityEngine(d_notification, c, "theory::fp::ee", true),
d_registeredTerms(u),
d_conv(u),
d_expansionRequested(false),
floatToRealMap(u),
abstractionMap(u)
{
+} /* TheoryFp::TheoryFp() */
+
+TheoryRewriter* TheoryFp::getTheoryRewriter() { return &d_rewriter; }
+
+bool TheoryFp::needsEqualityEngine(EeSetupInfo& esi)
+{
+ esi.d_notify = &d_notification;
+ esi.d_name = "theory::fp::ee";
+ return true;
+}
+
+void TheoryFp::finishInit()
+{
+ Assert(d_equalityEngine != nullptr);
// Kinds that are to be handled in the congruence closure
- d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_ABS);
- d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_NEG);
- d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_PLUS);
- // d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_SUB); // Removed
- d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_MULT);
- d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_DIV);
- d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_FMA);
- d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_SQRT);
- d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_REM);
- d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_RTI);
- // d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_MIN); // Removed
- // d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_MAX); // Removed
- d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_MIN_TOTAL);
- d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_MAX_TOTAL);
-
- // d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_EQ); // Removed
- d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_LEQ);
- d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_LT);
- // d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_GEQ); // Removed
- // d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_GT); // Removed
- d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_ISN);
- d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_ISSN);
- d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_ISZ);
- d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_ISINF);
- d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_ISNAN);
- d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_ISNEG);
- d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_ISPOS);
-
- d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR);
- d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT);
- d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_TO_FP_REAL);
- d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR);
- d_equalityEngine.addFunctionKind(
+ d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_ABS);
+ d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_NEG);
+ d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_PLUS);
+ // d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_SUB); // Removed
+ d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_MULT);
+ d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_DIV);
+ d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_FMA);
+ d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_SQRT);
+ d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_REM);
+ d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_RTI);
+ // d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_MIN); // Removed
+ // d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_MAX); // Removed
+ d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_MIN_TOTAL);
+ d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_MAX_TOTAL);
+
+ // d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_EQ); // Removed
+ d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_LEQ);
+ d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_LT);
+ // d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_GEQ); // Removed
+ // d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_GT); // Removed
+ d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_ISN);
+ d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_ISSN);
+ d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_ISZ);
+ d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_ISINF);
+ d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_ISNAN);
+ d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_ISNEG);
+ d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_ISPOS);
+
+ d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR);
+ d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT);
+ d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_FP_REAL);
+ d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR);
+ d_equalityEngine->addFunctionKind(
kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR);
- // d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_TO_FP_GENERIC); //
+ // d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_FP_GENERIC); //
// Needed in parsing, should be rewritten away
- // d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_TO_UBV); // Removed
- // d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_TO_SBV); // Removed
- // d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_TO_REAL); // Removed
- d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_TO_UBV_TOTAL);
- d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_TO_SBV_TOTAL);
- d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_TO_REAL_TOTAL);
-
- d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_COMPONENT_NAN);
- d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_COMPONENT_INF);
- d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_COMPONENT_ZERO);
- d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_COMPONENT_SIGN);
- d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_COMPONENT_EXPONENT);
- d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND);
- d_equalityEngine.addFunctionKind(kind::ROUNDINGMODE_BITBLAST);
-} /* TheoryFp::TheoryFp() */
+ // d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_UBV); // Removed
+ // d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_SBV); // Removed
+ // d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_REAL); // Removed
+ d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_UBV_TOTAL);
+ d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_SBV_TOTAL);
+ d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_REAL_TOTAL);
+
+ d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_COMPONENT_NAN);
+ d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_COMPONENT_INF);
+ d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_COMPONENT_ZERO);
+ d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_COMPONENT_SIGN);
+ d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_COMPONENT_EXPONENT);
+ d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND);
+ d_equalityEngine->addFunctionKind(kind::ROUNDINGMODE_BITBLAST);
+}
Node TheoryFp::minUF(Node node) {
Assert(node.getKind() == kind::FLOATINGPOINT_MIN);
// Add to the equality engine
if (k == kind::EQUAL)
{
- d_equalityEngine.addTriggerEquality(node);
+ d_equalityEngine->addTriggerEquality(node);
}
else
{
- d_equalityEngine.addTerm(node);
+ d_equalityEngine->addTerm(node);
}
// Give the expansion of classifications in terms of equalities
if (negated) {
Debug("fp-eq") << "TheoryFp::check(): adding dis-equality " << fact[0]
<< std::endl;
- d_equalityEngine.assertEquality(predicate, false, fact);
-
+ d_equalityEngine->assertEquality(predicate, false, fact);
} else {
Debug("fp-eq") << "TheoryFp::check(): adding equality " << fact
<< std::endl;
- d_equalityEngine.assertEquality(predicate, true, fact);
+ d_equalityEngine->assertEquality(predicate, true, fact);
}
} else {
// A system-wide invariant; predicates are registered before they are
// asserted
Assert(isRegistered(predicate));
- if (d_equalityEngine.isFunctionKind(predicate.getKind())) {
+ if (d_equalityEngine->isFunctionKind(predicate.getKind()))
+ {
Debug("fp-eq") << "TheoryFp::check(): adding predicate " << predicate
<< " is " << !negated << std::endl;
- d_equalityEngine.assertPredicate(predicate, !negated, fact);
+ d_equalityEngine->assertPredicate(predicate, !negated, fact);
}
}
}
} /* TheoryFp::check() */
-void TheoryFp::setMasterEqualityEngine(eq::EqualityEngine *eq) {
- d_equalityEngine.setMasterEqualityEngine(eq);
-}
-
TrustNode TheoryFp::explain(TNode n)
{
Trace("fp") << "TheoryFp::explain(): explain " << n << std::endl;
bool polarity = n.getKind() != kind::NOT;
TNode atom = polarity ? n : n[0];
if (atom.getKind() == kind::EQUAL) {
- d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions);
+ d_equalityEngine->explainEquality(atom[0], atom[1], polarity, assumptions);
} else {
- d_equalityEngine.explainPredicate(atom, polarity, assumptions);
+ d_equalityEngine->explainPredicate(atom, polarity, assumptions);
}
Node exp = helper::buildConjunct(assumptions);
<< " = " << t2 << std::endl;
std::vector<TNode> assumptions;
- d_theorySolver.d_equalityEngine.explainEquality(t1, t2, true, assumptions);
+ d_theorySolver.d_equalityEngine->explainEquality(t1, t2, true, assumptions);
Node conflict = helper::buildConjunct(assumptions);
Valuation valuation,
const LogicInfo& logicInfo,
ProofNodeManager* pnm = nullptr);
-
- TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
+ //--------------------------------- initialization
+ /** get the official theory rewriter of this theory */
+ TheoryRewriter* getTheoryRewriter() override;
+ /**
+ * Returns true if we need an equality engine. If so, we initialize the
+ * information regarding how it should be setup. For details, see the
+ * documentation in Theory::needsEqualityEngine.
+ */
+ bool needsEqualityEngine(EeSetupInfo& esi) override;
+ /** finish initialization */
+ void finishInit() override;
+ //--------------------------------- end initialization
TrustNode expandDefinition(Node node) override;
std::string identify() const override { return "THEORY_FP"; }
- void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
-
TrustNode explain(TNode n) override;
protected:
friend NotifyClass;
NotifyClass d_notification;
- eq::EqualityEngine d_equalityEngine;
/** General utility **/
void registerTerm(TNode node);
TheoryQuantifiers::~TheoryQuantifiers() {
}
+TheoryRewriter* TheoryQuantifiers::getTheoryRewriter() { return &d_rewriter; }
void TheoryQuantifiers::finishInit()
{
// quantifiers are not evaluated in getModelValue
ProofNodeManager* pnm = nullptr);
~TheoryQuantifiers();
- TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
-
+ //--------------------------------- initialization
+ /** get the official theory rewriter of this theory */
+ TheoryRewriter* getTheoryRewriter() override;
/** finish initialization */
void finishInit() override;
+ //--------------------------------- end initialization
+
void preRegisterTerm(TNode n) override;
void presolve() override;
void ppNotifyAssertions(const std::vector<Node>& assertions) override;
: Theory(THEORY_SEP, c, u, out, valuation, logicInfo, pnm),
d_lemmas_produced_c(u),
d_notify(*this),
- d_equalityEngine(d_notify, c, "theory::sep::ee", true),
d_conflict(c, false),
d_reduce(u),
d_infer(c),
d_true = NodeManager::currentNM()->mkConst<bool>(true);
d_false = NodeManager::currentNM()->mkConst<bool>(false);
d_bounds_init = false;
-
- // The kinds we are treating as function application in congruence
- d_equalityEngine.addFunctionKind(kind::SEP_PTO);
- //d_equalityEngine.addFunctionKind(kind::SEP_STAR);
}
TheorySep::~TheorySep() {
}
}
-void TheorySep::setMasterEqualityEngine(eq::EqualityEngine* eq) {
- d_equalityEngine.setMasterEqualityEngine(eq);
+TheoryRewriter* TheorySep::getTheoryRewriter() { return &d_rewriter; }
+
+bool TheorySep::needsEqualityEngine(EeSetupInfo& esi)
+{
+ esi.d_notify = &d_notify;
+ esi.d_name = "theory::sep::ee";
+ return true;
+}
+
+void TheorySep::finishInit()
+{
+ Assert(d_equalityEngine != nullptr);
+ // The kinds we are treating as function application in congruence
+ d_equalityEngine->addFunctionKind(kind::SEP_PTO);
+ // we could but don't do congruence on SEP_STAR here.
}
Node TheorySep::mkAnd( std::vector< TNode >& assumptions ) {
bool polarity = literal.getKind() != kind::NOT;
TNode atom = polarity ? literal : literal[0];
if (atom.getKind() == kind::EQUAL) {
- d_equalityEngine.explainEquality( atom[0], atom[1], polarity, assumptions, NULL );
+ d_equalityEngine->explainEquality(
+ atom[0], atom[1], polarity, assumptions, NULL);
} else {
- d_equalityEngine.explainPredicate( atom, polarity, assumptions );
+ d_equalityEngine->explainPredicate(atom, polarity, assumptions);
}
}
}
void TheorySep::addSharedTerm(TNode t) {
Debug("sep") << "TheorySep::addSharedTerm(" << t << ")" << std::endl;
- d_equalityEngine.addTriggerTerm(t, THEORY_SEP);
+ d_equalityEngine->addTriggerTerm(t, THEORY_SEP);
}
EqualityStatus TheorySep::getEqualityStatus(TNode a, TNode b) {
- Assert(d_equalityEngine.hasTerm(a) && d_equalityEngine.hasTerm(b));
- if (d_equalityEngine.areEqual(a, b)) {
+ Assert(d_equalityEngine->hasTerm(a) && d_equalityEngine->hasTerm(b));
+ if (d_equalityEngine->areEqual(a, b))
+ {
// The terms are implied to be equal
return EQUALITY_TRUE;
}
- else if (d_equalityEngine.areDisequal(a, b, false)) {
+ else if (d_equalityEngine->areDisequal(a, b, false))
+ {
// The terms are implied to be dis-equal
return EQUALITY_FALSE;
}
computeRelevantTerms(termSet);
// Send the equality engine information to the model
- return m->assertEqualityEngine(&d_equalityEngine, &termSet);
+ return m->assertEqualityEngine(d_equalityEngine, &termSet);
}
void TheorySep::postProcessModel( TheoryModel* m ){
if( !is_spatial ){
Trace("sep-assert") << "Asserting " << atom << ", pol = " << polarity << " to EE..." << std::endl;
if( s_atom.getKind()==kind::EQUAL ){
- d_equalityEngine.assertEquality(atom, polarity, fact);
+ d_equalityEngine->assertEquality(atom, polarity, fact);
}else{
- d_equalityEngine.assertPredicate(atom, polarity, fact);
+ d_equalityEngine->assertPredicate(atom, polarity, fact);
}
Trace("sep-assert") << "Done asserting " << atom << " to EE." << std::endl;
}else if( s_atom.getKind()==kind::SEP_PTO ){
Node pto_lbl = NodeManager::currentNM()->mkNode( kind::SINGLETON, s_atom[0] );
Assert(s_lbl == pto_lbl);
Trace("sep-assert") << "Asserting " << s_atom << std::endl;
- d_equalityEngine.assertPredicate(s_atom, polarity, fact);
+ d_equalityEngine->assertPredicate(s_atom, polarity, fact);
//associate the equivalence class of the lhs with this pto
Node r = getRepresentative( s_lbl );
HeapAssertInfo * ei = getOrMakeEqcInfo( r, true );
Trace("sep-process") << "---" << std::endl;
}
if(Trace.isOn("sep-eqc")) {
- eq::EqClassesIterator eqcs2_i = eq::EqClassesIterator( &d_equalityEngine );
+ eq::EqClassesIterator eqcs2_i = eq::EqClassesIterator(d_equalityEngine);
Trace("sep-eqc") << "EQC:" << std::endl;
while( !eqcs2_i.isFinished() ){
Node eqc = (*eqcs2_i);
- eq::EqClassIterator eqc2_i = eq::EqClassIterator( eqc, &d_equalityEngine );
+ eq::EqClassIterator eqc2_i = eq::EqClassIterator(eqc, d_equalityEngine);
Trace("sep-eqc") << "Eqc( " << eqc << " ) : { ";
while( !eqc2_i.isFinished() ) {
if( (*eqc2_i)!=eqc ){
}
Node TheorySep::getRepresentative( Node t ) {
- if( d_equalityEngine.hasTerm( t ) ){
- return d_equalityEngine.getRepresentative( t );
+ if (d_equalityEngine->hasTerm(t))
+ {
+ return d_equalityEngine->getRepresentative(t);
}else{
return t;
}
}
-bool TheorySep::hasTerm( Node a ){
- return d_equalityEngine.hasTerm( a );
-}
+bool TheorySep::hasTerm(Node a) { return d_equalityEngine->hasTerm(a); }
bool TheorySep::areEqual( Node a, Node b ){
if( a==b ){
return true;
}else if( hasTerm( a ) && hasTerm( b ) ){
- return d_equalityEngine.areEqual( a, b );
+ return d_equalityEngine->areEqual(a, b);
}else{
return false;
}
if( a==b ){
return false;
}else if( hasTerm( a ) && hasTerm( b ) ){
- if( d_equalityEngine.areDisequal( a, b, false ) ){
+ if (d_equalityEngine->areDisequal(a, b, false))
+ {
return true;
}
}
bool pol = d_pending[i].getKind()!=kind::NOT;
Trace("sep-pending") << "Sep : Assert to EE : " << atom << ", pol = " << pol << std::endl;
if( atom.getKind()==kind::EQUAL ){
- d_equalityEngine.assertEquality(atom, pol, d_pending_exp[i]);
+ d_equalityEngine->assertEquality(atom, pol, d_pending_exp[i]);
}else{
- d_equalityEngine.assertPredicate(atom, pol, d_pending_exp[i]);
+ d_equalityEngine->assertPredicate(atom, pol, d_pending_exp[i]);
}
}
}else{
ProofNodeManager* pnm = nullptr);
~TheorySep();
- TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
-
- void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
+ //--------------------------------- initialization
+ /** get the official theory rewriter of this theory */
+ TheoryRewriter* getTheoryRewriter() override;
+ /**
+ * Returns true if we need an equality engine. If so, we initialize the
+ * information regarding how it should be setup. For details, see the
+ * documentation in Theory::needsEqualityEngine.
+ */
+ bool needsEqualityEngine(EeSetupInfo& esi) override;
+ /** finish initialization */
+ void finishInit() override;
+ //--------------------------------- end initialization
std::string identify() const override { return std::string("TheorySep"); }
/** The notify class for d_equalityEngine */
NotifyClass d_notify;
- /** Equaltity engine */
- eq::EqualityEngine d_equalityEngine;
-
/** Are we in conflict? */
context::CDO<bool> d_conflict;
std::vector< Node > d_pending_exp;
void doPendingFacts();
public:
- eq::EqualityEngine* getEqualityEngine() override { return &d_equalityEngine; }
void initializeBounds();
};/* class TheorySep */
ProofNodeManager* pnm)
: Theory(THEORY_SETS, c, u, out, valuation, logicInfo, pnm),
d_internal(new TheorySetsPrivate(*this, c, u)),
- d_notify(*d_internal.get()),
- d_equalityEngine(d_notify, c, "theory::sets::ee", true)
+ d_notify(*d_internal.get())
{
// Do not move me to the header.
// The constructor + destructor are not in the header as d_internal is a
return d_internal->getTheoryRewriter();
}
+bool TheorySets::needsEqualityEngine(EeSetupInfo& esi)
+{
+ esi.d_notify = &d_notify;
+ esi.d_name = "theory::sets::ee";
+ return true;
+}
+
void TheorySets::finishInit()
{
+ Assert(d_equalityEngine != nullptr);
+
d_valuation.setUnevaluatedKind(COMPREHENSION);
// choice is used to eliminate witness
d_valuation.setUnevaluatedKind(WITNESS);
// functions we are doing congruence over
- d_equalityEngine.addFunctionKind(kind::SINGLETON);
- d_equalityEngine.addFunctionKind(kind::UNION);
- d_equalityEngine.addFunctionKind(kind::INTERSECTION);
- d_equalityEngine.addFunctionKind(kind::SETMINUS);
- d_equalityEngine.addFunctionKind(kind::MEMBER);
- d_equalityEngine.addFunctionKind(kind::SUBSET);
+ d_equalityEngine->addFunctionKind(kind::SINGLETON);
+ d_equalityEngine->addFunctionKind(kind::UNION);
+ d_equalityEngine->addFunctionKind(kind::INTERSECTION);
+ d_equalityEngine->addFunctionKind(kind::SETMINUS);
+ d_equalityEngine->addFunctionKind(kind::MEMBER);
+ d_equalityEngine->addFunctionKind(kind::SUBSET);
// relation operators
- d_equalityEngine.addFunctionKind(PRODUCT);
- d_equalityEngine.addFunctionKind(JOIN);
- d_equalityEngine.addFunctionKind(TRANSPOSE);
- d_equalityEngine.addFunctionKind(TCLOSURE);
- d_equalityEngine.addFunctionKind(JOIN_IMAGE);
- d_equalityEngine.addFunctionKind(IDEN);
- d_equalityEngine.addFunctionKind(APPLY_CONSTRUCTOR);
+ d_equalityEngine->addFunctionKind(PRODUCT);
+ d_equalityEngine->addFunctionKind(JOIN);
+ d_equalityEngine->addFunctionKind(TRANSPOSE);
+ d_equalityEngine->addFunctionKind(TCLOSURE);
+ d_equalityEngine->addFunctionKind(JOIN_IMAGE);
+ d_equalityEngine->addFunctionKind(IDEN);
+ d_equalityEngine->addFunctionKind(APPLY_CONSTRUCTOR);
// we do congruence over cardinality
- d_equalityEngine.addFunctionKind(CARD);
+ d_equalityEngine->addFunctionKind(CARD);
// finish initialization internally
d_internal->finishInit();
return d_internal->isEntailed( n, pol );
}
-eq::EqualityEngine* TheorySets::getEqualityEngine()
-{
- return &d_equalityEngine;
-}
-
-void TheorySets::setMasterEqualityEngine(eq::EqualityEngine* eq)
-{
- d_equalityEngine.setMasterEqualityEngine(eq);
-}
-
/**************************** eq::NotifyClass *****************************/
bool TheorySets::NotifyClass::eqNotifyTriggerEquality(TNode equality,
//--------------------------------- initialization
/** get the official theory rewriter of this theory */
TheoryRewriter* getTheoryRewriter() override;
+ /**
+ * Returns true if we need an equality engine. If so, we initialize the
+ * information regarding how it should be setup. For details, see the
+ * documentation in Theory::needsEqualityEngine.
+ */
+ bool needsEqualityEngine(EeSetupInfo& esi) override;
/** finish initialization */
void finishInit() override;
//--------------------------------- end initialization
PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
void presolve() override;
void propagate(Effort) override;
- void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
bool isEntailed(Node n, bool pol);
- /* equality engine */
- virtual eq::EqualityEngine* getEqualityEngine() override;
private:
/** Functions to handle callbacks from equality engine */
class NotifyClass : public eq::EqualityEngineNotify
/** The internal theory */
std::unique_ptr<TheorySetsPrivate> d_internal;
/** Instance of the above class */
- NotifyClass d_notify;
- /** Equality engine */
- eq::EqualityEngine d_equalityEngine;
+ NotifyClass d_notify;
}; /* class TheorySets */
}/* CVC4::theory::sets namespace */
SolverState::SolverState(context::Context* c,
context::UserContext* u,
- eq::EqualityEngine& ee,
Valuation& v)
: d_context(c),
d_ucontext(u),
- d_ee(ee),
+ d_ee(nullptr),
d_eeDisequalities(c),
d_valuation(v),
d_conflict(c, false),
}
}
+void SolverState::finishInit(eq::EqualityEngine* ee)
+{
+ Assert(ee != nullptr);
+ d_ee = ee;
+}
+
context::Context* SolverState::getSatContext() const { return d_context; }
context::UserContext* SolverState::getUserContext() const { return d_ucontext; }
Node SolverState::getRepresentative(Node t) const
{
- if (d_ee.hasTerm(t))
+ if (d_ee->hasTerm(t))
{
- return d_ee.getRepresentative(t);
+ return d_ee->getRepresentative(t);
}
return t;
}
-bool SolverState::hasTerm(Node a) const { return d_ee.hasTerm(a); }
+bool SolverState::hasTerm(Node a) const { return d_ee->hasTerm(a); }
bool SolverState::areEqual(Node a, Node b) const
{
}
else if (hasTerm(a) && hasTerm(b))
{
- return d_ee.areEqual(a, b);
+ return d_ee->areEqual(a, b);
}
return false;
}
}
else if (hasTerm(a) && hasTerm(b))
{
- Node ar = d_ee.getRepresentative(a);
- Node br = d_ee.getRepresentative(b);
+ Node ar = d_ee->getRepresentative(a);
+ Node br = d_ee->getRepresentative(b);
return (ar != br && ar.isConst() && br.isConst())
- || d_ee.areDisequal(ar, br, false);
+ || d_ee->areDisequal(ar, br, false);
}
Node ar = getRepresentative(a);
Node br = getRepresentative(b);
return ar != br && ar.isConst() && br.isConst();
}
-eq::EqualityEngine* SolverState::getEqualityEngine() const { return &d_ee; }
+eq::EqualityEngine* SolverState::getEqualityEngine() const { return d_ee; }
const context::CDList<Node>& SolverState::getDisequalityList() const
{
Kind k = t.getKind();
if (k == STRING_LENGTH || k == STRING_TO_CODE)
{
- Node r = d_ee.getRepresentative(t[0]);
+ Node r = d_ee->getRepresentative(t[0]);
EqcInfo* ei = getOrMakeEqcInfo(r);
if (k == STRING_LENGTH)
{
NodeManager* nm = NodeManager::currentNM();
for (const Node& eqc : n)
{
- Assert(d_ee.getRepresentative(eqc) == eqc);
+ Assert(d_ee->getRepresentative(eqc) == eqc);
TypeNode tnEqc = eqc.getType();
EqcInfo* ei = getOrMakeEqcInfo(eqc, false);
Node lt = ei ? ei->d_lengthTerm : Node::null();
if (!lt.isNull())
{
lt = nm->mkNode(STRING_LENGTH, lt);
- Node r = d_ee.getRepresentative(lt);
+ Node r = d_ee->getRepresentative(lt);
std::pair<Node, TypeNode> lkey(r, tnEqc);
if (eqc_to_leqc.find(lkey) == eqc_to_leqc.end())
{
public:
SolverState(context::Context* c,
context::UserContext* u,
- eq::EqualityEngine& ee,
Valuation& v);
~SolverState();
+ /**
+ * Finish initialize, ee is a pointer to the official equality engine
+ * of theory of strings.
+ */
+ void finishInit(eq::EqualityEngine* ee);
/** Get the SAT context */
context::Context* getSatContext() const;
/** Get the user context */
context::Context* d_context;
/** Pointer to the user context object used by the theory of strings. */
context::UserContext* d_ucontext;
- /** Reference to equality engine of the theory of strings. */
- eq::EqualityEngine& d_ee;
+ /** Pointer to equality engine of the theory of strings. */
+ eq::EqualityEngine* d_ee;
/**
* The (SAT-context-dependent) list of disequalities that have been asserted
* to the equality engine above.
StringsProxyVarAttribute;
TermRegistry::TermRegistry(SolverState& s,
- eq::EqualityEngine& ee,
OutputChannel& out,
SequencesStatistics& statistics,
ProofNodeManager* pnm)
: d_state(s),
- d_ee(ee),
d_out(out),
d_statistics(statistics),
d_hasStrCode(false),
{
return;
}
+ eq::EqualityEngine* ee = d_state.getEqualityEngine();
d_preregisteredTerms.insert(n);
Trace("strings-preregister")
<< "TheoryString::preregister : " << n << std::endl;
ss << "Equality between regular expressions is not supported";
throw LogicException(ss.str());
}
- d_ee.addTriggerEquality(n);
+ ee->addTriggerEquality(n);
return;
}
else if (k == STRING_IN_REGEXP)
{
d_out.requirePhase(n, true);
- d_ee.addTriggerPredicate(n);
- d_ee.addTerm(n[0]);
- d_ee.addTerm(n[1]);
+ ee->addTriggerPredicate(n);
+ ee->addTerm(n[0]);
+ ee->addTerm(n[1]);
return;
}
else if (k == STRING_TO_CODE)
}
}
}
- d_ee.addTerm(n);
+ ee->addTerm(n);
}
else if (tn.isBoolean())
{
// Get triggered for both equal and dis-equal
- d_ee.addTriggerPredicate(n);
+ ee->addTriggerPredicate(n);
}
else
{
// Function applications/predicates
- d_ee.addTerm(n);
+ ee->addTerm(n);
}
// Set d_functionsTerms stores all function applications that are
// relevant to theory combination. Notice that this is a subset of
// Concatenation terms do not need to be considered here because
// their arguments have string type and do not introduce any shared
// terms.
- if (n.hasOperator() && d_ee.isFunctionKind(k) && k != STRING_CONCAT)
+ if (n.hasOperator() && ee->isFunctionKind(k) && k != STRING_CONCAT)
{
d_functionsTerms.push_back(n);
}
{
// preregister the empty word for the type
Node emp = Word::mkEmptyWord(tn);
- if (!d_ee.hasTerm(emp))
+ if (!d_state.hasTerm(emp))
{
preRegisterTerm(emp);
}
public:
TermRegistry(SolverState& s,
- eq::EqualityEngine& ee,
OutputChannel& out,
SequencesStatistics& statistics,
ProofNodeManager* pnm);
uint32_t d_cardSize;
/** Reference to the solver state of the theory of strings. */
SolverState& d_state;
- /** Reference to equality engine of the theory of strings. */
- eq::EqualityEngine& d_ee;
/** Reference to the output channel of the theory of strings. */
OutputChannel& d_out;
/** Reference to the statistics for the theory of strings/sequences. */
: Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo, pnm),
d_notify(*this),
d_statistics(),
- d_equalityEngine(d_notify, c, "theory::strings::ee", true),
- d_state(c, u, d_equalityEngine, d_valuation),
- d_termReg(d_state, d_equalityEngine, out, d_statistics, nullptr),
+ d_state(c, u, d_valuation),
+ d_termReg(d_state, out, d_statistics, nullptr),
d_extTheory(this),
d_im(c, u, d_state, d_termReg, d_extTheory, out, d_statistics),
d_rewriter(&d_statistics.d_rewrites),
d_statistics),
d_stringsFmf(c, u, valuation, d_termReg)
{
- bool eagerEval = options::stringEagerEval();
- // The kinds we are treating as function application in congruence
- d_equalityEngine.addFunctionKind(kind::STRING_LENGTH, eagerEval);
- d_equalityEngine.addFunctionKind(kind::STRING_CONCAT, eagerEval);
- d_equalityEngine.addFunctionKind(kind::STRING_IN_REGEXP, eagerEval);
- d_equalityEngine.addFunctionKind(kind::STRING_TO_CODE, eagerEval);
- d_equalityEngine.addFunctionKind(kind::SEQ_UNIT, eagerEval);
-
- // extended functions
- d_equalityEngine.addFunctionKind(kind::STRING_STRCTN, eagerEval);
- d_equalityEngine.addFunctionKind(kind::STRING_LEQ, eagerEval);
- d_equalityEngine.addFunctionKind(kind::STRING_SUBSTR, eagerEval);
- d_equalityEngine.addFunctionKind(kind::STRING_UPDATE, eagerEval);
- d_equalityEngine.addFunctionKind(kind::STRING_ITOS, eagerEval);
- d_equalityEngine.addFunctionKind(kind::STRING_STOI, eagerEval);
- d_equalityEngine.addFunctionKind(kind::STRING_STRIDOF, eagerEval);
- d_equalityEngine.addFunctionKind(kind::STRING_STRREPL, eagerEval);
- d_equalityEngine.addFunctionKind(kind::STRING_STRREPLALL, eagerEval);
- d_equalityEngine.addFunctionKind(kind::STRING_REPLACE_RE, eagerEval);
- d_equalityEngine.addFunctionKind(kind::STRING_REPLACE_RE_ALL, eagerEval);
- d_equalityEngine.addFunctionKind(kind::STRING_STRREPLALL, eagerEval);
- d_equalityEngine.addFunctionKind(kind::STRING_TOLOWER, eagerEval);
- d_equalityEngine.addFunctionKind(kind::STRING_TOUPPER, eagerEval);
- d_equalityEngine.addFunctionKind(kind::STRING_REV, eagerEval);
d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) );
d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) );
}
TheoryRewriter* TheoryStrings::getTheoryRewriter() { return &d_rewriter; }
-std::string TheoryStrings::identify() const
-{
- return std::string("TheoryStrings");
-}
-eq::EqualityEngine* TheoryStrings::getEqualityEngine()
+
+bool TheoryStrings::needsEqualityEngine(EeSetupInfo& esi)
{
- return &d_equalityEngine;
+ esi.d_notify = &d_notify;
+ esi.d_name = "theory::strings::ee";
+ return true;
}
+
void TheoryStrings::finishInit()
{
+ Assert(d_equalityEngine != nullptr);
+
// witness is used to eliminate str.from_code
d_valuation.setUnevaluatedKind(WITNESS);
+
+ bool eagerEval = options::stringEagerEval();
+ // The kinds we are treating as function application in congruence
+ d_equalityEngine->addFunctionKind(kind::STRING_LENGTH, eagerEval);
+ d_equalityEngine->addFunctionKind(kind::STRING_CONCAT, eagerEval);
+ d_equalityEngine->addFunctionKind(kind::STRING_IN_REGEXP, eagerEval);
+ d_equalityEngine->addFunctionKind(kind::STRING_TO_CODE, eagerEval);
+ d_equalityEngine->addFunctionKind(kind::SEQ_UNIT, eagerEval);
+ // extended functions
+ d_equalityEngine->addFunctionKind(kind::STRING_STRCTN, eagerEval);
+ d_equalityEngine->addFunctionKind(kind::STRING_LEQ, eagerEval);
+ d_equalityEngine->addFunctionKind(kind::STRING_SUBSTR, eagerEval);
+ d_equalityEngine->addFunctionKind(kind::STRING_UPDATE, eagerEval);
+ d_equalityEngine->addFunctionKind(kind::STRING_ITOS, eagerEval);
+ d_equalityEngine->addFunctionKind(kind::STRING_STOI, eagerEval);
+ d_equalityEngine->addFunctionKind(kind::STRING_STRIDOF, eagerEval);
+ d_equalityEngine->addFunctionKind(kind::STRING_STRREPL, eagerEval);
+ d_equalityEngine->addFunctionKind(kind::STRING_STRREPLALL, eagerEval);
+ d_equalityEngine->addFunctionKind(kind::STRING_REPLACE_RE, eagerEval);
+ d_equalityEngine->addFunctionKind(kind::STRING_REPLACE_RE_ALL, eagerEval);
+ d_equalityEngine->addFunctionKind(kind::STRING_STRREPLALL, eagerEval);
+ d_equalityEngine->addFunctionKind(kind::STRING_TOLOWER, eagerEval);
+ d_equalityEngine->addFunctionKind(kind::STRING_TOUPPER, eagerEval);
+ d_equalityEngine->addFunctionKind(kind::STRING_REV, eagerEval);
+
+ d_state.finishInit(d_equalityEngine);
+}
+
+std::string TheoryStrings::identify() const
+{
+ return std::string("TheoryStrings");
}
bool TheoryStrings::areCareDisequal( TNode x, TNode y ) {
- Assert(d_equalityEngine.hasTerm(x));
- Assert(d_equalityEngine.hasTerm(y));
- if( d_equalityEngine.isTriggerTerm(x, THEORY_STRINGS) && d_equalityEngine.isTriggerTerm(y, THEORY_STRINGS) ){
- TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_STRINGS);
- TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_STRINGS);
+ Assert(d_equalityEngine->hasTerm(x));
+ Assert(d_equalityEngine->hasTerm(y));
+ if (d_equalityEngine->isTriggerTerm(x, THEORY_STRINGS)
+ && d_equalityEngine->isTriggerTerm(y, THEORY_STRINGS))
+ {
+ TNode x_shared =
+ d_equalityEngine->getTriggerTermRepresentative(x, THEORY_STRINGS);
+ TNode y_shared =
+ d_equalityEngine->getTriggerTermRepresentative(y, THEORY_STRINGS);
EqualityStatus eqStatus = d_valuation.getEqualityStatus(x_shared, y_shared);
if( eqStatus==EQUALITY_FALSE_AND_PROPAGATED || eqStatus==EQUALITY_FALSE || eqStatus==EQUALITY_FALSE_IN_MODEL ){
return true;
return false;
}
-void TheoryStrings::setMasterEqualityEngine(eq::EqualityEngine* eq) {
- d_equalityEngine.setMasterEqualityEngine(eq);
-}
-
void TheoryStrings::addSharedTerm(TNode t) {
Debug("strings") << "TheoryStrings::addSharedTerm(): "
<< t << " " << t.getType().isBoolean() << endl;
- d_equalityEngine.addTriggerTerm(t, THEORY_STRINGS);
+ d_equalityEngine->addTriggerTerm(t, THEORY_STRINGS);
if (options::stringExp())
{
d_esolver.addSharedTerm(t);
}
EqualityStatus TheoryStrings::getEqualityStatus(TNode a, TNode b) {
- if( d_equalityEngine.hasTerm(a) && d_equalityEngine.hasTerm(b) ){
- if (d_equalityEngine.areEqual(a, b)) {
+ if (d_equalityEngine->hasTerm(a) && d_equalityEngine->hasTerm(b))
+ {
+ if (d_equalityEngine->areEqual(a, b))
+ {
// The terms are implied to be equal
return EQUALITY_TRUE;
}
- if (d_equalityEngine.areDisequal(a, b, false)) {
+ if (d_equalityEngine->areDisequal(a, b, false))
+ {
// The terms are implied to be dis-equal
return EQUALITY_FALSE;
}
// Compute terms appearing in assertions and shared terms
computeRelevantTerms(termSet);
// assert the (relevant) portion of the equality engine to the model
- if (!m->assertEqualityEngine(&d_equalityEngine, &termSet))
+ if (!m->assertEqualityEngine(d_equalityEngine, &termSet))
{
Unreachable()
<< "TheoryStrings::collectModelInfo: failed to assert equality engine"
<< "Theory of strings " << e << " effort check " << std::endl;
if(Trace.isOn("strings-eqc")) {
for( unsigned t=0; t<2; t++ ) {
- eq::EqClassesIterator eqcs2_i = eq::EqClassesIterator( &d_equalityEngine );
+ eq::EqClassesIterator eqcs2_i = eq::EqClassesIterator(d_equalityEngine);
Trace("strings-eqc") << (t==0 ? "STRINGS:" : "OTHER:") << std::endl;
while( !eqcs2_i.isFinished() ){
Node eqc = (*eqcs2_i);
bool print = (t == 0 && eqc.getType().isStringLike())
|| (t == 1 && !eqc.getType().isStringLike());
if (print) {
- eq::EqClassIterator eqc2_i = eq::EqClassIterator( eqc, &d_equalityEngine );
+ eq::EqClassIterator eqc2_i =
+ eq::EqClassIterator(eqc, d_equalityEngine);
Trace("strings-eqc") << "Eqc( " << eqc << " ) : { ";
while( !eqc2_i.isFinished() ) {
if( (*eqc2_i)!=eqc && (*eqc2_i).getKind()!=kind::EQUAL ){
if( t2!=NULL ){
Node f1 = t1->getData();
Node f2 = t2->getData();
- if( !d_equalityEngine.areEqual( f1, f2 ) ){
+ if (!d_equalityEngine->areEqual(f1, f2))
+ {
Trace("strings-cg-debug") << "TheoryStrings::computeCareGraph(): checking function " << f1 << " and " << f2 << std::endl;
vector< pair<TNode, TNode> > currentPairs;
for (unsigned k = 0; k < f1.getNumChildren(); ++ k) {
TNode x = f1[k];
TNode y = f2[k];
- Assert(d_equalityEngine.hasTerm(x));
- Assert(d_equalityEngine.hasTerm(y));
- Assert(!d_equalityEngine.areDisequal(x, y, false));
+ Assert(d_equalityEngine->hasTerm(x));
+ Assert(d_equalityEngine->hasTerm(y));
+ Assert(!d_equalityEngine->areDisequal(x, y, false));
Assert(!areCareDisequal(x, y));
- if( !d_equalityEngine.areEqual( x, y ) ){
- if( d_equalityEngine.isTriggerTerm(x, THEORY_STRINGS) && d_equalityEngine.isTriggerTerm(y, THEORY_STRINGS) ){
- TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_STRINGS);
- TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_STRINGS);
+ if (!d_equalityEngine->areEqual(x, y))
+ {
+ if (d_equalityEngine->isTriggerTerm(x, THEORY_STRINGS)
+ && d_equalityEngine->isTriggerTerm(y, THEORY_STRINGS))
+ {
+ TNode x_shared = d_equalityEngine->getTriggerTermRepresentative(
+ x, THEORY_STRINGS);
+ TNode y_shared = d_equalityEngine->getTriggerTermRepresentative(
+ y, THEORY_STRINGS);
currentPairs.push_back(make_pair(x_shared, y_shared));
}
}
std::map<TNode, TNodeTrie>::iterator it2 = it;
++it2;
for( ; it2 != t1->d_data.end(); ++it2 ){
- if( !d_equalityEngine.areDisequal(it->first, it2->first, false) ){
+ if (!d_equalityEngine->areDisequal(it->first, it2->first, false))
+ {
if( !areCareDisequal(it->first, it2->first) ){
addCarePairs( &it->second, &it2->second, arity, depth+1 );
}
{
for (std::pair<const TNode, TNodeTrie>& tt2 : t2->d_data)
{
- if (!d_equalityEngine.areDisequal(tt1.first, tt2.first, false))
+ if (!d_equalityEngine->areDisequal(tt1.first, tt2.first, false))
{
if (!areCareDisequal(tt1.first, tt2.first))
{
std::vector< TNode > reps;
bool has_trigger_arg = false;
for( unsigned j=0; j<f1.getNumChildren(); j++ ){
- reps.push_back( d_equalityEngine.getRepresentative( f1[j] ) );
- if( d_equalityEngine.isTriggerTerm( f1[j], THEORY_STRINGS ) ){
+ reps.push_back(d_equalityEngine->getRepresentative(f1[j]));
+ if (d_equalityEngine->isTriggerTerm(f1[j], THEORY_STRINGS))
+ {
has_trigger_arg = true;
}
}
const std::vector<Node>& seqc = d_bsolver.getStringEqc();
for (const Node& eqc : seqc)
{
- eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, &d_equalityEngine);
+ eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, d_equalityEngine);
while (!eqc_i.isFinished())
{
Node n = (*eqc_i);
const LogicInfo& logicInfo,
ProofNodeManager* pnm);
~TheoryStrings();
+ //--------------------------------- initialization
+ /** get the official theory rewriter of this theory */
+ TheoryRewriter* getTheoryRewriter() override;
+ /**
+ * Returns true if we need an equality engine. If so, we initialize the
+ * information regarding how it should be setup. For details, see the
+ * documentation in Theory::needsEqualityEngine.
+ */
+ bool needsEqualityEngine(EeSetupInfo& esi) override;
/** finish initialization */
void finishInit() override;
- /** Get the theory rewriter of this class */
- TheoryRewriter* getTheoryRewriter() override;
- /** Set the master equality engine */
- void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
+ //--------------------------------- end initialization
/** Identify this theory */
std::string identify() const override;
/** Propagate */
void propagate(Effort e) override;
/** Explain */
TrustNode explain(TNode literal) override;
- /** Get the equality engine */
- eq::EqualityEngine* getEqualityEngine() override;
/** Get current substitution */
bool getCurrentSubstitution(int effort,
std::vector<Node>& vars,
* theories is collected in this object.
*/
SequencesStatistics d_statistics;
- /** Equaltity engine */
- eq::EqualityEngine d_equalityEngine;
/** The solver state object */
SolverState d_state;
/** The term registry for this theory */
ProofNodeManager* pnm,
std::string name)
: d_id(id),
- d_instanceName(name),
d_satContext(satContext),
d_userContext(userContext),
d_logicInfo(logicInfo),
d_careGraph(NULL),
d_quantEngine(NULL),
d_decManager(nullptr),
+ d_instanceName(name),
d_checkTime(getStatsPrefix(id) + name + "::checkTime"),
d_computeCareGraphTime(getStatsPrefix(id) + name
+ "::computeCareGraphTime"),
d_sharedTerms(satContext),
d_out(&out),
d_valuation(valuation),
+ d_equalityEngine(nullptr),
+ d_allocEqualityEngine(nullptr),
d_proofsEnabled(false)
{
smtStatisticsRegistry()->registerStat(&d_checkTime);
smtStatisticsRegistry()->unregisterStat(&d_computeCareGraphTime);
}
-bool Theory::needsEqualityEngine(EeSetupInfo& esi) { return false; }
+bool Theory::needsEqualityEngine(EeSetupInfo& esi)
+{
+ // by default, this theory does not use an (official) equality engine
+ return false;
+}
+
+void Theory::setEqualityEngine(eq::EqualityEngine* ee)
+{
+ // set the equality engine pointer
+ d_equalityEngine = ee;
+}
+void Theory::setQuantifiersEngine(QuantifiersEngine* qe)
+{
+ Assert(d_quantEngine == nullptr);
+ d_quantEngine = qe;
+}
+
+void Theory::setDecisionManager(DecisionManager* dm)
+{
+ Assert(d_decManager == nullptr);
+ Assert(dm != nullptr);
+ d_decManager = dm;
+}
+
+void Theory::finishInitStandalone()
+{
+ EeSetupInfo esi;
+ if (needsEqualityEngine(esi))
+ {
+ // always associated with the same SAT context as the theory (d_satContext)
+ d_allocEqualityEngine.reset(new eq::EqualityEngine(
+ *esi.d_notify, d_satContext, esi.d_name, esi.d_constantsAreTriggers));
+ // use it as the official equality engine
+ d_equalityEngine = d_allocEqualityEngine.get();
+ }
+ finishInit();
+}
TheoryId Theory::theoryOf(options::TheoryOfMode mode, TNode node)
{
d_careGraph = NULL;
}
-void Theory::setQuantifiersEngine(QuantifiersEngine* qe) {
- Assert(d_quantEngine == NULL);
- Assert(qe != NULL);
- d_quantEngine = qe;
-}
-
-void Theory::setDecisionManager(DecisionManager* dm)
+eq::EqualityEngine* Theory::getEqualityEngine()
{
- Assert(d_decManager == nullptr);
- Assert(dm != nullptr);
- d_decManager = dm;
+ // get the assigned equality engine, which is a pointer stored in this class
+ return d_equalityEngine;
}
}/* CVC4::theory namespace */
* RegisteredAttr works. (If you need multiple instances of the same
* theory, you'll have to write a multiplexed theory that dispatches
* all calls to them.)
+ *
+ * NOTE: A Theory has a special way of being initialized. The owner of a Theory
+ * is either:
+ *
+ * (A) Using Theory as a standalone object, not associated with a TheoryEngine.
+ * In this case, simply call the public initialization method
+ * (Theory::finishInitStandalone).
+ *
+ * (B) TheoryEngine, which determines how the Theory acts in accordance with
+ * its theory combination policy. We require the following steps in order:
+ * (B.1) Get information about whether the theory wishes to use an equality
+ * eninge, and more specifically which equality engine notifications the Theory
+ * would like to be notified of (Theory::needsEqualityEngine).
+ * (B.2) Set the equality engine of the theory (Theory::setEqualityEngine),
+ * which we refer to as the "official equality engine" of this Theory. The
+ * equality engine passed to the theory must respect the contract(s) specified
+ * by the equality engine setup information (EeSetupInfo) returned in the
+ * previous step.
+ * (B.3) Set the other required utilities including setQuantifiersEngine and
+ * setDecisionManager.
+ * (B.4) Call the private initialization method (Theory::finishInit).
+ *
+ * Initialization of the second form happens during TheoryEngine::finishInit,
+ * after the quantifiers engine and model objects have been set up.
*/
class Theory {
- private:
friend class ::CVC4::TheoryEngine;
+ private:
// Disallow default construction, copy, assignment.
Theory() = delete;
Theory(const Theory&) = delete;
/** An integer identifying the type of the theory. */
TheoryId d_id;
- /** Name of this theory instance. Along with the TheoryId this should provide
- * an unique string identifier for each instance of a Theory class. We need
- * this to ensure unique statistics names over multiple theory instances. */
- std::string d_instanceName;
-
/** The SAT search context for the Theory. */
context::Context* d_satContext;
DecisionManager* d_decManager;
protected:
+ /** Name of this theory instance. Along with the TheoryId this should provide
+ * an unique string identifier for each instance of a Theory class. We need
+ * this to ensure unique statistics names over multiple theory instances. */
+ std::string d_instanceName;
// === STATISTICS ===
/** time spent in check calls */
* theory engine (and other theories).
*/
Valuation d_valuation;
-
+ /**
+ * Pointer to the official equality engine of this theory, which is owned by
+ * the equality engine manager of TheoryEngine.
+ */
+ eq::EqualityEngine* d_equalityEngine;
+ /**
+ * The official equality engine, if we allocated it.
+ */
+ std::unique_ptr<eq::EqualityEngine> d_allocEqualityEngine;
/**
* Whether proofs are enabled
*
* its value must be computed (approximated) by the non-linear solver.
*/
bool isLegalElimination(TNode x, TNode val);
+ //--------------------------------- private initialization
+ /**
+ * Called to set the official equality engine. This should be done by
+ * TheoryEngine only.
+ */
+ void setEqualityEngine(eq::EqualityEngine* ee);
+ /** Called to set the quantifiers engine. */
+ void setQuantifiersEngine(QuantifiersEngine* qe);
+ /** Called to set the decision manager. */
+ void setDecisionManager(DecisionManager* dm);
+ /**
+ * Finish theory initialization. At this point, options and the logic
+ * setting are final, the master equality engine and quantifiers
+ * engine (if any) are initialized, and the official equality engine of this
+ * theory has been assigned. This base class implementation
+ * does nothing. This should be called by TheoryEngine only.
+ */
+ virtual void finishInit() {}
+ //--------------------------------- end private initialization
public:
//--------------------------------- initialization
/**
- * @return The theory rewriter associated with this theory. This is primarily
- * called for the purposes of initializing the rewriter.
+ * @return The theory rewriter associated with this theory.
*/
virtual TheoryRewriter* getTheoryRewriter() = 0;
/**
- * !!!! TODO: use this method (https://github.com/orgs/CVC4/projects/39).
- *
* Returns true if this theory needs an equality engine for checking
* satisfiability.
*
* a notifications class (eq::EqualityEngineNotify).
*/
virtual bool needsEqualityEngine(EeSetupInfo& esi);
+ /**
+ * Finish theory initialization, standalone version. This is used to
+ * initialize this class if it is not associated with a theory engine.
+ * This allocates the official equality engine of this Theory and then
+ * calls the finishInit method above.
+ */
+ void finishInitStandalone();
//--------------------------------- end initialization
/**
/** Get the decision manager associated to this theory. */
DecisionManager* getDecisionManager() { return d_decManager; }
- /**
- * Finish theory initialization. At this point, options and the logic
- * setting are final, and the master equality engine and quantifiers
- * engine (if any) are initialized. This base class implementation
- * does nothing.
- */
- virtual void finishInit() { }
-
/**
* Expand definitions in the term node. This returns a term that is
* equivalent to node. It wraps this term in a TrustNode of kind
virtual void addSharedTerm(TNode n) { }
/**
- * Called to set the master equality engine.
+ * Get the official equality engine of this theory.
*/
- virtual void setMasterEqualityEngine(eq::EqualityEngine* eq) { }
-
- /** Called to set the quantifiers engine. */
- void setQuantifiersEngine(QuantifiersEngine* qe);
- /** Called to set the decision manager. */
- void setDecisionManager(DecisionManager* dm);
+ eq::EqualityEngine* getEqualityEngine();
/**
* Return the current theory care graph. Theories should overload
*/
virtual std::pair<bool, Node> entailmentCheck(TNode lit);
- /* equality engine TODO: use? */
- virtual eq::EqualityEngine* getEqualityEngine() { return NULL; }
-
/* get current substitution at an effort
* input : vars
* output : subs, exp
#include "theory/bv/theory_bv_utils.h"
#include "theory/care_graph.h"
#include "theory/decision_manager.h"
+#include "theory/ee_manager_distributed.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/fmf/model_engine.h"
#include "theory/quantifiers/theory_quantifiers.h"
}
void TheoryEngine::finishInit() {
- //initialize the quantifiers engine, master equality engine, model, model builder
- if( d_logicInfo.isQuantified() ) {
+ // initialize the quantifiers engine
+ if (d_logicInfo.isQuantified())
+ {
// initialize the quantifiers engine
d_quantEngine = new QuantifiersEngine(d_context, d_userContext, this);
- Assert(d_masterEqualityEngine == 0);
- d_masterEqualityEngine = new eq::EqualityEngine(d_masterEENotify,getSatContext(), "theory::master", false);
+ }
- for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) {
- if (d_theoryTable[theoryId]) {
- d_theoryTable[theoryId]->setQuantifiersEngine(d_quantEngine);
- d_theoryTable[theoryId]->setMasterEqualityEngine(d_masterEqualityEngine);
- }
- }
+ // Initialize the equality engine architecture for all theories, which
+ // includes the master equality engine.
+ d_eeDistributed.reset(new EqEngineManagerDistributed(*this));
+ d_eeDistributed->finishInit();
+ // Initialize the model and model builder.
+ if (d_logicInfo.isQuantified())
+ {
d_curr_model_builder = d_quantEngine->getModelBuilder();
d_curr_model = d_quantEngine->getModel();
} else {
d_userContext, "DefaultModel", options::assignFunctionValues());
d_aloc_curr_model = true;
}
+
//make the default builder, e.g. in the case that the quantifiers engine does not have a model builder
if( d_curr_model_builder==NULL ){
d_curr_model_builder = new theory::TheoryEngineModelBuilder(this);
d_aloc_curr_model_builder = true;
}
+ // finish initializing the theories
for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) {
- if (d_theoryTable[theoryId]) {
- // set the decision manager for the theory
- d_theoryTable[theoryId]->setDecisionManager(d_decManager.get());
- // finish initializing the theory
- d_theoryTable[theoryId]->finishInit();
+ Theory* t = d_theoryTable[theoryId];
+ if (t == nullptr)
+ {
+ continue;
}
- }
-}
-
-void TheoryEngine::eqNotifyNewClass(TNode t){
- if (d_logicInfo.isQuantified()) {
- d_quantEngine->eqNotifyNewClass( t );
+ // setup the pointers to the utilities
+ const EeTheoryInfo* eeti = d_eeDistributed->getEeTheoryInfo(theoryId);
+ Assert(eeti != nullptr);
+ // the theory's official equality engine is the one specified by the
+ // equality engine manager
+ t->setEqualityEngine(eeti->d_usedEe);
+ // set the quantifiers engine
+ t->setQuantifiersEngine(d_quantEngine);
+ // set the decision manager for the theory
+ t->setDecisionManager(d_decManager.get());
+ // finish initializing the theory
+ t->finishInit();
}
}
d_userContext(userContext),
d_logicInfo(logicInfo),
d_sharedTerms(this, context),
- d_masterEqualityEngine(nullptr),
- d_masterEENotify(*this),
+ d_eeDistributed(nullptr),
d_quantEngine(nullptr),
d_decManager(new DecisionManager(userContext)),
d_curr_model(nullptr),
delete d_quantEngine;
- delete d_masterEqualityEngine;
-
smtStatisticsRegistry()->unregisterStat(&d_combineTheoriesTime);
smtStatisticsRegistry()->unregisterStat(&d_arithSubstitutionsAdded);
}
Debug("theory") << ", need check = " << (needCheck() ? "YES" : "NO") << endl;
if( Theory::fullEffort(effort) && !d_inConflict && !needCheck()) {
- // case where we are about to answer SAT
- if( d_masterEqualityEngine != NULL ){
- AlwaysAssert(d_masterEqualityEngine->consistent());
+ // case where we are about to answer SAT, the master equality engine,
+ // if it exists, must be consistent.
+ eq::EqualityEngine* mee = getMasterEqualityEngine();
+ if (mee != NULL)
+ {
+ AlwaysAssert(mee->consistent());
}
if (d_curr_model->isBuilt())
{
}
}
+SharedTermsDatabase* TheoryEngine::getSharedTermsDatabase()
+{
+ return &d_sharedTerms;
+}
+
+theory::eq::EqualityEngine* TheoryEngine::getMasterEqualityEngine()
+{
+ Assert(d_eeDistributed != nullptr);
+ return d_eeDistributed->getMasterEqualityEngine();
+}
+
void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector, LemmaProofRecipe* proofRecipe) {
Assert(explanationVector.size() > 0);
namespace theory {
class TheoryModel;
class TheoryEngineModelBuilder;
+ class EqEngineManagerDistributed;
namespace eq {
class EqualityEngine;
SharedTermsDatabase d_sharedTerms;
/**
- * Master equality engine, to share with theories.
+ * The distributed equality manager. This class is responsible for
+ * configuring the theories of this class for handling equalties
+ * in a "distributed" fashion, i.e. each theory maintains a unique
+ * instance of an equality engine. These equality engines are memory
+ * managed by this class.
*/
- theory::eq::EqualityEngine* d_masterEqualityEngine;
-
- /** notify class for master equality engine */
- class NotifyClass : public theory::eq::EqualityEngineNotify {
- TheoryEngine& d_te;
- public:
- NotifyClass(TheoryEngine& te): d_te(te) {}
- bool eqNotifyTriggerEquality(TNode equality, bool value) override
- {
- return true;
- }
- bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
- {
- return true;
- }
- bool eqNotifyTriggerTermEquality(theory::TheoryId tag,
- TNode t1,
- TNode t2,
- bool value) override
- {
- return true;
- }
- void eqNotifyConstantTermMerge(TNode t1, TNode t2) override {}
- void eqNotifyNewClass(TNode t) override { d_te.eqNotifyNewClass(t); }
- void eqNotifyMerge(TNode t1, TNode t2) override {}
- void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override
- {
- }
- };/* class TheoryEngine::NotifyClass */
- NotifyClass d_masterEENotify;
-
- /**
- * notification methods
- */
- void eqNotifyNewClass(TNode t);
+ std::unique_ptr<theory::EqEngineManagerDistributed> d_eeDistributed;
/**
* The quantifiers engine
d_propEngine = propEngine;
}
- /** Called when all initialization of options/logic is done */
+ /**
+ * Called when all initialization of options/logic is done, after theory
+ * objects have been created.
+ *
+ * This initializes the quantifiers engine, the "official" equality engines
+ * of each theory as required, and the model and model builder utilities.
+ */
void finishInit();
/**
public:
void staticInitializeBVOptions(const std::vector<Node>& assertions);
- Node ppSimpITE(TNode assertion);
- /** Returns false if an assertion simplified to false. */
- bool donePPSimpITE(std::vector<Node>& assertions);
-
- SharedTermsDatabase* getSharedTermsDatabase() { return &d_sharedTerms; }
+ SharedTermsDatabase* getSharedTermsDatabase();
- theory::eq::EqualityEngine* getMasterEqualityEngine() { return d_masterEqualityEngine; }
+ theory::eq::EqualityEngine* getMasterEqualityEngine();
SortInference* getSortInference() { return &d_sortInfer; }
* so make sure it's initialized first. */
d_thss(nullptr),
d_ho(nullptr),
- d_equalityEngine(d_notify, c, instanceName + "theory::uf::ee", true),
d_conflict(c, false),
d_functionsTerms(c),
d_symb(u, instanceName)
{
d_true = NodeManager::currentNM()->mkConst( true );
- // The kinds we are treating as function application in congruence
- d_equalityEngine.addFunctionKind(kind::APPLY_UF, false, options::ufHo());
-
ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr;
if (pc != nullptr)
{
TheoryUF::~TheoryUF() {
}
-void TheoryUF::setMasterEqualityEngine(eq::EqualityEngine* eq) {
- d_equalityEngine.setMasterEqualityEngine(eq);
+TheoryRewriter* TheoryUF::getTheoryRewriter() { return &d_rewriter; }
+
+bool TheoryUF::needsEqualityEngine(EeSetupInfo& esi)
+{
+ esi.d_notify = &d_notify;
+ esi.d_name = d_instanceName + "theory::uf::ee";
+ return true;
}
void TheoryUF::finishInit() {
+ Assert(d_equalityEngine != nullptr);
// combined cardinality constraints are not evaluated in getModelValue
d_valuation.setUnevaluatedKind(kind::COMBINED_CARDINALITY_CONSTRAINT);
// Initialize the cardinality constraints solver if the logic includes UF,
d_thss.reset(new CardinalityExtension(
getSatContext(), getUserContext(), *d_out, this));
}
+ // The kinds we are treating as function application in congruence
+ d_equalityEngine->addFunctionKind(kind::APPLY_UF, false, options::ufHo());
if (options::ufHo())
{
- d_equalityEngine.addFunctionKind(kind::HO_APPLY);
+ d_equalityEngine->addFunctionKind(kind::HO_APPLY);
d_ho.reset(new HoExtension(*this, getSatContext(), getUserContext()));
}
}
bool polarity = fact.getKind() != kind::NOT;
TNode atom = polarity ? fact : fact[0];
if (atom.getKind() == kind::EQUAL) {
- d_equalityEngine.assertEquality(atom, polarity, fact);
+ d_equalityEngine->assertEquality(atom, polarity, fact);
if( options::ufHo() && options::ufHoExt() ){
if( !polarity && !d_conflict && atom[0].getType().isFunction() ){
// apply extensionality eagerly using the ho extension
}
//needed for models
if( options::produceModels() ){
- d_equalityEngine.assertPredicate(atom, polarity, fact);
+ d_equalityEngine->assertPredicate(atom, polarity, fact);
}
} else {
- d_equalityEngine.assertPredicate(atom, polarity, fact);
+ d_equalityEngine->assertPredicate(atom, polarity, fact);
}
}
if( node.getKind()==kind::APPLY_UF ){
return node.getOperator();
}else{
- return d_equalityEngine.getRepresentative( node[0] );
+ return d_equalityEngine->getRepresentative(node[0]);
}
}
switch (node.getKind()) {
case kind::EQUAL:
// Add the trigger for equality
- d_equalityEngine.addTriggerEquality(node);
+ d_equalityEngine->addTriggerEquality(node);
break;
case kind::APPLY_UF:
case kind::HO_APPLY:
// Maybe it's a predicate
if (node.getType().isBoolean()) {
// Get triggered for both equal and dis-equal
- d_equalityEngine.addTriggerPredicate(node);
+ d_equalityEngine->addTriggerPredicate(node);
} else {
// Function applications/predicates
- d_equalityEngine.addTerm(node);
+ d_equalityEngine->addTerm(node);
}
// Remember the function and predicate terms
d_functionsTerms.push_back(node);
break;
default:
// Variables etc
- d_equalityEngine.addTerm(node);
+ d_equalityEngine->addTerm(node);
break;
}
}/* TheoryUF::preRegisterTerm() */
bool polarity = literal.getKind() != kind::NOT;
TNode atom = polarity ? literal : literal[0];
if (atom.getKind() == kind::EQUAL) {
- d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions, pf);
+ d_equalityEngine->explainEquality(
+ atom[0], atom[1], polarity, assumptions, pf);
} else {
- d_equalityEngine.explainPredicate(atom, polarity, assumptions, pf);
+ d_equalityEngine->explainPredicate(atom, polarity, assumptions, pf);
}
if( pf ){
Debug("pf::uf") << std::endl;
// Compute terms appearing in assertions and shared terms
computeRelevantTerms(termSet);
- if (!m->assertEqualityEngine(&d_equalityEngine, &termSet))
+ if (!m->assertEqualityEngine(d_equalityEngine, &termSet))
{
Trace("uf") << "Collect model info fail UF" << std::endl;
return false;
EqualityStatus TheoryUF::getEqualityStatus(TNode a, TNode b) {
// Check for equality (simplest)
- if (d_equalityEngine.areEqual(a, b)) {
+ if (d_equalityEngine->areEqual(a, b))
+ {
// The terms are implied to be equal
return EQUALITY_TRUE;
}
// Check for disequality
- if (d_equalityEngine.areDisequal(a, b, false)) {
+ if (d_equalityEngine->areDisequal(a, b, false))
+ {
// The terms are implied to be dis-equal
return EQUALITY_FALSE;
}
void TheoryUF::addSharedTerm(TNode t) {
Debug("uf::sharing") << "TheoryUF::addSharedTerm(" << t << ")" << std::endl;
- d_equalityEngine.addTriggerTerm(t, THEORY_UF);
+ d_equalityEngine->addTriggerTerm(t, THEORY_UF);
}
bool TheoryUF::areCareDisequal(TNode x, TNode y){
- Assert(d_equalityEngine.hasTerm(x));
- Assert(d_equalityEngine.hasTerm(y));
- if( d_equalityEngine.isTriggerTerm(x, THEORY_UF) && d_equalityEngine.isTriggerTerm(y, THEORY_UF) ){
- TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_UF);
- TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_UF);
+ Assert(d_equalityEngine->hasTerm(x));
+ Assert(d_equalityEngine->hasTerm(y));
+ if (d_equalityEngine->isTriggerTerm(x, THEORY_UF)
+ && d_equalityEngine->isTriggerTerm(y, THEORY_UF))
+ {
+ TNode x_shared =
+ d_equalityEngine->getTriggerTermRepresentative(x, THEORY_UF);
+ TNode y_shared =
+ d_equalityEngine->getTriggerTermRepresentative(y, THEORY_UF);
EqualityStatus eqStatus = d_valuation.getEqualityStatus(x_shared, y_shared);
if( eqStatus==EQUALITY_FALSE_AND_PROPAGATED || eqStatus==EQUALITY_FALSE || eqStatus==EQUALITY_FALSE_IN_MODEL ){
return true;
if( t2!=NULL ){
Node f1 = t1->getData();
Node f2 = t2->getData();
- if( !d_equalityEngine.areEqual( f1, f2 ) ){
+ if (!d_equalityEngine->areEqual(f1, f2))
+ {
Debug("uf::sharing") << "TheoryUf::computeCareGraph(): checking function " << f1 << " and " << f2 << std::endl;
vector< pair<TNode, TNode> > currentPairs;
unsigned arg_start_index = getArgumentStartIndexForApplyTerm( f1 );
for (unsigned k = arg_start_index; k < f1.getNumChildren(); ++ k) {
TNode x = f1[k];
TNode y = f2[k];
- Assert(d_equalityEngine.hasTerm(x));
- Assert(d_equalityEngine.hasTerm(y));
- Assert(!d_equalityEngine.areDisequal(x, y, false));
+ Assert(d_equalityEngine->hasTerm(x));
+ Assert(d_equalityEngine->hasTerm(y));
+ Assert(!d_equalityEngine->areDisequal(x, y, false));
Assert(!areCareDisequal(x, y));
- if( !d_equalityEngine.areEqual( x, y ) ){
- if( d_equalityEngine.isTriggerTerm(x, THEORY_UF) && d_equalityEngine.isTriggerTerm(y, THEORY_UF) ){
- TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_UF);
- TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_UF);
+ if (!d_equalityEngine->areEqual(x, y))
+ {
+ if (d_equalityEngine->isTriggerTerm(x, THEORY_UF)
+ && d_equalityEngine->isTriggerTerm(y, THEORY_UF))
+ {
+ TNode x_shared =
+ d_equalityEngine->getTriggerTermRepresentative(x, THEORY_UF);
+ TNode y_shared =
+ d_equalityEngine->getTriggerTermRepresentative(y, THEORY_UF);
currentPairs.push_back(make_pair(x_shared, y_shared));
}
}
std::map<TNode, TNodeTrie>::iterator it2 = it;
++it2;
for( ; it2 != t1->d_data.end(); ++it2 ){
- if( !d_equalityEngine.areDisequal(it->first, it2->first, false) ){
+ if (!d_equalityEngine->areDisequal(it->first, it2->first, false))
+ {
if( !areCareDisequal(it->first, it2->first) ){
addCarePairs( &it->second, &it2->second, arity, depth+1 );
}
{
for (std::pair<const TNode, TNodeTrie>& tt2 : t2->d_data)
{
- if (!d_equalityEngine.areDisequal(tt1.first, tt2.first, false))
+ if (!d_equalityEngine->areDisequal(tt1.first, tt2.first, false))
{
if (!areCareDisequal(tt1.first, tt2.first))
{
std::vector< TNode > reps;
bool has_trigger_arg = false;
for( unsigned j=arg_start_index; j<f1.getNumChildren(); j++ ){
- reps.push_back( d_equalityEngine.getRepresentative( f1[j] ) );
- if( d_equalityEngine.isTriggerTerm( f1[j], THEORY_UF ) ){
+ reps.push_back(d_equalityEngine->getRepresentative(f1[j]));
+ if (d_equalityEngine->isTriggerTerm(f1[j], THEORY_UF))
+ {
has_trigger_arg = true;
}
}
/** the higher-order solver extension (or nullptr if it does not exist) */
std::unique_ptr<HoExtension> d_ho;
- /** Equaltity engine */
- eq::EqualityEngine d_equalityEngine;
-
/** Are we in conflict */
context::CDO<bool> d_conflict;
~TheoryUF();
- TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
-
- void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
+ //--------------------------------- initialization
+ /** get the official theory rewriter of this theory */
+ TheoryRewriter* getTheoryRewriter() override;
+ /**
+ * Returns true if we need an equality engine. If so, we initialize the
+ * information regarding how it should be setup. For details, see the
+ * documentation in Theory::needsEqualityEngine.
+ */
+ bool needsEqualityEngine(EeSetupInfo& esi) override;
+ /** finish initialization */
void finishInit() override;
+ //--------------------------------- end initialization
void check(Effort) override;
TrustNode expandDefinition(Node node) override;
std::string identify() const override { return "THEORY_UF"; }
- eq::EqualityEngine* getEqualityEngine() override { return &d_equalityEngine; }
-
/** get a pointer to the uf with cardinality */
CardinalityExtension* getCardinalityExtension() const { return d_thss.get(); }
/** are we in conflict? */
projects / cvc5.git / commitdiff