Home
last modified time | relevance | path

Searched refs:ETYPE_BV (Results 1 – 5 of 5) sorted by relevance

/dports/math/yices/yices-2.6.2/src/solvers/egraph/
H A Degraph.c2265 case ETYPE_BV: in constant_theory_var()
2385 case ETYPE_BV: in egraph_check_theory_diseq()
2940 case ETYPE_BV: in auto_activate()
3770 case ETYPE_BV: in propagate_thvar_equality()
5413 egraph->eg[ETYPE_BV]->prepare_model(egraph->th[ETYPE_BV]); in egraph_prepare_models()
5428 egraph->eg[ETYPE_BV]->release_model(egraph->th[ETYPE_BV]); in egraph_release_models()
5499 case ETYPE_BV: in egraph_gen_interface_lemmas()
5541 case ETYPE_BV: in diseq_in_model()
5608 case ETYPE_BV: in reconcile_thvar()
6003 c = egraph->ctrl[ETYPE_BV]->final_check(egraph->th[ETYPE_BV]); in baseline_final_check()
[all …]
H A Degraph_base_types.h411 ETYPE_BV, // 2 enumerator
H A Degraph_explanations.c592 case ETYPE_BV: in eterm_is_constant()
1615 case ETYPE_BV: in interface_lemma_candidate()
1616 satellite = egraph->th[ETYPE_BV]; in interface_lemma_candidate()
1617 interface = egraph->eg[ETYPE_BV]; in interface_lemma_candidate()
H A Degraph_utils.h192 return egraph_class_type(egraph, c) == ETYPE_BV; in egraph_class_is_bv()
H A Degraph_printer.c677 case ETYPE_BV: in print_egraph_terms()