1 /*++
2 Copyright (c) 2011 Microsoft Corporation
3 
4 Module Name:
5 
6     nlarith_util.h
7 
8 Abstract:
9 
10     Utilities for nln-linear arithmetic quantifier elimination and
11     solving.
12 
13 Author:
14 
15     Nikolaj (nbjorner) 2011-05-13
16 
17 Notes:
18 
19 --*/
20 #pragma once
21 
22 #include "ast/ast.h"
23 #include "util/lbool.h"
24 
25 namespace nlarith {
26 
27     /**
28         \brief A summary for branch side conditions and substitutions.
29 
30         Each branch in a split comprises of:
31         - preds    - a sequence of predicates used for the branching.
32         - branches - a sequence of branch side conditions
33         - subst    - a sequence of substitutions that replace 'preds' by formulas
34                      not containing the eliminated variable
35         - constraints - a sequence of side constraints to add to the main formula.
36     */
37     class branch_conditions {
38         expr_ref_vector         m_branches;
39         expr_ref_vector         m_preds;
40         vector<expr_ref_vector> m_subst;
41         expr_ref_vector         m_constraints;
42         expr_ref_vector         m_defs;
43         expr_ref_vector         m_a;
44         expr_ref_vector         m_b;
45         expr_ref_vector         m_c;
46 
47     public:
branch_conditions(ast_manager & m)48         branch_conditions(ast_manager& m) : m_branches(m), m_preds(m), m_constraints(m), m_defs(m), m_a(m), m_b(m), m_c(m) {}
add_pred(expr * p)49         void add_pred(expr* p) { m_preds.push_back(p); }
add_branch(expr * branch,expr * cond,expr_ref_vector const & subst,expr * def,expr * a,expr * b,expr * c)50         void add_branch(expr* branch, expr* cond, expr_ref_vector const& subst, expr* def, expr* a, expr* b, expr* c) {
51             m_branches.push_back(branch);
52             m_constraints.push_back(cond);
53             m_subst.push_back(subst);
54             m_defs.push_back(def);
55             m_a.push_back(a);
56             m_b.push_back(b);
57             m_c.push_back(c);
58         }
preds(unsigned i)59         expr*                          preds(unsigned i) const { return m_preds[i]; }
branches(unsigned i)60         expr*                          branches(unsigned i) const { return m_branches[i]; }
constraints(unsigned i)61         expr*                          constraints(unsigned i) const { return m_constraints[i]; }
def(unsigned i)62         expr*                          def(unsigned i) const { return m_defs[i]; }
a(unsigned i)63         expr*                          a(unsigned i) const { return m_a[i]; }
b(unsigned i)64         expr*                          b(unsigned i) const { return m_b[i]; }
c(unsigned i)65         expr*                          c(unsigned i) const { return m_c[i]; }
subst(unsigned i)66         expr_ref_vector const&         subst(unsigned i) const { return m_subst[i]; }
branches()67         expr_ref_vector const&         branches() const { return m_branches; }
preds()68         expr_ref_vector const&         preds() const  { return m_preds; }
subst()69         vector<expr_ref_vector> const& subst() const  { return m_subst; }
constraints()70         expr_ref_vector const&         constraints() const { return m_constraints; }
reset()71         void reset() {
72             m_branches.reset(); m_preds.reset(); m_subst.reset();
73             m_constraints.reset(); m_defs.reset();
74             m_a.reset(); m_b.reset(); m_c.reset();
75         }
76 
size()77         unsigned size() const { return branches().size(); }
num_preds()78         unsigned num_preds() const { return preds().size(); }
79     };
80 
81     class util {
82         class imp;
83         imp* m_imp;
84     public:
85         util(ast_manager& m);
86         ~util();
87 
88         /**
89            \brief Enable handling of linear variables.
90         */
91         void set_enable_linear(bool enable_linear);
92 
93         /**
94            \brief Create branches for non-linear variable x.
95         */
96         bool create_branches(app* x, unsigned nl, expr* const* lits, branch_conditions& bc);
97         /**
98            \brief Extract non-linear variables from ground formula.
99         */
100         void extract_non_linear(expr* e, ptr_vector<app>& nl_vars);
101 
102         /**
103            \brief literal sets. Opaque state.
104         */
105 
106         class literal_set;
107 
108         static void deallocate(literal_set* lits);
109 
110 
111 
112         /**
113            \brief Sign-based branching. v2.
114         */
115         typedef obj_hashtable<app> atoms;
116 
117         class eval {
118         public:
~eval()119             virtual ~eval() {}
120             virtual lbool operator()(app* a) = 0;
121         };
122 
123         enum atom_update { INSERT, REMOVE };
124 
125         class branch {
126         public:
~branch()127             virtual ~branch() {}
128             virtual app* get_constraint() = 0;
129             virtual void get_updates(ptr_vector<app>& atoms, svector<atom_update>& updates) = 0;
130         };
131 
132         /**
133             \brief select literals that contain non-linear variables.
134         */
135         bool get_sign_literals(atoms const& atoms, eval& eval, literal_set*& lits);
136 
137         /**
138             \brief given selected literals, generate branch conditions.
139         */
140         void get_sign_branches(literal_set& lits, eval& eval, ptr_vector<branch>& branches);
141 
142 
143 
144     };
145 
146 };
147 
148