Searched refs:SortInference (Results 1 – 10 of 10) sorted by relevance
| /dports/math/cvc4/CVC4-1.7/src/theory/ |
| H A D | sort_inference.cpp | 36 void SortInference::UnionFind::print(const char * c){ in print()
45 void SortInference::UnionFind::set( UnionFind& c ) { in set()
73 bool SortInference::UnionFind::isValid() { in isValid()
100 void SortInference::reset() { in reset()
196 Node SortInference::simplify(Node n, in simplify()
304 void SortInference::setEqual( int t1, int t2 ){ in setEqual()
344 int SortInference::getIdForType( TypeNode tn ){ in getIdForType()
579 TypeNode SortInference::getTypeForId( int t ){ in getTypeForId()
611 Node SortInference::simplifyNode( in simplifyNode()
775 int SortInference::getSortId( Node n ) { in getSortId()
[all …]
|
| H A D | sort_inference.h | 37 class SortInference {
108 SortInference() : d_sortCount(1) {} in SortInference() function
109 ~SortInference(){} in ~SortInference()
158 void getSortConstraints( Node n, SortInference::UnionFind& uf );
|
| H A D | theory_engine.h | 458 SortInference d_sortInfer;
888 SortInference* getSortInference() { return &d_sortInfer; } in getSortInference()
|
| /dports/math/vampire/vampire-4.5.1/FMB/ |
| H A D | SortInference.hpp | 88 class SortInference { class
90 CLASS_NAME(SortInference);
91 USE_ALLOCATOR(SortInference);
93 SortInference(ClauseList* clauses, in SortInference() function in FMB::SortInference
|
| H A D | SortInference.cpp | 59 void SortInference::doInference() in doInference()
714 unsigned SortInference::getDistinctSort(unsigned subsort, unsigned realVampireSort, bool createNew) in getDistinctSort()
|
| H A D | FiniteModelBuilder.cpp | 604 … SortInference inference(_clauses,del_f,del_p,equivalent_vampire_sorts,_distinct_sort_constraints); in init()
|
| /dports/math/cvc4/CVC4-1.7/src/preprocessing/passes/ |
| H A D | sort_infer.cpp | 36 SortInference* si = d_preprocContext->getTheoryEngine()->getSortInference(); in applyInternal()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/uf/ |
| H A D | theory_uf_strong_solver.h | 29 class SortInference; variable
369 SortInference* getSortInference();
|
| H A D | theory_uf_strong_solver.cpp | 1351 SortInference* StrongSolverTheoryUF::getSortInference() { in getSortInference()
|
| /dports/math/vampire/vampire-4.5.1/ |
| H A D | Makefile | 433 FMB/SortInference.o\
|