mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 03:33:35 +00:00
Code Activity

fix #2556, sign of of inequality is not restricted to -1, 0, 1, but can be -2, -3 etc

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-09-14 19:41:01 -04:00
parent 0c972b8bee
commit 0f20175bdd
3 changed files with 18 additions and 24 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/cmd_context/cmd_context.cpp
View file

@ -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;
}
}

33
src/nlsat/nlsat_explain.cpp
View file

@ -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();

4
src/smt/theory_seq.cpp
View file

@ -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";
}
}