From e21bd8dacc58b95c2d207092b1ec4a932b260086 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 15 Nov 2016 15:07:05 +0200 Subject: [PATCH 1/2] 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/2] 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) {