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