Home
last modified time | relevance | path

Searched refs:evaluateBuiltin (Results 1 – 7 of 7) sorted by relevance

/dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/
H A Dsygus_invariance.cpp101 d_exo.push_back(d_conj->getPbe()->evaluateBuiltin(tn, bvr, e, i)); in init()
154 Node nbvr_ex = d_conj->getPbe()->evaluateBuiltin(tn, nbvr, d_enum, j); in invariant()
215 Node nbvre = tds->evaluateBuiltin(tn, nbvr, d_ex[ii]); in invariant()
H A Dsygus_pbe.h193 Node evaluateBuiltin(TypeNode tn, Node bn, Node e, unsigned i);
H A Dsygus_pbe.cpp403 Node SygusPbe::evaluateBuiltin(TypeNode tn, Node bn, Node e, unsigned i) in evaluateBuiltin() function in CVC4::theory::quantifiers::SygusPbe
413 return d_tds->evaluateBuiltin(tn, bn, it->second[i]); in evaluateBuiltin()
H A Dterm_database_sygus.h274 Node evaluateBuiltin(TypeNode tn,
H A Dsygus_unif_rl.cpp1119 Node res = d_dt->d_unif->d_tds->evaluateBuiltin(tn, builtin_cond, pt); in computeCond()
H A Dsygus_unif_io.cpp545 Node res = d_tds->evaluateBuiltin(xtn, bv, d_examples[j]); in computeExamples()
H A Dterm_database_sygus.cpp1588 Node TermDbSygus::evaluateBuiltin(TypeNode tn, in evaluateBuiltin() function in CVC4::theory::quantifiers::TermDbSygus