From 4da56aa4dff9b7830ffcb7d393d8b367c0d3774d Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 29 May 2014 12:41:07 +0100 Subject: [PATCH 1/9] added debug assertion Signed-off-by: Christoph M. Wintersteiger --- src/api/python/z3.py | 1 + 1 file changed, 1 insertion(+) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 9233a41dc..4eae61c3d 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -4128,6 +4128,7 @@ class Datatype: """ if __debug__: _z3_assert(isinstance(name, str), "String expected") + _z3_assert(name != "") return self.declare_core(name, "is_" + name, *args) def __repr__(self): From 756645326bb2c0578b340e05e03c8276cacd1dd9 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 29 May 2014 17:33:03 +0100 Subject: [PATCH 2/9] Bugfix for And/Or operators in Python. Signed-off-by: Christoph M. Wintersteiger --- src/api/python/z3.py | 27 +++++++++++++++++++++++---- 1 file changed, 23 insertions(+), 4 deletions(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 4eae61c3d..ff0bd6641 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -899,6 +899,7 @@ def _coerce_expr_merge(s, a): return s else: if __debug__: + _z3_assert(s1.ctx == s.ctx, "context mismatch") _z3_assert(False, "sort mismatch") else: return s @@ -1459,9 +1460,18 @@ def And(*args): >>> And(P) And(p__0, p__1, p__2, p__3, p__4) """ - args = _get_args(args) - ctx = _ctx_from_ast_arg_list(args) + last_arg = None + if len(args) > 0: + last_arg = args[len(args)-1] + if isinstance(last_arg, Context): + ctx = args[len(args)-1] + args = args[:len(args)-1] + else: + ctx = main_ctx() + args = _get_args(args) + ctx_args = _ctx_from_ast_arg_list(args, ctx) if __debug__: + _z3_assert(ctx_args == None or ctx_args == ctx, "context mismatch") _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression or probe") if _has_probe(args): return _probe_and(args, ctx) @@ -1480,9 +1490,18 @@ def Or(*args): >>> Or(P) Or(p__0, p__1, p__2, p__3, p__4) """ - args = _get_args(args) - ctx = _ctx_from_ast_arg_list(args) + last_arg = None + if len(args) > 0: + last_arg = args[len(args)-1] + if isinstance(last_arg, Context): + ctx = args[len(args)-1] + args = args[:len(args)-1] + else: + ctx = main_ctx() + args = _get_args(args) + ctx_args = _ctx_from_ast_arg_list(args, ctx) if __debug__: + _z3_assert(ctx_args == None or ctx_args == ctx, "context mismatch") _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression or probe") if _has_probe(args): return _probe_or(args, ctx) From 1e774064bc9fbfde8c873c6664044b7e28645363 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 30 May 2014 12:26:55 +0100 Subject: [PATCH 3/9] assertion bug fix in z3py Signed-off-by: Christoph M. Wintersteiger --- 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 ff0bd6641..ce53a4c1f 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -4147,7 +4147,7 @@ class Datatype: """ if __debug__: _z3_assert(isinstance(name, str), "String expected") - _z3_assert(name != "") + _z3_assert(name != "", "Constructor name cannot be empty") return self.declare_core(name, "is_" + name, *args) def __repr__(self): From 49f9f4b3b53191e965e7a59dfd3b4868caa719ca Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 30 May 2014 20:52:39 +0530 Subject: [PATCH 4/9] fix crash in model construction from finite domain theory Signed-off-by: Nikolaj Bjorner --- src/ast/dl_decl_plugin.cpp | 18 +++++++++++++++++- src/ast/dl_decl_plugin.h | 2 ++ src/smt/smt_model_generator.cpp | 2 ++ src/smt/theory_dl.cpp | 7 +++---- 4 files changed, 24 insertions(+), 5 deletions(-) diff --git a/src/ast/dl_decl_plugin.cpp b/src/ast/dl_decl_plugin.cpp index 6d0823a24..badf8a59d 100644 --- a/src/ast/dl_decl_plugin.cpp +++ b/src/ast/dl_decl_plugin.cpp @@ -599,7 +599,23 @@ namespace datalog { return 0; } result = mk_compare(OP_DL_LT, m_lt_sym, domain); - break; + break; + + case OP_DL_REP: { + if (!check_domain(0, 0, num_parameters) || + !check_domain(1, 1, arity)) return 0; + func_decl_info info(m_family_id, k, 0, 0); + result = m_manager->mk_func_decl(symbol("rep"), 1, domain, range, info); + break; + } + + case OP_DL_ABS: { + if (!check_domain(0, 0, num_parameters) || + !check_domain(1, 1, arity)) return 0; + func_decl_info info(m_family_id, k, 0, 0); + result = m_manager->mk_func_decl(symbol("abs"), 1, domain, range, info); + break; + } default: m_manager->raise_exception("operator not recognized"); diff --git a/src/ast/dl_decl_plugin.h b/src/ast/dl_decl_plugin.h index a662de578..65b00235c 100644 --- a/src/ast/dl_decl_plugin.h +++ b/src/ast/dl_decl_plugin.h @@ -48,6 +48,8 @@ namespace datalog { OP_RA_CLONE, OP_DL_CONSTANT, OP_DL_LT, + OP_DL_REP, + OP_DL_ABS, LAST_RA_OP }; diff --git a/src/smt/smt_model_generator.cpp b/src/smt/smt_model_generator.cpp index cf22c3e3a..6c138fd57 100644 --- a/src/smt/smt_model_generator.cpp +++ b/src/smt/smt_model_generator.cpp @@ -102,6 +102,7 @@ namespace smt { if (th && th->build_models()) { if (r->get_th_var(th->get_id()) != null_theory_var) { proc = th->mk_value(r, *this); + SASSERT(proc); } else { TRACE("model_bug", tout << "creating fresh value for #" << r->get_owner_id() << "\n";); @@ -110,6 +111,7 @@ namespace smt { } else { proc = mk_model_value(r); + SASSERT(proc); } } SASSERT(proc); diff --git a/src/smt/theory_dl.cpp b/src/smt/theory_dl.cpp index 4ef1bd8e0..fc9138bf6 100644 --- a/src/smt/theory_dl.cpp +++ b/src/smt/theory_dl.cpp @@ -162,7 +162,7 @@ namespace smt { m.register_factory(alloc(dl_factory, m_util, m.get_model())); } - virtual smt::model_value_proc * mk_value(smt::enode * n) { + virtual smt::model_value_proc * mk_value(smt::enode * n, smt::model_generator&) { return alloc(dl_value_proc, *this, n); } @@ -201,9 +201,8 @@ namespace smt { if(!m_reps.find(s, r) || !m_vals.find(s,v)) { SASSERT(!m_reps.contains(s)); sort* bv = b().mk_sort(64); - // TBD: filter these from model. - r = m().mk_fresh_func_decl("rep",1, &s,bv); - v = m().mk_fresh_func_decl("val",1, &bv,s); + r = m().mk_func_decl(m_util.get_family_id(), datalog::OP_DL_REP, 0, 0, 1, &s, bv); + v = m().mk_func_decl(m_util.get_family_id(), datalog::OP_DL_ABS, 0, 0, 1, &bv, s); m_reps.insert(s, r); m_vals.insert(s, v); add_trail(r); From bc25ea404fc251bb3343bb724abf8cef24356947 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 30 May 2014 18:14:33 +0100 Subject: [PATCH 5/9] Fixed potential bug (warning on OSX). Signed-off-by: Christoph M. Wintersteiger --- src/smt/theory_arith_eq.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/theory_arith_eq.h b/src/smt/theory_arith_eq.h index 04e16e778..368ccb87d 100644 --- a/src/smt/theory_arith_eq.h +++ b/src/smt/theory_arith_eq.h @@ -193,7 +193,7 @@ namespace smt { return true; } - if (!r.get_base_var() == x && x > y) { + if (r.get_base_var() != x && x > y) { std::swap(x, y); k.neg(); } From f76b343bfa4d65417e2366da199189617604fa3a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 31 May 2014 11:25:54 +0530 Subject: [PATCH 6/9] expose parameter settings for controlling injectivity axiom. rquested by Jasmin Blanchette Signed-off-by: Nikolaj Bjorner --- src/smt/params/preprocessor_params.cpp | 1 + src/smt/params/smt_params_helper.pyg | 1 + 2 files changed, 2 insertions(+) diff --git a/src/smt/params/preprocessor_params.cpp b/src/smt/params/preprocessor_params.cpp index 4799b8b9f..9ad787c2a 100644 --- a/src/smt/params/preprocessor_params.cpp +++ b/src/smt/params/preprocessor_params.cpp @@ -23,6 +23,7 @@ void preprocessor_params::updt_local_params(params_ref const & _p) { smt_params_helper p(_p); m_macro_finder = p.macro_finder(); m_pull_nested_quantifiers = p.pull_nested_quantifiers(); + m_refine_inj_axiom = p.refine_inj_axioms(); } void preprocessor_params::updt_params(params_ref const & p) { diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 50bb6422b..869b8cdc4 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -14,6 +14,7 @@ def_module_params(module_name='smt', ('delay_units', BOOL, False, 'if true then z3 will not restart when a unit clause is learned'), ('delay_units_threshold', UINT, 32, 'maximum number of learned unit clauses before restarting, ingored if delay_units is false'), ('pull_nested_quantifiers', BOOL, False, 'pull nested quantifiers'), + ('refine_inj_axioms', BOOL, True, 'refine injectivity axioms'), ('soft_timeout', UINT, 0, 'soft timeout (0 means no timeout)'), ('mbqi', BOOL, True, 'model based quantifier instantiation (MBQI)'), ('mbqi.max_cexs', UINT, 1, 'initial maximal number of counterexamples used in MBQI, each counterexample generates a quantifier instantiation'), From 88bd01bc4fabb2800b3abfe6badf2bd3ae0fa68e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 3 Jun 2014 23:03:34 +0530 Subject: [PATCH 7/9] patching non-termination bug in datatype factory, reported by Tiago Signed-off-by: Nikolaj Bjorner --- src/smt/proto_model/datatype_factory.cpp | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/src/smt/proto_model/datatype_factory.cpp b/src/smt/proto_model/datatype_factory.cpp index 5e66ab738..3b0ec8e5f 100644 --- a/src/smt/proto_model/datatype_factory.cpp +++ b/src/smt/proto_model/datatype_factory.cpp @@ -191,8 +191,10 @@ expr * datatype_factory::get_fresh_value(sort * s) { // Approach 2) // For recursive datatypes. // search for constructor... + unsigned num_iterations = 0; if (m_util.is_recursive(s)) { while(true) { + ++num_iterations; TRACE("datatype_factory", tout << mk_pp(get_last_fresh_value(s), m_manager) << "\n";); ptr_vector const * constructors = m_util.get_datatype_constructors(s); ptr_vector::const_iterator it = constructors->begin(); @@ -212,7 +214,13 @@ expr * datatype_factory::get_fresh_value(sort * s) { << found_sibling << "\n";); if (!found_sibling && m_util.is_datatype(s_arg) && m_util.are_siblings(s, s_arg)) { found_sibling = true; - expr * maybe_new_arg = get_almost_fresh_value(s_arg); + expr * maybe_new_arg = 0; + if (num_iterations <= 1) { + maybe_new_arg = get_almost_fresh_value(s_arg); + } + else { + maybe_new_arg = get_fresh_value(s_arg); + } if (!maybe_new_arg) { TRACE("datatype_factory", tout << "no argument found for " << mk_pp(s_arg, m_manager) << "\n";); @@ -231,6 +239,7 @@ expr * datatype_factory::get_fresh_value(sort * s) { if (found_sibling) { expr_ref new_value(m_manager); new_value = m_manager.mk_app(constructor, args.size(), args.c_ptr()); + TRACE("datatype_factory", tout << "potential new value: " << mk_pp(new_value, m_manager) << "\n";); m_last_fresh_value.insert(s, new_value); if (!set->contains(new_value)) { register_value(new_value); From 8ef4ec7009abaeefa415b1a5b93f020bec3e3ae2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 8 Jun 2014 12:46:23 +0100 Subject: [PATCH 8/9] fix bit-vector rotation left bug Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp | 3 +++ src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h | 10 ++++++++-- src/ast/rewriter/bv_rewriter.cpp | 1 + 3 files changed, 12 insertions(+), 2 deletions(-) diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp index 80d319377..63843d31e 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp +++ b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp @@ -323,6 +323,9 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend); br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { result_pr = 0; + TRACE("bit_blaster", tout << f->get_name() << " "; + for (unsigned i = 0; i < num; ++i) tout << mk_pp(args[i], m()) << " "; + tout << "\n";); if (num == 0 && f->get_family_id() == null_family_id && butil().is_bv_sort(f->get_range())) { mk_const(f, result); return BR_DONE; diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h index 72c0a447e..b41aa2238 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h +++ b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h @@ -828,6 +828,12 @@ void bit_blaster_tpl::mk_eq(unsigned sz, expr * const * a_bits, expr * cons template void bit_blaster_tpl::mk_rotate_left(unsigned sz, expr * const * a_bits, unsigned n, expr_ref_vector & out_bits) { + TRACE("bit_blaster", tout << n << ": " << sz << " "; + for (unsigned i = 0; i < sz; ++i) { + tout << mk_pp(a_bits[i], m()) << " "; + } + tout << "\n"; + ); n = n % sz; for (unsigned i = sz - n; i < sz; i++) out_bits.push_back(a_bits[i]); @@ -974,7 +980,7 @@ void bit_blaster_tpl::mk_ashr(unsigned sz, expr * const * a_bits, expr * co mk_ite(eqs.get(i - j), a_bits[sz - j - 1], out, new_out); out = new_out; } - TRACE("bit_blaster_tpl", tout << (sz - i - 1) << " :\n" << mk_pp(out, m()) << "\n";); + TRACE("bit_blaster", tout << (sz - i - 1) << " :\n" << mk_pp(out, m()) << "\n";); out_bits.set(sz - i - 1, out); } } @@ -1004,7 +1010,7 @@ void bit_blaster_tpl::mk_ext_rotate_left_right(unsigned sz, expr * const * out = a_bits[i]; for (unsigned j = 1; j < sz; j++) { expr_ref new_out(m()); - unsigned src = (Left ? (i - j) : (i + j)) % sz; + unsigned src = (Left ? (sz + i - j) : (i + j)) % sz; mk_ite(eqs.get(j), a_bits[src], out, new_out); out = new_out; } diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp index 11b09003b..1115663d2 100644 --- a/src/ast/rewriter/bv_rewriter.cpp +++ b/src/ast/rewriter/bv_rewriter.cpp @@ -21,6 +21,7 @@ Notes: #include"poly_rewriter_def.h" #include"ast_smt2_pp.h" + mk_extract_proc::mk_extract_proc(bv_util & u): m_util(u), m_high(0), From a5e3713c2c5e1065510d927a9c07ab240b3bf870 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 14 Jun 2014 05:47:42 -0700 Subject: [PATCH 9/9] fix unmatched parenthsis and code odor Signed-off-by: Nikolaj Bjorner --- examples/tptp/tptp5.cpp | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/examples/tptp/tptp5.cpp b/examples/tptp/tptp5.cpp index d0e174914..00d03a8b0 100644 --- a/examples/tptp/tptp5.cpp +++ b/examples/tptp/tptp5.cpp @@ -1630,10 +1630,8 @@ public: unsigned parent_id = Z3_get_ast_id(ctx, p.arg(0)); std::set const& hyps = m_proof_hypotheses.find(parent_id)->second; print_hypotheses(out, hyps); - out << ").\n"; + out << "))).\n"; break; - display_inference(out, "lemma", "thm", p); - break; } case Z3_OP_PR_UNIT_RESOLUTION: display_inference(out, "unit_resolution", "thm", p);