Home
last modified time | relevance | path

Searched refs:variable_t (Results 1 – 25 of 178) sorted by relevance

12345678

/dports/math/yices/yices-2.6.2/src/mcsat/
H A Dvariable_db.h32 typedef int32_t variable_t; typedef
79 variable_t variable_db_get_variable(variable_db_t* var_db, term_t term);
90 term_t variable_db_get_term(const variable_db_t* var_db, variable_t term);
94 void (*new_variable) (struct variable_db_new_variable_notify_s* self, variable_t x);
104 bool variable_db_is_boolean(const variable_db_t* var_db, variable_t x);
107 bool variable_db_is_int(const variable_db_t* var_db, variable_t x);
110 bool variable_db_is_real(const variable_db_t* var_db, variable_t x);
113 bool variable_db_is_bitvector(const variable_db_t* var_db, variable_t x);
116 uint32_t variable_db_get_bitsize(const variable_db_t* var_db, variable_t x);
119 type_kind_t variable_db_get_type_kind(const variable_db_t* var_db, variable_t x);
[all …]
H A Dwatch_list_manager.h88 …list_manager_new_list(watch_list_manager_t* wlm, const variable_t* list, uint32_t size, variable_t
91 variable_t watch_list_manager_get_constraint(watch_list_manager_t* wlm, variable_list_ref_t var_lis…
94 bool watch_list_manager_has_constraint(watch_list_manager_t* wlm, variable_t constraint);
97 variable_list_ref_t watch_list_manager_get_list_of(watch_list_manager_t* wlm, variable_t constraint…
100 variable_t* watch_list_manager_get_list(watch_list_manager_t* wlm, variable_list_ref_t var_list);
105 …_manager_add_to_watch(watch_list_manager_t* wlm, variable_list_ref_t var_list, variable_t watcher);
119 variable_t watcher;
130 void remove_iterator_construct(remove_iterator_t* it, watch_list_manager_t* wlm, variable_t watcher…
139 const variable_t* remove_iterator_get_list(const remove_iterator_t* it);
142 variable_t remove_iterator_get_constraint(const remove_iterator_t* it);
H A Dvariable_queue.h56 variable_t *heap;
85 variable_t var_queue_pop(var_queue_t *queue);
88 variable_t var_queue_random(var_queue_t *queue, double *seed);
95 void var_queue_insert(var_queue_t *queue, variable_t x);
98 void var_queue_bump_variable(var_queue_t *heap, variable_t x, uint32_t factor);
101 double var_queue_get_activity(const var_queue_t* queue, variable_t x);
104 void var_queue_set_activity(var_queue_t* queue, variable_t x, double a);
110 int var_queue_cmp_variables(var_queue_t *queue, variable_t x, variable_t y);
H A Dtrail.h96 void trail_new_variable_notify(mcsat_trail_t* trail, variable_t x);
118 variable_t trail_at(const mcsat_trail_t* trail, uint32_t i) { in trail_at()
125 variable_t trail_back(const mcsat_trail_t* trail) { in trail_back()
138 bool trail_has_value(const mcsat_trail_t* trail, variable_t var) { in trail_has_value()
147 bool trail_has_cached_value(const mcsat_trail_t* trail, variable_t var) { in trail_has_cached_value()
154 bool trail_has_value_at_base(const mcsat_trail_t* trail, variable_t var) { in trail_has_value_at_base()
188 uint32_t trail_get_value_timestamp(const mcsat_trail_t* trail, variable_t var) { in trail_get_value_timestamp()
196 bool trail_get_boolean_value(const mcsat_trail_t* trail, variable_t var) { in trail_get_boolean_value()
204 uint32_t trail_get_level(const mcsat_trail_t* trail, variable_t var) { in trail_get_level()
212 uint32_t trail_get_index(const mcsat_trail_t* trail, variable_t var) { in trail_get_index()
[all …]
H A Dvariable_queue.c39 queue->heap = (variable_t *) safe_malloc((VAR_QUEUE_INITIAL_SIZE+1) * sizeof(variable_t)); in var_queue_construct()
87 variable_t *h, y; in var_queue_update_up()
120 variable_t *h; in var_queue_update_down()
121 variable_t x, y, z; in var_queue_update_down()
179 void var_queue_insert(var_queue_t *queue, variable_t x) { in var_queue_insert()
197 variable_t var_queue_pop(var_queue_t *queue) { in var_queue_pop()
198 variable_t top; in var_queue_pop()
213 variable_t var_queue_random(var_queue_t *queue, double* seed) { in var_queue_random()
261 int var_queue_cmp_variables(var_queue_t *queue, variable_t x, variable_t y) { in var_queue_cmp_variables()
292 variable_t x = var_queue_pop(queue); in var_queue_gc_sweep()
[all …]
H A Dwatch_list_manager.c56 …list_manager_new_list(watch_list_manager_t* wlm, const variable_t* list, uint32_t size, variable_t in watch_list_manager_new_list()
83 variable_t constraint_var = gc_vars->marked.data[marked_i]; in watch_list_manager_gc_mark()
86 variable_t* vars = watch_list_manager_get_list(wlm, list_ref); in watch_list_manager_gc_mark()
117 variable_t new_constraint = gc_info_get_reloc(gc_vars, old_constraint); in watch_list_manager_gc_sweep_lists()
127 variable_t list_element; in watch_list_manager_gc_sweep_lists()
140 variable_t watcher = wlm->all_watchers.data[watch_i]; in watch_list_manager_gc_sweep_lists()
236 variable_t remove_iterator_get_constraint(const remove_iterator_t* it) { in remove_iterator_get_constraint()
240 const variable_t* remove_iterator_get_list(const remove_iterator_t* it) { in remove_iterator_get_list()
265 variable_t x; in watch_list_manager_print()
277 variable_t* list = watch_list_manager_get_list(wlm, list_ref); in watch_list_manager_print()
[all …]
H A Dmodel.h47 void mcsat_model_new_variable_notify(mcsat_model_t* m, variable_t x);
50 bool mcsat_model_has_value(const mcsat_model_t* m, variable_t x);
53 uint32_t mcsat_model_get_value_timestamp(const mcsat_model_t* m, variable_t x);
56 const mcsat_value_t* mcsat_model_get_value(const mcsat_model_t* m, variable_t x);
59 void mcsat_model_set_value(mcsat_model_t* m, variable_t x, const mcsat_value_t* value);
62 void mcsat_model_unset_value(mcsat_model_t* m, variable_t x);
H A Dvariable_db.c55 static void variable_db_notify_new_variable(variable_db_t* var_db, variable_t x) { in variable_db_notify_new_variable()
65 variable_t variable_db_get_variable(variable_db_t* var_db, term_t term) { in variable_db_get_variable()
67 variable_t x; in variable_db_get_variable()
98 void variable_db_remove_variable(variable_db_t* var_db, variable_t x) { in variable_db_remove_variable()
133 term_t variable_db_get_term(const variable_db_t* var_db, variable_t x) { in variable_db_get_term()
180 bool variable_db_is_boolean(const variable_db_t* var_db, variable_t x) { in variable_db_is_boolean()
184 bool variable_db_is_real(const variable_db_t* var_db, variable_t x) { in variable_db_is_real()
188 bool variable_db_is_int(const variable_db_t* var_db, variable_t x) { in variable_db_is_int()
192 bool variable_db_is_bitvector(const variable_db_t* var_db, variable_t x) { in variable_db_is_bitvector()
196 uint32_t variable_db_get_bitsize(const variable_db_t* var_db, variable_t x) { in variable_db_get_bitsize()
[all …]
H A Dplugin.h102 void (*bump_variable) (plugin_context_t* self, variable_t x);
105 void (*bump_variable_n) (plugin_context_t* self, variable_t x, uint32_t n);
108 int (*cmp_variables) (plugin_context_t* self, variable_t x, variable_t y);
111 void (*request_top_decision) (plugin_context_t* self, variable_t x);
122 bool (*add) (trail_token_t* token, variable_t x, const mcsat_value_t* value);
130 …bool (*add_at_level) (trail_token_t* token, variable_t x, const mcsat_value_t* value, uint32_t lev…
215 void (*decide) (plugin_t* plugin, variable_t x, trail_token_t* decide, bool must);
241 term_t (*explain_propagation) (plugin_t* plugin, variable_t var, ivector_t* reasons);
H A Dconflict.h143 bool conflict_contains(const conflict_t* conflict, variable_t var);
146 bool conflict_contains_as_top(const conflict_t* conflict, variable_t var);
155 void conflict_resolve_propagation(conflict_t* conflict, variable_t var, term_t substitution, ivecto…
167 void conflict_get_literals_of(conflict_t* conflict, variable_t var, ivector_t* literals);
170 uint32_t conflict_get_literal_count_of(conflict_t* conflict, variable_t var);
176 term_t conflict_get_max_literal_of(conflict_t* conflict, variable_t var);
H A Dtrail.c53 void trail_new_variable_notify(mcsat_trail_t* trail, variable_t x) { in trail_new_variable_notify()
67 variable_t var; in trail_print()
81 variable_t prev_var = trail->elements.data[i-1]; in trail_print()
133 void trail_set_value(mcsat_trail_t* trail, variable_t x, const mcsat_value_t* value, uint32_t id, a… in trail_set_value()
155 void trail_undo_value(mcsat_trail_t* trail, variable_t x) { in trail_undo_value()
163 void trail_add_decision(mcsat_trail_t* trail, variable_t x, const mcsat_value_t* value, uint32_t id… in trail_add_decision()
176 variable_t x; in trail_pop_decision()
194 void trail_add_propagation(mcsat_trail_t* trail, variable_t x, const mcsat_value_t* value, uint32_t… in trail_add_propagation()
206 variable_t x; in trail_pop_propagation()
242 variable_t var; in trail_gc_mark()
[all …]
H A Dmodel.c71 void mcsat_model_new_variable_notify(mcsat_model_t* m, variable_t x) { in mcsat_model_new_variable_notify()
77 bool mcsat_model_has_value(const mcsat_model_t* m, variable_t x) { in mcsat_model_has_value()
85 const mcsat_value_t* mcsat_model_get_value(const mcsat_model_t* m, variable_t x) { in mcsat_model_get_value()
93 uint32_t mcsat_model_get_value_timestamp(const mcsat_model_t* m, variable_t x) { in mcsat_model_get_value_timestamp()
101 void mcsat_model_set_value(mcsat_model_t* m, variable_t x, const mcsat_value_t* value) { in mcsat_model_set_value()
113 void mcsat_model_unset_value(mcsat_model_t* m, variable_t x) { in mcsat_model_unset_value()
/dports/math/yices/yices-2.6.2/src/mcsat/nra/
H A Dnra_plugin_internal.h47 variable_t last_decided_and_unprocessed;
59 variable_t conflict_variable;
62 variable_t conflict_variable_int;
146 int nra_plugin_variable_has_lp_variable(nra_plugin_t* nra, variable_t mcsat_var);
152 void nra_plugin_add_lp_variable(nra_plugin_t* nra, variable_t mcsat_var);
155 lp_variable_t nra_plugin_get_lp_variable(nra_plugin_t* nra, variable_t t);
158 variable_t nra_plugin_get_variable_from_lp_variable(nra_plugin_t* nra, lp_variable_t lp_var);
161 void nra_plugin_set_unit_info(nra_plugin_t* nra, variable_t constraint, variable_t unit_var, constr…
164 constraint_unit_info_t nra_plugin_get_unit_info(nra_plugin_t* nra, variable_t constraint);
167 variable_t nra_plugin_get_unit_var(nra_plugin_t* nra, variable_t constraint);
[all …]
H A Dfeasible_set_db.h44 …ol feasible_set_db_update(feasible_set_db_t* db, variable_t x, lp_feasibility_set_t* new_set, vari…
47 lp_feasibility_set_t* feasible_set_db_get(feasible_set_db_t* db, variable_t x);
56 void feasible_set_db_get_conflict_reasons(feasible_set_db_t* db, nra_plugin_t* nra, variable_t x, i…
59 variable_t feasible_set_db_get_fixed(feasible_set_db_t* db);
65 void feasible_set_db_print_var(feasible_set_db_t* db, variable_t var, FILE* out);
68 variable_t feasible_set_db_get_cheap_unassigned(feasible_set_db_t* db, lp_value_t* value);
H A Dnra_plugin_internal.c88 variable_t var; in nra_plugin_get_term_variables()
114 variable_t var = variable_db_get_variable(var_db, pprod->prod[i].var); in nra_plugin_get_term_variables()
127 void nra_plugin_set_unit_info(nra_plugin_t* nra, variable_t constraint, variable_t unit_var, constr… in nra_plugin_set_unit_info()
157 constraint_unit_info_t nra_plugin_get_unit_info(nra_plugin_t* nra, variable_t constraint) { in nra_plugin_get_unit_info()
166 variable_t nra_plugin_get_unit_var(nra_plugin_t* nra, variable_t constraint) { in nra_plugin_get_unit_var()
176 variable_t mcsat_var = variable_db_get_variable(nra->ctx->var_db, t); in nra_plugin_term_has_lp_variable()
181 int nra_plugin_variable_has_lp_variable(nra_plugin_t* nra, variable_t mcsat_var) { in nra_plugin_variable_has_lp_variable()
198 variable_t mcsat_var = variable_db_get_variable(nra->ctx->var_db, t); in nra_plugin_add_lp_variable_from_term()
207 void nra_plugin_add_lp_variable(nra_plugin_t* nra, variable_t mcsat_var) { in nra_plugin_add_lp_variable()
234 lp_variable_t nra_plugin_get_lp_variable(nra_plugin_t* nra, variable_t mcsat_var) { in nra_plugin_get_lp_variable()
[all …]
H A Dfeasible_set_db.c39 variable_t* reasons;
126 variable_t var = it->key; in feasible_set_db_print()
208 …ol feasible_set_db_update(feasible_set_db_t* db, variable_t x, lp_feasibility_set_t* new_set, vari… in feasible_set_db_update()
335 variable_t x = ivector_last(&db->updates); in feasible_set_db_pop()
434 variable_t r1_i_var = db->memory[r1].reasons[i]; in compare_reasons()
453 variable_t r2_i_var = db->memory[r2].reasons[i]; in compare_reasons()
487 variable_t r_i_var = db->memory[r_i].reasons[j]; in print_conflict_reasons()
587 variable_t reason = element->reasons[0]; in feasible_set_db_get_conflict_reasons()
593 variable_t reason = element->reasons[j]; in feasible_set_db_get_conflict_reasons()
605 variable_t best_var = variable_null; in feasible_set_db_get_cheap_unassigned()
[all …]
/dports/math/wcalc/wcalc-2.5/src/common/
H A Dvariables.c36 variable_t *freeme; in cleanupvar()
62 variable_t *cursor = NULL; in printvariables()
78 cursor = (variable_t *)nextListElement(li); in printvariables()
96 variable_t *cursor = NULL; in listvarnames()
113 variable_t *freeme; in delnvar()
127 variable_t *getrealnvar(const size_t i) in getrealnvar()
163 variable_t *var; in getvar_full()
186 variable_t *cursor = NULL; in varexists()
208 variable_t *cursor = NULL; in getvar_core()
248 variable_t *cursor = NULL; in putexp()
[all …]
/dports/security/libprelude/libprelude-1.2.6/src/
H A Dvariable.c40 } variable_t; typedef
48 static variable_t *search_entry(const char *variable) in search_entry()
52 variable_t *item = NULL; in search_entry()
55 item = prelude_list_entry(tmp, variable_t, list); in search_entry()
71 variable_t *item; in create_entry()
100 static void destroy_variable(variable_t *item) in destroy_variable()
123 variable_t *item; in variable_get()
146 variable_t *item; in variable_set()
174 variable_t *item; in variable_unset()
189 variable_t *item; in variable_unset_all()
[all …]
/dports/science/siesta/siesta-4.1.5/Src/fdict/sources/src/
H A Dvariable.f9048 type :: variable_t type
59 end type variable_t
60 public :: variable_t
382 type(variable_t), intent(in) :: this
386 type(variable_t), intent(in) :: this
799 type(variable_t), intent(in) :: rhs
804 type(variable_t), intent(in) :: rhs
1725 type(variable_t), intent(in) :: this
1745 type(variable_t), intent(in) :: this
1791 type(variable_t), intent(in) :: this
[all …]
/dports/science/siesta/siesta-4.1.5/Src/fdict/src/
H A Dvariable_pp.F9056 type :: variable_t type
68 end type variable_t
69 public :: variable_t
166 type(variable_t), intent(in) :: this
171 type(variable_t), intent(in) :: this
215 type(variable_t), intent(in) :: this
232 type(variable_t), intent(in) :: this
299 type(variable_t), intent(in) :: rhs
304 type(variable_t), intent(in) :: rhs
345 type(variable_t), intent(in) :: rhs
[all …]
H A Dvariable_funcs_inc.inc6 type(variable_t), intent(inout) :: this
35 type(variable_t), intent(in) :: this
62 type(variable_t), intent(in) :: this
117 type(variable_t), intent(in) :: this
131 type(variable_t), intent(in) :: this
149 type(variable_t), intent(in) :: this
159 type(variable_t), intent(in) :: this
165 type(variable_t), intent(in) :: this
173 type(variable_t), intent(in) :: this
179 type(variable_t), intent(in) :: this
[all …]
/dports/math/yices/yices-2.6.2/src/mcsat/bv/
H A Dbv_feasible_set_db.h45 bool bv_feasible_set_db_update(bv_feasible_set_db_t* db, variable_t x, bdd_t new_set, variable_t* r…
48 bdd_t bv_feasible_set_db_get(const bv_feasible_set_db_t* db, variable_t x);
51 const mcsat_value_t* bv_feasible_set_db_pick_value(bv_feasible_set_db_t* db, variable_t x);
67 void bv_feasible_set_db_get_reasons(const bv_feasible_set_db_t* db, variable_t x, ivector_t* reason…
70 variable_t bv_feasible_set_db_get_fixed(bv_feasible_set_db_t* db);
76 void bv_feasible_set_db_print_var(const bv_feasible_set_db_t* db, variable_t var, FILE* out);
H A Dbv_explainer.h48 …bool (*can_explain_conflict) (bv_subexplainer_t* this, const ivector_t* conflict, variable_t confl…
56 …void (*explain_conflict) (bv_subexplainer_t* this, const ivector_t* conflict_in, variable_t confli…
59 bool (*can_explain_propagation) (bv_subexplainer_t* this, const ivector_t* reasons, variable_t x);
62 …term_t (*explain_propagation) (bv_subexplainer_t* this, const ivector_t* reasons_in, variable_t x,…
102 void bv_explainer_get_conflict(bv_explainer_t* exp, const ivector_t* conflict_in, variable_t confli…
116 term_t bv_explainer_explain_propagation(bv_explainer_t* exp, variable_t x, const ivector_t* reasons…
/dports/math/yices/yices-2.6.2/src/mcsat/bool/
H A Dliteral.h46 variable_t literal_get_variable(mcsat_literal_t l) { in literal_get_variable()
52 variable_t literal_get_variable_from_index(uint32_t l_index) { in literal_get_variable_from_index()
58 mcsat_literal_t literal_construct(variable_t var, bool negated) { in literal_construct()
70 uint32_t linter_index_max(variable_t var) { in linter_index_max()
82 mcsat_literal_t literal_construct_from_trail(variable_t x, const mcsat_trail_t* trail) { in literal_construct_from_trail()
103 variable_t l_var; in literal_get_value()
131 variable_t l_var; in literal_set_value()
/dports/math/yices/yices-2.6.2/src/mcsat/bv/explain/
H A Dfull_bv_trivial.c29 bool can_explain_conflict(bv_subexplainer_t* this, const ivector_t* conflict, variable_t conflict_v… in can_explain_conflict()
35 void explain_conflict(bv_subexplainer_t* this, const ivector_t* conflict_core, variable_t conflict_… in explain_conflict()
37 variable_t atom_i_var; in explain_conflict()
60 variable_t* atom_i_vars = watch_list_manager_get_list(this->wlm, list_ref); in explain_conflict()
73 variable_t var = assigned_vars_vec->data[i]; in explain_conflict()
100 bool can_explain_propagation(bv_subexplainer_t* this, const ivector_t* reasons, variable_t x) { in can_explain_propagation()
105 term_t explain_propagation(bv_subexplainer_t* this, const ivector_t* reasons_in, variable_t x, ivec… in explain_propagation()

12345678