1 /* 2 * This file is part of the Yices SMT Solver. 3 * Copyright (C) 2017 SRI International. 4 * 5 * Yices is free software: you can redistribute it and/or modify 6 * it under the terms of the GNU General Public License as published by 7 * the Free Software Foundation, either version 3 of the License, or 8 * (at your option) any later version. 9 * 10 * Yices is distributed in the hope that it will be useful, 11 * but WITHOUT ANY WARRANTY; without even the implied warranty of 12 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the 13 * GNU General Public License for more details. 14 * 15 * You should have received a copy of the GNU General Public License 16 * along with Yices. If not, see <http://www.gnu.org/licenses/>. 17 */ 18 19 #pragma once 20 21 #include <poly/poly.h> 22 #include <stdio.h> 23 24 #include "mcsat/variable_db.h" 25 #include "mcsat/mcsat_types.h" 26 27 typedef struct nra_plugin_s nra_plugin_t; 28 29 /** Contains the map from variables to feasible sets that can be backtracked */ 30 typedef struct feasible_set_db_struct feasible_set_db_t; 31 32 /** Create a new database */ 33 feasible_set_db_t* feasible_set_db_new(plugin_context_t* ctx); 34 35 /** Delete the database */ 36 void feasible_set_db_delete(feasible_set_db_t* db); 37 38 /** 39 * Update the feasible set of the variable with a new set. The new set is kept 40 * if it reduces the existing feasible set. Returns true if consistent. 41 * 42 * If more than one reason, it's considered a disjunctive top-level assertion (clause); 43 */ 44 bool feasible_set_db_update(feasible_set_db_t* db, variable_t x, lp_feasibility_set_t* new_set, variable_t* reasons, uint32_t reasons_count); 45 46 /** Get the feasible set of a variable */ 47 lp_feasibility_set_t* feasible_set_db_get(feasible_set_db_t* db, variable_t x); 48 49 /** Push the context */ 50 void feasible_set_db_push(feasible_set_db_t* db); 51 52 /** Pop the context */ 53 void feasible_set_db_pop(feasible_set_db_t* db); 54 55 /** Get the reason for a conflict on x. Feasible set of x should be empty. */ 56 void feasible_set_db_get_conflict_reasons(feasible_set_db_t* db, nra_plugin_t* nra, variable_t x, ivector_t* reasons_out, ivector_t* lemma_reasons_out); 57 58 /** Return any fixed variables */ 59 variable_t feasible_set_db_get_fixed(feasible_set_db_t* db); 60 61 /** Print the feasible set database */ 62 void feasible_set_db_print(feasible_set_db_t* db, FILE* out); 63 64 /** Print the feasible sets of given variable */ 65 void feasible_set_db_print_var(feasible_set_db_t* db, variable_t var, FILE* out); 66 67 /** Returns an unassigned variable with a value in its feasible set, or variable_null otherwise */ 68 variable_t feasible_set_db_get_cheap_unassigned(feasible_set_db_t* db, lp_value_t* value); 69 70 /** Marks all the top level reasons */ 71 void feasible_set_db_gc_mark(feasible_set_db_t* db, gc_info_t* gc_vars); 72