1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3
4 Module Name:
5
6 nlsat_explain.cpp
7
8 Abstract:
9
10 Functor that implements the "explain" procedure defined in Dejan and Leo's paper.
11
12 Author:
13
14 Leonardo de Moura (leonardo) 2012-01-13.
15
16 Revision History:
17
18 --*/
19 #include "nlsat/nlsat_explain.h"
20 #include "nlsat/nlsat_assignment.h"
21 #include "nlsat/nlsat_evaluator.h"
22 #include "math/polynomial/algebraic_numbers.h"
23 #include "util/ref_buffer.h"
24
25 namespace nlsat {
26
27 typedef polynomial::polynomial_ref_vector polynomial_ref_vector;
28 typedef ref_buffer<poly, pmanager> polynomial_ref_buffer;
29
30 struct explain::imp {
31 solver & m_solver;
32 assignment const & m_assignment;
33 atom_vector const & m_atoms;
34 atom_vector const & m_x2eq;
35 anum_manager & m_am;
36 polynomial::cache & m_cache;
37 pmanager & m_pm;
38 polynomial_ref_vector m_ps;
39 polynomial_ref_vector m_ps2;
40 polynomial_ref_vector m_psc_tmp;
41 polynomial_ref_vector m_factors;
42 scoped_anum_vector m_roots_tmp;
43 bool m_simplify_cores;
44 bool m_full_dimensional;
45 bool m_minimize_cores;
46 bool m_factor;
47 bool m_signed_project;
48
49 struct todo_set {
50 polynomial::cache & m_cache;
51 polynomial_ref_vector m_set;
52 svector<char> m_in_set;
53
todo_setnlsat::explain::imp::todo_set54 todo_set(polynomial::cache & u):m_cache(u), m_set(u.pm()) {}
55
resetnlsat::explain::imp::todo_set56 void reset() {
57 pmanager & pm = m_set.m();
58 unsigned sz = m_set.size();
59 for (unsigned i = 0; i < sz; i++) {
60 m_in_set[pm.id(m_set.get(i))] = false;
61 }
62 m_set.reset();
63 }
64
insertnlsat::explain::imp::todo_set65 void insert(poly * p) {
66 pmanager & pm = m_set.m();
67 p = m_cache.mk_unique(p);
68 unsigned pid = pm.id(p);
69 if (m_in_set.get(pid, false))
70 return;
71 m_in_set.setx(pid, true, false);
72 m_set.push_back(p);
73 }
74
emptynlsat::explain::imp::todo_set75 bool empty() const { return m_set.empty(); }
76
77 // Return max variable in todo_set
max_varnlsat::explain::imp::todo_set78 var max_var() const {
79 pmanager & pm = m_set.m();
80 var max = null_var;
81 unsigned sz = m_set.size();
82 for (unsigned i = 0; i < sz; i++) {
83 var x = pm.max_var(m_set.get(i));
84 SASSERT(x != null_var);
85 if (max == null_var || x > max)
86 max = x;
87 }
88 return max;
89 }
90
91 /**
92 \brief Remove the maximal polynomials from the set and store
93 them in max_polys. Return the maximal variable
94 */
remove_max_polysnlsat::explain::imp::todo_set95 var remove_max_polys(polynomial_ref_vector & max_polys) {
96 max_polys.reset();
97 var x = max_var();
98 pmanager & pm = m_set.m();
99 unsigned sz = m_set.size();
100 unsigned j = 0;
101 for (unsigned i = 0; i < sz; i++) {
102 poly * p = m_set.get(i);
103 var y = pm.max_var(p);
104 SASSERT(y <= x);
105 if (y == x) {
106 max_polys.push_back(p);
107 m_in_set[pm.id(p)] = false;
108 }
109 else {
110 m_set.set(j, p);
111 j++;
112 }
113 }
114 m_set.shrink(j);
115 return x;
116 }
117 };
118
119 // temporary field for store todo set of polynomials
120 todo_set m_todo;
121
122 // temporary fields for preprocessing core
123 scoped_literal_vector m_core1;
124 scoped_literal_vector m_core2;
125
126 // temporary fields for storing the result
127 scoped_literal_vector * m_result;
128 svector<char> m_already_added_literal;
129
130 evaluator & m_evaluator;
131
impnlsat::explain::imp132 imp(solver & s, assignment const & x2v, polynomial::cache & u, atom_vector const & atoms, atom_vector const & x2eq,
133 evaluator & ev):
134 m_solver(s),
135 m_assignment(x2v),
136 m_atoms(atoms),
137 m_x2eq(x2eq),
138 m_am(x2v.am()),
139 m_cache(u),
140 m_pm(u.pm()),
141 m_ps(m_pm),
142 m_ps2(m_pm),
143 m_psc_tmp(m_pm),
144 m_factors(m_pm),
145 m_roots_tmp(m_am),
146 m_todo(u),
147 m_core1(s),
148 m_core2(s),
149 m_result(nullptr),
150 m_evaluator(ev) {
151 m_simplify_cores = false;
152 m_full_dimensional = false;
153 m_minimize_cores = false;
154 m_signed_project = false;
155 }
156
~impnlsat::explain::imp157 ~imp() {
158 }
159
displaynlsat::explain::imp160 std::ostream& display(std::ostream & out, polynomial_ref const & p) const {
161 m_pm.display(out, p, m_solver.display_proc());
162 return out;
163 }
164
displaynlsat::explain::imp165 std::ostream& display(std::ostream & out, polynomial_ref_vector const & ps, char const * delim = "\n") const {
166 for (unsigned i = 0; i < ps.size(); i++) {
167 if (i > 0)
168 out << delim;
169 m_pm.display(out, ps.get(i), m_solver.display_proc());
170 }
171 return out;
172 }
173
displaynlsat::explain::imp174 std::ostream& display(std::ostream & out, literal l) const { return m_solver.display(out, l); }
display_varnlsat::explain::imp175 std::ostream& display_var(std::ostream & out, var x) const { return m_solver.display(out, x); }
displaynlsat::explain::imp176 std::ostream& display(std::ostream & out, unsigned sz, literal const * ls) const { return m_solver.display(out, sz, ls); }
displaynlsat::explain::imp177 std::ostream& display(std::ostream & out, literal_vector const & ls) const { return display(out, ls.size(), ls.data()); }
displaynlsat::explain::imp178 std::ostream& display(std::ostream & out, scoped_literal_vector const & ls) const { return display(out, ls.size(), ls.data()); }
179
180 /**
181 \brief Add literal to the result vector.
182 */
add_literalnlsat::explain::imp183 void add_literal(literal l) {
184 SASSERT(m_result != 0);
185 SASSERT(l != true_literal);
186 if (l == false_literal)
187 return;
188 unsigned lidx = l.index();
189 if (m_already_added_literal.get(lidx, false))
190 return;
191 TRACE("nlsat_explain", tout << "adding literal: " << lidx << "\n"; m_solver.display(tout, l) << "\n";);
192 m_already_added_literal.setx(lidx, true, false);
193 m_result->push_back(l);
194 }
195
196 /**
197 \brief Reset m_already_added vector using m_result
198 */
reset_already_addednlsat::explain::imp199 void reset_already_added() {
200 SASSERT(m_result != nullptr);
201 for (literal lit : *m_result)
202 m_already_added_literal[lit.index()] = false;
203 SASSERT(check_already_added());
204 }
205
206
207 /**
208 \brief evaluate the given polynomial in the current interpretation.
209 max_var(p) must be assigned in the current interpretation.
210 */
signnlsat::explain::imp211 ::sign sign(polynomial_ref const & p) {
212 SASSERT(max_var(p) == null_var || m_assignment.is_assigned(max_var(p)));
213 auto s = m_am.eval_sign_at(p, m_assignment);
214 TRACE("nlsat_explain", tout << "p: " << p << " var: " << max_var(p) << " sign: " << s << "\n";);
215 return s;
216 }
217
218 /**
219 \brief Wrapper for factorization
220 */
factornlsat::explain::imp221 void factor(polynomial_ref & p, polynomial_ref_vector & fs) {
222 // TODO: add params, caching
223 TRACE("nlsat_factor", tout << "factor\n" << p << "\n";);
224 fs.reset();
225 m_cache.factor(p.get(), fs);
226 }
227
228 /**
229 \brief Wrapper for psc chain computation
230 */
psc_chainnlsat::explain::imp231 void psc_chain(polynomial_ref & p, polynomial_ref & q, unsigned x, polynomial_ref_vector & result) {
232 // TODO caching
233 SASSERT(max_var(p) == max_var(q));
234 SASSERT(max_var(p) == x);
235 m_cache.psc_chain(p, q, x, result);
236 }
237
238 /**
239 \brief Store in ps the polynomials occurring in the given literals.
240 */
collect_polysnlsat::explain::imp241 void collect_polys(unsigned num, literal const * ls, polynomial_ref_vector & ps) {
242 ps.reset();
243 for (unsigned i = 0; i < num; i++) {
244 atom * a = m_atoms[ls[i].var()];
245 SASSERT(a != 0);
246 if (a->is_ineq_atom()) {
247 unsigned sz = to_ineq_atom(a)->size();
248 for (unsigned j = 0; j < sz; j++)
249 ps.push_back(to_ineq_atom(a)->p(j));
250 }
251 else {
252 ps.push_back(to_root_atom(a)->p());
253 }
254 }
255 }
256
257 /**
258 \brief Add literal p != 0 into m_result.
259 */
260 ptr_vector<poly> m_zero_fs;
261 bool_vector m_is_even;
add_zero_assumptionnlsat::explain::imp262 void add_zero_assumption(polynomial_ref & p) {
263 // If p is of the form p1^n1 * ... * pk^nk,
264 // then only the factors that are zero in the current interpretation needed to be considered.
265 // I don't want to create a nested conjunction in the clause.
266 // Then, I assert p_i1 * ... * p_im != 0
267 factor(p, m_factors);
268 unsigned num_factors = m_factors.size();
269 m_zero_fs.reset();
270 m_is_even.reset();
271 polynomial_ref f(m_pm);
272 for (unsigned i = 0; i < num_factors; i++) {
273 f = m_factors.get(i);
274 if (is_zero(sign(f))) {
275 m_zero_fs.push_back(m_factors.get(i));
276 m_is_even.push_back(false);
277 }
278 }
279 SASSERT(!m_zero_fs.empty()); // one of the factors must be zero in the current interpretation, since p is zero in it.
280 literal l = m_solver.mk_ineq_literal(atom::EQ, m_zero_fs.size(), m_zero_fs.data(), m_is_even.data());
281 l.neg();
282 TRACE("nlsat_explain", tout << "adding (zero assumption) literal:\n"; display(tout, l); tout << "\n";);
283 add_literal(l);
284 }
285
add_simple_assumptionnlsat::explain::imp286 void add_simple_assumption(atom::kind k, poly * p, bool sign = false) {
287 SASSERT(k == atom::EQ || k == atom::LT || k == atom::GT);
288 bool is_even = false;
289 bool_var b = m_solver.mk_ineq_atom(k, 1, &p, &is_even);
290 literal l(b, !sign);
291 add_literal(l);
292 }
293
add_assumptionnlsat::explain::imp294 void add_assumption(atom::kind k, poly * p, bool sign = false) {
295 // TODO: factor
296 add_simple_assumption(k, p, sign);
297 }
298
299 /**
300 \brief Eliminate "vanishing leading coefficients" of p.
301 That is, coefficients that vanish in the current
302 interpretation. The resultant p is a reduct of p s.t. its
303 leading coefficient does not vanish in the current
304 interpretation. If all coefficients of p vanish, then
305 the resultant p is the zero polynomial.
306 */
elim_vanishingnlsat::explain::imp307 void elim_vanishing(polynomial_ref & p) {
308 SASSERT(!is_const(p));
309 var x = max_var(p);
310 unsigned k = degree(p, x);
311 SASSERT(k > 0);
312 polynomial_ref lc(m_pm);
313 polynomial_ref reduct(m_pm);
314 while (true) {
315 TRACE("nlsat_explain", tout << "elim vanishing x" << x << " k:" << k << " " << p << "\n";);
316 if (is_const(p))
317 return;
318 if (k == 0) {
319 // x vanished from p, peek next maximal variable
320 x = max_var(p);
321 SASSERT(x != null_var);
322 k = degree(p, x);
323 }
324 #if 0
325 anum const & x_val = m_assignment.value(x);
326 if (m_am.is_zero(x_val)) {
327 // add_zero_assumption(lc);
328 lc = m_pm.coeff(p, x, k, reduct);
329 k--;
330 p = reduct;
331 continue;
332 }
333 #endif
334 if (m_pm.nonzero_const_coeff(p, x, k)) {
335 TRACE("nlsat_explain", tout << "nonzero const x" << x << "\n";);
336 return; // lc is a nonzero constant
337 }
338 lc = m_pm.coeff(p, x, k, reduct);
339 TRACE("nlsat_explain", tout << "lc: " << lc << " reduct: " << reduct << "\n";);
340 if (!is_zero(lc)) {
341 if (!::is_zero(sign(lc)))
342 return;
343 // lc is not the zero polynomial, but it vanished in the current interpretation.
344 // so we keep searching...
345 add_zero_assumption(lc);
346 }
347 if (k == 0) {
348 // all coefficients of p vanished in the current interpretation,
349 // and were added as assumptions.
350 p = m_pm.mk_zero();
351 return;
352 }
353 k--;
354 p = reduct;
355 }
356 }
357
358 /**
359 Eliminate vanishing coefficients of polynomials in ps.
360 The coefficients that are zero (i.e., vanished) are added
361 as assumptions into m_result.
362 */
elim_vanishingnlsat::explain::imp363 void elim_vanishing(polynomial_ref_vector & ps) {
364 unsigned j = 0;
365 unsigned sz = ps.size();
366 polynomial_ref p(m_pm);
367 for (unsigned i = 0; i < sz; i++) {
368 p = ps.get(i);
369 elim_vanishing(p);
370 if (!is_const(p)) {
371 ps.set(j, p);
372 j++;
373 }
374 }
375 ps.shrink(j);
376 }
377
378 /**
379 Normalize literal with respect to given maximal variable.
380 The basic idea is to eliminate vanishing (leading) coefficients from a (arithmetic) literal,
381 and factors from lower stages.
382
383 The vanishing coefficients and factors from lower stages are added as assumptions to the lemma
384 being generated.
385
386 Example 1)
387 Assume
388 - l is of the form (y^2 - 2)*x^3 + y*x + 1 > 0
389 - x is the maximal variable
390 - y is assigned to sqrt(2)
391 Thus, (y^2 - 2) the coefficient of x^3 vanished. This method returns
392 y*x + 1 > 0 and adds the assumption (y^2 - 2) = 0 to the lemma
393
394 Example 2)
395 Assume
396 - l is of the form (x + 2)*(y - 1) > 0
397 - x is the maximal variable
398 - y is assigned to 0
399 (x + 2) < 0 is returned and assumption (y - 1) < 0 is added as an assumption.
400
401 Remark: root atoms are not normalized
402 */
normalizenlsat::explain::imp403 literal normalize(literal l, var max) {
404 bool_var b = l.var();
405 if (b == true_bool_var)
406 return l;
407 SASSERT(m_atoms[b] != 0);
408 if (m_atoms[b]->is_ineq_atom()) {
409 polynomial_ref_buffer ps(m_pm);
410 sbuffer<bool> is_even;
411 polynomial_ref p(m_pm);
412 ineq_atom * a = to_ineq_atom(m_atoms[b]);
413 int atom_sign = 1;
414 unsigned sz = a->size();
415 bool normalized = false; // true if the literal needs to be normalized
416 for (unsigned i = 0; i < sz; i++) {
417 p = a->p(i);
418 if (max_var(p) == max)
419 elim_vanishing(p); // eliminate vanishing coefficients of max
420 if (is_const(p) || max_var(p) < max) {
421 int s = sign(p);
422 if (!is_const(p)) {
423 SASSERT(max_var(p) != null_var);
424 SASSERT(max_var(p) < max);
425 // factor p is a lower stage polynomial, so we should add assumption to justify p being eliminated
426 if (s == 0)
427 add_simple_assumption(atom::EQ, p); // add assumption p = 0
428 else if (a->is_even(i))
429 add_simple_assumption(atom::EQ, p, true); // add assumption p != 0
430 else if (s < 0)
431 add_simple_assumption(atom::LT, p); // add assumption p < 0
432 else
433 add_simple_assumption(atom::GT, p); // add assumption p > 0
434 }
435 if (s == 0) {
436 bool atom_val = a->get_kind() == atom::EQ;
437 bool lit_val = l.sign() ? !atom_val : atom_val;
438 return lit_val ? true_literal : false_literal;
439 }
440 else if (s < 0 && a->is_odd(i)) {
441 atom_sign = -atom_sign;
442 }
443 normalized = true;
444 }
445 else {
446 if (p != a->p(i)) {
447 SASSERT(!m_pm.eq(p, a->p(i)));
448 normalized = true;
449 }
450 is_even.push_back(a->is_even(i));
451 ps.push_back(p);
452 }
453 }
454 if (ps.empty()) {
455 SASSERT(atom_sign != 0);
456 // LHS is positive or negative. It is positive if atom_sign > 0 and negative if atom_sign < 0
457 bool atom_val;
458 if (a->get_kind() == atom::EQ)
459 atom_val = false;
460 else if (a->get_kind() == atom::LT)
461 atom_val = atom_sign < 0;
462 else
463 atom_val = atom_sign > 0;
464 bool lit_val = l.sign() ? !atom_val : atom_val;
465 return lit_val ? true_literal : false_literal;
466 }
467 else if (normalized) {
468 atom::kind new_k = a->get_kind();
469 if (atom_sign < 0)
470 new_k = atom::flip(new_k);
471 literal new_l = m_solver.mk_ineq_literal(new_k, ps.size(), ps.data(), is_even.data());
472 if (l.sign())
473 new_l.neg();
474 return new_l;
475 }
476 else {
477 SASSERT(atom_sign > 0);
478 return l;
479 }
480 }
481 else {
482 return l;
483 }
484 }
485
486 /**
487 Normalize literals (in the conflicting core) with respect
488 to given maximal variable. The basic idea is to eliminate
489 vanishing (leading) coefficients (and factors from lower
490 stages) from (arithmetic) literals,
491 */
normalizenlsat::explain::imp492 void normalize(scoped_literal_vector & C, var max) {
493 unsigned sz = C.size();
494 unsigned j = 0;
495 for (unsigned i = 0; i < sz; i++) {
496 literal new_l = normalize(C[i], max);
497 if (new_l == true_literal)
498 continue;
499 if (new_l == false_literal) {
500 // false literal was created. The assumptions added are sufficient for implying the conflict.
501 C.reset();
502 return;
503 }
504 C.set(j, new_l);
505 j++;
506 }
507 C.shrink(j);
508 }
509
max_varnlsat::explain::imp510 var max_var(poly const * p) { return m_pm.max_var(p); }
511
512 /**
513 \brief Return the maximal variable in a set of nonconstant polynomials.
514 */
max_varnlsat::explain::imp515 var max_var(polynomial_ref_vector const & ps) {
516 if (ps.empty())
517 return null_var;
518 var max = max_var(ps.get(0));
519 SASSERT(max != null_var); // there are no constant polynomials in ps
520 unsigned sz = ps.size();
521 for (unsigned i = 1; i < sz; i++) {
522 var curr = m_pm.max_var(ps.get(i));
523 SASSERT(curr != null_var);
524 if (curr > max)
525 max = curr;
526 }
527 return max;
528 }
529
max_varnlsat::explain::imp530 polynomial::var max_var(literal l) {
531 atom * a = m_atoms[l.var()];
532 if (a != nullptr)
533 return a->max_var();
534 else
535 return null_var;
536 }
537
538 /**
539 \brief Return the maximal variable in the given set of literals
540 */
max_varnlsat::explain::imp541 var max_var(unsigned sz, literal const * ls) {
542 var max = null_var;
543 for (unsigned i = 0; i < sz; i++) {
544 literal l = ls[i];
545 atom * a = m_atoms[l.var()];
546 if (a != nullptr) {
547 var x = a->max_var();
548 SASSERT(x != null_var);
549 if (max == null_var || x > max)
550 max = x;
551 }
552 }
553 return max;
554 }
555
556 /**
557 \brief Move the polynomials in q in ps that do not contain x to qs.
558 */
keep_p_xnlsat::explain::imp559 void keep_p_x(polynomial_ref_vector & ps, var x, polynomial_ref_vector & qs) {
560 unsigned sz = ps.size();
561 unsigned j = 0;
562 for (unsigned i = 0; i < sz; i++) {
563 poly * q = ps.get(i);
564 if (max_var(q) != x) {
565 qs.push_back(q);
566 }
567 else {
568 ps.set(j, q);
569 j++;
570 }
571 }
572 ps.shrink(j);
573 }
574
575 /**
576 \brief Add factors of p to todo
577 */
add_factorsnlsat::explain::imp578 void add_factors(polynomial_ref & p) {
579 if (is_const(p))
580 return;
581 elim_vanishing(p);
582 if (is_const(p))
583 return;
584 if (m_factor) {
585 TRACE("nlsat_explain", display(tout << "adding factors of\n", p); tout << "\n";);
586 factor(p, m_factors);
587 polynomial_ref f(m_pm);
588 for (unsigned i = 0; i < m_factors.size(); i++) {
589 f = m_factors.get(i);
590 elim_vanishing(f);
591 if (!is_const(f)) {
592 TRACE("nlsat_explain", tout << "adding factor:\n"; display(tout, f); tout << "\n";);
593 m_todo.insert(f);
594 }
595 }
596 }
597 else {
598 m_todo.insert(p);
599 }
600 }
601
602 /**
603 \brief Add leading coefficients of the polynomials in ps.
604
605 \pre all polynomials in ps contain x
606
607 Remark: the leading coefficients do not vanish in the current model,
608 since all polynomials in ps were pre-processed using elim_vanishing.
609 */
add_lcnlsat::explain::imp610 void add_lc(polynomial_ref_vector & ps, var x) {
611 polynomial_ref p(m_pm);
612 polynomial_ref lc(m_pm);
613 unsigned sz = ps.size();
614 for (unsigned i = 0; i < sz; i++) {
615 p = ps.get(i);
616 unsigned k = degree(p, x);
617 SASSERT(k > 0);
618 TRACE("nlsat_explain", tout << "add_lc, x: "; display_var(tout, x); tout << "\nk: " << k << "\n"; display(tout, p); tout << "\n";);
619 if (m_pm.nonzero_const_coeff(p, x, k)) {
620 TRACE("nlsat_explain", tout << "constant coefficient, skipping...\n";);
621 continue;
622 }
623 lc = m_pm.coeff(p, x, k);
624 SASSERT(sign(lc) != 0);
625 SASSERT(!is_const(lc));
626 add_factors(lc);
627 }
628 }
629
630 /**
631 \brief Add v-psc(p, q, x) into m_todo
632 */
pscnlsat::explain::imp633 void psc(polynomial_ref & p, polynomial_ref & q, var x) {
634 polynomial_ref_vector & S = m_psc_tmp;
635 polynomial_ref s(m_pm);
636
637 psc_chain(p, q, x, S);
638 unsigned sz = S.size();
639 TRACE("nlsat_explain", tout << "computing psc of\n"; display(tout, p); tout << "\n"; display(tout, q); tout << "\n";
640 for (unsigned i = 0; i < sz; ++i) {
641 s = S.get(i);
642 tout << "psc: " << s << "\n";
643 });
644
645 for (unsigned i = 0; i < sz; i++) {
646 s = S.get(i);
647 TRACE("nlsat_explain", display(tout << "processing psc(" << i << ")\n", s) << "\n";);
648 if (is_zero(s)) {
649 TRACE("nlsat_explain", tout << "skipping psc is the zero polynomial\n";);
650 continue;
651 }
652 if (is_const(s)) {
653 TRACE("nlsat_explain", tout << "done, psc is a constant\n";);
654 return;
655 }
656 if (is_zero(sign(s))) {
657 TRACE("nlsat_explain", tout << "psc vanished, adding zero assumption\n";);
658 add_zero_assumption(s);
659 continue;
660 }
661 TRACE("nlsat_explain",
662 tout << "adding v-psc of\n";
663 display(tout, p);
664 tout << "\n";
665 display(tout, q);
666 tout << "\n---->\n";
667 display(tout, s);
668 tout << "\n";);
669 // s did not vanish completely, but its leading coefficient may have vanished
670 add_factors(s);
671 return;
672 }
673 }
674
675 /**
676 \brief For each p in ps, add v-psc(x, p, p') into m_todo
677
678 \pre all polynomials in ps contain x
679
680 Remark: the leading coefficients do not vanish in the current model,
681 since all polynomials in ps were pre-processed using elim_vanishing.
682 */
psc_discriminantnlsat::explain::imp683 void psc_discriminant(polynomial_ref_vector & ps, var x) {
684 polynomial_ref p(m_pm);
685 polynomial_ref p_prime(m_pm);
686 unsigned sz = ps.size();
687 for (unsigned i = 0; i < sz; i++) {
688 p = ps.get(i);
689 if (degree(p, x) < 2)
690 continue;
691 p_prime = derivative(p, x);
692 psc(p, p_prime, x);
693 }
694 }
695
696 /**
697 \brief For each p and q in ps, p != q, add v-psc(x, p, q) into m_todo
698
699 \pre all polynomials in ps contain x
700
701 Remark: the leading coefficients do not vanish in the current model,
702 since all polynomials in ps were pre-processed using elim_vanishing.
703 */
psc_resultantnlsat::explain::imp704 void psc_resultant(polynomial_ref_vector & ps, var x) {
705 polynomial_ref p(m_pm);
706 polynomial_ref q(m_pm);
707 unsigned sz = ps.size();
708 for (unsigned i = 0; i < sz - 1; i++) {
709 p = ps.get(i);
710 for (unsigned j = i + 1; j < sz; j++) {
711 q = ps.get(j);
712 psc(p, q, x);
713 }
714 }
715 }
716
test_root_literalnlsat::explain::imp717 void test_root_literal(atom::kind k, var y, unsigned i, poly * p, scoped_literal_vector& result) {
718 m_result = &result;
719 add_root_literal(k, y, i, p);
720 reset_already_added();
721 m_result = nullptr;
722 }
723
724
add_root_literalnlsat::explain::imp725 void add_root_literal(atom::kind k, var y, unsigned i, poly * p) {
726 polynomial_ref pr(p, m_pm);
727 TRACE("nlsat_explain",
728 display(tout << "x" << y << " " << k << "[" << i << "](", pr); tout << ")\n";);
729
730 if (!mk_linear_root(k, y, i, p) &&
731 !mk_quadratic_root(k, y, i, p)) {
732 bool_var b = m_solver.mk_root_atom(k, y, i, p);
733 literal l(b, true);
734 TRACE("nlsat_explain", tout << "adding literal\n"; display(tout, l); tout << "\n";);
735 add_literal(l);
736 }
737 }
738
739 /**
740 * literal can be expressed using a linear ineq_atom
741 */
mk_linear_rootnlsat::explain::imp742 bool mk_linear_root(atom::kind k, var y, unsigned i, poly * p) {
743 scoped_mpz c(m_pm.m());
744 if (m_pm.degree(p, y) == 1 && m_pm.const_coeff(p, y, 1, c)) {
745 SASSERT(!m_pm.m().is_zero(c));
746 mk_linear_root(k, y, i, p, m_pm.m().is_neg(c));
747 return true;
748 }
749 return false;
750 }
751
752
753 /**
754 Create pseudo-linear root depending on the sign of the coefficient to y.
755 */
mk_plinear_rootnlsat::explain::imp756 bool mk_plinear_root(atom::kind k, var y, unsigned i, poly * p) {
757 if (m_pm.degree(p, y) != 1) {
758 return false;
759 }
760 polynomial_ref c(m_pm);
761 c = m_pm.coeff(p, y, 1);
762 int s = sign(c);
763 if (s == 0) {
764 return false;
765 }
766 ensure_sign(c);
767 mk_linear_root(k, y, i, p, s < 0);
768 return true;
769 }
770
771 /**
772 Encode root conditions for quadratic polynomials.
773
774 Basically implements Thom's theorem. The roots are characterized by the sign of polynomials and their derivatives.
775
776 b^2 - 4ac = 0:
777 - there is only one root, which is -b/2a.
778 - relation to root is a function of the sign of
779 - 2ax + b
780 b^2 - 4ac > 0:
781 - assert i == 1 or i == 2
782 - relation to root is a function of the signs of:
783 - 2ax + b
784 - ax^2 + bx + c
785 */
786
mk_quadratic_rootnlsat::explain::imp787 bool mk_quadratic_root(atom::kind k, var y, unsigned i, poly * p) {
788 if (m_pm.degree(p, y) != 2) {
789 return false;
790 }
791 if (i != 1 && i != 2) {
792 return false;
793 }
794
795 SASSERT(m_assignment.is_assigned(y));
796 polynomial_ref A(m_pm), B(m_pm), C(m_pm), q(m_pm), p_diff(m_pm), yy(m_pm);
797 A = m_pm.coeff(p, y, 2);
798 B = m_pm.coeff(p, y, 1);
799 C = m_pm.coeff(p, y, 0);
800 // TBD throttle based on degree of q?
801 q = (B*B) - (4*A*C);
802 yy = m_pm.mk_polynomial(y);
803 p_diff = 2*A*yy + B;
804 p_diff = m_pm.normalize(p_diff);
805 int sq = ensure_sign(q);
806 if (sq < 0) {
807 return false;
808 }
809 int sa = ensure_sign(A);
810 if (sa == 0) {
811 q = B*yy + C;
812 return mk_plinear_root(k, y, i, q);
813 }
814 ensure_sign(p_diff);
815 if (sq > 0) {
816 polynomial_ref pr(p, m_pm);
817 ensure_sign(pr);
818 }
819 return true;
820 }
821
ensure_signnlsat::explain::imp822 int ensure_sign(polynomial_ref & p) {
823 #if 0
824 polynomial_ref f(m_pm);
825 factor(p, m_factors);
826 m_is_even.reset();
827 unsigned num_factors = m_factors.size();
828 int s = 1;
829 for (unsigned i = 0; i < num_factors; i++) {
830 f = m_factors.get(i);
831 s *= sign(f);
832 m_is_even.push_back(false);
833 }
834 if (num_factors > 0) {
835 atom::kind k = atom::EQ;
836 if (s == 0) k = atom::EQ;
837 if (s < 0) k = atom::LT;
838 if (s > 0) k = atom::GT;
839 bool_var b = m_solver.mk_ineq_atom(k, num_factors, m_factors.c_ptr(), m_is_even.c_ptr());
840 add_literal(literal(b, true));
841 }
842 return s;
843 #else
844 int s = sign(p);
845 if (!is_const(p)) {
846 TRACE("nlsat_explain", tout << p << "\n";);
847 add_simple_assumption(s == 0 ? atom::EQ : (s < 0 ? atom::LT : atom::GT), p);
848 }
849 return s;
850 #endif
851 }
852
853 /**
854 Auxiliary function to linear roots.
855 y > root[1](-2*y - z)
856 y > -z/2
857 y + z/2 > 0
858 2y + z > 0
859
860 */
mk_linear_rootnlsat::explain::imp861 void mk_linear_root(atom::kind k, var y, unsigned i, poly * p, bool mk_neg) {
862 polynomial_ref p_prime(m_pm);
863 p_prime = p;
864 bool lsign = false;
865 if (mk_neg)
866 p_prime = neg(p_prime);
867 p = p_prime.get();
868 switch (k) {
869 case atom::ROOT_EQ: k = atom::EQ; lsign = false; break;
870 case atom::ROOT_LT: k = atom::LT; lsign = false; break;
871 case atom::ROOT_GT: k = atom::GT; lsign = false; break;
872 case atom::ROOT_LE: k = atom::GT; lsign = true; break;
873 case atom::ROOT_GE: k = atom::LT; lsign = true; break;
874 default:
875 UNREACHABLE();
876 break;
877 }
878 add_simple_assumption(k, p, lsign);
879 }
880
881 /**
882 Add one or two literals that specify in which cell of variable y the current interpretation is.
883 One literal is added for the cases:
884 - y in (-oo, min) where min is the minimal root of the polynomials p2 in ps
885 We add literal
886 ! (y < root_1(p2))
887 - y in (max, oo) where max is the maximal root of the polynomials p1 in ps
888 We add literal
889 ! (y > root_k(p1)) where k is the number of real roots of p
890 - y = r where r is the k-th root of a polynomial p in ps
891 We add literal
892 ! (y = root_k(p))
893 Two literals are added when
894 - y in (l, u) where (l, u) does not contain any root of polynomials p in ps, and
895 l is the i-th root of a polynomial p1 in ps, and u is the j-th root of a polynomial p2 in ps.
896 We add literals
897 ! (y > root_i(p1)) or !(y < root_j(p2))
898 */
add_cell_litsnlsat::explain::imp899 void add_cell_lits(polynomial_ref_vector & ps, var y) {
900 SASSERT(m_assignment.is_assigned(y));
901 bool lower_inf = true;
902 bool upper_inf = true;
903 scoped_anum_vector & roots = m_roots_tmp;
904 scoped_anum lower(m_am);
905 scoped_anum upper(m_am);
906 anum const & y_val = m_assignment.value(y);
907 TRACE("nlsat_explain", tout << "adding literals for "; display_var(tout, y); tout << " -> ";
908 m_am.display_decimal(tout, y_val); tout << "\n";);
909 polynomial_ref p_lower(m_pm);
910 unsigned i_lower = UINT_MAX;
911 polynomial_ref p_upper(m_pm);
912 unsigned i_upper = UINT_MAX;
913 polynomial_ref p(m_pm);
914 unsigned sz = ps.size();
915 for (unsigned k = 0; k < sz; k++) {
916 p = ps.get(k);
917 if (max_var(p) != y)
918 continue;
919 roots.reset();
920 // Variable y is assigned in m_assignment. We must temporarily unassign it.
921 // Otherwise, the isolate_roots procedure will assume p is a constant polynomial.
922 m_am.isolate_roots(p, undef_var_assignment(m_assignment, y), roots);
923 unsigned num_roots = roots.size();
924 for (unsigned i = 0; i < num_roots; i++) {
925 int s = m_am.compare(y_val, roots[i]);
926 TRACE("nlsat_explain",
927 m_am.display_decimal(tout << "comparing root: ", roots[i]); tout << "\n";
928 m_am.display_decimal(tout << "with y_val:", y_val);
929 tout << "\nsign " << s << "\n";
930 tout << "poly: " << p << "\n";
931 );
932 if (s == 0) {
933 // y_val == roots[i]
934 // add literal
935 // ! (y = root_i(p))
936 add_root_literal(atom::ROOT_EQ, y, i+1, p);
937 return;
938 }
939 else if (s < 0) {
940 // y_val < roots[i]
941
942 // check if roots[i] is a better upper bound
943 if (upper_inf || m_am.lt(roots[i], upper)) {
944 upper_inf = false;
945 m_am.set(upper, roots[i]);
946 p_upper = p;
947 i_upper = i+1;
948 }
949 }
950 else if (s > 0) {
951 // roots[i] < y_val
952
953 // check if roots[i] is a better lower bound
954 if (lower_inf || m_am.lt(lower, roots[i])) {
955 lower_inf = false;
956 m_am.set(lower, roots[i]);
957 p_lower = p;
958 i_lower = i+1;
959 }
960 }
961 }
962 }
963
964 if (!lower_inf) {
965 add_root_literal(m_full_dimensional ? atom::ROOT_GE : atom::ROOT_GT, y, i_lower, p_lower);
966 }
967 if (!upper_inf) {
968 add_root_literal(m_full_dimensional ? atom::ROOT_LE : atom::ROOT_LT, y, i_upper, p_upper);
969 }
970 }
971
972 /**
973 \brief Return true if all polynomials in ps are univariate in x.
974 */
all_univnlsat::explain::imp975 bool all_univ(polynomial_ref_vector const & ps, var x) {
976 unsigned sz = ps.size();
977 for (unsigned i = 0; i < sz; i++) {
978 poly * p = ps.get(i);
979 if (max_var(p) != x)
980 return false;
981 if (!m_pm.is_univariate(p))
982 return false;
983 }
984 return true;
985 }
986
987 /**
988 \brief Apply model-based projection operation defined in our paper.
989 */
projectnlsat::explain::imp990 void project(polynomial_ref_vector & ps, var max_x) {
991 if (ps.empty())
992 return;
993 m_todo.reset();
994 for (poly* p : ps) {
995 m_todo.insert(p);
996 }
997 var x = m_todo.remove_max_polys(ps);
998 // Remark: after vanishing coefficients are eliminated, ps may not contain max_x anymore
999 if (x < max_x)
1000 add_cell_lits(ps, x);
1001 while (true) {
1002 if (all_univ(ps, x) && m_todo.empty()) {
1003 m_todo.reset();
1004 break;
1005 }
1006 TRACE("nlsat_explain", tout << "project loop, processing var "; display_var(tout, x); tout << "\npolynomials\n";
1007 display(tout, ps); tout << "\n";);
1008 add_lc(ps, x);
1009 psc_discriminant(ps, x);
1010 psc_resultant(ps, x);
1011 if (m_todo.empty())
1012 break;
1013 x = m_todo.remove_max_polys(ps);
1014 add_cell_lits(ps, x);
1015 }
1016 }
1017
check_already_addednlsat::explain::imp1018 bool check_already_added() const {
1019 for (bool b : m_already_added_literal) {
1020 (void)b;
1021 SASSERT(!b);
1022 }
1023 return true;
1024 }
1025
1026 /*
1027 Conflicting core simplification using equations.
1028 The idea is to use equations to reduce the complexity of the
1029 conflicting core.
1030
1031 Basic idea:
1032 Let l be of the form
1033 h > 0
1034 and eq of the form
1035 p = 0
1036
1037 Using pseudo-division we have that:
1038 lc(p)^d h = q p + r
1039 where q and r are the pseudo-quotient and pseudo-remainder
1040 d is the integer returned by the pseudo-division algorithm.
1041 lc(p) is the leading coefficient of p
1042 If d is even or sign(lc(p)) > 0, we have that
1043 sign(h) = sign(r)
1044 Otherwise
1045 sign(h) = -sign(r) flipped the sign
1046
1047 We have the following rules
1048
1049 If
1050 (C and h > 0) implies false
1051 Then
1052 1. (C and p = 0 and lc(p) != 0 and r > 0) implies false if d is even
1053 2. (C and p = 0 and lc(p) > 0 and r > 0) implies false if lc(p) > 0 and d is odd
1054 3. (C and p = 0 and lc(p) < 0 and r < 0) implies false if lc(p) < 0 and d is odd
1055
1056 If
1057 (C and h = 0) implies false
1058 Then
1059 (C and p = 0 and lc(p) != 0 and r = 0) implies false
1060
1061 If
1062 (C and h < 0) implies false
1063 Then
1064 1. (C and p = 0 and lc(p) != 0 and r < 0) implies false if d is even
1065 2. (C and p = 0 and lc(p) > 0 and r < 0) implies false if lc(p) > 0 and d is odd
1066 3. (C and p = 0 and lc(p) < 0 and r > 0) implies false if lc(p) < 0 and d is odd
1067
1068 Good cases:
1069 - lc(p) is a constant
1070 - p = 0 is already in the conflicting core
1071 - p = 0 is linear
1072
1073 We only use equations from the conflicting core and lower stages.
1074 Equations from lower stages are automatically added to the lemma.
1075 */
1076 struct eq_info {
1077 poly const * m_eq;
1078 polynomial::var m_x;
1079 unsigned m_k;
1080 poly * m_lc;
1081 int m_lc_sign;
1082 bool m_lc_const;
1083 bool m_lc_add;
1084 bool m_lc_add_ineq;
add_lc_ineqnlsat::explain::imp::eq_info1085 void add_lc_ineq() {
1086 m_lc_add = true;
1087 m_lc_add_ineq = true;
1088 }
add_lc_diseqnlsat::explain::imp::eq_info1089 void add_lc_diseq() {
1090 if (!m_lc_add) {
1091 m_lc_add = true;
1092 m_lc_add_ineq = false;
1093 }
1094 }
1095 };
simplifynlsat::explain::imp1096 void simplify(literal l, eq_info & info, var max, scoped_literal & new_lit) {
1097 bool_var b = l.var();
1098 atom * a = m_atoms[b];
1099 SASSERT(a);
1100 if (a->is_root_atom()) {
1101 new_lit = l;
1102 return;
1103 }
1104 ineq_atom * _a = to_ineq_atom(a);
1105 unsigned num_factors = _a->size();
1106 if (num_factors == 1 && _a->p(0) == info.m_eq) {
1107 new_lit = l;
1108 return;
1109 }
1110 TRACE("nlsat_simplify_core", display(tout << "trying to simplify literal\n", l) << "\nusing equation\n";
1111 m_pm.display(tout, info.m_eq, m_solver.display_proc()); tout << "\n";);
1112 int atom_sign = 1;
1113 bool modified_lit = false;
1114 polynomial_ref_buffer new_factors(m_pm);
1115 sbuffer<bool> new_factors_even;
1116 polynomial_ref new_factor(m_pm);
1117 for (unsigned s = 0; s < num_factors; s++) {
1118 poly * f = _a->p(s);
1119 bool is_even = _a->is_even(s);
1120 if (m_pm.degree(f, info.m_x) < info.m_k) {
1121 new_factors.push_back(f);
1122 new_factors_even.push_back(is_even);
1123 continue;
1124 }
1125 modified_lit = true;
1126 unsigned d;
1127 m_pm.pseudo_remainder(f, info.m_eq, info.m_x, d, new_factor);
1128 polynomial_ref fact(f, m_pm), eq(const_cast<poly*>(info.m_eq), m_pm);
1129
1130 TRACE("nlsat_simplify_core", tout << "d: " << d << " factor " << fact << " eq " << eq << " new factor " << new_factor << "\n";);
1131 // adjust sign based on sign of lc of eq
1132 if (d % 2 == 1 && // d is odd
1133 !is_even && // degree of the factor is odd
1134 info.m_lc_sign < 0) { // lc of the eq is negative
1135 atom_sign = -atom_sign; // flipped the sign of the current literal
1136 TRACE("nlsat_simplify_core", tout << "odd degree\n";);
1137 }
1138 if (is_const(new_factor)) {
1139 TRACE("nlsat_simplify_core", tout << "new factor is const\n";);
1140 auto s = sign(new_factor);
1141 if (is_zero(s)) {
1142 bool atom_val = a->get_kind() == atom::EQ;
1143 bool lit_val = l.sign() ? !atom_val : atom_val;
1144 new_lit = lit_val ? true_literal : false_literal;
1145 TRACE("nlsat_simplify_core", tout << "zero sign: " << info.m_lc_const << "\n";);
1146 if (!info.m_lc_const) {
1147 // We have essentially shown the current factor must be zero If the leading coefficient is not zero.
1148 // Note that, if the current factor is zero, then the whole polynomial is zero.
1149 // The atom is true if it is an equality, and false otherwise.
1150 // The sign of the leading coefficient (info.m_lc) of info.m_eq doesn't matter.
1151 // However, we have to store the fact it is not zero.
1152 info.add_lc_diseq();
1153 }
1154 return;
1155 }
1156 else {
1157 TRACE("nlsat_simplify_core", tout << "non-zero sign: " << info.m_lc_const << "\n";);
1158 // We have shown the current factor is a constant MODULO the sign of the leading coefficient (of the equation used to rewrite the factor).
1159 if (!info.m_lc_const) {
1160 // If the leading coefficient is not a constant, we must store this information as an extra assumption.
1161 if (d % 2 == 0 || // d is even
1162 is_even || // rewriting a factor of even degree, sign flip doesn't matter
1163 _a->get_kind() == atom::EQ) { // rewriting an equation, sign flip doesn't matter
1164 info.add_lc_diseq();
1165 }
1166 else {
1167 info.add_lc_ineq();
1168 }
1169 }
1170 if (s < 0 && !is_even) {
1171 atom_sign = -atom_sign;
1172 }
1173 }
1174 }
1175 else {
1176 new_factors.push_back(new_factor);
1177 new_factors_even.push_back(is_even);
1178 if (!info.m_lc_const) {
1179 if (d % 2 == 0 || // d is even
1180 is_even || // rewriting a factor of even degree, sign flip doesn't matter
1181 _a->get_kind() == atom::EQ) { // rewriting an equation, sign flip doesn't matter
1182 info.add_lc_diseq();
1183 }
1184 else {
1185 info.add_lc_ineq();
1186 }
1187 }
1188 }
1189 }
1190 if (modified_lit) {
1191 atom::kind new_k = _a->get_kind();
1192 if (atom_sign < 0)
1193 new_k = atom::flip(new_k);
1194 new_lit = m_solver.mk_ineq_literal(new_k, new_factors.size(), new_factors.data(), new_factors_even.data());
1195 if (l.sign())
1196 new_lit.neg();
1197 TRACE("nlsat_simplify_core", tout << "simplified literal:\n"; display(tout, new_lit) << " " << m_solver.value(new_lit) << "\n";);
1198
1199 if (max_var(new_lit) < max) {
1200 if (m_solver.value(new_lit) == l_true) {
1201 new_lit = l;
1202 }
1203 else {
1204 add_literal(new_lit);
1205 new_lit = true_literal;
1206 }
1207 }
1208 else {
1209 new_lit = normalize(new_lit, max);
1210 TRACE("nlsat_simplify_core", tout << "simplified literal after normalization:\n"; display(tout, new_lit); tout << " " << m_solver.value(new_lit) << "\n";);
1211 }
1212 }
1213 else {
1214 new_lit = l;
1215 }
1216 }
1217
simplifynlsat::explain::imp1218 bool simplify(scoped_literal_vector & C, poly const * eq, var max) {
1219 bool modified_core = false;
1220 eq_info info;
1221 info.m_eq = eq;
1222 info.m_x = m_pm.max_var(info.m_eq);
1223 info.m_k = m_pm.degree(eq, info.m_x);
1224 polynomial_ref lc_eq(m_pm);
1225 lc_eq = m_pm.coeff(eq, info.m_x, info.m_k);
1226 info.m_lc = lc_eq.get();
1227 info.m_lc_sign = sign(lc_eq);
1228 info.m_lc_add = false;
1229 info.m_lc_add_ineq = false;
1230 info.m_lc_const = m_pm.is_const(lc_eq);
1231 SASSERT(info.m_lc != 0);
1232 scoped_literal new_lit(m_solver);
1233 unsigned sz = C.size();
1234 unsigned j = 0;
1235 for (unsigned i = 0; i < sz; i++) {
1236 literal l = C[i];
1237 new_lit = null_literal;
1238 simplify(l, info, max, new_lit);
1239 SASSERT(new_lit != null_literal);
1240 if (l == new_lit) {
1241 C.set(j, l);
1242 j++;
1243 continue;
1244 }
1245 modified_core = true;
1246 if (new_lit == true_literal)
1247 continue;
1248 if (new_lit == false_literal) {
1249 // false literal was created. The assumptions added are sufficient for implying the conflict.
1250 j = 0; // force core to be reset
1251 break;
1252 }
1253 C.set(j, new_lit);
1254 j++;
1255 }
1256 C.shrink(j);
1257 if (info.m_lc_add) {
1258 if (info.m_lc_add_ineq)
1259 add_assumption(info.m_lc_sign < 0 ? atom::LT : atom::GT, info.m_lc);
1260 else
1261 add_assumption(atom::EQ, info.m_lc, true);
1262 }
1263 return modified_core;
1264 }
1265
1266 /**
1267 \brief (try to) Select an equation from C. Returns 0 if C does not contain any equality.
1268 This method selects the equation of minimal degree in max.
1269 */
select_eqnlsat::explain::imp1270 poly * select_eq(scoped_literal_vector & C, var max) {
1271 poly * r = nullptr;
1272 unsigned min_d = UINT_MAX;
1273 unsigned sz = C.size();
1274 for (unsigned i = 0; i < sz; i++) {
1275 literal l = C[i];
1276 if (l.sign())
1277 continue;
1278 bool_var b = l.var();
1279 atom * a = m_atoms[b];
1280 SASSERT(a != 0);
1281 if (a->get_kind() != atom::EQ)
1282 continue;
1283 ineq_atom * _a = to_ineq_atom(a);
1284 if (_a->size() > 1)
1285 continue;
1286 if (_a->is_even(0))
1287 continue;
1288 unsigned d = m_pm.degree(_a->p(0), max);
1289 SASSERT(d > 0);
1290 if (d < min_d) {
1291 r = _a->p(0);
1292 min_d = d;
1293 if (min_d == 1)
1294 break;
1295 }
1296 }
1297 return r;
1298 }
1299
1300 /**
1301 \brief Select an equation eq s.t.
1302 max_var(eq) < max, and
1303 it can be used to rewrite a literal in C.
1304 Return 0, if such equation was not found.
1305 */
1306 var_vector m_select_tmp;
select_lower_stage_eqnlsat::explain::imp1307 ineq_atom * select_lower_stage_eq(scoped_literal_vector & C, var max) {
1308 var_vector & xs = m_select_tmp;
1309 for (literal l : C) {
1310 bool_var b = l.var();
1311 atom * a = m_atoms[b];
1312 if (a->is_root_atom())
1313 continue; // we don't rewrite root atoms
1314 ineq_atom * _a = to_ineq_atom(a);
1315 unsigned num_factors = _a->size();
1316 for (unsigned j = 0; j < num_factors; j++) {
1317 poly * p = _a->p(j);
1318 xs.reset();
1319 m_pm.vars(p, xs);
1320 for (var y : xs) {
1321 if (y >= max)
1322 continue;
1323 atom * eq = m_x2eq[y];
1324 if (eq == nullptr)
1325 continue;
1326 SASSERT(eq->is_ineq_atom());
1327 SASSERT(to_ineq_atom(eq)->size() == 1);
1328 SASSERT(!to_ineq_atom(eq)->is_even(0));
1329 poly * eq_p = to_ineq_atom(eq)->p(0);
1330 SASSERT(m_pm.degree(eq_p, y) > 0);
1331 // TODO: create a parameter
1332 // In the current experiments, using equations with non constant coefficients produces a blowup
1333 if (!m_pm.nonzero_const_coeff(eq_p, y, m_pm.degree(eq_p, y)))
1334 continue;
1335 if (m_pm.degree(p, y) >= m_pm.degree(eq_p, y))
1336 return to_ineq_atom(eq);
1337 }
1338 }
1339 }
1340 return nullptr;
1341 }
1342
1343 /**
1344 \brief Simplify the core using equalities.
1345 */
simplifynlsat::explain::imp1346 void simplify(scoped_literal_vector & C, var max) {
1347 // Simplify using equations in the core
1348 while (!C.empty()) {
1349 poly * eq = select_eq(C, max);
1350 if (eq == nullptr)
1351 break;
1352 TRACE("nlsat_simplify_core", tout << "using equality for simplifying core\n";
1353 m_pm.display(tout, eq, m_solver.display_proc()); tout << "\n";);
1354 if (!simplify(C, eq, max))
1355 break;
1356 }
1357 // Simplify using equations using variables from lower stages.
1358 while (!C.empty()) {
1359 ineq_atom * eq = select_lower_stage_eq(C, max);
1360 if (eq == nullptr)
1361 break;
1362 SASSERT(eq->size() == 1);
1363 SASSERT(!eq->is_even(0));
1364 poly * eq_p = eq->p(0);
1365 VERIFY(simplify(C, eq_p, max));
1366 // add equation as an assumption
1367 TRACE("nlsat_simpilfy_core", display(tout << "adding equality as assumption ", literal(eq->bvar(), true)); tout << "\n";);
1368 add_literal(literal(eq->bvar(), true));
1369 }
1370 }
1371
1372 /**
1373 \brief Main procedure. The explain the given unsat core, and store the result in m_result
1374 */
mainnlsat::explain::imp1375 void main(unsigned num, literal const * ls) {
1376 if (num == 0)
1377 return;
1378 collect_polys(num, ls, m_ps);
1379 var max_x = max_var(m_ps);
1380 TRACE("nlsat_explain", tout << "polynomials in the conflict:\n"; display(tout, m_ps); tout << "\n";);
1381 elim_vanishing(m_ps);
1382 TRACE("nlsat_explain", tout << "elim vanishing\n"; display(tout, m_ps); tout << "\n";);
1383 project(m_ps, max_x);
1384 TRACE("nlsat_explain", tout << "after projection\n"; display(tout, m_ps); tout << "\n";);
1385 }
1386
process2nlsat::explain::imp1387 void process2(unsigned num, literal const * ls) {
1388 if (m_simplify_cores) {
1389 m_core2.reset();
1390 m_core2.append(num, ls);
1391 var max = max_var(num, ls);
1392 SASSERT(max != null_var);
1393 normalize(m_core2, max);
1394 TRACE("nlsat_explain", display(tout << "core after normalization\n", m_core2) << "\n";);
1395 simplify(m_core2, max);
1396 TRACE("nlsat_explain", display(tout << "core after simplify\n", m_core2) << "\n";);
1397 main(m_core2.size(), m_core2.data());
1398 m_core2.reset();
1399 }
1400 else {
1401 main(num, ls);
1402 }
1403 }
1404
1405 // Auxiliary method for core minimization.
1406 literal_vector m_min_newtodo;
minimize_corenlsat::explain::imp1407 bool minimize_core(literal_vector & todo, literal_vector & core) {
1408 SASSERT(!todo.empty());
1409 literal_vector & new_todo = m_min_newtodo;
1410 new_todo.reset();
1411 interval_set_manager & ism = m_evaluator.ism();
1412 interval_set_ref r(ism);
1413 // Copy the union of the infeasible intervals of core into r.
1414 unsigned sz = core.size();
1415 for (unsigned i = 0; i < sz; i++) {
1416 literal l = core[i];
1417 atom * a = m_atoms[l.var()];
1418 SASSERT(a != 0);
1419 interval_set_ref inf = m_evaluator.infeasible_intervals(a, l.sign(), nullptr);
1420 r = ism.mk_union(inf, r);
1421 if (ism.is_full(r)) {
1422 // Done
1423 return false;
1424 }
1425 }
1426 TRACE("nlsat_minimize", tout << "interval set after adding partial core:\n" << r << "\n";);
1427 if (todo.size() == 1) {
1428 // Done
1429 core.push_back(todo[0]);
1430 return false;
1431 }
1432 // Copy the union of the infeasible intervals of todo into r until r becomes full.
1433 sz = todo.size();
1434 for (unsigned i = 0; i < sz; i++) {
1435 literal l = todo[i];
1436 atom * a = m_atoms[l.var()];
1437 SASSERT(a != 0);
1438 interval_set_ref inf = m_evaluator.infeasible_intervals(a, l.sign(), nullptr);
1439 r = ism.mk_union(inf, r);
1440 if (ism.is_full(r)) {
1441 // literal l must be in the core
1442 core.push_back(l);
1443 new_todo.swap(todo);
1444 return !todo.empty();
1445 }
1446 else {
1447 new_todo.push_back(l);
1448 }
1449 }
1450 UNREACHABLE();
1451 return true;
1452 }
1453
1454 literal_vector m_min_todo;
1455 literal_vector m_min_core;
minimizenlsat::explain::imp1456 void minimize(unsigned num, literal const * ls, scoped_literal_vector & r) {
1457 literal_vector & todo = m_min_todo;
1458 literal_vector & core = m_min_core;
1459 todo.reset(); core.reset();
1460 todo.append(num, ls);
1461 while (true) {
1462 TRACE("nlsat_minimize", tout << "core minimization:\n"; display(tout, todo); tout << "\nCORE:\n"; display(tout, core) << "\n";);
1463 if (!minimize_core(todo, core))
1464 break;
1465 std::reverse(todo.begin(), todo.end());
1466 TRACE("nlsat_minimize", tout << "core minimization:\n"; display(tout, todo); tout << "\nCORE:\n"; display(tout, core) << "\n";);
1467 if (!minimize_core(todo, core))
1468 break;
1469 }
1470 TRACE("nlsat_minimize", tout << "core:\n"; display(tout, core););
1471 r.append(core.size(), core.data());
1472 }
1473
processnlsat::explain::imp1474 void process(unsigned num, literal const * ls) {
1475 if (m_minimize_cores && num > 1) {
1476 m_core1.reset();
1477 minimize(num, ls, m_core1);
1478 process2(m_core1.size(), m_core1.data());
1479 m_core1.reset();
1480 }
1481 else {
1482 process2(num, ls);
1483 }
1484 }
1485
operator ()nlsat::explain::imp1486 void operator()(unsigned num, literal const * ls, scoped_literal_vector & result) {
1487 SASSERT(check_already_added());
1488 SASSERT(num > 0);
1489 TRACE("nlsat_explain",
1490 tout << "[explain] set of literals is infeasible in the current interpretation\n";
1491 display(tout, num, ls) << "\n";
1492 m_assignment.display(tout);
1493 );
1494 m_result = &result;
1495 process(num, ls);
1496 reset_already_added();
1497 m_result = nullptr;
1498 TRACE("nlsat_explain", display(tout << "[explain] result\n", result) << "\n";);
1499 CASSERT("nlsat", check_already_added());
1500 }
1501
1502
projectnlsat::explain::imp1503 void project(var x, unsigned num, literal const * ls, scoped_literal_vector & result) {
1504
1505 m_result = &result;
1506 svector<literal> lits;
1507 TRACE("nlsat", tout << "project x" << x << "\n";
1508 m_solver.display(tout, num, ls);
1509 m_solver.display(tout););
1510
1511 DEBUG_CODE(
1512 for (unsigned i = 0; i < num; ++i) {
1513 SASSERT(m_solver.value(ls[i]) == l_true);
1514 atom* a = m_atoms[ls[i].var()];
1515 SASSERT(!a || m_evaluator.eval(a, ls[i].sign()));
1516 });
1517 split_literals(x, num, ls, lits);
1518 collect_polys(lits.size(), lits.data(), m_ps);
1519 var mx_var = max_var(m_ps);
1520 if (!m_ps.empty()) {
1521 svector<var> renaming;
1522 if (x != mx_var) {
1523 for (var i = 0; i < m_solver.num_vars(); ++i) {
1524 renaming.push_back(i);
1525 }
1526 std::swap(renaming[x], renaming[mx_var]);
1527 m_solver.reorder(renaming.size(), renaming.data());
1528 TRACE("qe", tout << "x: " << x << " max: " << mx_var << " num_vars: " << m_solver.num_vars() << "\n";
1529 m_solver.display(tout););
1530 }
1531 elim_vanishing(m_ps);
1532 if (m_signed_project) {
1533 signed_project(m_ps, mx_var);
1534 }
1535 else {
1536 project(m_ps, mx_var);
1537 }
1538 reset_already_added();
1539 m_result = nullptr;
1540 if (x != mx_var) {
1541 m_solver.restore_order();
1542 }
1543 }
1544 else {
1545 reset_already_added();
1546 m_result = nullptr;
1547 }
1548 for (unsigned i = 0; i < result.size(); ++i) {
1549 result.set(i, ~result[i]);
1550 }
1551 DEBUG_CODE(
1552 TRACE("nlsat", m_solver.display(tout, result.size(), result.data()) << "\n"; );
1553 for (literal l : result) {
1554 CTRACE("nlsat", l_true != m_solver.value(l), m_solver.display(tout, l) << " " << m_solver.value(l) << "\n";);
1555 SASSERT(l_true == m_solver.value(l));
1556 });
1557
1558 }
1559
split_literalsnlsat::explain::imp1560 void split_literals(var x, unsigned n, literal const* ls, svector<literal>& lits) {
1561 var_vector vs;
1562 for (unsigned i = 0; i < n; ++i) {
1563 vs.reset();
1564 m_solver.vars(ls[i], vs);
1565 if (vs.contains(x)) {
1566 lits.push_back(ls[i]);
1567 }
1568 else {
1569 add_literal(~ls[i]);
1570 }
1571 }
1572 }
1573
1574 /**
1575 Signed projection.
1576
1577 Assumptions:
1578 - any variable in ps is at most x.
1579 - root expressions are satisfied (positive literals)
1580
1581 Effect:
1582 - if x not in p, then
1583 - if sign(p) < 0: p < 0
1584 - if sign(p) = 0: p = 0
1585 - if sign(p) > 0: p > 0
1586 else:
1587 - let roots_j be the roots of p_j or roots_j[i]
1588 - let L = { roots_j[i] | M(roots_j[i]) < M(x) }
1589 - let U = { roots_j[i] | M(roots_j[i]) > M(x) }
1590 - let E = { roots_j[i] | M(roots_j[i]) = M(x) }
1591 - let glb in L, s.t. forall l in L . M(glb) >= M(l)
1592 - let lub in U, s.t. forall u in U . M(lub) <= M(u)
1593 - if root in E, then
1594 - add E x . x = root & x > lb for lb in L
1595 - add E x . x = root & x < ub for ub in U
1596 - add E x . x = root & x = root2 for root2 in E \ { root }
1597 - else
1598 - assume |L| <= |U| (other case is symmetric)
1599 - add E x . lb <= x & x <= glb for lb in L
1600 - add E x . x = glb & x < ub for ub in U
1601 */
1602
1603
signed_projectnlsat::explain::imp1604 void signed_project(polynomial_ref_vector& ps, var x) {
1605
1606 TRACE("nlsat_explain", tout << "Signed projection\n";);
1607 polynomial_ref p(m_pm);
1608 unsigned eq_index = 0;
1609 bool eq_valid = false;
1610 unsigned eq_degree = 0;
1611 for (unsigned i = 0; i < ps.size(); ++i) {
1612 p = ps.get(i);
1613 int s = sign(p);
1614 if (max_var(p) != x) {
1615 atom::kind k = (s == 0)?(atom::EQ):((s < 0)?(atom::LT):(atom::GT));
1616 add_simple_assumption(k, p, false);
1617 ps[i] = ps.back();
1618 ps.pop_back();
1619 --i;
1620 }
1621 else if (s == 0) {
1622 if (!eq_valid || degree(p, x) < eq_degree) {
1623 eq_index = i;
1624 eq_valid = true;
1625 eq_degree = degree(p, x);
1626 }
1627 }
1628 }
1629
1630 if (ps.empty()) {
1631 return;
1632 }
1633
1634 if (ps.size() == 1) {
1635 project_single(x, ps.get(0));
1636 return;
1637 }
1638
1639 // ax + b = 0, p(x) > 0 ->
1640
1641 if (eq_valid) {
1642 p = ps.get(eq_index);
1643 if (degree(p, x) == 1) {
1644 // ax + b = 0
1645 // let d be maximal degree of x in p.
1646 // p(x) -> a^d*p(-b/a), a
1647 // perform virtual substitution with equality.
1648 solve_eq(x, eq_index, ps);
1649 }
1650 else {
1651 project_pairs(x, eq_index, ps);
1652 }
1653 return;
1654 }
1655
1656 unsigned num_lub = 0, num_glb = 0;
1657 unsigned glb_index = 0, lub_index = 0;
1658 scoped_anum lub(m_am), glb(m_am), x_val(m_am);
1659 x_val = m_assignment.value(x);
1660 bool glb_valid = false, lub_valid = false;
1661 for (unsigned i = 0; i < ps.size(); ++i) {
1662 p = ps.get(i);
1663 scoped_anum_vector & roots = m_roots_tmp;
1664 roots.reset();
1665 m_am.isolate_roots(p, undef_var_assignment(m_assignment, x), roots);
1666 for (auto const& r : roots) {
1667 int s = m_am.compare(x_val, r);
1668 SASSERT(s != 0);
1669
1670 if (s < 0 && (!lub_valid || m_am.lt(r, lub))) {
1671 lub_index = i;
1672 m_am.set(lub, r);
1673 lub_valid = true;
1674 }
1675
1676 if (s > 0 && (!glb_valid || m_am.lt(glb, r))) {
1677 glb_index = i;
1678 m_am.set(glb, r);
1679 glb_valid = true;
1680 }
1681 if (s < 0) ++num_lub;
1682 if (s > 0) ++num_glb;
1683 }
1684 }
1685 TRACE("nlsat_explain", tout << "glb: " << num_glb << " lub: " << num_lub << "\n" << lub_index << "\n" << glb_index << "\n" << ps << "\n";);
1686
1687 if (num_lub == 0) {
1688 project_plus_infinity(x, ps);
1689 return;
1690 }
1691
1692 if (num_glb == 0) {
1693 project_minus_infinity(x, ps);
1694 return;
1695 }
1696
1697 if (num_lub <= num_glb) {
1698 glb_index = lub_index;
1699 }
1700
1701 project_pairs(x, glb_index, ps);
1702 }
1703
project_plus_infinitynlsat::explain::imp1704 void project_plus_infinity(var x, polynomial_ref_vector const& ps) {
1705 polynomial_ref p(m_pm), lc(m_pm);
1706 for (unsigned i = 0; i < ps.size(); ++i) {
1707 p = ps.get(i);
1708 unsigned d = degree(p, x);
1709 lc = m_pm.coeff(p, x, d);
1710 if (!is_const(lc)) {
1711 int s = sign(p);
1712 SASSERT(s != 0);
1713 atom::kind k = (s > 0)?(atom::GT):(atom::LT);
1714 add_simple_assumption(k, lc);
1715 }
1716 }
1717 }
1718
project_minus_infinitynlsat::explain::imp1719 void project_minus_infinity(var x, polynomial_ref_vector const& ps) {
1720 polynomial_ref p(m_pm), lc(m_pm);
1721 for (unsigned i = 0; i < ps.size(); ++i) {
1722 p = ps.get(i);
1723 unsigned d = degree(p, x);
1724 lc = m_pm.coeff(p, x, d);
1725 if (!is_const(lc)) {
1726 int s = sign(p);
1727 TRACE("nlsat_explain", tout << "degree: " << d << " " << lc << " sign: " << s << "\n";);
1728 SASSERT(s != 0);
1729 atom::kind k;
1730 if (s > 0) {
1731 k = (d % 2 == 0)?(atom::GT):(atom::LT);
1732 }
1733 else {
1734 k = (d % 2 == 0)?(atom::LT):(atom::GT);
1735 }
1736 add_simple_assumption(k, lc);
1737 }
1738 }
1739 }
1740
project_pairsnlsat::explain::imp1741 void project_pairs(var x, unsigned idx, polynomial_ref_vector const& ps) {
1742 TRACE("nlsat_explain", tout << "project pairs\n";);
1743 polynomial_ref p(m_pm);
1744 p = ps.get(idx);
1745 for (unsigned i = 0; i < ps.size(); ++i) {
1746 if (i != idx) {
1747 project_pair(x, ps.get(i), p);
1748 }
1749 }
1750 }
1751
project_pairnlsat::explain::imp1752 void project_pair(var x, polynomial::polynomial* p1, polynomial::polynomial* p2) {
1753 m_ps2.reset();
1754 m_ps2.push_back(p1);
1755 m_ps2.push_back(p2);
1756 project(m_ps2, x);
1757 }
1758
project_singlenlsat::explain::imp1759 void project_single(var x, polynomial::polynomial* p) {
1760 m_ps2.reset();
1761 m_ps2.push_back(p);
1762 project(m_ps2, x);
1763 }
1764
solve_eqnlsat::explain::imp1765 void solve_eq(var x, unsigned idx, polynomial_ref_vector const& ps) {
1766 polynomial_ref p(m_pm), A(m_pm), B(m_pm), C(m_pm), D(m_pm), E(m_pm), q(m_pm), r(m_pm);
1767 polynomial_ref_vector As(m_pm), Bs(m_pm);
1768 p = ps.get(idx);
1769 SASSERT(degree(p, x) == 1);
1770 A = m_pm.coeff(p, x, 1);
1771 B = m_pm.coeff(p, x, 0);
1772 As.push_back(m_pm.mk_const(rational(1)));
1773 Bs.push_back(m_pm.mk_const(rational(1)));
1774 B = neg(B);
1775 TRACE("nlsat_explain", tout << "p: " << p << " A: " << A << " B: " << B << "\n";);
1776 // x = B/A
1777 for (unsigned i = 0; i < ps.size(); ++i) {
1778 if (i != idx) {
1779 q = ps.get(i);
1780 unsigned d = degree(q, x);
1781 D = m_pm.mk_const(rational(1));
1782 E = D;
1783 r = m_pm.mk_zero();
1784 for (unsigned j = As.size(); j <= d; ++j) {
1785 D = As.back(); As.push_back(A * D);
1786 D = Bs.back(); Bs.push_back(B * D);
1787 }
1788 for (unsigned j = 0; j <= d; ++j) {
1789 // A^d*p0 + A^{d-1}*B*p1 + ... + B^j*A^{d-j}*pj + ... + B^d*p_d
1790 C = m_pm.coeff(q, x, j);
1791 TRACE("nlsat_explain", tout << "coeff: q" << j << ": " << C << "\n";);
1792 if (!is_zero(C)) {
1793 D = As.get(d - j);
1794 E = Bs.get(j);
1795 r = r + D*E*C;
1796 }
1797 }
1798 TRACE("nlsat_explain", tout << "p: " << p << " q: " << q << " r: " << r << "\n";);
1799 ensure_sign(r);
1800 }
1801 else {
1802 ensure_sign(A);
1803 }
1804 }
1805
1806 }
1807
maximizenlsat::explain::imp1808 void maximize(var x, unsigned num, literal const * ls, scoped_anum& val, bool& unbounded) {
1809 svector<literal> lits;
1810 polynomial_ref p(m_pm);
1811 split_literals(x, num, ls, lits);
1812 collect_polys(lits.size(), lits.data(), m_ps);
1813 unbounded = true;
1814 scoped_anum x_val(m_am);
1815 x_val = m_assignment.value(x);
1816 for (unsigned i = 0; i < m_ps.size(); ++i) {
1817 p = m_ps.get(i);
1818 scoped_anum_vector & roots = m_roots_tmp;
1819 roots.reset();
1820 m_am.isolate_roots(p, undef_var_assignment(m_assignment, x), roots);
1821 for (unsigned j = 0; j < roots.size(); ++j) {
1822 int s = m_am.compare(x_val, roots[j]);
1823 if (s <= 0 && (unbounded || m_am.compare(roots[j], val) <= 0)) {
1824 unbounded = false;
1825 val = roots[j];
1826 }
1827 }
1828 }
1829 }
1830
1831 };
1832
explain(solver & s,assignment const & x2v,polynomial::cache & u,atom_vector const & atoms,atom_vector const & x2eq,evaluator & ev)1833 explain::explain(solver & s, assignment const & x2v, polynomial::cache & u,
1834 atom_vector const& atoms, atom_vector const& x2eq, evaluator & ev) {
1835 m_imp = alloc(imp, s, x2v, u, atoms, x2eq, ev);
1836 }
1837
~explain()1838 explain::~explain() {
1839 dealloc(m_imp);
1840 }
1841
reset()1842 void explain::reset() {
1843 m_imp->m_core1.reset();
1844 m_imp->m_core2.reset();
1845 }
1846
set_simplify_cores(bool f)1847 void explain::set_simplify_cores(bool f) {
1848 m_imp->m_simplify_cores = f;
1849 }
1850
set_full_dimensional(bool f)1851 void explain::set_full_dimensional(bool f) {
1852 m_imp->m_full_dimensional = f;
1853 }
1854
set_minimize_cores(bool f)1855 void explain::set_minimize_cores(bool f) {
1856 m_imp->m_minimize_cores = f;
1857 }
1858
set_factor(bool f)1859 void explain::set_factor(bool f) {
1860 m_imp->m_factor = f;
1861 }
1862
set_signed_project(bool f)1863 void explain::set_signed_project(bool f) {
1864 m_imp->m_signed_project = f;
1865 }
1866
operator ()(unsigned n,literal const * ls,scoped_literal_vector & result)1867 void explain::operator()(unsigned n, literal const * ls, scoped_literal_vector & result) {
1868 (*m_imp)(n, ls, result);
1869 }
1870
project(var x,unsigned n,literal const * ls,scoped_literal_vector & result)1871 void explain::project(var x, unsigned n, literal const * ls, scoped_literal_vector & result) {
1872 m_imp->project(x, n, ls, result);
1873 }
1874
maximize(var x,unsigned n,literal const * ls,scoped_anum & val,bool & unbounded)1875 void explain::maximize(var x, unsigned n, literal const * ls, scoped_anum& val, bool& unbounded) {
1876 m_imp->maximize(x, n, ls, val, unbounded);
1877 }
1878
test_root_literal(atom::kind k,var y,unsigned i,poly * p,scoped_literal_vector & result)1879 void explain::test_root_literal(atom::kind k, var y, unsigned i, poly* p, scoped_literal_vector & result) {
1880 m_imp->test_root_literal(k, y, i, p, result);
1881 }
1882
1883 };
1884
1885 #ifdef Z3DEBUG
pp(nlsat::explain::imp & ex,unsigned num,nlsat::literal const * ls)1886 void pp(nlsat::explain::imp & ex, unsigned num, nlsat::literal const * ls) {
1887 ex.display(std::cout, num, ls);
1888 }
pp(nlsat::explain::imp & ex,nlsat::scoped_literal_vector & ls)1889 void pp(nlsat::explain::imp & ex, nlsat::scoped_literal_vector & ls) {
1890 ex.display(std::cout, ls);
1891 }
pp(nlsat::explain::imp & ex,polynomial_ref const & p)1892 void pp(nlsat::explain::imp & ex, polynomial_ref const & p) {
1893 ex.display(std::cout, p);
1894 std::cout << std::endl;
1895 }
pp(nlsat::explain::imp & ex,polynomial::polynomial * p)1896 void pp(nlsat::explain::imp & ex, polynomial::polynomial * p) {
1897 polynomial_ref _p(p, ex.m_pm);
1898 ex.display(std::cout, _p);
1899 std::cout << std::endl;
1900 }
pp(nlsat::explain::imp & ex,polynomial_ref_vector const & ps)1901 void pp(nlsat::explain::imp & ex, polynomial_ref_vector const & ps) {
1902 ex.display(std::cout, ps);
1903 }
pp_var(nlsat::explain::imp & ex,nlsat::var x)1904 void pp_var(nlsat::explain::imp & ex, nlsat::var x) {
1905 ex.display(std::cout, x);
1906 std::cout << std::endl;
1907 }
pp_lit(nlsat::explain::imp & ex,nlsat::literal l)1908 void pp_lit(nlsat::explain::imp & ex, nlsat::literal l) {
1909 ex.display(std::cout, l);
1910 std::cout << std::endl;
1911 }
1912 #endif
1913
1914