Home
last modified time | relevance | path

Searched refs:bool2term (Results 1 – 12 of 12) sorted by relevance

/dports/math/yices/yices-2.6.2/src/mcsat/
H A Dconflict.c291 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 Dval_to_term.c67 return bool2term(boolobj_value(vtbl, v)); in convert_bool()
H A Dliteral_collector.c951 return bool2term(b); in lit_collector_visit_xor_formula()
/dports/math/yices/yices-2.6.2/src/terms/
H A Dterm_utils.c748 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 Dterm_manager.c1107 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 Dterms.h1031 static inline term_t bool2term(bool tt) { in bool2term() function
/dports/math/yices/yices-2.6.2/src/mcsat/bv/
H A Dbv_plugin.c1190 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 Dnra_plugin.c1466 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 Dbool_plugin.c757 return bool2term(var_value); in bool_plugin_explain_propagation()
/dports/math/yices/yices-2.6.2/src/mcsat/bv/explain/
H A Deq_ext_con.c1076 a1[0] = bool2term(atom_i_value); in bv_slicing_construct()
/dports/math/yices/yices-2.6.2/src/parser_utils/
H A Dterm_stack2.c1689 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 Dcontext_simplifier.c2225 intern_tbl_add_subst(intern, r, bool2term(tt)); in flatten_assertion()