Home
last modified time | relevance | path

Searched refs:get_bvar_antecedent (Results 1 – 2 of 2) sorted by relevance

/dports/math/yices/yices-2.6.2/src/solvers/cdcl/
H A Dsmt_core.h1452 static inline antecedent_t get_bvar_antecedent(smt_core_t *s, bvar_t x) { in get_bvar_antecedent() function
/dports/math/yices/yices-2.6.2/src/solvers/egraph/
H A Degraph_explanations.c496 a = get_bvar_antecedent(egraph->core, var_of(l)); in explain_eq()