From fed977b492aa98d672a50abe8e5cca404bd214d1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Aug 2018 10:08:16 -0700 Subject: [PATCH] fix #1782 Signed-off-by: Nikolaj Bjorner --- scripts/update_api.py | 6 +++--- src/api/z3_logger.h | 1 + src/api/z3_replayer.cpp | 8 ++++++-- src/ast/ast.cpp | 1 + src/sat/ba_solver.cpp | 1 + src/sat/sat_solver.cpp | 13 ++++++++----- 6 files changed, 20 insertions(+), 10 deletions(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index 22c0dea99..375a855de 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -311,7 +311,7 @@ def display_args_to_z3(params): core_py.write("a%s" % i) i = i + 1 -NULLWrapped = [ 'Z3_mk_context', 'Z3_mk_context_rc', 'Z3_mk_interpolation_context' ] +NULLWrapped = [ 'Z3_mk_context', 'Z3_mk_context_rc' ] Unwrapped = [ 'Z3_del_context', 'Z3_get_error_code' ] def mk_py_wrappers(): @@ -955,9 +955,9 @@ def def_API(name, result, params): log_c.write(" Au(a%s);\n" % sz) exe_c.write("in.get_uint_array(%s)" % i) elif ty == INT: - log_c.write("U(a%s[i]);" % i) + log_c.write("I(a%s[i]);" % i) log_c.write(" }\n") - log_c.write(" Au(a%s);\n" % sz) + log_c.write(" Ai(a%s);\n" % sz) exe_c.write("in.get_int_array(%s)" % i) elif ty == BOOL: log_c.write("U(a%s[i]);" % i) diff --git a/src/api/z3_logger.h b/src/api/z3_logger.h index 211601713..8f0eb5371 100644 --- a/src/api/z3_logger.h +++ b/src/api/z3_logger.h @@ -42,6 +42,7 @@ static void __declspec(noinline) Sy(Z3_symbol sym) { } static void __declspec(noinline) Ap(unsigned sz) { *g_z3_log << "p " << sz << "\n"; g_z3_log->flush(); } static void __declspec(noinline) Au(unsigned sz) { *g_z3_log << "u " << sz << "\n"; g_z3_log->flush(); } +static void __declspec(noinline) Ai(unsigned sz) { *g_z3_log << "i " << sz << "\n"; g_z3_log->flush(); } static void __declspec(noinline) Asy(unsigned sz) { *g_z3_log << "s " << sz << "\n"; g_z3_log->flush(); } static void __declspec(noinline) C(unsigned id) { *g_z3_log << "C " << id << "\n"; g_z3_log->flush(); } void __declspec(noinline) _Z3_append_log(char const * msg) { *g_z3_log << "M \"" << ll_escaped(msg) << "\"\n"; g_z3_log->flush(); } diff --git a/src/api/z3_replayer.cpp b/src/api/z3_replayer.cpp index 0e8297879..8ebac8068 100644 --- a/src/api/z3_replayer.cpp +++ b/src/api/z3_replayer.cpp @@ -78,6 +78,7 @@ struct z3_replayer::imp { std::stringstream strm; strm << "expecting " << kind2string(k) << " at position " << pos << " but got " << kind2string(m_args[pos].m_kind); + TRACE("z3_replayer", tout << strm.str() << "\n";); throw z3_replayer_exception(strm.str().c_str()); } } @@ -186,10 +187,10 @@ struct z3_replayer::imp { sz++; } else { - throw z3_replayer_exception("invalid scaped character"); + throw z3_replayer_exception("invalid escaped character"); } if (val > 255) - throw z3_replayer_exception("invalid scaped character"); + throw z3_replayer_exception("invalid escaped character"); next(); } TRACE("z3_replayer_escape", tout << "val: " << val << "\n";); @@ -497,6 +498,7 @@ struct z3_replayer::imp { case 'p': case 's': case 'u': + case 'i': // push array next(); skip_blank(); read_uint64(); TRACE("z3_replayer", tout << "[" << m_line << "] " << "A " << m_uint64 << "\n";); @@ -504,6 +506,8 @@ struct z3_replayer::imp { push_array(static_cast(m_uint64), OBJECT); else if (c == 's') push_array(static_cast(m_uint64), SYMBOL); + else if (c == 'i') + push_array(static_cast(m_uint64), INT64); else push_array(static_cast(m_uint64), UINT64); break; diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 5a14a64c0..11a15492c 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1403,6 +1403,7 @@ void ast_manager::init() { inc_ref(m_false); } + template static void mark_array_ref(ast_mark& mark, unsigned sz, T * const * a) { for(unsigned i = 0; i < sz; i++) { diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp index 38cd07fa7..4226b9791 100644 --- a/src/sat/ba_solver.cpp +++ b/src/sat/ba_solver.cpp @@ -1976,6 +1976,7 @@ namespace sat { for (unsigned i = 0; !found && i < c.k(); ++i) { found = c[i] == l; } + CTRACE("ba",!found, s().display(tout << l << ":" << c << "\n");); SASSERT(found);); // IF_VERBOSE(0, if (_debug_conflict) verbose_stream() << "ante " << l << " " << c << "\n"); diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 04a0274c4..7ddc80813 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -1552,12 +1552,15 @@ namespace sat { void solver::reinit_assumptions() { if (tracking_assumptions() && at_base_lvl() && !inconsistent()) { TRACE("sat", tout << m_assumptions << "\n";); + if (!propagate(false)) return; push(); - for (unsigned i = 0; !inconsistent() && i < m_user_scope_literals.size(); ++i) { - assign(~m_user_scope_literals[i], justification()); + for (literal lit : m_user_scope_literals) { + if (inconsistent()) break; + assign(~lit, justification()); } - for (unsigned i = 0; !inconsistent() && i < m_assumptions.size(); ++i) { - assign(m_assumptions[i], justification()); + for (literal lit : m_assumptions) { + if (inconsistent()) break; + assign(lit, justification()); } TRACE("sat", for (literal a : m_assumptions) { @@ -2934,7 +2937,7 @@ namespace sat { break; } case justification::EXT_JUSTIFICATION: { - fill_ext_antecedents(m_lemma[i], js); + fill_ext_antecedents(~m_lemma[i], js); for (literal l : m_ext_antecedents) { update_lrb_reasoned(l); }