| /dports/math/cvc4/CVC4-1.7/src/theory/bv/ |
| H A D | bv_subtheory_core.h | 58 bool eqNotifyTriggerTermEquality(TheoryId tag,
|
| H A D | bv_subtheory_core.cpp | 387 bool CoreSolver::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool va… in eqNotifyTriggerTermEquality() function in CoreSolver::NotifyClass
|
| /dports/math/cvc4/CVC4-1.7/src/theory/fp/ |
| H A D | theory_fp.h | 70 bool eqNotifyTriggerTermEquality(TheoryId tag,
|
| H A D | theory_fp.cpp | 1176 bool TheoryFp::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, in eqNotifyTriggerTermEquality() function in CVC4::theory::fp::TheoryFp::NotifyClass
|
| /dports/math/cvc4/CVC4-1.7/src/theory/arith/ |
| H A D | congruence_manager.h | 68 bool eqNotifyTriggerTermEquality(TheoryId tag,
|
| H A D | congruence_manager.cpp | 106 bool ArithCongruenceManager::ArithCongruenceNotify::eqNotifyTriggerTermEquality(TheoryId tag, TNode… in eqNotifyTriggerTermEquality() function in CVC4::theory::arith::ArithCongruenceManager::ArithCongruenceNotify
|
| /dports/math/cvc4/CVC4-1.7/src/theory/ |
| H A D | shared_terms_database.h | 93 bool eqNotifyTriggerTermEquality(theory::TheoryId tag, in eqNotifyTriggerTermEquality() function
|
| H A D | theory_engine.h | 166 bool eqNotifyTriggerTermEquality(theory::TheoryId tag, in eqNotifyTriggerTermEquality() function
|
| /dports/math/cvc4/CVC4-1.7/src/theory/uf/ |
| H A D | equality_engine.h | 83 virtual bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) = 0;
142 bool eqNotifyTriggerTermEquality(TheoryId tag, in eqNotifyTriggerTermEquality() function
|
| H A D | theory_uf.h | 71 bool eqNotifyTriggerTermEquality(TheoryId tag, in eqNotifyTriggerTermEquality() function
|
| H A D | equality_engine.cpp | 508 … if (!d_notify.eqNotifyTriggerTermEquality(aTag, d_nodes[aSharedId], d_nodes[bSharedId], false)) { in assertEquality()
727 … if (!d_notify.eqNotifyTriggerTermEquality(tag1, d_nodes[tag1id], d_nodes[tag2id], true)) { in merge()
1777 …if (eqNodeId != triggerId && !d_notify.eqNotifyTriggerTermEquality(tag, t, d_nodes[triggerId], tru… in addTriggerTerm()
2124 … if (!d_notify.eqNotifyTriggerTermEquality(currentTag, d_nodes[myRep], d_nodes[tagRep], false)) { in propagateTriggerTermDisequalities()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/sep/ |
| H A D | theory_sep.h | 158 bool eqNotifyTriggerTermEquality(TheoryId tag, in eqNotifyTriggerTermEquality() function
|
| /dports/math/cvc4/CVC4-1.7/src/theory/sets/ |
| H A D | theory_sets_private.h | 294 bool eqNotifyTriggerTermEquality(TheoryId tag,
|
| H A D | theory_sets_private.cpp | 2311 bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, … in eqNotifyTriggerTermEquality() function in CVC4::theory::sets::TheorySetsPrivate::NotifyClass
|
| /dports/math/cvc4/CVC4-1.7/src/theory/arrays/ |
| H A D | theory_arrays.h | 301 bool eqNotifyTriggerTermEquality(TheoryId tag, in eqNotifyTriggerTermEquality() function
|
| /dports/math/cvc4/CVC4-1.7/src/theory/datatypes/ |
| H A D | theory_datatypes.h | 79 bool eqNotifyTriggerTermEquality(TheoryId tag, in eqNotifyTriggerTermEquality() function
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/ |
| H A D | conjecture_generator.h | 257 bool eqNotifyTriggerTermEquality(TheoryId tag, in eqNotifyTriggerTermEquality() function
|
| /dports/math/cvc4/CVC4-1.7/src/theory/strings/ |
| H A D | theory_strings.h | 200 bool eqNotifyTriggerTermEquality(TheoryId tag, in eqNotifyTriggerTermEquality() function
|