Searched refs:bool2term (Results 1 – 12 of 12) sorted by relevance
/dports/math/yices/yices-2.6.2/src/mcsat/ |
H A D | conflict.c | 291 return bool2term(false); in conflict_disjunct_substitute() 369 if (disjunct == bool2term(false)) { in conflict_add_disjunct()
|
/dports/math/yices/yices-2.6.2/src/model/ |
H A D | val_to_term.c | 67 return bool2term(boolobj_value(vtbl, v)); in convert_bool()
|
H A D | literal_collector.c | 951 return bool2term(b); in lit_collector_visit_xor_formula()
|
/dports/math/yices/yices-2.6.2/src/terms/ |
H A D | term_utils.c | 748 if (a->arg[i] != bool2term(tst_bit64(c->value, i))) { in disequal_bitarray_bvconst64() 771 if (a->arg[i] != bool2term(bvconst_tst_bit(c->data, i))) { in disequal_bitarray_bvconst() 3093 bit = bool2term(tst_bit64(c, i)); in extract_bit() 3098 bit = bool2term(bvconst_tst_bit(d, i)); in extract_bit() 3189 b = bool2term(tst_bit64(u->value, i)); // bit i of u in check_eq_bvconst64() 3212 b = bool2term(bvconst_tst_bit(u->data, i)); // bit i of u in check_eq_bvconst() 3309 b = bool2term(tst_bit64(u->value, i)); // bit i of u in flatten_eq_bvconst64() 3330 b = bool2term(bvconst_tst_bit(u->data, i)); // bit i of u in flatten_eq_bvconst()
|
H A D | term_manager.c | 1107 return bool2term(negate); in mk_xor() 1217 bu = bool2term(tst_bit64(u->value, i)); // bit i of u in mk_bvconst64_ite() 1218 bv = bool2term(tst_bit64(v->value, i)); // bit i of v in mk_bvconst64_ite() 1241 bu = bool2term(bvconst_tst_bit(u->data, i)); in mk_bvconst_ite() 1242 bv = bool2term(bvconst_tst_bit(v->data, i)); in mk_bvconst_ite() 1305 b = bool2term(tst_bit64(u->value, i)); // bit i of u in check_ite_bvconst64() 1332 b = bool2term(bvconst_tst_bit(u->data, i)); // bit i of u in check_ite_bvconst() 4205 v->data[i] = bool2term(bvconst_tst_bit(c, i)); in bvarray_copy_constant() 4218 v->data[i] = bool2term(tst_bit64(c, i)); in bvarray_copy_constant64() 5405 u = bool2term(tst_bit64(d->value, i)); in mk_bitextract() [all …]
|
H A D | terms.h | 1031 static inline term_t bool2term(bool tt) { in bool2term() function
|
/dports/math/yices/yices-2.6.2/src/mcsat/bv/ |
H A D | bv_plugin.c | 1190 return bool2term(true); in bv_plugin_explain_propagation() 1194 return bool2term(false); in bv_plugin_explain_propagation()
|
/dports/math/yices/yices-2.6.2/src/mcsat/nra/ |
H A D | nra_plugin.c | 1466 return bool2term(true); in nra_plugin_explain_propagation() 1470 return bool2term(false); in nra_plugin_explain_propagation()
|
/dports/math/yices/yices-2.6.2/src/mcsat/bool/ |
H A D | bool_plugin.c | 757 return bool2term(var_value); in bool_plugin_explain_propagation()
|
/dports/math/yices/yices-2.6.2/src/mcsat/bv/explain/ |
H A D | eq_ext_con.c | 1076 a1[0] = bool2term(atom_i_value); in bv_slicing_construct()
|
/dports/math/yices/yices-2.6.2/src/parser_utils/ |
H A D | term_stack2.c | 1689 t = bool2term(tst_bit64(e->val.bv64.value, i)); in elem_bit_select() 1694 t = bool2term(bvconst_tst_bit(e->val.bv.data, i)); in elem_bit_select()
|
/dports/math/yices/yices-2.6.2/src/context/ |
H A D | context_simplifier.c | 2225 intern_tbl_add_subst(intern, r, bool2term(tt)); in flatten_assertion()
|