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 <stdio.h> 22 #include <poly/polynomial.h> 23 #include <poly/sign_condition.h> 24 25 #include "mcsat/nra/nra_plugin_internal.h" 26 #include "utils/int_hash_map.h" 27 28 /** Construct a regular constraint, takes over the polynomial */ 29 void poly_constraint_construct_regular(poly_constraint_t* cstr, lp_polynomial_t* p, lp_sign_condition_t sgn_contition); 30 31 /** Construct a root constraint */ 32 void poly_constraint_construct_root(poly_constraint_t* cstr, lp_polynomial_t* p, lp_sign_condition_t sgn_contition, lp_variable_t x, uint32_t root_index); 33 34 /** Allocate and construct the constraint, takes over the polynomial */ 35 poly_constraint_t* poly_constraint_new_regular(lp_polynomial_t* p, lp_sign_condition_t sgn_contition); 36 37 /** Allocate and construct the constraint, takes over the polynomial */ 38 poly_constraint_t* poly_constraint_new_root(lp_polynomial_t* p, lp_sign_condition_t sgn_contition, lp_variable_t x, uint32_t root_index); 39 40 /** Destruct the constraint */ 41 void poly_constraint_destruct(poly_constraint_t* cstr); 42 43 /** Destruct and free the constraint */ 44 void poly_constraint_delete(poly_constraint_t* cstr); 45 46 /** Print the constraint */ 47 void poly_constraint_print(const poly_constraint_t* cstr, FILE* out); 48 49 /** Print the constraint to mathematica */ 50 void poly_constraint_print_mathematica(const poly_constraint_t* cstr, bool neageted, FILE* out); 51 52 /** Get the feasible set of the constraint */ 53 lp_feasibility_set_t* poly_constraint_get_feasible_set(const poly_constraint_t* cstr, const lp_assignment_t* m, bool negated); 54 55 /** 56 * Is this a valid constraint in the current order. 57 */ 58 bool poly_constraint_is_valid(const poly_constraint_t* cstr); 59 60 /** 61 * Evaluate the constraint. Returns the value, and sets the level to the level of the constraint. 62 * recomputed. The return value is true if evaluation is OK. If return value is false, 63 * it means that the top variable of a root constraint is not top anymore, so we 64 * can ignore it. 65 */ 66 bool poly_constraint_evaluate(const poly_constraint_t* cstr, nra_plugin_t* nra, bool* value_out); 67 68 /** Get the top variable of the constraint */ 69 lp_variable_t poly_constraint_get_top_variable(const poly_constraint_t* cstr); 70 71 /** Get the sign condition of the constraint */ 72 lp_sign_condition_t poly_constraint_get_sign_condition(const poly_constraint_t* cstr); 73 74 /** Get the polynomial of the constraint */ 75 const lp_polynomial_t* poly_constraint_get_polynomial(const poly_constraint_t* cstr); 76 77 /** Is this a root constraint */ 78 bool poly_constraint_is_root_constraint(const poly_constraint_t* cstr); 79 80 /** Get the variable of the root constraint */ 81 lp_variable_t poly_constraint_get_variable(const poly_constraint_t* cstr); 82 83 /** Get the root index (if a root constraint) */ 84 uint32_t poly_constraint_get_root_index(const poly_constraint_t* cstr); 85 86 /** Construct the database */ 87 void poly_constraint_db_construct(poly_constraint_db_t* db, nra_plugin_t* nra); 88 89 /** Construct the database */ 90 poly_constraint_db_t* poly_constraint_db_new(nra_plugin_t* nra); 91 92 /** Destruct the database */ 93 void poly_constraint_db_destruct(poly_constraint_db_t* db); 94 95 /** Delete the database */ 96 void poly_constraint_db_delete(poly_constraint_db_t* db); 97 98 /** Get the constraint of the variable (must exist) */ 99 const poly_constraint_t* poly_constraint_db_get(poly_constraint_db_t* db, variable_t constraint_var); 100 101 /** Add a new constraint */ 102 void poly_constraint_db_add(poly_constraint_db_t* db, variable_t constraint_var); 103 104 /** Mark all the variables from the constraints */ 105 void poly_constraint_db_gc_mark(poly_constraint_db_t* db, gc_info_t* gc_vars); 106 107 /** Remove unised constraints */ 108 void poly_constraint_db_gc_sweep(poly_constraint_db_t* db, const gc_info_t* gc_vars); 109