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