Searched refs:d_reps (Results 1 – 9 of 9) sorted by relevance
| /dports/math/cvc4/CVC4-1.7/src/theory/ |
| H A D | theory_model.cpp | 76 d_reps.clear(); in reset()
262 Assert(d_reps.find(ret) != d_reps.end()); in getModelValue()
263 std::map<Node, Node>::const_iterator it2 = d_reps.find(ret); in getModelValue()
264 if (it2 != d_reps.end()) in getModelValue()
488 d_reps[ n ] = n; in assertSkeleton()
532 if( d_reps.find( r )!=d_reps.end() ){ in getRepresentative()
533 return d_reps[ r ]; in getRepresentative()
589 d_reps[r] = f_def; in assignFunctionDefinition()
|
| H A D | theory_model_builder.cpp | 389 if (tm->d_reps.find(n) != tm->d_reps.end()) in buildModel()
396 rep = tm->d_reps[n]; in buildModel()
788 tm->d_reps.clear(); in buildModel()
792 tm->d_reps[itMap->first] = itMap->second; in buildModel()
800 tm->d_reps[itMap->first] = itMap->second; in buildModel()
809 tm->d_reps[*i] = *i; in buildModel()
|
| H A D | theory_model.h | 302 std::map<Node, Node> d_reps; variable
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/ |
| H A D | local_theory_ext.cpp | 149 d_reps.clear(); in reset()
155 d_reps[tn].push_back( r ); in reset()
258 std::map< TypeNode, std::vector< Node > >::iterator it = d_reps.find( types[iindex] ); in getPartialInstantiations()
259 if( it!=d_reps.end() ){ in getPartialInstantiations()
|
| H A D | local_theory_ext.h | 35 std::map< TypeNode, std::vector< Node > > d_reps; variable
|
| /dports/math/cvc4/CVC4-1.7/src/theory/uf/ |
| H A D | symmetry_breaker.cpp | 60 d_reps() { in Template()
64 unordered_map<TNode, TNode, TNodeHashFunction>::iterator i = d_reps.find(n); in find()
65 if(i == d_reps.end()) { in find()
68 return d_reps[n] = find((*i).second); in find()
112 d_reps[t] = n; in matchRecursive()
119 d_reps[t] = n; in matchRecursive()
124 d_reps[n] = t; in matchRecursive()
167 d_reps.clear(); in reset()
|
| H A D | theory_uf_strong_solver.cpp | 470 d_reps(c, 0), in SortModel()
552 d_reps = d_reps + 1; in newEqClass()
611 d_reps = d_reps - 1; in merge()
687 if( d_reps<=(unsigned)d_cardinality ){ in check()
688 …Debug("uf-ss-debug") << "We have " << d_reps << " representatives for type " << d_type << ", <= " … in check()
690 …Debug("uf-ss-sat") << "We have " << d_reps << " representatives for type " << d_type << ", <= " <<… in check()
1152 Debug( c ) << "Number of reps = " << d_reps << std::endl; in debugPrint()
1173 if( debugReps!=d_reps ){ in debugPrint()
1174 Debug( c ) << "***Bad reps: " << d_reps << ", " in debugPrint()
|
| H A D | symmetry_breaker.h | 69 std::unordered_map<TNode, TNode, TNodeHashFunction> d_reps; variable
|
| H A D | theory_uf_strong_solver.h | 230 context::CDO< unsigned > d_reps; variable
|