| /dports/math/cvc4/CVC4-1.7/src/theory/ |
| H A D | theory_model_builder.cpp | 322 eq::EqClassIterator eqc_i = in buildModel() local
324 for (; !eqc_i.isFinished(); ++eqc_i) in buildModel()
384 for (; !eqc_i.isFinished(); ++eqc_i) in buildModel()
386 Node n = *eqc_i; in buildModel()
490 for (; !eqc_i.isFinished(); ++eqc_i) in buildModel()
492 Node n = *eqc_i; in buildModel()
655 eq::EqClassIterator eqc_i = in buildModel() local
659 for (; !eqc_i.isFinished(); ++eqc_i) in buildModel()
661 Node n = *eqc_i; in buildModel()
864 for (; !eqc_i.isFinished(); ++eqc_i) in debugCheckModel()
[all …]
|
| H A D | theory_model.cpp | 430 eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, ee); in assertEqualityEngine() local
433 for (; !eqc_i.isFinished(); ++eqc_i) { in assertEqualityEngine()
434 if (termSet != NULL && termSet->find(*eqc_i) == termSet->end()) { in assertEqualityEngine()
441 if (!assertPredicate(*eqc_i, predTrue)) in assertEqualityEngine()
448 rep = (*eqc_i); in assertEqualityEngine()
462 rep = (*eqc_i); in assertEqualityEngine()
472 if (!assertEquality(*eqc_i, rep, true)) in assertEqualityEngine()
591 eq::EqClassIterator eqc_i = eq::EqClassIterator(r,d_equalityEngine); in assignFunctionDefinition() local
592 while( !eqc_i.isFinished() ) { in assignFunctionDefinition()
593 Node n = *eqc_i; in assignFunctionDefinition()
[all …]
|
| H A D | quantifiers_engine.cpp | 1274 eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee ); in debugPrintEqualityEngine() local
1275 while( !eqc_i.isFinished() ){ in debugPrintEqualityEngine()
1276 TNode n = (*eqc_i); in debugPrintEqualityEngine()
1284 ++eqc_i; in debugPrintEqualityEngine()
|
| /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() local
823 while( h.isNull() && !eqc_i.isFinished() ){ in getEligibleTermInEqc()
824 TNode n = (*eqc_i); in getEligibleTermInEqc()
825 ++eqc_i; in getEligibleTermInEqc()
915 eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee ); in reset() local
916 while( !eqc_i.isFinished() ){ in reset()
917 TNode n = (*eqc_i); in reset()
927 ++eqc_i; in reset()
963 while( !eqc_i.isFinished() ){ in reset()
964 TNode n = (*eqc_i); in reset()
[all …]
|
| H A D | conjecture_generator.cpp | 167 std::map< Node, EqcInfo* >::iterator eqc_i = d_eqc_info.find( n ); in getOrMakeEqcInfo() local
168 if( eqc_i!=d_eqc_info.end() ){ in getOrMakeEqcInfo()
169 return eqc_i->second; in getOrMakeEqcInfo()
458 eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee ); in check() local
459 while( !eqc_i.isFinished() ){ in check()
460 TNode n = (*eqc_i); in check()
477 ++eqc_i; in check()
|
| H A D | quant_conflict_find.cpp | 2133 eq::EqClassIterator eqc_i = eq::EqClassIterator( n, getEqualityEngine() ); in debugPrint() local
2135 while( !eqc_i.isFinished() ){ in debugPrint()
2136 Node nn = (*eqc_i); in debugPrint()
2141 ++eqc_i; 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() local
612 TNode rep = d_mayEqualEqualityEngine.getRepresentative(*eqc_i); in checkWeakEquiv()
614 for (; !eqc_i.isFinished(); ++eqc_i) { in checkWeakEquiv()
615 TNode n = *eqc_i; in checkWeakEquiv()
1076 eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, &d_equalityEngine); in collectModelInfo() local
1077 for (; !eqc_i.isFinished(); ++eqc_i) { in collectModelInfo()
1078 Node n = *eqc_i; in collectModelInfo()
1102 eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, &d_equalityEngine); in collectModelInfo() local
1103 for (; !eqc_i.isFinished(); ++eqc_i) { in collectModelInfo()
1104 Node n = *eqc_i; in collectModelInfo()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/datatypes/ |
| H A D | theory_datatypes.cpp | 101 if( eqc_i != d_eqc_info.end() ){ in getOrMakeEqcInfo()
102 ei = eqc_i->second; in getOrMakeEqcInfo()
119 std::map< Node, EqcInfo* >::iterator eqc_i = d_eqc_info.find( n ); in getOrMakeEqcInfo() local
120 return (*eqc_i).second; in getOrMakeEqcInfo()
2159 while( !eqc_i.isFinished() ){ in printModelDebug()
2160 if( (*eqc_i)!=eqc ){ in printModelDebug()
2161 Trace( c ) << (*eqc_i) << " "; in printModelDebug()
2163 ++eqc_i; in printModelDebug()
2233 while (!eqc_i.isFinished()) in getRelevantTerms()
2235 TNode n = (*eqc_i); in getRelevantTerms()
[all …]
|
| /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() local
1296 while( !eqc_i.isFinished() ){ in processAssertions()
1297 d_curr_eqc[pvr].push_back( *eqc_i ); in processAssertions()
1298 ++eqc_i; in processAssertions()
1355 eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee ); in processAssertions() local
1356 while( !eqc_i.isFinished() ){ in processAssertions()
1357 Trace("cbqi-proc-debug") << *eqc_i << " "; in processAssertions()
1358 d_curr_eqc[r].push_back( *eqc_i ); in processAssertions()
1359 ++eqc_i; in processAssertions()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/uf/ |
| H A D | theory_uf.cpp | 899 eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); in checkAppCompletion() local
900 while( !eqc_i.isFinished() ){ in checkAppCompletion()
901 Node n = *eqc_i; in checkAppCompletion()
946 ++eqc_i; in checkAppCompletion()
|
| /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() local
159 while( !eqc_i.isFinished() ){ in collectRelsInfo()
160 Node eqc_node = (*eqc_i); in collectRelsInfo()
221 ++eqc_i; in collectRelsInfo()
1647 std::map< Node, EqcInfo* >::iterator eqc_i = d_eqc_info.find( n ); in getOrMakeEqcInfo() local
1648 if( eqc_i == d_eqc_info.end() ){ in getOrMakeEqcInfo()
1651 if( eqc_i!=d_eqc_info.end() ){ in getOrMakeEqcInfo()
1652 ei = eqc_i->second; in getOrMakeEqcInfo()
1669 return (*eqc_i).second; in getOrMakeEqcInfo()
|
| H A D | theory_sets_private.cpp | 202 std::map< Node, EqcInfo* >::iterator eqc_i = d_eqc_info.find( n ); in getOrMakeEqcInfo() local
203 if( eqc_i==d_eqc_info.end() ){ in getOrMakeEqcInfo()
211 return eqc_i->second; in getOrMakeEqcInfo()
553 eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); in fullEffortCheck() local
554 while( !eqc_i.isFinished() ) { in fullEffortCheck()
555 Node n = (*eqc_i); in fullEffortCheck()
660 ++eqc_i; in fullEffortCheck()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/strings/ |
| H A D | theory_strings.cpp | 1090 if( eqc_i==d_eqc_info.end() ){ in getOrMakeEqcInfo()
1099 return (*eqc_i).second; in getOrMakeEqcInfo()
1399 Node n = *eqc_i; in checkInit()
1495 ++eqc_i; in checkInit()
2401 Node n = (*eqc_i); in checkCycles()
2453 ++eqc_i; in checkCycles()
2471 Node n = (*eqc_i); in checkNormalFormsEq()
2475 ++eqc_i; in checkNormalFormsEq()
2708 while( !eqc_i.isFinished() ){ in getNormalForms()
2709 Node n = (*eqc_i); in getNormalForms()
[all …]
|