From 2b48092541925a0f89f3cf83e3dceffc7486f513 Mon Sep 17 00:00:00 2001 From: unknown Date: Sun, 23 Aug 2015 10:58:12 -0700 Subject: [PATCH 1/4] local sat solver change Signed-off-by: unknown --- src/sat/sat_solver.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 3d6130d5e..8761873bc 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -2626,7 +2626,7 @@ namespace sat { out << "p wcnf " << num_vars() << " " << num_clauses() + sz << " " << max_weight << "\n"; for (unsigned i = 0; i < m_trail.size(); i++) { - out << dimacs_lit(m_trail[i]) << " 0\n"; + out << max_weight << " " << dimacs_lit(m_trail[i]) << " 0\n"; } vector::const_iterator it = m_watches.begin(); vector::const_iterator end = m_watches.end(); From ee5f1ad6b62269624c961c45f44cab46daf904fb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 24 Aug 2015 15:55:40 -0700 Subject: [PATCH 2/4] fix issue #203: domain range was one too large Signed-off-by: unknown --- src/smt/theory_dl.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_dl.cpp b/src/smt/theory_dl.cpp index fc9138bf6..43ec5682e 100644 --- a/src/smt/theory_dl.cpp +++ b/src/smt/theory_dl.cpp @@ -235,13 +235,14 @@ namespace smt { } app* mk_bv_constant(uint64 val, sort* s) { - return b().mk_numeral(rational(val,rational::ui64()),64); + return b().mk_numeral(rational(val, rational::ui64()), 64); } app* max_value(sort* s) { uint64 sz; VERIFY(u().try_get_size(s, sz)); - return mk_bv_constant(sz, s); + SASSERT(sz > 0); + return mk_bv_constant(sz-1, s); } void mk_lt(app* x, app* y) { From ef7915858bca5e759ee0a34df2ae976e7e507bef Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 24 Aug 2015 16:27:07 -0700 Subject: [PATCH 3/4] add filter to detect circumventing the default semantics of bit-vector division with the use of the sat-based bit-vector solver. Provides a way to fix issue #190 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/bv_rewriter.h | 2 ++ src/tactic/bv/bv1_blaster_tactic.cpp | 3 +++ src/tactic/probe.cpp | 3 +++ 3 files changed, 8 insertions(+) diff --git a/src/ast/rewriter/bv_rewriter.h b/src/ast/rewriter/bv_rewriter.h index 26c5a33d5..1c9b44b52 100644 --- a/src/ast/rewriter/bv_rewriter.h +++ b/src/ast/rewriter/bv_rewriter.h @@ -168,6 +168,8 @@ public: } br_status mk_eq_core(expr * lhs, expr * rhs, expr_ref & result); + + bool hi_div0() const { return m_hi_div0; } }; #endif diff --git a/src/tactic/bv/bv1_blaster_tactic.cpp b/src/tactic/bv/bv1_blaster_tactic.cpp index 5f20015ca..f6a6017de 100644 --- a/src/tactic/bv/bv1_blaster_tactic.cpp +++ b/src/tactic/bv/bv1_blaster_tactic.cpp @@ -28,6 +28,7 @@ Notes: #include"rewriter_def.h" #include"for_each_expr.h" #include"cooperate.h" +#include"bv_rewriter.h" class bv1_blaster_tactic : public tactic { @@ -491,6 +492,8 @@ tactic * mk_bv1_blaster_tactic(ast_manager & m, params_ref const & p) { class is_qfbv_eq_probe : public probe { public: virtual result operator()(goal const & g) { + bv_rewriter rw(g.m()); + if (!rw.hi_div0()) return false; bv1_blaster_tactic t(g.m()); return t.is_target(g); diff --git a/src/tactic/probe.cpp b/src/tactic/probe.cpp index 0fdd49a6b..dd27691d3 100644 --- a/src/tactic/probe.cpp +++ b/src/tactic/probe.cpp @@ -23,6 +23,7 @@ Revision History: #include"arith_decl_plugin.h" #include"bv_decl_plugin.h" #include"goal_util.h" +#include"bv_rewriter.h" class memory_probe : public probe { public: @@ -303,6 +304,8 @@ public: class is_qfbv_probe : public probe { public: virtual result operator()(goal const & g) { + bv_rewriter rw(g.m()); + if (!rw.hi_div0()) return false; return !test(g); } }; From b2ebd095cb76eacb9fa4f083b1300e68f0035626 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 24 Aug 2015 17:01:46 -0700 Subject: [PATCH 4/4] fix for unintialized variable m_conflict_lvl Signed-off-by: Nikolaj Bjorner --- src/opt/maxres.cpp | 4 +++- src/sat/sat_solver.cpp | 1 + 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index 693200f61..f4d8e1b43 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -228,7 +228,6 @@ public: switch (is_sat) { case l_true: get_current_correction_set(cs); - IF_VERBOSE(2, display_vec(verbose_stream() << "correction set: ", cs);); if (cs.empty()) { m_found_feasible_optimum = m_model.get() != 0; m_lower = m_upper; @@ -350,9 +349,11 @@ public: is_sat = minimize_core(core); ++m_stats.m_num_cores; if (is_sat != l_true) { + IF_VERBOSE(100, verbose_stream() << "(opt.maxres minimization failed)\n";); break; } if (core.empty()) { + IF_VERBOSE(100, verbose_stream() << "(opt.maxres core is empty)\n";); cores.reset(); m_lower = m_upper; return l_true; @@ -470,6 +471,7 @@ public: SASSERT(!core.empty()); rational w = split_core(core); TRACE("opt", display_vec(tout << "minimized core: ", core);); + IF_VERBOSE(10, display_vec(verbose_stream() << "core: ", core);); max_resolve(core, w); fml = mk_not(m, mk_and(m, m_B.size(), m_B.c_ptr())); s().assert_expr(fml); diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index db82cbe0e..9d4f5df0f 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -964,6 +964,7 @@ namespace sat { set_conflict(justification(), ~lit); flet _min1(m_config.m_minimize_core, false); flet _min2(m_config.m_minimize_core_partial, false); + m_conflict_lvl = 1; resolve_conflict_for_unsat_core(); m_assumptions.pop_back(); weight += weights[i];