From 5be4365b47fe518ddbe3583ce8c3449567c4ab7d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 15 Sep 2013 16:53:52 -0700 Subject: [PATCH 01/27] redo edit Signed-off-by: Nikolaj Bjorner --- src/smt/proto_model/value_factory.h | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/smt/proto_model/value_factory.h b/src/smt/proto_model/value_factory.h index 5bd0a1f75..92ad2373b 100644 --- a/src/smt/proto_model/value_factory.h +++ b/src/smt/proto_model/value_factory.h @@ -189,11 +189,12 @@ public: max_size = Number(usz); has_max = true; } + Number start = set->m_next; Number & next = set->m_next; while (!is_new) { result = mk_value(next, s, is_new); next++; - if (has_max && next > max_size + set->m_next) { + if (has_max && next > max_size + start) { return 0; } } From 8a44766382df18b1a8610d7dd54b47f9b85b56e6 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 18 Sep 2013 13:47:20 +0100 Subject: [PATCH 02/27] qfbv-sls tactic bugfix Signed-off-by: Christoph M. Wintersteiger --- src/tactic/sls/sls_tactic.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp index 69e1c8bc3..eb806e23c 100644 --- a/src/tactic/sls/sls_tactic.cpp +++ b/src/tactic/sls/sls_tactic.cpp @@ -1343,6 +1343,7 @@ class sls_tactic : public tactic { m_zero(m_mpz_manager.mk_z(0)), m_one(m_mpz_manager.mk_z(1)), m_two(m_mpz_manager.mk_z(2)), + m_cancel(false), m_bv_util(m), m_tracker(m, m_bv_util, m_mpz_manager, m_powers) { From 4be468d312aa166fe15d7579639ee6d2dc31cf50 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 19 Sep 2013 16:18:23 +0100 Subject: [PATCH 03/27] Reorganized the SLS code. Signed-off-by: Christoph M. Wintersteiger --- src/tactic/sls/sls_evaluator.h | 620 +++++++++++++++ src/tactic/sls/sls_params.pyg | 8 + src/tactic/sls/sls_powers.h | 49 ++ src/tactic/sls/sls_tactic.cpp | 1303 +------------------------------- src/tactic/sls/sls_tracker.h | 675 +++++++++++++++++ 5 files changed, 1374 insertions(+), 1281 deletions(-) create mode 100644 src/tactic/sls/sls_evaluator.h create mode 100644 src/tactic/sls/sls_params.pyg create mode 100644 src/tactic/sls/sls_powers.h create mode 100644 src/tactic/sls/sls_tracker.h diff --git a/src/tactic/sls/sls_evaluator.h b/src/tactic/sls/sls_evaluator.h new file mode 100644 index 000000000..77ff50454 --- /dev/null +++ b/src/tactic/sls/sls_evaluator.h @@ -0,0 +1,620 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + sls_evaluator.h + +Abstract: + + SLS Evaluator + +Author: + + Christoph (cwinter) 2012-02-29 + +Notes: + +--*/ + +#ifndef _SLS_EVALUATOR_H_ +#define _SLS_EVALUATOR_H_ + +#include"sls_powers.h" +#include"sls_tracker.h" + +class sls_evaluator { + ast_manager & m_manager; + bv_util & m_bv_util; + family_id m_basic_fid; + family_id m_bv_fid; + sls_tracker & m_tracker; + unsynch_mpz_manager & m_mpz_manager; + mpz m_zero, m_one, m_two; + powers & m_powers; + expr_ref_buffer m_temp_exprs; + vector > m_traversal_stack; + +public: + sls_evaluator(ast_manager & m, bv_util & bvu, sls_tracker & t, unsynch_mpz_manager & mm, powers & p) : + m_manager(m), + m_bv_util(bvu), + m_tracker(t), + m_mpz_manager(mm), + m_zero(m_mpz_manager.mk_z(0)), + m_one(m_mpz_manager.mk_z(1)), + m_two(m_mpz_manager.mk_z(2)), + m_powers(p), + m_temp_exprs(m) { + m_bv_fid = m_bv_util.get_family_id(); + m_basic_fid = m_manager.get_basic_family_id(); + } + + ~sls_evaluator() { + m_mpz_manager.del(m_zero); + m_mpz_manager.del(m_one); + m_mpz_manager.del(m_two); + } + + void operator()(app * n, mpz & result) { + family_id nfid = n->get_family_id(); + func_decl * fd = n->get_decl(); + unsigned n_args = n->get_num_args(); + + if (n_args == 0) { + m_mpz_manager.set(result, m_tracker.get_value(n)); + return; + } + + expr * const * args = n->get_args(); + + m_mpz_manager.set(result, m_zero); + + if (nfid == m_basic_fid) { + switch (n->get_decl_kind()) { + case OP_AND: { + m_mpz_manager.set(result, m_one); + for (unsigned i = 0; i < n_args; i++) + if (m_mpz_manager.neq(m_tracker.get_value(args[i]), result)) { + m_mpz_manager.set(result, m_zero); + break; + } + break; + } + case OP_OR: { + for (unsigned i = 0; i < n_args; i++) + if (m_mpz_manager.neq(m_tracker.get_value(args[i]), result)) { + m_mpz_manager.set(result, m_one); + break; + } + break; + } + case OP_NOT: { + SASSERT(n_args == 1); + const mpz & child = m_tracker.get_value(args[0]); + SASSERT(m_mpz_manager.is_one(child) || m_mpz_manager.is_zero(child)); + m_mpz_manager.set(result, (m_mpz_manager.is_zero(child)) ? m_one : m_zero); + break; + } + case OP_EQ: { + SASSERT(n_args >= 2); + m_mpz_manager.set(result, m_one); + const mpz & first = m_tracker.get_value(args[0]); + for (unsigned i = 1; i < n_args; i++) + if (m_mpz_manager.neq(m_tracker.get_value(args[i]), first)) { + m_mpz_manager.set(result, m_zero); + break; + } + break; + } + case OP_DISTINCT: { + m_mpz_manager.set(result, m_one); + for (unsigned i = 0; i < n_args && m_mpz_manager.is_one(result); i++) { + for (unsigned j = i+1; j < n_args && m_mpz_manager.is_one(result); j++) { + if (m_mpz_manager.eq(m_tracker.get_value(args[i]), m_tracker.get_value(args[j]))) + m_mpz_manager.set(result, m_zero); + } + } + break; + } + default: + NOT_IMPLEMENTED_YET(); + } + } + else if (nfid == m_bv_fid) { + bv_op_kind k = static_cast(fd->get_decl_kind()); + switch(k) { + case OP_CONCAT: { + SASSERT(n_args >= 2); + for (unsigned i = 0; i < n_args; i++) { + if (i != 0) { + const mpz & p = m_powers(m_bv_util.get_bv_size(args[i])); + m_mpz_manager.mul(result, p, result); + } + m_mpz_manager.add(result, m_tracker.get_value(args[i]), result); + } + break; + } + case OP_EXTRACT: { + SASSERT(n_args == 1); + const mpz & child = m_tracker.get_value(args[0]); + unsigned h = m_bv_util.get_extract_high(n); + unsigned l = m_bv_util.get_extract_low(n); + + m_mpz_manager.rem(child, m_powers(h+1), result); // result = [h:0] of child + m_mpz_manager.machine_div2k(result, l, result); + break; + } + case OP_BADD: { + SASSERT(n_args >= 2); + for (unsigned i = 0; i < n_args; i++) { + const mpz & next = m_tracker.get_value(args[i]); + m_mpz_manager.add(result, next, result); + } + const mpz & p = m_powers(m_bv_util.get_bv_size(n)); + m_mpz_manager.rem(result, p, result); + break; + } + case OP_BSUB: { + SASSERT(n_args == 2); + const mpz & p = m_powers(m_bv_util.get_bv_size(n)); + mpz temp; + m_mpz_manager.sub(m_tracker.get_value(args[0]), m_tracker.get_value(args[1]), temp); + m_mpz_manager.mod(temp, p, result); + m_mpz_manager.del(temp); + break; + } + case OP_BMUL: { + SASSERT(n_args >= 2); + m_mpz_manager.set(result, m_tracker.get_value(args[0])); + for (unsigned i = 1; i < n_args; i++) { + const mpz & next = m_tracker.get_value(args[i]); + m_mpz_manager.mul(result, next, result); + } + const mpz & p = m_powers(m_bv_util.get_bv_size(n)); + m_mpz_manager.rem(result, p, result); + break; + } + case OP_BNEG: { // 2's complement unary minus + SASSERT(n_args == 1); + const mpz & child = m_tracker.get_value(args[0]); + if (m_mpz_manager.is_zero(child)) { + m_mpz_manager.set(result, m_zero); + } + else { + unsigned bv_sz = m_bv_util.get_bv_size(n); + m_mpz_manager.bitwise_not(bv_sz, child, result); + m_mpz_manager.inc(result); // can't overflow + } + break; + } + case OP_BSDIV: + case OP_BSDIV0: + case OP_BSDIV_I: { + SASSERT(n_args == 2); + mpz x; m_mpz_manager.set(x, m_tracker.get_value(args[0])); + mpz y; m_mpz_manager.set(y, m_tracker.get_value(args[1])); + SASSERT(m_mpz_manager.is_nonneg(x) && m_mpz_manager.is_nonneg(y)); + unsigned bv_sz = m_bv_util.get_bv_size(args[0]); + const mpz & p = m_powers(bv_sz); + const mpz & p_half = m_powers(bv_sz-1); + if (x >= p_half) { m_mpz_manager.sub(x, p, x); } + if (y >= p_half) { m_mpz_manager.sub(y, p, y); } + + if (m_mpz_manager.is_zero(y)) { + if (m_mpz_manager.is_neg(x)) + m_mpz_manager.set(result, m_one); + else { + m_mpz_manager.set(result, m_powers(m_bv_util.get_bv_size(n))); + m_mpz_manager.dec(result); + } + } + else { + m_mpz_manager.machine_div(x, y, result); + } + if (m_mpz_manager.is_neg(result)) + m_mpz_manager.add(result, p, result); + m_mpz_manager.del(x); + m_mpz_manager.del(y); + break; + } + case OP_BUDIV: + case OP_BUDIV0: + case OP_BUDIV_I: { + SASSERT(n_args == 2); + mpz x; m_mpz_manager.set(x, m_tracker.get_value(args[0])); + mpz y; m_mpz_manager.set(y, m_tracker.get_value(args[1])); + + if (m_mpz_manager.is_zero(y)) { + m_mpz_manager.set(result, m_powers(m_bv_util.get_bv_size(n))); + m_mpz_manager.dec(result); + } + else { + m_mpz_manager.machine_div(x, y, result); + } + m_mpz_manager.del(x); + m_mpz_manager.del(y); + break; + } + case OP_BSREM: + case OP_BSREM0: + case OP_BSREM_I: { + SASSERT(n_args == 2); + mpz x; m_mpz_manager.set(x, m_tracker.get_value(args[0])); + mpz y; m_mpz_manager.set(y, m_tracker.get_value(args[1])); + unsigned bv_sz = m_bv_util.get_bv_size(args[0]); + const mpz & p = m_powers(bv_sz); + const mpz & p_half = m_powers(bv_sz-1); + if (x >= p_half) { m_mpz_manager.sub(x, p, x); } + if (y >= p_half) { m_mpz_manager.sub(y, p, y); } + + if (m_mpz_manager.is_zero(y)) { + m_mpz_manager.set(result, x); + } + else { + m_mpz_manager.rem(x, y, result); + } + if (m_mpz_manager.is_neg(result)) + m_mpz_manager.add(result, p, result); + m_mpz_manager.del(x); + m_mpz_manager.del(y); + break; + } + case OP_BUREM: + case OP_BUREM0: + case OP_BUREM_I: { + SASSERT(n_args == 2); + mpz x; m_mpz_manager.set(x, m_tracker.get_value(args[0])); + mpz y; m_mpz_manager.set(y, m_tracker.get_value(args[1])); + + if (m_mpz_manager.is_zero(y)) { + m_mpz_manager.set(result, x); + } + else { + m_mpz_manager.mod(x, y, result); + } + m_mpz_manager.del(x); + m_mpz_manager.del(y); + break; + } + case OP_BSMOD: + case OP_BSMOD0: + case OP_BSMOD_I:{ + SASSERT(n_args == 2); + mpz x; m_mpz_manager.set(x, m_tracker.get_value(args[0])); + mpz y; m_mpz_manager.set(y, m_tracker.get_value(args[1])); + unsigned bv_sz = m_bv_util.get_bv_size(args[0]); + const mpz & p = m_powers(bv_sz); + const mpz & p_half = m_powers(bv_sz-1); + if (x >= p_half) { m_mpz_manager.sub(x, p, x); } + if (y >= p_half) { m_mpz_manager.sub(y, p, y); } + + if (m_mpz_manager.is_zero(y)) + m_mpz_manager.set(result, x); + else { + bool neg_x = m_mpz_manager.is_neg(x); + bool neg_y = m_mpz_manager.is_neg(y); + mpz abs_x, abs_y; + m_mpz_manager.set(abs_x, x); + m_mpz_manager.set(abs_y, y); + if (neg_x) m_mpz_manager.neg(abs_x); + if (neg_y) m_mpz_manager.neg(abs_y); + SASSERT(m_mpz_manager.is_nonneg(abs_x) && m_mpz_manager.is_nonneg(abs_y)); + + m_mpz_manager.mod(abs_x, abs_y, result); + + if (m_mpz_manager.is_zero(result) || (!neg_x && !neg_y)) { + /* Nothing */ + } + else if (neg_x && !neg_y) { + m_mpz_manager.neg(result); + m_mpz_manager.add(result, y, result); + } + else if (!neg_x && neg_y) { + m_mpz_manager.add(result, y, result); + } + else { + m_mpz_manager.neg(result); + } + + m_mpz_manager.del(abs_x); + m_mpz_manager.del(abs_y); + } + + if (m_mpz_manager.is_neg(result)) + m_mpz_manager.add(result, p, result); + + m_mpz_manager.del(x); + m_mpz_manager.del(y); + break; + } + case OP_BAND: { + SASSERT(n_args >= 2); + m_mpz_manager.set(result, m_tracker.get_value(args[0])); + for (unsigned i = 1; i < n_args; i++) + m_mpz_manager.bitwise_and(result, m_tracker.get_value(args[i]), result); + break; + } + case OP_BOR: { + SASSERT(n_args >= 2); + m_mpz_manager.set(result, m_tracker.get_value(args[0])); + for (unsigned i = 1; i < n_args; i++) { + m_mpz_manager.bitwise_or(result, m_tracker.get_value(args[i]), result); + } + break; + } + case OP_BXOR: { + SASSERT(n_args >= 2); + m_mpz_manager.set(result, m_tracker.get_value(args[0])); + for (unsigned i = 1; i < n_args; i++) + m_mpz_manager.bitwise_xor(result, m_tracker.get_value(args[i]), result); + break; + } + case OP_BNAND: { + SASSERT(n_args >= 2); + mpz temp; + unsigned bv_sz = m_bv_util.get_bv_size(n); + m_mpz_manager.set(result, m_tracker.get_value(args[0])); + for (unsigned i = 1; i < n_args; i++) { + m_mpz_manager.bitwise_and(result, m_tracker.get_value(args[i]), temp); + m_mpz_manager.bitwise_not(bv_sz, temp, result); + } + m_mpz_manager.del(temp); + break; + } + case OP_BNOR: { + SASSERT(n_args >= 2); + mpz temp; + unsigned bv_sz = m_bv_util.get_bv_size(n); + m_mpz_manager.set(result, m_tracker.get_value(args[0])); + for (unsigned i = 1; i < n_args; i++) { + m_mpz_manager.bitwise_or(result, m_tracker.get_value(args[i]), temp); + m_mpz_manager.bitwise_not(bv_sz, temp, result); + } + m_mpz_manager.del(temp); + break; + } + case OP_BNOT: { + SASSERT(n_args == 1); + m_mpz_manager.bitwise_not(m_bv_util.get_bv_size(args[0]), m_tracker.get_value(args[0]), result); + break; + } + case OP_ULT: + case OP_ULEQ: + case OP_UGT: + case OP_UGEQ: { + SASSERT(n_args == 2); + const mpz & x = m_tracker.get_value(args[0]); + const mpz & y = m_tracker.get_value(args[1]); + if ((k == OP_ULT && m_mpz_manager.lt(x, y)) || + (k == OP_ULEQ && m_mpz_manager.le(x, y)) || + (k == OP_UGT && m_mpz_manager.gt(x, y)) || + (k == OP_UGEQ && m_mpz_manager.ge(x, y))) + m_mpz_manager.set(result, m_one); + break; + } + case OP_SLT: + case OP_SLEQ: + case OP_SGT: + case OP_SGEQ: { + SASSERT(n_args == 2); + mpz x; m_mpz_manager.set(x, m_tracker.get_value(args[0])); + mpz y; m_mpz_manager.set(y, m_tracker.get_value(args[1])); + unsigned bv_sz = m_bv_util.get_bv_size(args[0]); + const mpz & p = m_powers(bv_sz); + const mpz & p_half = m_powers(bv_sz-1); + if (x >= p_half) { m_mpz_manager.sub(x, p, x); } + if (y >= p_half) { m_mpz_manager.sub(y, p, y); } + if ((k == OP_SLT && m_mpz_manager.lt(x, y)) || + (k == OP_SLEQ && m_mpz_manager.le(x, y)) || + (k == OP_SGT && m_mpz_manager.gt(x, y)) || + (k == OP_SGEQ && m_mpz_manager.ge(x, y))) + m_mpz_manager.set(result, m_one); + m_mpz_manager.del(x); + m_mpz_manager.del(y); + break; + } + case OP_BIT2BOOL: { + SASSERT(n_args == 1); + const mpz & child = m_tracker.get_value(args[0]); + m_mpz_manager.set(result, child); + break; + } + case OP_BASHR: { + SASSERT(n_args == 2); + m_mpz_manager.set(result, m_tracker.get_value(args[0])); + mpz first; + const mpz & p = m_powers(m_bv_util.get_bv_size(args[0])-1); + m_mpz_manager.bitwise_and(result, p, first); + mpz shift; m_mpz_manager.set(shift, m_tracker.get_value(args[1])); + mpz temp; + while (!m_mpz_manager.is_zero(shift)) { + m_mpz_manager.machine_div(result, m_two, temp); + m_mpz_manager.add(temp, first, result); + m_mpz_manager.dec(shift); + } + m_mpz_manager.del(first); + m_mpz_manager.del(shift); + m_mpz_manager.del(temp); + break; + } + case OP_BLSHR: { + SASSERT(n_args == 2); + m_mpz_manager.set(result, m_tracker.get_value(args[0])); + mpz shift; m_mpz_manager.set(shift, m_tracker.get_value(args[1])); + while (!m_mpz_manager.is_zero(shift)) { + m_mpz_manager.machine_div(result, m_two, result); + m_mpz_manager.dec(shift); + } + m_mpz_manager.del(shift); + break; + } + case OP_BSHL: { + SASSERT(n_args == 2); + m_mpz_manager.set(result, m_tracker.get_value(args[0])); + mpz shift; m_mpz_manager.set(shift, m_tracker.get_value(args[1])); + while (!m_mpz_manager.is_zero(shift)) { + m_mpz_manager.mul(result, m_two, result); + m_mpz_manager.dec(shift); + } + const mpz & p = m_powers(m_bv_util.get_bv_size(n)); + m_mpz_manager.rem(result, p, result); + m_mpz_manager.del(shift); + break; + } + case OP_SIGN_EXT: { + SASSERT(n_args == 1); + m_mpz_manager.set(result, m_tracker.get_value(args[0])); + break; + } + default: + NOT_IMPLEMENTED_YET(); + } + } + else { + NOT_IMPLEMENTED_YET(); + } + + TRACE("sls_eval", tout << "(" << fd->get_name(); + for (unsigned i = 0; i < n_args; i++) + tout << " " << m_mpz_manager.to_string(m_tracker.get_value(args[i])); + tout << ") ---> " << m_mpz_manager.to_string(result); + if (m_manager.is_bool(fd->get_range())) tout << " [Boolean]"; + else tout << " [vector size: " << m_bv_util.get_bv_size(fd->get_range()) << "]"; + tout << std::endl; ); + + SASSERT(m_mpz_manager.is_nonneg(result)); + } + + void eval_checked(expr * n, mpz & result) { + switch(n->get_kind()) { + case AST_APP: { + app * a = to_app(n); + (*this)(a, result); + + unsigned n_args = a->get_num_args(); + m_temp_exprs.reset(); + for (unsigned i = 0; i < n_args; i++) { + expr * arg = a->get_arg(i); + const mpz & v = m_tracker.get_value(arg); + m_temp_exprs.push_back(m_tracker.mpz2value(m_manager.get_sort(arg), v)); + } + expr_ref q(m_manager), temp(m_manager); + q = m_manager.mk_app(a->get_decl(), m_temp_exprs.size(), m_temp_exprs.c_ptr()); + model dummy_model(m_manager); + model_evaluator evaluator(dummy_model); + evaluator(q, temp); + mpz check_res; + m_tracker.value2mpz(temp, check_res); + CTRACE("sls", !m_mpz_manager.eq(check_res, result), + tout << "EVAL BUG: IS " << m_mpz_manager.to_string(result) << + " SHOULD BE " << m_mpz_manager.to_string(check_res) << std::endl; ); + SASSERT(m_mpz_manager.eq(check_res, result)); + m_mpz_manager.del(check_res); + + break; + } + default: + NOT_IMPLEMENTED_YET(); + } + } + + void run_update(unsigned cur_depth) { + // precondition: m_traversal_stack contains the entry point(s) + expr_fast_mark1 visited; + mpz new_value; + + SASSERT(cur_depth < m_traversal_stack.size()); + while (cur_depth != static_cast(-1)) { + ptr_vector & cur_depth_exprs = m_traversal_stack[cur_depth]; + + for (unsigned i = 0; i < cur_depth_exprs.size(); i++) { + expr * cur = cur_depth_exprs[i]; + + (*this)(to_app(cur), new_value); + m_tracker.set_value(cur, new_value); + m_tracker.set_score(cur, m_tracker.score(cur)); + + if (m_tracker.has_uplinks(cur)) { + ptr_vector & ups = m_tracker.get_uplinks(cur); + for (unsigned j = 0; j < ups.size(); j++) { + expr * next = ups[j]; + unsigned next_d = m_tracker.get_distance(next); + SASSERT(next_d < cur_depth); + if (!visited.is_marked(next)) { + m_traversal_stack[next_d].push_back(next); + visited.mark(next); + } + } + } + } + + cur_depth_exprs.reset(); + cur_depth--; + } + + m_mpz_manager.del(new_value); + } + + void update_all() { + unsigned max_depth = 0; + + sls_tracker::entry_point_type::iterator start = m_tracker.get_entry_points().begin(); + sls_tracker::entry_point_type::iterator end = m_tracker.get_entry_points().end(); + for (sls_tracker::entry_point_type::iterator it = start; it != end; it++) { + expr * ep = m_tracker.get_entry_point(it->m_key); + unsigned cur_depth = m_tracker.get_distance(ep); + if (m_traversal_stack.size() <= cur_depth) + m_traversal_stack.resize(cur_depth+1); + m_traversal_stack[cur_depth].push_back(ep); + if (cur_depth > max_depth) max_depth = cur_depth; + } + + run_update(max_depth); + } + + void update(func_decl * fd, const mpz & new_value) { + m_tracker.set_value(fd, new_value); + expr * ep = m_tracker.get_entry_point(fd); + unsigned cur_depth = m_tracker.get_distance(ep); + if (m_traversal_stack.size() <= cur_depth) + m_traversal_stack.resize(cur_depth+1); + m_traversal_stack[cur_depth].push_back(ep); + + run_update(cur_depth); + } + + void randomize_local(goal_ref const & g) { + ptr_vector & unsat_constants = m_tracker.get_unsat_constants(g); + + // Randomize _all_ candidates: + + //// bool did_something = false; + //for (unsigned i = 0; i < unsat_constants.size(); i++) { + // func_decl * fd = unsat_constants[i]; + // mpz temp = m_tracker.get_random(fd->get_range()); + // // if (m_mpz_manager.neq(temp, m_tracker.get_value(fd))) { + // // did_something = true; + // // } + // update(fd, temp); + // m_mpz_manager.del(temp); + //} + + // Randomize _one_ candidate: + unsigned r = m_tracker.get_random_uint(16) % unsat_constants.size(); + func_decl * fd = unsat_constants[r]; + mpz temp = m_tracker.get_random(fd->get_range()); + update(fd, temp); + m_mpz_manager.del(temp); + + TRACE("sls", /*tout << "Randomization candidates: "; + for (unsigned i = 0; i < unsat_constants.size(); i++) + tout << unsat_constants[i]->get_name() << ", "; + tout << std::endl;*/ + tout << "Randomization candidate: " << unsat_constants[r]->get_name() << std::endl; + tout << "Locally randomized model: " << std::endl; + m_tracker.show_model(tout); ); + } +}; + +#endif \ No newline at end of file diff --git a/src/tactic/sls/sls_params.pyg b/src/tactic/sls/sls_params.pyg new file mode 100644 index 000000000..cc3e05966 --- /dev/null +++ b/src/tactic/sls/sls_params.pyg @@ -0,0 +1,8 @@ +def_module_params('sls', + export=True, + description='Experimental Stochastic Local Search Solver (for QFBV only).', + params=(max_memory_param(), + ('restarts', UINT, UINT_MAX, '(max) number of restarts'), + ('plateau_limit', UINT, 10, 'pleateau limit'), + ('random_seed', UINT, 0, 'random seed') + )) diff --git a/src/tactic/sls/sls_powers.h b/src/tactic/sls/sls_powers.h new file mode 100644 index 000000000..d0cc0815e --- /dev/null +++ b/src/tactic/sls/sls_powers.h @@ -0,0 +1,49 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + sls_powers.h + +Abstract: + + Power-of-2 module for SLS + +Author: + + Christoph (cwinter) 2012-02-29 + +Notes: + +--*/ + +#ifndef _SLS_POWERS_H_ +#define _SLS_POWERS_H_ + +#include"mpz.h" + +class powers : public u_map { + unsynch_mpz_manager & m; +public: + powers(unsynch_mpz_manager & m) : m(m) {} + ~powers() { + for (iterator it = begin(); it != end(); it++) { + m.del(*it->m_value); + dealloc(it->m_value); + } + } + + const mpz & operator()(unsigned n) { + u_map::iterator it = find_iterator(n); + if (it != end()) + return *it->m_value; + else { + mpz * new_obj = alloc(mpz); + m.mul2k(m.mk_z(1), n, *new_obj); + insert(n, new_obj); + return *new_obj; + } + } +}; + +#endif \ No newline at end of file diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp index eb806e23c..fff082bd8 100644 --- a/src/tactic/sls/sls_tactic.cpp +++ b/src/tactic/sls/sls_tactic.cpp @@ -35,6 +35,10 @@ Notes: #include"sls_tactic.h" #include"nnf_tactic.h" +#include"sls_params.hpp" +#include"sls_evaluator.h" +#include"sls_tracker.h" + class sls_tactic : public tactic { class stats { public: @@ -62,1265 +66,7 @@ class sls_tactic : public tactic { } }; - struct imp { - class score_tracker; - - class powers : public u_map { - unsynch_mpz_manager & m; - public: - powers(unsynch_mpz_manager & m) : m(m) {} - ~powers() { - for (iterator it = begin(); it != end(); it++) { - m.del(*it->m_value); - dealloc(it->m_value); - } - } - - const mpz & operator()(unsigned n) { - u_map::iterator it = find_iterator(n); - if (it != end()) - return *it->m_value; - else { - mpz * new_obj = alloc(mpz); - insert(n, new_obj); - m.power(unsynch_mpz_manager::mk_z(2), n, *new_obj); - return *new_obj; - } - } - }; - - class evaluator { - ast_manager & m_manager; - bv_util & m_bv_util; - family_id m_bv_fid; - score_tracker & m_tracker; - unsynch_mpz_manager & m_mpz_manager; - mpz m_zero, m_one, m_two; - powers & m_powers; - - - public: - evaluator(ast_manager & m, bv_util & bvu, score_tracker & t, unsynch_mpz_manager & mm, powers & p) : - m_manager(m), - m_bv_util(bvu), - m_tracker(t), - m_mpz_manager(mm), - m_zero(m_mpz_manager.mk_z(0)), - m_one(m_mpz_manager.mk_z(1)), - m_two(m_mpz_manager.mk_z(2)), - m_powers(p) { - m_bv_fid = m_bv_util.get_family_id(); - } - - ~evaluator() { - m_mpz_manager.del(m_zero); - m_mpz_manager.del(m_one); - m_mpz_manager.del(m_two); - } - - void operator()(app * n, mpz & result) { - func_decl * fd = n->get_decl(); - unsigned n_args = n->get_num_args(); - expr * const * args = n->get_args(); - - m_mpz_manager.set(result, m_zero); - - if (m_manager.is_and(n)) { - m_mpz_manager.set(result, m_one); - for (unsigned i = 0; i < n_args; i++) { - if (m_mpz_manager.neq(m_tracker.get_value(args[i]), result)) { - m_mpz_manager.set(result, m_zero); - break; - } - } - } - else if (m_manager.is_or(n)) { - for (unsigned i = 0; i < n_args; i++) { - if (m_mpz_manager.neq(m_tracker.get_value(args[i]), result)) { - m_mpz_manager.set(result, m_one); - break; - } - } - } - else if (m_manager.is_not(n)) { - SASSERT(n_args == 1); - const mpz & child = m_tracker.get_value(args[0]); - SASSERT(m_mpz_manager.is_one(child) || m_mpz_manager.is_zero(child)); - m_mpz_manager.set(result, (m_mpz_manager.is_zero(child)) ? m_one : m_zero); - } - else if (m_manager.is_eq(n)) { - SASSERT(n_args >= 2); - m_mpz_manager.set(result, m_one); - const mpz & first = m_tracker.get_value(args[0]); - for (unsigned i = 1; i < n_args; i++) { - if (m_mpz_manager.neq(m_tracker.get_value(args[i]), first)) { - m_mpz_manager.set(result, m_zero); - break; - } - } - } - else if (m_manager.is_distinct(n)) { - m_mpz_manager.set(result, m_one); - for (unsigned i = 0; i < n_args && m_mpz_manager.is_one(result); i++) { - for (unsigned j = i+1; j < n_args && m_mpz_manager.is_one(result); j++) { - if (m_mpz_manager.eq(m_tracker.get_value(args[i]), m_tracker.get_value(args[j]))) - m_mpz_manager.set(result, m_zero); - } - } - } - else if (fd->get_family_id() == m_bv_fid) { - bv_op_kind k = static_cast(fd->get_decl_kind()); - switch(k) { - case OP_CONCAT: { - SASSERT(n_args >= 2); - for (unsigned i = 0; i < n_args; i++) { - if (i != 0) { - const mpz & p = m_powers(m_bv_util.get_bv_size(args[i])); - m_mpz_manager.mul(result, p, result); - } - m_mpz_manager.add(result, m_tracker.get_value(args[i]), result); - } - break; - } - case OP_EXTRACT: { - SASSERT(n_args == 1); - const mpz & child = m_tracker.get_value(args[0]); - unsigned h = m_bv_util.get_extract_high(n); - unsigned l = m_bv_util.get_extract_low(n); - - mpz mask; - m_mpz_manager.set(mask, m_powers(h+1)); - m_mpz_manager.dec(mask); - m_mpz_manager.bitwise_and(child, mask, result); // result = [h:0] of child - - // shift result by l - for (; l != 0 ; l--) - m_mpz_manager.machine_div(result, m_two, result); - - m_mpz_manager.del(mask); - break; - } - case OP_BADD: { - SASSERT(n_args >= 2); - for (unsigned i = 0; i < n_args; i++) { - const mpz & next = m_tracker.get_value(args[i]); - m_mpz_manager.add(result, next, result); - } - const mpz & p = m_powers(m_bv_util.get_bv_size(n)); - m_mpz_manager.rem(result, p, result); - break; - } - case OP_BSUB: { - SASSERT(n_args == 2); - const mpz & p = m_powers(m_bv_util.get_bv_size(n)); - mpz temp; - m_mpz_manager.sub(m_tracker.get_value(args[0]), m_tracker.get_value(args[1]), temp); - m_mpz_manager.mod(temp, p, result); - m_mpz_manager.del(temp); - break; - } - case OP_BMUL: { - SASSERT(n_args >= 2); - m_mpz_manager.set(result, m_tracker.get_value(args[0])); - for (unsigned i = 1; i < n_args; i++) { - const mpz & next = m_tracker.get_value(args[i]); - m_mpz_manager.mul(result, next, result); - } - const mpz & p = m_powers(m_bv_util.get_bv_size(n)); - m_mpz_manager.rem(result, p, result); - break; - } - case OP_BNEG: { // 2's complement unary minus - SASSERT(n_args == 1); - const mpz & child = m_tracker.get_value(args[0]); - if (m_mpz_manager.is_zero(child)) { - m_mpz_manager.set(result, m_zero); - } - else { - unsigned bv_sz = m_bv_util.get_bv_size(n); - m_mpz_manager.bitwise_not(bv_sz, child, result); - m_mpz_manager.inc(result); // can't overflow - } - break; - } - case OP_BSDIV: - case OP_BSDIV0: - case OP_BSDIV_I: { - SASSERT(n_args == 2); - mpz x; m_mpz_manager.set(x, m_tracker.get_value(args[0])); - mpz y; m_mpz_manager.set(y, m_tracker.get_value(args[1])); - SASSERT(m_mpz_manager.is_nonneg(x) && m_mpz_manager.is_nonneg(y)); - unsigned bv_sz = m_bv_util.get_bv_size(args[0]); - const mpz & p = m_powers(bv_sz); - const mpz & p_half = m_powers(bv_sz-1); - if (x >= p_half) { m_mpz_manager.sub(x, p, x); } - if (y >= p_half) { m_mpz_manager.sub(y, p, y); } - - if (m_mpz_manager.is_zero(y)) { - if (m_mpz_manager.is_neg(x)) - m_mpz_manager.set(result, m_one); - else { - m_mpz_manager.set(result, m_powers(m_bv_util.get_bv_size(n))); - m_mpz_manager.dec(result); - } - } - else { - m_mpz_manager.machine_div(x, y, result); - } - if (m_mpz_manager.is_neg(result)) - m_mpz_manager.add(result, p, result); - m_mpz_manager.del(x); - m_mpz_manager.del(y); - break; - } - case OP_BUDIV: - case OP_BUDIV0: - case OP_BUDIV_I: { - SASSERT(n_args == 2); - mpz x; m_mpz_manager.set(x, m_tracker.get_value(args[0])); - mpz y; m_mpz_manager.set(y, m_tracker.get_value(args[1])); - - if (m_mpz_manager.is_zero(y)) { - m_mpz_manager.set(result, m_powers(m_bv_util.get_bv_size(n))); - m_mpz_manager.dec(result); - } - else { - m_mpz_manager.machine_div(x, y, result); - } - m_mpz_manager.del(x); - m_mpz_manager.del(y); - break; - } - case OP_BSREM: - case OP_BSREM0: - case OP_BSREM_I: { - SASSERT(n_args == 2); - mpz x; m_mpz_manager.set(x, m_tracker.get_value(args[0])); - mpz y; m_mpz_manager.set(y, m_tracker.get_value(args[1])); - unsigned bv_sz = m_bv_util.get_bv_size(args[0]); - const mpz & p = m_powers(bv_sz); - const mpz & p_half = m_powers(bv_sz-1); - if (x >= p_half) { m_mpz_manager.sub(x, p, x); } - if (y >= p_half) { m_mpz_manager.sub(y, p, y); } - - if (m_mpz_manager.is_zero(y)) { - m_mpz_manager.set(result, x); - } - else { - m_mpz_manager.rem(x, y, result); - } - if (m_mpz_manager.is_neg(result)) - m_mpz_manager.add(result, p, result); - m_mpz_manager.del(x); - m_mpz_manager.del(y); - break; - } - case OP_BUREM: - case OP_BUREM0: - case OP_BUREM_I: { - SASSERT(n_args == 2); - mpz x; m_mpz_manager.set(x, m_tracker.get_value(args[0])); - mpz y; m_mpz_manager.set(y, m_tracker.get_value(args[1])); - - if (m_mpz_manager.is_zero(y)) { - m_mpz_manager.set(result, x); - } - else { - m_mpz_manager.mod(x, y, result); - } - m_mpz_manager.del(x); - m_mpz_manager.del(y); - break; - } - case OP_BSMOD: - case OP_BSMOD0: - case OP_BSMOD_I:{ - SASSERT(n_args == 2); - mpz x; m_mpz_manager.set(x, m_tracker.get_value(args[0])); - mpz y; m_mpz_manager.set(y, m_tracker.get_value(args[1])); - unsigned bv_sz = m_bv_util.get_bv_size(args[0]); - const mpz & p = m_powers(bv_sz); - const mpz & p_half = m_powers(bv_sz-1); - if (x >= p_half) { m_mpz_manager.sub(x, p, x); } - if (y >= p_half) { m_mpz_manager.sub(y, p, y); } - - if (m_mpz_manager.is_zero(y)) - m_mpz_manager.set(result, x); - else { - bool neg_x = m_mpz_manager.is_neg(x); - bool neg_y = m_mpz_manager.is_neg(y); - mpz abs_x, abs_y; - m_mpz_manager.set(abs_x, x); - m_mpz_manager.set(abs_y, y); - if (neg_x) m_mpz_manager.neg(abs_x); - if (neg_y) m_mpz_manager.neg(abs_y); - SASSERT(m_mpz_manager.is_nonneg(abs_x) && m_mpz_manager.is_nonneg(abs_y)); - - m_mpz_manager.mod(abs_x, abs_y, result); - - if (m_mpz_manager.is_zero(result) || (!neg_x && !neg_y)) { - /* Nothing */ - } - else if (neg_x && !neg_y) { - m_mpz_manager.neg(result); - m_mpz_manager.add(result, y, result); - } - else if (!neg_x && neg_y) { - m_mpz_manager.add(result, y, result); - } - else { - m_mpz_manager.neg(result); - } - - m_mpz_manager.del(abs_x); - m_mpz_manager.del(abs_y); - } - - if (m_mpz_manager.is_neg(result)) - m_mpz_manager.add(result, p, result); - - m_mpz_manager.del(x); - m_mpz_manager.del(y); - break; - } - case OP_BAND: { - SASSERT(n_args >= 2); - m_mpz_manager.set(result, m_tracker.get_value(args[0])); - for (unsigned i = 1; i < n_args; i++) - m_mpz_manager.bitwise_and(result, m_tracker.get_value(args[i]), result); - break; - } - case OP_BOR: { - SASSERT(n_args >= 2); - m_mpz_manager.set(result, m_tracker.get_value(args[0])); - for (unsigned i = 1; i < n_args; i++) { - m_mpz_manager.bitwise_or(result, m_tracker.get_value(args[i]), result); - } - break; - } - case OP_BXOR: { - SASSERT(n_args >= 2); - m_mpz_manager.set(result, m_tracker.get_value(args[0])); - for (unsigned i = 1; i < n_args; i++) - m_mpz_manager.bitwise_xor(result, m_tracker.get_value(args[i]), result); - break; - } - case OP_BNAND: { - SASSERT(n_args >= 2); - mpz temp; - unsigned bv_sz = m_bv_util.get_bv_size(n); - m_mpz_manager.set(result, m_tracker.get_value(args[0])); - for (unsigned i = 1; i < n_args; i++) { - m_mpz_manager.bitwise_and(result, m_tracker.get_value(args[i]), temp); - m_mpz_manager.bitwise_not(bv_sz, temp, result); - } - m_mpz_manager.del(temp); - break; - } - case OP_BNOR: { - SASSERT(n_args >= 2); - mpz temp; - unsigned bv_sz = m_bv_util.get_bv_size(n); - m_mpz_manager.set(result, m_tracker.get_value(args[0])); - for (unsigned i = 1; i < n_args; i++) { - m_mpz_manager.bitwise_or(result, m_tracker.get_value(args[i]), temp); - m_mpz_manager.bitwise_not(bv_sz, temp, result); - } - m_mpz_manager.del(temp); - break; - } - case OP_BNOT: { - SASSERT(n_args == 1); - m_mpz_manager.bitwise_not(m_bv_util.get_bv_size(args[0]), m_tracker.get_value(args[0]), result); - break; - } - case OP_ULT: - case OP_ULEQ: - case OP_UGT: - case OP_UGEQ: { - SASSERT(n_args == 2); - const mpz & x = m_tracker.get_value(args[0]); - const mpz & y = m_tracker.get_value(args[1]); - if ((k == OP_ULT && m_mpz_manager.lt(x, y)) || - (k == OP_ULEQ && m_mpz_manager.le(x, y)) || - (k == OP_UGT && m_mpz_manager.gt(x, y)) || - (k == OP_UGEQ && m_mpz_manager.ge(x, y))) - m_mpz_manager.set(result, m_one); - break; - } - case OP_SLT: - case OP_SLEQ: - case OP_SGT: - case OP_SGEQ: { - SASSERT(n_args == 2); - mpz x; m_mpz_manager.set(x, m_tracker.get_value(args[0])); - mpz y; m_mpz_manager.set(y, m_tracker.get_value(args[1])); - unsigned bv_sz = m_bv_util.get_bv_size(args[0]); - const mpz & p = m_powers(bv_sz); - const mpz & p_half = m_powers(bv_sz-1); - if (x >= p_half) { m_mpz_manager.sub(x, p, x); } - if (y >= p_half) { m_mpz_manager.sub(y, p, y); } - if ((k == OP_SLT && m_mpz_manager.lt(x, y)) || - (k == OP_SLEQ && m_mpz_manager.le(x, y)) || - (k == OP_SGT && m_mpz_manager.gt(x, y)) || - (k == OP_SGEQ && m_mpz_manager.ge(x, y))) - m_mpz_manager.set(result, m_one); - m_mpz_manager.del(x); - m_mpz_manager.del(y); - break; - } - case OP_BIT2BOOL: { - SASSERT(n_args == 1); - const mpz & child = m_tracker.get_value(args[0]); - m_mpz_manager.set(result, child); - break; - } - case OP_BASHR: { - SASSERT(n_args == 2); - m_mpz_manager.set(result, m_tracker.get_value(args[0])); - mpz first; - const mpz & p = m_powers(m_bv_util.get_bv_size(args[0])-1); - m_mpz_manager.bitwise_and(result, p, first); - mpz shift; m_mpz_manager.set(shift, m_tracker.get_value(args[1])); - mpz temp; - while (!m_mpz_manager.is_zero(shift)) { - m_mpz_manager.machine_div(result, m_two, temp); - m_mpz_manager.add(temp, first, result); - m_mpz_manager.dec(shift); - } - m_mpz_manager.del(first); - m_mpz_manager.del(shift); - m_mpz_manager.del(temp); - break; - } - case OP_BLSHR: { - SASSERT(n_args == 2); - m_mpz_manager.set(result, m_tracker.get_value(args[0])); - mpz shift; m_mpz_manager.set(shift, m_tracker.get_value(args[1])); - while (!m_mpz_manager.is_zero(shift)) { - m_mpz_manager.machine_div(result, m_two, result); - m_mpz_manager.dec(shift); - } - m_mpz_manager.del(shift); - break; - } - case OP_BSHL: { - SASSERT(n_args == 2); - m_mpz_manager.set(result, m_tracker.get_value(args[0])); - mpz shift; m_mpz_manager.set(shift, m_tracker.get_value(args[1])); - while (!m_mpz_manager.is_zero(shift)) { - m_mpz_manager.mul(result, m_two, result); - m_mpz_manager.dec(shift); - } - const mpz & p = m_powers(m_bv_util.get_bv_size(n)); - m_mpz_manager.rem(result, p, result); - m_mpz_manager.del(shift); - break; - } - case OP_SIGN_EXT: { - SASSERT(n_args == 1); - m_mpz_manager.set(result, m_tracker.get_value(args[0])); - break; - } - default: - NOT_IMPLEMENTED_YET(); - } - } - else { - NOT_IMPLEMENTED_YET(); - } - - TRACE("sls_eval", tout << "(" << fd->get_name(); - for (unsigned i = 0; i < n_args; i++) - tout << " " << m_mpz_manager.to_string(m_tracker.get_value(args[i])); - tout << ") ---> " << m_mpz_manager.to_string(result); - if (m_manager.is_bool(fd->get_range())) tout << " [Boolean]"; - else tout << " [vector size: " << m_bv_util.get_bv_size(fd->get_range()) << "]"; - tout << std::endl; ); - - SASSERT(m_mpz_manager.is_nonneg(result)); - } - }; - - class score_tracker { - ast_manager & m_manager; - unsynch_mpz_manager & m_mpz_manager; - bv_util & m_bv_util; - powers & m_powers; - random_gen m_rng; - unsigned m_random_bits; - unsigned m_random_bits_cnt; - vector > m_traversal_stack; - evaluator m_sls_evaluator; - mpz m_zero, m_one, m_two; - - model m_dummy_model; - model_evaluator m_evaluator; - expr_ref_buffer m_temp_exprs; - - struct value_score { - value_score() : m(0), value(unsynch_mpz_manager::mk_z(0)), score(0.0), distance(0) { }; - ~value_score() { if (m) m->del(value); } - unsynch_mpz_manager * m; - mpz value; - double score; - unsigned distance; // max distance from any root - value_score & operator=(const value_score & other) { - SASSERT(m == 0 || m == other.m); - if (m) m->set(value, 0); else m = other.m; - m->set(value, other.value); - score = other.score; - distance = other.distance; - return *this; - } - }; - - typedef obj_map scores_type; - typedef obj_map > uplinks_type; - typedef obj_map entry_point_type; - typedef obj_map > occ_type; - scores_type m_scores; - uplinks_type m_uplinks; - entry_point_type m_entry_points; - ptr_vector m_constants; - ptr_vector m_temp_constants; - occ_type m_constants_occ; - - public: - score_tracker(ast_manager & m, bv_util & bvu, unsynch_mpz_manager & mm, powers & p) : - m_manager(m), - m_mpz_manager(mm), - m_bv_util(bvu), - m_powers(p), - m_random_bits_cnt(0), - m_sls_evaluator(m, m_bv_util, *this, m_mpz_manager, p), - m_zero(m_mpz_manager.mk_z(0)), - m_one(m_mpz_manager.mk_z(1)), - m_two(m_mpz_manager.mk_z(2)), - m_dummy_model(m), - m_evaluator(m_dummy_model), - m_temp_exprs(m) { - } - - ~score_tracker() { - m_mpz_manager.del(m_zero); - m_mpz_manager.del(m_one); - m_mpz_manager.del(m_two); - } - - void set_value(expr * n, const mpz & r) { - SASSERT(m_scores.contains(n)); - m_mpz_manager.set(m_scores.find(n).value, r); - } - - void set_value(func_decl * fd, const mpz & r) { - SASSERT(m_entry_points.contains(fd)); - expr * ep = get_entry_point(fd); - set_value(ep, r); - } - - mpz & get_value(expr * n) { - SASSERT(m_scores.contains(n)); - return m_scores.find(n).value; - } - - mpz & get_value(func_decl * fd) { - SASSERT(m_entry_points.contains(fd)); - expr * ep = get_entry_point(fd); - return get_value(ep); - } - - void set_score(expr * n, double score) { - SASSERT(m_scores.contains(n)); - m_scores.find(n).score = score; - } - - void set_score(func_decl * fd, double score) { - SASSERT(m_entry_points.contains(fd)); - expr * ep = get_entry_point(fd); - set_score(ep, score); - } - - double & get_score(expr * n) { - SASSERT(m_scores.contains(n)); - return m_scores.find(n).score; - } - - double & get_score(func_decl * fd) { - SASSERT(m_entry_points.contains(fd)); - expr * ep = get_entry_point(fd); - return get_score(ep); - } - - unsigned get_distance(expr * n) { - SASSERT(m_scores.contains(n)); - return m_scores.find(n).distance; - } - - void set_distance(expr * n, unsigned d) { - SASSERT(m_scores.contains(n)); - m_scores.find(n).distance = d; - } - - expr * get_entry_point(func_decl * fd) { - SASSERT(m_entry_points.contains(fd)); - return m_entry_points.find(fd); - } - - bool has_uplinks(expr * n) { - return m_uplinks.contains(n); - } - - ptr_vector & get_uplinks(expr * n) { - SASSERT(m_uplinks.contains(n)); - return m_uplinks.find(n); - } - - void initialize(app * n) { - // Build score table - if (!m_scores.contains(n)) { - value_score vs; - vs.m = & m_mpz_manager; - m_scores.insert(n, vs); - } - - // Update uplinks - unsigned na = n->get_num_args(); - for (unsigned i = 0; i < na; i++) { - expr * c = n->get_arg(i); - uplinks_type::obj_map_entry * entry = m_uplinks.insert_if_not_there2(c, ptr_vector()); - entry->get_data().m_value.push_back(n); - } - - func_decl * d = n->get_decl(); - - if (n->get_num_args() == 0) { - if (d->get_family_id() != null_family_id) { - // Interpreted constant - mpz t; - value2mpz(n, t); - set_value(n, t); - m_mpz_manager.del(t); - } - else { - // Uninterpreted constant - m_entry_points.insert_if_not_there(d, n); - m_constants.push_back(d); - } - } - } - - struct init_proc { - ast_manager & m_manager; - score_tracker & m_tracker; - - init_proc(ast_manager & m, score_tracker & tracker): - m_manager(m), - m_tracker(tracker) { - } - - void operator()(var * n) {} - - void operator()(quantifier * n) {} - - void operator()(app * n) { - m_tracker.initialize(n); - } - }; - - struct find_func_decls_proc { - ast_manager & m_manager; - ptr_vector & m_occs; - - find_func_decls_proc (ast_manager & m, ptr_vector & occs): - m_manager(m), - m_occs(occs) { - } - - void operator()(var * n) {} - - void operator()(quantifier * n) {} - - void operator()(app * n) { - if (n->get_num_args() != 0) - return; - func_decl * d = n->get_decl(); - if (d->get_family_id() != null_family_id) - return; - m_occs.push_back(d); - } - }; - - void calculate_expr_distances(goal_ref const & g) { - // precondition: m_scores is set up. - unsigned sz = g->size(); - ptr_vector stack; - for (unsigned i = 0; i < sz; i++) - stack.push_back(to_app(g->form(i))); - while (!stack.empty()) { - app * cur = stack.back(); - stack.pop_back(); - - unsigned d = get_distance(cur); - - for (unsigned i = 0; i < cur->get_num_args(); i++) { - app * child = to_app(cur->get_arg(i)); - unsigned d_child = get_distance(child); - if (d >= d_child) { - set_distance(child, d+1); - stack.push_back(child); - } - } - } - } - - void initialize(goal_ref const & g) { - init_proc proc(m_manager, *this); - expr_mark visited; - unsigned sz = g->size(); - for (unsigned i = 0; i < sz; i++) { - expr * e = g->form(i); - for_each_expr(proc, visited, e); - } - - visited.reset(); - - for (unsigned i = 0; i < sz; i++) { - expr * e = g->form(i); - ptr_vector t; - m_constants_occ.insert_if_not_there(e, t); - find_func_decls_proc ffd_proc(m_manager, m_constants_occ.find(e)); - expr_fast_mark1 visited; - quick_for_each_expr(ffd_proc, visited, e); - } - - calculate_expr_distances(g); - - TRACE("sls", tout << "Initial model:" << std::endl; show_model(tout); ); - } - - void show_model(std::ostream & out) { - unsigned sz = get_num_constants(); - for (unsigned i = 0; i < sz; i++) { - func_decl * fd = get_constant(i); - out << fd->get_name() << " = " << m_mpz_manager.to_string(get_value(fd)) << std::endl; - } - } - - model_ref get_model() { - model_ref res = alloc(model, m_manager); - unsigned sz = get_num_constants(); - for (unsigned i = 0; i < sz; i++) { - func_decl * fd = get_constant(i); - res->register_decl(fd, mpz2value(fd->get_range(), get_value(fd))); - } - return res; - } - - unsigned get_num_constants() { - return m_constants.size(); - } - - ptr_vector & get_constants() { - return m_constants; - } - - func_decl * get_constant(unsigned i) { - return m_constants[i]; - } - - void set_random_seed(unsigned s) { - m_rng.set_seed(s); - } - - mpz get_random_bv(sort * s) { - SASSERT(m_bv_util.is_bv_sort(s)); - unsigned bv_size = m_bv_util.get_bv_size(s); - mpz r; m_mpz_manager.set(r, 0); - - mpz temp; - do - { - m_mpz_manager.mul(r, m_two, temp); - m_mpz_manager.add(temp, get_random_bool(), r); - } while (--bv_size > 0); - m_mpz_manager.del(temp); - - return r; - } - - mpz & get_random_bool() { - if (m_random_bits_cnt == 0) { - m_random_bits = m_rng(); - m_random_bits_cnt = 15; // random_gen produces 15 bits of randomness. - } - - bool val = (m_random_bits & 0x01) != 0; - m_random_bits = m_random_bits >> 1; - m_random_bits_cnt--; - - return (val) ? m_one : m_zero; - } - - unsigned get_random_uint(unsigned bits) { - if (m_random_bits_cnt == 0) { - m_random_bits = m_rng(); - m_random_bits_cnt = 15; // random_gen produces 15 bits of randomness. - } - - unsigned val = 0; - while (bits-- > 0) { - if ((m_random_bits & 0x01) != 0) val++; - val <<= 1; - m_random_bits >>= 1; - m_random_bits_cnt--; - - if (m_random_bits_cnt == 0) { - m_random_bits = m_rng(); - m_random_bits_cnt = 15; // random_gen produces 15 bits of randomness. - } - } - - return val; - } - - mpz get_random(sort * s) { - if (m_bv_util.is_bv_sort(s)) - return get_random_bv(s); - else if (m_manager.is_bool(s)) - return get_random_bool(); - else - NOT_IMPLEMENTED_YET(); // This only works for bit-vectors for now. - } - - void randomize() { - TRACE("sls", tout << "Abandoned model:" << std::endl; show_model(tout); ); - - for (entry_point_type::iterator it = m_entry_points.begin(); it != m_entry_points.end(); it++) { - func_decl * fd = it->m_key; - sort * s = fd->get_range(); - mpz temp = get_random(s); - set_value(it->m_value, temp); - m_mpz_manager.del(temp); - } - - TRACE("sls", tout << "Randomized model:" << std::endl; show_model(tout); ); - } - - void randomize_local(goal_ref const & g) { - ptr_vector & unsat_constants = get_unsat_constants(g); - // bool did_something = false; - for (unsigned i = 0; i < unsat_constants.size(); i++) { - func_decl * fd = unsat_constants[i]; - mpz temp = get_random(fd->get_range()); - if (m_mpz_manager.neq(temp, get_value(fd))) { - // did_something = true; - } - update(fd, temp); - m_mpz_manager.del(temp); - } - TRACE("sls", tout << "Randomization candidates: "; - for (unsigned i = 0; i < unsat_constants.size(); i++) - tout << unsat_constants[i]->get_name() << ", "; - tout << std::endl; - tout << "Locally randomized model: " << std::endl; show_model(tout); ); - } - - #define _SCORE_AND_MIN - - double score_bool(expr * n, bool negated = false) { - TRACE("sls_score", tout << ((negated)?"NEG ":"") << "BOOL: " << mk_ismt2_pp(n, m_manager) << std::endl; ); - - double res = 0.0; - - if (is_uninterp_const(n)) { - const mpz & r = get_value(n); - if (negated) - res = (m_mpz_manager.is_one(r)) ? 0.0 : 1.0; - else - res = (m_mpz_manager.is_one(r)) ? 1.0 : 0.0; - } - else if (m_manager.is_and(n)) { - SASSERT(!negated); - app * a = to_app(n); - expr * const * args = a->get_args(); - #ifdef _SCORE_AND_MIN - double min = 1.0; - for (unsigned i = 0; i < a->get_num_args(); i++) { - double cur = get_score(args[i]); - if (cur < min) min = cur; - } - res = min; - #else - double sum = 0.0; - for (unsigned i = 0; i < a->get_num_args(); i++) - sum += get_score(args[i]); - res = sum / (double) a->get_num_args(); - #endif - } - else if (m_manager.is_or(n)) { - SASSERT(!negated); - app * a = to_app(n); - expr * const * args = a->get_args(); - double max = 0.0; - for (unsigned i = 0; i < a->get_num_args(); i++) { - double cur = get_score(args[i]); - if (cur > max) max = cur; - } - res = max; - } - else if (m_manager.is_ite(n)) { - SASSERT(!negated); - app * a = to_app(n); - SASSERT(a->get_num_args() == 3); - const mpz & cond = get_value(a->get_arg(0)); - double s_t = get_score(a->get_arg(1)); - double s_f = get_score(a->get_arg(2)); - res = (m_mpz_manager.is_one(cond)) ? s_t : s_f; - } - else if (m_manager.is_eq(n) || m_manager.is_iff(n)) { - app * a = to_app(n); - SASSERT(a->get_num_args() == 2); - expr * arg0 = a->get_arg(0); - expr * arg1 = a->get_arg(1); - const mpz & v0 = get_value(arg0); - const mpz & v1 = get_value(arg1); - - if (negated) { - res = (m_mpz_manager.eq(v0, v1)) ? 0.0 : 1.0; - TRACE("sls_score", tout << "V0 = " << m_mpz_manager.to_string(v0) << " ; V1 = " << - m_mpz_manager.to_string(v1) << std::endl; ); - } - else if (m_manager.is_bool(arg0)) { - res = m_mpz_manager.eq(v0, v1) ? 1.0 : 0.0; - TRACE("sls_score", tout << "V0 = " << m_mpz_manager.to_string(v0) << " ; V1 = " << - m_mpz_manager.to_string(v1) << std::endl; ); - } - else if (m_bv_util.is_bv(arg0)) { - mpz diff, diff_m1; - m_mpz_manager.bitwise_xor(v0, v1, diff); - unsigned hamming_distance = 0; - unsigned bv_sz = m_bv_util.get_bv_size(arg0); - #if 1 // unweighted hamming distance - while (!m_mpz_manager.is_zero(diff)) { - //m_mpz_manager.set(diff_m1, diff); - //m_mpz_manager.dec(diff_m1); - //m_mpz_manager.bitwise_and(diff, diff_m1, diff); - //hamming_distance++; - if (!m_mpz_manager.is_even(diff)) { - hamming_distance++; - } - m_mpz_manager.machine_div(diff, m_two, diff); - } - res = 1.0 - (hamming_distance / (double) bv_sz); - #else - rational r(diff); - r /= m_powers(bv_sz); - double dbl = r.get_double(); - res = (dbl < 0.0) ? 1.0 : (dbl > 1.0) ? 0.0 : 1.0 - dbl; - #endif - TRACE("sls_score", tout << "V0 = " << m_mpz_manager.to_string(v0) << " ; V1 = " << - m_mpz_manager.to_string(v1) << " ; HD = " << hamming_distance << - " ; SZ = " << bv_sz << std::endl; ); - m_mpz_manager.del(diff); - m_mpz_manager.del(diff_m1); - } - else - NOT_IMPLEMENTED_YET(); - } - else if (m_bv_util.is_bv_ule(n)) { // x <= y - app * a = to_app(n); - SASSERT(a->get_num_args() == 2); - const mpz & x = get_value(a->get_arg(0)); - const mpz & y = get_value(a->get_arg(1)); - unsigned bv_sz = m_bv_util.get_bv_size(a->get_decl()->get_domain()[0]); - - if (negated) { - if (m_mpz_manager.gt(x, y)) - res = 1.0; - else { - mpz diff; - m_mpz_manager.sub(y, x, diff); - m_mpz_manager.inc(diff); - rational n(diff); - n /= rational(m_powers(bv_sz)); - double dbl = n.get_double(); - // In extreme cases, n is 0.9999 but to_double returns something > 1.0 - res = (dbl > 1.0) ? 0.0 : (dbl < 0.0) ? 1.0 : 1.0 - dbl; - m_mpz_manager.del(diff); - } - } - else { - if (m_mpz_manager.le(x, y)) - res = 1.0; - else { - mpz diff; - m_mpz_manager.sub(x, y, diff); - rational n(diff); - n /= rational(m_powers(bv_sz)); - double dbl = n.get_double(); - res = (dbl > 1.0) ? 1.0 : (dbl < 0.0) ? 0.0 : dbl; - m_mpz_manager.del(diff); - } - } - TRACE("sls_score", tout << "x = " << m_mpz_manager.to_string(x) << " ; y = " << - m_mpz_manager.to_string(y) << " ; SZ = " << bv_sz << std::endl; ); - } - else if (m_bv_util.is_bv_sle(n)) { // x <= y - app * a = to_app(n); - SASSERT(a->get_num_args() == 2); - mpz x; m_mpz_manager.set(x, get_value(a->get_arg(0))); - mpz y; m_mpz_manager.set(y, get_value(a->get_arg(1))); - unsigned bv_sz = m_bv_util.get_bv_size(a->get_decl()->get_domain()[0]); - const mpz & p = m_powers(bv_sz); - const mpz & p_half = m_powers(bv_sz-1); - if (x >= p_half) { m_mpz_manager.sub(x, p, x); } - if (y >= p_half) { m_mpz_manager.sub(y, p, y); } - - if (negated) { - if (x > y) - res = 1.0; - else { - mpz diff; - m_mpz_manager.sub(y, x, diff); - m_mpz_manager.inc(diff); - rational n(diff); - n /= p; - double dbl = n.get_double(); - res = (dbl > 1.0) ? 0.0 : (dbl < 0.0) ? 1.0 : 1.0 - dbl; - m_mpz_manager.del(diff); - } - TRACE("sls_score", tout << "x = " << m_mpz_manager.to_string(x) << " ; y = " << - m_mpz_manager.to_string(y) << " ; SZ = " << bv_sz << std::endl; ); - } - else { - if (x <= y) - res = 1.0; - else { - mpz diff; - m_mpz_manager.sub(x, y, diff); - rational n(diff); - n /= p; - double dbl = n.get_double(); - res = (dbl > 1.0) ? 1.0 : (dbl < 0.0) ? 0.0 : dbl; - m_mpz_manager.del(diff); - } - TRACE("sls_score", tout << "x = " << m_mpz_manager.to_string(x) << " ; y = " << - m_mpz_manager.to_string(y) << " ; SZ = " << bv_sz << std::endl; ); - } - m_mpz_manager.del(x); - m_mpz_manager.del(y); - } - else if (m_manager.is_not(n)) { - SASSERT(!negated); - app * a = to_app(n); - SASSERT(a->get_num_args() == 1); - expr * child = a->get_arg(0); - if (m_manager.is_and(child) || m_manager.is_or(child)) // Precondition: Assertion set is in NNF. - NOT_IMPLEMENTED_YET(); - res = score_bool(child, true); - } - else if (m_manager.is_distinct(n)) { - app * a = to_app(n); - unsigned pairs = 0, distinct_pairs = 0; - unsigned sz = a->get_num_args(); - for (unsigned i = 0; i < sz; i++) { - for (unsigned j = i+1; j < sz; j++) { - // pair i/j - const mpz & v0 = get_value(a->get_arg(0)); - const mpz & v1 = get_value(a->get_arg(1)); - pairs++; - if (v0 != v1) - distinct_pairs++; - } - } - res = (distinct_pairs/(double)pairs); - if (negated) res = 1.0 - res; - } - else - NOT_IMPLEMENTED_YET(); - - SASSERT(res >= 0.0 && res <= 1.0); - - TRACE("sls_score", tout << "SCORE = " << res << std::endl; ); - return res; - } - - double score_bv(expr * n) { - return 0.0; // a bv-expr is always scored as 0.0; we won't use those scores. - } - - void value2mpz(expr * n, mpz & result) { - m_mpz_manager.set(result, m_zero); - - if (m_manager.is_bool(n)) { - m_mpz_manager.set(result, m_manager.is_true(n) ? m_one : m_zero); - } - else if (m_bv_util.is_bv(n)) { - unsigned bv_sz = m_bv_util.get_bv_size(n); - rational q; - if (!m_bv_util.is_numeral(n, q, bv_sz)) - NOT_IMPLEMENTED_YET(); - mpq temp = q.to_mpq(); - SASSERT(m_mpz_manager.is_one(temp.denominator())); - m_mpz_manager.set(result, temp.numerator()); - } - else - NOT_IMPLEMENTED_YET(); - } - - expr_ref mpz2value(sort * s, const mpz & r) { - expr_ref res(m_manager); - if (m_manager.is_bool(s)) - res = (m_mpz_manager.is_zero(r)) ? m_manager.mk_false() : m_manager.mk_true(); - else if (m_bv_util.is_bv_sort(s)) { - rational rat(r); - res = m_bv_util.mk_numeral(rat, s); - } - else - NOT_IMPLEMENTED_YET(); - return res; - } - - void eval(expr * n, mpz & result) { - switch(n->get_kind()) { - case AST_APP: { - app * a = to_app(n); - unsigned n_args = a->get_num_args(); - - if (n_args == 0) { - m_mpz_manager.set(result, get_value(n)); - } - else { - m_sls_evaluator(a, result); - - //#define _EVAL_CHECKED - #ifdef _EVAL_CHECKED - m_temp_exprs.reset(); - for (unsigned i = 0; i < n_args; i++) { - expr * arg = a->get_arg(i); - const mpz & v = get_value(arg); - m_temp_exprs.push_back(mpz2value(m_manager.get_sort(arg), v)); - } - expr_ref q(m_manager), temp(m_manager); - q = m_manager.mk_app(fd, m_temp_exprs.size(), m_temp_exprs.c_ptr()); - m_evaluator(q, temp); - mpz check_res; - value2mpz(temp, check_res); - if (!m_mpz_manager.eq(check_res, result)) - TRACE("sls", tout << "EVAL BUG: IS " << m_mpz_manager.to_string(result) << - " SHOULD BE " << m_mpz_manager.to_string(check_res) << std::endl; ); - SASSERT(m_mpz_manager.eq(check_res, result)); - m_mpz_manager.del(check_res); - #endif - } - break; - } - default: - NOT_IMPLEMENTED_YET(); - } - // TRACE("sls", tout << "EVAL: " << mk_ismt2_pp(n, m_manager) << " IS " << res << std::endl;); - } - - double score(expr * n) { - if (m_manager.is_bool(n)) - return score_bool(n); - else if (m_bv_util.is_bv(n)) - return score_bv(n); - else - NOT_IMPLEMENTED_YET(); - } - - void run_update(unsigned cur_depth) { - // precondition: m_traversal_stack contains the entry point(s) - expr_fast_mark1 visited; - mpz new_value; - - SASSERT(cur_depth < m_traversal_stack.size()); - while (cur_depth != static_cast(-1)) { - ptr_vector & cur_depth_exprs = m_traversal_stack[cur_depth]; - - for (unsigned i = 0; i < cur_depth_exprs.size(); i++) { - expr * cur = cur_depth_exprs[i]; - - eval(cur, new_value); - set_value(cur, new_value); - set_score(cur, score(cur)); - - if (has_uplinks(cur)) { - ptr_vector & ups = get_uplinks(cur); - for (unsigned j = 0; j < ups.size(); j++) { - expr * next = ups[j]; - unsigned next_d = get_distance(next); - SASSERT(next_d < cur_depth); - if (!visited.is_marked(next)) { - m_traversal_stack[next_d].push_back(next); - visited.mark(next); - } - } - } - } - - cur_depth_exprs.reset(); - cur_depth--; - } - - m_mpz_manager.del(new_value); - } - - void update_all() { - unsigned max_depth = 0; - - for (entry_point_type::iterator it = m_entry_points.begin(); - it != m_entry_points.end(); - it++) { - expr * ep = get_entry_point(it->m_key); - unsigned cur_depth = get_distance(ep); - if (m_traversal_stack.size() <= cur_depth) - m_traversal_stack.resize(cur_depth+1); - m_traversal_stack[cur_depth].push_back(ep); - if (cur_depth > max_depth) max_depth = cur_depth; - } - - run_update(max_depth); - } - - void update(func_decl * fd, const mpz & new_value) { - set_value(fd, new_value); - expr * ep = get_entry_point(fd); - unsigned cur_depth = get_distance(ep); - if (m_traversal_stack.size() <= cur_depth) - m_traversal_stack.resize(cur_depth+1); - m_traversal_stack[cur_depth].push_back(ep); - - run_update(cur_depth); - } - - ptr_vector & get_unsat_constants(goal_ref const & g) { - unsigned sz = g->size(); - - if (sz == 1) { - return get_constants(); - } - else { - m_temp_constants.reset(); - for (unsigned i = 0; i < sz; i++) { - expr * q = g->form(i); - if (m_mpz_manager.eq(get_value(q), m_one)) - continue; - ptr_vector const & this_decls = m_constants_occ.find(q); - unsigned sz2 = this_decls.size(); - for (unsigned j = 0; j < sz2; j++) { - func_decl * fd = this_decls[j]; - if (!m_temp_constants.contains(fd)) - m_temp_constants.push_back(fd); - } - } - return m_temp_constants; - } - } - }; - + struct imp { ast_manager & m_manager; stats & m_stats; unsynch_mpz_manager m_mpz_manager; @@ -1329,7 +75,8 @@ class sls_tactic : public tactic { bool m_produce_models; volatile bool m_cancel; bv_util m_bv_util; - score_tracker m_tracker; + sls_tracker m_tracker; + sls_evaluator m_evaluator; unsigned m_max_restarts; unsigned m_plateau_limit; @@ -1345,7 +92,8 @@ class sls_tactic : public tactic { m_two(m_mpz_manager.mk_z(2)), m_cancel(false), m_bv_util(m), - m_tracker(m, m_bv_util, m_mpz_manager, m_powers) + m_tracker(m, m_bv_util, m_mpz_manager, m_powers), + m_evaluator(m, m_bv_util, m_tracker, m_mpz_manager, m_powers) { updt_params(p); } @@ -1363,17 +111,15 @@ class sls_tactic : public tactic { void reset_cancel() { set_cancel(false); } static void collect_param_descrs(param_descrs & r) { - insert_produce_models(r); - r.insert("sls_restarts", CPK_UINT, "(default: infty) # of SLS restarts."); - r.insert("random_seed", CPK_UINT, "(default: 0) random seed."); - r.insert("plateau_limit", CPK_UINT, "(default: 100) SLS plateau limit."); + sls_params::collect_param_descrs(r); } - void updt_params(params_ref const & p) { - m_produce_models = p.get_bool("produce_models", false); - m_max_restarts = p.get_uint("sls_restarts", (unsigned)-1); - m_tracker.set_random_seed(p.get_uint("random_seed", 0)); - m_plateau_limit = p.get_uint("plateau_limit", 100); + void updt_params(params_ref const & _p) { + sls_params p(_p); + m_produce_models = _p.get_bool("model", false); + m_max_restarts = p.restarts(); + m_tracker.set_random_seed(p.random_seed()); + m_plateau_limit = p.plateau_limit(); } void checkpoint() { @@ -1429,13 +175,13 @@ class sls_tactic : public tactic { } double rescore(goal_ref const & g) { - m_tracker.update_all(); + m_evaluator.update_all(); m_stats.m_full_evals++; return top_score(g); } double incremental_score(goal_ref const & g, func_decl * fd, const mpz & new_value) { - m_tracker.update(fd, new_value); + m_evaluator.update(fd, new_value); m_stats.m_incr_evals++; return top_score(g); } @@ -1539,7 +285,7 @@ class sls_tactic : public tactic { NOT_IMPLEMENTED_YET(); } - m_tracker.update(fd, new_value); + m_evaluator.update(fd, new_value); TRACE("sls", tout << "Randomization candidates: "; for (unsigned i = 0; i < unsat_constants.size(); i++) @@ -1713,7 +459,8 @@ class sls_tactic : public tactic { else { plateau_cnt++; if (plateau_cnt < m_plateau_limit) { - m_tracker.randomize_local(g); + TRACE("sls", tout << "In a plateau (" << plateau_cnt << "/" << m_plateau_limit << "); randomizing locally." << std::endl; ); + m_evaluator.randomize_local(g); //mk_random_move(g); score = top_score(g); } @@ -1890,13 +637,7 @@ tactic * mk_preamble(ast_manager & m, params_ref const & p) { } tactic * mk_qfbv_sls_tactic(ast_manager & m, params_ref const & p) { - params_ref sls_p(p); - sls_p.set_uint("sls_restarts", 10000); - sls_p.set_uint("plateau_limit", 100); - - tactic * t = and_then(mk_preamble(m, p), - using_params(mk_sls_tactic(m, p), sls_p)); - + tactic * t = and_then(mk_preamble(m, p), mk_sls_tactic(m)); t->updt_params(p); return t; } diff --git a/src/tactic/sls/sls_tracker.h b/src/tactic/sls/sls_tracker.h new file mode 100644 index 000000000..7fbafec60 --- /dev/null +++ b/src/tactic/sls/sls_tracker.h @@ -0,0 +1,675 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + sls_score_tracker.h + +Abstract: + + Score and value tracking module for SLS + +Author: + + Christoph (cwinter) 2012-02-29 + +Notes: + +--*/ + +#ifndef _SLS_TRACKER_H_ +#define _SLS_TRACKER_H_ + +class sls_tracker { + ast_manager & m_manager; + unsynch_mpz_manager & m_mpz_manager; + bv_util & m_bv_util; + powers & m_powers; + random_gen m_rng; + unsigned m_random_bits; + unsigned m_random_bits_cnt; + mpz m_zero, m_one, m_two; + + struct value_score { + value_score() : m(0), value(unsynch_mpz_manager::mk_z(0)), score(0.0), distance(0) { }; + ~value_score() { if (m) m->del(value); } + unsynch_mpz_manager * m; + mpz value; + double score; + unsigned distance; // max distance from any root + value_score & operator=(const value_score & other) { + SASSERT(m == 0 || m == other.m); + if (m) m->set(value, 0); else m = other.m; + m->set(value, other.value); + score = other.score; + distance = other.distance; + return *this; + } + }; + +public: + typedef obj_map entry_point_type; + +private: + typedef obj_map scores_type; + typedef obj_map > uplinks_type; + typedef obj_map > occ_type; + scores_type m_scores; + uplinks_type m_uplinks; + entry_point_type m_entry_points; + ptr_vector m_constants; + ptr_vector m_temp_constants; + occ_type m_constants_occ; + +public: + sls_tracker(ast_manager & m, bv_util & bvu, unsynch_mpz_manager & mm, powers & p) : + m_manager(m), + m_mpz_manager(mm), + m_bv_util(bvu), + m_powers(p), + m_random_bits_cnt(0), + m_zero(m_mpz_manager.mk_z(0)), + m_one(m_mpz_manager.mk_z(1)), + m_two(m_mpz_manager.mk_z(2)) { + } + + ~sls_tracker() { + m_mpz_manager.del(m_zero); + m_mpz_manager.del(m_one); + m_mpz_manager.del(m_two); + } + + inline void set_value(expr * n, const mpz & r) { + SASSERT(m_scores.contains(n)); + m_mpz_manager.set(m_scores.find(n).value, r); + } + + inline void set_value(func_decl * fd, const mpz & r) { + SASSERT(m_entry_points.contains(fd)); + expr * ep = get_entry_point(fd); + set_value(ep, r); + } + + inline mpz & get_value(expr * n) { + SASSERT(m_scores.contains(n)); + return m_scores.find(n).value; + } + + inline mpz & get_value(func_decl * fd) { + SASSERT(m_entry_points.contains(fd)); + expr * ep = get_entry_point(fd); + return get_value(ep); + } + + inline void set_score(expr * n, double score) { + SASSERT(m_scores.contains(n)); + m_scores.find(n).score = score; + } + + inline void set_score(func_decl * fd, double score) { + SASSERT(m_entry_points.contains(fd)); + expr * ep = get_entry_point(fd); + set_score(ep, score); + } + + inline double & get_score(expr * n) { + SASSERT(m_scores.contains(n)); + return m_scores.find(n).score; + } + + inline double & get_score(func_decl * fd) { + SASSERT(m_entry_points.contains(fd)); + expr * ep = get_entry_point(fd); + return get_score(ep); + } + + inline unsigned get_distance(expr * n) { + SASSERT(m_scores.contains(n)); + return m_scores.find(n).distance; + } + + inline void set_distance(expr * n, unsigned d) { + SASSERT(m_scores.contains(n)); + m_scores.find(n).distance = d; + } + + inline expr * get_entry_point(func_decl * fd) { + SASSERT(m_entry_points.contains(fd)); + return m_entry_points.find(fd); + } + + inline entry_point_type const & get_entry_points() { + return m_entry_points; + } + + inline bool has_uplinks(expr * n) { + return m_uplinks.contains(n); + } + + inline ptr_vector & get_uplinks(expr * n) { + SASSERT(m_uplinks.contains(n)); + return m_uplinks.find(n); + } + + void initialize(app * n) { + // Build score table + if (!m_scores.contains(n)) { + value_score vs; + vs.m = & m_mpz_manager; + m_scores.insert(n, vs); + } + + // Update uplinks + unsigned na = n->get_num_args(); + for (unsigned i = 0; i < na; i++) { + expr * c = n->get_arg(i); + uplinks_type::obj_map_entry * entry = m_uplinks.insert_if_not_there2(c, ptr_vector()); + entry->get_data().m_value.push_back(n); + } + + func_decl * d = n->get_decl(); + + if (n->get_num_args() == 0) { + if (d->get_family_id() != null_family_id) { + // Interpreted constant + mpz t; + value2mpz(n, t); + set_value(n, t); + m_mpz_manager.del(t); + } + else { + // Uninterpreted constant + m_entry_points.insert_if_not_there(d, n); + m_constants.push_back(d); + } + } + } + + struct init_proc { + ast_manager & m_manager; + sls_tracker & m_tracker; + + init_proc(ast_manager & m, sls_tracker & tracker): + m_manager(m), + m_tracker(tracker) { + } + + void operator()(var * n) {} + + void operator()(quantifier * n) {} + + void operator()(app * n) { + m_tracker.initialize(n); + } + }; + + struct find_func_decls_proc { + ast_manager & m_manager; + ptr_vector & m_occs; + + find_func_decls_proc (ast_manager & m, ptr_vector & occs): + m_manager(m), + m_occs(occs) { + } + + void operator()(var * n) {} + + void operator()(quantifier * n) {} + + void operator()(app * n) { + if (n->get_num_args() != 0) + return; + func_decl * d = n->get_decl(); + if (d->get_family_id() != null_family_id) + return; + m_occs.push_back(d); + } + }; + + void calculate_expr_distances(goal_ref const & g) { + // precondition: m_scores is set up. + unsigned sz = g->size(); + ptr_vector stack; + for (unsigned i = 0; i < sz; i++) + stack.push_back(to_app(g->form(i))); + while (!stack.empty()) { + app * cur = stack.back(); + stack.pop_back(); + + unsigned d = get_distance(cur); + + for (unsigned i = 0; i < cur->get_num_args(); i++) { + app * child = to_app(cur->get_arg(i)); + unsigned d_child = get_distance(child); + if (d >= d_child) { + set_distance(child, d+1); + stack.push_back(child); + } + } + } + } + + void initialize(goal_ref const & g) { + init_proc proc(m_manager, *this); + expr_mark visited; + unsigned sz = g->size(); + for (unsigned i = 0; i < sz; i++) { + expr * e = g->form(i); + for_each_expr(proc, visited, e); + } + + visited.reset(); + + for (unsigned i = 0; i < sz; i++) { + expr * e = g->form(i); + ptr_vector t; + m_constants_occ.insert_if_not_there(e, t); + find_func_decls_proc ffd_proc(m_manager, m_constants_occ.find(e)); + expr_fast_mark1 visited; + quick_for_each_expr(ffd_proc, visited, e); + } + + calculate_expr_distances(g); + + TRACE("sls", tout << "Initial model:" << std::endl; show_model(tout); ); + } + + void show_model(std::ostream & out) { + unsigned sz = get_num_constants(); + for (unsigned i = 0; i < sz; i++) { + func_decl * fd = get_constant(i); + out << fd->get_name() << " = " << m_mpz_manager.to_string(get_value(fd)) << std::endl; + } + } + + model_ref get_model() { + model_ref res = alloc(model, m_manager); + unsigned sz = get_num_constants(); + for (unsigned i = 0; i < sz; i++) { + func_decl * fd = get_constant(i); + res->register_decl(fd, mpz2value(fd->get_range(), get_value(fd))); + } + return res; + } + + unsigned get_num_constants() { + return m_constants.size(); + } + + ptr_vector & get_constants() { + return m_constants; + } + + func_decl * get_constant(unsigned i) { + return m_constants[i]; + } + + void set_random_seed(unsigned s) { + m_rng.set_seed(s); + } + + mpz get_random_bv(sort * s) { + SASSERT(m_bv_util.is_bv_sort(s)); + unsigned bv_size = m_bv_util.get_bv_size(s); + mpz r; m_mpz_manager.set(r, 0); + + mpz temp; + do + { + m_mpz_manager.mul(r, m_two, temp); + m_mpz_manager.add(temp, get_random_bool(), r); + } while (--bv_size > 0); + m_mpz_manager.del(temp); + + return r; + } + + mpz & get_random_bool() { + if (m_random_bits_cnt == 0) { + m_random_bits = m_rng(); + m_random_bits_cnt = 15; // random_gen produces 15 bits of randomness. + } + + bool val = (m_random_bits & 0x01) != 0; + m_random_bits = m_random_bits >> 1; + m_random_bits_cnt--; + + return (val) ? m_one : m_zero; + } + + unsigned get_random_uint(unsigned bits) { + if (m_random_bits_cnt == 0) { + m_random_bits = m_rng(); + m_random_bits_cnt = 15; // random_gen produces 15 bits of randomness. + } + + unsigned val = 0; + while (bits-- > 0) { + if ((m_random_bits & 0x01) != 0) val++; + val <<= 1; + m_random_bits >>= 1; + m_random_bits_cnt--; + + if (m_random_bits_cnt == 0) { + m_random_bits = m_rng(); + m_random_bits_cnt = 15; // random_gen produces 15 bits of randomness. + } + } + + return val; + } + + mpz get_random(sort * s) { + if (m_bv_util.is_bv_sort(s)) + return get_random_bv(s); + else if (m_manager.is_bool(s)) + return get_random_bool(); + else + NOT_IMPLEMENTED_YET(); // This only works for bit-vectors for now. + } + + void randomize() { + TRACE("sls", tout << "Abandoned model:" << std::endl; show_model(tout); ); + + for (entry_point_type::iterator it = m_entry_points.begin(); it != m_entry_points.end(); it++) { + func_decl * fd = it->m_key; + sort * s = fd->get_range(); + mpz temp = get_random(s); + set_value(it->m_value, temp); + m_mpz_manager.del(temp); + } + + TRACE("sls", tout << "Randomized model:" << std::endl; show_model(tout); ); + } + +#define _SCORE_AND_MIN + + double score_bool(expr * n, bool negated = false) { + TRACE("sls_score", tout << ((negated)?"NEG ":"") << "BOOL: " << mk_ismt2_pp(n, m_manager) << std::endl; ); + + double res = 0.0; + + if (is_uninterp_const(n)) { + const mpz & r = get_value(n); + if (negated) + res = (m_mpz_manager.is_one(r)) ? 0.0 : 1.0; + else + res = (m_mpz_manager.is_one(r)) ? 1.0 : 0.0; + } + else if (m_manager.is_and(n)) { + SASSERT(!negated); + app * a = to_app(n); + expr * const * args = a->get_args(); + #ifdef _SCORE_AND_MIN + double min = 1.0; + for (unsigned i = 0; i < a->get_num_args(); i++) { + double cur = get_score(args[i]); + if (cur < min) min = cur; + } + res = min; + #else + double sum = 0.0; + for (unsigned i = 0; i < a->get_num_args(); i++) + sum += get_score(args[i]); + res = sum / (double) a->get_num_args(); + #endif + } + else if (m_manager.is_or(n)) { + SASSERT(!negated); + app * a = to_app(n); + expr * const * args = a->get_args(); + double max = 0.0; + for (unsigned i = 0; i < a->get_num_args(); i++) { + double cur = get_score(args[i]); + if (cur > max) max = cur; + } + res = max; + } + else if (m_manager.is_ite(n)) { + SASSERT(!negated); + app * a = to_app(n); + SASSERT(a->get_num_args() == 3); + const mpz & cond = get_value(a->get_arg(0)); + double s_t = get_score(a->get_arg(1)); + double s_f = get_score(a->get_arg(2)); + res = (m_mpz_manager.is_one(cond)) ? s_t : s_f; + } + else if (m_manager.is_eq(n) || m_manager.is_iff(n)) { + app * a = to_app(n); + SASSERT(a->get_num_args() == 2); + expr * arg0 = a->get_arg(0); + expr * arg1 = a->get_arg(1); + const mpz & v0 = get_value(arg0); + const mpz & v1 = get_value(arg1); + + if (negated) { + res = (m_mpz_manager.eq(v0, v1)) ? 0.0 : 1.0; + TRACE("sls_score", tout << "V0 = " << m_mpz_manager.to_string(v0) << " ; V1 = " << + m_mpz_manager.to_string(v1) << std::endl; ); + } + else if (m_manager.is_bool(arg0)) { + res = m_mpz_manager.eq(v0, v1) ? 1.0 : 0.0; + TRACE("sls_score", tout << "V0 = " << m_mpz_manager.to_string(v0) << " ; V1 = " << + m_mpz_manager.to_string(v1) << std::endl; ); + } + else if (m_bv_util.is_bv(arg0)) { + mpz diff, diff_m1; + m_mpz_manager.bitwise_xor(v0, v1, diff); + unsigned hamming_distance = 0; + unsigned bv_sz = m_bv_util.get_bv_size(arg0); + #if 1 // unweighted hamming distance + while (!m_mpz_manager.is_zero(diff)) { + //m_mpz_manager.set(diff_m1, diff); + //m_mpz_manager.dec(diff_m1); + //m_mpz_manager.bitwise_and(diff, diff_m1, diff); + //hamming_distance++; + if (!m_mpz_manager.is_even(diff)) { + hamming_distance++; + } + m_mpz_manager.machine_div(diff, m_two, diff); + } + res = 1.0 - (hamming_distance / (double) bv_sz); + #else + rational r(diff); + r /= m_powers(bv_sz); + double dbl = r.get_double(); + res = (dbl < 0.0) ? 1.0 : (dbl > 1.0) ? 0.0 : 1.0 - dbl; + #endif + TRACE("sls_score", tout << "V0 = " << m_mpz_manager.to_string(v0) << " ; V1 = " << + m_mpz_manager.to_string(v1) << " ; HD = " << hamming_distance << + " ; SZ = " << bv_sz << std::endl; ); + m_mpz_manager.del(diff); + m_mpz_manager.del(diff_m1); + } + else + NOT_IMPLEMENTED_YET(); + } + else if (m_bv_util.is_bv_ule(n)) { // x <= y + app * a = to_app(n); + SASSERT(a->get_num_args() == 2); + const mpz & x = get_value(a->get_arg(0)); + const mpz & y = get_value(a->get_arg(1)); + unsigned bv_sz = m_bv_util.get_bv_size(a->get_decl()->get_domain()[0]); + + if (negated) { + if (m_mpz_manager.gt(x, y)) + res = 1.0; + else { + mpz diff; + m_mpz_manager.sub(y, x, diff); + m_mpz_manager.inc(diff); + rational n(diff); + n /= rational(m_powers(bv_sz)); + double dbl = n.get_double(); + // In extreme cases, n is 0.9999 but to_double returns something > 1.0 + res = (dbl > 1.0) ? 0.0 : (dbl < 0.0) ? 1.0 : 1.0 - dbl; + m_mpz_manager.del(diff); + } + } + else { + if (m_mpz_manager.le(x, y)) + res = 1.0; + else { + mpz diff; + m_mpz_manager.sub(x, y, diff); + rational n(diff); + n /= rational(m_powers(bv_sz)); + double dbl = n.get_double(); + res = (dbl > 1.0) ? 1.0 : (dbl < 0.0) ? 0.0 : dbl; + m_mpz_manager.del(diff); + } + } + TRACE("sls_score", tout << "x = " << m_mpz_manager.to_string(x) << " ; y = " << + m_mpz_manager.to_string(y) << " ; SZ = " << bv_sz << std::endl; ); + } + else if (m_bv_util.is_bv_sle(n)) { // x <= y + app * a = to_app(n); + SASSERT(a->get_num_args() == 2); + mpz x; m_mpz_manager.set(x, get_value(a->get_arg(0))); + mpz y; m_mpz_manager.set(y, get_value(a->get_arg(1))); + unsigned bv_sz = m_bv_util.get_bv_size(a->get_decl()->get_domain()[0]); + const mpz & p = m_powers(bv_sz); + const mpz & p_half = m_powers(bv_sz-1); + if (x >= p_half) { m_mpz_manager.sub(x, p, x); } + if (y >= p_half) { m_mpz_manager.sub(y, p, y); } + + if (negated) { + if (x > y) + res = 1.0; + else { + mpz diff; + m_mpz_manager.sub(y, x, diff); + m_mpz_manager.inc(diff); + rational n(diff); + n /= p; + double dbl = n.get_double(); + res = (dbl > 1.0) ? 0.0 : (dbl < 0.0) ? 1.0 : 1.0 - dbl; + m_mpz_manager.del(diff); + } + TRACE("sls_score", tout << "x = " << m_mpz_manager.to_string(x) << " ; y = " << + m_mpz_manager.to_string(y) << " ; SZ = " << bv_sz << std::endl; ); + } + else { + if (x <= y) + res = 1.0; + else { + mpz diff; + m_mpz_manager.sub(x, y, diff); + rational n(diff); + n /= p; + double dbl = n.get_double(); + res = (dbl > 1.0) ? 1.0 : (dbl < 0.0) ? 0.0 : dbl; + m_mpz_manager.del(diff); + } + TRACE("sls_score", tout << "x = " << m_mpz_manager.to_string(x) << " ; y = " << + m_mpz_manager.to_string(y) << " ; SZ = " << bv_sz << std::endl; ); + } + m_mpz_manager.del(x); + m_mpz_manager.del(y); + } + else if (m_manager.is_not(n)) { + SASSERT(!negated); + app * a = to_app(n); + SASSERT(a->get_num_args() == 1); + expr * child = a->get_arg(0); + if (m_manager.is_and(child) || m_manager.is_or(child)) // Precondition: Assertion set is in NNF. + NOT_IMPLEMENTED_YET(); + res = score_bool(child, true); + } + else if (m_manager.is_distinct(n)) { + app * a = to_app(n); + unsigned pairs = 0, distinct_pairs = 0; + unsigned sz = a->get_num_args(); + for (unsigned i = 0; i < sz; i++) { + for (unsigned j = i+1; j < sz; j++) { + // pair i/j + const mpz & v0 = get_value(a->get_arg(0)); + const mpz & v1 = get_value(a->get_arg(1)); + pairs++; + if (v0 != v1) + distinct_pairs++; + } + } + res = (distinct_pairs/(double)pairs); + if (negated) res = 1.0 - res; + } + else + NOT_IMPLEMENTED_YET(); + + SASSERT(res >= 0.0 && res <= 1.0); + + TRACE("sls_score", tout << "SCORE = " << res << std::endl; ); + return res; + } + + double score_bv(expr * n) { + return 0.0; // a bv-expr is always scored as 0.0; we won't use those scores. + } + + void value2mpz(expr * n, mpz & result) { + m_mpz_manager.set(result, m_zero); + + if (m_manager.is_bool(n)) { + m_mpz_manager.set(result, m_manager.is_true(n) ? m_one : m_zero); + } + else if (m_bv_util.is_bv(n)) { + unsigned bv_sz = m_bv_util.get_bv_size(n); + rational q; + if (!m_bv_util.is_numeral(n, q, bv_sz)) + NOT_IMPLEMENTED_YET(); + mpq temp = q.to_mpq(); + SASSERT(m_mpz_manager.is_one(temp.denominator())); + m_mpz_manager.set(result, temp.numerator()); + } + else + NOT_IMPLEMENTED_YET(); + } + + expr_ref mpz2value(sort * s, const mpz & r) { + expr_ref res(m_manager); + if (m_manager.is_bool(s)) + res = (m_mpz_manager.is_zero(r)) ? m_manager.mk_false() : m_manager.mk_true(); + else if (m_bv_util.is_bv_sort(s)) { + rational rat(r); + res = m_bv_util.mk_numeral(rat, s); + } + else + NOT_IMPLEMENTED_YET(); + return res; + } + + double score(expr * n) { + if (m_manager.is_bool(n)) + return score_bool(n); + else if (m_bv_util.is_bv(n)) + return score_bv(n); + else + NOT_IMPLEMENTED_YET(); + } + + ptr_vector & get_unsat_constants(goal_ref const & g) { + unsigned sz = g->size(); + + if (sz == 1) { + return get_constants(); + } + else { + m_temp_constants.reset(); + for (unsigned i = 0; i < sz; i++) { + expr * q = g->form(i); + if (m_mpz_manager.eq(get_value(q), m_one)) + continue; + ptr_vector const & this_decls = m_constants_occ.find(q); + unsigned sz2 = this_decls.size(); + for (unsigned j = 0; j < sz2; j++) { + func_decl * fd = this_decls[j]; + if (!m_temp_constants.contains(fd)) + m_temp_constants.push_back(fd); + } + } + return m_temp_constants; + } + } +}; + +#endif \ No newline at end of file From 41c9e2b1a47e23959f66fc655e3e142fd2864919 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 20 Sep 2013 11:27:52 -0700 Subject: [PATCH 04/27] check equalities with unknown evaluations Signed-off-by: Nikolaj Bjorner --- src/muz/pdr/pdr_util.cpp | 18 +++++++++++++++--- 1 file changed, 15 insertions(+), 3 deletions(-) diff --git a/src/muz/pdr/pdr_util.cpp b/src/muz/pdr/pdr_util.cpp index d021d5fb1..f122f1e2c 100644 --- a/src/muz/pdr/pdr_util.cpp +++ b/src/muz/pdr/pdr_util.cpp @@ -112,8 +112,8 @@ namespace pdr { set_value(e, val); } else { - IF_VERBOSE(3, verbose_stream() << "Not evaluated " << mk_pp(e, m) << "\n";); - TRACE("pdr", tout << "Variable is not tracked: " << mk_pp(e, m) << "\n";); + IF_VERBOSE(3, verbose_stream() << "Not evaluated " << mk_pp(e, m) << " := " << mk_pp(val, m) << "\n";); + TRACE("pdr", tout << "Variable is not tracked: " << mk_pp(e, m) << " := " << mk_pp(val, m) << "\n";); set_x(e); } } @@ -672,7 +672,19 @@ namespace pdr { eval_array_eq(e, arg1, arg2); } else if (is_x(arg1) || is_x(arg2)) { - set_x(e); + expr_ref eq(m), vl(m); + eq = m.mk_eq(arg1, arg2); + m_model->eval(eq, vl); + if (m.is_true(vl)) { + set_bool(e, true); + } + else if (m.is_false(vl)) { + set_bool(e, false); + } + else { + TRACE("pdr", tout << "cannot evaluate: " << mk_pp(vl, m) << "\n";); + set_x(e); + } } else if (m.is_bool(arg1)) { bool val = is_true(arg1) == is_true(arg2); From 0a964c324eba0b511c11b14f76c253d55b8d0e0c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 20 Sep 2013 12:32:16 -0700 Subject: [PATCH 05/27] test for undetermined accessor for PDR Signed-off-by: Nikolaj Bjorner --- src/muz/base/dl_context.cpp | 2 +- src/muz/base/dl_rule.cpp | 19 ++++++++++++++++--- src/muz/base/dl_rule.h | 2 +- 3 files changed, 18 insertions(+), 5 deletions(-) diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp index f08efb00a..8183744b5 100644 --- a/src/muz/base/dl_context.cpp +++ b/src/muz/base/dl_context.cpp @@ -576,7 +576,7 @@ namespace datalog { void context::check_uninterpreted_free(rule_ref& r) { func_decl* f = 0; - if (r->has_uninterpreted_non_predicates(f)) { + if (r->has_uninterpreted_non_predicates(m, f)) { std::stringstream stm; stm << "Uninterpreted '" << f->get_name() diff --git a/src/muz/base/dl_rule.cpp b/src/muz/base/dl_rule.cpp index 96e2b163a..184a5fa02 100644 --- a/src/muz/base/dl_rule.cpp +++ b/src/muz/base/dl_rule.cpp @@ -43,6 +43,7 @@ Revision History: #include"expr_safe_replace.h" #include"filter_model_converter.h" #include"scoped_proof.h" +#include"datatype_decl_plugin.h" namespace datalog { @@ -881,9 +882,12 @@ namespace datalog { } struct uninterpreted_function_finder_proc { + ast_manager& m; + datatype_util m_dt; bool m_found; func_decl* m_func; - uninterpreted_function_finder_proc() : m_found(false), m_func(0) {} + uninterpreted_function_finder_proc(ast_manager& m): + m(m), m_dt(m), m_found(false), m_func(0) {} void operator()(var * n) { } void operator()(quantifier * n) { } void operator()(app * n) { @@ -891,6 +895,14 @@ namespace datalog { m_found = true; m_func = n->get_decl(); } + else if (m_dt.is_accessor(n)) { + sort* s = m.get_sort(n->get_arg(0)); + SASSERT(m_dt.is_datatype(s)); + if (m_dt.get_datatype_constructors(s)->size() > 1) { + m_found = true; + m_func = n->get_decl(); + } + } } bool found(func_decl*& f) const { f = m_func; return m_found; } @@ -900,9 +912,9 @@ namespace datalog { // non-predicates may appear only in the interpreted tail, it is therefore // sufficient only to check the tail. // - bool rule::has_uninterpreted_non_predicates(func_decl*& f) const { + bool rule::has_uninterpreted_non_predicates(ast_manager& m, func_decl*& f) const { unsigned sz = get_tail_size(); - uninterpreted_function_finder_proc proc; + uninterpreted_function_finder_proc proc(m); expr_mark visited; for (unsigned i = get_uninterpreted_tail_size(); i < sz && !proc.found(f); ++i) { for_each_expr(proc, visited, get_tail(i)); @@ -910,6 +922,7 @@ namespace datalog { return proc.found(f); } + struct quantifier_finder_proc { bool m_exist; bool m_univ; diff --git a/src/muz/base/dl_rule.h b/src/muz/base/dl_rule.h index 77bf9ac74..1c31dc6b4 100644 --- a/src/muz/base/dl_rule.h +++ b/src/muz/base/dl_rule.h @@ -293,7 +293,7 @@ namespace datalog { */ bool is_in_tail(const func_decl * p, bool only_positive=false) const; - bool has_uninterpreted_non_predicates(func_decl*& f) const; + bool has_uninterpreted_non_predicates(ast_manager& m, func_decl*& f) const; void has_quantifiers(bool& existential, bool& universal) const; bool has_quantifiers() const; bool has_negation() const; From fd1f4b91911cb9628e3419244fcb3646540bad97 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 23 Sep 2013 04:07:08 +0300 Subject: [PATCH 06/27] fix bugs reported by Anvesh Signed-off-by: Nikolaj Bjorner --- src/api/python/z3.py | 2 +- src/smt/diff_logic.h | 7 +++++++ src/smt/theory_utvpi_def.h | 3 ++- 3 files changed, 10 insertions(+), 2 deletions(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 739a9e61a..f68457383 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -6449,7 +6449,7 @@ class Tactic: def _to_goal(a): if isinstance(a, BoolRef): - goal = Goal() + goal = Goal(a.ctx) goal.add(a) return goal else: diff --git a/src/smt/diff_logic.h b/src/smt/diff_logic.h index 6fd156e41..2717e4a92 100644 --- a/src/smt/diff_logic.h +++ b/src/smt/diff_logic.h @@ -820,6 +820,7 @@ public: } } +private: // Update the assignment of variable v, that is, // m_assignment[v] += inc // This method also stores the old value of v in the assignment stack. @@ -829,6 +830,12 @@ public: m_assignment[v] += inc; } +public: + + void inc_assignment(dl_var v, numeral const& inc) { + m_assignment[v] += inc; + } + struct every_var_proc { bool operator()(dl_var v) const { diff --git a/src/smt/theory_utvpi_def.h b/src/smt/theory_utvpi_def.h index 8463eb17f..6039b208a 100644 --- a/src/smt/theory_utvpi_def.h +++ b/src/smt/theory_utvpi_def.h @@ -752,7 +752,8 @@ namespace smt { for (unsigned j = 0; j < zero_v.size(); ++j) { int v = zero_v[j]; - m_graph.acc_assignment(v, numeral(-1)); + + m_graph.inc_assignment(v, numeral(-1)); th_var k = from_var(v); if (!is_parity_ok(k)) { todo.push_back(k); From 2e7f5303ebfe9fe7e77da8af34d97bf7063b0844 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 23 Sep 2013 04:56:38 +0300 Subject: [PATCH 07/27] address incompleteness bug in axiomatization of int2bv Signed-off-by: Nikolaj Bjorner --- src/smt/theory_bv.cpp | 31 +++++++++++++++++++++++++++---- 1 file changed, 27 insertions(+), 4 deletions(-) diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index 559ce155b..a338be50a 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -581,10 +581,13 @@ namespace smt { void theory_bv::assert_int2bv_axiom(app* n) { // // create the axiom: - // bv2int(n) = e mod 2^bit_width - // + // bv2int(n) = e mod 2^bit_width // where n = int2bv(e) // + // Create the axioms: + // bit2bool(i,n) == ((e div 2^i) mod 2 != 0) + // for i = 0,.., sz-1 + // SASSERT(get_context().e_internalized(n)); SASSERT(m_util.is_int2bv(n)); ast_manager & m = get_manager(); @@ -592,10 +595,12 @@ namespace smt { parameter param(m_autil.mk_int()); expr* n_expr = n; - expr* lhs = m.mk_app(get_id(), OP_BV2INT, 1, ¶m, 1, &n_expr); + expr* e = n->get_arg(0); + expr_ref lhs(m), rhs(m); + lhs = m.mk_app(get_id(), OP_BV2INT, 1, ¶m, 1, &n_expr); unsigned sz = m_util.get_bv_size(n); numeral mod = power(numeral(2), sz); - expr* rhs = m_autil.mk_mod(n->get_arg(0), m_autil.mk_numeral(mod, true)); + rhs = m_autil.mk_mod(e, m_autil.mk_numeral(mod, true)); literal l(mk_eq(lhs, rhs, false)); ctx.mark_as_relevant(l); @@ -605,6 +610,24 @@ namespace smt { tout << mk_pp(lhs, m) << " == \n"; tout << mk_pp(rhs, m) << "\n"; ); + + expr_ref_vector n_bits(m); + enode * n_enode = mk_enode(n); + get_bits(n_enode, n_bits); + + for (unsigned i = 0; i < sz; ++i) { + numeral div = power(numeral(2), i); + mod = numeral(2); + rhs = m_autil.mk_idiv(e, m_autil.mk_numeral(div,true)); + rhs = m_autil.mk_mod(rhs, m_autil.mk_numeral(mod, true)); + rhs = m.mk_eq(rhs, m_autil.mk_numeral(rational(1), true)); + lhs = n_bits.get(i); + TRACE("bv", tout << mk_pp(lhs, m) << " == " << mk_pp(rhs, m) << "\n";); + l = literal(mk_eq(lhs, rhs, false)); + ctx.mark_as_relevant(l); + ctx.mk_th_axiom(get_id(), 1, &l); + + } } From c1384095f356a478d91ec08759ed86d053d06b9c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 23 Sep 2013 21:44:24 +0300 Subject: [PATCH 08/27] fix default argument identification Signed-off-by: Nikolaj Bjorner --- src/api/python/z3.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index f68457383..aaad24256 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -6449,7 +6449,7 @@ class Tactic: def _to_goal(a): if isinstance(a, BoolRef): - goal = Goal(a.ctx) + goal = Goal(ctx = a.ctx) goal.add(a) return goal else: From 6554ac787a5cd53e60801f9df739da2cf87e0e60 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 24 Sep 2013 05:13:11 +0300 Subject: [PATCH 09/27] add test case for substitution Signed-off-by: Nikolaj Bjorner --- src/test/expr_substitution.cpp | 50 ++++++++++++++++++++++++++++++++++ src/test/main.cpp | 1 + 2 files changed, 51 insertions(+) create mode 100644 src/test/expr_substitution.cpp diff --git a/src/test/expr_substitution.cpp b/src/test/expr_substitution.cpp new file mode 100644 index 000000000..915ac96f3 --- /dev/null +++ b/src/test/expr_substitution.cpp @@ -0,0 +1,50 @@ +#include "expr_substitution.h" +#include "smt_params.h" +#include "substitution.h" +#include "unifier.h" +#include "bv_decl_plugin.h" +#include "ast_pp.h" +#include "arith_decl_plugin.h" +#include "reg_decl_plugins.h" +#include "th_rewriter.h" + +expr* mk_bv_xor(bv_util& bv, expr* a, expr* b) { + expr* args[2]; + args[0] = a; + args[1] = b; + return bv.mk_bv_xor(2, args); +} + +expr* mk_bv_and(bv_util& bv, expr* a, expr* b) { + expr* args[2]; + args[0] = a; + args[1] = b; + ast_manager& m = bv.get_manager(); + return m.mk_app(bv.get_family_id(), OP_BAND, 2, args); +} + +void tst_expr_substitution() { + memory::initialize(0); + ast_manager m; + reg_decl_plugins(m); + bv_util bv(m); + + expr_ref a(m), b(m), c(m); + expr_ref x(m); + x = m.mk_const(symbol("x"), bv.mk_sort(8)); + a = mk_bv_and(bv, mk_bv_xor(bv, x,bv.mk_numeral(8,8)), mk_bv_xor(bv,x,x)); + b = x; + c = bv.mk_bv_sub(x, bv.mk_numeral(4, 8)); + + expr_substitution subst(m); + subst.insert(b, c); + th_rewriter rw(m); + rw.set_substitution(&subst); + + expr_ref new_a(m); + proof_ref pr(m); + rw(a, new_a, pr); + + std::cout << mk_pp(new_a, m) << "\n"; + +} diff --git a/src/test/main.cpp b/src/test/main.cpp index 333456369..bc7e04124 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -215,6 +215,7 @@ int main(int argc, char ** argv) { TST(rcf); TST(polynorm); TST(qe_arith); + TST(expr_substitution); } void initialize_mam() {} From 1733af2641e0d0b37ef3adf2ad5a6c8090ffdab3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 24 Sep 2013 05:33:16 +0300 Subject: [PATCH 10/27] test case for non-termination of substitution/rewriting Signed-off-by: Nikolaj Bjorner --- src/test/expr_substitution.cpp | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) diff --git a/src/test/expr_substitution.cpp b/src/test/expr_substitution.cpp index 915ac96f3..f83bde97d 100644 --- a/src/test/expr_substitution.cpp +++ b/src/test/expr_substitution.cpp @@ -29,20 +29,26 @@ void tst_expr_substitution() { reg_decl_plugins(m); bv_util bv(m); - expr_ref a(m), b(m), c(m); + expr_ref a(m), b(m), c(m), d(m); expr_ref x(m); + expr_ref new_a(m); + proof_ref pr(m); x = m.mk_const(symbol("x"), bv.mk_sort(8)); a = mk_bv_and(bv, mk_bv_xor(bv, x,bv.mk_numeral(8,8)), mk_bv_xor(bv,x,x)); b = x; c = bv.mk_bv_sub(x, bv.mk_numeral(4, 8)); expr_substitution subst(m); - subst.insert(b, c); th_rewriter rw(m); + + // normalizing c does not help. + rw(c, d, pr); + subst.insert(b, d); + rw.set_substitution(&subst); - - expr_ref new_a(m); - proof_ref pr(m); + + + enable_trace("th_rewriter_step"); rw(a, new_a, pr); std::cout << mk_pp(new_a, m) << "\n"; From 2d01c4d50f77963028ea39b45f89896502495c5e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 24 Sep 2013 06:41:46 +0300 Subject: [PATCH 11/27] update join planner to take projected columns into account Signed-off-by: Nikolaj Bjorner --- src/muz/rel/dl_mk_simple_joins.cpp | 145 ++++++++++++++++------------- 1 file changed, 82 insertions(+), 63 deletions(-) diff --git a/src/muz/rel/dl_mk_simple_joins.cpp b/src/muz/rel/dl_mk_simple_joins.cpp index 4b9ce582a..c2214dad9 100644 --- a/src/muz/rel/dl_mk_simple_joins.cpp +++ b/src/muz/rel/dl_mk_simple_joins.cpp @@ -47,9 +47,9 @@ namespace datalog { being notified about it, it will surely see the decrease from length 3 to 2 which the threshold for rule being counted in this counter. */ - unsigned m_consumers; - bool m_stratified; - unsigned m_src_stratum; + unsigned m_consumers; + bool m_stratified; + unsigned m_src_stratum; public: var_idx_set m_all_nonlocal_vars; rule_vector m_rules; @@ -57,16 +57,13 @@ namespace datalog { pair_info() : m_consumers(0), m_stratified(true), m_src_stratum(0) {} bool can_be_joined() const { - return m_consumers>0; + return m_consumers > 0; } cost get_cost() const { - /*if(m_instantiated) { - return std::numeric_limits::min(); - }*/ - SASSERT(m_consumers>0); + SASSERT(m_consumers > 0); cost amortized = m_total_cost/m_consumers; - if(m_stratified) { + if (m_stratified) { return amortized * ( (amortized>0) ? (1/16.0f) : 16.0f); } else { @@ -81,19 +78,20 @@ namespace datalog { by the time of a call to this function */ void add_rule(join_planner & pl, app * t1, app * t2, rule * r, - const var_idx_set & non_local_vars_normalized) { - if(m_rules.empty()) { - m_total_cost = pl.compute_cost(t1, t2); + const var_idx_set & non_local_vars_normalized, + const var_idx_set & non_local_vars) { + if (m_rules.empty()) { + m_total_cost = pl.compute_cost(t1, t2, non_local_vars); m_src_stratum = std::max(pl.get_stratum(t1->get_decl()), pl.get_stratum(t2->get_decl())); } m_rules.push_back(r); - if(pl.m_rules_content.find_core(r)->get_data().m_value.size()>2) { + if (pl.m_rules_content.find(r).size()>2) { m_consumers++; } - if(m_stratified) { + if (m_stratified) { unsigned head_stratum = pl.get_stratum(r->get_decl()); SASSERT(head_stratum>=m_src_stratum); - if(head_stratum==m_src_stratum) { + if (head_stratum==m_src_stratum) { m_stratified = false; } } @@ -105,7 +103,7 @@ namespace datalog { */ bool remove_rule(rule * r, unsigned original_length) { TRUSTME( remove_from_vector(m_rules, r) ); - if(original_length>2) { + if (original_length>2) { SASSERT(m_consumers>0); m_consumers--; } @@ -165,7 +163,7 @@ namespace datalog { SASSERT(is_var(t->get_arg(i))); var * v = to_var(t->get_arg(i)); unsigned var_idx = v->get_idx(); - if(result[res_ofs-var_idx]==0) { + if (result[res_ofs-var_idx]==0) { result[res_ofs-var_idx]=m.mk_var(next_var, v->get_sort()); next_var++; } @@ -174,7 +172,7 @@ namespace datalog { void get_normalizer(app * t1, app * t2, expr_ref_vector & result) const { SASSERT(result.empty()); - if(t1->get_num_args()==0 && t2->get_num_args()==0) { + if (t1->get_num_args()==0 && t2->get_num_args()==0) { return; //nothing to normalize } SASSERT(!t1->is_ground() || !t2->is_ground()); @@ -186,14 +184,14 @@ namespace datalog { var_idx_set::iterator ovend = orig_var_set.end(); for(; ovit!=ovend; ++ovit) { unsigned var_idx = *ovit; - if(var_idx>max_var_idx) { + if (var_idx>max_var_idx) { max_var_idx = var_idx; } } } - if(t1->get_decl()!=t2->get_decl()) { - if(t1->get_decl()->get_id()get_decl()->get_id()) { + if (t1->get_decl()!=t2->get_decl()) { + if (t1->get_decl()->get_id()get_decl()->get_id()) { std::swap(t1, t2); } } @@ -207,9 +205,9 @@ namespace datalog { //so the only literals which appear in pairs are the ones that contain only variables. var * v1 = to_var(t1->get_arg(i)); var * v2 = to_var(t2->get_arg(i)); - if(v1->get_sort()!=v2->get_sort()) { + if (v1->get_sort()!=v2->get_sort()) { //different sorts mean we can distinguish the two terms - if(v1->get_sort()->get_id()get_sort()->get_id()) { + if (v1->get_sort()->get_id()get_sort()->get_id()) { std::swap(t1, t2); } break; @@ -221,9 +219,9 @@ namespace datalog { SASSERT(norm1[v1_idx]==-1); SASSERT(norm2[v2_idx]==-1); - if(norm2[v1_idx]!=norm1[v2_idx]) { + if (norm2[v1_idx]!=norm1[v2_idx]) { //now we can distinguish the two terms - if(norm2[v1_idx]t2n) { + if (t1n>t2n) { std::swap(t1n, t2n); } m_pinned.push_back(t1n); @@ -274,12 +272,10 @@ namespace datalog { by the time of a call to this function */ void register_pair(app * t1, app * t2, rule * r, const var_idx_set & non_local_vars) { - TRACE("dl", tout << mk_pp(t1, m) << " " << mk_pp(t2, m) << "\n"; - r->display(m_context, tout); tout << "\n";); SASSERT(t1!=t2); cost_map::entry * e = m_costs.insert_if_not_there2(get_key(t1, t2), 0); pair_info * & ptr_inf = e->get_data().m_value; - if(ptr_inf==0) { + if (ptr_inf==0) { ptr_inf = alloc(pair_info); } pair_info & inf = *ptr_inf; @@ -288,25 +284,30 @@ namespace datalog { get_normalizer(t1, t2, normalizer); unsigned norm_ofs = normalizer.size()-1; var_idx_set normalized_vars; - var_idx_set::iterator vit = non_local_vars.begin(); + var_idx_set::iterator vit = non_local_vars.begin(); var_idx_set::iterator vend = non_local_vars.end(); for(; vit!=vend; ++vit) { unsigned norm_var = to_var(normalizer.get(norm_ofs-*vit))->get_idx(); normalized_vars.insert(norm_var); } - inf.add_rule(*this, t1, t2, r, normalized_vars); + inf.add_rule(*this, t1, t2, r, normalized_vars, non_local_vars); + TRACE("dl", tout << mk_pp(t1, m) << " " << mk_pp(t2, m) << " "; + vit = non_local_vars.begin(); + for (; vit != vend; ++vit) tout << *vit << " "; + tout << "\n"; + r->display(m_context, tout); + if (inf.can_be_joined()) tout << "cost: " << inf.get_cost() << "\n";); + } pair_info & get_pair(app_pair key) const { - cost_map::entry * e = m_costs.find_core(key); - SASSERT(e); - return *e->get_data().m_value; + return *m_costs.find(key); } void remove_rule_from_pair(app_pair key, rule * r, unsigned original_len) { pair_info * ptr = &get_pair(key); - if(ptr->remove_rule(r, original_len)) { + if (ptr->remove_rule(r, original_len)) { SASSERT(ptr->m_rules.empty()); m_costs.remove(key); dealloc(ptr); @@ -349,7 +350,7 @@ namespace datalog { unsigned n=t->get_num_args(); for(unsigned i=0; iget_arg(i)); - if(v->get_idx()==var_idx) { + if (v->get_idx()==var_idx) { args.push_back(v); domain.push_back(m.get_sort(v)); return true; @@ -375,7 +376,7 @@ namespace datalog { unsigned var_idx=*ovit; bool found=extract_argument_info(var_idx, t1, args, domain); - if(!found) { + if (!found) { found=extract_argument_info(var_idx, t2, args, domain); } SASSERT(found); @@ -389,7 +390,7 @@ namespace datalog { func_decl* parent_head = one_parent->get_decl(); const char * one_parent_name = parent_head->get_name().bare_str(); std::string parent_name; - if(inf.m_rules.size()>1) { + if (inf.m_rules.size()>1) { parent_name = one_parent_name + std::string("_and_") + to_string(inf.m_rules.size()-1); } else { @@ -443,7 +444,7 @@ namespace datalog { } //remove edges between surviving tails and removed tails for(unsigned i=0; i & rule_content = m_rules_content.find_core(r)->get_data().m_value; + ptr_vector & rule_content = m_rules_content.find(r); unsigned len = rule_content.size(); - if(len==1) { + if (len==1) { return; } @@ -515,16 +516,16 @@ namespace datalog { ptr_vector added_tails; for(unsigned i1=0; i1get_decl()!=t1_pred) { + if (rt1->get_decl()!=t1_pred) { continue; } unsigned i2start = (t1_pred==t2_pred) ? (i1+1) : 0; for(unsigned i2=i2start; i2get_decl()!=t2_pred) { + if (i1==i2 || rt2->get_decl()!=t2_pred) { continue; } - if(get_key(rt1, rt2)!=pair_key) { + if (get_key(rt1, rt2)!=pair_key) { continue; } expr_ref_vector normalizer(m); @@ -558,7 +559,7 @@ namespace datalog { relation_sort sort = pred->get_domain(arg_index); return static_cast(m_context.get_sort_size_estimate(sort)); //unsigned sz; - //if(!m_context.get_sort_size(sort, sz)) { + //if (!m_context.get_sort_size(sort, sz)) { // sz=UINT_MAX; //} //return static_cast(sz); @@ -576,15 +577,15 @@ namespace datalog { return cost(1); } relation_manager& rm = rel->get_rmanager(); - if( (m_context.saturation_was_run() && rm.try_get_relation(pred)) + if ( (m_context.saturation_was_run() && rm.try_get_relation(pred)) || rm.is_saturated(pred)) { SASSERT(rm.try_get_relation(pred)); //if it is saturated, it should exist unsigned rel_size_int = rel->get_relation(pred).get_size_estimate_rows(); - if(rel_size_int!=0) { + if (rel_size_int!=0) { cost rel_size = static_cast(rel_size_int); cost curr_size = rel_size; for(unsigned i=0; iget_arg(i))) { + if (!is_var(t->get_arg(i))) { curr_size /= get_domain_size(pred, i); } } @@ -593,40 +594,58 @@ namespace datalog { } cost res = 1; for(unsigned i=0; iget_arg(i))) { + if (is_var(t->get_arg(i))) { res *= get_domain_size(pred, i); } } return res; } - cost compute_cost(app * t1, app * t2) const { + cost compute_cost(app * t1, app * t2, const var_idx_set & non_local_vars) const { func_decl * t1_pred = t1->get_decl(); func_decl * t2_pred = t2->get_decl(); cost inters_size = 1; variable_intersection vi(m_context.get_manager()); vi.populate(t1, t2); unsigned n = vi.size(); + // remove contributions from joined columns. for(unsigned i=0; iget_arg(arg_index1))); + if (non_local_vars.contains(to_var(t1->get_arg(arg_index1))->get_idx())) { + inters_size *= get_domain_size(t1_pred, arg_index1); + } //joined arguments must have the same domain SASSERT(get_domain_size(t1_pred, arg_index1)==get_domain_size(t2_pred, arg_index2)); } - cost res = estimate_size(t1)*estimate_size(t2)/(inters_size*inters_size); + // remove contributions from projected columns. + for (unsigned i = 0; i < t1->get_num_args(); ++i) { + if (is_var(t1->get_arg(i)) && + !non_local_vars.contains(to_var(t1->get_arg(i))->get_idx())) { + inters_size *= get_domain_size(t1_pred, i); + } + } + for (unsigned i = 0; i < t2->get_num_args(); ++i) { + if (is_var(t2->get_arg(i)) && + !non_local_vars.contains(to_var(t2->get_arg(i))->get_idx())) { + inters_size *= get_domain_size(t2_pred, i); + } + } + + cost res = estimate_size(t1)*estimate_size(t2)/ inters_size; // (inters_size*inters_size); //cost res = -inters_size; /*unsigned t1_strat = get_stratum(t1_pred); SASSERT(t1_strat<=m_head_stratum); - if(t1_strat0) { + if (res>0) { res /= 2; } else { @@ -653,17 +672,17 @@ namespace datalog { for(; it!=end; ++it) { app_pair key = it->m_key; pair_info & inf = *it->m_value; - if(!inf.can_be_joined()) { + if (!inf.can_be_joined()) { continue; } cost c = inf.get_cost(); - if(!found || cm_key; ptr_vector content = rcit->m_value; SASSERT(content.size()<=2); - if(content.size()==orig_r->get_positive_tail_size()) { + if (content.size()==orig_r->get_positive_tail_size()) { //rule did not change result->add_rule(orig_r); continue; @@ -728,7 +747,7 @@ namespace datalog { rule_set * mk_simple_joins::operator()(rule_set const & source) { rule_set rs_aux_copy(m_context); rs_aux_copy.replace_rules(source); - if(!rs_aux_copy.is_closed()) { + if (!rs_aux_copy.is_closed()) { rs_aux_copy.close(); } From 1b8d1a1ccc4cff6bd6889b1bae27b24d4cd426ff Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 24 Sep 2013 10:42:31 +0300 Subject: [PATCH 12/27] fix bug in ackerman reduction found by Anvesh Signed-off-by: Nikolaj Bjorner --- src/muz/transforms/dl_mk_array_blast.cpp | 116 +++++++++++++++-------- src/muz/transforms/dl_mk_array_blast.h | 3 +- 2 files changed, 79 insertions(+), 40 deletions(-) diff --git a/src/muz/transforms/dl_mk_array_blast.cpp b/src/muz/transforms/dl_mk_array_blast.cpp index 776a2da5b..93e31ff23 100644 --- a/src/muz/transforms/dl_mk_array_blast.cpp +++ b/src/muz/transforms/dl_mk_array_blast.cpp @@ -31,7 +31,6 @@ namespace datalog { rm(ctx.get_rule_manager()), m_rewriter(m, m_params), m_simplifier(ctx), - m_sub(m), m_next_var(0) { m_params.set_bool("expand_select_store",true); m_rewriter.updt_params(m_params); @@ -82,7 +81,6 @@ namespace datalog { return false; } if (v) { - m_sub.insert(e, v); m_defs.insert(e, to_var(v)); } else { @@ -92,71 +90,113 @@ namespace datalog { m_next_var = vars.size() + 1; } v = m.mk_var(m_next_var, m.get_sort(e)); - m_sub.insert(e, v); m_defs.insert(e, v); ++m_next_var; } return true; } + + bool mk_array_blast::is_select_eq_var(expr* e, app*& s, var*& v) const { + expr* x, *y; + if (m.is_eq(e, x, y) || m.is_iff(e, x, y)) { + if (a.is_select(y)) { + std::swap(x,y); + } + if (a.is_select(x) && is_var(y)) { + s = to_app(x); + v = to_var(y); + return true; + } + } + return false; + } + bool mk_array_blast::ackermanize(rule const& r, expr_ref& body, expr_ref& head) { - expr_ref_vector conjs(m); + expr_ref_vector conjs(m), trail(m); qe::flatten_and(body, conjs); m_defs.reset(); - m_sub.reset(); m_next_var = 0; ptr_vector todo; - todo.push_back(head); + obj_map cache; + ptr_vector args; + app_ref e1(m); + app* s; + var* v; + for (unsigned i = 0; i < conjs.size(); ++i) { expr* e = conjs[i].get(); - expr* x, *y; - if (m.is_eq(e, x, y) || m.is_iff(e, x, y)) { - if (a.is_select(y)) { - std::swap(x,y); - } - if (a.is_select(x) && is_var(y)) { - if (!insert_def(r, to_app(x), to_var(y))) { - return false; - } - } + if (is_select_eq_var(e, s, v)) { + todo.append(s->get_num_args(), s->get_args()); } - if (a.is_select(e) && !insert_def(r, to_app(e), 0)) { - return false; + else { + todo.push_back(e); } - todo.push_back(e); } - // now make sure to cover all occurrences. - ast_mark mark; while (!todo.empty()) { expr* e = todo.back(); - todo.pop_back(); - if (mark.is_marked(e)) { + if (cache.contains(e)) { + todo.pop_back(); continue; } - mark.mark(e, true); if (is_var(e)) { + cache.insert(e, e); + todo.pop_back(); continue; } if (!is_app(e)) { return false; } app* ap = to_app(e); - if (a.is_select(ap) && !m_defs.contains(ap)) { - if (!insert_def(r, ap, 0)) { - return false; + bool valid = true; + args.reset(); + for (unsigned i = 0; i < ap->get_num_args(); ++i) { + expr* arg; + if (cache.find(ap->get_arg(i), arg)) { + args.push_back(arg); + } + else { + todo.push_back(ap->get_arg(i)); + valid = false; } } - if (a.is_select(e)) { - get_select_args(e, todo); - continue; + if (valid) { + todo.pop_back(); + e1 = m.mk_app(ap->get_decl(), args.size(), args.c_ptr()); + trail.push_back(e1); + if (a.is_select(ap)) { + if (m_defs.find(e1, v)) { + cache.insert(e, v); + } + else if (!insert_def(r, e1, 0)) { + return false; + } + else { + cache.insert(e, m_defs.find(e1)); + } + } + else { + cache.insert(e, e1); + } + } + } + for (unsigned i = 0; i < conjs.size(); ++i) { + expr* e = conjs[i].get(); + if (is_select_eq_var(e, s, v)) { + args.reset(); + for (unsigned j = 0; j < s->get_num_args(); ++j) { + args.push_back(cache.find(s->get_arg(j))); + } + e1 = m.mk_app(s->get_decl(), args.size(), args.c_ptr()); + if (!m_defs.contains(e1) && !insert_def(r, e1, v)) { + return false; + } + conjs[i] = m.mk_eq(v, m_defs.find(e1)); } - for (unsigned i = 0; i < ap->get_num_args(); ++i) { - todo.push_back(ap->get_arg(i)); + else { + conjs[i] = cache.find(e); } } - m_sub(body); - m_sub(head); - conjs.reset(); // perform the Ackermann reduction by creating implications // i1 = i2 => val1 = val2 for each equality pair: @@ -171,6 +211,7 @@ namespace datalog { for (; it2 != end; ++it2) { app* a2 = it2->m_key; var* v2 = it2->m_value; + TRACE("dl", tout << mk_pp(a1, m) << " " << mk_pp(a2, m) << "\n";); if (get_select(a1) != get_select(a2)) { continue; } @@ -184,10 +225,7 @@ namespace datalog { conjs.push_back(m.mk_implies(m.mk_and(eqs.size(), eqs.c_ptr()), m.mk_eq(v1, v2))); } } - if (!conjs.empty()) { - conjs.push_back(body); - body = m.mk_and(conjs.size(), conjs.c_ptr()); - } + body = m.mk_and(conjs.size(), conjs.c_ptr()); m_rewriter(body); return true; } diff --git a/src/muz/transforms/dl_mk_array_blast.h b/src/muz/transforms/dl_mk_array_blast.h index f4b685b7a..c96573848 100644 --- a/src/muz/transforms/dl_mk_array_blast.h +++ b/src/muz/transforms/dl_mk_array_blast.h @@ -44,7 +44,6 @@ namespace datalog { mk_interp_tail_simplifier m_simplifier; defs_t m_defs; - expr_safe_replace m_sub; unsigned m_next_var; bool blast(rule& r, rule_set& new_rules); @@ -59,6 +58,8 @@ namespace datalog { bool insert_def(rule const& r, app* e, var* v); + bool is_select_eq_var(expr* e, app*& s, var*& v) const; + public: /** \brief Create rule transformer that removes array stores and selects by ackermannization. From 4363c9f44fa4f5ac0aa83a90b5d7e8a3e6c49d8a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 24 Sep 2013 18:47:19 +0300 Subject: [PATCH 13/27] use safe replace for external substitution Signed-off-by: Nikolaj Bjorner --- src/api/api_ast.cpp | 11 +++-------- 1 file changed, 3 insertions(+), 8 deletions(-) diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 293983c9a..c96328bf8 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -31,7 +31,7 @@ Revision History: #include"ast_smt2_pp.h" #include"th_rewriter.h" #include"var_subst.h" -#include"expr_substitution.h" +#include"expr_safe_replace.h" #include"pp.h" #include"scoped_ctrl_c.h" #include"cancel_eh.h" @@ -786,17 +786,12 @@ extern "C" { RETURN_Z3(of_expr(0)); } } - - expr_substitution subst(m); + expr_safe_replace subst(m); for (unsigned i = 0; i < num_exprs; i++) { subst.insert(from[i], to[i]); } - th_rewriter m_rw(m); - m_rw.set_substitution(&subst); - expr_ref new_a(m); - proof_ref pr(m); - m_rw(a, new_a, pr); + subst(a, new_a); mk_c(c)->save_ast_trail(new_a); r = new_a.get(); RETURN_Z3(of_expr(r)); From 8ef2fe7ddbec4e2c17002518ace7a5e0d555381d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 25 Sep 2013 18:58:13 -0700 Subject: [PATCH 14/27] Fix z3.py doctests to reflect recent changes in the substitute API Signed-off-by: Leonardo de Moura --- src/api/python/z3.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index aaad24256..22ec30ad2 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -6932,10 +6932,10 @@ def substitute(t, *m): >>> x = Int('x') >>> y = Int('y') >>> substitute(x + 1, (x, y + 1)) - 2 + y + y + 1 + 1 >>> f = Function('f', IntSort(), IntSort()) >>> substitute(f(x) + f(y), (f(x), IntVal(1)), (f(y), IntVal(1))) - 2 + 1 + 1 """ if isinstance(m, tuple): m1 = _get_args(m) From 5e6a47e2d37b1e348925d8455b06808631c942e3 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 26 Sep 2013 11:35:08 +0100 Subject: [PATCH 15/27] Example fixed (substitute does not include a rewriter call anymore). Signed-off-by: Christoph M. Wintersteiger --- src/api/python/z3.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index aaad24256..22ec30ad2 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -6932,10 +6932,10 @@ def substitute(t, *m): >>> x = Int('x') >>> y = Int('y') >>> substitute(x + 1, (x, y + 1)) - 2 + y + y + 1 + 1 >>> f = Function('f', IntSort(), IntSort()) >>> substitute(f(x) + f(y), (f(x), IntVal(1)), (f(y), IntVal(1))) - 2 + 1 + 1 """ if isinstance(m, tuple): m1 = _get_args(m) From 3d910028bf4ecdd3386d73816d186588a8065a00 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 27 Sep 2013 16:55:05 +0100 Subject: [PATCH 16/27] fixed potential performance problem with fully interpreted sorts in the quantifier instantiation. Signed-off-by: Christoph M. Wintersteiger --- src/smt/smt_model_finder.cpp | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index c4a48d9f8..8303d05ac 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -975,9 +975,11 @@ namespace smt { // Moreover, a model assigns an arbitrary intepretation to these sorts using "model_values" a model value. // If these module values "leak" inside the logical context, they may affect satisfiability. // - // n->insert(m_model->get_some_value(n->get_sort()), 0); - // TODO: we can use get_some_value if the sort n->get_sort() does not depend on any uninterpreted sorts. - n->insert(m_manager.mk_fresh_const("elem", n->get_sort()), 0); + sort * ns = n->get_sort(); + if (m_manager.is_fully_interp(ns)) + n->insert(m_model->get_some_value(ns), 0); + else + n->insert(m_manager.mk_fresh_const("elem", ns), 0); } } } From 9a9f8bbb341be84285d31956b030e7c89f3641a4 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 8 Oct 2013 20:01:39 +0100 Subject: [PATCH 17/27] rewriter and value recognition bugfixes for floats Signed-off-by: Christoph M. Wintersteiger --- src/ast/float_decl_plugin.cpp | 21 +++++++++++++++++++++ src/ast/rewriter/float_rewriter.cpp | 4 ++-- 2 files changed, 23 insertions(+), 2 deletions(-) diff --git a/src/ast/float_decl_plugin.cpp b/src/ast/float_decl_plugin.cpp index 4aab6ab32..128dd2ce7 100644 --- a/src/ast/float_decl_plugin.cpp +++ b/src/ast/float_decl_plugin.cpp @@ -85,6 +85,24 @@ bool float_decl_plugin::is_value(expr * n, mpf & val) { m_fm.set(val, m_values[to_app(n)->get_decl()->get_parameter(0).get_ext_id()]); return true; } + else if (is_app_of(n, m_family_id, OP_FLOAT_MINUS_INF)) { + unsigned ebits = to_app(n)->get_decl()->get_range()->get_parameter(0).get_int(); + unsigned sbits = to_app(n)->get_decl()->get_range()->get_parameter(1).get_int(); + m_fm.mk_ninf(ebits, sbits, val); + return true; + } + else if (is_app_of(n, m_family_id, OP_FLOAT_PLUS_INF)) { + unsigned ebits = to_app(n)->get_decl()->get_range()->get_parameter(0).get_int(); + unsigned sbits = to_app(n)->get_decl()->get_range()->get_parameter(1).get_int(); + m_fm.mk_pinf(ebits, sbits, val); + return true; + } + else if (is_app_of(n, m_family_id, OP_FLOAT_NAN)) { + unsigned ebits = to_app(n)->get_decl()->get_range()->get_parameter(0).get_int(); + unsigned sbits = to_app(n)->get_decl()->get_range()->get_parameter(1).get_int(); + m_fm.mk_nan(ebits, sbits, val); + return true; + } return false; } @@ -523,6 +541,9 @@ bool float_decl_plugin::is_value(app * e) const { case OP_RM_TOWARD_NEGATIVE: case OP_RM_TOWARD_ZERO: case OP_FLOAT_VALUE: + case OP_FLOAT_PLUS_INF: + case OP_FLOAT_MINUS_INF: + case OP_FLOAT_NAN: return true; case OP_TO_FLOAT: return m_manager->is_value(e->get_arg(0)); diff --git a/src/ast/rewriter/float_rewriter.cpp b/src/ast/rewriter/float_rewriter.cpp index 0a4c3fc4e..4f8c90301 100644 --- a/src/ast/rewriter/float_rewriter.cpp +++ b/src/ast/rewriter/float_rewriter.cpp @@ -354,7 +354,7 @@ br_status float_rewriter::mk_lt(expr * arg1, expr * arg2, expr_ref & result) { if (m_util.is_minus_inf(arg1)) { // -oo < arg2 --> not(arg2 = -oo) and not(arg2 = NaN) result = m().mk_and(m().mk_not(m().mk_eq(arg2, arg1)), mk_neq_nan(arg2)); - return BR_REWRITE2; + return BR_REWRITE3; } if (m_util.is_minus_inf(arg2)) { // arg1 < -oo --> false @@ -369,7 +369,7 @@ br_status float_rewriter::mk_lt(expr * arg1, expr * arg2, expr_ref & result) { if (m_util.is_plus_inf(arg2)) { // arg1 < +oo --> not(arg1 = +oo) and not(arg1 = NaN) result = m().mk_and(m().mk_not(m().mk_eq(arg1, arg2)), mk_neq_nan(arg1)); - return BR_REWRITE2; + return BR_REWRITE3; } scoped_mpf v1(m_util.fm()), v2(m_util.fm()); From 65a202873f2851b79cb0d498b5714be56e48d8a3 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 10 Oct 2013 15:38:54 +0100 Subject: [PATCH 18/27] Bugfix for equality rewriting on floats. Signed-off-by: Christoph M. Wintersteiger --- src/ast/rewriter/float_rewriter.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/ast/rewriter/float_rewriter.cpp b/src/ast/rewriter/float_rewriter.cpp index 4f8c90301..6ef147f1c 100644 --- a/src/ast/rewriter/float_rewriter.cpp +++ b/src/ast/rewriter/float_rewriter.cpp @@ -490,7 +490,11 @@ br_status float_rewriter::mk_is_sign_minus(expr * arg1, expr_ref & result) { br_status float_rewriter::mk_eq_core(expr * arg1, expr * arg2, expr_ref & result) { scoped_mpf v1(m_util.fm()), v2(m_util.fm()); if (m_util.is_value(arg1, v1) && m_util.is_value(arg2, v2)) { - result = (v1 == v2) ? m().mk_true() : m().mk_false(); + // Note: == is the floats-equality, here we need normal equality. + result = (m_fm.is_nan(v1) && m_fm.is_nan(v2)) ? m().mk_true() : + (m_fm.is_zero(v1) && m_fm.is_zero(v2) && m_fm.sgn(v1)!=m_fm.sgn(v2)) ? m().mk_false() : + (v1 == v2) ? m().mk_true() : + m().mk_false(); return BR_DONE; } From 9b34350646c4a75c718a914f2ffc0d14cec09c93 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 13 Oct 2013 06:25:26 -0700 Subject: [PATCH 19/27] test output predicates Signed-off-by: Nikolaj Bjorner --- src/muz/bmc/dl_bmc_engine.cpp | 4 ++++ src/muz/clp/clp_context.cpp | 3 +++ src/tactic/core/elim_uncnstr_tactic.cpp | 1 - 3 files changed, 7 insertions(+), 1 deletion(-) diff --git a/src/muz/bmc/dl_bmc_engine.cpp b/src/muz/bmc/dl_bmc_engine.cpp index eb4bc72c4..7a88c1188 100644 --- a/src/muz/bmc/dl_bmc_engine.cpp +++ b/src/muz/bmc/dl_bmc_engine.cpp @@ -1448,6 +1448,10 @@ namespace datalog { transformer.register_plugin(slice); m_ctx.transform_rules(transformer); } + if (m_ctx.get_rules().get_output_predicates().empty()) { + return l_false; + } + m_query_pred = m_ctx.get_rules().get_output_predicate(); m_rules.replace_rules(m_ctx.get_rules()); m_rules.close(); diff --git a/src/muz/clp/clp_context.cpp b/src/muz/clp/clp_context.cpp index 5f3a09e2d..0cd08e5b3 100644 --- a/src/muz/clp/clp_context.cpp +++ b/src/muz/clp/clp_context.cpp @@ -70,6 +70,9 @@ namespace datalog { m_goals.reset(); rm.mk_query(query, m_ctx.get_rules()); apply_default_transformation(m_ctx); + if (m_ctx.get_rules().get_output_predicates().empty()) { + return l_false; + } func_decl* head_decl = m_ctx.get_rules().get_output_predicate(); rule_set& rules = m_ctx.get_rules(); rule_vector const& rv = rules.get_predicate_rules(head_decl); diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp index 00e14a41f..4d64bf061 100644 --- a/src/tactic/core/elim_uncnstr_tactic.cpp +++ b/src/tactic/core/elim_uncnstr_tactic.cpp @@ -38,7 +38,6 @@ class elim_uncnstr_tactic : public tactic { typedef std::pair frame; svector m_stack; ptr_vector m_vars; - expr_sparse_mark m_uncnstr_vars; bool visit(expr * t) { if (m_visited.is_marked(t)) { From eb4c10c037c8ed920e36710bcc27dbd34efa0739 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 15 Oct 2013 03:53:33 -0700 Subject: [PATCH 20/27] fixing bugs with validation code Signed-off-by: Nikolaj Bjorner --- src/muz/pdr/pdr_context.cpp | 4 +--- src/muz/transforms/dl_mk_array_blast.cpp | 11 ++++++++++- src/muz/transforms/dl_mk_bit_blast.cpp | 4 +++- src/muz/transforms/dl_mk_quantifier_abstraction.cpp | 1 - 4 files changed, 14 insertions(+), 6 deletions(-) diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp index aab7b1388..b09280d35 100644 --- a/src/muz/pdr/pdr_context.cpp +++ b/src/muz/pdr/pdr_context.cpp @@ -1123,9 +1123,7 @@ namespace pdr { n->mk_instantiate(r0, r1, binding); proof_ref p1(m), p2(m); p1 = r0->get_proof(); - if (!p1) { - r0->display(dctx, std::cout); - } + IF_VERBOSE(0, if (!p1) r0->display(dctx, verbose_stream());); SASSERT(p1); pfs[0] = p1; rls[0] = r1; diff --git a/src/muz/transforms/dl_mk_array_blast.cpp b/src/muz/transforms/dl_mk_array_blast.cpp index 93e31ff23..9303181b6 100644 --- a/src/muz/transforms/dl_mk_array_blast.cpp +++ b/src/muz/transforms/dl_mk_array_blast.cpp @@ -19,6 +19,7 @@ Revision History: #include "dl_mk_array_blast.h" #include "qe_util.h" +#include "scoped_proof.h" namespace datalog { @@ -270,7 +271,7 @@ namespace datalog { } } - expr_ref fml2(m), body(m), head(m); + expr_ref fml1(m), fml2(m), body(m), head(m); body = m.mk_and(new_conjs.size(), new_conjs.c_ptr()); head = r.get_head(); sub(body); @@ -287,9 +288,17 @@ namespace datalog { proof_ref p(m); rule_set new_rules(m_ctx); rm.mk_rule(fml2, p, new_rules, r.name()); + rule_ref new_rule(rm); if (m_simplifier.transform_rule(new_rules.last(), new_rule)) { + if (r.get_proof()) { + scoped_proof _sc(m); + r.to_formula(fml1); + p = m.mk_rewrite(fml1, fml2); + p = m.mk_modus_ponens(r.get_proof(), p); + new_rule->set_proof(m, p); + } rules.add_rule(new_rule.get()); rm.mk_rule_rewrite_proof(r, *new_rule.get()); TRACE("dl", new_rule->display(m_ctx, tout << "new rule\n");); diff --git a/src/muz/transforms/dl_mk_bit_blast.cpp b/src/muz/transforms/dl_mk_bit_blast.cpp index 91481ed5a..112541541 100644 --- a/src/muz/transforms/dl_mk_bit_blast.cpp +++ b/src/muz/transforms/dl_mk_bit_blast.cpp @@ -25,6 +25,7 @@ Revision History: #include "filter_model_converter.h" #include "dl_mk_interp_tail_simplifier.h" #include "fixedpoint_params.hpp" +#include "scoped_proof.h" namespace datalog { @@ -268,7 +269,8 @@ namespace datalog { r->to_formula(fml); if (blast(r, fml)) { proof_ref pr(m); - if (m_context.generate_proof_trace()) { + if (r->get_proof()) { + scoped_proof _sc(m); pr = m.mk_asserted(fml); // loses original proof of r. } // TODO add logic for pc: diff --git a/src/muz/transforms/dl_mk_quantifier_abstraction.cpp b/src/muz/transforms/dl_mk_quantifier_abstraction.cpp index 0ad4d61ab..57948a2ff 100644 --- a/src/muz/transforms/dl_mk_quantifier_abstraction.cpp +++ b/src/muz/transforms/dl_mk_quantifier_abstraction.cpp @@ -341,7 +341,6 @@ namespace datalog { } head = mk_head(source, *result, r.get_head(), cnt); fml = m.mk_implies(m.mk_and(tail.size(), tail.c_ptr()), head); - rule_ref_vector added_rules(rm); proof_ref pr(m); rm.mk_rule(fml, pr, *result); TRACE("dl", result->last()->display(m_ctx, tout);); From f54b068669107059e80dafe70c1d96466c1c6144 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 17 Oct 2013 15:29:55 +0100 Subject: [PATCH 21/27] added floating point standard draft version 3 function symbols --- src/ast/float_decl_plugin.cpp | 46 ++++++++++++++++++++++++++++++++++- 1 file changed, 45 insertions(+), 1 deletion(-) diff --git a/src/ast/float_decl_plugin.cpp b/src/ast/float_decl_plugin.cpp index 128dd2ce7..eb8aba9ae 100644 --- a/src/ast/float_decl_plugin.cpp +++ b/src/ast/float_decl_plugin.cpp @@ -475,6 +475,7 @@ void float_decl_plugin::get_op_names(svector & op_names, symbol co op_names.push_back(builtin_name("plusInfinity", OP_FLOAT_PLUS_INF)); op_names.push_back(builtin_name("minusInfinity", OP_FLOAT_MINUS_INF)); op_names.push_back(builtin_name("NaN", OP_FLOAT_NAN)); + op_names.push_back(builtin_name("roundNearestTiesToEven", OP_RM_NEAREST_TIES_TO_EVEN)); op_names.push_back(builtin_name("roundNearestTiesToAway", OP_RM_NEAREST_TIES_TO_AWAY)); op_names.push_back(builtin_name("roundTowardPositive", OP_RM_TOWARD_POSITIVE)); @@ -486,7 +487,7 @@ void float_decl_plugin::get_op_names(svector & op_names, symbol co op_names.push_back(builtin_name("/", OP_FLOAT_DIV)); op_names.push_back(builtin_name("*", OP_FLOAT_MUL)); - op_names.push_back(builtin_name("abs", OP_FLOAT_ABS)); + op_names.push_back(builtin_name("abs", OP_FLOAT_ABS)); op_names.push_back(builtin_name("remainder", OP_FLOAT_REM)); op_names.push_back(builtin_name("fusedMA", OP_FLOAT_FUSED_MA)); op_names.push_back(builtin_name("squareRoot", OP_FLOAT_SQRT)); @@ -515,6 +516,49 @@ void float_decl_plugin::get_op_names(svector & op_names, symbol co if (m_bv_plugin) op_names.push_back(builtin_name("asIEEEBV", OP_TO_IEEE_BV)); + + // We also support draft version 3 + op_names.push_back(builtin_name("fp", OP_TO_FLOAT)); + + op_names.push_back(builtin_name("RNE", OP_RM_NEAREST_TIES_TO_EVEN)); + op_names.push_back(builtin_name("RNA", OP_RM_NEAREST_TIES_TO_AWAY)); + op_names.push_back(builtin_name("RTP", OP_RM_TOWARD_POSITIVE)); + op_names.push_back(builtin_name("RTN", OP_RM_TOWARD_NEGATIVE)); + op_names.push_back(builtin_name("RTZ", OP_RM_TOWARD_ZERO)); + + op_names.push_back(builtin_name("fp.abs", OP_FLOAT_ABS)); + op_names.push_back(builtin_name("fp.neg", OP_FLOAT_UMINUS)); + op_names.push_back(builtin_name("fp.add", OP_FLOAT_ADD)); + op_names.push_back(builtin_name("fp.sub", OP_FLOAT_SUB)); + op_names.push_back(builtin_name("fp.mul", OP_FLOAT_MUL)); + op_names.push_back(builtin_name("fp.div", OP_FLOAT_DIV)); + op_names.push_back(builtin_name("fp.fma", OP_FLOAT_FUSED_MA)); + op_names.push_back(builtin_name("fp.sqrt", OP_FLOAT_SQRT)); + op_names.push_back(builtin_name("fp.rem", OP_FLOAT_REM)); + op_names.push_back(builtin_name("fp.eq", OP_FLOAT_EQ)); + op_names.push_back(builtin_name("fp.leq", OP_FLOAT_LE)); + op_names.push_back(builtin_name("fp.lt", OP_FLOAT_LT)); + op_names.push_back(builtin_name("fp.geq", OP_FLOAT_GE)); + op_names.push_back(builtin_name("fp.gt", OP_FLOAT_GT)); + op_names.push_back(builtin_name("fp.isNormal", OP_FLOAT_IS_NORMAL)); + op_names.push_back(builtin_name("fp.isSubnormal", OP_FLOAT_IS_SUBNORMAL)); + op_names.push_back(builtin_name("fp.isZero", OP_FLOAT_IS_ZERO)); + op_names.push_back(builtin_name("fp.isInfinite", OP_FLOAT_IS_INF)); + op_names.push_back(builtin_name("fp.isNaN", OP_FLOAT_IS_NAN)); + op_names.push_back(builtin_name("fp.min", OP_FLOAT_MIN)); + op_names.push_back(builtin_name("fp.max", OP_FLOAT_MAX)); + op_names.push_back(builtin_name("fp.convert", OP_TO_FLOAT)); + + if (m_bv_plugin) { + // op_names.push_back(builtin_name("fp.fromBv", OP_TO_FLOAT)); + // op_names.push_back(builtin_name("fp.fromUBv", OP_TO_FLOAT)); + // op_names.push_back(builtin_name("fp.fromSBv", OP_TO_FLOAT)); + // op_names.push_back(builtin_name("fp.toUBv", OP_TO_IEEE_BV)); + // op_names.push_back(builtin_name("fp.toSBv", OP_TO_IEEE_BV)); + } + + op_names.push_back(builtin_name("fp.fromReal", OP_TO_FLOAT)); + // op_names.push_back(builtin_name("fp.toReal", ?)); } void float_decl_plugin::get_sort_names(svector & sort_names, symbol const & logic) { From 2b627b0821bdf37d3aa7680cbd99bb7ed87dce93 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 21 Oct 2013 17:28:21 +0100 Subject: [PATCH 22/27] fixed parameters to disallow overwriting them with illegal combinations on the command line Signed-off-by: Christoph M. Wintersteiger --- src/tactic/smtlogics/qfbv_tactic.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/tactic/smtlogics/qfbv_tactic.cpp b/src/tactic/smtlogics/qfbv_tactic.cpp index 51b040332..ac53ca0c8 100644 --- a/src/tactic/smtlogics/qfbv_tactic.cpp +++ b/src/tactic/smtlogics/qfbv_tactic.cpp @@ -43,6 +43,8 @@ tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p) { simp2_p.set_bool("push_ite_bv", false); simp2_p.set_bool("local_ctx", true); simp2_p.set_uint("local_ctx_limit", 10000000); + simp2_p.set_bool("flat", true); // required by som + simp2_p.set_bool("hoist_mul", false); // required by som params_ref local_ctx_p = p; local_ctx_p.set_bool("local_ctx", true); From ff265c6c6ccf9d11087388910cdc1702a4711bca Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 24 Oct 2013 17:48:03 +0100 Subject: [PATCH 23/27] bugfix for variable unmarking in the sat solver. Signed-off-by: Christoph M. Wintersteiger --- src/sat/sat_solver.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 3e9b60260..d9e11724c 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -1290,13 +1290,13 @@ namespace sat { bool solver::resolve_conflict() { while (true) { bool r = resolve_conflict_core(); + CASSERT("sat_check_marks", check_marks()); // after pop, clauses are reinitialized, this may trigger another conflict. if (!r) return false; if (!inconsistent()) return true; } - CASSERT("sat_check_marks", check_marks()); } bool solver::resolve_conflict_core() { @@ -1323,7 +1323,7 @@ namespace sat { TRACE("sat_conflict", tout << "not_l: " << m_not_l << "\n";); process_antecedent(m_not_l, num_marks); } - + literal consequent = m_not_l; justification js = m_conflict; @@ -1399,6 +1399,8 @@ namespace sat { dyn_sub_res(); TRACE("sat_lemma", tout << "new lemma (after minimization) size: " << m_lemma.size() << "\n" << m_lemma << "\n";); } + else + reset_lemma_var_marks(); literal_vector::iterator it = m_lemma.begin(); literal_vector::iterator end = m_lemma.end(); From 8b10e1325141cb9af1c3776a36a36c56019b186a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 4 Nov 2013 11:02:53 -0800 Subject: [PATCH 24/27] fix bug in factor_tactic Signed-off-by: Leonardo de Moura --- src/tactic/arith/factor_tactic.cpp | 58 +++++++++++++++--------------- 1 file changed, 29 insertions(+), 29 deletions(-) diff --git a/src/tactic/arith/factor_tactic.cpp b/src/tactic/arith/factor_tactic.cpp index 752f6681d..4eec83037 100644 --- a/src/tactic/arith/factor_tactic.cpp +++ b/src/tactic/arith/factor_tactic.cpp @@ -50,7 +50,7 @@ class factor_tactic : public tactic { return args[0]; return m_util.mk_mul(sz, args); } - + expr * mk_zero_for(expr * arg) { return m_util.mk_numeral(rational(0), m_util.is_int(arg)); } @@ -92,10 +92,10 @@ class factor_tactic : public tactic { return k; } } - + // p1^{2*k1} * p2^{2*k2 + 1} >=< 0 // --> - // (p1^2)*p2 >=<0 + // (p1^2)*p2 >=<0 void mk_comp(decl_kind k, polynomial::factors const & fs, expr_ref & result) { SASSERT(k == OP_LT || k == OP_GT || k == OP_LE || k == OP_GE); expr_ref_buffer args(m); @@ -127,7 +127,7 @@ class factor_tactic : public tactic { } } } - + // Strict case // p1^{2*k1} * p2^{2*k2 + 1} >< 0 // --> @@ -158,11 +158,11 @@ class factor_tactic : public tactic { args.push_back(m.mk_app(m_util.get_family_id(), k, mk_mul(odd_factors.size(), odd_factors.c_ptr()), mk_zero_for(odd_factors[0]))); } SASSERT(!args.empty()); - if (args.size() == 1) + if (args.size() == 1) result = args[0]; else if (strict) result = m.mk_and(args.size(), args.c_ptr()); - else + else result = m.mk_or(args.size(), args.c_ptr()); } @@ -173,7 +173,7 @@ class factor_tactic : public tactic { scoped_mpz d2(m_qm); m_expr2poly.to_polynomial(lhs, p1, d1); m_expr2poly.to_polynomial(rhs, p2, d2); - TRACE("factor_tactic_bug", + TRACE("factor_tactic_bug", tout << "lhs: " << mk_ismt2_pp(lhs, m) << "\n"; tout << "p1: " << p1 << "\n"; tout << "d1: " << d1 << "\n"; @@ -195,18 +195,18 @@ class factor_tactic : public tactic { SASSERT(fs.distinct_factors() > 0); TRACE("factor_tactic_bug", tout << "factors:\n"; fs.display(tout); tout << "\n";); if (fs.distinct_factors() == 1 && fs.get_degree(0) == 1) - return BR_FAILED; + return BR_FAILED; if (m.is_eq(f)) { if (m_split_factors) mk_split_eq(fs, result); - else + else mk_eq(fs, result); } else { decl_kind k = f->get_decl_kind(); if (m_qm.is_neg(fs.get_constant())) k = flip(k); - + if (m_split_factors) mk_split_comp(k, fs, result); else @@ -215,10 +215,10 @@ class factor_tactic : public tactic { return BR_DONE; } - br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { + br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { if (num != 2) return BR_FAILED; - if (m.is_eq(f) && (m_util.is_arith_expr(args[0]) || m_util.is_arith_expr(args[1]))) + if (m.is_eq(f) && (m_util.is_arith_expr(args[0]) || m_util.is_arith_expr(args[1])) && (!m.is_bool(args[0]))) return factor(f, args[0], args[1], result); if (f->get_family_id() != m_util.get_family_id()) return BR_FAILED; @@ -232,10 +232,10 @@ class factor_tactic : public tactic { return BR_FAILED; } }; - + struct rw : public rewriter_tpl { rw_cfg m_cfg; - + rw(ast_manager & m, params_ref const & p): rewriter_tpl(m, m.proofs_enabled(), m_cfg), m_cfg(m, p) { @@ -245,24 +245,24 @@ class factor_tactic : public tactic { struct imp { ast_manager & m; rw m_rw; - + imp(ast_manager & _m, params_ref const & p): m(_m), m_rw(m, p) { } - + void set_cancel(bool f) { m_rw.set_cancel(f); m_rw.cfg().m_pm.set_cancel(f); } - + void updt_params(params_ref const & p) { m_rw.cfg().updt_params(p); } - - void operator()(goal_ref const & g, - goal_ref_buffer & result, - model_converter_ref & mc, + + void operator()(goal_ref const & g, + goal_ref_buffer & result, + model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core) { SASSERT(g->is_well_sorted()); @@ -288,7 +288,7 @@ class factor_tactic : public tactic { SASSERT(g->is_well_sorted()); } }; - + imp * m_imp; params_ref m_params; public: @@ -300,7 +300,7 @@ public: virtual tactic * translate(ast_manager & m) { return alloc(factor_tactic, m, m_params); } - + virtual ~factor_tactic() { dealloc(m_imp); } @@ -311,14 +311,14 @@ public: } virtual void collect_param_descrs(param_descrs & r) { - r.insert("split_factors", CPK_BOOL, + r.insert("split_factors", CPK_BOOL, "(default: true) apply simplifications such as (= (* p1 p2) 0) --> (or (= p1 0) (= p2 0))."); polynomial::factor_params::get_param_descrs(r); } - - virtual void operator()(goal_ref const & in, - goal_ref_buffer & result, - model_converter_ref & mc, + + virtual void operator()(goal_ref const & in, + goal_ref_buffer & result, + model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core) { try { @@ -331,7 +331,7 @@ public: throw tactic_exception(ex.msg()); } } - + virtual void cleanup() { ast_manager & m = m_imp->m; imp * d = m_imp; From 825b72719ca60e978aef1137699744177199372f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 4 Nov 2013 11:57:29 -0800 Subject: [PATCH 25/27] fix https://z3.codeplex.com/workitem/62 Signed-off-by: Leonardo de Moura --- src/sat/sat_simplifier.cpp | 142 ++++++++++++------------ src/sat/sat_solver.cpp | 220 ++++++++++++++++++++----------------- 2 files changed, 189 insertions(+), 173 deletions(-) diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index ba0c67235..37d41a5fd 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -9,7 +9,7 @@ Abstract: SAT simplification procedures that use a "full" occurrence list: Subsumption, Blocked Clause Removal, Variable Elimination, ... - + Author: @@ -54,21 +54,21 @@ namespace sat { m_use_list[l2.index()].erase(c); } } - + simplifier::simplifier(solver & _s, params_ref const & p): s(_s), m_num_calls(0) { updt_params(p); reset_statistics(); } - + simplifier::~simplifier() { } inline watch_list & simplifier::get_wlist(literal l) { return s.get_wlist(l); } inline watch_list const & simplifier::get_wlist(literal l) const { return s.get_wlist(l); } - + inline bool simplifier::is_external(bool_var v) const { return s.is_external(v); } inline bool simplifier::was_eliminated(bool_var v) const { return s.was_eliminated(v); } @@ -78,7 +78,7 @@ namespace sat { lbool simplifier::value(literal l) const { return s.value(l); } inline void simplifier::checkpoint() { s.checkpoint(); } - + void simplifier::register_clauses(clause_vector & cs) { std::stable_sort(cs.begin(), cs.end(), size_lt()); clause_vector::iterator it = cs.begin(); @@ -117,7 +117,7 @@ namespace sat { SASSERT(s.get_wlist(~l1).contains(watched(l2, learned))); s.get_wlist(~l1).erase(watched(l2, learned)); } - + void simplifier::init_visited() { m_visited.reset(); m_visited.resize(2*s.num_vars(), false); @@ -155,7 +155,7 @@ namespace sat { if (!learned && (m_elim_blocked_clauses || m_elim_blocked_clauses_at == m_num_calls)) elim_blocked_clauses(); - + if (!learned) m_num_calls++; @@ -180,6 +180,7 @@ namespace sat { bool vars_eliminated = m_num_elim_vars > old_num_elim_vars; if (!m_need_cleanup) { + TRACE("after_simplifier", tout << "skipping cleanup...\n";); if (vars_eliminated) { // must remove learned clauses with eliminated variables cleanup_clauses(s.m_learned, true, true, learned_in_use_lists); @@ -189,6 +190,7 @@ namespace sat { free_memory(); return; } + TRACE("after_simplifier", tout << "cleanning watches...\n";); cleanup_watches(); cleanup_clauses(s.m_learned, true, vars_eliminated, learned_in_use_lists); cleanup_clauses(s.m_clauses, false, vars_eliminated, true); @@ -234,7 +236,7 @@ namespace sat { s.del_clause(c); continue; } - + if (learned && vars_eliminated) { unsigned sz = c.size(); unsigned i; @@ -293,7 +295,7 @@ namespace sat { mark_visited(c[i]); } } - + void simplifier::unmark_all(clause const & c) { unsigned sz = c.size(); for (unsigned i = 0; i < sz; i++) @@ -325,7 +327,7 @@ namespace sat { */ bool simplifier::subsumes1(clause const & c1, clause const & c2, literal & l) { unsigned sz2 = c2.size(); - for (unsigned i = 0; i < sz2; i++) + for (unsigned i = 0; i < sz2; i++) mark_visited(c2[i]); bool r = true; @@ -344,7 +346,7 @@ namespace sat { } } - for (unsigned i = 0; i < sz2; i++) + for (unsigned i = 0; i < sz2; i++) unmark_visited(c2[i]); return r; } @@ -353,7 +355,7 @@ namespace sat { \brief Return the clauses subsumed by c1 and the clauses that can be subsumed resolved using c1. The collections is populated using the use list of target. */ - void simplifier::collect_subsumed1_core(clause const & c1, clause_vector & out, literal_vector & out_lits, + void simplifier::collect_subsumed1_core(clause const & c1, clause_vector & out, literal_vector & out_lits, literal target) { clause_use_list const & cs = m_use_list.get(target); clause_use_list::iterator it = cs.mk_iterator(); @@ -362,7 +364,7 @@ namespace sat { CTRACE("resolution_bug", c2.was_removed(), tout << "clause has been removed:\n" << c2 << "\n";); SASSERT(!c2.was_removed()); if (&c2 != &c1 && - c1.size() <= c2.size() && + c1.size() <= c2.size() && approx_subset(c1.approx(), c2.approx())) { m_sub_counter -= c1.size() + c2.size(); literal l; @@ -373,7 +375,7 @@ namespace sat { } it.next(); } - } + } /** \brief Return the clauses subsumed by c1 and the clauses that can be subsumed resolved using c1. @@ -400,7 +402,7 @@ namespace sat { if (*l_it == null_literal) { // c2 was subsumed if (c1.is_learned() && !c2.is_learned()) - c1.unset_learned(); + c1.unset_learned(); TRACE("subsumption", tout << c1 << " subsumed " << c2 << "\n";); remove_clause(c2); m_num_subsumed++; @@ -447,9 +449,9 @@ namespace sat { */ bool simplifier::subsumes0(clause const & c1, clause const & c2) { unsigned sz2 = c2.size(); - for (unsigned i = 0; i < sz2; i++) + for (unsigned i = 0; i < sz2; i++) mark_visited(c2[i]); - + bool r = true; unsigned sz1 = c1.size(); for (unsigned i = 0; i < sz1; i++) { @@ -459,12 +461,12 @@ namespace sat { } } - for (unsigned i = 0; i < sz2; i++) + for (unsigned i = 0; i < sz2; i++) unmark_visited(c2[i]); - + return r; } - + /** \brief Collect the clauses subsumed by c1 (using the occurrence list of target). */ @@ -475,7 +477,7 @@ namespace sat { clause & c2 = it.curr(); SASSERT(!c2.was_removed()); if (&c2 != &c1 && - c1.size() <= c2.size() && + c1.size() <= c2.size() && approx_subset(c1.approx(), c2.approx())) { m_sub_counter -= c1.size() + c2.size(); if (subsumes0(c1, c2)) { @@ -485,7 +487,7 @@ namespace sat { it.next(); } } - + /** \brief Collect the clauses subsumed by c1 */ @@ -493,8 +495,8 @@ namespace sat { literal l = get_min_occ_var0(c1); collect_subsumed0_core(c1, out, l); } - - + + /** \brief Perform backward subsumption using c1. */ @@ -507,16 +509,16 @@ namespace sat { clause & c2 = *(*it); // c2 was subsumed if (c1.is_learned() && !c2.is_learned()) - c1.unset_learned(); + c1.unset_learned(); TRACE("subsumption", tout << c1 << " subsumed " << c2 << "\n";); remove_clause(c2); m_num_subsumed++; } } - + /** \brief Eliminate false literals from c, and update occurrence lists - + Return true if the clause is satisfied */ bool simplifier::cleanup_clause(clause & c, bool in_use_list) { @@ -666,7 +668,7 @@ namespace sat { back_subsumption1(c); if (w.is_learned() && !c.is_learned()) { SASSERT(wlist[j] == w); - TRACE("mark_not_learned_bug", + TRACE("mark_not_learned_bug", tout << "marking as not learned: " << l2 << " " << wlist[j].is_learned() << "\n";); wlist[j].mark_not_learned(); mark_as_not_learned_core(get_wlist(~l2), l); @@ -735,7 +737,7 @@ namespace sat { continue; } if (it2->get_literal() == last_lit) { - TRACE("subsumption", tout << "eliminating: " << ~to_literal(l_idx) + TRACE("subsumption", tout << "eliminating: " << ~to_literal(l_idx) << " " << it2->get_literal() << "\n";); elim++; } @@ -762,12 +764,12 @@ namespace sat { m_num_sub_res(s.m_num_sub_res) { m_watch.start(); } - + ~subsumption_report() { m_watch.stop(); - IF_VERBOSE(SAT_VB_LVL, + IF_VERBOSE(SAT_VB_LVL, verbose_stream() << " (sat-subsumer :subsumed " - << (m_simplifier.m_num_subsumed - m_num_subsumed) + << (m_simplifier.m_num_subsumed - m_num_subsumed) << " :subsumption-resolution " << (m_simplifier.m_num_sub_res - m_num_sub_res) << " :threshold " << m_simplifier.m_sub_counter << mem_stat() @@ -847,12 +849,12 @@ namespace sat { vector const & m_watches; public: literal_lt(use_list const & l, vector const & ws):m_use_list(l), m_watches(ws) {} - + unsigned weight(unsigned l_idx) const { return 2*m_use_list.get(~to_literal(l_idx)).size() + m_watches[l_idx].size(); } - - bool operator()(unsigned l_idx1, unsigned l_idx2) const { + + bool operator()(unsigned l_idx1, unsigned l_idx2) const { return weight(l_idx1) < weight(l_idx2); } }; @@ -861,9 +863,9 @@ namespace sat { heap m_queue; public: queue(use_list const & l, vector const & ws):m_queue(128, literal_lt(l, ws)) {} - void insert(literal l) { + void insert(literal l) { unsigned idx = l.index(); - m_queue.reserve(idx + 1); + m_queue.reserve(idx + 1); SASSERT(!m_queue.contains(idx)); m_queue.insert(idx); } @@ -877,14 +879,14 @@ namespace sat { literal next() { SASSERT(!empty()); return to_literal(m_queue.erase_min()); } bool empty() const { return m_queue.empty(); } }; - + simplifier & s; int m_counter; model_converter & mc; queue m_queue; clause_vector m_to_remove; - blocked_clause_elim(simplifier & _s, unsigned limit, model_converter & _mc, use_list & l, + blocked_clause_elim(simplifier & _s, unsigned limit, model_converter & _mc, use_list & l, vector & wlist): s(_s), m_counter(limit), @@ -946,7 +948,7 @@ namespace sat { clause_vector::iterator it = m_to_remove.begin(); clause_vector::iterator end = m_to_remove.end(); for (; it != end; ++it) { - s.remove_clause(*(*it)); + s.remove_clause(*(*it)); } } { @@ -1025,12 +1027,12 @@ namespace sat { m_num_blocked_clauses(s.m_num_blocked_clauses) { m_watch.start(); } - + ~blocked_cls_report() { m_watch.stop(); - IF_VERBOSE(SAT_VB_LVL, + IF_VERBOSE(SAT_VB_LVL, verbose_stream() << " (sat-blocked-clauses :elim-blocked-clauses " - << (m_simplifier.m_num_blocked_clauses - m_num_blocked_clauses) + << (m_simplifier.m_num_blocked_clauses - m_num_blocked_clauses) << mem_stat() << " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds() << ")\n";); } @@ -1062,8 +1064,8 @@ namespace sat { unsigned num_neg = m_use_list.get(neg_l).size(); unsigned num_bin_pos = get_num_non_learned_bin(pos_l); unsigned num_bin_neg = get_num_non_learned_bin(neg_l); - unsigned cost = 2 * num_pos * num_neg + num_pos * num_bin_neg + num_neg * num_bin_pos; - CTRACE("elim_vars_detail", cost == 0, tout << v << " num_pos: " << num_pos << " num_neg: " << num_neg << " num_bin_pos: " << num_bin_pos + unsigned cost = 2 * num_pos * num_neg + num_pos * num_bin_neg + num_neg * num_bin_pos; + CTRACE("elim_vars_detail", cost == 0, tout << v << " num_pos: " << num_pos << " num_neg: " << num_neg << " num_bin_pos: " << num_bin_pos << " num_bin_neg: " << num_bin_neg << " cost: " << cost << "\n";); return cost; } @@ -1071,7 +1073,7 @@ namespace sat { typedef std::pair bool_var_and_cost; struct bool_var_and_cost_lt { - bool operator()(bool_var_and_cost const & p1, bool_var_and_cost const & p2) const { return p1.second < p2.second; } + bool operator()(bool_var_and_cost const & p1, bool_var_and_cost const & p2) const { return p1.second < p2.second; } }; void simplifier::order_vars_for_elim(bool_var_vector & r) { @@ -1104,7 +1106,7 @@ namespace sat { r.push_back(it2->first); } } - + /** \brief Collect clauses and binary clauses containing l. */ @@ -1116,7 +1118,7 @@ namespace sat { SASSERT(r.back().size() == it.curr().size()); it.next(); } - + watch_list & wlist = get_wlist(~l); watch_list::iterator it2 = wlist.begin(); watch_list::iterator end2 = wlist.end(); @@ -1129,7 +1131,7 @@ namespace sat { } /** - \brief Resolve clauses c1 and c2. + \brief Resolve clauses c1 and c2. c1 must contain l. c2 must contain ~l. Store result in r. @@ -1149,7 +1151,7 @@ namespace sat { m_visited[l2.index()] = true; r.push_back(l2); } - + literal not_l = ~l; sz = c2.size(); m_elim_counter -= sz; @@ -1164,7 +1166,7 @@ namespace sat { if (!m_visited[l2.index()]) r.push_back(l2); } - + sz = c1.size(); for (unsigned i = 0; i < sz; i++) { literal l2 = c1[i]; @@ -1200,7 +1202,7 @@ namespace sat { break; } } - CTRACE("resolve_bug", it2 == end2, + CTRACE("resolve_bug", it2 == end2, tout << ~l1 << " -> "; display(tout, s.m_cls_allocator, wlist1); tout << "\n" << ~l2 << " -> "; display(tout, s.m_cls_allocator, wlist2); tout << "\n";); @@ -1262,7 +1264,7 @@ namespace sat { TRACE("resolution_bug", tout << "processing: " << v << "\n";); if (value(v) != l_undef) return false; - + literal pos_l(v, false); literal neg_l(v, true); unsigned num_bin_pos = get_num_non_learned_bin(pos_l); @@ -1274,12 +1276,12 @@ namespace sat { m_elim_counter -= num_pos + num_neg; TRACE("resolution", tout << v << " num_pos: " << num_pos << " neg_pos: " << num_neg << "\n";); - + if (num_pos >= m_res_occ_cutoff && num_neg >= m_res_occ_cutoff) return false; unsigned before_lits = num_bin_pos*2 + num_bin_neg*2; - + { clause_use_list::iterator it = pos_occs.mk_iterator(); while (!it.at_end()) { @@ -1287,7 +1289,7 @@ namespace sat { it.next(); } } - + { clause_use_list::iterator it2 = neg_occs.mk_iterator(); while (!it2.at_end()) { @@ -1297,23 +1299,23 @@ namespace sat { } TRACE("resolution", tout << v << " num_pos: " << num_pos << " neg_pos: " << num_neg << " before_lits: " << before_lits << "\n";); - + if (num_pos >= m_res_occ_cutoff3 && num_neg >= m_res_occ_cutoff3 && before_lits > m_res_lit_cutoff3 && s.m_clauses.size() > m_res_cls_cutoff2) return false; - if (num_pos >= m_res_occ_cutoff2 && num_neg >= m_res_occ_cutoff2 && before_lits > m_res_lit_cutoff2 && + if (num_pos >= m_res_occ_cutoff2 && num_neg >= m_res_occ_cutoff2 && before_lits > m_res_lit_cutoff2 && s.m_clauses.size() > m_res_cls_cutoff1 && s.m_clauses.size() <= m_res_cls_cutoff2) return false; - if (num_pos >= m_res_occ_cutoff1 && num_neg >= m_res_occ_cutoff1 && before_lits > m_res_lit_cutoff1 && + if (num_pos >= m_res_occ_cutoff1 && num_neg >= m_res_occ_cutoff1 && before_lits > m_res_lit_cutoff1 && s.m_clauses.size() <= m_res_cls_cutoff1) return false; - + m_pos_cls.reset(); m_neg_cls.reset(); collect_clauses(pos_l, m_pos_cls); collect_clauses(neg_l, m_neg_cls); - + m_elim_counter -= num_pos * num_neg + before_lits; - + TRACE("resolution_detail", tout << "collecting number of after_clauses\n";); unsigned before_clauses = num_pos + num_neg; unsigned after_clauses = 0; @@ -1350,7 +1352,7 @@ namespace sat { neg_occs.reset(); m_elim_counter -= num_pos * num_neg + before_lits; - + it1 = m_pos_cls.begin(); end1 = m_pos_cls.end(); for (; it1 != end1; ++it1) { @@ -1393,7 +1395,7 @@ namespace sat { return true; } } - + return true; } @@ -1406,10 +1408,10 @@ namespace sat { m_num_elim_vars(s.m_num_elim_vars) { m_watch.start(); } - + ~elim_var_report() { m_watch.stop(); - IF_VERBOSE(SAT_VB_LVL, + IF_VERBOSE(SAT_VB_LVL, verbose_stream() << " (sat-resolution :elim-bool-vars " << (m_simplifier.m_num_elim_vars - m_num_elim_vars) << " :threshold " << m_simplifier.m_elim_counter @@ -1417,12 +1419,12 @@ namespace sat { << " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds() << ")\n";); } }; - + void simplifier::elim_vars() { elim_var_report rpt(*this); bool_var_vector vars; order_vars_for_elim(vars); - + bool_var_vector::iterator it = vars.begin(); bool_var_vector::iterator end = vars.end(); for (; it != end; ++it) { @@ -1463,7 +1465,7 @@ namespace sat { void simplifier::collect_param_descrs(param_descrs & r) { sat_simplifier_params::collect_param_descrs(r); } - + void simplifier::collect_statistics(statistics & st) { st.update("subsumed", m_num_subsumed); st.update("subsumption resolution", m_num_sub_res); @@ -1471,7 +1473,7 @@ namespace sat { st.update("elim bool vars", m_num_elim_vars); st.update("elim blocked clauses", m_num_blocked_clauses); } - + void simplifier::reset_statistics() { m_num_blocked_clauses = 0; m_num_subsumed = 0; diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index d9e11724c..bb08ae5c3 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -27,7 +27,7 @@ Revision History: // define to create a copy of the solver before starting the search // useful for checking models // #define CLONE_BEFORE_SOLVING - + namespace sat { solver::solver(params_ref const & p, extension * ext): @@ -103,7 +103,7 @@ namespace sat { } } } - + // ----------------------- // // Variable & Clause creation @@ -312,7 +312,7 @@ namespace sat { /** \brief Select a watch literal starting the search at the given position. This method is only used for clauses created during the search. - + I use the following rules to select a watch literal. 1- select a literal l in idx >= starting_at such that value(l) = l_true, @@ -329,7 +329,7 @@ namespace sat { lvl(l) >= lvl(l') Without rule 3, boolean propagation is incomplete, that is, it may miss possible propagations. - + \remark The method select_lemma_watch_lit is used to select the watch literal for regular learned clauses. */ unsigned solver::select_watch_lit(clause const & cls, unsigned starting_at) const { @@ -443,7 +443,7 @@ namespace sat { erase_clause_watch(get_wlist(~c[0]), cls_off); erase_clause_watch(get_wlist(~c[1]), cls_off); } - + void solver::dettach_ter_clause(clause & c) { erase_ternary_watch(get_wlist(~c[0]), c[1], c[2]); erase_ternary_watch(get_wlist(~c[1]), c[0], c[2]); @@ -498,10 +498,10 @@ namespace sat { unsigned sz = c.size(); for (unsigned i = 0; i < sz; i++) { switch (value(c[i])) { - case l_true: + case l_true: return l_true; - case l_undef: - found_undef = true; + case l_undef: + found_undef = true; break; default: break; @@ -515,7 +515,7 @@ namespace sat { // Propagation // // ----------------------- - + bool solver::propagate_core(bool update) { if (m_inconsistent) return false; @@ -545,7 +545,7 @@ namespace sat { } for (; it != end; ++it) { switch (it->get_kind()) { - case watched::BINARY: + case watched::BINARY: l1 = it->get_literal(); switch (value(l1)) { case l_false: @@ -585,12 +585,26 @@ namespace sat { break; case watched::CLAUSE: { if (value(it->get_blocked_literal()) == l_true) { + TRACE("propagate_clause_bug", tout << "blocked literal " << it->get_blocked_literal() << "\n"; + clause_offset cls_off = it->get_clause_offset(); + clause & c = *(m_cls_allocator.get_clause(cls_off)); + tout << c << "\n";); *it2 = *it; it2++; break; } clause_offset cls_off = it->get_clause_offset(); clause & c = *(m_cls_allocator.get_clause(cls_off)); + TRACE("propagate_clause_bug", tout << "processing... " << c << "\nwas_removed: " << c.was_removed() << "\n";); + if (c.was_removed()) { + // Remark: this method may be invoked when the watch lists are not in a consistent state, + // and may contain dead/removed clauses. + // See: sat_simplifier.cpp + // So, we must check whether the clause was marked for deletion, and ignore it. + *it2 = *it; + it2++; + break; + } if (c[0] == not_l) std::swap(c[0], c[1]); CTRACE("propagate_bug", c[1] != not_l, tout << "l: " << l << " " << c << "\n";); @@ -693,7 +707,7 @@ namespace sat { m_conflicts_since_restart = 0; m_restart_threshold = m_config.m_restart_initial; } - + // iff3_finder(*this)(); simplify_problem(); @@ -704,10 +718,10 @@ namespace sat { IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "\"abort: max-conflicts = 0\"\n";); return l_undef; } - + while (true) { SASSERT(!inconsistent()); - + lbool r = bounded_search(); if (r != l_undef) return r; @@ -716,7 +730,7 @@ namespace sat { IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "\"abort: max-conflicts = " << m_conflicts << "\"\n";); return l_undef; } - + restart(); if (m_conflicts >= m_next_simplify) { simplify_problem(); @@ -734,7 +748,7 @@ namespace sat { bool_var solver::next_var() { bool_var next; - + if (m_rand() < static_cast(m_config.m_random_freq * random_gen::max_value())) { if (num_vars() == 0) return null_bool_var; @@ -743,16 +757,16 @@ namespace sat { if (value(next) == l_undef && !was_eliminated(next)) return next; } - + while (!m_case_split_queue.empty()) { next = m_case_split_queue.next_var(); if (value(next) == l_undef && !was_eliminated(next)) return next; } - + return null_bool_var; } - + bool solver::decide() { bool_var next = next_var(); if (next == null_bool_var) @@ -760,7 +774,7 @@ namespace sat { push(); m_stats.m_decision++; lbool phase = m_ext ? m_ext->get_phase(next) : l_undef; - + if (phase == l_undef) { switch (m_config.m_phase) { case PS_ALWAYS_TRUE: @@ -784,7 +798,7 @@ namespace sat { break; } } - + SASSERT(phase != l_undef); literal next_lit(next, phase == l_false); assign(next_lit, justification()); @@ -807,23 +821,23 @@ namespace sat { return l_undef; if (scope_lvl() == 0) { cleanup(); // cleaner may propagate frozen clauses - if (inconsistent()) + if (inconsistent()) return l_false; gc(); } } - + gc(); if (!decide()) { if (m_ext) { switch (m_ext->check()) { - case CR_DONE: + case CR_DONE: mk_model(); return l_true; - case CR_CONTINUE: + case CR_CONTINUE: break; - case CR_GIVEUP: + case CR_GIVEUP: throw abort_solver(); } } @@ -849,23 +863,23 @@ namespace sat { m_stopwatch.reset(); m_stopwatch.start(); } - + /** \brief Apply all simplifications. */ void solver::simplify_problem() { SASSERT(scope_lvl() == 0); - + m_cleaner(); CASSERT("sat_simplify_bug", check_invariant()); - + m_scc(); CASSERT("sat_simplify_bug", check_invariant()); - - m_simplifier(false); + + m_simplifier(false); CASSERT("sat_simplify_bug", check_invariant()); CASSERT("sat_missed_prop", check_missed_propagation()); - + if (!m_learned.empty()) { m_simplifier(true); CASSERT("sat_missed_prop", check_missed_propagation()); @@ -878,11 +892,11 @@ namespace sat { m_probing(); CASSERT("sat_missed_prop", check_missed_propagation()); CASSERT("sat_simplify_bug", check_invariant()); - + m_asymm_branch(); CASSERT("sat_missed_prop", check_missed_propagation()); CASSERT("sat_simplify_bug", check_invariant()); - + if (m_ext) { m_ext->clauses_modifed(); m_ext->simplify(); @@ -956,7 +970,7 @@ namespace sat { } } } - if (!m_mc.check_model(m)) + if (!m_mc.check_model(m)) ok = false; CTRACE("sat_model_bug", !ok, tout << m << "\n";); return ok; @@ -964,9 +978,9 @@ namespace sat { void solver::restart() { m_stats.m_restart++; - IF_VERBOSE(1, + IF_VERBOSE(1, verbose_stream() << "(sat-restart :conflicts " << m_stats.m_conflict << " :decisions " << m_stats.m_decision - << " :restarts " << m_stats.m_restart << mk_stat(*this) + << " :restarts " << m_stats.m_restart << mk_stat(*this) << " :time " << std::fixed << std::setprecision(2) << m_stopwatch.get_current_seconds() << ")\n";); IF_VERBOSE(30, display_status(verbose_stream());); pop(scope_lvl()); @@ -991,9 +1005,9 @@ namespace sat { // GC // // ----------------------- - + void solver::gc() { - if (m_conflicts_since_gc <= m_gc_threshold) + if (m_conflicts_since_gc <= m_gc_threshold) return; CASSERT("sat_gc_bug", check_invariant()); switch (m_config.m_gc_strategy) { @@ -1073,7 +1087,7 @@ namespace sat { std::stable_sort(m_learned.begin(), m_learned.end(), glue_lt()); gc_half("glue"); } - + void solver::gc_psm() { save_psm(); std::stable_sort(m_learned.begin(), m_learned.end(), psm_lt()); @@ -1134,8 +1148,8 @@ namespace sat { void solver::gc_dyn_psm() { // To do gc at scope_lvl() > 0, I will need to use the reinitialization stack, or live with the fact // that I may miss some propagations for reactivated clauses. - SASSERT(scope_lvl() == 0); - // compute + SASSERT(scope_lvl() == 0); + // compute // d_tk unsigned h = 0; unsigned V_tk = 0; @@ -1152,7 +1166,7 @@ namespace sat { double d_tk = V_tk == 0 ? static_cast(num_vars() + 1) : static_cast(h)/static_cast(V_tk); if (d_tk < m_min_d_tk) m_min_d_tk = d_tk; - TRACE("sat_frozen", tout << "m_min_d_tk: " << m_min_d_tk << "\n";); + TRACE("sat_frozen", tout << "m_min_d_tk: " << m_min_d_tk << "\n";); unsigned frozen = 0; unsigned deleted = 0; unsigned activated = 0; @@ -1218,15 +1232,15 @@ namespace sat { ++it2; } m_learned.set_end(it2); - IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat-gc :d_tk " << d_tk << " :min-d_tk " << m_min_d_tk << + IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat-gc :d_tk " << d_tk << " :min-d_tk " << m_min_d_tk << " :frozen " << frozen << " :activated " << activated << " :deleted " << deleted << ")\n";); } - + // return true if should keep the clause, and false if we should delete it. - bool solver::activate_frozen_clause(clause & c) { + bool solver::activate_frozen_clause(clause & c) { TRACE("sat_gc", tout << "reactivating:\n" << c << "\n";); SASSERT(scope_lvl() == 0); - // do some cleanup + // do some cleanup unsigned sz = c.size(); unsigned j = 0; for (unsigned i = 0; i < sz; i++) { @@ -1292,7 +1306,7 @@ namespace sat { bool r = resolve_conflict_core(); CASSERT("sat_check_marks", check_marks()); // after pop, clauses are reinitialized, this may trigger another conflict. - if (!r) + if (!r) return false; if (!inconsistent()) return true; @@ -1311,7 +1325,7 @@ namespace sat { if (m_conflict_lvl == 0) return false; m_lemma.reset(); - + forget_phase_of_vars(m_conflict_lvl); unsigned idx = skip_literals_above_conflict_level(); @@ -1326,7 +1340,7 @@ namespace sat { literal consequent = m_not_l; justification js = m_conflict; - + do { TRACE("sat_conflict_detail", tout << "processing consequent: " << consequent << "\n"; tout << "num_marks: " << num_marks << ", js kind: " << js.get_kind() << "\n";); @@ -1362,7 +1376,7 @@ namespace sat { fill_ext_antecedents(consequent, js); literal_vector::iterator it = m_ext_antecedents.begin(); literal_vector::iterator end = m_ext_antecedents.end(); - for (; it != end; ++it) + for (; it != end; ++it) process_antecedent(*it, num_marks); break; } @@ -1370,10 +1384,10 @@ namespace sat { UNREACHABLE(); break; } - + while (true) { literal l = m_trail[idx]; - if (is_marked(l.var())) + if (is_marked(l.var())) break; SASSERT(idx > 0); idx--; @@ -1386,9 +1400,9 @@ namespace sat { idx--; num_marks--; reset_mark(c_var); - } + } while (num_marks > 0); - + m_lemma[0] = ~consequent; TRACE("sat_lemma", tout << "new lemma size: " << m_lemma.size() << "\n" << m_lemma << "\n";); @@ -1401,7 +1415,7 @@ namespace sat { } else reset_lemma_var_marks(); - + literal_vector::iterator it = m_lemma.begin(); literal_vector::iterator end = m_lemma.end(); unsigned new_scope_lvl = 0; @@ -1432,10 +1446,10 @@ namespace sat { return 0; unsigned r = 0; - + if (consequent != null_literal) r = lvl(consequent); - + switch (js.get_kind()) { case justification::NONE: break; @@ -1468,7 +1482,7 @@ namespace sat { fill_ext_antecedents(consequent, js); literal_vector::iterator it = m_ext_antecedents.begin(); literal_vector::iterator end = m_ext_antecedents.end(); - for (; it != end; ++it) + for (; it != end; ++it) r = std::max(r, lvl(*it)); break; } @@ -1497,7 +1511,7 @@ namespace sat { } return idx; } - + void solver::process_antecedent(literal antecedent, unsigned & num_marks) { bool_var var = antecedent.var(); unsigned var_lvl = lvl(var); @@ -1511,7 +1525,7 @@ namespace sat { m_lemma.push_back(~antecedent); } } - + /** \brief js is an external justification. Collect its antecedents and store at m_ext_antecedents. */ @@ -1578,7 +1592,7 @@ namespace sat { unsigned var_lvl = lvl(var); if (!is_marked(var) && var_lvl > 0) { if (m_lvl_set.may_contain(var_lvl)) { - mark(var); + mark(var); m_unmark.push_back(var); m_lemma_min_stack.push_back(var); } @@ -1590,17 +1604,17 @@ namespace sat { } /** - \brief Return true if lit is implied by other marked literals - and/or literals assigned at the base level. - The set lvl_set is used as an optimization. + \brief Return true if lit is implied by other marked literals + and/or literals assigned at the base level. + The set lvl_set is used as an optimization. The idea is to stop the recursive search with a failure - as soon as we find a literal assigned in a level that is not in lvl_set. + as soon as we find a literal assigned in a level that is not in lvl_set. */ bool solver::implied_by_marked(literal lit) { m_lemma_min_stack.reset(); // avoid recursive function m_lemma_min_stack.push_back(lit.var()); unsigned old_size = m_unmark.size(); - + while (!m_lemma_min_stack.empty()) { bool_var var = m_lemma_min_stack.back(); m_lemma_min_stack.pop_back(); @@ -1701,7 +1715,7 @@ namespace sat { void solver::minimize_lemma() { m_unmark.reset(); updt_lemma_lvl_set(); - + unsigned sz = m_lemma.size(); unsigned i = 1; // the first literal is the FUIP unsigned j = 1; @@ -1717,12 +1731,12 @@ namespace sat { j++; } } - + reset_unmark(0); m_lemma.shrink(j); m_stats.m_minimized_lits += sz - j; } - + /** \brief Reset the mark of the variables in the current lemma. */ @@ -1742,17 +1756,17 @@ namespace sat { Only binary and ternary clauses are used. */ void solver::dyn_sub_res() { - unsigned sz = m_lemma.size(); + unsigned sz = m_lemma.size(); for (unsigned i = 0; i < sz; i++) { mark_lit(m_lemma[i]); } - + literal l0 = m_lemma[0]; // l0 is the FUIP, and we never remove the FUIP. - // + // // In the following loop, we use unmark_lit(l) to remove a // literal from m_lemma. - + for (unsigned i = 0; i < sz; i++) { literal l = m_lemma[i]; if (!is_marked_lit(l)) @@ -1764,8 +1778,8 @@ namespace sat { for (; it != end; ++it) { // In this for-loop, the conditions l0 != ~l2 and l0 != ~l3 // are not really needed if the solver does not miss unit propagations. - // However, we add them anyway because we don't want to rely on this - // property of the propagator. + // However, we add them anyway because we don't want to rely on this + // property of the propagator. // For example, if this property is relaxed in the future, then the code // without the conditions l0 != ~l2 and l0 != ~l3 may remove the FUIP if (it->is_binary_clause()) { @@ -1811,10 +1825,10 @@ namespace sat { // p1 \/ ~p2 // p2 \/ ~p3 // p3 \/ ~p4 - // q1 \/ q2 \/ p1 \/ p2 \/ p3 \/ p4 \/ l2 - // q1 \/ ~q2 \/ p1 \/ p2 \/ p3 \/ p4 \/ l2 - // ~q1 \/ q2 \/ p1 \/ p2 \/ p3 \/ p4 \/ l2 - // ~q1 \/ ~q2 \/ p1 \/ p2 \/ p3 \/ p4 \/ l2 + // q1 \/ q2 \/ p1 \/ p2 \/ p3 \/ p4 \/ l2 + // q1 \/ ~q2 \/ p1 \/ p2 \/ p3 \/ p4 \/ l2 + // ~q1 \/ q2 \/ p1 \/ p2 \/ p3 \/ p4 \/ l2 + // ~q1 \/ ~q2 \/ p1 \/ p2 \/ p3 \/ p4 \/ l2 // ... // // 2. Now suppose we learned the lemma @@ -1825,15 +1839,15 @@ namespace sat { // That is, l \/ l2 is an implied clause. Note that probing does not add // this clause to the clause database (there are too many). // - // 4. Lemma (*) is deleted (garbage collected). + // 4. Lemma (*) is deleted (garbage collected). // // 5. l is decided to be false, p1, p2, p3 and p4 are propagated using BCP, // but l2 is not since the lemma (*) was deleted. - // + // // Probing module still "knows" that l \/ l2 is valid binary clause - // + // // 6. A new lemma is created where ~l2 is the FUIP and the lemma also contains l. - // If we remove l0 != ~l2 may try to delete the FUIP. + // If we remove l0 != ~l2 may try to delete the FUIP. if (is_marked_lit(~l2) && l0 != ~l2) { // eliminate ~l2 from lemma because we have the clause l \/ l2 unmark_lit(~l2); @@ -1844,7 +1858,7 @@ namespace sat { // can't eliminat FUIP SASSERT(is_marked_lit(m_lemma[0])); - + unsigned j = 0; for (unsigned i = 0; i < sz; i++) { literal l = m_lemma[i]; @@ -1856,7 +1870,7 @@ namespace sat { } m_stats.m_dyn_sub_res += sz - j; - + SASSERT(j >= 1); m_lemma.shrink(j); } @@ -1949,7 +1963,7 @@ namespace sat { // Misc // // ----------------------- - + void solver::updt_params(params_ref const & p) { m_params = p; m_config.updt_params(p); @@ -1971,7 +1985,7 @@ namespace sat { void solver::set_cancel(bool f) { m_cancel = f; } - + void solver::collect_statistics(statistics & st) { m_stats.collect_statistics(st); m_cleaner.collect_statistics(st); @@ -2067,7 +2081,7 @@ namespace sat { } } } - + void solver::display_units(std::ostream & out) const { unsigned end = scope_lvl() == 0 ? m_trail.size() : m_scopes[0].m_trail_lim; for (unsigned i = 0; i < end; i++) { @@ -2221,26 +2235,26 @@ namespace sat { // Simplification // // ----------------------- - void solver::cleanup() { - if (scope_lvl() > 0 || inconsistent()) - return; + void solver::cleanup() { + if (scope_lvl() > 0 || inconsistent()) + return; if (m_cleaner() && m_ext) m_ext->clauses_modifed(); } - void solver::simplify(bool learned) { - if (scope_lvl() > 0 || inconsistent()) - return; - m_simplifier(learned); - m_simplifier.free_memory(); + void solver::simplify(bool learned) { + if (scope_lvl() > 0 || inconsistent()) + return; + m_simplifier(learned); + m_simplifier.free_memory(); if (m_ext) m_ext->clauses_modifed(); } - unsigned solver::scc_bin() { - if (scope_lvl() > 0 || inconsistent()) - return 0; - unsigned r = m_scc(); + unsigned solver::scc_bin() { + if (scope_lvl() > 0 || inconsistent()) + return 0; + unsigned r = m_scc(); if (r > 0 && m_ext) m_ext->clauses_modifed(); return r; @@ -2314,10 +2328,10 @@ namespace sat { out << " :inconsistent " << (m_inconsistent ? "true" : "false") << "\n"; out << " :vars " << num_vars() << "\n"; out << " :elim-vars " << num_elim << "\n"; - out << " :lits " << num_lits << "\n"; + out << " :lits " << num_lits << "\n"; out << " :assigned " << m_trail.size() << "\n"; - out << " :binary-clauses " << num_bin << "\n"; - out << " :ternary-clauses " << num_ter << "\n"; + out << " :binary-clauses " << num_bin << "\n"; + out << " :ternary-clauses " << num_ter << "\n"; out << " :clauses " << num_cls << "\n"; out << " :del-clause " << m_stats.m_del_clause << "\n"; out << " :avg-clause-size " << (total_cls == 0 ? 0.0 : static_cast(num_lits) / static_cast(total_cls)) << "\n"; From 88675ec728695d7df4e6f6ce8622332c23f1ed8f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 4 Nov 2013 12:24:25 -0800 Subject: [PATCH 26/27] fix assertion violations (reported by Christoph Wintersteiger) at sage/bench_1300.smt2 and sage/bench/2861.smt2 Signed-off-by: Leonardo de Moura --- src/sat/sat_solver.cpp | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index bb08ae5c3..f4bf5393c 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -596,18 +596,19 @@ namespace sat { clause_offset cls_off = it->get_clause_offset(); clause & c = *(m_cls_allocator.get_clause(cls_off)); TRACE("propagate_clause_bug", tout << "processing... " << c << "\nwas_removed: " << c.was_removed() << "\n";); - if (c.was_removed()) { + if (c[0] == not_l) + std::swap(c[0], c[1]); + CTRACE("propagate_bug", c[1] != not_l, tout << "l: " << l << " " << c << "\n";); + if (c.was_removed() || c[1] != not_l) { // Remark: this method may be invoked when the watch lists are not in a consistent state, - // and may contain dead/removed clauses. - // See: sat_simplifier.cpp - // So, we must check whether the clause was marked for deletion, and ignore it. + // and may contain dead/removed clauses, or clauses with removed literals. + // See: method propagate_unit at sat_simplifier.cpp + // So, we must check whether the clause was marked for deletion, or + // c[1] != not_l *it2 = *it; it2++; break; } - if (c[0] == not_l) - std::swap(c[0], c[1]); - CTRACE("propagate_bug", c[1] != not_l, tout << "l: " << l << " " << c << "\n";); SASSERT(c[1] == not_l); if (value(c[0]) == l_true) { it2->set_clause(c[0], cls_off); From 063f6fe15f7a0269359a59e6129b796a1e6950ae Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 4 Nov 2013 12:26:20 -0800 Subject: [PATCH 27/27] fix assertion violations (reported by Christoph Wintersteiger) at sage\app8\bench_2174.smt2, sage\app9\bench_1450.smt2, sage\app9\bench_1546.smt2 Signed-off-by: Leonardo de Moura --- src/sat/sat_simplifier.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 37d41a5fd..f20ffa7c7 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -407,7 +407,7 @@ namespace sat { remove_clause(c2); m_num_subsumed++; } - else { + else if (!c2.was_removed()) { // subsumption resolution TRACE("subsumption_resolution", tout << c1 << " sub-ref(" << *l_it << ") " << c2 << "\n";); elim_lit(c2, *l_it);