Searched refs:arith_atom_t (Results 1 – 6 of 6) sorted by relevance
/dports/math/yices/yices-2.6.2/src/solvers/simplex/ |
H A D | arith_atomtable.h | 74 } arith_atom_t; typedef 81 static inline thvar_t var_of_atom(arith_atom_t *atom) { in var_of_atom() 85 static inline arithatm_tag_t tag_of_atom(arith_atom_t *atom) { in tag_of_atom() 89 static inline bool atom_is_ge(arith_atom_t *atm) { in atom_is_ge() 93 static inline bool atom_is_le(arith_atom_t *atm) { in atom_is_le() 97 static inline bool atom_is_eq(arith_atom_t *atm) { in atom_is_eq() 101 static inline bvar_t boolvar_of_atom(arith_atom_t *atom) { in boolvar_of_atom() 105 static inline rational_t *bound_of_atom(arith_atom_t *atom) { in bound_of_atom() 150 arith_atom_t *atoms; 169 #define MAX_ARITHATOMTABLE_SIZE (UINT32_MAX/sizeof(arith_atom_t)) [all …]
|
H A D | arith_atomtable.c | 80 table->atoms = (arith_atom_t *) safe_malloc(n * sizeof(arith_atom_t)); in init_arith_atomtable() 103 table->atoms = (arith_atom_t *) safe_realloc(table->atoms, n * sizeof(arith_atom_t)); in extend_arith_atomtable() 191 arith_atom_t *a; in arith_atomtable_remove_atoms() 233 arith_atom_t *arith_atom_for_bvar(arith_atomtable_t *table, bvar_t v) { in arith_atom_for_bvar()
|
H A D | simplex_printer.c | 165 static void print_arith_atom(FILE *f, arith_vartable_t *table, arith_atom_t *atom) { in print_arith_atom() 173 arith_atom_t *a; in print_arith_atomtable() 562 arith_atom_t *a; in print_simplex_atomdef() 578 arith_atom_t *a; in print_simplex_atom_of_literal()
|
H A D | simplex_propagator0.h | 176 arith_atom_t *atom; in literal_of_assertion() 346 arith_atom_t *atom; in assertion_implied_by_lb() 407 arith_atom_t *atom; in assertion_implied_by_ub() 600 arith_atom_t *atom; in all_assertions_implied_by_lb() 645 arith_atom_t *atom; in all_assertions_implied_by_ub()
|
H A D | simplex_propagator1.h | 169 arith_atom_t *atom; in lb_can_propagate_literals() 211 arith_atom_t *atom; in ub_can_propagate_literals()
|
H A D | simplex.c | 1721 static void create_binary_lemma(simplex_solver_t *solver, arith_atom_t *atom1, arith_atom_t *atom2)… in create_binary_lemma() 1722 arith_atom_t *aux; in create_binary_lemma() 1827 arith_atom_t *atom, *atom1, *atom2, *aux; in build_binary_lemmas_for_atom() 4971 arith_atom_t *atom; in simplex_process_assertion() 5086 arith_atom_t *p; in check_lower_bound_implications() 5144 arith_atom_t *p; in check_upper_bound_implications() 10347 arith_atom_t *atm; in simplex_detach_dead_atoms() 10722 static bool simplex_eval_atom(simplex_solver_t *solver, arith_atom_t *atom) { in simplex_eval_atom() 10759 arith_atom_t *atom; in simplex_select_polarity() 12400 arith_atom_t *atom; in assertions_hold_in_model() [all …]
|