Home
last modified time | relevance | path

Searched refs:d_term_util (Results 1 – 4 of 4) sorted by relevance

/dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/
H A Dinstantiate.cpp37 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 Dinstantiate.h340 TermUtil* d_term_util; variable
/dports/math/cvc4/CVC4-1.7/src/theory/
H A Dquantifiers_engine.cpp83 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 Dquantifiers_engine.h346 std::unique_ptr<quantifiers::TermUtil> d_term_util; variable