Searched refs:d_term_util (Results 1 – 4 of 4) sorted by relevance
/dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/ |
H A D | instantiate.cpp | 37 d_term_util(nullptr), in Instantiate() 66 d_term_util = d_qe->getTermUtil(); in reset() 110 Assert(d_term_util != nullptr); in addInstantiation() 168 terms[i], d_term_util->d_inst_constants[q])) in addInstantiation() 242 Assert(d_term_util->d_vars[q].size() == terms.size()); in addInstantiation() 244 Node body = getInstantiation(q, d_term_util->d_vars[q], terms, doVts); in addInstantiation() 422 Node body_r = d_term_util->rewriteVtsSymbols(body); in getInstantiation() 432 Assert(d_term_util->d_vars.find(q) != d_term_util->d_vars.end()); in getInstantiation() 434 return getInstantiation(q, d_term_util->d_vars[q], m.d_vals, doVts); in getInstantiation() 439 Assert(d_term_util->d_vars.find(q) != d_term_util->d_vars.end()); in getInstantiation() [all …]
|
H A D | instantiate.h | 340 TermUtil* d_term_util; variable
|
/dports/math/cvc4/CVC4-1.7/src/theory/ |
H A D | quantifiers_engine.cpp | 83 d_term_util(new quantifiers::TermUtil(this)), in QuantifiersEngine() 122 d_util.push_back(d_term_util.get()); in QuantifiersEngine() 147 d_lemmas_produced_c[d_term_util->d_true] = true; in QuantifiersEngine() 331 return d_term_util.get(); in getTermUtil() 929 addTermToDatabase(d_term_util->getInstConstantBody(f), true); in assertQuantifier()
|
H A D | quantifiers_engine.h | 346 std::unique_ptr<quantifiers::TermUtil> d_term_util; variable
|