Searched refs:getEnumerateTerm (Results 1 – 8 of 8) sorted by relevance
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/ |
| H A D | term_enumeration.h | 44 Node getEnumerateTerm(TypeNode tn, unsigned i);
|
| H A D | term_enumeration.cpp | 27 Node TermEnumeration::getEnumerateTerm(TypeNode tn, unsigned index) in getEnumerateTerm() function in CVC4::theory::quantifiers::TermEnumeration
|
| H A D | sygus_sampler.cpp | 644 Node ret = d_tenum.getEnumerateTerm(tn, counter); in getRandomValue()
648 ret = d_tenum.getEnumerateTerm(tn, 0); in getRandomValue()
|
| H A D | first_order_model.cpp | 321 mbt = d_qe->getTermEnumeration()->getEnumerateTerm(tn, 0); in getModelBasisTerm()
|
| H A D | instantiate.cpp | 496 return d_qe->getTermEnumeration()->getEnumerateTerm(tn, 0); in getTermForType()
|
| H A D | conjecture_generator.cpp | 1120 && !te->getEnumerateTerm(types[index], vec[index] + 1).isNull()) in getEnumerateUfTerm()
1139 te->getEnumerateTerm(types[vec.size() - 1], vec[vec.size() - 1]); in getEnumerateUfTerm()
1152 Node nn = te->getEnumerateTerm(types[i], vec[i]); in getEnumerateUfTerm()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/ |
| H A D | ce_guided_single_inv.cpp | 549 s = d_qe->getTermEnumeration()->getEnumerateTerm( in getSolution()
|
| H A D | ce_guided_single_inv_sol.cpp | 721 Node ns = d_qe->getTermEnumeration()->getEnumerateTerm(stn, index); in reconstructSolution()
|