Home
last modified time | relevance | path

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 Darith_atomtable.h74 } 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 Darith_atomtable.c80 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 Dsimplex_printer.c165 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 Dsimplex_propagator0.h176 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 Dsimplex_propagator1.h169 arith_atom_t *atom; in lb_can_propagate_literals()
211 arith_atom_t *atom; in ub_can_propagate_literals()
H A Dsimplex.c1721 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 …]