Searched refs:evaluateBuiltin (Results 1 – 7 of 7) sorted by relevance
/dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/ |
H A D | sygus_invariance.cpp | 101 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 D | sygus_pbe.h | 193 Node evaluateBuiltin(TypeNode tn, Node bn, Node e, unsigned i);
|
H A D | sygus_pbe.cpp | 403 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 D | term_database_sygus.h | 274 Node evaluateBuiltin(TypeNode tn,
|
H A D | sygus_unif_rl.cpp | 1119 Node res = d_dt->d_unif->d_tds->evaluateBuiltin(tn, builtin_cond, pt); in computeCond()
|
H A D | sygus_unif_io.cpp | 545 Node res = d_tds->evaluateBuiltin(xtn, bv, d_examples[j]); in computeExamples()
|
H A D | term_database_sygus.cpp | 1588 Node TermDbSygus::evaluateBuiltin(TypeNode tn, in evaluateBuiltin() function in CVC4::theory::quantifiers::TermDbSygus
|