From e23509797a81c2730b066ea85330b1411e409324 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 19 Jan 2017 19:28:20 -0800 Subject: [PATCH 01/11] access parameters from Python API Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 31 +++++++++++++++++++++++++++++++ 1 file changed, 31 insertions(+) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 01dacace7..a6f91a0a2 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -691,6 +691,30 @@ class FuncDeclRef(AstRef): """ return Z3_get_decl_kind(self.ctx_ref(), self.ast) + def params(self): + ctx = self.ctx + n = Z3_get_decl_num_parameters(self.ctx_ref(), self.ast) + result = [ None for i in range(n) ] + for i in range(n): + k = Z3_get_decl_parameter_kind(self.ctx_ref(), self.ast, i) + if k == Z3_PARAMETER_INT: + result[i] = Z3_get_decl_int_parameter(self.ctx_ref(), self.ast, i) + elif k == Z3_PARAMETER_DOUBLE: + result[i] = Z3_get_decl_double_parameter(self.ctx_ref(), self.ast, i) + elif k == Z3_PARAMETER_RATIONAL: + result[i] = Z3_get_decl_rational_parameter(self.ctx_ref(), self.ast, i) + elif k == Z3_PARAMETER_SYMBOL: + result[i] = Z3_get_decl_symbol_parameter(self.ctx_ref(), self.ast, i) + elif k == Z3_PARAMETER_SORT: + result[i] = SortRef(Z3_get_decl_sort_parameter(self.ctx_ref(), self.ast, i), ctx) + elif k == Z3_PARAMETER_AST: + result[i] = ExprRef(Z3_get_decl_ast_parameter(self.ctx_ref(), self.ast, i), ctx) + elif k == Z3_PARAMETER_FUNC_DECL: + result[i] = FuncDeclRef(Z3_get_decl_func_decl_parameter(self.ctx_ref(), self.ast, i), ctx) + else: + assert(False) + return result + def __call__(self, *args): """Create a Z3 application expression using the function `self`, and the given arguments. @@ -2637,6 +2661,13 @@ class RatNumRef(ArithRef): """ return self.denominator().as_long() + def is_int(self): + return self.denominator().is_int() and self.denominator_as_long() == 1 + + def as_long(self): + _z3_assert(self.is_int(), "Expected integer fraction") + return self.numerator_as_long() + def as_decimal(self, prec): """ Return a Z3 rational value as a string in decimal notation using at most `prec` decimal places. From adf8072eaacea187a60ff3690a6b0aaa12b586af Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 21 Jan 2017 12:28:37 +0000 Subject: [PATCH 02/11] Added option to limit the distance of unsat core extension through patterns. --- src/smt/params/smt_params_helper.pyg | 3 ++- src/smt/smt_solver.cpp | 11 ++++++++--- 2 files changed, 10 insertions(+), 4 deletions(-) diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 178b2117f..a3f163ed4 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -63,5 +63,6 @@ def_module_params(module_name='smt', ('dack.threshold', UINT, 10, ' number of times the congruence rule must be used before Leibniz\'s axiom is expanded'), ('core.validate', BOOL, False, 'validate unsat core produced by SMT context'), ('core.minimize', BOOL, False, 'minimize unsat core produced by SMT context'), - ('core.extend_patterns', BOOL, False, 'extend unsat core with literals that trigger (potential) quantifier instances') + ('core.extend_patterns', BOOL, False, 'extend unsat core with literals that trigger (potential) quantifier instances'), + ('core.extend_patterns.max_distance', UINT, UINT_MAX, 'limits the distance of a pattern-extended unsat core') )) diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index f80ff09f4..ab6be5d91 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -37,6 +37,7 @@ namespace smt { symbol m_logic; bool m_minimizing_core; bool m_core_extend_patterns; + unsigned m_core_extend_patterns_max_distance; obj_map m_name2assertion; public: @@ -46,12 +47,14 @@ namespace smt { m_params(p), m_context(m, m_smt_params), m_minimizing_core(false), - m_core_extend_patterns(false) { + m_core_extend_patterns(false), + m_core_extend_patterns_max_distance(UINT_MAX) { m_logic = l; if (m_logic != symbol::null) m_context.set_logic(m_logic); smt_params_helper smth(p); m_core_extend_patterns = smth.core_extend_patterns(); + m_core_extend_patterns_max_distance = smth.core_extend_patterns_max_distance(); } virtual solver * translate(ast_manager & m, params_ref const & p) { @@ -283,7 +286,7 @@ namespace smt { func_decl_set pattern_fds; vector assrtn_fds; - do { + for (unsigned d = 0; d < m_core_extend_patterns_max_distance; d++) { new_core_literals.reset(); unsigned sz = core.size(); @@ -308,8 +311,10 @@ namespace smt { } core.append(new_core_literals.size(), new_core_literals.c_ptr()); + + if (new_core_literals.empty()) + break; } - while (!new_core_literals.empty()); } }; }; From 4ec4abd7e38a2a5a1794ddd6a51a8a7b10a2feab Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 23 Jan 2017 13:31:43 -0800 Subject: [PATCH 03/11] fix test for int-value Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index a6f91a0a2..c54cd6091 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -2394,7 +2394,7 @@ def is_int_value(a): >>> is_int_value(RealVal(1)) False """ - return is_arith(a) and a.is_int() and _is_numeral(a.ctx, a.as_ast()) + return isinstance(a, IntNumRef) def is_rational_value(a): """Return `True` if `a` is rational value of sort Real. From 60783e5696e4a741e7ff4aaeb4eb979d3c4bd77c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 25 Jan 2017 13:26:58 -0800 Subject: [PATCH 04/11] fix regression for z3num Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index c54cd6091..77b74336e 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -2394,7 +2394,7 @@ def is_int_value(a): >>> is_int_value(RealVal(1)) False """ - return isinstance(a, IntNumRef) + return is_arith(a) and a.is_int() and _is_numeral(a.ctx, a.as_ast()) def is_rational_value(a): """Return `True` if `a` is rational value of sort Real. @@ -2662,6 +2662,12 @@ class RatNumRef(ArithRef): return self.denominator().as_long() def is_int(self): + return False + + def is_real(self): + return True + + def is_int_value(self): return self.denominator().is_int() and self.denominator_as_long() == 1 def as_long(self): From 4782e19086d751147a7cfc654846ac455c0a7d15 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 25 Jan 2017 16:21:51 -0800 Subject: [PATCH 05/11] fix bug in sat-simplifier decreasing heap values of variables that are not in the heap Signed-off-by: Nikolaj Bjorner --- src/sat/sat_simplifier.cpp | 25 +++++++++++++++---------- 1 file changed, 15 insertions(+), 10 deletions(-) diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index c42572f1e..62fb99a11 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -896,7 +896,7 @@ namespace sat { unsigned idx = l.index(); if (m_queue.contains(idx)) m_queue.decreased(idx); - else + else m_queue.insert(idx); } literal next() { SASSERT(!empty()); return to_literal(m_queue.erase_min()); } @@ -918,16 +918,19 @@ namespace sat { } void insert(literal l) { - bool_var v = l.var(); - if (s.is_external(v) || s.was_eliminated(v)) - return; m_queue.insert(l); } + bool process_var(bool_var v) { + return !s.is_external(v) && !s.was_eliminated(v); + } + void operator()(unsigned num_vars) { for (bool_var v = 0; v < num_vars; v++) { - insert(literal(v, false)); - insert(literal(v, true)); + if (process_var(v)) { + insert(literal(v, false)); + insert(literal(v, true)); + } } while (!m_queue.empty()) { s.checkpoint(); @@ -941,9 +944,9 @@ namespace sat { void process(literal l) { TRACE("blocked_clause", tout << "processing: " << l << "\n";); model_converter::entry * new_entry = 0; - if (s.is_external(l.var()) || s.was_eliminated(l.var())) + if (!process_var(l.var())) { return; - + } { m_to_remove.reset(); { @@ -963,8 +966,10 @@ namespace sat { mc.insert(*new_entry, c); unsigned sz = c.size(); for (unsigned i = 0; i < sz; i++) { - if (c[i] != l) - m_queue.decreased(~c[i]); + literal lit = c[i]; + if (lit != l && process_var(lit.var())) { + m_queue.decreased(~lit); + } } } s.unmark_all(c); From 777091e653f0674a81e374634da9e3195ef50cd1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 25 Jan 2017 18:09:27 -0800 Subject: [PATCH 06/11] fix part 1 of #875 Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.cpp | 2 ++ src/smt/theory_seq.cpp | 28 +++++++++++++++------------- 2 files changed, 17 insertions(+), 13 deletions(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index c7aecca88..3c88a75a2 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -2031,11 +2031,13 @@ namespace smt { v.shrink(old_size); } +#if 0 void context::mark_as_deleted(clause * cls) { SASSERT(!cls->deleted()); remove_cls_occs(cls); cls->mark_as_deleted(m_manager); } +#endif /** \brief Undo variable assignments. diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index ed95ef8d7..cdea02c48 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -2958,22 +2958,19 @@ void theory_seq::tightest_prefix(expr* s, expr* x) { let i = Index(t, s, offset): offset >= len(t) => i = -1 - - offset fixed to 0: - len(t) != 0 & !contains(t, s) => i = -1 - len(t) != 0 & contains(t, s) => t = xsy & i = len(x) + + + offset = 0 & len(t) != 0 & contains(t, s) => t = xsy & i = len(x) tightest_prefix(x, s) - offset not fixed: 0 <= offset < len(t) => xy = t & len(x) = offset & (-1 = indexof(y, s, 0) => -1 = i) & (indexof(y, s, 0) >= 0 => indexof(t, s, 0) + offset = i) - if offset < 0 - under specified + offset < 0 => i = -1 optional lemmas: (len(s) > len(t) -> i = -1) @@ -2987,17 +2984,19 @@ void theory_seq::add_indexof_axiom(expr* i) { expr_ref minus_one(m_autil.mk_int(-1), m); expr_ref zero(m_autil.mk_int(0), m); expr_ref xsy(m); + + literal cnt = mk_literal(m_util.str.mk_contains(t, s)); + literal i_eq_m1 = mk_eq(i, minus_one, false); + add_axiom(cnt, i_eq_m1); + literal s_eq_empty = mk_eq_empty(s); + add_axiom(~s_eq_empty, mk_eq(i, zero, false)); + add_axiom(s_eq_empty, ~mk_eq_empty(t), i_eq_m1); if (!offset || (m_autil.is_numeral(offset, r) && r.is_zero())) { expr_ref x = mk_skolem(m_indexof_left, t, s); expr_ref y = mk_skolem(m_indexof_right, t, s); xsy = mk_concat(x, s, y); expr_ref lenx(m_util.str.mk_length(x), m); - literal cnt = mk_literal(m_util.str.mk_contains(t, s)); - literal s_eq_empty = mk_eq_empty(s); - add_axiom(cnt, mk_eq(i, minus_one, false)); - add_axiom(~s_eq_empty, mk_eq(i, zero, false)); - add_axiom(s_eq_empty, ~mk_eq_empty(t), mk_eq(i, minus_one, false)); add_axiom(~cnt, s_eq_empty, mk_seq_eq(t, xsy)); add_axiom(~cnt, s_eq_empty, mk_eq(i, lenx, false)); tightest_prefix(s, x); @@ -3024,10 +3023,13 @@ void theory_seq::add_indexof_axiom(expr* i) { add_axiom(~offset_ge_0, offset_ge_len, mk_seq_eq(t, mk_concat(x, y))); add_axiom(~offset_ge_0, offset_ge_len, mk_eq(m_util.str.mk_length(x), offset, false)); add_axiom(~offset_ge_0, offset_ge_len, - ~mk_eq(indexof0, minus_one, false), mk_eq(i, minus_one, false)); + ~mk_eq(indexof0, minus_one, false), i_eq_m1); add_axiom(~offset_ge_0, offset_ge_len, ~mk_literal(m_autil.mk_ge(indexof0, zero)), mk_eq(offset_p_indexof0, i, false)); + + // offset < 0 => -1 = i + add_axiom(offset_ge_0, i_eq_m1); } } From 7386e2f3e942b025d8266323dc299055a7dd1efa Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 25 Jan 2017 18:29:30 -0800 Subject: [PATCH 07/11] add warning for scearios of #876 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index cdea02c48..3e1436aa6 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -3819,6 +3819,15 @@ void theory_seq::new_eq_eh(dependency* deps, enode* n1, enode* n2) { solve_eqs(m_eqs.size()-1); enforce_length_coherence(n1, n2); } + else if (n1 != n2 && m_util.is_re(n1->get_owner())) { + warning_msg("equality between regular expressions is not yet supported"); + eautomaton* a1 = get_automaton(n1->get_owner()); + eautomaton* a2 = get_automaton(n2->get_owner()); + // eautomaton* b1 = mk_difference(*a1, *a2); + // eautomaton* b2 = mk_difference(*a2, *a1); + // eautomaton* c = mk_union(*b1, *b2); + // then some emptiness check. + } } void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) { From a0a81fc2d7c46283c2a37b3ffdf923701a3484dd Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 26 Jan 2017 08:37:37 -0800 Subject: [PATCH 08/11] add format #879 Signed-off-by: Nikolaj Bjorner --- scripts/update_api.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index 031b39c75..38b6213c1 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -942,7 +942,7 @@ def def_API(name, result, params): log_c.write(" Au(a%s);\n" % sz) exe_c.write("in.get_int_array(%s)" % i) else: - error ("unsupported parameter for %s, %s" % (ty, name, p)) + error ("unsupported parameter for %s, %s, %s" % (ty, name, p)) elif kind == OUT_ARRAY: sz = param_array_capacity_pos(p) sz_p = params[sz] From 962979b09c991fc47a02e10afb07d68a353308ff Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 26 Jan 2017 13:28:40 -0800 Subject: [PATCH 09/11] rework sat.mus to use restart count for bounded minimization Signed-off-by: Nikolaj Bjorner --- src/sat/sat_mus.cpp | 59 +++++++++++++++++--------------------------- src/sat/sat_mus.h | 3 +-- src/sat/sat_solver.h | 1 + 3 files changed, 24 insertions(+), 39 deletions(-) diff --git a/src/sat/sat_mus.cpp b/src/sat/sat_mus.cpp index 380b8ee94..06851d10d 100644 --- a/src/sat/sat_mus.cpp +++ b/src/sat/sat_mus.cpp @@ -23,7 +23,7 @@ Notes: namespace sat { - mus::mus(solver& s):s(s), m_is_active(false),m_restart(0), m_max_restarts(0) {} + mus::mus(solver& s):s(s), m_is_active(false), m_max_num_restarts(UINT_MAX) {} mus::~mus() {} @@ -31,8 +31,6 @@ namespace sat { m_core.reset(); m_mus.reset(); m_model.reset(); - m_max_restarts = (s.m_stats.m_restart - m_restart) + 10; - m_restart = s.m_stats.m_restart; } void mus::set_core() { @@ -49,12 +47,12 @@ namespace sat { } lbool mus::operator()() { + m_max_num_restarts = s.m_config.m_core_minimize_partial ? s.num_restarts() + 10 : UINT_MAX; flet _disable_min(s.m_config.m_core_minimize, false); flet _is_active(m_is_active, true); - IF_VERBOSE(3, verbose_stream() << "(sat.mus " << s.get_core() << ")\n";); + IF_VERBOSE(3, verbose_stream() << "(sat.mus size: " << s.get_core().size() << " core: [" << s.get_core() << "])\n";); reset(); lbool r = mus1(); - m_restart = s.m_stats.m_restart; return r; } @@ -63,13 +61,13 @@ namespace sat { TRACE("sat", tout << "old core: " << s.get_core() << "\n";); literal_vector& core = get_core(); literal_vector& mus = m_mus; - if (core.size() > 64) { + if (!minimize_partial && core.size() > 64) { return mus2(); } - unsigned delta_time = 0; - unsigned core_miss = 0; while (!core.empty()) { - IF_VERBOSE(3, verbose_stream() << "(opt.mus reducing core: " << core.size() << " mus: " << mus.size() << ")\n";); + IF_VERBOSE(1, verbose_stream() << "(sat.mus num-to-process: " << core.size() << " mus: " << mus.size(); + if (minimize_partial) verbose_stream() << " max-restarts: " << m_max_num_restarts; + verbose_stream() << ")\n";); TRACE("sat", tout << "core: " << core << "\n"; tout << "mus: " << mus << "\n";); @@ -78,34 +76,35 @@ namespace sat { set_core(); return l_undef; } - if (minimize_partial && 3*delta_time > core.size() && core.size() < mus.size()) { - break; - } unsigned num_literals = core.size() + mus.size(); if (num_literals <= 2) { // IF_VERBOSE(0, verbose_stream() << "num literals: " << core << " " << mus << "\n";); break; } - if (s.m_config.m_core_minimize_partial && s.m_stats.m_restart - m_restart > m_max_restarts) { - IF_VERBOSE(1, verbose_stream() << "(sat restart budget exceeded)\n";); - set_core(); - return l_true; - } literal lit = core.back(); core.pop_back(); lbool is_sat; { + flet _restart_bound(s.m_config.m_restart_max, m_max_num_restarts); scoped_append _sa(mus, core); mus.push_back(~lit); is_sat = s.check(mus.size(), mus.c_ptr()); TRACE("sat", tout << "mus: " << mus << "\n";); } + IF_VERBOSE(1, verbose_stream() << "(sat.mus " << is_sat << ")\n";); switch (is_sat) { case l_undef: - core.push_back(lit); - set_core(); - return l_undef; + if (!s.canceled()) { + // treat restart max as sat, so literal is in the mus + mus.push_back(lit); + } + else { + core.push_back(lit); + set_core(); + return l_undef; + } + break; case l_true: { SASSERT(value_at(lit, s.get_model()) == l_false); mus.push_back(lit); @@ -115,11 +114,9 @@ namespace sat { case l_false: literal_vector const& new_core = s.get_core(); if (new_core.contains(~lit)) { - IF_VERBOSE(3, verbose_stream() << "miss core " << lit << "\n";); - ++core_miss; + IF_VERBOSE(3, verbose_stream() << "(sat.mus unit reduction, literal is in both cores " << lit << ")\n";); } else { - core_miss = 0; TRACE("sat", tout << "core: " << new_core << " mus: " << mus << "\n";); core.reset(); for (unsigned i = 0; i < new_core.size(); ++i) { @@ -131,14 +128,6 @@ namespace sat { } break; } - - unsigned new_num_literals = core.size() + mus.size(); - if (new_num_literals == num_literals) { - delta_time++; - } - else { - delta_time = 0; - } } set_core(); IF_VERBOSE(3, verbose_stream() << "(sat.mus.new " << s.m_core << ")\n";); @@ -159,13 +148,9 @@ namespace sat { lbool mus::qx(literal_set& assignment, literal_set& support, bool has_support) { lbool is_sat = l_true; - if (s.m_config.m_core_minimize_partial && s.m_stats.m_restart - m_restart > m_max_restarts) { - IF_VERBOSE(1, verbose_stream() << "(sat restart budget exceeded)\n";); - return l_true; - } if (has_support) { scoped_append _sa(m_mus, support.to_vector()); - is_sat = s.check(m_mus.size(), m_mus.c_ptr()); + is_sat = s.check(m_mus.size(), m_mus.c_ptr()); switch (is_sat) { case l_false: { literal_set core(s.get_core()); @@ -173,7 +158,7 @@ namespace sat { assignment.reset(); return l_true; } - case l_undef: + case l_undef: return l_undef; case l_true: update_model(); diff --git a/src/sat/sat_mus.h b/src/sat/sat_mus.h index 74f6d75f0..946f66ed6 100644 --- a/src/sat/sat_mus.h +++ b/src/sat/sat_mus.h @@ -26,8 +26,7 @@ namespace sat { literal_vector m_mus; bool m_is_active; model m_model; // model obtained during minimal unsat core - unsigned m_restart; - unsigned m_max_restarts; + unsigned m_max_num_restarts; public: diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index dcf7e2acb..aa7e6edea 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -209,6 +209,7 @@ namespace sat { bool inconsistent() const { return m_inconsistent; } unsigned num_vars() const { return m_level.size(); } unsigned num_clauses() const; + unsigned num_restarts() const { return m_restarts; } bool is_external(bool_var v) const { return m_external[v] != 0; } bool was_eliminated(bool_var v) const { return m_eliminated[v] != 0; } unsigned scope_lvl() const { return m_scope_lvl; } From b70f1f0319a0d7f607f3f752e21a4957ee020645 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 27 Jan 2017 09:47:18 -0800 Subject: [PATCH 10/11] fix overflow exposed in #880 Signed-off-by: Nikolaj Bjorner --- src/smt/smt_solver.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index ab6be5d91..59a5ddf8f 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -122,7 +122,8 @@ namespace smt { SASSERT(n <= lvl); unsigned new_lvl = lvl - n; unsigned old_sz = m_scopes[new_lvl]; - for (unsigned i = cur_sz - 1; i >= old_sz; i--) { + for (unsigned i = cur_sz; i > old_sz; ) { + --i; expr * key = m_assumptions[i].get(); SASSERT(m_name2assertion.contains(key)); expr * value = m_name2assertion.find(key); From 37ee4c95c3a2d963002fab22b0f698191d0e92d8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 30 Jan 2017 02:09:08 -0800 Subject: [PATCH 11/11] adding parallel threads Signed-off-by: Nikolaj Bjorner --- contrib/cmake/src/sat/CMakeLists.txt | 1 + src/api/c++/z3++.h | 1 + src/sat/sat_config.cpp | 1 + src/sat/sat_config.h | 1 + src/sat/sat_par.cpp | 45 ++++++++ src/sat/sat_par.h | 39 +++++++ src/sat/sat_params.pyg | 1 + src/sat/sat_solver.cpp | 146 ++++++++++++++++++++++++-- src/sat/sat_solver.h | 10 ++ src/sat/sat_solver/inc_sat_solver.cpp | 3 + src/smt/theory_seq.cpp | 4 +- src/tactic/tactical.cpp | 7 -- src/util/rlimit.h | 9 ++ 13 files changed, 250 insertions(+), 18 deletions(-) create mode 100644 src/sat/sat_par.cpp create mode 100644 src/sat/sat_par.h diff --git a/contrib/cmake/src/sat/CMakeLists.txt b/contrib/cmake/src/sat/CMakeLists.txt index 3eec21ec3..d88a73708 100644 --- a/contrib/cmake/src/sat/CMakeLists.txt +++ b/contrib/cmake/src/sat/CMakeLists.txt @@ -12,6 +12,7 @@ z3_add_component(sat sat_integrity_checker.cpp sat_model_converter.cpp sat_mus.cpp + sat_par.cpp sat_probing.cpp sat_scc.cpp sat_simplifier.cpp diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 1556064d6..979d9aed7 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -1816,6 +1816,7 @@ namespace z3 { fmls, fml)); } + param_descrs get_param_descrs() { return param_descrs(ctx(), Z3_solver_get_param_descrs(ctx(), m_solver)); } }; diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index 4e01bfe55..ccf538dfe 100644 --- a/src/sat/sat_config.cpp +++ b/src/sat/sat_config.cpp @@ -77,6 +77,7 @@ namespace sat { m_burst_search = p.burst_search(); m_max_conflicts = p.max_conflicts(); + m_num_parallel = p.parallel_threads(); // These parameters are not exposed m_simplify_mult1 = _p.get_uint("simplify_mult1", 300); diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h index 910ca0360..405cbd092 100644 --- a/src/sat/sat_config.h +++ b/src/sat/sat_config.h @@ -57,6 +57,7 @@ namespace sat { unsigned m_random_seed; unsigned m_burst_search; unsigned m_max_conflicts; + unsigned m_num_parallel; unsigned m_simplify_mult1; double m_simplify_mult2; diff --git a/src/sat/sat_par.cpp b/src/sat/sat_par.cpp new file mode 100644 index 000000000..7a185a3b5 --- /dev/null +++ b/src/sat/sat_par.cpp @@ -0,0 +1,45 @@ +/*++ +Copyright (c) 2017 Microsoft Corporation + +Module Name: + + sat_par.cpp + +Abstract: + + Utilities for parallel SAT solving. + +Author: + + Nikolaj Bjorner (nbjorner) 2017-1-29. + +Revision History: + +--*/ +#include "sat_par.h" + + +namespace sat { + + par::par() {} + + void par::exchange(literal_vector const& in, unsigned& limit, literal_vector& out) { + #pragma omp critical (par_solver) + { + if (limit < m_units.size()) { + // this might repeat some literals. + out.append(m_units.size() - limit, m_units.c_ptr() + limit); + } + for (unsigned i = 0; i < in.size(); ++i) { + literal lit = in[i]; + if (!m_unit_set.contains(lit.index())) { + m_unit_set.insert(lit.index()); + m_units.push_back(lit); + } + } + limit = m_units.size(); + } + } + +}; + diff --git a/src/sat/sat_par.h b/src/sat/sat_par.h new file mode 100644 index 000000000..2b2592de7 --- /dev/null +++ b/src/sat/sat_par.h @@ -0,0 +1,39 @@ +/*++ +Copyright (c) 2017 Microsoft Corporation + +Module Name: + + sat_par.h + +Abstract: + + Utilities for parallel SAT solving. + +Author: + + Nikolaj Bjorner (nbjorner) 2017-1-29. + +Revision History: + +--*/ +#ifndef SAT_PAR_H_ +#define SAT_PAR_H_ + +#include"sat_types.h" +#include"hashtable.h" +#include"map.h" + +namespace sat { + + class par { + typedef hashtable index_set; + literal_vector m_units; + index_set m_unit_set; + public: + par(); + void exchange(literal_vector const& in, unsigned& limit, literal_vector& out); + }; + +}; + +#endif diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index 21a50bea2..60708fd5c 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -22,4 +22,5 @@ def_module_params('sat', ('dyn_sub_res', BOOL, True, 'dynamic subsumption resolution for minimizing learned clauses'), ('core.minimize', BOOL, False, 'minimize computed core'), ('core.minimize_partial', BOOL, False, 'apply partial (cheap) core minimization'), + ('parallel_threads', UINT, 1, 'number of parallel threads to use'), ('dimacs.core', BOOL, False, 'extract core from DIMACS benchmarks'))) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 37fb971fd..bf3dc1988 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -35,6 +35,7 @@ namespace sat { m_rlimit(l), m_config(p), m_ext(ext), + m_par(0), m_cleaner(*this), m_simplifier(*this, p), m_scc(*this, p), @@ -72,6 +73,8 @@ namespace sat { void solver::copy(solver const & src) { SASSERT(m_mc.empty() && src.m_mc.empty()); + SASSERT(scope_lvl() == 0); + SASSERT(src.scope_lvl() == 0); // create new vars if (num_vars() < src.num_vars()) { for (bool_var v = num_vars(); v < src.num_vars(); v++) { @@ -81,19 +84,25 @@ namespace sat { VERIFY(v == mk_var(ext, dvar)); } } + unsigned sz = src.scope_lvl() == 0 ? src.m_trail.size() : src.m_scopes[0].m_trail_lim; + for (unsigned i = 0; i < sz; ++i) { + assign(src.m_trail[i], justification()); + } + { // copy binary clauses - vector::const_iterator it = src.m_watches.begin(); - vector::const_iterator end = src.m_watches.begin(); - for (unsigned l_idx = 0; it != end; ++it, ++l_idx) { - watch_list const & wlist = *it; + unsigned sz = src.m_watches.size(); + for (unsigned l_idx = 0; l_idx < sz; ++l_idx) { literal l = ~to_literal(l_idx); - watch_list::const_iterator it2 = wlist.begin(); - watch_list::const_iterator end2 = wlist.end(); - for (; it2 != end2; ++it2) { - if (!it2->is_binary_non_learned_clause()) + watch_list const & wlist = src.m_watches[l_idx]; + watch_list::const_iterator it = wlist.begin(); + watch_list::const_iterator end = wlist.end(); + for (; it != end; ++it) { + if (!it->is_binary_non_learned_clause()) + continue; + literal l2 = it->get_literal(); + if (l.index() > l2.index()) continue; - literal l2 = it2->get_literal(); mk_clause_core(l, l2); } } @@ -711,6 +720,9 @@ namespace sat { pop_to_base_level(); IF_VERBOSE(2, verbose_stream() << "(sat.sat-solver)\n";); SASSERT(scope_lvl() == 0); + if (m_config.m_num_parallel > 0 && !m_par) { + return check_par(num_lits, lits); + } #ifdef CLONE_BEFORE_SOLVING if (m_mc.empty()) { m_clone = alloc(solver, m_params, 0 /* do not clone extension */); @@ -759,6 +771,7 @@ namespace sat { restart(); simplify_problem(); + exchange_par(); if (check_inconsistent()) return l_false; gc(); @@ -774,6 +787,121 @@ namespace sat { } } + enum par_exception_kind { + DEFAULT_EX, + ERROR_EX + }; + + lbool solver::check_par(unsigned num_lits, literal const* lits) { + int num_threads = static_cast(m_config.m_num_parallel); + scoped_limits scoped_rlimit(rlimit()); + vector rlims(num_threads); + ptr_vector solvers(num_threads); + sat::par par; + for (int i = 0; i < num_threads; ++i) { + m_params.set_uint("random_seed", i); + solvers[i] = alloc(sat::solver, m_params, rlims[i], 0); + solvers[i]->copy(*this); + solvers[i]->set_par(&par); + scoped_rlimit.push_child(&solvers[i]->rlimit()); + } + int finished_id = -1; + std::string ex_msg; + par_exception_kind ex_kind; + unsigned error_code = 0; + lbool result = l_undef; + #pragma omp parallel for + for (int i = 0; i < num_threads; ++i) { + try { + lbool r = solvers[i]->check(num_lits, lits); + bool first = false; + #pragma omp critical (par_solver) + { + if (finished_id == UINT_MAX) { + finished_id = i; + first = true; + result = r; + } + } + if (first) { + if (r == l_true) { + set_model(solvers[i]->get_model()); + } + else if (r == l_false) { + m_core.reset(); + m_core.append(solvers[i]->get_core()); + } + for (int j = 0; j < num_threads; ++j) { + if (i != j) { + rlims[j].cancel(); + } + } + } + } + catch (z3_error & err) { + if (i == 0) { + error_code = err.error_code(); + ex_kind = ERROR_EX; + } + } + catch (z3_exception & ex) { + if (i == 0) { + ex_msg = ex.msg(); + ex_kind = DEFAULT_EX; + } + } + } + for (int i = 0; i < num_threads; ++i) { + dealloc(solvers[i]); + } + if (finished_id == -1) { + switch (ex_kind) { + case ERROR_EX: throw z3_error(error_code); + default: throw default_exception(ex_msg.c_str()); + } + } + return result; + + } + + /* + \brief import lemmas/units from parallel sat solvers. + */ + void solver::exchange_par() { + if (m_par && scope_lvl() == 0) { + unsigned num_in = 0, num_out = 0; + SASSERT(scope_lvl() == 0); // parallel with assumptions is TBD + literal_vector in, out; + for (unsigned i = m_par_limit_out; i < m_trail.size(); ++i) { + literal lit = m_trail[i]; + if (lit.var() < m_par_num_vars) { + ++num_out; + out.push_back(lit); + } + } + m_par_limit_out = m_trail.size(); + m_par->exchange(out, m_par_limit_in, in); + for (unsigned i = 0; !inconsistent() && i < in.size(); ++i) { + literal lit = in[i]; + SASSERT(lit.var() < m_par_num_vars); + if (lvl(lit.var()) != 0 || value(lit) != l_true) { + ++num_in; + assign(lit, justification()); + } + } + if (num_in > 0 || num_out > 0) { + IF_VERBOSE(1, verbose_stream() << "(sat-sync out: " << num_out << " in: " << num_in << ")\n";); + } + } + } + + void solver::set_par(par* p) { + m_par = p; + m_par_num_vars = num_vars(); + m_par_limit_in = 0; + m_par_limit_out = 0; + } + bool_var solver::next_var() { bool_var next; diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index aa7e6edea..54b8a9bb2 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -33,6 +33,7 @@ Revision History: #include"sat_iff3_finder.h" #include"sat_probing.h" #include"sat_mus.h" +#include"sat_par.h" #include"params.h" #include"statistics.h" #include"stopwatch.h" @@ -74,6 +75,7 @@ namespace sat { config m_config; stats m_stats; extension * m_ext; + par* m_par; random_gen m_rand; clause_allocator m_cls_allocator; cleaner m_cleaner; @@ -128,6 +130,10 @@ namespace sat { literal_set m_assumption_set; // set of enabled assumptions literal_vector m_core; // unsat core + unsigned m_par_limit_in; + unsigned m_par_limit_out; + unsigned m_par_num_vars; + void del_clauses(clause * const * begin, clause * const * end); friend class integrity_checker; @@ -241,7 +247,9 @@ namespace sat { m_num_checkpoints = 0; if (memory::get_allocation_size() > m_config.m_max_memory) throw solver_exception(Z3_MAX_MEMORY_MSG); } + void set_par(par* p); bool canceled() { return !m_rlimit.inc(); } + config const& get_config() { return m_config; } typedef std::pair bin_clause; protected: watch_list & get_wlist(literal l) { return m_watches[l.index()]; } @@ -317,6 +325,8 @@ namespace sat { bool check_model(model const & m) const; void restart(); void sort_watch_lits(); + void exchange_par(); + lbool check_par(unsigned num_lits, literal const* lits); // ----------------------- // diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 33d10f428..65a7b021c 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -140,6 +140,7 @@ public: if (r != l_true) return r; r = m_solver.check(m_asms.size(), m_asms.c_ptr()); + switch (r) { case l_true: if (sz > 0) { @@ -276,6 +277,8 @@ public: return r; } + + virtual lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes) { sat::literal_vector ls; u_map lit2var; diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 3e1436aa6..d5251c56b 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -2940,8 +2940,8 @@ void theory_seq::deque_axiom(expr* n) { encode that s is not contained in of xs1 where s1 is all of s, except the last element. - lit or s = "" or s = s1*(unit c) - lit or s = "" or !contains(x*s1, s) + s = "" or s = s1*(unit c) + s = "" or !contains(x*s1, s) */ void theory_seq::tightest_prefix(expr* s, expr* x) { expr_ref s1 = mk_first(s); diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp index 4cb212265..33f8325fb 100644 --- a/src/tactic/tactical.cpp +++ b/src/tactic/tactical.cpp @@ -461,13 +461,6 @@ enum par_exception_kind { class par_tactical : public or_else_tactical { - struct scoped_limits { - reslimit& m_limit; - unsigned m_sz; - scoped_limits(reslimit& lim): m_limit(lim), m_sz(0) {} - ~scoped_limits() { for (unsigned i = 0; i < m_sz; ++i) m_limit.pop_child(); } - void push_child(reslimit* lim) { m_limit.push_child(lim); ++m_sz; } - }; public: par_tactical(unsigned num, tactic * const * ts):or_else_tactical(num, ts) {} diff --git a/src/util/rlimit.h b/src/util/rlimit.h index 913984768..283d7613d 100644 --- a/src/util/rlimit.h +++ b/src/util/rlimit.h @@ -61,4 +61,13 @@ public: }; +struct scoped_limits { + reslimit& m_limit; + unsigned m_sz; + scoped_limits(reslimit& lim): m_limit(lim), m_sz(0) {} + ~scoped_limits() { for (unsigned i = 0; i < m_sz; ++i) m_limit.pop_child(); } + void push_child(reslimit* lim) { m_limit.push_child(lim); ++m_sz; } +}; + + #endif