1 /*++ 2 Copyright (c) 2015 Microsoft Corporation 3 4 Module Name: 5 6 qsat.h 7 8 Abstract: 9 10 Quantifier Satisfiability Solver. 11 12 Author: 13 14 Nikolaj Bjorner (nbjorner) 2015-5-28 15 16 Revision History: 17 18 19 --*/ 20 21 #pragma once 22 23 #include "tactic/tactic.h" 24 #include "tactic/generic_model_converter.h" 25 #include "qe/qe_mbp.h" 26 27 namespace qe { 28 29 struct max_level { 30 unsigned m_ex, m_fa; max_levelmax_level31 max_level(): m_ex(UINT_MAX), m_fa(UINT_MAX) {} mergemax_level32 void merge(max_level const& other) { 33 merge(m_ex, other.m_ex); 34 merge(m_fa, other.m_fa); 35 } maxmax_level36 static unsigned max(unsigned a, unsigned b) { 37 if (a == UINT_MAX) return b; 38 if (b == UINT_MAX) return a; 39 return std::max(a, b); 40 } maxmax_level41 unsigned max() const { 42 return max(m_ex, m_fa); 43 } mergemax_level44 void merge(unsigned& lvl, unsigned other) { 45 lvl = max(lvl, other); 46 } displaymax_level47 std::ostream& display(std::ostream& out) const { 48 if (m_ex != UINT_MAX) out << "e" << m_ex << " "; 49 if (m_fa != UINT_MAX) out << "a" << m_fa << " "; 50 return out; 51 } 52 53 bool operator==(max_level const& other) const { 54 return 55 m_ex == other.m_ex && 56 m_fa == other.m_fa; 57 } 58 }; 59 60 inline std::ostream& operator<<(std::ostream& out, max_level const& lvl) { 61 return lvl.display(out); 62 } 63 64 class pred_abs { 65 ast_manager& m; 66 vector<app_ref_vector> m_preds; 67 expr_ref_vector m_asms; 68 unsigned_vector m_asms_lim; 69 obj_map<expr, expr*> m_pred2lit; // maintain definitions of predicates. 70 obj_map<expr, app*> m_lit2pred; // maintain reverse mapping to predicates 71 obj_map<expr, app*> m_asm2pred; // maintain map from assumptions to predicates 72 obj_map<expr, expr*> m_pred2asm; // predicates |-> assumptions 73 expr_ref_vector m_trail; 74 generic_model_converter_ref m_fmc; 75 ptr_vector<expr> todo; 76 obj_map<expr, max_level> m_elevel; 77 obj_map<func_decl, max_level> m_flevel; 78 79 template <typename T> dec_keys(obj_map<expr,T * > & map)80 void dec_keys(obj_map<expr, T*>& map) { 81 typename obj_map<expr, T*>::iterator it = map.begin(), end = map.end(); 82 for (; it != end; ++it) { 83 m.dec_ref(it->m_key); 84 } 85 } 86 void add_lit(app* p, app* lit); 87 void add_asm(app* p, expr* lit); 88 bool is_predicate(app* a, unsigned l); 89 void mk_concrete(expr_ref_vector& fmls, obj_map<expr, expr*> const& map); 90 public: 91 92 pred_abs(ast_manager& m); 93 generic_model_converter* fmc(); 94 void reset(); 95 max_level compute_level(app* e); 96 void push(); 97 void pop(unsigned num_scopes); 98 void insert(app* a, max_level const& lvl); 99 void insert_var(app* v, max_level const& lvl); 100 void get_assumptions(model* mdl, expr_ref_vector& asms); 101 void ensure_expr_level(app* v, unsigned lvl); 102 void set_expr_level(app* v, max_level const& lvl); 103 void set_decl_level(func_decl* v, max_level const& lvl); 104 void abstract_atoms(expr* fml, max_level& level, expr_ref_vector& defs); 105 void abstract_atoms(expr* fml, expr_ref_vector& defs); 106 expr_ref mk_abstract(expr* fml); 107 void pred2lit(expr_ref_vector& fmls); 108 expr_ref pred2asm(expr* fml); 109 void get_free_vars(expr* fml, app_ref_vector& vars); 110 expr_ref mk_assumption_literal(expr* a, model* mdl, max_level const& lvl, expr_ref_vector& defs); 111 void add_pred(app* p, app* lit); 112 app_ref fresh_bool(char const* name); 113 void display(std::ostream& out) const; 114 void display(std::ostream& out, expr_ref_vector const& asms) const; 115 void collect_statistics(statistics& st) const; 116 117 bool validate_defs(model& model) const; 118 }; 119 120 class qmax { 121 struct imp; 122 imp* m_imp; 123 public: 124 qmax(ast_manager& m, params_ref const& p = params_ref()); 125 ~qmax(); 126 lbool operator()(expr_ref_vector const& fmls, app* t, opt::inf_eps& value, model_ref& mdl); 127 void collect_statistics(statistics& st) const; 128 }; 129 130 lbool maximize(expr_ref_vector const& fmls, app* t, opt::inf_eps& value, model_ref& mdl, params_ref const& p); 131 132 } 133 134 tactic * mk_qsat_tactic(ast_manager & m, params_ref const& p = params_ref()); 135 136 tactic * mk_qe2_tactic(ast_manager & m, params_ref const& p = params_ref()); 137 138 tactic * mk_qe_rec_tactic(ast_manager & m, params_ref const& p = params_ref()); 139 140 141 /* 142 ADD_TACTIC("qsat", "apply a QSAT solver.", "mk_qsat_tactic(m, p)") 143 144 ADD_TACTIC("qe2", "apply a QSAT based quantifier elimination.", "mk_qe2_tactic(m, p)") 145 146 ADD_TACTIC("qe_rec", "apply a QSAT based quantifier elimination recursively.", "mk_qe_rec_tactic(m, p)") 147 148 */ 149 150