Searched refs:mcsat_var (Results 1 – 2 of 2) sorted by relevance
| /dports/math/yices/yices-2.6.2/src/mcsat/nra/ |
| H A D | nra_plugin_internal.c | 176 variable_t mcsat_var = variable_db_get_variable(nra->ctx->var_db, t); in nra_plugin_term_has_lp_variable() local
181 int nra_plugin_variable_has_lp_variable(nra_plugin_t* nra, variable_t mcsat_var) { in nra_plugin_variable_has_lp_variable() argument
198 variable_t mcsat_var = variable_db_get_variable(nra->ctx->var_db, t); in nra_plugin_add_lp_variable_from_term() local
201 assert(int_hmap_find(&nra->lp_data.mcsat_to_lp_var_map, mcsat_var) == NULL); in nra_plugin_add_lp_variable_from_term()
203 int_hmap_add(&nra->lp_data.lp_to_mcsat_var_map, lp_var, mcsat_var); in nra_plugin_add_lp_variable_from_term()
204 int_hmap_add(&nra->lp_data.mcsat_to_lp_var_map, mcsat_var, lp_var); 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() argument
209 term_t t = variable_db_get_term(nra->ctx->var_db, mcsat_var); in nra_plugin_add_lp_variable()
228 assert(int_hmap_find(&nra->lp_data.mcsat_to_lp_var_map, mcsat_var) == NULL); in nra_plugin_add_lp_variable()
230 int_hmap_add(&nra->lp_data.lp_to_mcsat_var_map, lp_var, mcsat_var); in nra_plugin_add_lp_variable()
[all …]
|
| H A D | nra_plugin_internal.h | 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);
|