| /dports/math/cvc4/CVC4-1.7/src/theory/arrays/ |
| H A D | theory_arrays.cpp | 605 eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(&d_mayEqualEqualityEngine); in checkWeakEquiv() local
606 for (; !eqcs_i.isFinished(); ++eqcs_i) { in checkWeakEquiv()
607 Node eqc = (*eqcs_i); in checkWeakEquiv()
1068 eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(&d_equalityEngine); in collectModelInfo() local
1069 for (; !eqcs_i.isFinished(); ++eqcs_i) { in collectModelInfo()
1070 Node eqc = (*eqcs_i); in collectModelInfo()
1099 eqcs_i = eq::EqClassesIterator(&d_equalityEngine); in collectModelInfo()
1100 for (; !eqcs_i.isFinished(); ++eqcs_i) { in collectModelInfo()
1101 Node eqc = (*eqcs_i); in collectModelInfo()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/bv/ |
| H A D | bv_subtheory_core.cpp | 222 eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(&d_equalityEngine); in buildModel() local
223 while (!eqcs_i.isFinished()) in buildModel()
225 TNode repr = *eqcs_i; in buildModel()
236 ++eqcs_i; in buildModel()
241 eqcs_i = eq::EqClassesIterator(&d_equalityEngine); in buildModel()
242 while (!eqcs_i.isFinished()) in buildModel()
244 TNode repr = *eqcs_i; in buildModel()
245 ++eqcs_i; in buildModel()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/datatypes/ |
| H A D | theory_datatypes.cpp | 195 Node n = (*eqcs_i); in check()
333 ++eqcs_i; in check()
1805 while( !eqcs_i.isFinished() ){ in checkCycles()
1806 Node eqc = (*eqcs_i); in checkCycles()
1842 ++eqcs_i; in checkCycles()
2149 while( !eqcs_i.isFinished() ){ in printModelDebug()
2150 Node eqc = (*eqcs_i); in printModelDebug()
2199 ++eqcs_i; in printModelDebug()
2225 while( !eqcs_i.isFinished() ){ in getRelevantTerms()
2226 TNode r = (*eqcs_i); in getRelevantTerms()
[all …]
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/cegqi/ |
| H A D | ceg_instantiator.cpp | 1340 eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); in processAssertions() local
1341 while( !eqcs_i.isFinished() ){ in processAssertions()
1342 Node r = *eqcs_i; in processAssertions()
1364 ++eqcs_i; in processAssertions()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/ |
| H A D | conjecture_generator.cpp | 379 eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); in check() local
380 while( !eqcs_i.isFinished() ){ in check()
381 TNode r = (*eqcs_i); in check()
409 ++eqcs_i; in check()
|
| H A D | local_theory_ext.cpp | 151 eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); in reset() local
152 while( !eqcs_i.isFinished() ){ in reset()
153 TNode r = (*eqcs_i); in reset()
156 ++eqcs_i; in reset()
|
| H A D | quant_conflict_find.cpp | 2107 eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( getEqualityEngine() ); in computeRelevantEqr() local
2108 while( !eqcs_i.isFinished() ){ in computeRelevantEqr()
2109 Node r = (*eqcs_i); in computeRelevantEqr()
2116 ++eqcs_i; in computeRelevantEqr()
2128 eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( getEqualityEngine() ); in debugPrint() local
2129 while( !eqcs_i.isFinished() ){ in debugPrint()
2130 Node n = (*eqcs_i); in debugPrint()
2144 ++eqcs_i; in debugPrint()
|
| H A D | term_database.cpp | 909 eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); in reset() local
910 while( !eqcs_i.isFinished() ){ in reset()
911 TNode r = (*eqcs_i); in reset()
929 ++eqcs_i; in reset()
956 eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); in reset() local
957 while( !eqcs_i.isFinished() ){ in reset()
958 TNode r = (*eqcs_i); in reset()
999 ++eqcs_i; in reset()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/fmf/ |
| H A D | full_model_check.cpp | 298 eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( fm->d_equalityEngine ); in preProcessBuildModel() local
299 while( !eqcs_i.isFinished() ){ in preProcessBuildModel()
300 Node r = *eqcs_i; in preProcessBuildModel()
303 ++eqcs_i; in preProcessBuildModel()
|
| H A D | model_builder.cpp | 59 eq::EqClassesIterator eqcs_i = in preProcessBuildModelStd() local
61 while( !eqcs_i.isFinished() ){ in preProcessBuildModelStd()
62 TypeNode tr = (*eqcs_i).getType(); in preProcessBuildModelStd()
64 ++eqcs_i; in preProcessBuildModelStd()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/ |
| H A D | quantifiers_engine.cpp | 1262 eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); in debugPrintEqualityEngine() local
1264 while( !eqcs_i.isFinished() ){ in debugPrintEqualityEngine()
1265 TNode r = (*eqcs_i); in debugPrintEqualityEngine()
1288 ++eqcs_i; in debugPrintEqualityEngine()
|
| H A D | theory_model.cpp | 416 eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); in assertEqualityEngine() local
417 for (; !eqcs_i.isFinished(); ++eqcs_i) { in assertEqualityEngine()
418 Node eqc = (*eqcs_i); in assertEqualityEngine()
|
| H A D | theory_model_builder.cpp | 317 eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine); in buildModel() local
320 for (; !eqcs_i.isFinished(); ++eqcs_i) in buildModel()
323 eq::EqClassIterator((*eqcs_i), tm->d_equalityEngine); in buildModel()
328 TypeNode tn = (*eqcs_i).getType(); in buildModel()
370 eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine); in buildModel()
371 for (; !eqcs_i.isFinished(); ++eqcs_i) in buildModel()
374 Node eqc = (*eqcs_i); in buildModel()
848 for (eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine); in debugCheckModel()
849 !eqcs_i.isFinished(); in debugCheckModel()
850 ++eqcs_i) in debugCheckModel()
[all …]
|
| /dports/math/cvc4/CVC4-1.7/src/theory/sets/ |
| H A D | theory_sets_private.cpp | 538 eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); in fullEffortCheck() local
539 while( !eqcs_i.isFinished() ){ in fullEffortCheck()
540 Node eqc = (*eqcs_i); in fullEffortCheck()
668 ++eqcs_i; in fullEffortCheck()
|
| H A D | theory_sets_rels.cpp | 152 eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( d_eqEngine ); in collectRelsInfo() local
153 while( !eqcs_i.isFinished() ){ in collectRelsInfo()
154 Node eqc_rep = (*eqcs_i); in collectRelsInfo()
223 ++eqcs_i; in collectRelsInfo()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/strings/ |
| H A D | theory_strings.cpp | 1388 eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); in checkInit() local
1389 while( !eqcs_i.isFinished() ){ in checkInit()
1390 Node eqc = (*eqcs_i); in checkInit()
1498 ++eqcs_i; in checkInit()
4615 eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); in getEquivalenceClasses() local
4616 while( !eqcs_i.isFinished() ) { in getEquivalenceClasses()
4617 Node eqc = (*eqcs_i); in getEquivalenceClasses()
4622 ++eqcs_i; in getEquivalenceClasses()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/uf/ |
| H A D | theory_uf.cpp | 813 eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); in checkExtensionality() local
814 while( !eqcs_i.isFinished() ){ in checkExtensionality()
815 Node eqc = (*eqcs_i); in checkExtensionality()
827 ++eqcs_i; in checkExtensionality()
894 eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); in checkAppCompletion() local
896 while( !eqcs_i.isFinished() ){ in checkAppCompletion()
897 Node eqc = (*eqcs_i); in checkAppCompletion()
948 ++eqcs_i; in checkAppCompletion()
|
| H A D | theory_uf_strong_solver.cpp | 1183 eq::EqClassesIterator eqcs_i = in debugModel() local
1185 while( !eqcs_i.isFinished() ){ in debugModel()
1186 Node eqc = (*eqcs_i); in debugModel()
1198 ++eqcs_i; in debugModel()
1584 eq::EqClassesIterator eqcs_i(d_th->getEqualityEngine()); in check() local
1585 while( !eqcs_i.isFinished() ){ in check()
1586 Node a = *eqcs_i; in check()
1608 ++eqcs_i; in check()
|