From 0f20175bdd716fc852395ae7ad54d169de3af42b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 14 Sep 2019 19:41:01 -0400 Subject: [PATCH] fix #2556, sign of of inequality is not restricted to -1, 0, 1, but can be -2, -3 etc Signed-off-by: Nikolaj Bjorner --- src/cmd_context/cmd_context.cpp | 5 +++-- src/nlsat/nlsat_explain.cpp | 33 +++++++++++++-------------------- src/smt/theory_seq.cpp | 4 ++-- 3 files changed, 18 insertions(+), 24 deletions(-) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 598c2a1f3fc..64007f5fd9e 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -1884,6 +1884,9 @@ void cmd_context::validate_model() { if (m().is_true(r)) continue; + analyze_failure(evaluator, a, true); + IF_VERBOSE(11, model_smt2_pp(verbose_stream(), *this, *md, 0);); + // The evaluator for array expressions is not complete // If r contains as_array/store/map/const expressions, then we do not generate the error. // TODO: improve evaluator for model expressions. @@ -1899,8 +1902,6 @@ void cmd_context::validate_model() { continue; } TRACE("model_validate", model_smt2_pp(tout, *this, *md, 0);); - analyze_failure(evaluator, a, true); - IF_VERBOSE(11, model_smt2_pp(verbose_stream(), *this, *md, 0);); invalid_model = true; } } diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index a2da3b31612..f90b38ca34d 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/src/nlsat/nlsat_explain.cpp @@ -157,32 +157,25 @@ namespace nlsat { ~imp() { } - void display(std::ostream & out, polynomial_ref const & p) const { + std::ostream& display(std::ostream & out, polynomial_ref const & p) const { m_pm.display(out, p, m_solver.display_proc()); + return out; } - void display(std::ostream & out, polynomial_ref_vector const & ps, char const * delim = "\n") const { + std::ostream& display(std::ostream & out, polynomial_ref_vector const & ps, char const * delim = "\n") const { for (unsigned i = 0; i < ps.size(); i++) { if (i > 0) out << delim; m_pm.display(out, ps.get(i), m_solver.display_proc()); } + return out; } - void display(std::ostream & out, literal l) const { m_solver.display(out, l); } - void display_var(std::ostream & out, var x) const { m_solver.display(out, x); } - void display(std::ostream & out, unsigned sz, literal const * ls) { - for (unsigned i = 0; i < sz; i++) { - display(out, ls[i]); - out << "\n"; - } - } - void display(std::ostream & out, literal_vector const & ls) { - display(out, ls.size(), ls.c_ptr()); - } - void display(std::ostream & out, scoped_literal_vector const & ls) { - display(out, ls.size(), ls.c_ptr()); - } + std::ostream& display(std::ostream & out, literal l) const { return m_solver.display(out, l); } + std::ostream& display_var(std::ostream & out, var x) const { return m_solver.display(out, x); } + std::ostream& display(std::ostream & out, unsigned sz, literal const * ls) const { return m_solver.display(out, sz, ls); } + std::ostream& display(std::ostream & out, literal_vector const & ls) const { return display(out, ls.size(), ls.c_ptr()); } + std::ostream& display(std::ostream & out, scoped_literal_vector const & ls) const { return display(out, ls.size(), ls.c_ptr()); } /** \brief Add literal to the result vector. @@ -430,7 +423,7 @@ namespace nlsat { bool lit_val = l.sign() ? !atom_val : atom_val; return lit_val ? true_literal : false_literal; } - else if (s == -1 && a->is_odd(i)) { + else if (s < 0 && a->is_odd(i)) { atom_sign = -atom_sign; } normalized = true; @@ -1135,7 +1128,7 @@ namespace nlsat { info.add_lc_ineq(); } } - if (s == -1 && !is_even) { + if (s < 0 && !is_even) { atom_sign = -atom_sign; } } @@ -1162,7 +1155,7 @@ namespace nlsat { new_lit = m_solver.mk_ineq_literal(new_k, new_factors.size(), new_factors.c_ptr(), new_factors_even.c_ptr()); if (l.sign()) new_lit.neg(); - TRACE("nlsat_simplify_core", tout << "simplified literal:\n"; display(tout, new_lit); tout << " " << m_solver.value(new_lit) << "\n";); + TRACE("nlsat_simplify_core", tout << "simplified literal:\n"; display(tout, new_lit) << " " << m_solver.value(new_lit) << "\n";); if (max_var(new_lit) < max) { if (m_solver.value(new_lit) == l_true) { @@ -1456,7 +1449,7 @@ namespace nlsat { void operator()(unsigned num, literal const * ls, scoped_literal_vector & result) { SASSERT(check_already_added()); SASSERT(num > 0); - TRACE("nlsat_explain", tout << "[explain] set of literals is infeasible in the current interpretation\n"; display(tout, num, ls);); + TRACE("nlsat_explain", tout << "[explain] set of literals is infeasible in the current interpretation\n"; display(tout, num, ls) << "\n";); m_result = &result; process(num, ls); reset_already_added(); diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 2d3db1f983a..626f268a915 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -1962,7 +1962,7 @@ bool theory_seq::fixed_length(expr* len_e, bool is_zero) { } seq = mk_concat(elems.size(), elems.c_ptr()); } - TRACE("seq", tout << "Fixed: " << mk_pp(e, m) << " " << lo << "\n";); + TRACE("seq", tout << "Fixed: " << mk_bounded_pp(e, m, 2) << " " << lo << "\n";); add_axiom(~mk_eq(len_e, m_autil.mk_numeral(lo, true), false), mk_seq_eq(seq, e)); if (!ctx.at_base_level()) { m_trail_stack.push(push_replay(alloc(replay_fixed_length, m, len_e))); @@ -3880,7 +3880,7 @@ void theory_seq::display(std::ostream & out) const { lower_bound(e, lo); upper_bound(e, hi); if (lo.is_pos() || !hi.is_minus_one()) { - out << mk_pp(e, m) << " [" << lo << ":" << hi << "]\n"; + out << mk_bounded_pp(e, m, 3) << " [" << lo << ":" << hi << "]\n"; } }