| /dports/math/yices/yices-2.6.2/src/scratch/ |
| H A D | flattening.c | 96 if (f_ite && is_boolean_term(terms, d->arg[1])) { in flattener_build_conjuncts()
97 assert(is_boolean_term(terms, d->arg[2])); in flattener_build_conjuncts()
123 if (f_iff && is_boolean_term(terms, d->arg[0])) { in flattener_build_conjuncts()
124 assert(is_boolean_term(terms, d->arg[1])); in flattener_build_conjuncts()
193 if (f_ite && is_boolean_term(terms, d->arg[1])) { in flattener_build_disjuncts()
194 assert(is_boolean_term(terms, d->arg[2])); in flattener_build_disjuncts()
221 assert(is_boolean_term(terms, d->arg[1])); in flattener_build_disjuncts()
290 assert(is_boolean_term(terms, d->arg[2])); in flattener_forall_conjuncts()
317 assert(is_boolean_term(terms, d->arg[1])); in flattener_forall_conjuncts()
401 assert(is_boolean_term(terms, d->arg[2])); in flattener_forall_disjuncts()
[all …]
|
| /dports/math/yices/yices-2.6.2/src/terms/ |
| H A D | bit_term_conversion.c | 42 assert(good_term(table, t) && is_boolean_term(table, t)); in convert_term_to_bit()
137 assert(is_boolean_term(terms, aux[0]) && is_boolean_term(terms, aux[1]));
151 assert(is_boolean_term(terms, aux[0]) && is_boolean_term(terms, aux[1]));
198 assert(is_boolean_term(terms, t));
|
| H A D | elim_subst.c | 275 if (is_boolean_term(terms, f)) { in elim_subst_try_map()
292 if (is_boolean_term(terms, t1)) { in elim_subst_try_map()
339 if (is_boolean_term(terms, t1)) { in elim_subst_try_cheap_map()
|
| H A D | term_manager.c | 1385 is_boolean_term(tbl, c)); in mk_bv_ite()
2021 is_boolean_term(manager->terms, e)); in mk_ite()
3327 if (is_boolean_term(tbl, t1)) { in mk_eq()
3328 assert(is_boolean_term(tbl, t2)); in mk_eq()
3369 if (is_boolean_term(tbl, t1)) { in mk_neq()
3370 assert(is_boolean_term(tbl, t2)); in mk_neq()
3995 assert(is_boolean_term(manager->terms, x) && in make_or2()
3996 is_boolean_term(manager->terms, y)); in make_or2()
4011 assert(is_boolean_term(manager->terms, x) && in make_xor2()
4012 is_boolean_term(manager->terms, y)); in make_xor2()
[all …]
|
| /dports/math/yices/yices-2.6.2/src/context/ |
| H A D | eq_learner.c | 104 assert(good_term(learner->terms, f) && is_boolean_term(learner->terms, f)); in find_cached_abstraction()
122 assert(good_term(learner->terms, f) && is_boolean_term(learner->terms, f) && p != NULL); in cache_abstraction()
136 assert(good_term(learner->terms, f) && is_boolean_term(learner->terms, f)); in get_cached_abstraction()
236 if (is_boolean_term(learner->terms, t1)) { in eq_abstract_eq()
237 assert(is_boolean_term(learner->terms, t2)); in eq_abstract_eq()
324 assert(is_boolean_term(learner->terms, f)); in eq_abstract()
|
| H A D | common_conjuncts.c | 101 assert(is_boolean_term(terms, t)); in bfs_collect_conjuncts()
159 assert(is_boolean_term(terms, t)); in bfs_collect_disjuncts()
|
| H A D | conditional_definitions.c | 249 assert(is_boolean_term(collect->terms, t)); in bool_vars_of_term()
288 if (is_boolean_term(terms, eq->arg[0])) { in bool_vars_of_term()
484 assert(is_boolean_term(c->terms, x[i]) &&
532 assert(is_boolean_term(c->terms, x[i]) && in print_definition_table()
969 assert(is_boolean_term(c->terms, t)); in truth_tbl_of_term()
1237 assert(is_boolean_term(terms, x)); in make_pseudo_product()
|
| H A D | context_simplifier.c | 1291 …assert(is_boolean_term(ctx->terms, t1) && is_boolean_term(ctx->terms, t2) && term_is_true(ctx, e)); in check_candidate_bool_subst()
1337 if (is_boolean_term(terms, t1)) { in process_subst_eqs()
1891 if (is_boolean_term(terms, t1)) { in flatten_eq()
1895 assert(is_boolean_term(terms, t2)); in flatten_eq()
2400 if (is_boolean_term(ctx->terms, t1)) { in process_aux_eq()
2558 assert(is_boolean_term(ctx->terms, t)); in flatten_or_push_term()
2569 assert(is_boolean_term(ctx->terms, t)); in flatten_or_add_term()
3162 assert(is_boolean_term(ctx->terms, t)); in analyze_dl()
3198 if (is_boolean_term(terms, cmp->arg[0])) { in analyze_dl()
|
| /dports/math/yices/yices-2.6.2/src/exists_forall/ |
| H A D | ef_analyze.c | 309 if (f_ite && is_boolean_term(terms, d->arg[1])) { in ef_flatten_quantifiers_conjuncts()
310 assert(is_boolean_term(terms, d->arg[2])); in ef_flatten_quantifiers_conjuncts()
336 if (f_iff && is_boolean_term(terms, d->arg[0])) { in ef_flatten_quantifiers_conjuncts()
337 assert(is_boolean_term(terms, d->arg[1])); in ef_flatten_quantifiers_conjuncts()
497 if (f_ite && is_boolean_term(terms, d->arg[1])) { in ef_build_disjuncts()
498 assert(is_boolean_term(terms, d->arg[2])); in ef_build_disjuncts()
524 if (f_iff && is_boolean_term(terms, d->arg[0])) { in ef_build_disjuncts()
525 assert(is_boolean_term(terms, d->arg[1])); in ef_build_disjuncts()
|
| H A D | efsolver.c | 251 assert(ctx != NULL && is_boolean_term(ctx->terms, f)); in update_exists_context()
328 assert(is_boolean_term(ctx->terms, b) && is_boolean_term(ctx->terms, c)); in forall_context_assert()
|
| /dports/math/yices/yices-2.6.2/src/model/ |
| H A D | model_queries.c | 65 assert(is_boolean_term(mdl->terms, f)); in formula_holds_in_model()
150 assert(is_boolean_term(mdl->terms, a[i])); in formulas_hold_in_model()
|
| H A D | literal_collector.c | 114 if (is_boolean_term(collect->terms, t) && !collect->bool_are_terms) { in lit_collector_find_cached_term()
140 if (is_boolean_term(collect->terms, t) && !collect->bool_are_terms) { in lit_collector_cache_result()
171 assert(is_boolean_term(collect->terms, t)); in term_is_true_in_model()
184 assert(is_boolean_term(collect->terms, t)); in term_is_false_in_model()
199 assert(is_boolean_term(collect->terms, t)); in is_true_in_model()
716 is_boolean_term(collect->terms, t1)) { in lit_collector_visit_eq()
724 assert(is_boolean_term(collect->terms, t2)); in lit_collector_visit_eq()
857 if (is_boolean_term(collect->terms, t)) { in lit_collector_visit_app()
1146 if (is_boolean_term(collect->terms, t)) { in lit_collector_visit_select()
1314 if (is_boolean_term(terms, t)) { in lit_collector_visit()
|
| /dports/math/yices/yices-2.6.2/src/mcsat/bv/ |
| H A D | bv_utils.h | 143 if (!is_boolean_term(terms, eq->arg[0]) && !is_bitvector_term(terms, eq->arg[0])) { in bv_term_get_type()
163 if (!is_boolean_term(terms, eq->arg[0]) && !is_bitvector_term(terms, eq->arg[0])) { in bv_term_is_variable()
404 assert(is_bitvector_term(tm->terms, t) || is_boolean_term(tm->terms, t)); in term_extract()
|
| H A D | bv_explainer.c | 127 if (is_boolean_term(terms, lhs)) { in bv_explainer_normalize_conflict()
128 assert(is_boolean_term(terms, rhs)); in bv_explainer_normalize_conflict()
|
| H A D | bv_evaluator.c | 472 if (!is_boolean_term(terms, lhs) && !is_bitvector_term(terms, lhs)) { in bv_evaluator_run_atom()
551 if (t_kind == EQ_TERM && is_boolean_term(terms, t_lhs)) { in bv_evaluator_run_atom()
698 assert(is_bitvector_term(terms, t) || is_boolean_term(terms, t)); in bv_evaluator_not_free_up_to()
|
| /dports/math/yices/yices-2.6.2/src/frontend/common/ |
| H A D | assumptions_and_core.c | 99 if (! is_boolean_term(a->terms, t)) { in collect_assumptions_from_signed_symbols()
|
| /dports/math/yices/yices-2.6.2/src/mcsat/bv/explain/ |
| H A D | arith_norm.c | 585 term_t result = (is_boolean_term(terms,t)) ? t : term_extract(tm, t, 0, w); in arith_normalise_upto()
598 term_t result = (is_boolean_term(terms,t)) ? t : term_extract(tm, t, 0, w); in arith_normalise_upto()
611 assert(is_boolean_term(terms,t)); in arith_normalise_upto()
635 term_t result = (is_boolean_term(terms,t)) ? t : term_extract(tm, t, 0, w); in arith_normalise_upto()
685 if (is_boolean_term(terms,t)) { in arith_normalise_upto()
861 assert(!is_boolean_term(terms,t)); in arith_normalise_upto()
|
| H A D | eq_ext_con.c | 820 assert(is_boolean_term(terms,t)); in term_is_ext_con()
1008 assert(is_boolean_term(terms,atom_i_term)); in bv_slicing_construct()
1572 if (result_subst != NULL_TERM && is_boolean_term(terms, x_term)) { in explain_propagation()
1584 …if (is_boolean_term(terms,x_term)) return false; // We don't explain when conflict variable is Boo… in can_explain_propagation()
|
| /dports/math/yices/yices-2.6.2/src/frontend/smt2/ |
| H A D | smt2_model_printer.c | 86 if (is_boolean_term(terms, t)) { in smt2_pp_bool_assignments()
229 if (is_boolean_term(terms, t)) { in smt2_eval_pp_bool_assignments()
|
| /dports/math/yices/yices-2.6.2/tests/unit/ |
| H A D | test_smt_parser.c | 79 assert(is_boolean_term(__yices_globals.terms, f)); in benchmark_reduced_to_false()
|
| H A D | test_dl_profiler.c | 138 assert(is_boolean_term(__yices_globals.terms, f)); in benchmark_reduced_to_false()
|
| H A D | test_truth_tables.c | 60 assert(is_boolean_term(c->terms, x[i]) && in print_truth_tbl()
286 assert(is_boolean_term(c->terms, t)); in truth_tbl_of_term()
|
| H A D | test_smt_blaster.c | 227 assert(is_boolean_term(__yices_globals.terms, f)); in benchmark_reduced_to_false()
|
| H A D | test_smt_internalizer.c | 381 assert(is_boolean_term(__yices_globals.terms, f)); in benchmark_reduced_to_false()
|
| /dports/math/yices/yices-2.6.2/src/io/ |
| H A D | model_printer.c | 76 if (is_boolean_term(terms, t)) { in model_print_bool_assignments()
424 if (is_boolean_term(terms, t)) { in eval_print_bool_assignments()
686 if (is_boolean_term(terms, t)) { in model_pp_bool_assignments()
1034 if (is_boolean_term(terms, t)) { in eval_pp_bool_assignments()
|