From e21bd8dacc58b95c2d207092b1ec4a932b260086 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 15 Nov 2016 15:07:05 +0200 Subject: [PATCH 1/5] fix lexicographic combinations for wmax: pb constrsaints were not interpreted in Boolean benchmarks. #782 Signed-off-by: Nikolaj Bjorner --- src/ast/pb_decl_plugin.h | 2 ++ src/muz/pdr/pdr_context.cpp | 1 + src/opt/maxsmt.cpp | 8 ++++++++ src/smt/theory_pb.h | 1 + 4 files changed, 12 insertions(+) diff --git a/src/ast/pb_decl_plugin.h b/src/ast/pb_decl_plugin.h index 2ed14a4ce..0750dcac7 100644 --- a/src/ast/pb_decl_plugin.h +++ b/src/ast/pb_decl_plugin.h @@ -73,6 +73,8 @@ public: unsigned arity, sort * const * domain, sort * range); virtual void get_op_names(svector & op_names, symbol const & logic); + virtual bool is_considered_uninterpreted(func_decl * f) { return false; } + }; diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp index b6a889756..6d3a57581 100644 --- a/src/muz/pdr/pdr_context.cpp +++ b/src/muz/pdr/pdr_context.cpp @@ -1760,6 +1760,7 @@ namespace pdr { smt::kernel solver(m, get_fparams()); solver.assert_expr(tmp); lbool res = solver.check(); + TRACE("pdr", tout << tmp << " " << res << "\n";); if (res != l_false) { msg << "rule validation failed when checking: " << mk_pp(tmp, m); IF_VERBOSE(0, verbose_stream() << msg.str() << "\n";); diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index fa4897046..7d3e8eda9 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -25,6 +25,7 @@ Notes: #include "uint_set.h" #include "opt_context.h" #include "theory_wmaxsat.h" +#include "theory_pb.h" #include "ast_util.h" #include "pb_decl_plugin.h" @@ -124,6 +125,13 @@ namespace opt { wth = alloc(smt::theory_wmaxsat, m, m_c.fm()); m_c.smt_context().register_plugin(wth); } + smt::theory_id th_pb = m.get_family_id("pb"); + smt::theory_pb* pb = dynamic_cast(m_c.smt_context().get_theory(th_pb)); + if (!pb) { + theory_pb_params params; + pb = alloc(smt::theory_pb, m, params); + m_c.smt_context().register_plugin(pb); + } return wth; } diff --git a/src/smt/theory_pb.h b/src/smt/theory_pb.h index b9fddba38..1a08b7b61 100644 --- a/src/smt/theory_pb.h +++ b/src/smt/theory_pb.h @@ -316,6 +316,7 @@ namespace smt { virtual void collect_statistics(::statistics & st) const; virtual model_value_proc * mk_value(enode * n, model_generator & mg); virtual void init_model(model_generator & m); + virtual bool include_func_interp(func_decl* f) { return false; } static literal assert_ge(context& ctx, unsigned k, unsigned n, literal const* xs); }; From e65d80dedd3ef33a3279d0a0abaea6b0631174d9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 15 Nov 2016 18:29:51 +0200 Subject: [PATCH 2/5] make semantics of extract/substr deterministic. Issue #781 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 37 ++++++++++++++++++++++--------------- 1 file changed, 22 insertions(+), 15 deletions(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index afb6d21b3..245ffe438 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -3259,15 +3259,18 @@ bool theory_seq::get_length(expr* e, rational& val) const { let e = extract(s, i, l) - 0 <= i <= len(s) -> prefix(xe,s) - 0 <= i <= len(s) -> len(x) = i - 0 <= i <= len(s) & 0 <= l <= len(s) - i -> len(e) = l - 0 <= i <= len(s) & len(s) < l + i -> len(e) = len(s) - i - 0 <= i <= len(s) & l < 0 -> len(e) = 0 - * i < 0 -> e = empty - * i > len(s) -> e = empty + 0 <= i <= |s| -> prefix(xe,s) + 0 <= i <= |s| -> len(x) = i + 0 <= i <= |s| & 0 <= l <= |s| - i -> |e| = l + 0 <= i <= |s| & |s| < l + i -> |e| = |s| - i + 0 <= i <= |s| & l < 0 -> |e| = 0 + i >= |s| => |e| = 0 + i < 0 => |e| = 0 + l <= 0 => |e| = 0 + + It follows that: + |e| = min(l, |s| - i) for 0 <= i < |s| and 0 < |l| - */ @@ -3301,16 +3304,20 @@ void theory_seq::add_extract_axiom(expr* e) { expr_ref zero(m_autil.mk_int(0), m); literal i_ge_0 = mk_literal(m_autil.mk_ge(i, zero)); - literal i_le_ls = mk_literal(m_autil.mk_le(mk_sub(i, ls), zero)); + literal ls_le_i = mk_literal(m_autil.mk_le(mk_sub(i, ls), zero)); literal li_ge_ls = mk_literal(m_autil.mk_ge(ls_minus_i_l, zero)); literal l_ge_zero = mk_literal(m_autil.mk_ge(l, zero)); + literal ls_le_0 = mk_literal(m_autil.mk_le(ls, zero)); -// add_axiom(~i_ge_0, ~i_le_ls, mk_literal(m_util.str.mk_prefix(xe, s))); - add_axiom(~i_ge_0, ~i_le_ls, mk_seq_eq(xey, s)); - add_axiom(~i_ge_0, ~i_le_ls, mk_eq(lx, i, false)); - add_axiom(~i_ge_0, ~i_le_ls, ~l_ge_zero, ~li_ge_ls, mk_eq(le, l, false)); - add_axiom(~i_ge_0, ~i_le_ls, li_ge_ls, mk_eq(le, mk_sub(ls, i), false)); - add_axiom(~i_ge_0, ~i_le_ls, l_ge_zero, mk_eq(le, zero, false)); +// add_axiom(~i_ge_0, ~ls_le_i, mk_literal(m_util.str.mk_prefix(xe, s))); + add_axiom(~i_ge_0, ~ls_le_i, mk_seq_eq(xey, s)); + add_axiom(~i_ge_0, ~ls_le_i, mk_eq(lx, i, false)); + add_axiom(~i_ge_0, ~ls_le_i, ~l_ge_zero, ~li_ge_ls, mk_eq(le, l, false)); + add_axiom(~i_ge_0, ~ls_le_i, li_ge_ls, mk_eq(le, mk_sub(ls, i), false)); + add_axiom(~i_ge_0, ~ls_le_i, l_ge_zero, mk_eq(le, zero, false)); + add_axiom(i_ge_0, mk_eq(le, zero, false)); + add_axiom(ls_le_i, mk_eq(le, zero, false)); + add_axiom(~ls_le_0, mk_eq(le, zero, false)); } void theory_seq::add_tail_axiom(expr* e, expr* s) { From 014815a6408a1c54ee6c324353880fe46e46bf0a Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 15 Nov 2016 08:59:18 -0800 Subject: [PATCH 3/5] Fixed Windows distribution script. --- scripts/mk_win_dist.py | 26 ++++++++++---------------- 1 file changed, 10 insertions(+), 16 deletions(-) diff --git a/scripts/mk_win_dist.py b/scripts/mk_win_dist.py index 65d780f0d..92d89480f 100644 --- a/scripts/mk_win_dist.py +++ b/scripts/mk_win_dist.py @@ -236,23 +236,9 @@ def mk_zip(): VS_RUNTIME_PATS = [re.compile('vcomp.*\.dll'), re.compile('msvcp.*\.dll'), re.compile('msvcr.*\.dll')] - -VS_RUNTIME_FILES = [] -def cp_vs_runtime_visitor(pattern, dir, files): - global VS_RUNTIME_FILES - for filename in files: - for pat in VS_RUNTIME_PATS: - if pat.match(filename): - if fnmatch(filename, pattern): - fname = os.path.join(dir, filename) - if not os.path.isdir(fname): - VS_RUNTIME_FILES.append(fname) - break - # Copy Visual Studio Runtime libraries -def cp_vs_runtime_core(x64): - global VS_RUNTIME_FILES +def cp_vs_runtime_core(x64): if x64: platform = "x64" @@ -261,7 +247,15 @@ def cp_vs_runtime_core(x64): vcdir = os.environ['VCINSTALLDIR'] path = '%sredist\\%s' % (vcdir, platform) VS_RUNTIME_FILES = [] - os.walk(path, cp_vs_runtime_visitor, '*.dll') + for root, dirs, files in os.walk(path): + for filename in files: + if fnmatch(filename, '*.dll'): + for pat in VS_RUNTIME_PATS: + if pat.match(filename): + fname = os.path.join(root, filename) + if not os.path.isdir(fname): + VS_RUNTIME_FILES.append(fname) + bin_dist_path = os.path.join(DIST_DIR, get_dist_path(x64), 'bin') for f in VS_RUNTIME_FILES: shutil.copy(f, bin_dist_path) From ee60ba824f0a116ec0bb5e9e615dd4fe2e9802db Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 15 Nov 2016 19:59:08 +0000 Subject: [PATCH 4/5] Bugfix for rewriter exceptions in theory_fpa. Relates to #570. --- src/smt/theory_fpa.cpp | 37 ++++++++++++++++++++++--------------- 1 file changed, 22 insertions(+), 15 deletions(-) diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 89acc0ecf..4b53c1341 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -334,23 +334,30 @@ namespace smt { TRACE("t_fpa_detail", tout << "term: " << mk_ismt2_pp(e, get_manager()) << std::endl; tout << "converted term: " << mk_ismt2_pp(e_conv, get_manager()) << std::endl;); - if (m_fpa_util.is_rm(e)) { - SASSERT(m_fpa_util.is_bv2rm(e_conv)); - expr_ref bv_rm(m); - m_th_rw(to_app(e_conv)->get_arg(0), bv_rm); - res = m_fpa_util.mk_bv2rm(bv_rm); + try { + if (m_fpa_util.is_rm(e)) { + SASSERT(m_fpa_util.is_bv2rm(e_conv)); + expr_ref bv_rm(m); + m_th_rw(to_app(e_conv)->get_arg(0), bv_rm); + res = m_fpa_util.mk_bv2rm(bv_rm); + } + else if (m_fpa_util.is_float(e)) { + SASSERT(m_fpa_util.is_fp(e_conv)); + expr_ref sgn(m), sig(m), exp(m); + m_converter.split_fp(e_conv, sgn, exp, sig); + m_th_rw(sgn); + m_th_rw(exp); + m_th_rw(sig); + res = m_fpa_util.mk_fp(sgn, exp, sig); + } + else + UNREACHABLE(); } - else if (m_fpa_util.is_float(e)) { - SASSERT(m_fpa_util.is_fp(e_conv)); - expr_ref sgn(m), sig(m), exp(m); - m_converter.split_fp(e_conv, sgn, exp, sig); - m_th_rw(sgn); - m_th_rw(exp); - m_th_rw(sig); - res = m_fpa_util.mk_fp(sgn, exp, sig); + catch (rewriter_exception &) + { + m_th_rw.reset(); + throw; } - else - UNREACHABLE(); return res; } From c7787feebb5ed79b2274741b4f24299aa87a2057 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 15 Nov 2016 19:59:22 +0000 Subject: [PATCH 5/5] Assertion fix for theory_fpa. Relates to #570. --- src/smt/theory_fpa.cpp | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 4b53c1341..57cd6a914 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -750,8 +750,15 @@ namespace smt { // These are the conversion functions fp.to_* */ SASSERT(!m_fpa_util.is_float(n) && !m_fpa_util.is_rm(n)); } - else - UNREACHABLE(); + else { + /* Theory variables can be merged when (= bv-term (bvwrap fp-term)), + in which case context::relevant_eh may call theory_fpa::relevant_eh + after theory_bv::relevant_eh, regardless of whether theory_fpa is + interested in this term. But, this can only happen because of + (bvwrap ...) terms, i.e., `n' must be a bit-vector expression, + which we can safely ignore. */ + SASSERT(m_bv_util.is_bv(n)); + } } void theory_fpa::reset_eh() {