1 /*++
2 Copyright (c) 2018 Microsoft Corporation
3 
4 Module Name:
5 
6     qe_mbi.h
7 
8 Abstract:
9 
10     Model-based interpolation utilities
11 
12 Author:
13 
14     Nikolaj Bjorner (nbjorner), Arie Gurfinkel 2018-6-8
15 
16 Revision History:
17 
18 
19 --*/
20 
21 #pragma once
22 
23 #include "qe/mbp/mbp_arith.h"
24 #include "qe/mbp/mbp_plugin.h"
25 #include "util/lbool.h"
26 
27 namespace qe {
28     enum mbi_result {
29         mbi_sat,
30         mbi_unsat,
31         mbi_augment,
32         mbi_undef,
33     };
34 
35     class mbi_plugin {
36     protected:
37         ast_manager& m;
38         func_decl_ref_vector     m_shared_trail;
39         obj_hashtable<func_decl> m_shared;
40         svector<lbool>           m_is_shared;
41         std::function<expr*(expr*)> m_rep;
42 
43         lbool is_shared_cached(expr* e);
44     public:
mbi_plugin(ast_manager & m)45         mbi_plugin(ast_manager& m): m(m), m_shared_trail(m) {}
~mbi_plugin()46         virtual ~mbi_plugin() {}
47 
48         /**
49          * Set the shared symbols.
50          */
set_shared(func_decl_ref_vector const & vars)51         void set_shared(func_decl_ref_vector const& vars) {
52             m_shared_trail.reset();
53             m_shared.reset();
54             m_is_shared.reset();
55             m_shared_trail.append(vars);
56             for (auto* f : vars) m_shared.insert(f);
57         }
58 
59         void set_shared(expr* a, expr* b);
60 
61         /**
62          * Set representative (shared) expression finder.
63          */
set_rep(std::function<expr * (expr *)> & rep)64         void set_rep(std::function<expr*(expr*)>& rep) { m_rep = rep; }
65 
66         /**
67          * determine whether expression/function is shared.
68          */
69         bool is_shared(expr* e);
70         bool is_shared(func_decl* f);
71 
72         /**
73          * \brief Utility that works modulo a background state.
74          * - vars
75          *   variables to preferably project onto (other variables would require quantification to fit interpolation signature)
76          * - lits
77          *   set of literals to check satisfiability with respect to.
78          * - mdl
79          *   optional model for caller.
80          * on return:
81          * - mbi_sat:
82          *   populates mdl with a satisfying state, and lits with implicant for background state.
83          * - mbi_unsat:
84          *   populates lits to be inconsistent with background state.
85          *   For all practical purposes it is a weakening of lits or even a subset of lits.
86          * - mbi_augment:
87          *   populates lits with strengthening of lits (superset)
88          * - mbi_undef:
89          *   inconclusive,
90          */
91         virtual mbi_result operator()(expr_ref_vector& lits, model_ref& mdl) = 0;
92 
93         /**
94          * \brief Block conjunction of lits from future mbi_augment or mbi_sat.
95          */
96         virtual void block(expr_ref_vector const& lits) = 0;
97 
98         /**
99          * \brief perform a full check, consume internal auguments if necessary.
100          */
101         lbool check(expr_ref_vector& lits, model_ref& mdl);
102 
103     };
104 
105     class prop_mbi_plugin : public mbi_plugin {
106         solver_ref m_solver;
107     public:
108         prop_mbi_plugin(solver* s);
~prop_mbi_plugin()109         ~prop_mbi_plugin() override {}
110         mbi_result operator()(expr_ref_vector& lits, model_ref& mdl) override;
111         void block(expr_ref_vector const& lits) override;
112     };
113 
114     class uflia_mbi : public mbi_plugin {
115         expr_ref_vector     m_atoms;
116         obj_hashtable<expr> m_atom_set;
117         expr_ref_vector     m_fmls;
118         solver_ref          m_solver;
119         solver_ref          m_dual_solver;
120         struct is_atom_proc;
121 
122         bool get_literals(model_ref& mdl, expr_ref_vector& lits);
123         void collect_atoms(expr_ref_vector const& fmls);
124         void order_avars(app_ref_vector& avars);
125 
126         void add_dcert(model_ref& mdl, expr_ref_vector& lits);
127         void add_arith_dcert(model& mdl, expr_ref_vector& lits);
128         void add_arith_dcert(model& mdl, expr_ref_vector& lits, app* a, app* b);
129         app_ref_vector get_arith_vars(expr_ref_vector const& lits);
130         vector<::mbp::def> arith_project(model_ref& mdl, app_ref_vector& avars, expr_ref_vector& lits);
131         void project_euf(model_ref& mdl, expr_ref_vector& lits);
132         void split_arith(expr_ref_vector const& lits,
133                          expr_ref_vector& alits,
134                          expr_ref_vector& uflits);
135     public:
136         uflia_mbi(solver* s, solver* emptySolver);
~uflia_mbi()137         ~uflia_mbi() override {}
138         mbi_result operator()(expr_ref_vector& lits, model_ref& mdl) override;
139         void project(model_ref& mdl, expr_ref_vector& lits);
140         void block(expr_ref_vector const& lits) override;
141     };
142 
143     /**
144      * use cases for interpolation.
145      */
146     class interpolator {
147         ast_manager&         m;
148     public:
interpolator(ast_manager & m)149         interpolator(ast_manager& m):m(m) {}
150         lbool pingpong(mbi_plugin& a, mbi_plugin& b, expr_ref& itp);
151         lbool pogo(mbi_plugin& a, mbi_plugin& b, expr_ref& itp);
152         lbool pogo(solver_factory& sf, expr* a, expr* b, expr_ref& itp);
153     };
154 
155 };
156