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