/dports/math/yices/yices-2.6.2/src/mcsat/ |
H A D | variable_db.h | 32 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 D | watch_list_manager.h | 88 …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 D | variable_queue.h | 56 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 D | trail.h | 96 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 D | variable_queue.c | 39 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 D | watch_list_manager.c | 56 …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 D | model.h | 47 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 D | variable_db.c | 55 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 D | plugin.h | 102 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 D | conflict.h | 143 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 D | trail.c | 53 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 D | model.c | 71 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 D | nra_plugin_internal.h | 47 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 D | feasible_set_db.h | 44 …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 D | nra_plugin_internal.c | 88 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 D | feasible_set_db.c | 39 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 D | variables.c | 36 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 D | variable.c | 40 } 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 D | variable.f90 | 48 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 D | variable_pp.F90 | 56 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 D | variable_funcs_inc.inc | 6 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 D | bv_feasible_set_db.h | 45 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 D | bv_explainer.h | 48 …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 D | literal.h | 46 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 D | full_bv_trivial.c | 29 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()
|