1 /*++
2 Copyright (c) 2011 Microsoft Corporation
3 
4 Module Name:
5 
6     spacer_util.h
7 
8 Abstract:
9 
10     Utility functions for SPACER.
11 
12 Author:
13 
14     Krystof Hoder (t-khoder) 2011-8-19.
15     Arie Gurfinkel
16     Anvesh Komuravelli
17 
18 Revision History:
19 
20 --*/
21 
22 #pragma once
23 
24 #include "ast/ast.h"
25 #include "ast/ast_pp.h"
26 #include "util/obj_hashtable.h"
27 #include "util/ref_vector.h"
28 #include "util/trace.h"
29 #include "util/vector.h"
30 #include "ast/arith_decl_plugin.h"
31 #include "ast/array_decl_plugin.h"
32 #include "ast/bv_decl_plugin.h"
33 #include "ast/ast_util.h"
34 #include "ast/expr_map.h"
35 #include "model/model.h"
36 
37 #include "util/stopwatch.h"
38 #include "muz/spacer/spacer_antiunify.h"
39 
40 class model;
41 class model_core;
42 
43 namespace spacer {
44 
infty_level()45     inline unsigned infty_level () {
46         return UINT_MAX;
47     }
48 
is_infty_level(unsigned lvl)49     inline bool is_infty_level(unsigned lvl) {
50         // XXX: level is 16 bits in class pob
51         return lvl >= 65535;
52     }
53 
next_level(unsigned lvl)54     inline unsigned next_level(unsigned lvl) {
55         return is_infty_level(lvl)?lvl:(lvl+1);
56     }
57 
prev_level(unsigned lvl)58     inline unsigned prev_level (unsigned lvl) {
59         if (is_infty_level(lvl)) return infty_level();
60         if (lvl == 0) return 0;
61         return lvl - 1;
62     }
63 
64     struct pp_level {
65         unsigned m_level;
pp_levelpp_level66         pp_level(unsigned l): m_level(l) {}
67     };
68 
69     inline std::ostream& operator<<(std::ostream& out, pp_level const& p) {
70         if (is_infty_level(p.m_level)) {
71             return out << "oo";
72         } else {
73             return out << p.m_level;
74         }
75     }
76 
77     typedef ptr_vector<app> app_vector;
78     typedef ptr_vector<func_decl> decl_vector;
79     typedef obj_hashtable<func_decl> func_decl_set;
80 
81     /**
82        \brief hoist non-boolean if expressions.
83     */
84 
85     void to_mbp_benchmark(std::ostream &out, const expr* fml, const app_ref_vector &vars);
86 
87 
88     // TBD: deprecate by qe::mbp
89     /**
90      * do the following in sequence
91      * 1. use qe_lite to cheaply eliminate vars
92      * 2. for remaining boolean vars, substitute using M
93      * 3. use MBP for remaining array and arith variables
94      * 4. for any remaining arith variables, substitute using M
95      */
96     void qe_project (ast_manager& m, app_ref_vector& vars,
97                      expr_ref& fml, model &mdl,
98                      bool reduce_all_selects=false,
99                      bool native_mbp=false,
100                      bool dont_sub=false);
101 
102     // deprecate
103     void qe_project (ast_manager& m, app_ref_vector& vars, expr_ref& fml,
104                      model_ref& M, expr_map& map);
105 
106     // TBD: sort out
107     void expand_literals(ast_manager &m, expr_ref_vector& conjs);
108     expr_ref_vector compute_implicant_literals(model &mdl,
109                                     expr_ref_vector &formula);
110     void simplify_bounds (expr_ref_vector &lemmas);
111     void normalize(expr *e, expr_ref &out, bool use_simplify_bounds = true, bool factor_eqs = false);
112 
113     /**
114      * Ground expression by replacing all free variables by skolem
115      * constants. On return, out is the resulting expression, and vars is
116      * a map from variable ids to corresponding skolem constants.
117      */
118     void ground_expr (expr *e, expr_ref &out, app_ref_vector &vars);
119 
120     void mbqi_project(model &mdl, app_ref_vector &vars, expr_ref &fml);
121 
122     bool contains_selects (expr* fml, ast_manager& m);
123     void get_select_indices (expr* fml, app_ref_vector& indices);
124 
125     void find_decls (expr* fml, app_ref_vector& decls, std::string& prefix);
126 
127     /**
128      * extended pretty-printer
129      * used for debugging
130      * disables aliasing of common sub-expressions
131      */
132     struct mk_epp : public mk_pp {
133         params_ref m_epp_params;
134         expr_ref m_epp_expr;
135     mk_epp(ast *t, ast_manager &m, unsigned indent = 0, unsigned num_vars = 0, char const * var_prefix = nullptr);
136         void rw(expr *e, expr_ref &out);
137     };
138 
139     bool is_clause(ast_manager &m, expr *n);
140     bool is_literal(ast_manager &m, expr *n);
141     bool is_atom(ast_manager &m, expr *n);
142 
143     // set f to true in model
144     void set_true_in_mdl(model &model, func_decl *f);
145 }
146 
147