| /dports/math/cvc4/CVC4-1.7/src/theory/uf/ |
| H A D | equality_engine.cpp | 38 EqualityEngine::Statistics::~Statistics() { in ~Statistics()
76 void EqualityEngine::init() { in init()
100 EqualityEngine::~EqualityEngine() { in ~EqualityEngine()
105 EqualityEngine::EqualityEngine(context::Context* context, std::string name, bool constantsAreTrigge… in EqualityEngine() function in CVC4::theory::eq::EqualityEngine
155 void EqualityEngine::setMasterEqualityEngine(EqualityEngine* master) { in setMasterEqualityEngine()
373 bool EqualityEngine::hasTerm(TNode t) const { in hasTerm()
784 void EqualityEngine::backtrack() { in backtrack()
1471 void EqualityEngine::propagate() { in propagate()
1631 void EqualityEngine::debugPrintGraph() const { in debugPrintGraph()
1683 EqualityEngine* nonConst = const_cast<EqualityEngine*>(this); in areDisequal()
[all …]
|
| H A D | equality_engine.h | 53 friend class EqualityEngine; variable
174 class EqualityEngine : public context::ContextNotifyObj {
186 EqualityEngine* d_masterEqualityEngine;
193 …EqualityEngine(EqualityEngineNotify& notify, context::Context* context, std::string name, bool con…
198 EqualityEngine(context::Context* context, std::string name, bool constantsAreTriggers);
203 virtual ~EqualityEngine();
209 void setMasterEqualityEngine(EqualityEngine* master);
898 const eq::EqualityEngine* d_ee;
902 EqClassesIterator(const eq::EqualityEngine* ee);
915 const eq::EqualityEngine* d_ee;
[all …]
|
| H A D | theory_uf.h | 125 eq::EqualityEngine d_equalityEngine;
279 void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
301 eq::EqualityEngine* getEqualityEngine() override { return &d_equalityEngine; } in getEqualityEngine()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/ |
| H A D | equality_query.cpp | 49 eq::EqualityEngine* ee = getEngine(); in processInferences()
89 eq::EqualityEngine* ee = getEngine(); in getRepresentative()
101 eq::EqualityEngine* ee = getEngine(); in areEqual()
114 eq::EqualityEngine* ee = getEngine(); in areDisequal()
213 eq::EqualityEngine* EqualityQueryQuantifiersEngine::getEngine(){ in getEngine()
218 eq::EqualityEngine* ee = getEngine(); in getEquivalenceClass()
|
| H A D | quant_util.h | 141 eq::EqualityEngine * getEqualityEngine();
229 virtual eq::EqualityEngine* getEngine() = 0;
|
| H A D | dynamic_rewrite.h | 115 eq::EqualityEngine d_equalityEngine;
|
| H A D | equality_query.h | 70 eq::EqualityEngine* getEngine() override;
|
| /dports/math/cvc4/CVC4-1.7/src/theory/arrays/ |
| H A D | array_proof_reconstruction.h | 34 ArrayProofReconstruction(const eq::EqualityEngine* equalityEngine);
52 const eq::EqualityEngine* d_equalityEngine;
|
| H A D | theory_arrays.h | 147 void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
168 eq::EqualityEngine d_ppEqualityEngine;
227 eq::EqualityEngine d_mayEqualEqualityEngine;
347 eq::EqualityEngine d_equalityEngine;
486 eq::EqualityEngine* getEqualityEngine() override { return &d_equalityEngine; } in getEqualityEngine()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/bv/ |
| H A D | bv_subtheory_core.h | 74 eq::EqualityEngine d_equalityEngine;
107 void setMasterEqualityEngine(eq::EqualityEngine* eq);
132 eq::EqualityEngine * getEqualityEngine() { return &d_equalityEngine; } in getEqualityEngine()
|
| H A D | theory_bv.h | 75 void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
96 eq::EqualityEngine* getEqualityEngine() override;
|
| /dports/math/cvc4/CVC4-1.7/src/theory/ |
| H A D | theory_model.h | 122 bool assertEqualityEngine(const eq::EqualityEngine* ee,
220 eq::EqualityEngine* getEqualityEngine() { return d_equalityEngine; } in getEqualityEngine()
291 eq::EqualityEngine* d_equalityEngine;
|
| H A D | shared_terms_database.h | 116 theory::eq::EqualityEngine d_equalityEngine;
248 theory::eq::EqualityEngine* getEqualityEngine() { return &d_equalityEngine; } in getEqualityEngine()
|
| H A D | theory.h | 67 class EqualityEngine; variable
468 virtual void setMasterEqualityEngine(eq::EqualityEngine* eq) { } in setMasterEqualityEngine()
823 virtual eq::EqualityEngine* getEqualityEngine() { return NULL; } in getEqualityEngine()
|
| H A D | theory_engine.h | 90 class EqualityEngine; variable
151 theory::eq::EqualityEngine* d_masterEqualityEngine;
884 theory::eq::EqualityEngine* getMasterEqualityEngine() { return d_masterEqualityEngine; } in getMasterEqualityEngine()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/arith/ |
| H A D | congruence_manager.h | 105 eq::EqualityEngine d_ee;
118 void setMasterEqualityEngine(eq::EqualityEngine* eq);
183 eq::EqualityEngine * getEqualityEngine() { return &d_ee; } in getEqualityEngine()
|
| H A D | theory_arith.h | 61 void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
|
| /dports/math/cvc4/CVC4-1.7/src/theory/fp/ |
| H A D | theory_fp.h | 56 void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
83 eq::EqualityEngine d_equalityEngine;
|
| /dports/math/cvc4/CVC4-1.7/test/regress/regress0/ |
| H A D | bug382.smt2 | 13 (get-value ((f x))); assert-fails in EqualityEngine
|
| /dports/math/cvc4/CVC4-1.7/src/theory/sep/ |
| H A D | theory_sep.h | 69 void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
201 eq::EqualityEngine d_equalityEngine;
325 eq::EqualityEngine* getEqualityEngine() override { return &d_equalityEngine; } in getEqualityEngine()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/datatypes/ |
| H A D | theory_datatypes.h | 154 eq::EqualityEngine d_equalityEngine;
266 void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
306 eq::EqualityEngine* getEqualityEngine() override { return &d_equalityEngine; } in getEqualityEngine()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/sets/ |
| H A D | theory_sets.h | 59 void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
|
| H A D | theory_sets_rels.h | 56 eq::EqualityEngine*,
91 eq::EqualityEngine *d_eqEngine;
|
| H A D | theory_sets.cpp | 100 void TheorySets::setMasterEqualityEngine(eq::EqualityEngine* eq) { in setMasterEqualityEngine()
|
| /dports/math/cvc4/CVC4-1.7/test/regress/regress0/rewriterules/ |
| H A D | native_arrays.smt2 | 2 ;; This example can't be done if we don't access the EqualityEngine of
|