From f84de9400e7d63453234d0648980c5fd595b0e35 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 15 Feb 2019 17:58:26 -0800 Subject: [PATCH 01/41] also deal with initializing boolean variables in smt context Signed-off-by: Nikolaj Bjorner --- src/sat/sat_unit_walk.cpp | 18 +++++------------- src/sat/sat_unit_walk.h | 1 - src/smt/smt_kernel.cpp | 8 ++++++++ 3 files changed, 13 insertions(+), 14 deletions(-) diff --git a/src/sat/sat_unit_walk.cpp b/src/sat/sat_unit_walk.cpp index 314c275f3..8c7a6c6f9 100644 --- a/src/sat/sat_unit_walk.cpp +++ b/src/sat/sat_unit_walk.cpp @@ -99,6 +99,7 @@ namespace sat { while (s.rlimit().inc() && st == l_undef) { if (inconsistent() && !m_decisions.empty()) do_pop(); else if (inconsistent()) st = l_false; + else if (should_restart()) restart(); else if (should_backjump()) st = do_backjump(); else st = decide(); } @@ -276,9 +277,6 @@ namespace sat { init_runs(); init_phase(); } - if (false && should_restart()) { - restart(); - } } bool unit_walk::should_restart() { @@ -287,9 +285,7 @@ namespace sat { ++m_luby_index; return true; } - else { - return false; - } + return false; } void unit_walk::restart() { @@ -328,9 +324,9 @@ namespace sat { } void unit_walk::propagate() { - while (m_qhead < m_trail.size() && !inconsistent()) - propagate(choose_literal()); - // IF_VERBOSE(1, verbose_stream() << m_trail.size() << " " << inconsistent() << "\n";); + while (m_qhead < m_trail.size() && !inconsistent()) { + propagate(m_trail[m_qhead++]); + } } std::ostream& unit_walk::display(std::ostream& out) const { @@ -495,10 +491,6 @@ namespace sat { << ")\n";); } - literal unit_walk::choose_literal() { - return m_trail[m_qhead++]; - } - void unit_walk::set_conflict(literal l1, literal l2) { set_conflict(); } diff --git a/src/sat/sat_unit_walk.h b/src/sat/sat_unit_walk.h index 2aead871f..14588a63c 100644 --- a/src/sat/sat_unit_walk.h +++ b/src/sat/sat_unit_walk.h @@ -91,7 +91,6 @@ namespace sat { void flip_phase(literal l); void propagate(); void propagate(literal lit); - literal choose_literal(); void set_conflict(literal l1, literal l2); void set_conflict(literal l1, literal l2, literal l3); void set_conflict(clause const& c); diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp index 571032039..adcda3979 100644 --- a/src/smt/smt_kernel.cpp +++ b/src/smt/smt_kernel.cpp @@ -156,6 +156,14 @@ namespace smt { } void set_activity(expr* lit, double act) { + SASSERT(m().is_bool(lit)); + m().is_not(lit, lit); + if (!m_kernel.b_internalized(lit)) { + m_kernel.internalize(lit, false); + } + if (!m_kernel.b_internalized(lit)) { + return; + } auto v = m_kernel.get_bool_var(lit); double old_act = m_kernel.get_activity(v); m_kernel.set_activity(v, act); From 4f223542acb829a5085b4437dd6803ed2b7335c5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 16 Feb 2019 09:38:47 -0800 Subject: [PATCH 02/41] fix #2129 Signed-off-by: Nikolaj Bjorner --- src/model/model_evaluator.cpp | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index 53defbc3d..968aca51f 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -217,13 +217,18 @@ struct evaluator_cfg : public default_rewriter_cfg { return BR_DONE; } if (get_macro(g, def, q, def_pr)) { - sort_ref_vector vars(m); + sort_ref_vector sorts(m); + expr_ref_vector vars(m); svector var_names; - for (unsigned i = 0; i < g->get_arity(); ++i) { - var_names.push_back(symbol(i)); - vars.push_back(g->get_domain(i)); + unsigned sz = g->get_arity(); + for (unsigned i = 0; i < sz; ++i) { + var_names.push_back(symbol(sz - i - 1)); + vars.push_back(m.mk_var(sz - i - 1, g->get_domain(i))); + sorts.push_back(g->get_domain(i)); } - result = m.mk_lambda(vars.size(), vars.c_ptr(), var_names.c_ptr(), def); + var_subst subst(m, false); + result = subst(def, sorts.size(), vars.c_ptr()); + result = m.mk_lambda(sorts.size(), sorts.c_ptr(), var_names.c_ptr(), result); model_evaluator ev(m_model, m_params); result = ev(result); m_pinned.push_back(result); From 7f51cc79310b8503abb22e37c0feb449dc9b6969 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 16 Feb 2019 09:54:05 -0800 Subject: [PATCH 03/41] fix #2140 Signed-off-by: Nikolaj Bjorner --- src/tactic/portfolio/default_tactic.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/tactic/portfolio/default_tactic.cpp b/src/tactic/portfolio/default_tactic.cpp index 23334bf07..c2bccd75b 100644 --- a/src/tactic/portfolio/default_tactic.cpp +++ b/src/tactic/portfolio/default_tactic.cpp @@ -35,7 +35,7 @@ Notes: tactic * mk_default_tactic(ast_manager & m, params_ref const & p) { tactic * st = using_params(and_then(mk_simplify_tactic(m), - cond(mk_is_propositional_probe(), if_no_proofs(mk_fd_tactic(m, p)), + cond(mk_and(mk_is_propositional_probe(), mk_not(mk_produce_proofs_probe())), mk_fd_tactic(m, p), cond(mk_is_qfbv_probe(), mk_qfbv_tactic(m), cond(mk_is_qfaufbv_probe(), mk_qfaufbv_tactic(m), cond(mk_is_qflia_probe(), mk_qflia_tactic(m), From 886c62ef41106740589eb5806f579fddc55ba67e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 16 Feb 2019 10:30:44 -0800 Subject: [PATCH 04/41] add example from #2138 Signed-off-by: Nikolaj Bjorner --- examples/c++/example.cpp | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp index ab9c73209..f93045c9d 100644 --- a/examples/c++/example.cpp +++ b/examples/c++/example.cpp @@ -1166,6 +1166,14 @@ static void parse_example() { // expr b = c.parse_string("(benchmark tst :extrafuns ((x Int) (y Int)) :formula (> x y) :formula (> x 0))"); } +static void parse_string() { + std::cout << "parse string\n"; + z3::context c; + z3::solver s(c); + s.from_string("(declare-const x Int)(assert (> x 10))"); + std::cout << s.check() << "\n"; +} + void mk_model_example() { context c; @@ -1252,6 +1260,7 @@ int main() { sudoku_example(); std::cout << "\n"; consequence_example(); std::cout << "\n"; parse_example(); std::cout << "\n"; + parse_string(); std::cout << "\n"; mk_model_example(); std::cout << "\n"; recfun_example(); std::cout << "\n"; std::cout << "done\n"; From c1402ad70fc416b8fc8d814f7b4f85464bb451b0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 16 Feb 2019 20:39:15 -0800 Subject: [PATCH 05/41] tone down verbosity of integrity checking Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver.cpp | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index b933b6ddb..541c4f0f5 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -1790,11 +1790,11 @@ namespace sat { m_mc(m_model); if (!check_clauses(m_model)) { - IF_VERBOSE(0, verbose_stream() << "failure checking clauses on transformed model\n";); + IF_VERBOSE(1, verbose_stream() << "failure checking clauses on transformed model\n";); IF_VERBOSE(10, m_mc.display(verbose_stream())); //IF_VERBOSE(0, display_units(verbose_stream())); //IF_VERBOSE(0, display(verbose_stream())); - IF_VERBOSE(0, for (bool_var v = 0; v < num; v++) verbose_stream() << v << ": " << m_model[v] << "\n";); + IF_VERBOSE(1, for (bool_var v = 0; v < num; v++) verbose_stream() << v << ": " << m_model[v] << "\n";); throw solver_exception("check model failed"); } @@ -1806,8 +1806,8 @@ namespace sat { if (!m_clone->check_model(m_model)) { //IF_VERBOSE(0, display(verbose_stream())); //IF_VERBOSE(0, display_watches(verbose_stream())); - IF_VERBOSE(0, m_mc.display(verbose_stream())); - IF_VERBOSE(0, display_units(verbose_stream())); + IF_VERBOSE(1, m_mc.display(verbose_stream())); + IF_VERBOSE(1, display_units(verbose_stream())); //IF_VERBOSE(0, m_clone->display(verbose_stream() << "clone\n")); throw solver_exception("check model failed (for cloned solver)"); } @@ -1819,7 +1819,7 @@ namespace sat { for (clause const* cp : m_clauses) { clause const & c = *cp; if (!c.satisfied_by(m)) { - IF_VERBOSE(0, verbose_stream() << "failed clause " << c.id() << ": " << c << "\n";); + IF_VERBOSE(1, verbose_stream() << "failed clause " << c.id() << ": " << c << "\n";); TRACE("sat", tout << "failed: " << c << "\n"; tout << "assumptions: " << m_assumptions << "\n"; tout << "trail: " << m_trail << "\n"; @@ -1827,7 +1827,7 @@ namespace sat { m_mc.display(tout); ); for (literal l : c) { - if (was_eliminated(l.var())) IF_VERBOSE(0, verbose_stream() << "eliminated: " << l << "\n";); + if (was_eliminated(l.var())) IF_VERBOSE(1, verbose_stream() << "eliminated: " << l << "\n";); } ok = false; } @@ -1843,8 +1843,8 @@ namespace sat { if (l.index() > l2.index()) continue; if (value_at(l2, m) != l_true) { - IF_VERBOSE(0, verbose_stream() << "failed binary: " << l << " := " << value_at(l, m) << " " << l2 << " := " << value_at(l2, m) << "\n"); - IF_VERBOSE(0, verbose_stream() << "elim l1: " << was_eliminated(l.var()) << " elim l2: " << was_eliminated(l2) << "\n"); + IF_VERBOSE(1, verbose_stream() << "failed binary: " << l << " := " << value_at(l, m) << " " << l2 << " := " << value_at(l2, m) << "\n"); + IF_VERBOSE(1, verbose_stream() << "elim l1: " << was_eliminated(l.var()) << " elim l2: " << was_eliminated(l2) << "\n"); TRACE("sat", m_mc.display(tout << "failed binary: " << l << " " << l2 << "\n");); ok = false; } @@ -1855,7 +1855,7 @@ namespace sat { for (literal l : m_assumptions) { if (value_at(l, m) != l_true) { VERIFY(is_external(l.var())); - IF_VERBOSE(0, verbose_stream() << "assumption: " << l << " does not model check " << value_at(l, m) << "\n";); + IF_VERBOSE(1, verbose_stream() << "assumption: " << l << " does not model check " << value_at(l, m) << "\n";); TRACE("sat", tout << l << " does not model check\n"; tout << "trail: " << m_trail << "\n"; @@ -1876,8 +1876,8 @@ namespace sat { if (ok && !m_mc.check_model(m)) { ok = false; TRACE("sat", tout << "model: " << m << "\n"; m_mc.display(tout);); + IF_VERBOSE(0, verbose_stream() << "model check failed\n"); } - IF_VERBOSE(1, verbose_stream() << "model check " << (ok?"OK":"failed") << "\n";); return ok; } From ea778eefb2fdba2102f8c1e6064b4e7968360822 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 16 Feb 2019 20:58:30 -0800 Subject: [PATCH 06/41] skip optimization Signed-off-by: Nikolaj Bjorner --- src/opt/maxlex.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/opt/maxlex.cpp b/src/opt/maxlex.cpp index b2799f1c8..111d6f07a 100644 --- a/src/opt/maxlex.cpp +++ b/src/opt/maxlex.cpp @@ -245,6 +245,7 @@ namespace opt { // every time probing whether to include soft_i, // include suffix that is known to be assignable to T + // lbool maxlexN() { unsigned sz = m_soft.size(); for (unsigned i = 0; i < sz; ++i) { @@ -297,7 +298,7 @@ namespace opt { lbool operator()() override { init(); - return maxlexN(); + return maxlex1(); } From 8c085f1a185087c82075a963e31f0f62acf40c94 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 16 Feb 2019 21:26:29 -0800 Subject: [PATCH 07/41] removing unused and fixing suspect optimization Signed-off-by: Nikolaj Bjorner --- src/opt/maxlex.cpp | 137 +++------------------------------------------ 1 file changed, 8 insertions(+), 129 deletions(-) diff --git a/src/opt/maxlex.cpp b/src/opt/maxlex.cpp index 111d6f07a..56dbfebf5 100644 --- a/src/opt/maxlex.cpp +++ b/src/opt/maxlex.cpp @@ -74,11 +74,6 @@ namespace opt { } } - void set_value(soft& soft, lbool v) { - soft.set_value(v); - assert_value(soft); - } - void update_assignment(model_ref & mdl) { bool first_undef = true, second_undef = false; for (auto & soft : m_soft) { @@ -95,7 +90,9 @@ namespace opt { soft.set_value(v); } else { - set_value(soft, v); // also update constraints + SASSERT(v == l_true); + soft.set_value(v); + assert_value(soft); } } } @@ -130,121 +127,8 @@ namespace opt { if (mdl) update_assignment(mdl); } - lbool maxlex1() { - for (auto & soft : m_soft) { - if (soft.value == l_true) { - continue; - } - SASSERT(soft.value == l_undef); - expr* a = soft.s; - lbool is_sat = s().check_sat(1, &a); - switch (is_sat) { - case l_false: - set_value(soft, l_false); - update_bounds(); - break; - case l_true: - update_assignment(); - SASSERT(soft.value == l_true); - break; - case l_undef: - return l_undef; - } - } - return l_true; - } - - // try two literals per round. - // doesn't seem to make a difference based on sample test. - lbool maxlex2() { - unsigned sz = m_soft.size(); - for (unsigned i = 0; i < sz; ++i) { - auto& soft = m_soft[i]; - if (soft.value != l_undef) { - continue; - } - SASSERT(soft.value == l_undef); - if (i + 1 == sz) { - expr* a = soft.s; - lbool is_sat = s().check_sat(1, &a); - switch (is_sat) { - case l_false: - set_value(soft, l_false); - update_bounds(); - break; - case l_true: - update_assignment(); - SASSERT(soft.value == l_true); - break; - case l_undef: - return l_undef; - } - } - else { - auto& soft2 = m_soft[i+1]; - expr_ref_vector core(m); - expr* a = soft.s; - expr* b = soft2.s; - expr* asms[2] = { a, b }; - lbool is_sat = s().check_sat(2, asms); - switch (is_sat) { - case l_true: - update_assignment(); - SASSERT(soft.value == l_true); - SASSERT(soft2.value == l_true); - break; - case l_false: - s().get_unsat_core(core); - if (core.contains(b)) { - expr_ref not_b(mk_not(m, b), m); - asms[1] = not_b; - switch (s().check_sat(2, asms)) { - case l_true: - // a, b is unsat, a, not b is sat. - set_value(soft2, l_false); - update_assignment(); - SASSERT(soft.value == l_true); - SASSERT(soft2.value == l_false); - break; - case l_false: - // a, b is unsat, a, not b is unsat -> a is unsat - // b is unsat, a, not b is unsat -> not a, not b - set_value(soft, l_false); - // core1 = { b } - // core2 = { a, not b } - if (!core.contains(a)) { - set_value(soft2, l_false); - } - else { - // core1 = { a, b} - // core2 = { not_b } - core.reset(); - s().get_unsat_core(core); - if (!core.contains(a)) { - set_value(soft2, l_true); - } - } - update_bounds(); - break; - case l_undef: - return l_undef; - } - } - else { - set_value(soft, l_false); - update_bounds(); - } - break; - case l_undef: - return l_undef; - } - } - } - return l_true; - } - - // every time probing whether to include soft_i, - // include suffix that is known to be assignable to T + // + // include soft constraints that are known to be assignable to true after failed literal. // lbool maxlexN() { unsigned sz = m_soft.size(); @@ -255,12 +139,6 @@ namespace opt { } expr_ref_vector asms(m); asms.push_back(soft.s); - for (unsigned j = i + 1; j < sz; ++j) { - auto& soft2 = m_soft[j]; - if (soft2.value == l_true) { - asms.push_back(soft2.s); - } - } lbool is_sat = s().check_sat(asms); switch (is_sat) { case l_true: @@ -268,7 +146,8 @@ namespace opt { SASSERT(soft.value == l_true); break; case l_false: - set_value(soft, l_false); + soft.set_value(l_false); + assert_value(soft); for (unsigned j = i + 1; j < sz; ++j) { auto& soft2 = m_soft[j]; if (soft2.value != l_true) { @@ -298,7 +177,7 @@ namespace opt { lbool operator()() override { init(); - return maxlex1(); + return maxlexN(); } From 5b57c6b780f156b0d757c3aecf82d080bbc8c71e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 17 Feb 2019 01:30:26 -0800 Subject: [PATCH 08/41] unused variable warnings Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/hoist_rewriter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/rewriter/hoist_rewriter.cpp b/src/ast/rewriter/hoist_rewriter.cpp index 5deeebdf4..31909f12b 100644 --- a/src/ast/rewriter/hoist_rewriter.cpp +++ b/src/ast/rewriter/hoist_rewriter.cpp @@ -69,7 +69,6 @@ br_status hoist_rewriter::mk_or(unsigned num_args, expr * const * es, expr_ref & turn = !turn; (*preds)[turn].reset(); reset(m_uf0); - unsigned v1 = 0, v2 = 0; VERIFY(is_and(es[j], args[turn])); for (expr* e : *args[turn]) { @@ -196,6 +195,7 @@ bool hoist_rewriter::is_and(expr * e, expr_ref_vector* args) { void hoist_rewriter::reset(basic_union_find& uf) { uf.reset(); for (expr* e : m_var2expr) { + (void)e; uf.mk_var(); } } From 0aafa8b7ce3adb82125d72c10370151e35a2fd18 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 18 Feb 2019 15:52:42 +0100 Subject: [PATCH 09/41] optimize binary output Signed-off-by: Nikolaj Bjorner --- src/sat/sat_drat.cpp | 19 ++++++++++++------- src/sat/sat_simplifier.cpp | 1 - 2 files changed, 12 insertions(+), 8 deletions(-) diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp index c0799c061..f8e04a583 100644 --- a/src/sat/sat_drat.cpp +++ b/src/sat/sat_drat.cpp @@ -120,22 +120,27 @@ namespace sat { case status::deleted: ch = 'd'; break; default: UNREACHABLE(); break; } - (*m_bout) << ch; + char buffer[10000]; + int len = 0; + buffer[len++] = ch; for (unsigned i = 0; i < n; ++i) { literal lit = c[i]; unsigned v = 2 * lit.var() + (lit.sign() ? 1 : 0); do { - ch = static_cast(v & ((1 << 7) - 1)); + ch = static_cast(v & 255); v >>= 7; - if (v) ch |= (1 << 7); - //std::cout << std::hex << ((unsigned char)ch) << std::dec << " "; - (*m_bout) << ch; + if (v) ch |= 128; + buffer[len++] = ch; + if (len == sizeof(buffer)) { + m_bout->write(buffer, len); + len = 0; + } } while (v); } - ch = 0; - (*m_bout) << ch; + buffer[len++] = 0; + m_bout->write(buffer, len); } bool drat::is_cleaned(clause& c) const { diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index f536dda03..58dab0ff5 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -1222,7 +1222,6 @@ namespace sat { RI literals. */ void minimize_covered_clause(unsigned idx) { - literal _blocked = m_covered_clause[idx]; for (literal l : m_tautology) VERIFY(s.is_marked(l)); for (literal l : m_covered_clause) s.unmark_visited(l); for (literal l : m_tautology) s.mark_visited(l); From 7fb2c6a908d5e1a1c4740e0bd3e1b104e33fff19 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 18 Feb 2019 15:55:24 +0100 Subject: [PATCH 10/41] turn off model validation unless specified by parameter Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 541c4f0f5..779cb7aad 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -1788,7 +1788,10 @@ namespace sat { // m_mc.set_solver(nullptr); m_mc(m_model); - + + if (!gparams::get_ref().get_bool("model_validate", false)) { + return; + } if (!check_clauses(m_model)) { IF_VERBOSE(1, verbose_stream() << "failure checking clauses on transformed model\n";); IF_VERBOSE(10, m_mc.display(verbose_stream())); From 591abead4bf9e6c931ec9db691b0ae346e3fc287 Mon Sep 17 00:00:00 2001 From: Audrey Dutcher Date: Mon, 18 Feb 2019 23:51:11 -0700 Subject: [PATCH 11/41] Revert "Don't delete the reference to the native library in the python bindings" This reverts commit 3339be6d221567f372fac19ef53215beff8b0164. --- scripts/update_api.py | 1 + 1 file changed, 1 insertion(+) diff --git a/scripts/update_api.py b/scripts/update_api.py index 557ac4c6c..161c783e8 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -1704,6 +1704,7 @@ def write_exe_c_preamble(exe_c): def write_core_py_post(core_py): core_py.write(""" # Clean up +del _lib del _default_dirs del _all_dirs del _ext From c2cb2c9fad49d59821a8239c3ad0cb4cef0c5b16 Mon Sep 17 00:00:00 2001 From: Audrey Dutcher Date: Mon, 18 Feb 2019 23:59:27 -0700 Subject: [PATCH 12/41] python bindings: add core functions with _bytes suffix that do not decode strings --- scripts/update_api.py | 47 +++++++++++++++++++++++++------------------ 1 file changed, 27 insertions(+), 20 deletions(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index 161c783e8..6b953eefe 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -338,26 +338,33 @@ def Z3_set_error_handler(ctx, hndlr, _elems=Elementaries(_lib.Z3_set_error_handl """) for sig in _API2PY: - name = sig[0] - result = sig[1] - params = sig[2] - num = len(params) - core_py.write("def %s(" % name) - display_args(num) - comma = ", " if num != 0 else "" - core_py.write("%s_elems=Elementaries(_lib.%s)):\n" % (comma, name)) - lval = "r = " if result != VOID else "" - core_py.write(" %s_elems.f(" % lval) - display_args_to_z3(params) - core_py.write(")\n") - if len(params) > 0 and param_type(params[0]) == CONTEXT and not name in Unwrapped: - core_py.write(" _elems.Check(a0)\n") - if result == STRING: - core_py.write(" return _to_pystr(r)\n") - elif result != VOID: - core_py.write(" return r\n") - core_py.write("\n") - core_py + mk_py_wrapper_single(sig) + if sig[1] == STRING: + mk_py_wrapper_single(sig, decode_string=False) + +def mk_py_wrapper_single(sig, decode_string=True): + name = sig[0] + result = sig[1] + params = sig[2] + num = len(params) + def_name = name + if not decode_string: + def_name += '_bytes' + core_py.write("def %s(" % def_name) + display_args(num) + comma = ", " if num != 0 else "" + core_py.write("%s_elems=Elementaries(_lib.%s)):\n" % (comma, name)) + lval = "r = " if result != VOID else "" + core_py.write(" %s_elems.f(" % lval) + display_args_to_z3(params) + core_py.write(")\n") + if len(params) > 0 and param_type(params[0]) == CONTEXT and not name in Unwrapped: + core_py.write(" _elems.Check(a0)\n") + if result == STRING and decode_string: + core_py.write(" return _to_pystr(r)\n") + elif result != VOID: + core_py.write(" return r\n") + core_py.write("\n") ## .NET API native interface From 2138a5232f61a3fa5d18b99cfc671e276d069505 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 19 Feb 2019 10:16:50 +0100 Subject: [PATCH 13/41] fix #2142 Signed-off-by: Nikolaj Bjorner --- src/ast/bv_decl_plugin.cpp | 4 ++++ src/sat/sat_drat.cpp | 15 +++++++++++---- 2 files changed, 15 insertions(+), 4 deletions(-) diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp index 6bbe3ce13..7071f169c 100644 --- a/src/ast/bv_decl_plugin.cpp +++ b/src/ast/bv_decl_plugin.cpp @@ -548,11 +548,15 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p case OP_ROTATE_LEFT: if (arity != 1) m_manager->raise_exception("rotate left expects one argument"); + if (num_parameters != 1 || !parameters[0].is_int()) + m_manager->raise_exception("rotate left expects one integer parameter"); return m_manager->mk_func_decl(m_rotate_left_sym, arity, domain, domain[0], func_decl_info(m_family_id, k, num_parameters, parameters)); case OP_ROTATE_RIGHT: if (arity != 1) m_manager->raise_exception("rotate right expects one argument"); + if (num_parameters != 1 || !parameters[0].is_int()) + m_manager->raise_exception("rotate right expects one integer parameter"); return m_manager->mk_func_decl(m_rotate_right_sym, arity, domain, domain[0], func_decl_info(m_family_id, k, num_parameters, parameters)); case OP_REPEAT: diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp index f8e04a583..ac05b50f1 100644 --- a/src/sat/sat_drat.cpp +++ b/src/sat/sat_drat.cpp @@ -173,7 +173,13 @@ namespace sat { if (st == status::deleted) { return; } - assign_propagate(l); + if (m_check_unsat) { + assign_propagate(l); + } + + clause* c = s.alloc_clause(1, &l, st == status::learned); + m_proof.push_back(c); + m_status.push_back(st); } void drat::append(literal l1, literal l2, status st) { @@ -190,6 +196,7 @@ namespace sat { clause* c = s.alloc_clause(2, lits, st == status::learned); m_proof.push_back(c); m_status.push_back(st); + if (!m_check_unsat) return; unsigned idx = m_watched_clauses.size(); m_watched_clauses.push_back(watched_clause(c, l1, l2)); m_watches[(~l1).index()].push_back(idx); @@ -362,7 +369,7 @@ namespace sat { void drat::validate_propagation() const { for (unsigned i = 0; i < m_proof.size(); ++i) { status st = m_status[i]; - if (m_proof[i] && st != status::deleted) { + if (m_proof[i] && m_proof[i]->size() > 1 && st != status::deleted) { clause& c = *m_proof[i]; unsigned num_undef = 0, num_true = 0; for (unsigned j = 0; j < c.size(); ++j) { @@ -385,7 +392,7 @@ namespace sat { SASSERT(lits.size() == n); for (unsigned i = 0; i < m_proof.size(); ++i) { status st = m_status[i]; - if (m_proof[i] && (st == status::asserted || st == status::external)) { + if (m_proof[i] && m_proof[i]->size() > 1 && (st == status::asserted || st == status::external)) { clause& c = *m_proof[i]; unsigned j = 0; for (; j < c.size() && c[j] != ~l; ++j) {} @@ -583,7 +590,7 @@ namespace sat { void drat::add() { if (m_out) (*m_out) << "0\n"; - if (m_bout) bdump(0, nullptr, learned); + if (m_bout) bdump(0, nullptr, status::learned); if (m_check_unsat) { SASSERT(m_inconsistent); } From 8c2584bcf702859605f0a0a48de3cad0670bd9bd Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 19 Feb 2019 10:51:53 +0000 Subject: [PATCH 14/41] eliminate a few ref incs/decs plus remove unused variable --- src/tactic/bv/elim_small_bv_tactic.cpp | 9 ++------- 1 file changed, 2 insertions(+), 7 deletions(-) diff --git a/src/tactic/bv/elim_small_bv_tactic.cpp b/src/tactic/bv/elim_small_bv_tactic.cpp index a9f94ca3f..9608ab0f7 100644 --- a/src/tactic/bv/elim_small_bv_tactic.cpp +++ b/src/tactic/bv/elim_small_bv_tactic.cpp @@ -37,7 +37,6 @@ class elim_small_bv_tactic : public tactic { bv_util m_util; th_rewriter m_simp; ref m_mc; - goal * m_goal; unsigned m_max_bits; unsigned long long m_max_steps; unsigned long long m_max_memory; // in bytes @@ -53,7 +52,6 @@ class elim_small_bv_tactic : public tactic { m_bindings(_m), m_num_eliminated(0) { updt_params(p); - m_goal = nullptr; m_max_steps = UINT_MAX; } @@ -76,7 +74,7 @@ class elim_small_bv_tactic : public tactic { TRACE("elim_small_bv", tout << "replace idx " << idx << " with " << mk_ismt2_pp(replacement, m) << " in " << mk_ismt2_pp(e, m) << std::endl;); expr_ref res(m); - expr_ref_vector substitution(m); + ptr_vector substitution; substitution.resize(num_decls, nullptr); substitution[num_decls - idx - 1] = replacement; @@ -152,9 +150,7 @@ class elim_small_bv_tactic : public tactic { expr_ref_vector new_bodies(m); for (unsigned j = 0; j < bv_sz && !max_steps_exceeded(num_steps); j ++) { expr_ref n(m_util.mk_numeral(j, bv_sz), m); - expr_ref nb(m); - nb = replace_var(uv, num_decls, max_var_idx_p1, i, s, body, n); - new_bodies.push_back(nb); + new_bodies.push_back(replace_var(uv, num_decls, max_var_idx_p1, i, s, body, n)); num_steps++; } @@ -250,7 +246,6 @@ public: fail_if_unsat_core_generation("elim-small-bv", g); m_rw.cfg().m_produce_models = g->models_enabled(); - m_rw.m_cfg.m_goal = g.get(); expr_ref new_curr(m); proof_ref new_pr(m); unsigned size = g->size(); From 8e4ef19f45380aec024a8835e13150928b5f6ebc Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 19 Feb 2019 10:54:41 +0000 Subject: [PATCH 15/41] fix debug build --- src/tactic/bv/elim_small_bv_tactic.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/tactic/bv/elim_small_bv_tactic.cpp b/src/tactic/bv/elim_small_bv_tactic.cpp index 9608ab0f7..256586896 100644 --- a/src/tactic/bv/elim_small_bv_tactic.cpp +++ b/src/tactic/bv/elim_small_bv_tactic.cpp @@ -92,7 +92,7 @@ class elim_small_bv_tactic : public tactic { TRACE("elim_small_bv", tout << "substitution: " << std::endl; for (unsigned k = 0; k < substitution.size(); k++) { - expr * se = substitution[k].get(); + expr * se = substitution[k]; tout << k << " = "; if (se == 0) tout << "0"; else tout << mk_ismt2_pp(se, m); From edf0df634d5564cff49b463851081f5a135261f2 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 19 Feb 2019 13:18:20 +0000 Subject: [PATCH 16/41] simplifications to refs --- src/ackermannization/lackr.cpp | 2 +- src/ackermannization/lackr_model_constructor.cpp | 10 +++------- src/util/obj_ref.h | 6 ++---- src/util/ref_buffer.h | 6 ++++++ src/util/ref_vector.h | 4 ++-- 5 files changed, 14 insertions(+), 14 deletions(-) diff --git a/src/ackermannization/lackr.cpp b/src/ackermannization/lackr.cpp index a965fc261..4fe7797d4 100644 --- a/src/ackermannization/lackr.cpp +++ b/src/ackermannization/lackr.cpp @@ -122,7 +122,7 @@ bool lackr::ackr(app * const t1, app * const t2) { TRACE("ackermannize", tout << "ackr constr abs:" << mk_ismt2_pp(cga, m_m, 2) << "\n";); if (m_m.is_true(cga)) return false; m_st.m_ackrs_sz++; - m_ackrs.push_back(cga); + m_ackrs.push_back(std::move(cga)); return true; } diff --git a/src/ackermannization/lackr_model_constructor.cpp b/src/ackermannization/lackr_model_constructor.cpp index df0aac15e..f24a53cdb 100644 --- a/src/ackermannization/lackr_model_constructor.cpp +++ b/src/ackermannization/lackr_model_constructor.cpp @@ -237,7 +237,7 @@ struct lackr_model_constructor::imp { // handle functions if (m_ackr_helper.should_ackermannize(a)) { // handle uninterpreted app_ref key(m_m.mk_app(a->get_decl(), values.c_ptr()), m_m); - if (!make_value_uninterpreted_function(a, values, key.get(), result)) { + if (!make_value_uninterpreted_function(a, key.get(), result)) { return false; } } @@ -284,7 +284,6 @@ struct lackr_model_constructor::imp { } bool make_value_uninterpreted_function(app* a, - expr_ref_vector& values, app* key, expr_ref& result) { // get ackermann constant @@ -370,15 +369,12 @@ lackr_model_constructor::lackr_model_constructor(ast_manager& m, ackr_info_ref i {} lackr_model_constructor::~lackr_model_constructor() { - if (m_imp) dealloc(m_imp); + dealloc(m_imp); } bool lackr_model_constructor::check(model_ref& abstr_model) { m_conflicts.reset(); - if (m_imp) { - dealloc(m_imp); - m_imp = nullptr; - } + dealloc(m_imp); m_imp = alloc(lackr_model_constructor::imp, m_m, m_info, abstr_model, m_conflicts); const bool rv = m_imp->check(); m_state = rv ? CHECKED : CONFLICT; diff --git a/src/util/obj_ref.h b/src/util/obj_ref.h index 8908f2cdd..e3b0d0710 100644 --- a/src/util/obj_ref.h +++ b/src/util/obj_ref.h @@ -94,10 +94,8 @@ public: obj_ref & operator=(obj_ref && n) { SASSERT(&m_manager == &n.m_manager); - if (this != &n) { - std::swap(m_obj, n.m_obj); - n.reset(); - } + std::swap(m_obj, n.m_obj); + n.reset(); return *this; } diff --git a/src/util/ref_buffer.h b/src/util/ref_buffer.h index 4768c3f28..49213cc62 100644 --- a/src/util/ref_buffer.h +++ b/src/util/ref_buffer.h @@ -58,6 +58,12 @@ public: inc_ref(n); m_buffer.push_back(n); } + + template + void push_back(obj_ref && n) { + m_buffer.push_back(n.get()); + n.steal(); + } void pop_back() { SASSERT(!m_buffer.empty()); diff --git a/src/util/ref_vector.h b/src/util/ref_vector.h index d0e9a8f55..732ec20dd 100644 --- a/src/util/ref_vector.h +++ b/src/util/ref_vector.h @@ -99,8 +99,8 @@ public: return *this; } - template - ref_vector_core& push_back(obj_ref && n) { + template + ref_vector_core& push_back(obj_ref && n) { m_nodes.push_back(n.get()); n.steal(); return *this; From 61272fdc0cfa742adc25f8059c40d3d82f7b7888 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 19 Feb 2019 13:36:39 +0000 Subject: [PATCH 17/41] remove a few more inc/dec refs --- src/ast/rewriter/der.cpp | 6 ++---- src/ast/rewriter/distribute_forall.cpp | 3 +-- src/ast/rewriter/var_subst.cpp | 7 ++----- src/tactic/core/distribute_forall_tactic.cpp | 6 ++---- 4 files changed, 7 insertions(+), 15 deletions(-) diff --git a/src/ast/rewriter/der.cpp b/src/ast/rewriter/der.cpp index 027846c31..c95c07f63 100644 --- a/src/ast/rewriter/der.cpp +++ b/src/ast/rewriter/der.cpp @@ -374,13 +374,11 @@ void der::apply_substitution(quantifier * q, expr_ref & r) { expr_ref_buffer new_patterns(m_manager); expr_ref_buffer new_no_patterns(m_manager); for (unsigned j = 0; j < q->get_num_patterns(); j++) { - expr_ref new_pat = m_subst(q->get_pattern(j), m_subst_map.size(), m_subst_map.c_ptr()); - new_patterns.push_back(new_pat); + new_patterns.push_back(m_subst(q->get_pattern(j), m_subst_map.size(), m_subst_map.c_ptr())); } for (unsigned j = 0; j < q->get_num_no_patterns(); j++) { - expr_ref new_nopat = m_subst(q->get_no_pattern(j), m_subst_map.size(), m_subst_map.c_ptr()); - new_no_patterns.push_back(new_nopat); + new_no_patterns.push_back(m_subst(q->get_no_pattern(j), m_subst_map.size(), m_subst_map.c_ptr())); } r = m_manager.update_quantifier(q, new_patterns.size(), new_patterns.c_ptr(), diff --git a/src/ast/rewriter/distribute_forall.cpp b/src/ast/rewriter/distribute_forall.cpp index 54d7e2eca..c621579cb 100644 --- a/src/ast/rewriter/distribute_forall.cpp +++ b/src/ast/rewriter/distribute_forall.cpp @@ -126,8 +126,7 @@ void distribute_forall::reduce1_quantifier(quantifier * q) { br.mk_not(arg, not_arg); quantifier_ref tmp_q(m_manager); tmp_q = m_manager.update_quantifier(q, not_arg); - expr_ref new_q = elim_unused_vars(m_manager, tmp_q, params_ref()); - new_args.push_back(new_q); + new_args.push_back(elim_unused_vars(m_manager, tmp_q, params_ref())); } expr_ref result(m_manager); // m_bsimp.mk_and actually constructs a (not (or ...)) formula, diff --git a/src/ast/rewriter/var_subst.cpp b/src/ast/rewriter/var_subst.cpp index cbd79e08c..ff479b565 100644 --- a/src/ast/rewriter/var_subst.cpp +++ b/src/ast/rewriter/var_subst.cpp @@ -135,17 +135,14 @@ expr_ref unused_vars_eliminator::operator()(quantifier* q) { return result; } - expr_ref tmp(m); expr_ref_buffer new_patterns(m); expr_ref_buffer new_no_patterns(m); for (unsigned i = 0; i < num_patterns; i++) { - tmp = m_subst(q->get_pattern(i), var_mapping.size(), var_mapping.c_ptr()); - new_patterns.push_back(tmp); + new_patterns.push_back(m_subst(q->get_pattern(i), var_mapping.size(), var_mapping.c_ptr())); } for (unsigned i = 0; i < num_no_patterns; i++) { - tmp = m_subst(q->get_no_pattern(i), var_mapping.size(), var_mapping.c_ptr()); - new_no_patterns.push_back(tmp); + new_no_patterns.push_back(m_subst(q->get_no_pattern(i), var_mapping.size(), var_mapping.c_ptr())); } result = m.mk_quantifier(q->get_kind(), diff --git a/src/tactic/core/distribute_forall_tactic.cpp b/src/tactic/core/distribute_forall_tactic.cpp index c2688f741..800644d9e 100644 --- a/src/tactic/core/distribute_forall_tactic.cpp +++ b/src/tactic/core/distribute_forall_tactic.cpp @@ -49,8 +49,7 @@ class distribute_forall_tactic : public tactic { expr * not_arg = m.mk_not(arg); quantifier_ref tmp_q(m); tmp_q = m.update_quantifier(old_q, not_arg); - expr_ref new_q = elim_unused_vars(m, tmp_q, params_ref()); - new_args.push_back(new_q); + new_args.push_back(elim_unused_vars(m, tmp_q, params_ref())); } result = m.mk_and(new_args.size(), new_args.c_ptr()); return true; @@ -68,8 +67,7 @@ class distribute_forall_tactic : public tactic { expr * arg = to_app(new_body)->get_arg(i); quantifier_ref tmp_q(m); tmp_q = m.update_quantifier(old_q, arg); - expr_ref new_q = elim_unused_vars(m, tmp_q, params_ref()); - new_args.push_back(new_q); + new_args.push_back(elim_unused_vars(m, tmp_q, params_ref())); } result = m.mk_and(new_args.size(), new_args.c_ptr()); return true; From caa15ea04d555dd494cfe38beb960d6c61716112 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 19 Feb 2019 18:17:07 +0100 Subject: [PATCH 18/41] enable cardinality constraints in nla2bv Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver.cpp | 47 +++++++++++++-------------- src/sat/sat_solver.h | 1 + src/tactic/arith/nla2bv_tactic.cpp | 37 ++++++++++++++------- src/tactic/smtlogics/qfnia_tactic.cpp | 18 ++++++---- 4 files changed, 60 insertions(+), 43 deletions(-) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 779cb7aad..2df184c88 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -1779,41 +1779,30 @@ namespace sat { } #endif - IF_VERBOSE(10, verbose_stream() << "\"checking model\"\n";); - if (!check_clauses(m_model)) { - throw solver_exception("check model failed"); + if (m_clone) { + IF_VERBOSE(10, verbose_stream() << "\"checking model\"\n";); + if (!check_clauses(m_model)) { + throw solver_exception("check model failed"); + } } - if (m_config.m_drat) m_drat.check_model(m_model); + if (m_config.m_drat) { + m_drat.check_model(m_model); + } - // m_mc.set_solver(nullptr); m_mc(m_model); - if (!gparams::get_ref().get_bool("model_validate", false)) { - return; - } - if (!check_clauses(m_model)) { + if (m_clone && !check_clauses(m_model)) { IF_VERBOSE(1, verbose_stream() << "failure checking clauses on transformed model\n";); IF_VERBOSE(10, m_mc.display(verbose_stream())); - //IF_VERBOSE(0, display_units(verbose_stream())); - //IF_VERBOSE(0, display(verbose_stream())); - IF_VERBOSE(1, for (bool_var v = 0; v < num; v++) verbose_stream() << v << ": " << m_model[v] << "\n";); - + IF_VERBOSE(10, display_model(verbose_stream())); throw solver_exception("check model failed"); } - TRACE("sat", for (bool_var v = 0; v < num; v++) tout << v << ": " << m_model[v] << "\n";); - - if (m_clone) { - IF_VERBOSE(1, verbose_stream() << "\"checking model (on original set of clauses)\"\n";); - if (!m_clone->check_model(m_model)) { - //IF_VERBOSE(0, display(verbose_stream())); - //IF_VERBOSE(0, display_watches(verbose_stream())); - IF_VERBOSE(1, m_mc.display(verbose_stream())); - IF_VERBOSE(1, display_units(verbose_stream())); - //IF_VERBOSE(0, m_clone->display(verbose_stream() << "clone\n")); - throw solver_exception("check model failed (for cloned solver)"); - } + if (m_clone && !m_clone->check_model(m_model)) { + IF_VERBOSE(1, m_mc.display(verbose_stream())); + IF_VERBOSE(1, display_units(verbose_stream())); + throw solver_exception("check model failed (for cloned solver)"); } } @@ -3546,6 +3535,14 @@ namespace sat { return true; } + std::ostream& solver::display_model(std::ostream& out) const { + unsigned num = num_vars(); + for (bool_var v = 0; v < num; v++) { + out << v << ": " << m_model[v] << "\n"; + } + return out; +} + void solver::display_binary(std::ostream & out) const { unsigned sz = m_watches.size(); for (unsigned l_idx = 0; l_idx < sz; l_idx++) { diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 89b161c9f..53c3062a8 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -668,6 +668,7 @@ namespace sat { void display_watches(std::ostream & out) const; void display_watches(std::ostream & out, literal lit) const; void display_dimacs(std::ostream & out) const override; + std::ostream& display_model(std::ostream& out) const; void display_wcnf(std::ostream & out, unsigned sz, literal const* lits, unsigned const* weights) const; void display_assignment(std::ostream & out) const; std::ostream& display_justification(std::ostream & out, justification const& j) const; diff --git a/src/tactic/arith/nla2bv_tactic.cpp b/src/tactic/arith/nla2bv_tactic.cpp index 06150e18b..0a58740d1 100644 --- a/src/tactic/arith/nla2bv_tactic.cpp +++ b/src/tactic/arith/nla2bv_tactic.cpp @@ -21,6 +21,7 @@ Notes: #include "tactic/tactical.h" #include "ast/arith_decl_plugin.h" #include "ast/bv_decl_plugin.h" +#include "ast/pb_decl_plugin.h" #include "ast/for_each_expr.h" #include "ast/rewriter/expr_replacer.h" #include "util/optional.h" @@ -85,13 +86,18 @@ class nla2bv_tactic : public tactic { TRACE("nla2bv", g.display(tout); tout << "Muls: " << count_mul(g) << "\n"; ); + tactic_report report("nla->bv", g); m_fmc = alloc(generic_model_converter, m_manager, "nla2bv"); m_bounds(g); collect_power2(g); - if(!collect_vars(g)) { + switch (collect_vars(g)) { + case has_num: + break; + case not_supported: throw tactic_exception("goal is not in the fragment supported by nla2bv"); + case is_bool: + return; } - tactic_report report("nla->bv", g); substitute_vars(g); TRACE("nla2bv", g.display(tout << "substitute vars\n");); reduce_bv2int(g); @@ -308,27 +314,30 @@ class nla2bv_tactic : public tactic { class get_uninterp_proc { imp& m_imp; + arith_util& a; + ast_manager& m; + pb_util pb; ptr_vector m_vars; bool m_in_supported_fragment; public: - get_uninterp_proc(imp& s): m_imp(s), m_in_supported_fragment(true) {} + get_uninterp_proc(imp& s): m_imp(s), a(s.m_arith), m(a.get_manager()), pb(m), m_in_supported_fragment(true) {} ptr_vector const& vars() { return m_vars; } void operator()(var * n) { m_in_supported_fragment = false; } void operator()(app* n) { - arith_util& a = m_imp.m_arith; - ast_manager& m = a.get_manager(); - if (a.is_int(n) && - is_uninterp_const(n)) { + if (a.is_int(n) && is_uninterp_const(n)) { + TRACE("nla2bv", tout << "Not supported: " << mk_ismt2_pp(n, m) << "\n";); m_vars.push_back(n); } - else if (a.is_real(n) && - is_uninterp_const(n)) { + else if (a.is_real(n) && is_uninterp_const(n)) { m_vars.push_back(n); } else if (m.is_bool(n) && is_uninterp_const(n)) { + } + else if (m.is_bool(n) && n->get_decl()->get_family_id() == pb.get_family_id()) { + } else if (!(a.is_mul(n) || a.is_add(n) || @@ -342,7 +351,7 @@ class nla2bv_tactic : public tactic { m_imp.m_bv2real.is_pos_le(n) || m_imp.m_bv2real.is_pos_lt(n) || n->get_family_id() == a.get_manager().get_basic_family_id())) { - TRACE("nla2bv", tout << "Not supported: " << mk_ismt2_pp(n, a.get_manager()) << "\n";); + TRACE("nla2bv", tout << "Not supported: " << mk_ismt2_pp(n, m) << "\n";); m_in_supported_fragment = false; } m_imp.update_num_bits(n); @@ -353,13 +362,17 @@ class nla2bv_tactic : public tactic { bool is_supported() const { return m_in_supported_fragment; } }; - bool collect_vars(goal const & g) { + enum collect_t { has_num, not_supported, is_bool }; + + collect_t collect_vars(goal const & g) { get_uninterp_proc fe_var(*this); for_each_expr_at(fe_var, g); for (unsigned i = 0; i < fe_var.vars().size(); ++i) { add_var(fe_var.vars()[i]); } - return fe_var.is_supported() && !fe_var.vars().empty(); + if (!fe_var.is_supported()) return not_supported; + if (!fe_var.vars().empty()) return is_bool; + return has_num; } class count_mul_proc { diff --git a/src/tactic/smtlogics/qfnia_tactic.cpp b/src/tactic/smtlogics/qfnia_tactic.cpp index d28034a1d..528a6c048 100644 --- a/src/tactic/smtlogics/qfnia_tactic.cpp +++ b/src/tactic/smtlogics/qfnia_tactic.cpp @@ -27,6 +27,7 @@ Notes: #include "sat/tactic/sat_tactic.h" #include "tactic/arith/nla2bv_tactic.h" #include "tactic/arith/lia2card_tactic.h" +#include "tactic/arith/card2bv_tactic.h" #include "tactic/core/ctx_simplify_tactic.h" #include "tactic/core/cofactor_term_ite_tactic.h" #include "nlsat/tactic/qfnra_nlsat_tactic.h" @@ -73,7 +74,8 @@ static tactic * mk_qfnia_premable(ast_manager & m, params_ref const & p_ref) { using_params(mk_ctx_simplify_tactic(m), ctx_simp_p), using_params(mk_simplify_tactic(m), pull_ite_p), mk_elim_uncnstr_tactic(m), - mk_lia2card_tactic(m), + mk_lia2card_tactic(m), + mk_card2bv_tactic(m, p_ref), skip_if_failed(using_params(mk_cofactor_term_ite_tactic(m), elim_p))); } @@ -105,7 +107,9 @@ static tactic * mk_qfnia_nlsat_solver(ast_manager & m, params_ref const & p) { static tactic * mk_qfnia_smt_solver(ast_manager& m, params_ref const& p) { params_ref simp_p = p; simp_p.set_bool("som", true); // expand into sums of monomials - return and_then(using_params(mk_simplify_tactic(m), simp_p), mk_smt_tactic(m)); + return and_then( + using_params(mk_simplify_tactic(m), simp_p), + mk_smt_tactic(m)); } tactic * mk_qfnia_tactic(ast_manager & m, params_ref const & p) { @@ -113,9 +117,11 @@ tactic * mk_qfnia_tactic(ast_manager & m, params_ref const & p) { return and_then( mk_report_verbose_tactic("(qfnia-tactic)", 10), mk_qfnia_premable(m, p), - or_else(mk_qfnia_sat_solver(m, p), - try_for(mk_qfnia_smt_solver(m, p), 2000), - mk_qfnia_nlsat_solver(m, p), - mk_qfnia_smt_solver(m, p)) + mk_qfnia_sat_solver(m, p) + +// or_else(mk_qfnia_sat_solver(m, p), +// try_for(mk_qfnia_smt_solver(m, p), 2000), +// mk_qfnia_nlsat_solver(m, p), +// mk_qfnia_smt_solver(m, p)) ); } From cc216f8cc3c05dcf267a913395be30f893e14f48 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 19 Feb 2019 21:24:44 +0100 Subject: [PATCH 19/41] fix regressions breaking build Signed-off-by: Nikolaj Bjorner --- src/tactic/arith/nla2bv_tactic.cpp | 3 +-- src/tactic/smtlogics/qfnia_tactic.cpp | 9 ++++----- 2 files changed, 5 insertions(+), 7 deletions(-) diff --git a/src/tactic/arith/nla2bv_tactic.cpp b/src/tactic/arith/nla2bv_tactic.cpp index 0a58740d1..c09fc695d 100644 --- a/src/tactic/arith/nla2bv_tactic.cpp +++ b/src/tactic/arith/nla2bv_tactic.cpp @@ -327,7 +327,6 @@ class nla2bv_tactic : public tactic { } void operator()(app* n) { if (a.is_int(n) && is_uninterp_const(n)) { - TRACE("nla2bv", tout << "Not supported: " << mk_ismt2_pp(n, m) << "\n";); m_vars.push_back(n); } else if (a.is_real(n) && is_uninterp_const(n)) { @@ -371,7 +370,7 @@ class nla2bv_tactic : public tactic { add_var(fe_var.vars()[i]); } if (!fe_var.is_supported()) return not_supported; - if (!fe_var.vars().empty()) return is_bool; + if (fe_var.vars().empty()) return is_bool; return has_num; } diff --git a/src/tactic/smtlogics/qfnia_tactic.cpp b/src/tactic/smtlogics/qfnia_tactic.cpp index 528a6c048..a9a6032f1 100644 --- a/src/tactic/smtlogics/qfnia_tactic.cpp +++ b/src/tactic/smtlogics/qfnia_tactic.cpp @@ -117,11 +117,10 @@ tactic * mk_qfnia_tactic(ast_manager & m, params_ref const & p) { return and_then( mk_report_verbose_tactic("(qfnia-tactic)", 10), mk_qfnia_premable(m, p), - mk_qfnia_sat_solver(m, p) -// or_else(mk_qfnia_sat_solver(m, p), -// try_for(mk_qfnia_smt_solver(m, p), 2000), -// mk_qfnia_nlsat_solver(m, p), -// mk_qfnia_smt_solver(m, p)) + or_else(mk_qfnia_sat_solver(m, p), + try_for(mk_qfnia_smt_solver(m, p), 2000), + mk_qfnia_nlsat_solver(m, p), + mk_qfnia_smt_solver(m, p)) ); } From 3548057bd11be58ebc35f65364cae30ef187de13 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 20 Feb 2019 14:00:05 +0100 Subject: [PATCH 20/41] fix detection of arithmetic operations Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver.cpp | 1 + src/sat/sat_solver.h | 3 ++- src/sat/sat_solver_core.h | 2 ++ src/sat/tactic/sat_tactic.cpp | 5 +++++ src/tactic/arith/nla2bv_tactic.cpp | 32 +++++++++++++++++------------- 5 files changed, 28 insertions(+), 15 deletions(-) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 2df184c88..3deb6fc17 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -1157,6 +1157,7 @@ namespace sat { } catch (const abort_solver &) { m_reason_unknown = "sat.giveup"; + IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort giveup\")\n";); return l_undef; } } diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 53c3062a8..c000ccb79 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -328,6 +328,7 @@ namespace sat { if (!m_rlimit.inc()) { m_mc.reset(); m_model_is_current = false; + TRACE("sat", tout << "canceled\n";); throw solver_exception(Z3_CANCELED_MSG); } ++m_num_checkpoints; @@ -384,7 +385,7 @@ namespace sat { model_converter const & get_model_converter() const { return m_mc; } void flush(model_converter& mc) override { mc.flush(m_mc); } void set_model(model const& mdl); - char const* get_reason_unknown() const { return m_reason_unknown.c_str(); } + char const* get_reason_unknown() const override { return m_reason_unknown.c_str(); } bool check_clauses(model const& m) const; bool is_assumption(bool_var v) const; void set_activity(bool_var v, unsigned act); diff --git a/src/sat/sat_solver_core.h b/src/sat/sat_solver_core.h index 543a84fa7..b3c43ea6a 100644 --- a/src/sat/sat_solver_core.h +++ b/src/sat/sat_solver_core.h @@ -50,6 +50,8 @@ namespace sat { // check satisfiability virtual lbool check(unsigned num_lits = 0, literal const* lits = nullptr) = 0; + virtual char const* get_reason_unknown() const { return "reason unavailable"; } + // add clauses virtual void add_clause(unsigned n, literal* lits, bool is_redundant) = 0; void add_clause(literal l1, literal l2, bool is_redundant) { diff --git a/src/sat/tactic/sat_tactic.cpp b/src/sat/tactic/sat_tactic.cpp index 1f6fe11ad..2739932e6 100644 --- a/src/sat/tactic/sat_tactic.cpp +++ b/src/sat/tactic/sat_tactic.cpp @@ -65,6 +65,7 @@ class sat_tactic : public tactic { TRACE("sat_dimacs", m_solver->display_dimacs(tout);); dep2assumptions(dep2asm, assumptions); lbool r = m_solver->check(assumptions.size(), assumptions.c_ptr()); + TRACE("sat", tout << "result of checking: " << r << " " << m_solver->get_reason_unknown() << "\n";); if (r == l_false) { expr_dependency * lcore = nullptr; if (produce_core) { @@ -198,6 +199,10 @@ public: proc.m_solver->collect_statistics(m_stats); throw tactic_exception(ex.msg()); } + catch (z3_exception& ex) { + TRACE("sat", tout << ex.msg() << "\n";); + throw; + } TRACE("sat_stats", m_stats.display_smt2(tout);); } diff --git a/src/tactic/arith/nla2bv_tactic.cpp b/src/tactic/arith/nla2bv_tactic.cpp index c09fc695d..6662aec33 100644 --- a/src/tactic/arith/nla2bv_tactic.cpp +++ b/src/tactic/arith/nla2bv_tactic.cpp @@ -318,10 +318,12 @@ class nla2bv_tactic : public tactic { ast_manager& m; pb_util pb; ptr_vector m_vars; + bool m_no_arith; bool m_in_supported_fragment; public: - get_uninterp_proc(imp& s): m_imp(s), a(s.m_arith), m(a.get_manager()), pb(m), m_in_supported_fragment(true) {} + get_uninterp_proc(imp& s): m_imp(s), a(s.m_arith), m(a.get_manager()), pb(m), m_no_arith(true), m_in_supported_fragment(true) {} ptr_vector const& vars() { return m_vars; } + bool no_arith() const { return m_no_arith; } void operator()(var * n) { m_in_supported_fragment = false; } @@ -338,18 +340,20 @@ class nla2bv_tactic : public tactic { else if (m.is_bool(n) && n->get_decl()->get_family_id() == pb.get_family_id()) { } - else if (!(a.is_mul(n) || - a.is_add(n) || - a.is_sub(n) || - a.is_le(n) || - a.is_lt(n) || - a.is_ge(n) || - a.is_gt(n) || - a.is_numeral(n) || - a.is_uminus(n) || - m_imp.m_bv2real.is_pos_le(n) || - m_imp.m_bv2real.is_pos_lt(n) || - n->get_family_id() == a.get_manager().get_basic_family_id())) { + else if (a.is_mul(n) || + a.is_add(n) || + a.is_sub(n) || + a.is_le(n) || + a.is_lt(n) || + a.is_ge(n) || + a.is_gt(n) || + a.is_numeral(n) || + a.is_uminus(n) || + m_imp.m_bv2real.is_pos_le(n) || + m_imp.m_bv2real.is_pos_lt(n)) { + m_no_arith = false; + } + else if (n->get_family_id() != m.get_basic_family_id()) { TRACE("nla2bv", tout << "Not supported: " << mk_ismt2_pp(n, m) << "\n";); m_in_supported_fragment = false; } @@ -370,7 +374,7 @@ class nla2bv_tactic : public tactic { add_var(fe_var.vars()[i]); } if (!fe_var.is_supported()) return not_supported; - if (fe_var.vars().empty()) return is_bool; + if (fe_var.vars().empty() && fe_var.no_arith()) return is_bool; return has_num; } From 598fc810b57462552f69f69110fbc0930d772d8d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 20 Feb 2019 15:34:47 +0100 Subject: [PATCH 21/41] adding FP Signed-off-by: Nikolaj Bjorner --- src/solver/smt_logics.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/solver/smt_logics.cpp b/src/solver/smt_logics.cpp index d0fd8f809..a8dcf2f90 100644 --- a/src/solver/smt_logics.cpp +++ b/src/solver/smt_logics.cpp @@ -80,6 +80,7 @@ bool smt_logics::logic_has_arith(symbol const & s) { s == "LRA" || s == "UFIDL" || s == "QF_FP" || + s == "FP" || s == "QF_FPBV" || s == "QF_BVFP" || s == "QF_S" || @@ -101,6 +102,7 @@ bool smt_logics::logic_has_bv(symbol const & s) { s == "QF_AUFBV" || s == "QF_BVRE" || s == "QF_FPBV" || + s == "FP" || s == "QF_BVFP" || logic_is_allcsp(s) || s == "QF_FD" || @@ -138,7 +140,7 @@ bool smt_logics::logic_has_str(symbol const & s) { } bool smt_logics::logic_has_fpa(symbol const & s) { - return s == "QF_FP" || s == "QF_FPBV" || s == "QF_BVFP" || s == "QF_FPLRA" || logic_is_allcsp(s); + return s == "FP" || s == "QF_FP" || s == "QF_FPBV" || s == "QF_BVFP" || s == "QF_FPLRA" || logic_is_allcsp(s); } bool smt_logics::logic_has_uf(symbol const & s) { From f3cd7d646d021a02d6d1dbc6a419ec22668b5158 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Thu, 21 Feb 2019 10:42:42 +0000 Subject: [PATCH 22/41] further simplifications to scoped_timer --- src/util/scoped_timer.cpp | 33 +++++++++++++-------------------- 1 file changed, 13 insertions(+), 20 deletions(-) diff --git a/src/util/scoped_timer.cpp b/src/util/scoped_timer.cpp index e3b96fa15..58416289a 100644 --- a/src/util/scoped_timer.cpp +++ b/src/util/scoped_timer.cpp @@ -26,39 +26,33 @@ Revision History: struct scoped_timer::imp { - event_handler * m_eh; +private: std::thread m_thread; std::timed_mutex m_mutex; - unsigned m_ms; - static void* thread_func(imp * st) { - auto end = std::chrono::steady_clock::now() + std::chrono::milliseconds(st->m_ms); + static void thread_func(unsigned ms, event_handler * eh, std::timed_mutex * mutex) { + auto end = std::chrono::steady_clock::now() + std::chrono::milliseconds(ms); - while (!st->m_mutex.try_lock_until(end)) { - if (std::chrono::steady_clock::now() > end) { - st->m_eh->operator()(TIMEOUT_EH_CALLER); - return nullptr; - } + while (!mutex->try_lock_until(end)) { + if (std::chrono::steady_clock::now() >= end) { + eh->operator()(TIMEOUT_EH_CALLER); + return; + } } - st->m_mutex.unlock(); - return nullptr; + mutex->unlock(); } - imp(unsigned ms, event_handler * eh): - m_eh(eh), m_ms(ms) { +public: + imp(unsigned ms, event_handler * eh) { m_mutex.lock(); - m_thread = std::thread(thread_func, this); + m_thread = std::thread(thread_func, ms, eh, &m_mutex); } ~imp() { m_mutex.unlock(); - while (!m_thread.joinable()) { - std::this_thread::yield(); - } m_thread.join(); } - }; scoped_timer::scoped_timer(unsigned ms, event_handler * eh) { @@ -69,6 +63,5 @@ scoped_timer::scoped_timer(unsigned ms, event_handler * eh) { } scoped_timer::~scoped_timer() { - if (m_imp) - dealloc(m_imp); + dealloc(m_imp); } From a76c0fbbfbb7e0e80c5d491da99fb6b56f408139 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Thu, 21 Feb 2019 11:49:41 +0000 Subject: [PATCH 23/41] simplify timeout mechanism and fix race conditions there --- src/shell/main.cpp | 7 +++++-- src/util/timeout.cpp | 26 ++++++++++---------------- 2 files changed, 15 insertions(+), 18 deletions(-) diff --git a/src/shell/main.cpp b/src/shell/main.cpp index b036628b1..260cf8a79 100644 --- a/src/shell/main.cpp +++ b/src/shell/main.cpp @@ -115,6 +115,7 @@ void display_usage() { } void parse_cmd_line_args(int argc, char ** argv) { + long timeout = 0; int i = 1; char * eq_pos = nullptr; while (i < argc) { @@ -216,8 +217,7 @@ void parse_cmd_line_args(int argc, char ** argv) { else if (strcmp(opt_name, "T") == 0) { if (!opt_arg) error("option argument (-T:timeout) is missing."); - long tm = strtol(opt_arg, nullptr, 10); - set_timeout(tm * 1000); + timeout = strtol(opt_arg, nullptr, 10); } else if (strcmp(opt_name, "t") == 0) { if (!opt_arg) @@ -292,6 +292,9 @@ void parse_cmd_line_args(int argc, char ** argv) { } i++; } + + if (timeout) + set_timeout(timeout * 1000); } diff --git a/src/util/timeout.cpp b/src/util/timeout.cpp index ad02a747d..1a92ae867 100644 --- a/src/util/timeout.cpp +++ b/src/util/timeout.cpp @@ -19,7 +19,6 @@ Revision History: --*/ #include -#include "util/z3_omp.h" #include "util/util.h" #include "util/timeout.h" #include "util/error_codes.h" @@ -34,26 +33,21 @@ namespace { class g_timeout_eh : public event_handler { public: void operator()(event_handler_caller_t caller_id) override { - #pragma omp critical (g_timeout_cs) - { - std::cout << "timeout\n"; - m_caller_id = caller_id; - if (g_on_timeout) - g_on_timeout(); - if (g_timeout) - delete g_timeout; - g_timeout = nullptr; - throw z3_error(ERR_TIMEOUT); - } + std::cout << "timeout\n"; + m_caller_id = caller_id; + if (g_on_timeout) + g_on_timeout(); + throw z3_error(ERR_TIMEOUT); } }; } -void set_timeout(long ms) { - if (g_timeout) - delete g_timeout; +static g_timeout_eh eh; - g_timeout = new scoped_timer(ms, new g_timeout_eh()); +void set_timeout(long ms) { + SASSERT(!g_timeout); + // this is leaked, but since it's only used in the shell, it's ok + g_timeout = new scoped_timer(ms, &eh); } void register_on_timeout_proc(void (*proc)()) { From 2ff2e77739c0948ffc083ee7f88b6b1f8f1eac86 Mon Sep 17 00:00:00 2001 From: Daniel Schemmel Date: Mon, 21 May 2018 03:19:19 +0200 Subject: [PATCH 24/41] Move buffer.h to old_buffer.h and add a shim buffer.h --- src/util/buffer.h | 265 ++--------------------------------------- src/util/old_buffer.h | 268 ++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 275 insertions(+), 258 deletions(-) create mode 100644 src/util/old_buffer.h diff --git a/src/util/buffer.h b/src/util/buffer.h index c64e23d8b..7a89ffef3 100644 --- a/src/util/buffer.h +++ b/src/util/buffer.h @@ -1,268 +1,17 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - buffer.h - -Abstract: - - - -Author: - - Leonardo de Moura (leonardo) 2006-10-16. - -Revision History: - ---*/ #ifndef BUFFER_H_ #define BUFFER_H_ -#include -#include "util/memory_manager.h" +#include "old_buffer.h" template -class buffer { -protected: - T * m_buffer; - unsigned m_pos; - unsigned m_capacity; - char m_initial_buffer[INITIAL_SIZE * sizeof(T)]; - - void free_memory() { - if (m_buffer != reinterpret_cast(m_initial_buffer)) { - dealloc_svect(m_buffer); - } - } +using buffer = old_buffer; - void expand() { - unsigned new_capacity = m_capacity << 1; - T * new_buffer = reinterpret_cast(memory::allocate(sizeof(T) * new_capacity)); - memcpy(new_buffer, m_buffer, m_pos * sizeof(T)); - free_memory(); - m_buffer = new_buffer; - m_capacity = new_capacity; - } - - void destroy_elements() { - iterator it = begin(); - iterator e = end(); - for (; it != e; ++it) { - it->~T(); - } - } - - void destroy() { - if (CallDestructors) { - destroy_elements(); - } - free_memory(); - } - -public: - typedef T data; - typedef T * iterator; - typedef const T * const_iterator; - - buffer(): - m_buffer(reinterpret_cast(m_initial_buffer)), - m_pos(0), - m_capacity(INITIAL_SIZE) { - } - - buffer(const buffer & source): - m_buffer(reinterpret_cast(m_initial_buffer)), - m_pos(0), - m_capacity(INITIAL_SIZE) { - unsigned sz = source.size(); - for(unsigned i = 0; i < sz; i++) { - push_back(source.m_buffer[i]); - } - } - - buffer(unsigned sz, const T & elem): - m_buffer(reinterpret_cast(m_initial_buffer)), - m_pos(0), - m_capacity(INITIAL_SIZE) { - for (unsigned i = 0; i < sz; i++) { - push_back(elem); - } - SASSERT(size() == sz); - } - - ~buffer() { - destroy(); - } - - void reset() { - if (CallDestructors) { - destroy_elements(); - } - m_pos = 0; - } - - void finalize() { - destroy(); - m_buffer = reinterpret_cast(m_initial_buffer); - m_pos = 0; - m_capacity = INITIAL_SIZE; - } - - unsigned size() const { - return m_pos; - } - - bool empty() const { - return m_pos == 0; - } - - iterator begin() { - return m_buffer; - } - - iterator end() { - return m_buffer + size(); - } - - void set_end(iterator it) { - m_pos = static_cast(it - m_buffer); - if (CallDestructors) { - iterator e = end(); - for (; it != e; ++it) { - it->~T(); - } - } - } - - const_iterator begin() const { - return m_buffer; - } - - const_iterator end() const { - return m_buffer + size(); - } - - void push_back(const T & elem) { - if (m_pos >= m_capacity) - expand(); - new (m_buffer + m_pos) T(elem); - m_pos++; - } - - void push_back(T && elem) { - if (m_pos >= m_capacity) - expand(); - new (m_buffer + m_pos) T(std::move(elem)); - m_pos++; - } - - void pop_back() { - if (CallDestructors) { - back().~T(); - } - m_pos--; - } - - const T & back() const { - SASSERT(!empty()); - SASSERT(m_pos > 0); - return m_buffer[m_pos - 1]; - } - - T & back() { - SASSERT(!empty()); - SASSERT(m_pos > 0); - return m_buffer[m_pos - 1]; - } - - T * c_ptr() const { - return m_buffer; - } - - void append(unsigned n, T const * elems) { - for (unsigned i = 0; i < n; i++) { - push_back(elems[i]); - } - } - - void append(const buffer& source) { - append(source.size(), source.c_ptr()); - } - - T & operator[](unsigned idx) { - SASSERT(idx < size()); - return m_buffer[idx]; - } - - const T & operator[](unsigned idx) const { - SASSERT(idx < size()); - return m_buffer[idx]; - } - - T & get(unsigned idx) { - SASSERT(idx < size()); - return m_buffer[idx]; - } - - const T & get(unsigned idx) const { - SASSERT(idx < size()); - return m_buffer[idx]; - } - - void set(unsigned idx, T const & val) { - SASSERT(idx < size()); - m_buffer[idx] = val; - } - - void resize(unsigned nsz, const T & elem=T()) { - unsigned sz = size(); - if (nsz > sz) { - for (unsigned i = sz; i < nsz; i++) { - push_back(elem); - } - } - else if (nsz < sz) { - for (unsigned i = nsz; i < sz; i++) { - pop_back(); - } - } - SASSERT(size() == nsz); - } - - void shrink(unsigned nsz) { - unsigned sz = size(); - SASSERT(nsz <= sz); - for (unsigned i = nsz; i < sz; i++) - pop_back(); - SASSERT(size() == nsz); - } - - buffer & operator=(buffer const & other) { - if (this == &other) - return *this; - reset(); - append(other); - return *this; - } -}; +// note that the append added in the old_ptr_buffer is actually not an addition over its base class old_buffer, +// which already has an append function with the same signature and implementation +template +using ptr_buffer = old_ptr_buffer; template -class ptr_buffer : public buffer { -public: - void append(unsigned n, T * const * elems) { - for (unsigned i = 0; i < n; i++) { - this->push_back(elems[i]); - } - } -}; - -template -class sbuffer : public buffer { -public: - sbuffer(): buffer() {} - sbuffer(unsigned sz, const T& elem) : buffer(sz,elem) {} -}; +using sbuffer = old_sbuffer; #endif /* BUFFER_H_ */ - diff --git a/src/util/old_buffer.h b/src/util/old_buffer.h new file mode 100644 index 000000000..5ed1df583 --- /dev/null +++ b/src/util/old_buffer.h @@ -0,0 +1,268 @@ +/*++ +Copyright (c) 2006 Microsoft Corporation + +Module Name: + + old_buffer.h + +Abstract: + + + +Author: + + Leonardo de Moura (leonardo) 2006-10-16. + +Revision History: + +--*/ +#ifndef OLD_BUFFER_H_ +#define OLD_BUFFER_H_ + +#include +#include "util/memory_manager.h" + +template +class old_buffer { +protected: + T * m_buffer; + unsigned m_pos; + unsigned m_capacity; + char m_initial_buffer[INITIAL_SIZE * sizeof(T)]; + + void free_memory() { + if (m_buffer != reinterpret_cast(m_initial_buffer)) { + dealloc_svect(m_buffer); + } + } + + void expand() { + unsigned new_capacity = m_capacity << 1; + T * new_buffer = reinterpret_cast(memory::allocate(sizeof(T) * new_capacity)); + memcpy(new_buffer, m_buffer, m_pos * sizeof(T)); + free_memory(); + m_buffer = new_buffer; + m_capacity = new_capacity; + } + + void destroy_elements() { + iterator it = begin(); + iterator e = end(); + for (; it != e; ++it) { + it->~T(); + } + } + + void destroy() { + if (CallDestructors) { + destroy_elements(); + } + free_memory(); + } + +public: + typedef T data; + typedef T * iterator; + typedef const T * const_iterator; + + old_buffer(): + m_buffer(reinterpret_cast(m_initial_buffer)), + m_pos(0), + m_capacity(INITIAL_SIZE) { + } + + old_buffer(const old_buffer & source): + m_buffer(reinterpret_cast(m_initial_buffer)), + m_pos(0), + m_capacity(INITIAL_SIZE) { + unsigned sz = source.size(); + for(unsigned i = 0; i < sz; i++) { + push_back(source.m_buffer[i]); + } + } + + old_buffer(unsigned sz, const T & elem): + m_buffer(reinterpret_cast(m_initial_buffer)), + m_pos(0), + m_capacity(INITIAL_SIZE) { + for (unsigned i = 0; i < sz; i++) { + push_back(elem); + } + SASSERT(size() == sz); + } + + ~old_buffer() { + destroy(); + } + + void reset() { + if (CallDestructors) { + destroy_elements(); + } + m_pos = 0; + } + + void finalize() { + destroy(); + m_buffer = reinterpret_cast(m_initial_buffer); + m_pos = 0; + m_capacity = INITIAL_SIZE; + } + + unsigned size() const { + return m_pos; + } + + bool empty() const { + return m_pos == 0; + } + + iterator begin() { + return m_buffer; + } + + iterator end() { + return m_buffer + size(); + } + + void set_end(iterator it) { + m_pos = static_cast(it - m_buffer); + if (CallDestructors) { + iterator e = end(); + for (; it != e; ++it) { + it->~T(); + } + } + } + + const_iterator begin() const { + return m_buffer; + } + + const_iterator end() const { + return m_buffer + size(); + } + + void push_back(const T & elem) { + if (m_pos >= m_capacity) + expand(); + new (m_buffer + m_pos) T(elem); + m_pos++; + } + + void push_back(T && elem) { + if (m_pos >= m_capacity) + expand(); + new (m_buffer + m_pos) T(std::move(elem)); + m_pos++; + } + + void pop_back() { + if (CallDestructors) { + back().~T(); + } + m_pos--; + } + + const T & back() const { + SASSERT(!empty()); + SASSERT(m_pos > 0); + return m_buffer[m_pos - 1]; + } + + T & back() { + SASSERT(!empty()); + SASSERT(m_pos > 0); + return m_buffer[m_pos - 1]; + } + + T * c_ptr() const { + return m_buffer; + } + + void append(unsigned n, T const * elems) { + for (unsigned i = 0; i < n; i++) { + push_back(elems[i]); + } + } + + void append(const old_buffer& source) { + append(source.size(), source.c_ptr()); + } + + T & operator[](unsigned idx) { + SASSERT(idx < size()); + return m_buffer[idx]; + } + + const T & operator[](unsigned idx) const { + SASSERT(idx < size()); + return m_buffer[idx]; + } + + T & get(unsigned idx) { + SASSERT(idx < size()); + return m_buffer[idx]; + } + + const T & get(unsigned idx) const { + SASSERT(idx < size()); + return m_buffer[idx]; + } + + void set(unsigned idx, T const & val) { + SASSERT(idx < size()); + m_buffer[idx] = val; + } + + void resize(unsigned nsz, const T & elem=T()) { + unsigned sz = size(); + if (nsz > sz) { + for (unsigned i = sz; i < nsz; i++) { + push_back(elem); + } + } + else if (nsz < sz) { + for (unsigned i = nsz; i < sz; i++) { + pop_back(); + } + } + SASSERT(size() == nsz); + } + + void shrink(unsigned nsz) { + unsigned sz = size(); + SASSERT(nsz <= sz); + for (unsigned i = nsz; i < sz; i++) + pop_back(); + SASSERT(size() == nsz); + } + + old_buffer & operator=(old_buffer const & other) { + if (this == &other) + return *this; + reset(); + append(other); + return *this; + } +}; + +template +class old_ptr_buffer : public old_buffer { +public: + void append(unsigned n, T * const * elems) { + for (unsigned i = 0; i < n; i++) { + this->push_back(elems[i]); + } + } +}; + +template +class old_sbuffer : public old_buffer { +public: + old_sbuffer(): old_buffer() {} + old_sbuffer(unsigned sz, const T& elem) : old_buffer(sz,elem) {} +}; + +#endif /* OLD_BUFFER_H_ */ + From 3a5263be9544a9801da9cf6b8397e5bf7819e77c Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Thu, 21 Feb 2019 13:30:27 +0000 Subject: [PATCH 25/41] modernize stopwatch --- src/util/stopwatch.h | 182 ++++++++----------------------------------- 1 file changed, 33 insertions(+), 149 deletions(-) diff --git a/src/util/stopwatch.h b/src/util/stopwatch.h index a11a87484..44d7a104b 100644 --- a/src/util/stopwatch.h +++ b/src/util/stopwatch.h @@ -20,171 +20,55 @@ Revision History: #ifndef STOPWATCH_H_ #define STOPWATCH_H_ -#if defined(_WINDOWS) || defined(_CYGWIN) || defined(_MINGW) - -// Does this redefinition work? - -#include +#include "util/debug.h" +#include class stopwatch { -private: - LARGE_INTEGER m_elapsed; - LARGE_INTEGER m_last_start_time; - LARGE_INTEGER m_last_stop_time; - LARGE_INTEGER m_frequency; + std::chrono::time_point m_start; + std::chrono::steady_clock::duration m_elapsed; +#if Z3DEBUG + bool m_running = false; +#endif + + static std::chrono::time_point get() { + return std::chrono::steady_clock::now(); + } public: stopwatch() { - QueryPerformanceFrequency(&m_frequency); - reset(); + reset(); } - ~stopwatch() {}; - - void add (const stopwatch &s) {/* TODO */} - - void reset() { m_elapsed.QuadPart = 0; } - - void start() { - QueryPerformanceCounter(&m_last_start_time); - } - - void stop() { - QueryPerformanceCounter(&m_last_stop_time); - m_elapsed.QuadPart += m_last_stop_time.QuadPart - m_last_start_time.QuadPart; + void add(const stopwatch &s) { + m_elapsed += s.m_elapsed; } - double get_seconds() const { - return static_cast(m_elapsed.QuadPart / static_cast(m_frequency.QuadPart)) ; + void reset() { + m_elapsed = std::chrono::steady_clock::duration::zero(); + } + + void start() { + SASSERT(!m_running); + DEBUG_CODE(m_running = true); + m_start = get(); + } + + void stop() { + SASSERT(m_running); + DEBUG_CODE(m_running = false); + m_elapsed += get() - m_start; + } + + double get_seconds() const { + return std::chrono::duration_cast(m_elapsed).count() / 1000.0; } double get_current_seconds() const { - LARGE_INTEGER t; - QueryPerformanceCounter(&t); - return static_cast( (t.QuadPart - m_last_start_time.QuadPart) / static_cast(m_frequency.QuadPart)); + return std::chrono::duration_cast(get() - m_start).count() / 1000.0; } }; -#undef max -#undef min - - -#elif defined(__APPLE__) && defined (__MACH__) // macOS - -#include -#include - -class stopwatch { - unsigned long long m_time; // elapsed time in ns - bool m_running; - clock_serv_t m_host_clock; - mach_timespec_t m_start; - -public: - stopwatch():m_time(0), m_running(false) { - host_get_clock_service(mach_host_self(), SYSTEM_CLOCK, &m_host_clock); - } - - ~stopwatch() {} - - void add (const stopwatch &s) {m_time += s.m_time;} - - void reset() { - m_time = 0ull; - } - - void start() { - if (!m_running) { - clock_get_time(m_host_clock, &m_start); - m_running = true; - } - } - - void stop() { - if (m_running) { - mach_timespec_t _stop; - clock_get_time(m_host_clock, &_stop); - m_time += (_stop.tv_sec - m_start.tv_sec) * 1000000000ull; - m_time += (_stop.tv_nsec - m_start.tv_nsec); - m_running = false; - } - } - - double get_seconds() const { - if (m_running) { - const_cast(this)->stop(); - /* update m_time */ - const_cast(this)->start(); - } - return static_cast(m_time)/static_cast(1000000000ull); - } - - double get_current_seconds() const { - return get_seconds(); - } -}; - - -#else // Linux - -#include - -#ifndef CLOCK_PROCESS_CPUTIME_ID -/* BSD */ -# define CLOCK_PROCESS_CPUTIME_ID CLOCK_MONOTONIC -#endif - -class stopwatch { - unsigned long long m_time; // elapsed time in ns - bool m_running; - struct timespec m_start; - -public: - stopwatch():m_time(0), m_running(false) { - } - - ~stopwatch() {} - - void add (const stopwatch &s) {m_time += s.m_time;} - - void reset() { - m_time = 0ull; - } - - void start() { - if (!m_running) { - clock_gettime(CLOCK_PROCESS_CPUTIME_ID, &m_start); - m_running = true; - } - } - - void stop() { - if (m_running) { - struct timespec _stop; - clock_gettime(CLOCK_PROCESS_CPUTIME_ID, &_stop); - m_time += (_stop.tv_sec - m_start.tv_sec) * 1000000000ull; - if (m_time != 0 || _stop.tv_nsec >= m_start.tv_nsec) - m_time += (_stop.tv_nsec - m_start.tv_nsec); - m_running = false; - } - } - - double get_seconds() const { - if (m_running) { - const_cast(this)->stop(); - /* update m_time */ - const_cast(this)->start(); - } - return static_cast(m_time)/static_cast(1000000000ull); - } - - double get_current_seconds() const { - return get_seconds(); - } -}; - -#endif struct scoped_watch { stopwatch &m_sw; From 3a7c467822f6792a57fb9b97a707efec1683bbfa Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Thu, 21 Feb 2019 13:33:52 +0000 Subject: [PATCH 26/41] fix debug build.. --- src/util/stopwatch.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/util/stopwatch.h b/src/util/stopwatch.h index 44d7a104b..e35380153 100644 --- a/src/util/stopwatch.h +++ b/src/util/stopwatch.h @@ -50,13 +50,13 @@ public: void start() { SASSERT(!m_running); - DEBUG_CODE(m_running = true); + DEBUG_CODE(m_running = true;); m_start = get(); } void stop() { SASSERT(m_running); - DEBUG_CODE(m_running = false); + DEBUG_CODE(m_running = false;); m_elapsed += get() - m_start; } From 85162d90d1c68838f150704c672e82a457922e54 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Thu, 21 Feb 2019 13:57:38 +0000 Subject: [PATCH 27/41] simplify timer.h --- src/util/timer.cpp | 40 ---------------------------------------- src/util/timer.h | 28 ++++++++++++++++++---------- 2 files changed, 18 insertions(+), 50 deletions(-) delete mode 100644 src/util/timer.cpp diff --git a/src/util/timer.cpp b/src/util/timer.cpp deleted file mode 100644 index 2d80b732c..000000000 --- a/src/util/timer.cpp +++ /dev/null @@ -1,40 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - timer.cpp - -Abstract: - - - -Author: - - Leonardo de Moura (leonardo) 2009-01-06. - -Revision History: - ---*/ -#include "util/util.h" -#include "util/memory_manager.h" -#include "util/stopwatch.h" -#include "util/timer.h" - -timer::timer(){ - m_watch = alloc(stopwatch); - start(); -} - -timer::~timer() { - dealloc(m_watch); -} - -void timer::start() { - m_watch->start(); -} - -double timer::get_seconds() { - return m_watch->get_current_seconds(); -} - diff --git a/src/util/timer.h b/src/util/timer.h index b4a69f8bf..37566e613 100644 --- a/src/util/timer.h +++ b/src/util/timer.h @@ -19,21 +19,29 @@ Revision History: #ifndef TIMER_H_ #define TIMER_H_ -class stopwatch; +#include "util/stopwatch.h" /** - \brief Wrapper for the stopwatch class. It hides windows.h dependency. + \brief Wrapper for the stopwatch class. */ class timer { - stopwatch * m_watch; + stopwatch m_watch; public: - timer(); - ~timer(); - void start(); - double get_seconds(); - bool timeout(unsigned secs) { return secs > 0 && secs != UINT_MAX && get_seconds() > secs; } - bool ms_timeout(unsigned ms) { return ms > 0 && ms != UINT_MAX && get_seconds() * 1000 > ms; } + void start() { + m_watch.start(); + } + + double get_seconds() const { + return m_watch.get_current_seconds(); + } + + bool timeout(unsigned secs) const { + return secs != 0 && secs != UINT_MAX && get_seconds() > secs; + } + + bool ms_timeout(unsigned ms) const { + return ms != 0 && ms != UINT_MAX && get_seconds() * 1000 > ms; + } }; #endif /* TIMER_H_ */ - From 721ea2a8d3eec8819e3f3b2c4b55ed5212c67dcb Mon Sep 17 00:00:00 2001 From: Daniel Schemmel Date: Sat, 26 May 2018 05:22:39 +0200 Subject: [PATCH 28/41] Move vector.h to old_vector.h and add a shim vector.h To do so, one instance of the class keyword needs to be removed. --- src/util/lp/dense_matrix.cpp | 2 +- src/util/old_vector.h | 609 ++++++++++++++++++++++++++++++++++ src/util/vector.h | 617 +---------------------------------- 3 files changed, 622 insertions(+), 606 deletions(-) create mode 100644 src/util/old_vector.h diff --git a/src/util/lp/dense_matrix.cpp b/src/util/lp/dense_matrix.cpp index 50f2598c8..4ababc47a 100644 --- a/src/util/lp/dense_matrix.cpp +++ b/src/util/lp/dense_matrix.cpp @@ -35,6 +35,6 @@ template lp::dense_matrix >::dense_matrix(uns template lp::dense_matrix >& lp::dense_matrix >::operator=(lp::dense_matrix > const&); template lp::dense_matrix > lp::operator* >(lp::matrix >&, lp::matrix >&); template void lp::dense_matrix >::apply_from_right( vector< lp::mpq> &); -template void lp::dense_matrix::apply_from_right(class vector &); +template void lp::dense_matrix::apply_from_right(vector &); template void lp::dense_matrix::apply_from_left(vector&); #endif diff --git a/src/util/old_vector.h b/src/util/old_vector.h new file mode 100644 index 000000000..53450e6cf --- /dev/null +++ b/src/util/old_vector.h @@ -0,0 +1,609 @@ +/*++ +Copyright (c) 2006 Microsoft Corporation + +Module Name: + + old_vector.h + +Abstract: + Dynamic array implementation. + Remarks: + + - Empty arrays consume only sizeof(T *) bytes. + + - There is the option of disabling the destructor invocation for elements stored in the vector. + This is useful for vectors of int. + +Author: + + Leonardo de Moura (leonardo) 2006-09-11. + +Revision History: + +--*/ +#ifndef OLD_VECTOR_H_ +#define OLD_VECTOR_H_ + +#include "util/debug.h" +#include +#include +#include +#include +#include "util/memory_manager.h" +#include "util/hash.h" +#include "util/z3_exception.h" + +// disable warning for constant 'if' expressions. +// these are used heavily in templates. +#ifdef _MSC_VER +#pragma warning(disable:4127) +#endif + +template +class old_vector { +#define SIZE_IDX -1 +#define CAPACITY_IDX -2 + T * m_data; + + void destroy_elements() { + iterator it = begin(); + iterator e = end(); + for (; it != e; ++it) { + it->~T(); + } + } + + void free_memory() { + memory::deallocate(reinterpret_cast(reinterpret_cast(m_data) - 2)); + } + + void expand_vector() { + if (m_data == nullptr) { + SZ capacity = 2; + SZ * mem = reinterpret_cast(memory::allocate(sizeof(T) * capacity + sizeof(SZ) * 2)); + *mem = capacity; + mem++; + *mem = 0; + mem++; + m_data = reinterpret_cast(mem); + } + else { + SASSERT(capacity() > 0); + SZ old_capacity = reinterpret_cast(m_data)[CAPACITY_IDX]; + SZ old_capacity_T = sizeof(T) * old_capacity + sizeof(SZ) * 2; + SZ new_capacity = (3 * old_capacity + 1) >> 1; + SZ new_capacity_T = sizeof(T) * new_capacity + sizeof(SZ) * 2; + if (new_capacity <= old_capacity || new_capacity_T <= old_capacity_T) { + throw default_exception("Overflow encountered when expanding old_vector"); + } + SZ *mem, *old_mem = reinterpret_cast(m_data) - 2; +#if defined(__GNUC__) && !defined(__clang__) && __GNUC__ < 5 + if (__has_trivial_copy(T)) { +#else + if (std::is_trivially_copyable::value) { +#endif + mem = (SZ*)memory::reallocate(old_mem, new_capacity_T); + m_data = reinterpret_cast(mem + 2); + } else { + mem = (SZ*)memory::allocate(new_capacity_T); + auto old_data = m_data; + auto old_size = size(); + mem[1] = old_size; + m_data = reinterpret_cast(mem + 2); + for (unsigned i = 0; i < old_size; ++i) { + new (&m_data[i]) T(std::move(old_data[i])); + old_data[i].~T(); + } + memory::deallocate(old_mem); + } + *mem = new_capacity; + } + } + + void copy_core(old_vector const & source) { + SZ size = source.size(); + SZ capacity = source.capacity(); + SZ * mem = reinterpret_cast(memory::allocate(sizeof(T) * capacity + sizeof(SZ) * 2)); + *mem = capacity; + mem++; + *mem = size; + mem++; + m_data = reinterpret_cast(mem); + const_iterator it = source.begin(); + iterator it2 = begin(); + SASSERT(it2 == m_data); + const_iterator e = source.end(); + for (; it != e; ++it, ++it2) { + new (it2) T(*it); + } + } + + void destroy() { + if (m_data) { + if (CallDestructors) { + destroy_elements(); + } + free_memory(); + } + } + +public: + typedef T data; + typedef T * iterator; + typedef const T * const_iterator; + + old_vector(): + m_data(nullptr) { + } + + old_vector(SZ s) { + if (s == 0) { + m_data = nullptr; + return; + } + SZ * mem = reinterpret_cast(memory::allocate(sizeof(T) * s + sizeof(SZ) * 2)); + *mem = s; + mem++; + *mem = s; + mem++; + m_data = reinterpret_cast(mem); + // initialize elements + iterator it = begin(); + iterator e = end(); + for (; it != e; ++it) { + new (it) T(); + } + } + + old_vector(SZ s, T const & elem): + m_data(nullptr) { + resize(s, elem); + } + + old_vector(old_vector const & source): + m_data(nullptr) { + if (source.m_data) { + copy_core(source); + } + SASSERT(size() == source.size()); + } + + old_vector(old_vector&& other) : m_data(nullptr) { + std::swap(m_data, other.m_data); + } + + old_vector(SZ s, T const * data): + m_data(nullptr) { + for (SZ i = 0; i < s; i++) { + push_back(data[i]); + } + } + + + ~old_vector() { + destroy(); + } + + void finalize() { + destroy(); + m_data = nullptr; + } + + bool operator==(old_vector const & other) const { + if (this == &other) { + return true; + } + if (size() != other.size()) + return false; + for (unsigned i = 0; i < size(); i++) { + if ((*this)[i] != other[i]) + return false; + } + return true; + } + + bool operator!=(old_vector const & other) const { + return !(*this == other); + } + + + old_vector & operator=(old_vector const & source) { + if (this == &source) { + return *this; + } + destroy(); + if (source.m_data) { + copy_core(source); + } + else { + m_data = nullptr; + } + return *this; + } + + old_vector & operator=(old_vector && source) { + if (this == &source) { + return *this; + } + destroy(); + m_data = nullptr; + std::swap(m_data, source.m_data); + return *this; + } + + bool containsp(std::function& predicate) const { + for (auto const& t : *this) + if (predicate(t)) + return true; + return false; + } + + /** + * retain elements that satisfy predicate. aka 'where'. + */ + old_vector filter_pure(std::function& predicate) const { + old_vector result; + for (auto& t : *this) + if (predicate(t)) + result.push_back(t); + return result; + } + + old_vector& filter_update(std::function& predicate) { + unsigned j = 0; + for (auto& t : *this) + if (predicate(t)) + set(j++, t); + shrink(j); + return *this; + } + + /** + * update elements using f, aka 'select' + */ + template + old_vector map_pure(std::function& f) const { + old_vector result; + for (auto& t : *this) + result.push_back(f(t)); + return result; + } + + old_vector& map_update(std::function& f) { + unsigned j = 0; + for (auto& t : *this) + set(j++, f(t)); + return *this; + } + + void reset() { + if (m_data) { + if (CallDestructors) { + destroy_elements(); + } + reinterpret_cast(m_data)[SIZE_IDX] = 0; + } + } + + void clear() { reset(); } + + bool empty() const { + return m_data == nullptr || reinterpret_cast(m_data)[SIZE_IDX] == 0; + } + + SZ size() const { + if (m_data == nullptr) { + return 0; + } + return reinterpret_cast(m_data)[SIZE_IDX]; + } + + SZ capacity() const { + if (m_data == nullptr) { + return 0; + } + return reinterpret_cast(m_data)[CAPACITY_IDX]; + } + + iterator begin() { + return m_data; + } + + iterator end() { + return m_data + size(); + } + + const_iterator begin() const { + return m_data; + } + + const_iterator end() const { + return m_data + size(); + } + + class reverse_iterator { + T* v; + public: + reverse_iterator(T* v):v(v) {} + + T operator*() { return *v; } + reverse_iterator operator++(int) { + reverse_iterator tmp = *this; + --v; + return tmp; + } + reverse_iterator& operator++() { + --v; + return *this; + } + + bool operator==(reverse_iterator const& other) const { + return other.v == v; + } + bool operator!=(reverse_iterator const& other) const { + return other.v != v; + } + }; + + reverse_iterator rbegin() { return reverse_iterator(end() - 1); } + reverse_iterator rend() { return reverse_iterator(begin() - 1); } + + void set_end(iterator it) { + if (m_data) { + SZ new_sz = static_cast(it - m_data); + if (CallDestructors) { + iterator e = end(); + for(; it != e; ++it) { + it->~T(); + } + } + reinterpret_cast(m_data)[SIZE_IDX] = new_sz; + } + else { + SASSERT(it == 0); + } + } + + T & operator[](SZ idx) { + SASSERT(idx < size()); + return m_data[idx]; + } + + T const & operator[](SZ idx) const { + SASSERT(idx < size()); + return m_data[idx]; + } + + T & get(SZ idx) { + SASSERT(idx < size()); + return m_data[idx]; + } + + T const & get(SZ idx) const { + SASSERT(idx < size()); + return m_data[idx]; + } + + void set(SZ idx, T const & val) { + SASSERT(idx < size()); + m_data[idx] = val; + } + + void set(SZ idx, T && val) { + SASSERT(idx < size()); + m_data[idx] = std::move(val); + } + + T & back() { + SASSERT(!empty()); + return operator[](size() - 1); + } + + T const & back() const { + SASSERT(!empty()); + return operator[](size() - 1); + } + + void pop_back() { + SASSERT(!empty()); + if (CallDestructors) { + back().~T(); + } + reinterpret_cast(m_data)[SIZE_IDX]--; + } + + void push_back(T const & elem) { + if (m_data == nullptr || reinterpret_cast(m_data)[SIZE_IDX] == reinterpret_cast(m_data)[CAPACITY_IDX]) { + expand_vector(); + } + new (m_data + reinterpret_cast(m_data)[SIZE_IDX]) T(elem); + reinterpret_cast(m_data)[SIZE_IDX]++; + } + + void push_back(T && elem) { + if (m_data == nullptr || reinterpret_cast(m_data)[SIZE_IDX] == reinterpret_cast(m_data)[CAPACITY_IDX]) { + expand_vector(); + } + new (m_data + reinterpret_cast(m_data)[SIZE_IDX]) T(std::move(elem)); + reinterpret_cast(m_data)[SIZE_IDX]++; + } + + void insert(T const & elem) { + push_back(elem); + } + + void erase(iterator pos) { + SASSERT(pos >= begin() && pos < end()); + iterator prev = pos; + ++pos; + iterator e = end(); + for(; pos != e; ++pos, ++prev) { + *prev = *pos; + } + reinterpret_cast(m_data)[SIZE_IDX]--; + } + + void erase(T const & elem) { + iterator it = std::find(begin(), end(), elem); + if (it != end()) { + erase(it); + } + } + + void shrink(SZ s) { + if (m_data) { + SASSERT(s <= reinterpret_cast(m_data)[SIZE_IDX]); + if (CallDestructors) { + iterator it = m_data + s; + iterator e = end(); + for(; it != e; ++it) { + it->~T(); + } + } + reinterpret_cast(m_data)[SIZE_IDX] = s; + } + else { + SASSERT(s == 0); + } + } + + template + void resize(SZ s, Args args...) { + SZ sz = size(); + if (s <= sz) { shrink(s); return; } + while (s > capacity()) { + expand_vector(); + } + SASSERT(m_data != 0); + reinterpret_cast(m_data)[SIZE_IDX] = s; + iterator it = m_data + sz; + iterator end = m_data + s; + for (; it != end; ++it) { + new (it) T(std::forward(args)); + } + } + + void resize(SZ s) { + SZ sz = size(); + if (s <= sz) { shrink(s); return; } + while (s > capacity()) { + expand_vector(); + } + SASSERT(m_data != 0); + reinterpret_cast(m_data)[SIZE_IDX] = s; + iterator it = m_data + sz; + iterator end = m_data + s; + for (; it != end; ++it) { + new (it) T(); + } + } + + void append(old_vector const & other) { + for(SZ i = 0; i < other.size(); ++i) { + push_back(other[i]); + } + } + + void append(SZ sz, T const * data) { + for(SZ i = 0; i < sz; ++i) { + push_back(data[i]); + } + } + + T * c_ptr() const { + return m_data; + } + + void swap(old_vector & other) { + std::swap(m_data, other.m_data); + } + + void reverse() { + SZ sz = size(); + for (SZ i = 0; i < sz/2; ++i) { + std::swap(m_data[i], m_data[sz-i-1]); + } + } + + void fill(T const & elem) { + iterator i = begin(); + iterator e = end(); + for (; i != e; ++i) { + *i = elem; + } + } + + void fill(unsigned sz, T const & elem) { + resize(sz); + fill(elem); + } + + bool contains(T const & elem) const { + const_iterator it = begin(); + const_iterator e = end(); + for (; it != e; ++it) { + if (*it == elem) { + return true; + } + } + return false; + } + + // set pos idx with elem. If idx >= size, then expand using default. + void setx(SZ idx, T const & elem, T const & d) { + if (idx >= size()) { + resize(idx+1, d); + } + m_data[idx] = elem; + } + + // return element at position idx, if idx >= size, then return default + T const & get(SZ idx, T const & d) const { + if (idx >= size()) { + return d; + } + return m_data[idx]; + } + + void reserve(SZ s, T const & d) { + if (s > size()) + resize(s, d); + } + + void reserve(SZ s) { + if (s > size()) + resize(s); + } +}; + +template +class old_ptr_vector : public old_vector { +public: + old_ptr_vector():old_vector() {} + old_ptr_vector(unsigned s):old_vector(s) {} + old_ptr_vector(unsigned s, T * elem):old_vector(s, elem) {} + old_ptr_vector(old_ptr_vector const & source):old_vector(source) {} + old_ptr_vector(old_ptr_vector && other) : old_vector(std::move(other)) {} + old_ptr_vector(unsigned s, T * const * data):old_vector(s, const_cast(data)) {} + old_ptr_vector & operator=(old_ptr_vector const & source) { + old_vector::operator=(source); + return *this; + } +}; + +template +class old_svector : public old_vector { +public: + old_svector():old_vector() {} + old_svector(SZ s):old_vector(s) {} + old_svector(SZ s, T const & elem):old_vector(s, elem) {} + old_svector(old_svector const & source):old_vector(source) {} + old_svector(old_svector && other) : old_vector(std::move(other)) {} + old_svector(SZ s, T const * data):old_vector(s, data) {} + old_svector & operator=(old_svector const & source) { + old_vector::operator=(source); + return *this; + } +}; + +#endif /* OLD_VECTOR_H_ */ diff --git a/src/util/vector.h b/src/util/vector.h index acbcd1357..b3625bdfc 100644 --- a/src/util/vector.h +++ b/src/util/vector.h @@ -1,616 +1,23 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - vector.h - -Abstract: - Dynamic array implementation. - Remarks: - - - Empty arrays consume only sizeof(T *) bytes. - - - There is the option of disabling the destructor invocation for elements stored in the vector. - This is useful for vectors of int. - -Author: - - Leonardo de Moura (leonardo) 2006-09-11. - -Revision History: - ---*/ #ifndef VECTOR_H_ #define VECTOR_H_ -#include "util/debug.h" -#include -#include -#include -#include -#include "util/memory_manager.h" -#include "util/hash.h" -#include "util/z3_exception.h" - -// disable warning for constant 'if' expressions. -// these are used heavily in templates. -#ifdef _MSC_VER -#pragma warning(disable:4127) -#endif +#include "old_vector.h" +#include "hash.h" template -class vector { -#define SIZE_IDX -1 -#define CAPACITY_IDX -2 - T * m_data; - - void destroy_elements() { - iterator it = begin(); - iterator e = end(); - for (; it != e; ++it) { - it->~T(); - } - } - - void free_memory() { - memory::deallocate(reinterpret_cast(reinterpret_cast(m_data) - 2)); - } - - void expand_vector() { - if (m_data == nullptr) { - SZ capacity = 2; - SZ * mem = reinterpret_cast(memory::allocate(sizeof(T) * capacity + sizeof(SZ) * 2)); - *mem = capacity; - mem++; - *mem = 0; - mem++; - m_data = reinterpret_cast(mem); - } - else { - SASSERT(capacity() > 0); - SZ old_capacity = reinterpret_cast(m_data)[CAPACITY_IDX]; - SZ old_capacity_T = sizeof(T) * old_capacity + sizeof(SZ) * 2; - SZ new_capacity = (3 * old_capacity + 1) >> 1; - SZ new_capacity_T = sizeof(T) * new_capacity + sizeof(SZ) * 2; - if (new_capacity <= old_capacity || new_capacity_T <= old_capacity_T) { - throw default_exception("Overflow encountered when expanding vector"); - } - SZ *mem, *old_mem = reinterpret_cast(m_data) - 2; -#if defined(__GNUC__) && !defined(__clang__) && __GNUC__ < 5 - if (__has_trivial_copy(T)) { -#else - if (std::is_trivially_copyable::value) { -#endif - mem = (SZ*)memory::reallocate(old_mem, new_capacity_T); - m_data = reinterpret_cast(mem + 2); - } else { - mem = (SZ*)memory::allocate(new_capacity_T); - auto old_data = m_data; - auto old_size = size(); - mem[1] = old_size; - m_data = reinterpret_cast(mem + 2); - for (unsigned i = 0; i < old_size; ++i) { - new (&m_data[i]) T(std::move(old_data[i])); - old_data[i].~T(); - } - memory::deallocate(old_mem); - } - *mem = new_capacity; - } - } - - void copy_core(vector const & source) { - SZ size = source.size(); - SZ capacity = source.capacity(); - SZ * mem = reinterpret_cast(memory::allocate(sizeof(T) * capacity + sizeof(SZ) * 2)); - *mem = capacity; - mem++; - *mem = size; - mem++; - m_data = reinterpret_cast(mem); - const_iterator it = source.begin(); - iterator it2 = begin(); - SASSERT(it2 == m_data); - const_iterator e = source.end(); - for (; it != e; ++it, ++it2) { - new (it2) T(*it); - } - } - - void destroy() { - if (m_data) { - if (CallDestructors) { - destroy_elements(); - } - free_memory(); - } - } - -public: - typedef T data; - typedef T * iterator; - typedef const T * const_iterator; - - vector(): - m_data(nullptr) { - } - - vector(SZ s) { - if (s == 0) { - m_data = nullptr; - return; - } - SZ * mem = reinterpret_cast(memory::allocate(sizeof(T) * s + sizeof(SZ) * 2)); - *mem = s; - mem++; - *mem = s; - mem++; - m_data = reinterpret_cast(mem); - // initialize elements - iterator it = begin(); - iterator e = end(); - for (; it != e; ++it) { - new (it) T(); - } - } - - vector(SZ s, T const & elem): - m_data(nullptr) { - resize(s, elem); - } - - vector(vector const & source): - m_data(nullptr) { - if (source.m_data) { - copy_core(source); - } - SASSERT(size() == source.size()); - } - - vector(vector&& other) : m_data(nullptr) { - std::swap(m_data, other.m_data); - } - - vector(SZ s, T const * data): - m_data(nullptr) { - for (SZ i = 0; i < s; i++) { - push_back(data[i]); - } - } - - - ~vector() { - destroy(); - } - - void finalize() { - destroy(); - m_data = nullptr; - } - - bool operator==(vector const & other) const { - if (this == &other) { - return true; - } - if (size() != other.size()) - return false; - for (unsigned i = 0; i < size(); i++) { - if ((*this)[i] != other[i]) - return false; - } - return true; - } - - bool operator!=(vector const & other) const { - return !(*this == other); - } - - - vector & operator=(vector const & source) { - if (this == &source) { - return *this; - } - destroy(); - if (source.m_data) { - copy_core(source); - } - else { - m_data = nullptr; - } - return *this; - } - - vector & operator=(vector && source) { - if (this == &source) { - return *this; - } - destroy(); - m_data = nullptr; - std::swap(m_data, source.m_data); - return *this; - } - - bool containsp(std::function& predicate) const { - for (auto const& t : *this) - if (predicate(t)) - return true; - return false; - } - - /** - * retain elements that satisfy predicate. aka 'where'. - */ - vector filter_pure(std::function& predicate) const { - vector result; - for (auto& t : *this) - if (predicate(t)) - result.push_back(t); - return result; - } - - vector& filter_update(std::function& predicate) { - unsigned j = 0; - for (auto& t : *this) - if (predicate(t)) - set(j++, t); - shrink(j); - return *this; - } - - /** - * update elements using f, aka 'select' - */ - template - vector map_pure(std::function& f) const { - vector result; - for (auto& t : *this) - result.push_back(f(t)); - return result; - } - - vector& map_update(std::function& f) { - unsigned j = 0; - for (auto& t : *this) - set(j++, f(t)); - return *this; - } - - void reset() { - if (m_data) { - if (CallDestructors) { - destroy_elements(); - } - reinterpret_cast(m_data)[SIZE_IDX] = 0; - } - } - - void clear() { reset(); } - - bool empty() const { - return m_data == nullptr || reinterpret_cast(m_data)[SIZE_IDX] == 0; - } - - SZ size() const { - if (m_data == nullptr) { - return 0; - } - return reinterpret_cast(m_data)[SIZE_IDX]; - } - - SZ capacity() const { - if (m_data == nullptr) { - return 0; - } - return reinterpret_cast(m_data)[CAPACITY_IDX]; - } - - iterator begin() { - return m_data; - } - - iterator end() { - return m_data + size(); - } - - const_iterator begin() const { - return m_data; - } - - const_iterator end() const { - return m_data + size(); - } - - class reverse_iterator { - T* v; - public: - reverse_iterator(T* v):v(v) {} - - T operator*() { return *v; } - reverse_iterator operator++(int) { - reverse_iterator tmp = *this; - --v; - return tmp; - } - reverse_iterator& operator++() { - --v; - return *this; - } - - bool operator==(reverse_iterator const& other) const { - return other.v == v; - } - bool operator!=(reverse_iterator const& other) const { - return other.v != v; - } - }; - - reverse_iterator rbegin() { return reverse_iterator(end() - 1); } - reverse_iterator rend() { return reverse_iterator(begin() - 1); } - - void set_end(iterator it) { - if (m_data) { - SZ new_sz = static_cast(it - m_data); - if (CallDestructors) { - iterator e = end(); - for(; it != e; ++it) { - it->~T(); - } - } - reinterpret_cast(m_data)[SIZE_IDX] = new_sz; - } - else { - SASSERT(it == 0); - } - } - - T & operator[](SZ idx) { - SASSERT(idx < size()); - return m_data[idx]; - } - - T const & operator[](SZ idx) const { - SASSERT(idx < size()); - return m_data[idx]; - } - - T & get(SZ idx) { - SASSERT(idx < size()); - return m_data[idx]; - } - - T const & get(SZ idx) const { - SASSERT(idx < size()); - return m_data[idx]; - } - - void set(SZ idx, T const & val) { - SASSERT(idx < size()); - m_data[idx] = val; - } - - void set(SZ idx, T && val) { - SASSERT(idx < size()); - m_data[idx] = std::move(val); - } - - T & back() { - SASSERT(!empty()); - return operator[](size() - 1); - } - - T const & back() const { - SASSERT(!empty()); - return operator[](size() - 1); - } - - void pop_back() { - SASSERT(!empty()); - if (CallDestructors) { - back().~T(); - } - reinterpret_cast(m_data)[SIZE_IDX]--; - } - - void push_back(T const & elem) { - if (m_data == nullptr || reinterpret_cast(m_data)[SIZE_IDX] == reinterpret_cast(m_data)[CAPACITY_IDX]) { - expand_vector(); - } - new (m_data + reinterpret_cast(m_data)[SIZE_IDX]) T(elem); - reinterpret_cast(m_data)[SIZE_IDX]++; - } - - void push_back(T && elem) { - if (m_data == nullptr || reinterpret_cast(m_data)[SIZE_IDX] == reinterpret_cast(m_data)[CAPACITY_IDX]) { - expand_vector(); - } - new (m_data + reinterpret_cast(m_data)[SIZE_IDX]) T(std::move(elem)); - reinterpret_cast(m_data)[SIZE_IDX]++; - } - - void insert(T const & elem) { - push_back(elem); - } - - void erase(iterator pos) { - SASSERT(pos >= begin() && pos < end()); - iterator prev = pos; - ++pos; - iterator e = end(); - for(; pos != e; ++pos, ++prev) { - *prev = *pos; - } - reinterpret_cast(m_data)[SIZE_IDX]--; - } - - void erase(T const & elem) { - iterator it = std::find(begin(), end(), elem); - if (it != end()) { - erase(it); - } - } - - void shrink(SZ s) { - if (m_data) { - SASSERT(s <= reinterpret_cast(m_data)[SIZE_IDX]); - if (CallDestructors) { - iterator it = m_data + s; - iterator e = end(); - for(; it != e; ++it) { - it->~T(); - } - } - reinterpret_cast(m_data)[SIZE_IDX] = s; - } - else { - SASSERT(s == 0); - } - } - - template - void resize(SZ s, Args args...) { - SZ sz = size(); - if (s <= sz) { shrink(s); return; } - while (s > capacity()) { - expand_vector(); - } - SASSERT(m_data != 0); - reinterpret_cast(m_data)[SIZE_IDX] = s; - iterator it = m_data + sz; - iterator end = m_data + s; - for (; it != end; ++it) { - new (it) T(std::forward(args)); - } - } - - void resize(SZ s) { - SZ sz = size(); - if (s <= sz) { shrink(s); return; } - while (s > capacity()) { - expand_vector(); - } - SASSERT(m_data != 0); - reinterpret_cast(m_data)[SIZE_IDX] = s; - iterator it = m_data + sz; - iterator end = m_data + s; - for (; it != end; ++it) { - new (it) T(); - } - } - - void append(vector const & other) { - for(SZ i = 0; i < other.size(); ++i) { - push_back(other[i]); - } - } - - void append(SZ sz, T const * data) { - for(SZ i = 0; i < sz; ++i) { - push_back(data[i]); - } - } - - T * c_ptr() const { - return m_data; - } - - void swap(vector & other) { - std::swap(m_data, other.m_data); - } - - void reverse() { - SZ sz = size(); - for (SZ i = 0; i < sz/2; ++i) { - std::swap(m_data[i], m_data[sz-i-1]); - } - } - - void fill(T const & elem) { - iterator i = begin(); - iterator e = end(); - for (; i != e; ++i) { - *i = elem; - } - } - - void fill(unsigned sz, T const & elem) { - resize(sz); - fill(elem); - } - - bool contains(T const & elem) const { - const_iterator it = begin(); - const_iterator e = end(); - for (; it != e; ++it) { - if (*it == elem) { - return true; - } - } - return false; - } - - // set pos idx with elem. If idx >= size, then expand using default. - void setx(SZ idx, T const & elem, T const & d) { - if (idx >= size()) { - resize(idx+1, d); - } - m_data[idx] = elem; - } - - // return element at position idx, if idx >= size, then return default - T const & get(SZ idx, T const & d) const { - if (idx >= size()) { - return d; - } - return m_data[idx]; - } - - void reserve(SZ s, T const & d) { - if (s > size()) - resize(s, d); - } - - void reserve(SZ s) { - if (s > size()) - resize(s); - } -}; - -template -class ptr_vector : public vector { -public: - ptr_vector():vector() {} - ptr_vector(unsigned s):vector(s) {} - ptr_vector(unsigned s, T * elem):vector(s, elem) {} - ptr_vector(ptr_vector const & source):vector(source) {} - ptr_vector(ptr_vector && other) : vector(std::move(other)) {} - ptr_vector(unsigned s, T * const * data):vector(s, const_cast(data)) {} - ptr_vector & operator=(ptr_vector const & source) { - vector::operator=(source); - return *this; - } -}; +using vector = old_vector; template -class svector : public vector { -public: - svector():vector() {} - svector(SZ s):vector(s) {} - svector(SZ s, T const & elem):vector(s, elem) {} - svector(svector const & source):vector(source) {} - svector(svector && other) : vector(std::move(other)) {} - svector(SZ s, T const * data):vector(s, data) {} - svector & operator=(svector const & source) { - vector::operator=(source); - return *this; - } -}; +using svector = old_svector; -typedef svector int_vector; -typedef svector unsigned_vector; -typedef svector char_vector; -typedef svector signed_char_vector; -typedef svector double_vector; +template +using ptr_vector = old_ptr_vector; + +using int_vector = old_svector; +using unsigned_vector = old_svector; +using char_vector = old_svector; +using signed_char_vector = old_svector; +using double_vector = old_svector; inline std::ostream& operator<<(std::ostream& out, unsigned_vector const& v) { for (unsigned u : v) out << u << " "; From 2f33bafd5a7696a57a04555bc6521063f069ef59 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Thu, 21 Feb 2019 14:59:31 +0000 Subject: [PATCH 29/41] stopwatches: fix a few places that would call start/stop multiple times --- src/muz/rel/dl_instruction.cpp | 11 +++++------ src/sat/sat_local_search.cpp | 1 - src/smt/smt_context.cpp | 1 - src/util/timer.h | 2 +- 4 files changed, 6 insertions(+), 9 deletions(-) diff --git a/src/muz/rel/dl_instruction.cpp b/src/muz/rel/dl_instruction.cpp index 2b76d99f7..79508a4f6 100644 --- a/src/muz/rel/dl_instruction.cpp +++ b/src/muz/rel/dl_instruction.cpp @@ -41,7 +41,6 @@ namespace datalog { execution_context::~execution_context() { reset(); - dealloc(m_stopwatch); } void execution_context::reset() { @@ -104,15 +103,15 @@ namespace datalog { m_timelimit_ms = time_in_ms; if (!m_stopwatch) { m_stopwatch = alloc(stopwatch); + } else { + m_stopwatch->stop(); + m_stopwatch->reset(); } - m_stopwatch->stop(); - m_stopwatch->reset(); m_stopwatch->start(); } void execution_context::reset_timelimit() { - if (m_stopwatch) { - m_stopwatch->stop(); - } + dealloc(m_stopwatch); + m_stopwatch = nullptr; m_timelimit_ms = 0; } diff --git a/src/sat/sat_local_search.cpp b/src/sat/sat_local_search.cpp index 7c3ebb688..cdb90e2a0 100644 --- a/src/sat/sat_local_search.cpp +++ b/src/sat/sat_local_search.cpp @@ -515,7 +515,6 @@ namespace sat { reinit(); DEBUG_CODE(verify_slack();); timer timer; - timer.start(); unsigned step = 0, total_flips = 0, tries = 0; for (tries = 1; !m_unsat_stack.empty() && m_limit.inc(); ++tries) { diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 86b3374fc..ecb69b418 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -3496,7 +3496,6 @@ namespace smt { m_case_split_queue ->init_search_eh(); m_next_progress_sample = 0; TRACE("literal_occ", display_literal_num_occs(tout);); - m_timer.start(); } void context::end_search() { diff --git a/src/util/timer.h b/src/util/timer.h index 37566e613..e2ddb55e7 100644 --- a/src/util/timer.h +++ b/src/util/timer.h @@ -27,7 +27,7 @@ Revision History: class timer { stopwatch m_watch; public: - void start() { + timer() { m_watch.start(); } From 3d7878bafc228877c77891a8985e78c21f780664 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Thu, 21 Feb 2019 15:25:26 +0000 Subject: [PATCH 30/41] hopefully fix build with VS 2012 --- src/util/stopwatch.h | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/util/stopwatch.h b/src/util/stopwatch.h index e35380153..e8665054b 100644 --- a/src/util/stopwatch.h +++ b/src/util/stopwatch.h @@ -31,7 +31,8 @@ class stopwatch bool m_running = false; #endif - static std::chrono::time_point get() { + // FIXME: just use auto with VS 2015+ + static decltype(std::chrono::steady_clock::now()) get() { return std::chrono::steady_clock::now(); } From 6598aedbb206986a9e48e5c1fe3b7ce807f97895 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Thu, 21 Feb 2019 15:52:52 +0000 Subject: [PATCH 31/41] fix VS build, take 2 --- src/sat/sat_solver.cpp | 3 +++ src/util/CMakeLists.txt | 1 - src/util/stopwatch.h | 11 +++++++---- 3 files changed, 10 insertions(+), 5 deletions(-) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 3deb6fc17..8b7d53897 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -27,6 +27,9 @@ Revision History: #include "util/trace.h" #include "util/max_cliques.h" #include "util/gparams.h" +#ifdef _MSC_VER +# include +#endif // define to update glue during propagation #define UPDATE_GLUE diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index b6abb785f..5b1f336d1 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -56,7 +56,6 @@ z3_add_component(util symbol.cpp timeit.cpp timeout.cpp - timer.cpp trace.cpp util.cpp warning.cpp diff --git a/src/util/stopwatch.h b/src/util/stopwatch.h index e8665054b..5fe10fb3b 100644 --- a/src/util/stopwatch.h +++ b/src/util/stopwatch.h @@ -25,14 +25,17 @@ Revision History: class stopwatch { - std::chrono::time_point m_start; - std::chrono::steady_clock::duration m_elapsed; + typedef decltype(std::chrono::steady_clock::now()) clock_t; + typedef decltype(std::chrono::steady_clock::now() - std::chrono::steady_clock::now()) duration_t; + + clock_t m_start; + duration_t m_elapsed; #if Z3DEBUG bool m_running = false; #endif // FIXME: just use auto with VS 2015+ - static decltype(std::chrono::steady_clock::now()) get() { + static clock_t get() { return std::chrono::steady_clock::now(); } @@ -46,7 +49,7 @@ public: } void reset() { - m_elapsed = std::chrono::steady_clock::duration::zero(); + m_elapsed = duration_t::zero(); } void start() { From bb7aa16223965644a65e7f5f4eaf050fb5ef8058 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Thu, 21 Feb 2019 16:38:48 +0000 Subject: [PATCH 32/41] stopwatch: fix debug build crash in sat solver --- src/util/stopwatch.h | 1 + 1 file changed, 1 insertion(+) diff --git a/src/util/stopwatch.h b/src/util/stopwatch.h index 5fe10fb3b..1135c893e 100644 --- a/src/util/stopwatch.h +++ b/src/util/stopwatch.h @@ -50,6 +50,7 @@ public: void reset() { m_elapsed = duration_t::zero(); + DEBUG_CODE(m_running = false;); } void start() { From 4c799c144a2f7554b449dc3a0ad6432e4a348c3f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 22 Feb 2019 11:14:20 +0100 Subject: [PATCH 33/41] fix gc to not remove ternary clauses that are on assignment trail. This addresses issue with drat proofs that don't pass drat-trim due to deletion during gc, but use in conflicts Signed-off-by: Nikolaj Bjorner --- src/sat/sat_clause.cpp | 2 +- src/sat/sat_drat.cpp | 113 +++++++++++++++++++++++++--------- src/sat/sat_drat.h | 4 ++ src/sat/sat_elim_eqs.cpp | 2 +- src/sat/sat_probing.cpp | 3 + src/sat/sat_simplifier.cpp | 24 ++++---- src/sat/sat_simplifier.h | 2 +- src/sat/sat_solver.cpp | 88 ++++++++++++++++++++++---- src/sat/sat_solver.h | 23 +++---- src/sat/sat_watched.cpp | 10 ++- src/sat/tactic/sat_tactic.cpp | 1 + 11 files changed, 201 insertions(+), 71 deletions(-) diff --git a/src/sat/sat_clause.cpp b/src/sat/sat_clause.cpp index d27820e71..03ae55092 100644 --- a/src/sat/sat_clause.cpp +++ b/src/sat/sat_clause.cpp @@ -38,7 +38,6 @@ namespace sat { memcpy(m_lits, lits, sizeof(literal) * sz); mark_strengthened(); SASSERT(check_approx()); - SASSERT(sz > 1); } var_approx_set clause::approx(unsigned num, literal const * lits) { @@ -83,6 +82,7 @@ namespace sat { i++; for (; i < m_size; i++) m_lits[i-1] = m_lits[i]; + m_lits[m_size-1] = l; m_size--; mark_strengthened(); } diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp index ac05b50f1..de65aca92 100644 --- a/src/sat/sat_drat.cpp +++ b/src/sat/sat_drat.cpp @@ -49,10 +49,13 @@ namespace sat { dealloc(m_bout); for (unsigned i = 0; i < m_proof.size(); ++i) { clause* c = m_proof[i]; - if (c && (c->size() == 2 || m_status[i] == status::deleted || m_status[i] == status::external)) { - s.dealloc_clause(c); + if (c) { + m_alloc.del_clause(c); } } + m_proof.reset(); + m_out = nullptr; + m_bout = nullptr; } void drat::updt_config() { @@ -75,7 +78,7 @@ namespace sat { if (st == status::asserted || st == status::external) { return; } - + char buffer[10000]; char digits[20]; // enough for storing unsigned char* lastd = digits + sizeof(digits); @@ -166,6 +169,9 @@ namespace sat { } void drat::append(literal l, status st) { + TRACE("sat_drat", tout << st << " " << l << "\n";); + + declare(l); IF_VERBOSE(20, trace(verbose_stream(), 1, &l, st);); if (st == status::learned) { verify(1, &l); @@ -177,13 +183,15 @@ namespace sat { assign_propagate(l); } - clause* c = s.alloc_clause(1, &l, st == status::learned); - m_proof.push_back(c); - m_status.push_back(st); + m_units.push_back(l); } void drat::append(literal l1, literal l2, status st) { + TRACE("sat_drat", tout << st << " " << l1 << " " << l2 << "\n";); + declare(l1); + declare(l2); literal lits[2] = { l1, l2 }; + IF_VERBOSE(20, trace(verbose_stream(), 2, lits, st);); if (st == status::deleted) { // noop @@ -193,7 +201,7 @@ namespace sat { if (st == status::learned) { verify(2, lits); } - clause* c = s.alloc_clause(2, lits, st == status::learned); + clause* c = m_alloc.mk_clause(2, lits, st == status::learned); m_proof.push_back(c); m_status.push_back(st); if (!m_check_unsat) return; @@ -214,14 +222,37 @@ namespace sat { } } +#if 0 + // debugging code + bool drat::is_clause(clause& c, literal l1, literal l2, literal l3, drat::status st1, drat::status st2) { + //if (st1 != st2) return false; + if (c.size() != 3) return false; + if (l1 == c[0]) { + if (l2 == c[1] && l3 == c[2]) return true; + if (l2 == c[2] && l3 == c[1]) return true; + } + if (l2 == c[0]) { + if (l1 == c[1] && l3 == c[2]) return true; + if (l1 == c[2] && l3 == c[1]) return true; + } + if (l3 == c[0]) { + if (l1 == c[1] && l2 == c[2]) return true; + if (l1 == c[2] && l2 == c[1]) return true; + } + return false; + } +#endif + void drat::append(clause& c, status st) { + TRACE("sat_drat", tout << st << " " << c << "\n";); + for (literal lit : c) declare(lit); unsigned n = c.size(); IF_VERBOSE(20, trace(verbose_stream(), n, c.begin(), st);); if (st == status::learned) { verify(c); } - + m_status.push_back(st); m_proof.push_back(&c); if (st == status::deleted) { @@ -274,6 +305,7 @@ namespace sat { } void drat::declare(literal l) { + if (!m_check) return; unsigned n = static_cast(l.var()); while (m_assignment.size() <= n) { m_assignment.push_back(l_undef); @@ -379,7 +411,7 @@ namespace sat { case l_undef: num_undef++; break; } } - CTRACE("sat", num_true == 0 && num_undef == 1, display(tout);); + CTRACE("sat_drat", num_true == 0 && num_undef == 1, display(tout);); SASSERT(num_true != 0 || num_undef != 1); } } @@ -423,7 +455,7 @@ namespace sat { exit(0); UNREACHABLE(); //display(std::cout); - TRACE("sat", + TRACE("sat_drat", tout << literal_vector(n, c) << "\n"; display(tout); s.display(tout);); @@ -431,16 +463,41 @@ namespace sat { } } + bool drat::contains(literal c, justification const& j) { + if (!m_check_sat) { + return true; + } + switch (j.get_kind()) { + case justification::NONE: + return m_units.contains(c); + case justification::BINARY: + return contains(c, j.get_literal()); + case justification::TERNARY: + return contains(c, j.get_literal1(), j.get_literal2()); + case justification::CLAUSE: + return contains(s.get_clause(j)); + default: + return true; + } + } + bool drat::contains(unsigned n, literal const* lits) { if (!m_check) return true; + unsigned num_add = 0; + unsigned num_del = 0; for (unsigned i = m_proof.size(); i-- > 0; ) { clause& c = *m_proof[i]; status st = m_status[i]; if (match(n, lits, c)) { - return st != status::deleted; + if (st == status::deleted) { + num_del++; + } + else { + num_add++; + } } } - return false; + return num_add > num_del; } bool drat::match(unsigned n, literal const* lits, clause const& c) const { @@ -454,7 +511,9 @@ namespace sat { break; } } - if (!found) return false; + if (!found) { + return false; + } } return true; } @@ -512,7 +571,7 @@ namespace sat { void drat::assign(literal l) { lbool new_value = l.sign() ? l_false : l_true; lbool old_value = value(l); -// TRACE("sat", tout << "assign " << l << " := " << new_value << " from " << old_value << "\n";); +// TRACE("sat_drat", tout << "assign " << l << " := " << new_value << " from " << old_value << "\n";); switch (old_value) { case l_false: m_inconsistent = true; @@ -544,7 +603,7 @@ namespace sat { watched_clause& wc = m_watched_clauses[idx]; clause& c = *wc.m_clause; - //TRACE("sat", tout << "Propagate " << l << " " << c << " watch: " << wc.m_l1 << " " << wc.m_l2 << "\n";); + //TRACE("sat_drat", tout << "Propagate " << l << " " << c << " watch: " << wc.m_l1 << " " << wc.m_l2 << "\n";); if (wc.m_l1 == ~l) { std::swap(wc.m_l1, wc.m_l2); } @@ -596,17 +655,12 @@ namespace sat { } } void drat::add(literal l, bool learned) { - TRACE("sat", tout << "add: " << l << " " << (learned?"l":"t") << "\n";); - declare(l); status st = get_status(learned); if (m_out) dump(1, &l, st); if (m_bout) bdump(1, &l, st); if (m_check) append(l, st); } void drat::add(literal l1, literal l2, bool learned) { - TRACE("sat", tout << "add: " << l1 << " " << l2 << " " << (learned?"l":"t") << "\n";); - declare(l1); - declare(l2); literal ls[2] = {l1, l2}; status st = get_status(learned); if (m_out) dump(2, ls, st); @@ -614,12 +668,13 @@ namespace sat { if (m_check) append(l1, l2, st); } void drat::add(clause& c, bool learned) { - TRACE("sat", tout << "add: " << c << "\n";); - for (unsigned i = 0; i < c.size(); ++i) declare(c[i]); status st = get_status(learned); if (m_out) dump(c.size(), c.begin(), st); if (m_bout) bdump(c.size(), c.begin(), st); - if (m_check_unsat) append(c, get_status(learned)); + if (m_check) { + clause* cl = m_alloc.mk_clause(c.size(), c.begin(), learned); + append(*cl, get_status(learned)); + } } void drat::add(literal_vector const& lits, svector const& premises) { if (m_check) { @@ -627,7 +682,7 @@ namespace sat { case 0: add(); break; case 1: append(lits[0], status::external); break; default: { - clause* c = s.alloc_clause(lits.size(), lits.c_ptr(), true); + clause* c = m_alloc.mk_clause(lits.size(), lits.c_ptr(), true); append(*c, status::external); break; } @@ -635,16 +690,16 @@ namespace sat { } } void drat::add(literal_vector const& c) { - for (unsigned i = 0; i < c.size(); ++i) declare(c[i]); if (m_out) dump(c.size(), c.begin(), status::learned); if (m_bout) bdump(c.size(), c.begin(), status::learned); if (m_check) { + for (literal lit : c) declare(lit); switch (c.size()) { case 0: add(); break; case 1: append(c[0], status::learned); break; default: { verify(c.size(), c.begin()); - clause* cl = s.alloc_clause(c.size(), c.c_ptr(), true); + clause* cl = m_alloc.mk_clause(c.size(), c.c_ptr(), true); append(*cl, status::external); break; } @@ -657,8 +712,10 @@ namespace sat { if (m_bout) bdump(1, &l, status::deleted); if (m_check_unsat) append(l, status::deleted); } + void drat::del(literal l1, literal l2) { literal ls[2] = {l1, l2}; + SASSERT(!(l1 == literal(13923, false) && l2 == literal(14020, true))); if (m_out) dump(2, ls, status::deleted); if (m_bout) bdump(2, ls, status::deleted); if (m_check) append(l1, l2, status::deleted); @@ -677,11 +734,11 @@ namespace sat { } #endif - TRACE("sat", tout << "del: " << c << "\n";); + //SASSERT(!(c.size() == 2 && c[0] == literal(13923, false) && c[1] == literal(14020, true))); if (m_out) dump(c.size(), c.begin(), status::deleted); if (m_bout) bdump(c.size(), c.begin(), status::deleted); if (m_check) { - clause* c1 = s.alloc_clause(c.size(), c.begin(), c.is_learned()); + clause* c1 = m_alloc.mk_clause(c.size(), c.begin(), c.is_learned()); append(*c1, status::deleted); } } diff --git a/src/sat/sat_drat.h b/src/sat/sat_drat.h index 35e5a0655..7224da063 100644 --- a/src/sat/sat_drat.h +++ b/src/sat/sat_drat.h @@ -45,6 +45,7 @@ namespace sat { svector m_watched_clauses; typedef svector watch; solver& s; + clause_allocator m_alloc; std::ostream* m_out; std::ostream* m_bout; ptr_vector m_proof; @@ -61,6 +62,8 @@ namespace sat { void append(literal l1, literal l2, status st); void append(clause& c, status st); + bool is_clause(clause& c, literal l1, literal l2, literal l3, status st1, status st2); + friend std::ostream& operator<<(std::ostream & out, status st); status get_status(bool learned) const; @@ -104,6 +107,7 @@ namespace sat { bool contains(unsigned n, literal const* c); bool contains(literal l1, literal l2) { literal lits[2] = {l1, l2}; return contains(2, lits); } bool contains(literal l1, literal l2, literal l3) { literal lits[3] = {l1, l2, l3}; return contains(3, lits); } + bool contains(literal c, justification const& j); void check_model(model const& m); }; diff --git a/src/sat/sat_elim_eqs.cpp b/src/sat/sat_elim_eqs.cpp index bc69c1f5d..7e19bf520 100644 --- a/src/sat/sat_elim_eqs.cpp +++ b/src/sat/sat_elim_eqs.cpp @@ -207,7 +207,7 @@ namespace sat { c.update_approx(); } if (m_solver.m_config.m_drat) { - m_solver.m_drat.add(c, true); + m_solver.m_drat.add(c, true); drat_delete_clause(); } diff --git a/src/sat/sat_probing.cpp b/src/sat/sat_probing.cpp index 5689112d4..e12e78560 100644 --- a/src/sat/sat_probing.cpp +++ b/src/sat/sat_probing.cpp @@ -52,6 +52,9 @@ namespace sat { unsigned tr_sz = s.m_trail.size(); for (unsigned i = old_tr_sz; i < tr_sz; i++) { entry.m_lits.push_back(s.m_trail[i]); + if (s.m_config.m_drat) { + s.m_drat.add(~l, s.m_trail[i], true); + } } } diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 58dab0ff5..86094d7a3 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -124,9 +124,9 @@ namespace sat { } } - inline void simplifier::remove_clause(clause & c) { + inline void simplifier::remove_clause(clause & c, bool is_unique) { if (!c.was_removed()) { - if (s.m_config.m_drat) { + if (s.m_config.m_drat && is_unique) { s.m_drat.del(c); } for (literal l : c) { @@ -477,7 +477,7 @@ namespace sat { s.set_learned(c1, false); } TRACE("subsumption", tout << c1 << " subsumed " << c2 << "\n";); - remove_clause(c2); + remove_clause(c2, false); m_num_subsumed++; } else if (!c2.was_removed()) { @@ -577,7 +577,7 @@ namespace sat { if (c1.is_learned() && !c2.is_learned()) s.set_learned(c1, false); TRACE("subsumption", tout << c1 << " subsumed " << c2 << "\n";); - remove_clause(c2); + remove_clause(c2, false); m_num_subsumed++; } } @@ -662,7 +662,7 @@ namespace sat { for (auto it = cs.mk_iterator(); !it.at_end(); ) { clause & c = it.curr(); it.next(); - remove_clause(c); + remove_clause(c, true); } cs.reset(); } @@ -674,10 +674,12 @@ namespace sat { m_num_elim_lits++; insert_elim_todo(l.var()); if (s.m_config.m_drat && c.contains(l)) { - m_dummy.set(c.size(), c.begin(), c.is_learned()); + unsigned sz = c.size(); c.elim(l); s.m_drat.add(c, true); - s.m_drat.del(*m_dummy.get()); + c.restore(sz); + s.m_drat.del(c); + c.shrink(sz-1); } else { c.elim(l); @@ -690,7 +692,7 @@ namespace sat { if (cleanup_clause(c)) { // clause was satisfied TRACE("elim_lit", tout << "clause was satisfied\n";); - remove_clause(c); + remove_clause(c, true); return; } unsigned sz = c.size(); @@ -710,7 +712,7 @@ namespace sat { c.restore(sz0); s.mk_bin_clause(c[0], c[1], c.is_learned()); m_sub_bin_todo.push_back(bin_clause(c[0], c[1], c.is_learned())); - remove_clause(c); + remove_clause(c, sz0 != sz); break; default: if (s.m_config.m_drat && sz0 != sz) { @@ -888,7 +890,7 @@ namespace sat { if (s.m_trail.size() > m_last_sub_trail_sz) { unsigned sz0 = c.size(); if (cleanup_clause(c)) { - remove_clause(c); + remove_clause(c, true); continue; } unsigned sz = c.size(); @@ -906,7 +908,7 @@ namespace sat { s.mk_bin_clause(c[0], c[1], c.is_learned()); m_sub_bin_todo.push_back(bin_clause(c[0], c[1], c.is_learned())); c.restore(sz0); - remove_clause(c); + remove_clause(c, sz != sz0); continue; default: if (s.m_config.m_drat && sz != sz0) { diff --git a/src/sat/sat_simplifier.h b/src/sat/sat_simplifier.h index 2aa2b4252..895ebdcb5 100644 --- a/src/sat/sat_simplifier.h +++ b/src/sat/sat_simplifier.h @@ -133,7 +133,7 @@ namespace sat { void register_clauses(clause_vector & cs); - void remove_clause(clause & c); + void remove_clause(clause & c, bool is_unique); void set_learned(clause & c); void set_learned(literal l1, literal l2); diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 3deb6fc17..4a0397cee 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -33,19 +33,22 @@ Revision History: namespace sat { + static unsigned s_lemma_count = 0; + static bool s_verify_contains = false; + solver::solver(params_ref const & p, reslimit& l): solver_core(l), m_checkpoint_enabled(true), m_config(p), m_par(nullptr), m_cls_allocator_idx(false), + m_drat(*this), m_cleaner(*this), m_simplifier(*this, p), m_scc(*this, p), m_asymm_branch(*this, p), m_probing(*this, p), m_mus(*this), - m_drat(*this), m_inconsistent(false), m_searching(false), m_num_frozen(0), @@ -382,6 +385,9 @@ namespace sat { if (!learned && !at_search_lvl()) m_clauses_to_reinit.push_back(clause_wrapper(l1, l2)); } + if (l1 == literal(29327, false) && l2 == literal(29328, false)) { + std::cout << s_lemma_count << "\n"; + } m_stats.m_mk_bin_clause++; get_wlist(~l1).push_back(watched(l2, learned)); get_wlist(~l2).push_back(watched(l1, learned)); @@ -413,8 +419,6 @@ namespace sat { clause * r = alloc_clause(3, lits, learned); bool reinit = attach_ter_clause(*r); if (reinit && !learned) push_reinit_stack(*r); - if (m_config.m_drat) m_drat.add(*r, learned); - if (learned) m_learned.push_back(r); else @@ -424,6 +428,9 @@ namespace sat { bool solver::attach_ter_clause(clause & c) { bool reinit = false; + if (m_config.m_drat) m_drat.add(c, c.is_learned()); + TRACE("sat", tout << c << "\n";); + SASSERT(!c.was_removed()); m_watches[(~c[0]).index()].push_back(watched(c[1], c[2])); m_watches[(~c[1]).index()].push_back(watched(c[0], c[2])); m_watches[(~c[2]).index()].push_back(watched(c[0], c[1])); @@ -459,8 +466,9 @@ namespace sat { else { m_clauses.push_back(r); } - if (m_config.m_drat) + if (m_config.m_drat) { m_drat.add(*r, learned); + } return r; } @@ -2163,6 +2171,36 @@ namespace sat { IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat-gc :strategy " << st_name << " :deleted " << (sz - new_sz) << ")\n";); } + bool solver::can_delete3(literal l1, literal l2, literal l3) const { + if (value(l1) == l_true && + value(l2) == l_false && + value(l3) == l_false) { + justification const& j = m_justification[l1.var()]; + if (j.is_ternary_clause()) { + watched w1(l2, l3); + watched w2(j.get_literal1(), j.get_literal2()); + return w1 != w2; + } + } + return true; + } + + bool solver::can_delete(clause const & c) const { + if (c.on_reinit_stack()) + return false; + if (c.size() == 3) { + return + can_delete3(c[0],c[1],c[2]) && + can_delete3(c[1],c[0],c[2]) && + can_delete3(c[2],c[0],c[1]); + } + literal l0 = c[0]; + if (value(l0) != l_true) + return true; + justification const & jst = m_justification[l0.var()]; + return !jst.is_clause() || cls_allocator().get_clause(jst.get_clause_offset()) != &c; + } + /** \brief Use gc based on dynamic psm. Clauses are initially frozen. */ @@ -2381,6 +2419,21 @@ namespace sat { } } + s_lemma_count++; + + if (s_lemma_count == 51802) { + disable_trace("sat"); + disable_trace("sat_conflict"); + s_verify_contains = false; + } + + + if (s_lemma_count == 51801) { + enable_trace("sat"); + enable_trace("sat_conflict"); + s_verify_contains = true; + } + m_lemma.reset(); unsigned idx = skip_literals_above_conflict_level(); @@ -2401,6 +2454,9 @@ namespace sat { do { TRACE("sat_conflict_detail", tout << "processing consequent: " << consequent << "\n"; tout << "num_marks: " << num_marks << ", js: " << js << "\n";); + + // VERIFY(!s_verify_contains || !m_config.m_drat || m_drat.contains(consequent, js)); + switch (js.get_kind()) { case justification::NONE: break; @@ -2455,6 +2511,8 @@ namespace sat { idx--; num_marks--; reset_mark(c_var); + + TRACE("sat", display_justification(tout << consequent << " ", js) << "\n";); } while (num_marks > 0); @@ -2467,12 +2525,13 @@ namespace sat { TRACE("sat_lemma", tout << "new lemma size: " << m_lemma.size() << "\n" << m_lemma << "\n";); unsigned new_scope_lvl = 0; + bool sub_min = false, res_min = false; if (!m_lemma.empty()) { if (m_config.m_minimize_lemmas) { - minimize_lemma(); + res_min = minimize_lemma(); reset_lemma_var_marks(); if (m_config.m_dyn_sub_res) - dyn_sub_res(); + sub_min = dyn_sub_res(); TRACE("sat_lemma", tout << "new lemma (after minimization) size: " << m_lemma.size() << "\n" << m_lemma << "\n";); } else @@ -2492,12 +2551,12 @@ namespace sat { m_slow_glue_avg.update(glue); pop_reinit(m_scope_lvl - new_scope_lvl); TRACE("sat_conflict_detail", tout << glue << " " << new_scope_lvl << "\n";); - // unsound: m_asymm_branch.minimize(m_scc, m_lemma); clause * lemma = mk_clause_core(m_lemma.size(), m_lemma.c_ptr(), true); if (lemma) { lemma->set_glue(glue); if (m_par) m_par->share_clause(*this, *lemma); } + TRACE("sat_conflict_detail", tout << new_scope_lvl << "\n";); decay_activity(); updt_phase_counters(); @@ -2844,7 +2903,7 @@ namespace sat { if (m_lvl_set.may_contain(var_lvl)) { mark(var); m_unmark.push_back(var); - m_lemma_min_stack.push_back(var); + m_lemma_min_stack.push_back(antecedent); } else { return false; @@ -2862,11 +2921,12 @@ namespace sat { */ bool solver::implied_by_marked(literal lit) { m_lemma_min_stack.reset(); // avoid recursive function - m_lemma_min_stack.push_back(lit.var()); + m_lemma_min_stack.push_back(lit); unsigned old_size = m_unmark.size(); while (!m_lemma_min_stack.empty()) { - bool_var var = m_lemma_min_stack.back(); + lit = m_lemma_min_stack.back(); + bool_var var = lit.var(); m_lemma_min_stack.pop_back(); justification const& js = m_justification[var]; switch(js.get_kind()) { @@ -2928,6 +2988,8 @@ namespace sat { UNREACHABLE(); break; } + TRACE("sat_conflict", + display_justification(tout << var << " ",js) << "\n";); } return true; } @@ -2958,7 +3020,7 @@ namespace sat { literals that are implied by other literals in m_lemma and/or literals assigned at level 0. */ - void solver::minimize_lemma() { + bool solver::minimize_lemma() { SASSERT(!m_lemma.empty()); SASSERT(m_unmark.empty()); updt_lemma_lvl_set(); @@ -2982,6 +3044,7 @@ namespace sat { reset_unmark(0); m_lemma.shrink(j); m_stats.m_minimized_lits += sz - j; + return j < sz; } /** @@ -3055,7 +3118,7 @@ namespace sat { \brief Apply dynamic subsumption resolution to new lemma. Only binary and ternary clauses are used. */ - void solver::dyn_sub_res() { + bool solver::dyn_sub_res() { unsigned sz = m_lemma.size(); for (unsigned i = 0; i < sz; i++) { mark_lit(m_lemma[i]); @@ -3168,6 +3231,7 @@ namespace sat { SASSERT(j >= 1); m_lemma.shrink(j); + return j < sz; } diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index c000ccb79..47e226cc4 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -85,9 +85,10 @@ namespace sat { stats m_stats; scoped_ptr m_ext; parallel* m_par; - random_gen m_rand; + drat m_drat; // DRAT for generating proofs clause_allocator m_cls_allocator[2]; bool m_cls_allocator_idx; + random_gen m_rand; cleaner m_cleaner; model m_model; model_converter m_mc; @@ -97,7 +98,6 @@ namespace sat { asymm_branch m_asymm_branch; probing m_probing; mus m_mus; // MUS for minimal core extraction - drat m_drat; // DRAT for generating proofs bool m_inconsistent; bool m_searching; // A conflict is usually a single justification. That is, a justification @@ -461,17 +461,8 @@ namespace sat { void gc_dyn_psm(); bool activate_frozen_clause(clause & c); unsigned psm(clause const & c) const; - bool can_delete(clause const & c) const { - if (c.on_reinit_stack()) - return false; - if (c.size() == 3) - return true; // not needed to justify anything. - literal l0 = c[0]; - if (value(l0) != l_true) - return true; - justification const & jst = m_justification[l0.var()]; - return !jst.is_clause() || cls_allocator().get_clause(jst.get_clause_offset()) != &c; - } + bool can_delete(clause const & c) const; + bool can_delete3(literal l1, literal l2, literal l3) const; clause& get_clause(watch_list::iterator it) const { SASSERT(it->get_kind() == watched::CLAUSE); @@ -522,14 +513,14 @@ namespace sat { typedef approx_set_tpl level_approx_set; bool_var_vector m_unmark; level_approx_set m_lvl_set; - bool_var_vector m_lemma_min_stack; + literal_vector m_lemma_min_stack; bool process_antecedent_for_minimization(literal antecedent); bool implied_by_marked(literal lit); void reset_unmark(unsigned old_size); void updt_lemma_lvl_set(); - void minimize_lemma(); void reset_lemma_var_marks(); - void dyn_sub_res(); + bool minimize_lemma(); + bool dyn_sub_res(); // ----------------------- // diff --git a/src/sat/sat_watched.cpp b/src/sat/sat_watched.cpp index 966bd8325..8811a4e74 100644 --- a/src/sat/sat_watched.cpp +++ b/src/sat/sat_watched.cpp @@ -86,7 +86,15 @@ namespace sat { } } wlist.set_end(it2); - //VERIFY(found); +#if 0 + VERIFY(found); + for (watched const& w2 : wlist) { + if (w2 == w) { + std::cout << l1 << " " << l2 << "\n"; + } + //VERIFY(w2 != w); + } +#endif } void conflict_cleanup(watch_list::iterator it, watch_list::iterator it2, watch_list& wlist) { diff --git a/src/sat/tactic/sat_tactic.cpp b/src/sat/tactic/sat_tactic.cpp index 2739932e6..b2137795b 100644 --- a/src/sat/tactic/sat_tactic.cpp +++ b/src/sat/tactic/sat_tactic.cpp @@ -200,6 +200,7 @@ public: throw tactic_exception(ex.msg()); } catch (z3_exception& ex) { + (void)ex; TRACE("sat", tout << ex.msg() << "\n";); throw; } From 699834261e6e8f70d3928409f6a7fde22f34d2ee Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 22 Feb 2019 12:55:01 +0000 Subject: [PATCH 34/41] Fix translation of FPA numerals in ast_smt_pp. Fixes #2145. --- src/ast/ast_smt_pp.cpp | 30 ++++++++++++++---------------- 1 file changed, 14 insertions(+), 16 deletions(-) diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp index 2490e0314..ea220f7e7 100644 --- a/src/ast/ast_smt_pp.cpp +++ b/src/ast/ast_smt_pp.cpp @@ -24,6 +24,7 @@ Revision History: #include "util/vector.h" #include "util/smt2_util.h" #include "ast/ast_smt_pp.h" +#include "ast/ast_smt2_pp.h" #include "ast/arith_decl_plugin.h" #include "ast/bv_decl_plugin.h" #include "ast/array_decl_plugin.h" @@ -223,7 +224,7 @@ class smt_printer { } } else if (m_manager.is_ite(d)) { - m_out << "ite"; + m_out << "ite"; } else if (m_manager.is_implies(d)) { m_out << "=>"; @@ -266,7 +267,7 @@ class smt_printer { else { m_out << "(_ " << sym << " "; } - + for (unsigned i = 0; i < num_params; ++i) { parameter const& p = params[i]; if (p.is_ast()) { @@ -320,7 +321,7 @@ class smt_printer { if (num_sorts > 0) { m_out << "("; } - m_out << m_renaming.get_symbol(s->get_name(), false); + m_out << m_renaming.get_symbol(s->get_name(), false); if (num_sorts > 0) { for (unsigned i = 0; i < num_sorts; ++i) { m_out << " "; @@ -388,10 +389,7 @@ class smt_printer { m_out << "(_ bv" << val << " " << bv_size << ")"; } else if (m_futil.is_numeral(n, float_val)) { - m_out << "((_ to_fp " << - float_val.get().get_ebits() << " " << - float_val.get().get_sbits() << ") RTZ " << - m_futil.fm().to_string(float_val).c_str() << ")"; + m_out << mk_ismt2_pp(n, m_manager); } else if (m_bvutil.is_bit2bool(n)) { unsigned bit = n->get_decl()->get_parameter(0).get_int(); @@ -402,7 +400,7 @@ class smt_printer { else if (m_manager.is_label(n, pos, names) && !names.empty()) { m_out << "(! "; pp_marked_expr(n->get_arg(0)); - m_out << (pos?":lblpos":":lblneg") << " " << m_renaming.get_symbol(names[0], false) << ")"; + m_out << (pos?":lblpos":":lblneg") << " " << m_renaming.get_symbol(names[0], false) << ")"; } else if (m_manager.is_label_lit(n, names) && !names.empty()) { m_out << "(! true :lblpos " << m_renaming.get_symbol(names[0], false) << ")"; @@ -435,7 +433,7 @@ class smt_printer { pp_arg(curr, n); m_out << ")"; - } + } else if (m_manager.is_distinct(decl)) { ptr_vector args(num_args, n->get_args()); unsigned idx = 0; @@ -613,7 +611,7 @@ class smt_printer { pp_id(n); m_out << " "; pp_expr(n); - m_out << ")"; + m_out << ")"; m_out << ")"; newline(); } @@ -781,7 +779,7 @@ public: datatype_util util(m_manager); SASSERT(util.is_datatype(s)); - sort_ref_vector ps(m_manager); + sort_ref_vector ps(m_manager); ptr_vector defs; util.get_defs(s, defs); @@ -790,7 +788,7 @@ public: if (mark.is_marked(sr)) return; // already processed mark.mark(sr, true); } - + m_out << "(declare-datatypes ("; bool first_def = true; for (datatype::def* d : defs) { @@ -800,7 +798,7 @@ public: m_out << ") ("; bool first_sort = true; for (datatype::def* d : defs) { - if (!first_sort) m_out << "\n "; else first_sort = false; + if (!first_sort) m_out << "\n "; else first_sort = false; if (!d->params().empty()) { m_out << "(par ("; bool first_param = true; @@ -814,7 +812,7 @@ public: bool first_constr = true; for (datatype::constructor* f : *d) { if (!first_constr) m_out << " "; else first_constr = false; - m_out << "("; + m_out << "("; m_out << m_renaming.get_symbol(f->name(), false); for (datatype::accessor* a : *f) { m_out << " (" << m_renaming.get_symbol(a->name(), false) << " "; @@ -828,7 +826,7 @@ public: } m_out << ")"; } - m_out << "))"; + m_out << "))"; newline(); } @@ -864,7 +862,7 @@ public: } m_out << ") "; visit_sort(d->get_range()); - m_out << ")"; + m_out << ")"; } void visit_pred(func_decl* d) { From 73060ecaec864ad09ba6a5c916607bb6c5ca78da Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 22 Feb 2019 13:57:09 +0100 Subject: [PATCH 35/41] remove debug code Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver.cpp | 21 --------------------- 1 file changed, 21 deletions(-) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 3669f801e..c6b04cfd8 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -36,8 +36,6 @@ Revision History: namespace sat { - static unsigned s_lemma_count = 0; - static bool s_verify_contains = false; solver::solver(params_ref const & p, reslimit& l): solver_core(l), @@ -388,9 +386,6 @@ namespace sat { if (!learned && !at_search_lvl()) m_clauses_to_reinit.push_back(clause_wrapper(l1, l2)); } - if (l1 == literal(29327, false) && l2 == literal(29328, false)) { - std::cout << s_lemma_count << "\n"; - } m_stats.m_mk_bin_clause++; get_wlist(~l1).push_back(watched(l2, learned)); get_wlist(~l2).push_back(watched(l1, learned)); @@ -2422,20 +2417,6 @@ namespace sat { } } - s_lemma_count++; - - if (s_lemma_count == 51802) { - disable_trace("sat"); - disable_trace("sat_conflict"); - s_verify_contains = false; - } - - - if (s_lemma_count == 51801) { - enable_trace("sat"); - enable_trace("sat_conflict"); - s_verify_contains = true; - } m_lemma.reset(); @@ -2458,8 +2439,6 @@ namespace sat { TRACE("sat_conflict_detail", tout << "processing consequent: " << consequent << "\n"; tout << "num_marks: " << num_marks << ", js: " << js << "\n";); - // VERIFY(!s_verify_contains || !m_config.m_drat || m_drat.contains(consequent, js)); - switch (js.get_kind()) { case justification::NONE: break; From c2ebbc92104c2faf5aecfc030bdaccd26c23d52c Mon Sep 17 00:00:00 2001 From: Daniel Schemmel Date: Fri, 22 Feb 2019 19:50:15 +0100 Subject: [PATCH 36/41] fix -Wsign-compare (len can never become negative anyway) --- src/sat/sat_drat.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp index de65aca92..5de340674 100644 --- a/src/sat/sat_drat.cpp +++ b/src/sat/sat_drat.cpp @@ -83,7 +83,7 @@ namespace sat { char digits[20]; // enough for storing unsigned char* lastd = digits + sizeof(digits); - int len = 0; + unsigned len = 0; if (st == status::deleted) { buffer[0] = 'd'; buffer[1] = ' '; From c0d20f8ea8a39b51b8651481a79e49157bb86548 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 23 Feb 2019 10:59:10 +0100 Subject: [PATCH 37/41] add cr Signed-off-by: Nikolaj Bjorner --- src/util/buffer.h | 13 +++++++++++++ src/util/old_buffer.h | 2 ++ src/util/old_vector.h | 2 ++ src/util/vector.h | 13 +++++++++++++ 4 files changed, 30 insertions(+) diff --git a/src/util/buffer.h b/src/util/buffer.h index 7a89ffef3..0d32245d3 100644 --- a/src/util/buffer.h +++ b/src/util/buffer.h @@ -1,3 +1,16 @@ +/*++ +Copyright (c) 2019 Microsoft Corporation + +Module Name: + + buffer.h + +Author: + + Daniel Schemmel 2019-2-23 + +--*/ + #ifndef BUFFER_H_ #define BUFFER_H_ diff --git a/src/util/old_buffer.h b/src/util/old_buffer.h index 5ed1df583..88800b05a 100644 --- a/src/util/old_buffer.h +++ b/src/util/old_buffer.h @@ -15,6 +15,8 @@ Author: Revision History: + 2019-2-23 Renamed to old_buffer from buffer to provide new implementation + --*/ #ifndef OLD_BUFFER_H_ #define OLD_BUFFER_H_ diff --git a/src/util/old_vector.h b/src/util/old_vector.h index 53450e6cf..47dc88aab 100644 --- a/src/util/old_vector.h +++ b/src/util/old_vector.h @@ -20,6 +20,8 @@ Author: Revision History: + 2019-2-23 Renamed from vector to old_vector to provide new implementation + --*/ #ifndef OLD_VECTOR_H_ #define OLD_VECTOR_H_ diff --git a/src/util/vector.h b/src/util/vector.h index b3625bdfc..9e2e35acc 100644 --- a/src/util/vector.h +++ b/src/util/vector.h @@ -1,3 +1,16 @@ +/*++ +Copyright (c) 2019 Microsoft Corporation + +Module Name: + + vector.h + +Author: + + Daniel Schemmel 2019-2-23 + +--*/ + #ifndef VECTOR_H_ #define VECTOR_H_ From 773c61369480b6f031eb8fa98a7eb24bd52c7070 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 23 Feb 2019 11:10:01 +0100 Subject: [PATCH 38/41] fix #2149 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/array_rewriter.cpp | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/ast/rewriter/array_rewriter.cpp b/src/ast/rewriter/array_rewriter.cpp index 83749c82d..56e094dab 100644 --- a/src/ast/rewriter/array_rewriter.cpp +++ b/src/ast/rewriter/array_rewriter.cpp @@ -375,7 +375,13 @@ br_status array_rewriter::mk_set_intersect(unsigned num_args, expr * const * arg br_status array_rewriter::mk_set_complement(expr * arg, expr_ref & result) { - return mk_map_core(m().mk_not_decl(), 1, &arg, result); + func_decl* fnot = m().mk_not_decl(); + br_status st = mk_map_core(fnot, 1, &arg, result); + if (BR_FAILED == st) { + result = m_util.mk_map(fnot, 1, &arg); + st = BR_DONE; + } + return st; } br_status array_rewriter::mk_set_difference(expr * arg1, expr * arg2, expr_ref & result) { From 36643aafd27cae92e5195b6dcb6f7847e9fb1ea9 Mon Sep 17 00:00:00 2001 From: Daniel Schemmel Date: Fri, 22 Feb 2019 19:54:53 +0100 Subject: [PATCH 39/41] fix -Wmisleading-indentation --- src/smt/theory_jobscheduler.cpp | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_jobscheduler.cpp b/src/smt/theory_jobscheduler.cpp index a7f877f15..fbf0a3eb2 100644 --- a/src/smt/theory_jobscheduler.cpp +++ b/src/smt/theory_jobscheduler.cpp @@ -499,7 +499,10 @@ namespace smt { std::ostream& theory_jobscheduler::display(std::ostream & out, job_resource const& jr) const { return out << "r:" << jr.m_resource_id << " cap:" << jr.m_capacity << " load:" << jr.m_loadpct << " end:" << jr.m_finite_capacity_end; - for (auto const& s : jr.m_properties) out << " " << s; out << "\n"; + for (auto const& s : jr.m_properties) { + out << " " << s; + } + out << "\n"; } std::ostream& theory_jobscheduler::display(std::ostream & out, job_info const& j) const { @@ -511,7 +514,10 @@ namespace smt { std::ostream& theory_jobscheduler::display(std::ostream & out, res_available const& r) const { return out << "[" << r.m_start << ":" << r.m_end << "] @ " << r.m_loadpct << "%"; - for (auto const& s : r.m_properties) out << " " << s; out << "\n"; + for (auto const& s : r.m_properties) { + out << " " << s; + } + out << "\n"; } std::ostream& theory_jobscheduler::display(std::ostream & out, res_info const& r) const { From 142f3638cf93e0012fcf49afbbfbee43a79ccd84 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 23 Feb 2019 22:45:39 +0100 Subject: [PATCH 40/41] spaces Signed-off-by: Nikolaj Bjorner --- src/smt/theory_jobscheduler.cpp | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/smt/theory_jobscheduler.cpp b/src/smt/theory_jobscheduler.cpp index fbf0a3eb2..53b64ab08 100644 --- a/src/smt/theory_jobscheduler.cpp +++ b/src/smt/theory_jobscheduler.cpp @@ -500,9 +500,9 @@ namespace smt { std::ostream& theory_jobscheduler::display(std::ostream & out, job_resource const& jr) const { return out << "r:" << jr.m_resource_id << " cap:" << jr.m_capacity << " load:" << jr.m_loadpct << " end:" << jr.m_finite_capacity_end; for (auto const& s : jr.m_properties) { - out << " " << s; - } - out << "\n"; + out << " " << s; + } + out << "\n"; } std::ostream& theory_jobscheduler::display(std::ostream & out, job_info const& j) const { @@ -515,9 +515,9 @@ namespace smt { std::ostream& theory_jobscheduler::display(std::ostream & out, res_available const& r) const { return out << "[" << r.m_start << ":" << r.m_end << "] @ " << r.m_loadpct << "%"; for (auto const& s : r.m_properties) { - out << " " << s; - } - out << "\n"; + out << " " << s; + } + out << "\n"; } std::ostream& theory_jobscheduler::display(std::ostream & out, res_info const& r) const { From 6ef3e5e3638fa5a3ba87bf3bc46f5eab81fbabfd Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 24 Feb 2019 14:21:34 -0800 Subject: [PATCH 41/41] integrate some self-contained fixes from #2147 Signed-off-by: Nikolaj Bjorner --- src/ast/substitution/substitution.cpp | 2 +- src/util/array.h | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/ast/substitution/substitution.cpp b/src/ast/substitution/substitution.cpp index 7e981aab8..e16fdf3dd 100644 --- a/src/ast/substitution/substitution.cpp +++ b/src/ast/substitution/substitution.cpp @@ -112,7 +112,7 @@ void substitution::apply(unsigned num_actual_offsets, unsigned const * deltas, e TRACE("subst_bug", tout << "visited: " << visited << ", n1: " << mk_pp(n1.get_expr(), m_manager) << " : " << n1.get_offset() << "\n";); if (visited) { m_todo.pop_back(); - expr * new_expr; + expr * new_expr = nullptr; m_apply_cache.find(n1, new_expr); m_apply_cache.insert(n, new_expr); TRACE("subst_bug", tout << "1. insert n: " << mk_pp(n.get_expr(), m_manager) << " : " << n.get_offset() diff --git a/src/util/array.h b/src/util/array.h index 9f0321777..41b36693a 100644 --- a/src/util/array.h +++ b/src/util/array.h @@ -151,7 +151,7 @@ public: if (m_data == nullptr) { return 0; } - return static_cast(reinterpret_cast(m_data)[SIZE_IDX]); + return static_cast(reinterpret_cast(m_data)[ARRAY_SIZE_IDX]); } bool empty() const { return m_data == nullptr; }