1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3
4 Module Name:
5
6 diff_neq_tactic.cpp
7
8 Abstract:
9
10 Solver for integer problems that contains literals of the form
11 k <= x
12 x <= k
13 x - y != k
14 And all variables are bounded.
15
16 Author:
17
18 Leonardo de Moura (leonardo) 2012-02-07.
19
20 Revision History:
21
22 --*/
23 #include "tactic/tactical.h"
24 #include "ast/arith_decl_plugin.h"
25 #include "ast/ast_smt2_pp.h"
26 #include "model/model.h"
27
28 class diff_neq_tactic : public tactic {
29 struct imp {
30 ast_manager & m;
31 arith_util u;
32 typedef unsigned var;
33
34 expr_ref_vector m_var2expr;
35 obj_map<expr, var> m_expr2var;
36
37 svector<int> m_lower;
38 svector<int> m_upper;
39 struct diseq {
40 var m_y;
41 int m_k;
diseqdiff_neq_tactic::imp::diseq42 diseq(var y, int k):m_y(y), m_k(k) {}
43 };
44 typedef svector<diseq> diseqs;
45 vector<diseqs> m_var_diseqs;
46 typedef svector<int> decision_stack;
47 decision_stack m_stack;
48
49 bool m_produce_models;
50 rational m_max_k;
51 rational m_max_neg_k;
52
53 unsigned m_num_conflicts;
54
impdiff_neq_tactic::imp55 imp(ast_manager & _m, params_ref const & p):
56 m(_m),
57 u(m),
58 m_var2expr(m) {
59 updt_params(p);
60 }
61
updt_paramsdiff_neq_tactic::imp62 void updt_params(params_ref const & p) {
63 m_max_k = rational(p.get_uint("diff_neq_max_k", 1024));
64 m_max_neg_k = -m_max_k;
65 if (m_max_k >= rational(INT_MAX/2))
66 m_max_k = rational(INT_MAX/2);
67 }
68
throw_not_supporteddiff_neq_tactic::imp69 void throw_not_supported() {
70 throw tactic_exception("goal is not diff neq");
71 }
72
num_varsdiff_neq_tactic::imp73 unsigned num_vars() const {
74 return m_upper.size();
75 }
76
mk_vardiff_neq_tactic::imp77 var mk_var(expr * t) {
78 SASSERT(is_uninterp_const(t));
79 var x;
80 if (m_expr2var.find(t, x))
81 return x;
82 x = m_upper.size();
83 m_expr2var.insert(t, x);
84 m_var2expr.push_back(t);
85 m_lower.push_back(INT_MIN); // unknown
86 m_upper.push_back(INT_MAX); // unknown
87 m_var_diseqs.push_back(diseqs());
88 return x;
89 }
90
process_lediff_neq_tactic::imp91 void process_le(expr * lhs, expr * rhs) {
92 if (!u.is_int(lhs))
93 throw_not_supported();
94 rational k;
95 if (is_uninterp_const(lhs) && u.is_numeral(rhs, k) && m_max_neg_k <= k && k <= m_max_k) {
96 var x = mk_var(lhs);
97 int _k = static_cast<int>(k.get_int64());
98 m_upper[x] = std::min(m_upper[x], _k);
99
100 }
101 else if (is_uninterp_const(rhs) && u.is_numeral(lhs, k) && m_max_neg_k <= k && k <= m_max_k) {
102 var x = mk_var(rhs);
103 int _k = static_cast<int>(k.get_int64());
104 m_lower[x] = std::max(m_lower[x], _k);
105 }
106 else {
107 throw_not_supported();
108 }
109 }
110
111 // process t1 - t2 != k
process_neq_corediff_neq_tactic::imp112 void process_neq_core(expr * t1, expr * t2, int k) {
113 var x1 = mk_var(t1);
114 var x2 = mk_var(t2);
115 if (x1 == x2)
116 throw_not_supported(); // must simplify first
117 if (x1 < x2) {
118 std::swap(x1, x2);
119 k = -k;
120 }
121 m_var_diseqs[x1].push_back(diseq(x2, k));
122 }
123
process_neqdiff_neq_tactic::imp124 void process_neq(expr * lhs, expr * rhs) {
125 if (!u.is_int(lhs))
126 throw_not_supported();
127 if (is_uninterp_const(lhs) && is_uninterp_const(rhs)) {
128 process_neq_core(lhs, rhs, 0);
129 return;
130 }
131 if (u.is_numeral(lhs))
132 std::swap(lhs, rhs);
133 rational k;
134 if (!u.is_numeral(rhs, k))
135 throw_not_supported();
136 if (!(m_max_neg_k <= k && k <= m_max_k))
137 throw_not_supported();
138 int _k = static_cast<int>(k.get_int64());
139 expr * t1, * t2, * mt1, * mt2;
140 if (u.is_add(lhs, t1, t2)) {
141 if (is_uninterp_const(t1) && u.is_times_minus_one(t2, mt2) && is_uninterp_const(mt2))
142 process_neq_core(t1, mt2, _k);
143 else if (is_uninterp_const(t2) && u.is_times_minus_one(t1, mt1) && is_uninterp_const(mt1))
144 process_neq_core(t2, mt1, _k);
145 else
146 throw_not_supported();
147 }
148 else {
149 throw_not_supported();
150 }
151 }
152
153 // throws exception if contains unbounded variable
check_unboundeddiff_neq_tactic::imp154 void check_unbounded() {
155 unsigned num = num_vars();
156 for (var x = 0; x < num; x++) {
157 if (m_lower[x] == INT_MIN || m_upper[x] == INT_MAX)
158 throw_not_supported();
159 // possible extension: support bound normalization here
160 if (m_lower[x] != 0)
161 throw_not_supported(); // use bound normalizer
162 }
163 }
164
compilediff_neq_tactic::imp165 void compile(goal const & g) {
166 expr * lhs;
167 expr * rhs;
168 unsigned sz = g.size();
169 for (unsigned i = 0; i < sz; i++) {
170 expr * f = g.form(i);
171 TRACE("diff_neq_tactic", tout << "processing: " << mk_ismt2_pp(f, m) << "\n";);
172 if (u.is_le(f, lhs, rhs))
173 process_le(lhs, rhs);
174 else if (u.is_ge(f, lhs, rhs))
175 process_le(rhs, lhs);
176 else if (m.is_not(f, f) && m.is_eq(f, lhs, rhs))
177 process_neq(lhs, rhs);
178 else
179 throw_not_supported();
180 }
181 check_unbounded();
182 }
183
displaydiff_neq_tactic::imp184 void display(std::ostream & out) {
185 unsigned num = num_vars();
186 for (var x = 0; x < num; x++) {
187 out << m_lower[x] << " <= " << mk_ismt2_pp(m_var2expr.get(x), m) << " <= " << m_upper[x] << "\n";
188 }
189 for (var x = 0; x < num; x++) {
190 diseqs::iterator it = m_var_diseqs[x].begin();
191 diseqs::iterator end = m_var_diseqs[x].end();
192 for (; it != end; ++it) {
193 out << mk_ismt2_pp(m_var2expr.get(x), m) << " != " << mk_ismt2_pp(m_var2expr.get(it->m_y), m) << " + " << it->m_k << "\n";
194 }
195 }
196 }
197
display_modeldiff_neq_tactic::imp198 void display_model(std::ostream & out) {
199 unsigned num = m_stack.size();
200 for (var x = 0; x < num; x++) {
201 out << mk_ismt2_pp(m_var2expr.get(x), m) << " := " << m_stack[x] << "\n";
202 }
203 }
204
205 bool_vector m_forbidden;
206
207 // make sure m_forbidden.size() > max upper bound
init_forbiddendiff_neq_tactic::imp208 void init_forbidden() {
209 int max = 0;
210 unsigned num = num_vars();
211 for (var x = 0; x < num; x++) {
212 if (m_upper[x] > max)
213 max = m_upper[x];
214 }
215 m_forbidden.reset();
216 m_forbidden.resize(max+1, false);
217 }
218
219 // Return a value v s.t. v >= starting_at and v <= m_upper[x] and all diseqs in m_var_diseqs[x] are satisfied.
220 // Return -1 if such value does not exist.
choose_valuediff_neq_tactic::imp221 int choose_value(var x, int starting_at) {
222 int max = starting_at-1;
223 int v = starting_at;
224 int upper = m_upper[x];
225 if (starting_at > upper)
226 return -1;
227 diseqs const & ds = m_var_diseqs[x];
228 diseqs::const_iterator it = ds.begin();
229 diseqs::const_iterator end = ds.end();
230 for (; it != end; ++it) {
231 int bad_v = m_stack[it->m_y] + it->m_k;
232 if (bad_v < v)
233 continue;
234 if (bad_v > upper)
235 continue;
236 if (bad_v == v) {
237 while (true) {
238 v++;
239 if (v > upper)
240 return -1;
241 if (!m_forbidden[v])
242 break;
243 m_forbidden[v] = false;
244 }
245 continue;
246 }
247 SASSERT(bad_v > v && bad_v <= upper);
248 m_forbidden[bad_v] = true;
249 if (bad_v > max)
250 max = bad_v;
251 }
252 // reset forbidden
253 for (int i = starting_at + 1; i <= max; i++)
254 m_forbidden[i] = false;
255 DEBUG_CODE({
256 for (unsigned i = 0; i < m_forbidden.size(); i++) {
257 SASSERT(!m_forbidden[i]);
258 }
259 });
260 return v;
261 }
262
extend_modeldiff_neq_tactic::imp263 bool extend_model(var x) {
264 int v = choose_value(x, 0);
265 if (v == -1)
266 return false;
267 m_stack.push_back(v);
268 return true;
269 }
270
resolve_conflictdiff_neq_tactic::imp271 bool resolve_conflict() {
272 m_num_conflicts++;
273 while (!m_stack.empty()) {
274 int v = m_stack.back();
275 m_stack.pop_back();
276 var x = m_stack.size();
277 v = choose_value(x, v+1);
278 if (v != -1) {
279 m_stack.push_back(v);
280 return true;
281 }
282 }
283 return false;
284 }
285
searchdiff_neq_tactic::imp286 bool search() {
287 m_num_conflicts = 0;
288 init_forbidden();
289 unsigned nvars = num_vars();
290 while (m_stack.size() < nvars) {
291 if (!m.inc())
292 throw tactic_exception(m.limit().get_cancel_msg());
293 TRACE("diff_neq_tactic", display_model(tout););
294 var x = m_stack.size();
295 if (extend_model(x))
296 continue;
297 if (!resolve_conflict())
298 return false;
299 }
300 TRACE("diff_neq_tactic", display_model(tout););
301 return true;
302 }
303
mk_modeldiff_neq_tactic::imp304 model * mk_model() {
305 model * md = alloc(model, m);
306 unsigned num = num_vars();
307 SASSERT(m_stack.size() == num);
308 for (var x = 0; x < num; x++) {
309 func_decl * d = to_app(m_var2expr.get(x))->get_decl();
310 md->register_decl(d, u.mk_numeral(rational(m_stack[x]), true));
311 }
312 return md;
313 }
314
operator ()diff_neq_tactic::imp315 void operator()(goal_ref const & g,
316 goal_ref_buffer & result) {
317 m_produce_models = g->models_enabled();
318 result.reset();
319 tactic_report report("diff-neq", *g);
320 fail_if_proof_generation("diff-neq", g);
321 fail_if_unsat_core_generation("diff-neq", g);
322 if (g->inconsistent()) {
323 result.push_back(g.get());
324 return;
325 }
326 compile(*g);
327 TRACE("diff_neq_tactic", g->display(tout); display(tout););
328 bool r = search();
329 report_tactic_progress(":conflicts", m_num_conflicts);
330 if (r) {
331 if (m_produce_models) {
332 g->add(model2model_converter(mk_model()));
333 }
334 g->reset();
335 }
336 else {
337 g->assert_expr(m.mk_false());
338 }
339 g->inc_depth();
340 result.push_back(g.get());
341 }
342 };
343
344 imp * m_imp;
345 params_ref m_params;
346 public:
diff_neq_tactic(ast_manager & m,params_ref const & p)347 diff_neq_tactic(ast_manager & m, params_ref const & p):
348 m_params(p) {
349 m_imp = alloc(imp, m, p);
350 }
351
translate(ast_manager & m)352 tactic * translate(ast_manager & m) override {
353 return alloc(diff_neq_tactic, m, m_params);
354 }
355
~diff_neq_tactic()356 ~diff_neq_tactic() override {
357 dealloc(m_imp);
358 }
359
updt_params(params_ref const & p)360 void updt_params(params_ref const & p) override {
361 m_params = p;
362 m_imp->updt_params(p);
363 }
364
collect_param_descrs(param_descrs & r)365 void collect_param_descrs(param_descrs & r) override {
366 r.insert("diff_neq_max_k", CPK_UINT, "(default: 1024) maximum variable upper bound for diff neq solver.");
367 }
368
collect_statistics(statistics & st) const369 void collect_statistics(statistics & st) const override {
370 st.update("conflicts", m_imp->m_num_conflicts);
371 }
372
reset_statistics()373 void reset_statistics() override {
374 m_imp->m_num_conflicts = 0;
375 }
376
377 /**
378 \brief Fix a DL variable in s to 0.
379 If s is not really in the difference logic fragment, then this is a NOOP.
380 */
operator ()(goal_ref const & in,goal_ref_buffer & result)381 void operator()(goal_ref const & in,
382 goal_ref_buffer & result) override {
383 (*m_imp)(in, result);
384 }
385
cleanup()386 void cleanup() override {
387 imp * d = alloc(imp, m_imp->m, m_params);
388 d->m_num_conflicts = m_imp->m_num_conflicts;
389 std::swap(d, m_imp);
390 dealloc(d);
391 }
392
393 };
394
mk_diff_neq_tactic(ast_manager & m,params_ref const & p)395 tactic * mk_diff_neq_tactic(ast_manager & m, params_ref const & p) {
396 return clean(alloc(diff_neq_tactic, m, p));
397 }
398
399
400
401