| /dports/math/cvc4/CVC4-1.7/src/theory/uf/ |
| H A D | equality_engine.h | 45 class EqClassIterator; variable
177 friend class EqClassIterator; variable
914 class EqClassIterator {
921 EqClassIterator();
922 EqClassIterator(Node eqc, const eq::EqualityEngine* ee);
924 bool operator==(const EqClassIterator& i) const;
925 bool operator!=(const EqClassIterator& i) const;
926 EqClassIterator& operator++();
927 EqClassIterator operator++(int);
|
| H A D | equality_engine.cpp | 2180 EqClassIterator::EqClassIterator() in EqClassIterator() function in CVC4::theory::eq::EqClassIterator
2186 EqClassIterator::EqClassIterator(Node eqc, const eq::EqualityEngine* ee) in EqClassIterator() function in CVC4::theory::eq::EqClassIterator
2195 Node EqClassIterator::operator*() const { in operator *()
2199 bool EqClassIterator::operator==(const EqClassIterator& i) const { in operator ==()
2203 bool EqClassIterator::operator!=(const EqClassIterator& i) const { in operator !=()
2207 EqClassIterator& EqClassIterator::operator++() { in operator ++()
2228 EqClassIterator EqClassIterator::operator++(int) { in operator ++()
2229 EqClassIterator i = *this; in operator ++()
2234 bool EqClassIterator::isFinished() const { in isFinished()
|
| H A D | theory_uf.cpp | 899 eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); in checkAppCompletion()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/ |
| H A D | theory_model_builder.cpp | 322 eq::EqClassIterator eqc_i = in buildModel()
323 eq::EqClassIterator((*eqcs_i), tm->d_equalityEngine); in buildModel()
383 eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, tm->d_equalityEngine); in buildModel()
488 eq::EqClassIterator eqc_i = in buildModel()
489 eq::EqClassIterator(*i2, tm->d_equalityEngine); in buildModel()
655 eq::EqClassIterator eqc_i = in buildModel()
656 eq::EqClassIterator(*i2, tm->d_equalityEngine); in buildModel()
863 eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, tm->d_equalityEngine); in debugCheckModel()
|
| H A D | theory_model.cpp | 430 eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, ee); in assertEqualityEngine()
591 eq::EqClassIterator eqc_i = eq::EqClassIterator(r,d_equalityEngine); in assignFunctionDefinition()
|
| H A D | quantifiers_engine.cpp | 1274 eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee ); in debugPrintEqualityEngine()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/ematching/ |
| H A D | candidate_generator.h | 110 eq::EqClassIterator d_eqc_iter;
152 eq::EqClassIterator d_eqc_false;
|
| H A D | candidate_generator.cpp | 64 d_eqc_iter = eq::EqClassIterator( rep, ee ); in reset()
140 d_eqc_false = eq::EqClassIterator( false_term, d_qe->getEqualityQuery()->getEngine() ); in reset()
|
| H A D | inst_match_generator.cpp | 949 eq::EqClassIterator eqc( in processNewInstantiations()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/ |
| H A D | term_database.cpp | 822 eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee ); in getEligibleTermInEqc()
915 eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee ); in reset()
962 eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee ); in reset()
|
| H A D | inst_match_trie.cpp | 58 eq::EqClassIterator eqc( in addInstMatch()
312 eq::EqClassIterator eqc( in addInstMatch()
|
| H A D | equality_query.cpp | 221 eq::EqClassIterator eqc_iter( rep, ee ); in getEquivalenceClass()
|
| H A D | conjecture_generator.cpp | 397 eq::EqClassIterator ieqc_i = eq::EqClassIterator( r, ee ); in check()
458 eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee ); in check()
837 eq::EqClassIterator ueqc_i = eq::EqClassIterator( r, &d_uequalityEngine ); in check()
|
| H A D | quant_conflict_find.cpp | 2133 eq::EqClassIterator eqc_i = eq::EqClassIterator( n, getEqualityEngine() ); in debugPrint()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/arrays/ |
| H A D | theory_arrays.cpp | 611 eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, &d_mayEqualEqualityEngine); in checkWeakEquiv()
1076 eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, &d_equalityEngine); in collectModelInfo()
1102 eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, &d_equalityEngine); in collectModelInfo()
1109 eq::EqClassIterator array_eqc_i = eq::EqClassIterator(array_eqc, &d_equalityEngine); in collectModelInfo()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/cegqi/ |
| H A D | ceg_instantiator.cpp | 1295 eq::EqClassIterator eqc_i = eq::EqClassIterator( pvr, ee ); in processAssertions()
1355 eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee ); in processAssertions()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/bv/ |
| H A D | bv_subtheory_core.cpp | 229 eq::EqClassIterator it(repr, &d_equalityEngine); in buildModel()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/strings/ |
| H A D | theory_strings.cpp | 979 eq::EqClassIterator eqc2_i = eq::EqClassIterator( eqc, &d_equalityEngine ); in check()
1397 eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); in checkInit()
2399 eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); in checkCycles()
2469 eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); in checkNormalFormsEq()
2707 eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); in getNormalForms()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/datatypes/ |
| H A D | theory_datatypes.cpp | 2158 eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); in printModelDebug()
2232 eq::EqClassIterator eqc_i = eq::EqClassIterator(r, &d_equalityEngine); in getRelevantTerms()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/sep/ |
| H A D | theory_sep.cpp | 622 eq::EqClassIterator eqc2_i = eq::EqClassIterator( eqc, &d_equalityEngine ); in check()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/sets/ |
| H A D | theory_sets_rels.cpp | 155 eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc_rep, d_eqEngine ); in collectRelsInfo()
|
| H A D | theory_sets_private.cpp | 553 eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); in fullEffortCheck()
|