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