Searched refs:d_masterEqualityEngine (Results 1 – 4 of 4) sorted by relevance
107 , d_masterEqualityEngine(0) in EqualityEngine()132 , d_masterEqualityEngine(0) in EqualityEngine()156 Assert(d_masterEqualityEngine == 0); in setMasterEqualityEngine()157 d_masterEqualityEngine = master; in setMasterEqualityEngine()361 if (d_masterEqualityEngine && !d_isInternal[result]) { in addTermInternal()362 d_masterEqualityEngine->addTermInternal(t); in addTermInternal()1584 if (d_masterEqualityEngine && !d_isInternal[t1classId] && !d_isInternal[t2classId]) { in propagate()1585 …d_masterEqualityEngine->assertEqualityInternal(d_nodes[t1classId], d_nodes[t2classId], TNode::null… in propagate()1586 d_masterEqualityEngine->propagate(); in propagate()
186 EqualityEngine* d_masterEqualityEngine; variable
151 theory::eq::EqualityEngine* d_masterEqualityEngine; variable884 theory::eq::EqualityEngine* getMasterEqualityEngine() { return d_masterEqualityEngine; } in getMasterEqualityEngine()
224 Assert(d_masterEqualityEngine == 0); in finishInit()225 …d_masterEqualityEngine = new eq::EqualityEngine(d_masterEENotify,getSatContext(), "theory::master"… in finishInit()230 d_theoryTable[theoryId]->setMasterEqualityEngine(d_masterEqualityEngine); in finishInit()292 d_masterEqualityEngine(nullptr), in TheoryEngine()365 delete d_masterEqualityEngine; in ~TheoryEngine()640 if( d_masterEqualityEngine != NULL ){ in check()641 AlwaysAssert(d_masterEqualityEngine->consistent()); in check()