1 /*++ 2 Copyright (c) 2006 Microsoft Corporation 3 4 Module Name: 5 6 grobner.h 7 8 Abstract: 9 10 <abstract> 11 12 Author: 13 14 Leonardo de Moura (leonardo) 2008-12-04. 15 16 Revision History: 17 18 --*/ 19 #pragma once 20 21 #include "ast/ast.h" 22 #include "ast/arith_decl_plugin.h" 23 #include "util/heap.h" 24 #include "util/obj_hashtable.h" 25 #include "util/region.h" 26 #include "util/dependency.h" 27 28 29 struct grobner_stats { 30 long m_simplify; long m_superpose; long m_compute_basis; long m_num_processed; resetgrobner_stats31 void reset() { memset(this, 0, sizeof(grobner_stats)); } grobner_statsgrobner_stats32 grobner_stats() { reset(); } 33 }; 34 35 36 /** 37 \brief Simple Grobner basis implementation with no indexing. 38 */ 39 class grobner { 40 protected: 41 struct monomial_lt; 42 public: 43 grobner_stats m_stats; 44 class monomial { 45 rational m_coeff; 46 ptr_vector<expr> m_vars; //!< sorted variables 47 48 friend class grobner; 49 friend struct monomial_lt; 50 monomial()51 monomial() {} 52 public: get_coeff()53 rational const & get_coeff() const { return m_coeff; } get_degree()54 unsigned get_degree() const { return m_vars.size(); } get_size()55 unsigned get_size() const { return get_degree(); } get_var(unsigned idx)56 expr * get_var(unsigned idx) const { return m_vars[idx]; } 57 }; 58 59 class equation { 60 unsigned m_scope_lvl; //!< scope level when this equation was created. 61 unsigned m_bidx:31; //!< position at m_equations_to_delete 62 unsigned m_lc:1; //!< true if equation if a linear combination of the input equations. 63 ptr_vector<monomial> m_monomials; //!< sorted monomials 64 v_dependency * m_dep; //!< justification for the equality 65 friend class grobner; equation()66 equation() {} 67 public: get_num_monomials()68 unsigned get_num_monomials() const { return m_monomials.size(); } get_monomial(unsigned idx)69 monomial const * get_monomial(unsigned idx) const { return m_monomials[idx]; } get_monomials()70 monomial * const * get_monomials() const { return m_monomials.data(); } get_dependency()71 v_dependency * get_dependency() const { return m_dep; } hash()72 unsigned hash() const { return m_bidx; } is_linear_combination()73 bool is_linear_combination() const { return m_lc; } 74 }; 75 76 protected: 77 static bool is_eq_monomial_body(monomial const * m1, monomial const * m2); 78 79 struct var_lt { 80 obj_map<expr, int> & m_var2weight; var_ltvar_lt81 var_lt(obj_map<expr, int> & m):m_var2weight(m) {} 82 bool operator()(expr * v1, expr * v2) const; 83 }; 84 85 struct monomial_lt { 86 var_lt & m_var_lt; monomial_ltmonomial_lt87 monomial_lt(var_lt & lt):m_var_lt(lt) {} 88 bool operator()(monomial * m1, monomial * m2) const; 89 }; 90 91 typedef obj_hashtable<equation> equation_set; 92 typedef ptr_vector<equation> equation_vector; 93 94 ast_manager & m_manager; 95 v_dependency_manager & m_dep_manager; 96 arith_util m_util; 97 obj_map<expr, int> m_var2weight; 98 var_lt m_var_lt; 99 monomial_lt m_monomial_lt; 100 equation_set m_processed; 101 equation_set m_to_process; 102 equation_vector m_equations_to_unfreeze; 103 equation_vector m_equations_to_delete; 104 bool m_changed_leading_term; // set to true, if the leading term was simplified. 105 equation * m_unsat; 106 struct scope { 107 unsigned m_equations_to_unfreeze_lim; 108 unsigned m_equations_to_delete_lim; 109 }; 110 svector<scope> m_scopes; 111 ptr_vector<monomial> m_tmp_monomials; 112 ptr_vector<monomial> m_del_monomials; 113 ptr_vector<expr> m_tmp_vars1; 114 ptr_vector<expr> m_tmp_vars2; 115 unsigned m_num_new_equations; // temporary variable 116 117 bool is_monomial_lt(monomial const & m1, monomial const & m2) const; 118 119 void display_vars(std::ostream & out, unsigned num_vars, expr * const * vars) const; 120 121 void display_var(std::ostream & out, expr * var) const; 122 123 void display_monomials(std::ostream & out, unsigned num_monomials, monomial * const * monomials) const; 124 125 void display_equations(std::ostream & out, equation_set const & v, char const * header) const; 126 127 void del_equations(unsigned old_size); 128 129 void del_monomials(ptr_vector<monomial>& monomials); 130 131 void unfreeze_equations(unsigned old_size); 132 133 void del_equation(equation * eq); 134 135 void flush(); 136 137 bool update_order(equation * eq); 138 139 void update_order(equation_set & s, bool processed); 140 141 void add_var(monomial * m, expr * v); 142 143 monomial * mk_monomial(rational const & coeff, expr * m); 144 145 void init_equation(equation * eq, v_dependency * d); 146 147 void extract_monomials(expr * lhs, ptr_buffer<expr> & monomials); 148 149 void merge_monomials(ptr_vector<monomial> & monomials); 150 151 bool is_inconsistent(equation * eq) const; 152 153 bool is_trivial(equation * eq) const; 154 155 void normalize_coeff(ptr_vector<monomial> & monomials); 156 157 void simplify(ptr_vector<monomial> & monomials); 158 159 void simplify(equation * eq); 160 161 bool is_subset(monomial const * m1, monomial const * m2, ptr_vector<expr> & rest) const; 162 163 void mul_append(unsigned start_idx, equation const * source, rational const & coeff, ptr_vector<expr> const & vars, ptr_vector<monomial> & result); 164 165 monomial * copy_monomial(monomial const * m); 166 167 equation * copy_equation(equation const * eq); 168 169 equation * simplify(equation const * source, equation * target); 170 171 equation * simplify_using_processed(equation * eq); 172 173 bool is_better_choice(equation * eq1, equation * eq2); 174 175 equation * pick_next(); 176 177 bool simplify_processed(equation * eq); 178 179 void simplify_to_process(equation * eq); 180 181 bool unify(monomial const * m1, monomial const * m2, ptr_vector<expr> & rest1, ptr_vector<expr> & rest2); 182 183 void superpose(equation * eq1, equation * eq2); 184 185 void superpose(equation * eq); 186 187 void copy_to(equation_set const & s, ptr_vector<equation> & result) const; 188 189 public: 190 grobner(ast_manager & m, v_dependency_manager & dep_m); 191 192 ~grobner(); 193 get_scope_level()194 unsigned get_scope_level() const { return m_scopes.size(); } 195 196 /** 197 \brief Set the weight of a term that is viewed as a variable by this module. 198 The weight is used to order monomials. If the weight is not set for a term t, then the 199 weight of t is assumed to be 0. 200 */ 201 void set_weight(expr * n, int weight); 202 get_weight(expr * n)203 int get_weight(expr * n) const { int w = 0; m_var2weight.find(n, w); return w; } 204 205 /** 206 \brief Update equations after set_weight was invoked once or more. 207 */ 208 void update_order(); 209 210 /** 211 \brief Create a new monomial. The caller owns the monomial until it invokes assert_eq_0. 212 A monomial cannot be use to create several equations. 213 */ 214 monomial * mk_monomial(rational const & coeff, unsigned num_vars, expr * const * vars); 215 216 void del_monomial(monomial * m); 217 218 /** 219 \brief Assert the given equality. 220 This method assumes eq is simplified. 221 */ 222 void assert_eq(expr * eq, v_dependency * ex = nullptr); 223 224 /** 225 \brief Assert the equality monomials[0] + ... + monomials[num_monomials - 1] = 0. 226 This method assumes the monomials were simplified. 227 */ 228 void assert_eq_0(unsigned num_monomials, expr * const * monomials, v_dependency * ex = nullptr); 229 230 /** 231 \brief Assert the equality monomials[0] + ... + monomials[num_monomials - 1] = 0. 232 This method assumes the monomials were simplified. 233 */ 234 void assert_eq_0(unsigned num_monomials, monomial * const * monomials, v_dependency * ex = nullptr); 235 236 /** 237 \brief Assert the equality coeffs[0] * monomials[0] + ... + coeffs[num_monomials-1] * monomials[num_monomials - 1] = 0. 238 This method assumes the monomials were simplified. 239 */ 240 void assert_eq_0(unsigned num_monomials, rational const * coeffs, expr * const * monomials, v_dependency * ex = nullptr); 241 242 /** 243 \brief Assert the monomial tautology (quote (x_1 * ... * x_n)) - x_1 * ... * x_n = 0 244 */ 245 void assert_monomial_tautology(expr * m); 246 247 /** 248 \brief Compute Grobner basis. 249 Return true if the threshold was not reached. 250 */ 251 bool compute_basis(unsigned threshold); 252 253 /** 254 \brief Compute one step Grobner basis. 255 Return true if there is no new equation to take. 256 */ 257 void compute_basis_init(); 258 bool compute_basis_step(); get_num_new_equations()259 unsigned get_num_new_equations() { return m_num_new_equations; } 260 261 262 /** 263 \brief Return true if an inconsistency was detected. 264 */ inconsistent()265 bool inconsistent() const { return m_unsat != nullptr; } 266 267 /** 268 \brief Simplify the given expression using the equalities asserted 269 using assert_eq. Store the result in 'result'. 270 */ 271 void simplify(expr * n, expr_ref & result); 272 273 /** 274 \brief Reset state. Remove all equalities asserted with assert_eq. 275 */ 276 void reset(); 277 278 void get_equations(ptr_vector<equation> & result) const; 279 280 void push_scope(); 281 282 void pop_scope(unsigned num_scopes); 283 284 void display_equation(std::ostream & out, equation const & eq) const; 285 286 void display_monomial(std::ostream & out, monomial const & m) const; 287 288 void display(std::ostream & out) const; 289 }; 290 291 292