1 /*++ 2 Copyright (c) 2011 Microsoft Corporation 3 4 Module Name: 5 6 expr2polynomial.h 7 8 Abstract: 9 10 Translator from Z3 expressions into multivariate polynomials (and back). 11 12 13 Author: 14 15 Leonardo (leonardo) 2011-12-23 16 17 Notes: 18 19 --*/ 20 #pragma once 21 22 #include "ast/ast.h" 23 #include "math/polynomial/polynomial.h" 24 25 class expr2var; 26 27 class expr2polynomial { 28 struct imp; 29 imp * m_imp; 30 public: 31 expr2polynomial(ast_manager & am, 32 polynomial::manager & pm, 33 expr2var * e2v, 34 /* 35 If true, the expressions converted into 36 polynomials should only contain Z3 free variables. 37 A Z3 variable x, with idx i, is converted into 38 the variable i of the polynomial manager pm. 39 40 An exception is thrown if there is a mismatch between 41 the sorts x and the variable in the polynomial manager. 42 43 The argument e2v is ignored when use_var_idxs is true. 44 45 Moreover, only real variables are allowed. 46 */ 47 bool use_var_idxs = false 48 ); 49 virtual ~expr2polynomial(); 50 51 ast_manager & m() const; 52 polynomial::manager & pm() const; 53 54 /** 55 \brief Convert a Z3 expression into a polynomial in Z[x0, ..., x_n]. 56 Since Z3 expressions may be representing polynomials in Q[x0, ..., x_n], 57 the method also returns a "denominator" d. 58 Thus, we have that n is equal to p/d 59 60 \remark Return false if t is not an integer or real expression. 61 62 \pre The only supported operators are MUL, ADD, SUB, UMINUS, TO_REAL, TO_INT, POWER (with constants) 63 */ 64 bool to_polynomial(expr * t, polynomial::polynomial_ref & p, polynomial::scoped_numeral & d); 65 66 /** 67 \brief Convert a polynomial into a Z3 expression. 68 69 \remark If the polynomial has one real variable, then the resultant 70 expression is an real expression. Otherwise, it is an integer 71 */ 72 void to_expr(polynomial::polynomial_ref const & p, bool use_power, expr_ref & r); 73 74 /** 75 \brief Return true if t was encoded as a variable by the translator. 76 */ 77 bool is_var(expr * t) const; 78 79 80 /** 81 \brief Return the mapping from expressions to variables 82 83 \pre the object was created using use_var_idxs = false. 84 */ 85 expr2var const & get_mapping() const; 86 87 /** 88 \brief Cancel/Interrupt execution. 89 */ 90 void set_cancel(bool f); 91 92 /** 93 \brief Return true if the variable is associated with an expression of integer sort. 94 */ is_int(polynomial::var x)95 virtual bool is_int(polynomial::var x) const { UNREACHABLE(); return false; } 96 97 protected: mk_var(bool is_int)98 virtual polynomial::var mk_var(bool is_int) { UNREACHABLE(); return polynomial::null_var; } 99 }; 100 101 class default_expr2polynomial : public expr2polynomial { 102 bool_vector m_is_int; 103 public: 104 default_expr2polynomial(ast_manager & am, polynomial::manager & pm); 105 ~default_expr2polynomial() override; 106 bool is_int(polynomial::var x) const override; 107 protected: 108 polynomial::var mk_var(bool is_int) override; 109 }; 110 111