Searched refs:boolvar_of_atom (Results 1 – 4 of 4) sorted by relevance
| /dports/math/yices/yices-2.6.2/src/solvers/simplex/ |
| H A D | arith_atomtable.c | 221 assert(boolvar_of_atom(arith_atom(table, id)) == v); in arith_atom_id_for_bvar()
240 assert(boolvar_of_atom(arith_atom(table, id)) == v); in arith_atom_for_bvar()
|
| H A D | arith_atomtable.h | 101 static inline bvar_t boolvar_of_atom(arith_atom_t *atom) { in boolvar_of_atom() function
|
| H A D | simplex.c | 1732 print_simplex_atomdef(stdout, solver, boolvar_of_atom(atom1)); in create_binary_lemma()
1734 print_simplex_atomdef(stdout, solver, boolvar_of_atom(atom2)); in create_binary_lemma()
1757 l1 = pos_lit(boolvar_of_atom(atom1)); in create_binary_lemma()
1758 l2 = pos_lit(boolvar_of_atom(atom2)); in create_binary_lemma()
4980 z = boolvar_of_atom(atom); in simplex_process_assertion()
10665 assert(boolvar_of_atom(arith_atom(&solver->atbl, id)) == var_of(l)); in simplex_assert_atom()
12410 v = boolvar_of_atom(atom); in assertions_hold_in_model()
12922 switch (bvar_value(solver->core, boolvar_of_atom(atom))) { in check_assertion()
12928 print_bvar(stdout, boolvar_of_atom(atom)); in check_assertion()
12940 print_bvar(stdout, boolvar_of_atom(atom)); in check_assertion()
[all …]
|
| H A D | simplex_propagator0.h | 181 return mk_lit(boolvar_of_atom(atom), sign_of_assertion(a)); in literal_of_assertion()
|