From adf8072eaacea187a60ff3690a6b0aaa12b586af Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 21 Jan 2017 12:28:37 +0000 Subject: [PATCH 1/4] 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 2/4] 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 3/4] 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 4/4] 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);