| /dports/math/yices/yices-2.6.2/src/solvers/cdcl/ |
| H A D | gates_manager.c | 455 add_unit_clause(s, a[0]); in assert_xor()
607 add_unit_clause(s, l1); in assert_ite()
616 add_unit_clause(s, l2); in assert_ite()
628 add_unit_clause(s, c); in assert_ite()
629 add_unit_clause(s, l1); // assert (and c l1) in assert_ite()
633 add_unit_clause(s, not(c)); in assert_ite()
634 add_unit_clause(s, l2); // assert (and (not c) l2) in assert_ite()
651 add_unit_clause(s, l1); in assert_ite()
|
| H A D | delegate.c | 136 d->add_unit_clause = ysat_add_unit_clause; in ysat_as_delegate()
272 d->add_unit_clause = cadical_add_unit_clause; in cadical_as_delegate()
369 d->add_unit_clause = cryptominisat_add_unit_clause; in cryptominisat_as_delegate()
483 d->add_unit_clause(d->solver, true_literal); // CHECK THIS in copy_unit_clauses()
488 d->add_unit_clause(d->solver, stack->lit[i]); in copy_unit_clauses()
|
| H A D | delegate.h | 83 add_unit_clause_fun_t add_unit_clause; member
|
| H A D | smt_core.h | 1631 extern void add_unit_clause(smt_core_t *s, literal_t l);
|
| H A D | new_sat_solver2.c | 3325 static void add_unit_clause(sat_solver_t *solver, literal_t l) { in add_unit_clause() function
3431 add_unit_clause(solver, lit[0]); in nsat_solver_simplify_and_add_clause()
4782 add_unit_clause(solver, a[0]); in subst_and_simplify_clause()
4833 add_unit_clause(solver, a[0]); in subst_and_simplify_binary_clause()
4840 add_unit_clause(solver, a[0]); in subst_and_simplify_binary_clause()
8362 add_unit_clause(solver, l); in resolve_conflict()
8386 add_unit_clause(solver, l); in process_subst_units()
|
| H A D | new_sat_solver.c | 3693 static void add_unit_clause(sat_solver_t *solver, literal_t l) { in add_unit_clause() function
3799 add_unit_clause(solver, lit[0]); in nsat_solver_simplify_and_add_clause()
5156 add_unit_clause(solver, a[0]); in subst_and_simplify_clause()
5207 add_unit_clause(solver, a[0]); in subst_and_simplify_binary_clause()
5214 add_unit_clause(solver, a[0]); in subst_and_simplify_binary_clause()
9738 add_unit_clause(solver, l); in resolve_conflict()
9762 add_unit_clause(solver, l); in process_subst_units()
|
| H A D | smt_core.c | 4247 void add_unit_clause(smt_core_t *s, literal_t l) { in add_unit_clause() function
|
| /dports/math/z3/z3-z3-4.8.13/src/math/subpaving/ |
| H A D | subpaving_t_def.h | 813 add_unit_clause(atoms[0], true); in add_clause_core()
865 void context_t<C>::add_unit_clause(ineq * a, bool axiom) { in add_unit_clause() function
874 add_unit_clause(unit, axiom); in add_ineq()
|
| H A D | subpaving_t.h | 560 void add_unit_clause(ineq * a, bool axiom);
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/math/subpaving/ |
| H A D | subpaving_t_def.h | 813 add_unit_clause(atoms[0], true); in add_clause_core()
865 void context_t<C>::add_unit_clause(ineq * a, bool axiom) { in add_unit_clause() function
874 add_unit_clause(unit, axiom); in add_ineq()
|
| H A D | subpaving_t.h | 560 void add_unit_clause(ineq * a, bool axiom);
|
| /dports/math/yices/yices-2.6.2/src/solvers/bv/ |
| H A D | bvsolver.c | 6218 add_unit_clause(solver->core, not(l)); in bv_solver_assert_neq0()
6284 add_unit_clause(solver->core, not(l)); in bv_solver_assert_eq_axiom()
6334 add_unit_clause(solver->core, signed_literal(l, tt)); in bv_solver_assert_ge_axiom()
6390 add_unit_clause(solver->core, signed_literal(l, tt)); in bv_solver_assert_sge_axiom()
6408 add_unit_clause(solver->core, signed_literal(l, tt)); in bv_solver_set_bit()
|
| H A D | bit_blaster.c | 509 add_unit_clause(s->solver, l); in bit_blaster_add_unit_clause()
|
| /dports/math/yices/yices-2.6.2/src/context/ |
| H A D | context.c | 3260 add_unit_clause(ctx->core, l); in assert_internalization_code()
3812 add_unit_clause(ctx->core, l); in assert_arith_distinct()
3827 add_unit_clause(ctx->core, l); in assert_bv_distinct()
|
| /dports/math/yices/yices-2.6.2/src/solvers/floyd_warshall/ |
| H A D | idl_floyd_warshall.c | 2421 add_unit_clause(solver->core, not(c)); in idl_assert_cond_vareq_axiom()
|
| H A D | rdl_floyd_warshall.c | 2623 add_unit_clause(solver->core, not(c)); in rdl_assert_cond_vareq_axiom()
|
| /dports/math/yices/yices-2.6.2/src/solvers/egraph/ |
| H A D | egraph.c | 3183 add_unit_clause(egraph->core, l); in egraph_add_type_constraints()
6413 add_unit_clause(egraph->core, not(l)); in egraph_assert_diseq_axiom()
6510 add_unit_clause(egraph->core, not(l)); in egraph_assert_notpred_axiom()
|
| /dports/math/yices/yices-2.6.2/src/solvers/simplex/ |
| H A D | simplex.c | 3196 add_unit_clause(solver->core, not(c)); in simplex_assert_cond_vareq_axiom()
5064 add_unit_clause(solver->core, l); in simplex_implied_literal()
9436 add_unit_clause(solver->core, not(l)); in simplex_trichotomy_lemma()
11860 add_unit_clause(solver->core, not(l)); in simplex_gen_interface_lemma()
|
| /dports/math/yices/yices-2.6.2/src/solvers/funs/ |
| H A D | fun_solver.c | 801 add_unit_clause(solver->core, eq); in fun_solver_update_axiom1()
|