From 2d41b0e29b150629bb68119686cf7a91e78e9aad Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 15 Jan 2016 03:31:30 +0530 Subject: [PATCH 01/17] fix tout -> out. Tune generation of automata transitions Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 57 ++++++++++++++++++++----------- src/ast/rewriter/seq_rewriter.h | 21 ++++++++---- src/smt/theory_seq.cpp | 15 +++----- 3 files changed, 57 insertions(+), 36 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 80d125c32..1cbc2d288 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -29,12 +29,27 @@ Notes: expr_ref sym_expr::accept(expr* e) { ast_manager& m = m_t.get_manager(); expr_ref result(m); - if (m_is_pred) { + switch (m_ty) { + case t_pred: { var_subst subst(m); subst(m_t, 1, &e, result); + break; } - else { + case t_char: result = m.mk_eq(e, m_t); + break; + case t_range: { + bv_util bv(m); + rational r1, r2, r3; + unsigned sz; + if (bv.is_numeral(m_t, r1, sz) && bv.is_numeral(e, r2, sz) && bv.is_numeral(m_s, r3, sz)) { + result = m.mk_bool_val((r1 <= r2) && (r2 <= r3)); + } + else { + result = m.mk_and(bv.mk_ule(m_t, e), bv.mk_ule(e, m_s)); + } + break; + } } return result; } @@ -104,8 +119,7 @@ eautomaton* re2automaton::re2aut(expr* e) { expr_ref v(m.mk_var(0, s), m); expr_ref _start(bv.mk_numeral(start, nb), m); expr_ref _stop(bv.mk_numeral(stop, nb), m); - expr_ref cond(m.mk_and(bv.mk_ule(_start, v), bv.mk_ule(v, _stop)), m); - a = alloc(eautomaton, sm, sym_expr::mk_pred(cond)); + a = alloc(eautomaton, sm, sym_expr::mk_range(_start, _stop)); return a.detach(); } else { @@ -703,7 +717,8 @@ br_status seq_rewriter::mk_str_stoi(expr* a, expr_ref& result) { void seq_rewriter::add_next(u_map& next, expr_ref_vector& trail, unsigned idx, expr* cond) { expr* acc; if (!m().is_true(cond) && next.find(idx, acc)) { - cond = m().mk_or(cond, acc); + expr* args[2] = { cond, acc }; + cond = mk_or(m(), 2, args); } trail.push_back(cond); next.insert(idx, cond); @@ -817,7 +832,7 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) { aut->get_moves_from(state, mvs, false); for (unsigned j = 0; j < mvs.size(); ++j) { eautomaton::move const& mv = mvs[j]; - SASSERT(mv.t()); + SASSERT(mv.t()); if (mv.t()->is_char() && m().is_value(mv.t()->get_char()) && m().is_value(ch)) { if (mv.t()->get_char() == ch) { add_next(next, trail, mv.dst(), acc); @@ -828,7 +843,11 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) { } else { cond = mv.t()->accept(ch); - if (!m().is_true(acc)) cond = m().mk_and(acc, cond); + if (m().is_false(cond)) { + continue; + } + expr* args[2] = { cond, acc }; + cond = mk_and(m(), 2, args); add_next(next, trail, mv.dst(), cond); } } @@ -856,18 +875,18 @@ br_status seq_rewriter::mk_str_to_regexp(expr* a, expr_ref& result) { return BR_FAILED; } br_status seq_rewriter::mk_re_concat(expr* a, expr* b, expr_ref& result) { - if (m_util.re.is_full(a) && m_util.re.is_full(b)) { - result = a; - return BR_DONE; - } - if (m_util.re.is_empty(a)) { - result = a; - return BR_DONE; - } - if (m_util.re.is_empty(b)) { - result = b; - return BR_DONE; - } + if (m_util.re.is_full(a) && m_util.re.is_full(b)) { + result = a; + return BR_DONE; + } + if (m_util.re.is_empty(a)) { + result = a; + return BR_DONE; + } + if (m_util.re.is_empty(b)) { + result = b; + return BR_DONE; + } if (is_epsilon(a)) { result = b; return BR_DONE; diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index f65b22b12..89cbb2566 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -27,20 +27,27 @@ Notes: #include"automaton.h" class sym_expr { - bool m_is_pred; + enum ty { + t_char, + t_pred, + t_range + }; + ty m_ty; expr_ref m_t; + expr_ref m_s; unsigned m_ref; - sym_expr(bool is_pred, expr_ref& t) : m_is_pred(is_pred), m_t(t), m_ref(0) {} + sym_expr(ty ty, expr_ref& t, expr_ref& s) : m_ty(ty), m_t(t), m_s(s), m_ref(0) {} public: expr_ref accept(expr* e); - static sym_expr* mk_char(expr_ref& t) { return alloc(sym_expr, false, t); } - static sym_expr* mk_char(ast_manager& m, expr* t) { expr_ref tr(t, m); return alloc(sym_expr, false, tr); } - static sym_expr* mk_pred(expr_ref& t) { return alloc(sym_expr, true, t); } + static sym_expr* mk_char(expr_ref& t) { return alloc(sym_expr, t_char, t, t); } + static sym_expr* mk_char(ast_manager& m, expr* t) { expr_ref tr(t, m); return mk_char(tr); } + static sym_expr* mk_pred(expr_ref& t) { return alloc(sym_expr, t_pred, t, t); } + static sym_expr* mk_range(expr_ref& lo, expr_ref& hi) { return alloc(sym_expr, t_range, lo, hi); } void inc_ref() { ++m_ref; } void dec_ref() { --m_ref; if (m_ref == 0) dealloc(this); } std::ostream& display(std::ostream& out) const; - bool is_char() const { return !m_is_pred; } - bool is_pred() const { return m_is_pred; } + bool is_char() const { return m_ty == t_char; } + bool is_pred() const { return !is_char(); } expr* get_char() const { SASSERT(is_char()); return m_t; } }; diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 4ac7e8f7e..07ddf3886 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -634,15 +634,12 @@ void theory_seq::enforce_length_coherence(enode* n1, enode* n2) { expr* o1 = n1->get_owner(); expr* o2 = n2->get_owner(); if (m_util.str.is_concat(o1) && m_util.str.is_concat(o2)) { - //std::cout << "concats:\n" << mk_pp(o1,m) << "\n" << mk_pp(o2,m) << "\n"; return; } if (has_length(o1) && !has_length(o2)) { - //std::cout << "enforce length: " << mk_pp(o1,m) << " -> " << mk_pp(o2,m) << "\n"; enforce_length(n2); } else if (has_length(o2) && !has_length(o1)) { - //std::cout << "enforce length: " << mk_pp(o2,m) << " -> " << mk_pp(o1,m) << "\n"; enforce_length(n1); } } @@ -835,7 +832,6 @@ bool theory_seq::propagate_max_length(expr* l, expr* r, dependency* deps) { } rational hi; if (is_tail(l, s, idx) && has_length(s) && m_util.str.is_empty(r) && !upper_bound(s, hi)) { - //std::cout << "max length " << mk_pp(s, m) << " " << idx << "\n"; propagate_lit(deps, 0, 0, mk_literal(m_autil.mk_le(m_util.str.mk_length(s), m_autil.mk_int(idx+1)))); return true; } @@ -1008,7 +1004,7 @@ bool theory_seq::solve_ne(unsigned idx) { } TRACE("seq", for (unsigned j = 0; j < lhs.size(); ++j) { - tout << mk_pp(lhs[j].get(), m) << " "; + tout << mk_pp(lhs[j].get(), m) << " " << mk_pp(rhs[j].get(), m) << "\n"; } tout << "\n"; tout << n.ls(i) << " != " << n.rs(i) << "\n";); @@ -1018,10 +1014,9 @@ bool theory_seq::solve_ne(unsigned idx) { expr* nr = rhs[j].get(); if (m_util.is_seq(nl) || m_util.is_re(nl)) { ls.reset(); - rs.reset(); - SASSERT(!m_util.str.is_concat(nl)); - SASSERT(!m_util.str.is_concat(nr)); - ls.push_back(nl); rs.push_back(nr); + rs.reset(); + m_util.str.get_concat(nl, ls); + m_util.str.get_concat(nr, rs); new_ls.push_back(ls); new_rs.push_back(rs); } @@ -1240,7 +1235,7 @@ void theory_seq::display_deps(std::ostream& out, dependency* dep) const { for (unsigned i = 0; i < lits.size(); ++i) { literal lit = lits[i]; get_context().display_literals_verbose(out << " ", 1, &lit); - tout << "\n"; + out << "\n"; } } From 7cbd59bf06b3b843234e9f09e200232b662ffe2f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 15 Jan 2016 03:40:33 +0530 Subject: [PATCH 02/17] enhance model validation to invoke rewriter if result isn't true using the simplify-based model evaluator Signed-off-by: Nikolaj Bjorner --- src/cmd_context/cmd_context.cpp | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 4c00b4e3a..6fe29e6d3 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -43,6 +43,7 @@ Notes: #include"model_smt2_pp.h" #include"model_v2_pp.h" #include"model_params.hpp" +#include"th_rewriter.h" func_decls::func_decls(ast_manager & m, func_decl * f): m_decls(TAG(func_decl*, f, 0)) { @@ -1624,6 +1625,11 @@ void cmd_context::validate_model() { TRACE("model_validate", tout << "checking\n" << mk_ismt2_pp(a, m()) << "\nresult:\n" << mk_ismt2_pp(r, m()) << "\n";); if (m().is_true(r)) continue; + th_rewriter thr(m()); + thr(r); + if (m().is_true(r)) + continue; + // The evaluator for array expressions is not complete // If r contains as_array/store/map/const expressions, then we do not generate the error. // TODO: improve evaluator for model expressions. From a295dd48dc010827756dfeb3daf2449fcf5dd508 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 15 Jan 2016 04:02:48 +0530 Subject: [PATCH 03/17] add seq_rewriter to model_evaluator, remove th_rewriter additional step in validator Signed-off-by: Nikolaj Bjorner --- src/cmd_context/cmd_context.cpp | 4 ---- src/model/model_evaluator.cpp | 9 ++++++++- 2 files changed, 8 insertions(+), 5 deletions(-) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 6fe29e6d3..f068d8ede 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -1623,10 +1623,6 @@ void cmd_context::validate_model() { r = 0; evaluator(a, r); TRACE("model_validate", tout << "checking\n" << mk_ismt2_pp(a, m()) << "\nresult:\n" << mk_ismt2_pp(r, m()) << "\n";); - if (m().is_true(r)) - continue; - th_rewriter thr(m()); - thr(r); if (m().is_true(r)) continue; diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index 2baedacdd..7488e6b18 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -24,6 +24,7 @@ Revision History: #include"arith_rewriter.h" #include"bv_rewriter.h" #include"pb_rewriter.h" +#include"seq_rewriter.h" #include"datatype_rewriter.h" #include"array_rewriter.h" #include"fpa_rewriter.h" @@ -39,6 +40,7 @@ struct evaluator_cfg : public default_rewriter_cfg { datatype_rewriter m_dt_rw; pb_rewriter m_pb_rw; fpa_rewriter m_f_rw; + seq_rewriter m_seq_rw; unsigned long long m_max_memory; unsigned m_max_steps; bool m_model_completion; @@ -55,7 +57,8 @@ struct evaluator_cfg : public default_rewriter_cfg { m_ar_rw(m, p), m_dt_rw(m), m_pb_rw(m), - m_f_rw(m) { + m_f_rw(m), + m_seq_rw(m) { m_b_rw.set_flat(false); m_a_rw.set_flat(false); m_bv_rw.set_flat(false); @@ -139,6 +142,8 @@ struct evaluator_cfg : public default_rewriter_cfg { st = m_dt_rw.mk_eq_core(args[0], args[1], result); else if (s_fid == m_f_rw.get_fid()) st = m_f_rw.mk_eq_core(args[0], args[1], result); + else if (s_fid == m_seq_rw.get_fid()) + st = m_seq_rw.mk_eq_core(args[0], args[1], result); if (st != BR_FAILED) return st; } @@ -157,6 +162,8 @@ struct evaluator_cfg : public default_rewriter_cfg { st = m_pb_rw.mk_app_core(f, num, args, result); else if (fid == m_f_rw.get_fid()) st = m_f_rw.mk_app_core(f, num, args, result); + else if (fid == m_seq_rw.get_fid()) + st = m_seq_rw.mk_app_core(f, num, args, result); else if (evaluate(f, num, args, result)) { TRACE("model_evaluator", tout << "reduce_app " << f->get_name() << "\n"; for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << "\n"; From 150c5c283debf90297b0b65b988696c5ea3e47cc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 15 Jan 2016 10:11:39 +0530 Subject: [PATCH 04/17] update re simplification Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 91 ++++++++++++++++++++++++++++++- src/ast/rewriter/seq_rewriter.h | 1 + src/ast/seq_decl_plugin.cpp | 3 +- src/math/automata/automaton.h | 4 ++ 4 files changed, 95 insertions(+), 4 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 1cbc2d288..879aa2144 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -222,7 +222,8 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con case OP_RE_RANGE: return BR_FAILED; case OP_RE_INTERSECT: - return BR_FAILED; + SASSERT(num_args == 2); + return mk_re_inter(args[0], args[1], result); case OP_RE_LOOP: return mk_re_loop(num_args, args, result); case OP_RE_EMPTY_SET: @@ -788,6 +789,14 @@ bool seq_rewriter::is_sequence(expr* e, expr_ref_vector& seq) { } br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) { + if (m_util.re.is_empty(b)) { + result = m().mk_false(); + return BR_DONE; + } + if (m_util.re.is_full(b)) { + result = m().mk_true(); + return BR_DONE; + } scoped_ptr aut; expr_ref_vector seq(m()); if (!(aut = m_re2aut(b))) { @@ -935,6 +944,38 @@ br_status seq_rewriter::mk_re_union(expr* a, expr* b, expr_ref& result) { } +/** + (emp n r) = emp + (r n emp) = emp + (all n r) = r + (r n all) = r + (r n r) = r + */ +br_status seq_rewriter::mk_re_inter(expr* a, expr* b, expr_ref& result) { + if (a == b) { + result = a; + return BR_DONE; + } + if (m_util.re.is_empty(a)) { + result = a; + return BR_DONE; + } + if (m_util.re.is_empty(b)) { + result = b; + return BR_DONE; + } + if (m_util.re.is_full(a)) { + result = b; + return BR_DONE; + } + if (m_util.re.is_full(b)) { + result = a; + return BR_DONE; + } + return BR_FAILED; +} + + br_status seq_rewriter::mk_re_loop(unsigned num_args, expr* const* args, expr_ref& result) { rational n1, n2; switch (num_args) { @@ -964,13 +1005,26 @@ br_status seq_rewriter::mk_re_loop(unsigned num_args, expr* const* args, expr_re (a* + b)* = (a + b)* (a + b*)* = (a + b)* (a*b*)* = (a + b)* + a+* = a* + emp* = "" + all* = all */ br_status seq_rewriter::mk_re_star(expr* a, expr_ref& result) { expr* b, *c, *b1, *c1; - if (m_util.re.is_star(a) || m_util.re.is_empty(a) || m_util.re.is_full(a)) { + if (m_util.re.is_star(a) || m_util.re.is_full(a)) { result = a; return BR_DONE; } + if (m_util.re.is_empty(a)) { + sort* seq_sort = 0; + VERIFY(m_util.is_re(a, seq_sort)); + result = m_util.re.mk_to_re(m_util.str.mk_empty(seq_sort)); + return BR_DONE; + } + if (m_util.re.is_plus(a, b)) { + result = m_util.re.mk_star(b); + return BR_DONE; + } if (m_util.re.is_union(a, b, c)) { if (m_util.re.is_star(b, b1)) { result = m_util.re.mk_star(m_util.re.mk_union(b1, c)); @@ -980,6 +1034,14 @@ br_status seq_rewriter::mk_re_star(expr* a, expr_ref& result) { result = m_util.re.mk_star(m_util.re.mk_union(b, c1)); return BR_REWRITE2; } + if (is_epsilon(b)) { + result = m_util.re.mk_star(c); + return BR_REWRITE2; + } + if (is_epsilon(c)) { + result = m_util.re.mk_star(b); + return BR_REWRITE2; + } } if (m_util.re.is_concat(a, b, c) && m_util.re.is_star(b, b1) && m_util.re.is_star(c, c1)) { @@ -991,9 +1053,34 @@ br_status seq_rewriter::mk_re_star(expr* a, expr_ref& result) { } /* + emp+ = emp + all+ = all + a*+ = a* + a++ = a+ a+ = aa* */ br_status seq_rewriter::mk_re_plus(expr* a, expr_ref& result) { + if (m_util.re.is_empty(a)) { + result = a; + return BR_DONE; + } + if (m_util.re.is_full(a)) { + result = a; + return BR_DONE; + } + if (is_epsilon(a)) { + result = a; + return BR_DONE; + } + if (m_util.re.is_plus(a)) { + result = a; + return BR_DONE; + } + if (m_util.re.is_star(a)) { + result = a; + return BR_DONE; + } + return BR_FAILED; // result = m_util.re.mk_concat(a, m_util.re.mk_star(a)); // return BR_REWRITE2; diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index 89cbb2566..ee1ba42e2 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -95,6 +95,7 @@ class seq_rewriter { br_status mk_str_to_regexp(expr* a, expr_ref& result); br_status mk_re_concat(expr* a, expr* b, expr_ref& result); br_status mk_re_union(expr* a, expr* b, expr_ref& result); + br_status mk_re_inter(expr* a, expr* b, expr_ref& result); br_status mk_re_star(expr* a, expr_ref& result); br_status mk_re_plus(expr* a, expr_ref& result); br_status mk_re_opt(expr* a, expr_ref& result); diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 5bbc26e6d..c137801ff 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -612,9 +612,8 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, func_decl_info(m_family_id, OP_STRING_CONST, num_parameters, parameters)); case OP_RE_UNION: - return mk_assoc_fun(k, arity, domain, range, k, k); - case OP_RE_CONCAT: + case OP_RE_INTERSECT: return mk_assoc_fun(k, arity, domain, range, k, k); case OP_SEQ_CONCAT: diff --git a/src/math/automata/automaton.h b/src/math/automata/automaton.h index a5acc18af..54c969bbb 100644 --- a/src/math/automata/automaton.h +++ b/src/math/automata/automaton.h @@ -105,6 +105,8 @@ public: // create an automaton from initial state, final states, and moves automaton(M& m, unsigned init, unsigned_vector const& final, moves const& mvs): m(m) { m_init = init; + m_delta.push_back(moves()); + m_delta_inv.push_back(moves()); for (unsigned i = 0; i < final.size(); ++i) { add_to_final_states(final[i]); } @@ -331,6 +333,7 @@ public: // Src - ET -> dst - e -> dst1 => Src - ET -> dst1 if out_degree(dst) = 1, // void compress() { + SASSERT(!m_delta.empty()); for (unsigned i = 0; i < m_delta.size(); ++i) { for (unsigned j = 0; j < m_delta[i].size(); ++j) { move const& mv = m_delta[i][j]; @@ -419,6 +422,7 @@ public: } } } + SASSERT(!m_delta.empty()); while (true) { SASSERT(!m_delta.empty()); unsigned src = m_delta.size() - 1; From 14c19fe9283968d295ba2106a32584de6be52ba7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 15 Jan 2016 10:39:21 +0530 Subject: [PATCH 05/17] add parameter validation to sequence expressions Signed-off-by: Nikolaj Bjorner --- src/api/python/z3.py | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 0626d2f3c..323e57c79 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -9095,6 +9095,10 @@ def _coerce_seq(s, ctx=None): if isinstance(s, str): ctx = _get_ctx(ctx) s = StringVal(s, ctx) + if not is_expr(s): + raise Z3Exception("Non-expression passed as a sequence") + if not is_seq(s): + raise Z3Exception("Non-sequence passed as a sequence") return s def _get_ctx2(a, b, ctx=None): From 88362a1c3adbc98832e6560bf3cfb49fec50fa0d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 15 Jan 2016 16:32:43 +0530 Subject: [PATCH 06/17] fix bugs in sequence extraction from NFA Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 879aa2144..fce29426c 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -731,8 +731,14 @@ bool seq_rewriter::is_sequence(eautomaton& aut, expr_ref_vector& seq) { unsigned state = aut.init(); uint_set visited; eautomaton::moves mvs; - aut.get_moves_from(state, mvs, true); - while (!aut.is_final_state(state)) { + unsigned_vector states; + aut.get_epsilon_closure(state, states); + bool has_final = false; + for (unsigned i = 0; !has_final && i < states.size(); ++i) { + has_final = aut.is_final_state(states[i]); + } + aut.get_moves_from(state, mvs, true); + while (!has_final) { if (mvs.size() != 1) { return false; } @@ -751,6 +757,12 @@ bool seq_rewriter::is_sequence(eautomaton& aut, expr_ref_vector& seq) { state = mvs[0].dst(); mvs.reset(); aut.get_moves_from(state, mvs, true); + states.reset(); + has_final = false; + aut.get_epsilon_closure(state, states); + for (unsigned i = 0; !has_final && i < states.size(); ++i) { + has_final = aut.is_final_state(states[i]); + } } return mvs.empty(); } From 01cb20e098818b520b23fe3e70f95d52f81d4afb Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 16 Jan 2016 13:53:29 +0000 Subject: [PATCH 07/17] Fix for escape sequences in SMT2 scanner --- src/parsers/smt2/smt2scanner.cpp | 36 +++++++++++++++++++------------- 1 file changed, 22 insertions(+), 14 deletions(-) diff --git a/src/parsers/smt2/smt2scanner.cpp b/src/parsers/smt2/smt2scanner.cpp index 3664ed903..8a0dc1639 100644 --- a/src/parsers/smt2/smt2scanner.cpp +++ b/src/parsers/smt2/smt2scanner.cpp @@ -46,7 +46,7 @@ namespace smt2 { } m_spos++; } - + void scanner::read_comment() { SASSERT(curr() == ';'); next(); @@ -62,7 +62,7 @@ namespace smt2 { next(); } } - + scanner::token scanner::read_quoted_symbol() { SASSERT(curr() == '|'); bool escape = false; @@ -105,7 +105,7 @@ namespace smt2 { } } } - + scanner::token scanner::read_symbol() { SASSERT(m_normalized[static_cast(curr())] == 'a' || curr() == ':' || curr() == '-'); m_string.reset(); @@ -113,14 +113,14 @@ namespace smt2 { next(); return read_symbol_core(); } - + scanner::token scanner::read_number() { SASSERT('0' <= curr() && curr() <= '9'); rational q(1); m_number = rational(curr() - '0'); next(); bool is_float = false; - + while (true) { char c = curr(); if ('0' <= c && c <= '9') { @@ -139,7 +139,7 @@ namespace smt2 { break; } } - if (is_float) + if (is_float) m_number /= q; TRACE("scanner", tout << "new number: " << m_number << "\n";); return is_float ? FLOAT_TOKEN : INT_TOKEN; @@ -160,14 +160,14 @@ namespace smt2 { return read_symbol_core(); } } - + scanner::token scanner::read_string() { SASSERT(curr() == '\"'); next(); m_string.reset(); while (true) { char c = curr(); - if (c == EOF) + if (c == EOF) throw scanner_exception("unexpected end of string", m_line, m_spos); if (c == '\n') { new_line(); @@ -179,11 +179,19 @@ namespace smt2 { return STRING_TOKEN; } } + else if (c == '\\') { + next(); + c = curr(); + if (c == EOF) + throw scanner_exception("unexpected end of string", m_line, m_spos); + if (c != '\\' && c != '\"') + throw scanner_exception("invalid escape sequence", m_line, m_spos); + } m_string.push_back(c); next(); } } - + scanner::token scanner::read_bv_literal() { SASSERT(curr() == '#'); next(); @@ -200,7 +208,7 @@ namespace smt2 { } else if ('a' <= c && c <= 'f') { m_number *= rational(16); - m_number += rational(10 + (c - 'a')); + m_number += rational(10 + (c - 'a')); } else if ('A' <= c && c <= 'F') { m_number *= rational(16); @@ -236,9 +244,9 @@ namespace smt2 { throw scanner_exception("invalid bit-vector literal, expecting 'x' or 'b'", m_line, m_spos); } } - + scanner::scanner(cmd_context & ctx, std::istream& stream, bool interactive): - m_interactive(interactive), + m_interactive(interactive), m_spos(0), m_curr(0), // avoid Valgrind warning m_line(1), @@ -248,7 +256,7 @@ namespace smt2 { m_bend(0), m_stream(stream), m_cache_input(false) { - + m_smtlib2_compliant = ctx.params().m_smtlib2_compliant; for (int i = 0; i < 256; ++i) { @@ -287,7 +295,7 @@ namespace smt2 { m_normalized[static_cast('/')] = 'a'; next(); } - + scanner::token scanner::scan() { while (true) { signed char c = curr(); From 99d2ab4e8e51e39791922d6a8c750879d0657c88 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sun, 17 Jan 2016 14:24:02 +0000 Subject: [PATCH 08/17] Undid previous update of SMT2 scanner to support the new SMT2.5 string escaping. --- src/parsers/smt2/smt2scanner.cpp | 8 -------- 1 file changed, 8 deletions(-) diff --git a/src/parsers/smt2/smt2scanner.cpp b/src/parsers/smt2/smt2scanner.cpp index 8a0dc1639..156cc2e5d 100644 --- a/src/parsers/smt2/smt2scanner.cpp +++ b/src/parsers/smt2/smt2scanner.cpp @@ -179,14 +179,6 @@ namespace smt2 { return STRING_TOKEN; } } - else if (c == '\\') { - next(); - c = curr(); - if (c == EOF) - throw scanner_exception("unexpected end of string", m_line, m_spos); - if (c != '\\' && c != '\"') - throw scanner_exception("invalid escape sequence", m_line, m_spos); - } m_string.push_back(c); next(); } From 85d44c5d660034a2b43da22d8f8c061fc391d3e7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 18 Jan 2016 11:09:41 +0530 Subject: [PATCH 09/17] fix axioms for extract, add extensionality checking for shared variables, convert exceptions to unknown status per #419 Signed-off-by: Nikolaj Bjorner --- src/cmd_context/cmd_context.cpp | 4 ++- src/opt/opt_context.cpp | 5 +-- src/opt/opt_context.h | 2 ++ src/opt/opt_solver.cpp | 4 +++ src/opt/opt_solver.h | 1 + src/sat/sat_solver/inc_sat_solver.cpp | 11 ++++-- src/smt/smt_context.cpp | 5 ++- src/smt/smt_context.h | 2 ++ src/smt/smt_context_pp.cpp | 4 +-- src/smt/smt_kernel.cpp | 8 +++++ src/smt/smt_kernel.h | 6 ++++ src/smt/smt_solver.cpp | 4 +++ src/smt/theory_seq.cpp | 51 +++++++++++++++++++++++++-- src/smt/theory_seq.h | 2 ++ src/solver/check_sat_result.h | 2 ++ src/solver/combined_solver.cpp | 5 +++ src/solver/tactic2solver.cpp | 7 ++++ 17 files changed, 110 insertions(+), 13 deletions(-) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index f068d8ede..bc39577db 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -44,6 +44,7 @@ Notes: #include"model_v2_pp.h" #include"model_params.hpp" #include"th_rewriter.h" +#include"tactic_exception.h" func_decls::func_decls(ast_manager & m, func_decl * f): m_decls(TAG(func_decl*, f, 0)) { @@ -1463,7 +1464,8 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions throw ex; } catch (z3_exception & ex) { - throw cmd_exception(ex.msg()); + m_solver->set_reason_unknown(ex.msg()); + r = l_undef; } m_solver->set_status(r); } diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 5d95af0a4..97b8c999d 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -132,7 +132,8 @@ namespace opt { m_objective_refs(m), m_enable_sat(false), m_is_clausal(false), - m_pp_neat(false) + m_pp_neat(false), + m_unknown("unknown") { params_ref p; p.set_bool("model", true); @@ -487,7 +488,7 @@ namespace opt { if (m_solver.get()) { return m_solver->reason_unknown(); } - return std::string("unknown"); + return m_unknown; } void context::display_bounds(std::ostream& out, bounds_t const& b) const { diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index a919d1575..24051f7cb 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -163,6 +163,7 @@ namespace opt { symbol m_maxsat_engine; symbol m_logic; svector m_labels; + std::string m_unknown; public: context(ast_manager& m); virtual ~context(); @@ -184,6 +185,7 @@ namespace opt { virtual void get_labels(svector & r); virtual void get_unsat_core(ptr_vector & r) {} virtual std::string reason_unknown() const; + virtual void set_reason_unknown(char const* msg) { m_unknown = msg; } virtual void display_assignment(std::ostream& out); virtual bool is_pareto() { return m_pareto.get() != 0; } diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index 78b52a9ea..097cf5f3e 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -290,6 +290,10 @@ namespace opt { std::string opt_solver::reason_unknown() const { return m_context.last_failure_as_string(); } + + void opt_solver::set_reason_unknown(char const* msg) { + m_context.set_reason_unknown(msg); + } void opt_solver::get_labels(svector & r) { r.reset(); diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h index 7337b86ed..128836089 100644 --- a/src/opt/opt_solver.h +++ b/src/opt/opt_solver.h @@ -99,6 +99,7 @@ namespace opt { virtual void get_model(model_ref & _m); virtual proof * get_proof(); virtual std::string reason_unknown() const; + virtual void set_reason_unknown(char const* msg); virtual void get_labels(svector & r); virtual void set_progress_callback(progress_callback * callback); virtual unsigned get_num_assertions() const; diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 4f002f20b..33889e4ef 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -60,6 +60,8 @@ class inc_sat_solver : public solver { model_converter_ref m_mc2; expr_dependency_ref m_dep_core; svector m_weights; + std::string m_unknown; + typedef obj_map dep2asm_t; public: @@ -73,7 +75,8 @@ public: m_map(m), m_bb_rewriter(m, p), m_num_scopes(0), - m_dep_core(m) { + m_dep_core(m), + m_unknown("no reason given") { m_params.set_bool("elim_vars", false); m_solver.updt_params(m_params); params_ref simp2_p = p; @@ -243,8 +246,12 @@ public: UNREACHABLE(); return 0; } + virtual std::string reason_unknown() const { - return "no reason given"; + return m_unknown; + } + virtual void set_reason_unknown(char const* msg) { + m_unknown = msg; } virtual void get_labels(svector & r) { } diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index f12708150..1a8658c99 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -72,6 +72,7 @@ namespace smt { m_not_l(null_literal), m_conflict_resolution(mk_conflict_resolution(m, *this, m_dyn_ack_manager, p, m_assigned_literals, m_watches)), m_unsat_proof(m), + m_unknown("unknown"), m_unsat_core(m), #ifdef Z3DEBUG m_trail_enabled(true), @@ -4110,8 +4111,7 @@ namespace smt { m_fingerprints.display(tout); ); failure fl = get_last_search_failure(); - if (fl == TIMEOUT || fl == MEMOUT || fl == CANCELED || fl == NUM_CONFLICTS) { - // don't generate model. + if (fl == MEMOUT || fl == CANCELED || fl == TIMEOUT || fl == NUM_CONFLICTS) { return; } @@ -4126,7 +4126,6 @@ namespace smt { if (m_fparams.m_model_compact) m_proto_model->compress(); TRACE("mbqi_bug", tout << "after cleanup:\n"; model_pp(tout, *m_proto_model);); - //SASSERT(validate_model()); } } diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 38463abe2..85fd63033 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -71,6 +71,7 @@ namespace smt { std::ostream& display_last_failure(std::ostream& out) const; std::string last_failure_as_string() const; + void set_reason_unknown(char const* msg) { m_unknown = msg; } void set_progress_callback(progress_callback *callback); @@ -197,6 +198,7 @@ namespace smt { // ----------------------------------- proto_model_ref m_proto_model; model_ref m_model; + std::string m_unknown; void mk_proto_model(lbool r); struct scoped_mk_model; diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp index 695c71eea..b06b2f463 100644 --- a/src/smt/smt_context_pp.cpp +++ b/src/smt/smt_context_pp.cpp @@ -62,7 +62,7 @@ namespace smt { std::string context::last_failure_as_string() const { std::string r; switch(m_last_search_failure) { - case OK: r = "ok"; break; + case OK: r = m_unknown; break; case TIMEOUT: r = "timeout"; break; case MEMOUT: r = "memout"; break; case CANCELED: r = "canceled"; break; @@ -79,7 +79,7 @@ namespace smt { break; } case QUANTIFIERS: r = "(incomplete quantifiers)"; break; - case UNKNOWN: r = "incomplete"; break; + case UNKNOWN: r = m_unknown; break; } return r; } diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp index f390b2f33..418dfdb04 100644 --- a/src/smt/smt_kernel.cpp +++ b/src/smt/smt_kernel.cpp @@ -123,6 +123,10 @@ namespace smt { return m_kernel.last_failure_as_string(); } + void set_reason_unknown(char const* msg) { + m_kernel.set_reason_unknown(msg); + } + void get_assignments(expr_ref_vector & result) { m_kernel.get_assignments(result); } @@ -284,6 +288,10 @@ namespace smt { return m_imp->last_failure_as_string(); } + void kernel::set_reason_unknown(char const* msg) { + m_imp->set_reason_unknown(msg); + } + void kernel::get_assignments(expr_ref_vector & result) { m_imp->get_assignments(result); } diff --git a/src/smt/smt_kernel.h b/src/smt/smt_kernel.h index ce429151b..be06e5ea5 100644 --- a/src/smt/smt_kernel.h +++ b/src/smt/smt_kernel.h @@ -155,6 +155,12 @@ namespace smt { */ std::string last_failure_as_string() const; + + /** + \brief Set the reason for unknown. + */ + void set_reason_unknown(char const* msg); + /** \brief Return the set of formulas assigned by the kernel. */ diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 3d84483e5..1778ce076 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -95,6 +95,10 @@ namespace smt { return m_context.last_failure_as_string(); } + virtual void set_reason_unknown(char const* msg) { + m_context.set_reason_unknown(msg); + } + virtual void get_labels(svector & r) { buffer tmp; m_context.get_relevant_labels(0, tmp); diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 57a3be5d9..3c3d82402 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -221,6 +221,11 @@ final_check_status theory_seq::final_check_eh() { TRACE("seq", tout << ">>propagate_automata\n";); return FC_CONTINUE; } + if (!check_extensionality()) { + ++m_stats.m_extensionality; + TRACE("seq", tout << ">>extensionality\n";); + return FC_CONTINUE; + } if (is_solved()) { TRACE("seq", tout << ">>is_solved\n";); return FC_DONE; @@ -541,6 +546,45 @@ void theory_seq::mk_decompose(expr* e, expr_ref& head, expr_ref& tail) { } } +/* + \brief Check extensionality (for sequences). + */ +bool theory_seq::check_extensionality() { + context& ctx = get_context(); + unsigned sz = get_num_vars(); + unsigned_vector seqs; + bool added_assumption = false; + for (unsigned v = 0; v < sz; ++v) { + enode* n = get_enode(v); + expr* o1 = n->get_owner(); + if (n != n->get_root()) { + continue; + } + if (!seqs.empty() && ctx.is_relevant(n) && m_util.is_seq(o1) && ctx.is_shared(n)) { + dependency* dep = 0; + expr_ref e1 = canonize(o1, dep); + for (unsigned i = 0; i < seqs.size(); ++i) { + enode* n2 = get_enode(seqs[i]); + expr* o2 = n2->get_owner(); + if (m_exclude.contains(o1, o2)) { + continue; + } + expr_ref e2 = canonize(n2->get_owner(), dep); + m_lhs.reset(); m_rhs.reset(); + bool change = false; + if (!m_seq_rewrite.reduce_eq(o1, o2, m_lhs, m_rhs, change)) { + m_exclude.update(o1, o2); + continue; + } + TRACE("seq", tout << mk_pp(o1, m) << " = " << mk_pp(o2, m) << "\n";); + ctx.assume_eq(n, n2); + return false; + } + } + seqs.push_back(v); + } + return true; +} /* - Eqs = 0 @@ -1248,6 +1292,7 @@ void theory_seq::collect_statistics(::statistics & st) const { st.update("seq solve !=", m_stats.m_solve_nqs); st.update("seq solve =", m_stats.m_solve_eqs); st.update("seq add axiom", m_stats.m_add_axiom); + st.update("seq extensionality", m_stats.m_extensionality); } void theory_seq::init_model(expr_ref_vector const& es) { @@ -1917,18 +1962,18 @@ void theory_seq::add_extract_axiom(expr* e) { expr_ref ls(m_util.str.mk_length(s), m); expr_ref lx(m_util.str.mk_length(x), m); expr_ref le(m_util.str.mk_length(e), m); - expr_ref ls_minus_i(mk_sub(ls, i), m); + expr_ref ls_minus_i_l(mk_sub(mk_sub(ls, i),l), m); expr_ref xe = mk_concat(x, e); expr_ref zero(m_autil.mk_int(0), m); literal i_ge_0 = mk_literal(m_autil.mk_ge(i, zero)); literal i_ge_ls = mk_literal(m_autil.mk_ge(mk_sub(i, ls), zero)); - literal l_ge_ls = mk_literal(m_autil.mk_ge(mk_sub(l, 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)); add_axiom(~i_ge_0, i_ge_ls, mk_literal(m_util.str.mk_prefix(xe, s))); add_axiom(~i_ge_0, i_ge_ls, mk_eq(lx, i, false)); - add_axiom(~i_ge_0, i_ge_ls, ~l_ge_ls, mk_eq(le, ls_minus_i, false)); + add_axiom(~i_ge_0, i_ge_ls, ~li_ge_ls, mk_eq(le, l, false)); add_axiom(~i_ge_0, i_ge_ls, l_ge_zero, mk_eq(le, zero, false)); } diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 8e0b8e17e..fd1219d4b 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -239,6 +239,7 @@ namespace smt { unsigned m_solve_nqs; unsigned m_solve_eqs; unsigned m_add_axiom; + unsigned m_extensionality; }; ast_manager& m; dependency_manager m_dm; @@ -312,6 +313,7 @@ namespace smt { bool check_length_coherence(expr* e); bool propagate_length_coherence(expr* e); + bool check_extensionality(); bool solve_eqs(unsigned start); bool solve_eq(expr_ref_vector const& l, expr_ref_vector const& r, dependency* dep); bool simplify_eq(expr_ref_vector& l, expr_ref_vector& r, dependency* dep); diff --git a/src/solver/check_sat_result.h b/src/solver/check_sat_result.h index 73a24fc7b..e6586d492 100644 --- a/src/solver/check_sat_result.h +++ b/src/solver/check_sat_result.h @@ -51,6 +51,7 @@ public: virtual void get_model(model_ref & m) = 0; virtual proof * get_proof() = 0; virtual std::string reason_unknown() const = 0; + virtual void set_reason_unknown(char const* msg) = 0; virtual void get_labels(svector & r) = 0; virtual ast_manager& get_manager() = 0; }; @@ -75,6 +76,7 @@ struct simple_check_sat_result : public check_sat_result { virtual proof * get_proof(); virtual std::string reason_unknown() const; virtual void get_labels(svector & r); + virtual void set_reason_unknown(char const* msg) { m_unknown = msg; } }; #endif diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp index c1f21226b..08463cf20 100644 --- a/src/solver/combined_solver.cpp +++ b/src/solver/combined_solver.cpp @@ -297,6 +297,11 @@ public: return m_solver2->reason_unknown(); } + virtual void set_reason_unknown(char const* msg) { + m_solver1->set_reason_unknown(msg); + m_solver2->set_reason_unknown(msg); + } + virtual void get_labels(svector & r) { if (m_use_solver1_results) return m_solver1->get_labels(r); diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp index f66132f00..f661ca184 100644 --- a/src/solver/tactic2solver.cpp +++ b/src/solver/tactic2solver.cpp @@ -65,6 +65,7 @@ public: virtual void get_model(model_ref & m); virtual proof * get_proof(); virtual std::string reason_unknown() const; + virtual void set_reason_unknown(char const* msg); virtual void get_labels(svector & r) {} virtual void set_progress_callback(progress_callback * callback) {} @@ -225,6 +226,12 @@ std::string tactic2solver::reason_unknown() const { return std::string("unknown"); } +void tactic2solver::set_reason_unknown(char const* msg) { + if (m_result.get()) { + m_result->set_reason_unknown(msg); + } +} + unsigned tactic2solver::get_num_assertions() const { return m_assertions.size(); } From c9373ebc9fd06653227ff09ebcc7a1f2e557a21a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 18 Jan 2016 12:01:15 +0530 Subject: [PATCH 10/17] fix axiomatization for at Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context_pp.cpp | 2 +- src/smt/theory_seq.cpp | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp index b06b2f463..d04165c5b 100644 --- a/src/smt/smt_context_pp.cpp +++ b/src/smt/smt_context_pp.cpp @@ -238,7 +238,7 @@ namespace smt { out << "equivalence classes:\n"; first = false; } - out << "#" << n->get_id() << " -> #" << r->get_id() << "\n"; + out << "#" << n->get_id() << " -> #" << r->get_id() << ": "; out << mk_pp(n, m_manager) << " -> " << mk_pp(r, m_manager) << "\n"; } } diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 3c3d82402..61c09b020 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -1987,8 +1987,8 @@ void theory_seq::add_at_axiom(expr* e) { expr* s, *i; VERIFY(m_util.str.is_at(e, s, i)); expr_ref x(m), y(m), lx(m), le(m), xey(m), zero(m), one(m), len_e(m), len_x(m); - x = mk_skolem(m_at_left, s); - y = mk_skolem(m_at_right, s); + x = mk_skolem(m_at_left, s, i); + y = mk_skolem(m_at_right, s, i); xey = mk_concat(x, e, y); zero = m_autil.mk_int(0); one = m_autil.mk_int(1); From 99176cca60efb8d7f4ce1bfc48e1e990a6276ad5 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 18 Jan 2016 18:00:04 +0000 Subject: [PATCH 11/17] Bugfix for FP model converter. --- src/tactic/fpa/fpa2bv_model_converter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/tactic/fpa/fpa2bv_model_converter.cpp b/src/tactic/fpa/fpa2bv_model_converter.cpp index 799083a5f..a41b92b2d 100644 --- a/src/tactic/fpa/fpa2bv_model_converter.cpp +++ b/src/tactic/fpa/fpa2bv_model_converter.cpp @@ -384,7 +384,7 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) { if (!seen.contains(f)) { TRACE("fpa2bv_mc", tout << "Keeping: " << mk_ismt2_pp(f, m) << std::endl;); - func_interp * val = bv_mdl->get_func_interp(f); + func_interp * val = bv_mdl->get_func_interp(f)->copy(); float_mdl->register_decl(f, val); } } From 4dba5270ad42e632592b484cbae9a17901a81fc1 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 18 Jan 2016 18:09:29 +0000 Subject: [PATCH 12/17] Efficiency fix for fp.div. --- src/ast/fpa/fpa2bv_converter.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 863d1d8db..1d66b793d 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -923,7 +923,8 @@ void fpa2bv_converter::mk_div(func_decl * f, unsigned num, expr * const * args, m_bv_util.mk_bv_sub(b_exp_ext, b_lz_ext)); expr_ref quotient(m); - quotient = m.mk_app(m_bv_util.get_fid(), OP_BUDIV, a_sig_ext, b_sig_ext); + // b_sig_ext can't be 0 here, so it's safe to use OP_BUDIV_I + quotient = m.mk_app(m_bv_util.get_fid(), OP_BUDIV_I, a_sig_ext, b_sig_ext); dbg_decouple("fpa2bv_div_quotient", quotient); From cccd502a4d6d8d686a4c991605385e5de23121f9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 19 Jan 2016 13:57:47 +0100 Subject: [PATCH 13/17] bug-fixes to sequence theory Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 5 +- src/ast/seq_decl_plugin.h | 1 + src/smt/theory_seq.cpp | 117 ++++++++++++++++++++---------- src/smt/theory_seq.h | 5 +- 4 files changed, 87 insertions(+), 41 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index fce29426c..cbccfeb5e 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -374,7 +374,7 @@ br_status seq_rewriter::mk_seq_length(expr* a, expr_ref& result) { es.push_back(m_autil.mk_numeral(rational(len, rational::ui64()), true)); } result = m_autil.mk_add(es.size(), es.c_ptr()); - return BR_DONE; + return BR_REWRITE2; } return BR_FAILED; } @@ -1170,14 +1170,13 @@ bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_ rs.pop_back(); } else { - expr_ref s2(m_util.str.mk_string(s.extract(0, s.length()-2)), m()); + expr_ref s2(m_util.str.mk_string(s.extract(0, s.length()-1)), m()); rs[rs.size()-1] = s2; } } else { break; } - TRACE("seq", tout << "change back\n";); change = true; lchange = true; } diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 611020a69..29ec98b07 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -268,6 +268,7 @@ public: MATCH_TERNARY(is_extract); MATCH_BINARY(is_contains); MATCH_BINARY(is_at); + MATCH_BINARY(is_index); MATCH_TERNARY(is_index); MATCH_TERNARY(is_replace); MATCH_BINARY(is_prefix); diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 61c09b020..cc84388d3 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -244,9 +244,9 @@ bool theory_seq::branch_variable() { unsigned k = (i + start) % sz; eq const& e = m_eqs[k]; unsigned id = e.id(); - TRACE("seq", tout << e.ls() << " = " << e.rs() << "\n";); s = find_branch_start(2*id); + TRACE("seq", tout << s << " " << 2*id << ": " << e.ls() << " = " << e.rs() << "\n";); bool found = find_branch_candidate(s, e.dep(), e.ls(), e.rs()); insert_branch_start(2*id, s); if (found) { @@ -297,11 +297,14 @@ bool theory_seq::find_branch_candidate(unsigned& start, dependency* dep, expr_re expr_ref v0(m); v0 = m_util.str.mk_empty(m.get_sort(l)); - if (can_be_equal(ls.size() - 1, ls.c_ptr() + 1, rs.size(), rs.c_ptr()) && l_false != assume_equality(l, v0)) { - TRACE("seq", tout << mk_pp(l, m) << " " << v0 << "\n";); - return true; + literal_vector lits; + if (can_be_equal(ls.size() - 1, ls.c_ptr() + 1, rs.size(), rs.c_ptr())) { + if (l_false != assume_equality(l, v0)) { + TRACE("seq", tout << mk_pp(l, m) << " " << v0 << "\n";); + return true; + } + lits.push_back(~mk_eq_empty(l)); } -// start = 0; for (; start < rs.size(); ++start) { unsigned j = start; SASSERT(!m_util.str.is_concat(rs[j])); @@ -325,11 +328,11 @@ bool theory_seq::find_branch_candidate(unsigned& start, dependency* dep, expr_re all_units &= m_util.str.is_unit(rs[j]); } if (all_units) { - literal_vector lits; - lits.push_back(~mk_eq_empty(l)); for (unsigned i = 0; i < rs.size(); ++i) { - v0 = mk_concat(i + 1, rs.c_ptr()); - lits.push_back(~mk_eq(l, v0, false)); + if (can_be_equal(ls.size() - 1, ls.c_ptr() + 1, rs.size() - i - 1, rs.c_ptr() + i + 1)) { + v0 = mk_concat(i + 1, rs.c_ptr()); + lits.push_back(~mk_eq(l, v0, false)); + } } set_conflict(dep, lits); TRACE("seq", tout << mk_pp(l, m) << " " << v0 << "\n";); @@ -506,11 +509,23 @@ expr_ref theory_seq::mk_nth(expr* s, expr* idx) { } expr_ref theory_seq::mk_last(expr* s) { + zstring str; + if (m_util.str.is_string(s, str) && str.length() > 0) { + return expr_ref(m_util.str.mk_char(str, str.length()-1), m); + } sort* char_sort = 0; VERIFY(m_util.is_seq(m.get_sort(s), char_sort)); return mk_skolem(m_seq_last, s, 0, 0, char_sort); } +expr_ref theory_seq::mk_first(expr* s) { + zstring str; + if (m_util.str.is_string(s, str) && str.length() > 0) { + return expr_ref(m_util.str.mk_string(str.extract(0, str.length()-1)), m); + } + return mk_skolem(m_seq_first, s); +} + void theory_seq::mk_decompose(expr* e, expr_ref& head, expr_ref& tail) { expr* e1, *e2; @@ -819,7 +834,6 @@ bool theory_seq::solve_eqs(unsigned i) { bool change = false; for (; !ctx.inconsistent() && i < m_eqs.size(); ++i) { eq const& e = m_eqs[i]; - TRACE("seq", tout << i << "\n";); if (solve_eq(e.ls(), e.rs(), e.dep())) { if (i + 1 != m_eqs.size()) { eq e1 = m_eqs[m_eqs.size()-1]; @@ -1579,8 +1593,9 @@ void theory_seq::propagate() { ++m_axioms_head; } while (!m_replay.empty() && !ctx.inconsistent()) { - (*m_replay[m_replay.size()-1])(*this); TRACE("seq", tout << "replay at level: " << ctx.get_scope_level() << "\n";); + apply* app = m_replay[m_replay.size() - 1]; + (*app)(*this); m_replay.pop_back(); } if (m_new_solution) { @@ -1632,7 +1647,7 @@ void theory_seq::deque_axiom(expr* n) { lit or s = "" or !prefix(s, x*s1) */ void theory_seq::tightest_prefix(expr* s, expr* x, literal lit1, literal lit2) { - expr_ref s1 = mk_skolem(m_seq_first, s); + expr_ref s1 = mk_first(s); expr_ref c = mk_last(s); expr_ref s1c = mk_concat(s1, m_util.str.mk_unit(c)); literal s_eq_emp = mk_eq_empty(s); @@ -1668,30 +1683,34 @@ void theory_seq::tightest_prefix(expr* s, expr* x, literal lit1, literal lit2) { (len(s) <= len(t) -> i <= len(t)-len(s)) */ void theory_seq::add_indexof_axiom(expr* i) { - expr* s, *t, *offset; + expr* s, *t, *offset = 0; rational r; - VERIFY(m_util.str.is_index(i, t, s, offset)); + VERIFY(m_util.str.is_index(i, t, s) || + m_util.str.is_index(i, t, s, offset)); expr_ref minus_one(m_autil.mk_int(-1), m); expr_ref zero(m_autil.mk_int(0), m); expr_ref xsy(m); - // offset >= len(t) => indexof(s, t, offset) = -1 - expr_ref len_t(m_util.str.mk_length(t), m); - literal offset_ge_len = mk_literal(m_autil.mk_ge(mk_sub(offset, len_t), zero)); - add_axiom(offset_ge_len, mk_eq(i, minus_one, false)); - if (m_autil.is_numeral(offset, r) && r.is_zero()) { + if (!offset || (m_autil.is_numeral(offset, r) && r.is_zero())) { expr_ref x = mk_skolem(m_contains_left, t, s); expr_ref y = mk_skolem(m_contains_right, t, s); - xsy = mk_concat(x,s,y); + xsy = mk_concat(x, s, y); literal cnt = mk_literal(m_util.str.mk_contains(t, s)); literal eq_empty = mk_eq_empty(s); add_axiom(cnt, mk_eq(i, minus_one, false)); add_axiom(~eq_empty, mk_eq(i, zero, false)); + add_axiom(eq_empty, ~mk_eq_empty(t), mk_eq(i, minus_one, false)); add_axiom(~cnt, eq_empty, mk_eq(t, xsy, false)); tightest_prefix(s, x, ~cnt); } else { + // offset >= len(t) => indexof(s, t, offset) = -1 + + expr_ref len_t(m_util.str.mk_length(t), m); + literal offset_ge_len = mk_literal(m_autil.mk_ge(mk_sub(offset, len_t), zero)); + add_axiom(offset_ge_len, mk_eq(i, minus_one, false)); + expr_ref x = mk_skolem(m_indexof_left, t, s, offset); expr_ref y = mk_skolem(m_indexof_right, t, s, offset); expr_ref indexof0(m_util.str.mk_index(y, s, zero), m); @@ -2067,6 +2086,15 @@ literal theory_seq::mk_eq_empty(expr* _e) { expr_ref e(_e, m); SASSERT(m_util.is_seq(e)); expr_ref emp(m); + zstring s; + if (m_util.str.is_string(e, s)) { + if (s.length() == 0) { + return true_literal; + } + else { + return false_literal; + } + } emp = m_util.str.mk_empty(m.get_sort(e)); return mk_equals(e, emp); } @@ -2074,10 +2102,11 @@ literal theory_seq::mk_eq_empty(expr* _e) { void theory_seq::add_axiom(literal l1, literal l2, literal l3, literal l4) { context& ctx = get_context(); literal_vector lits; - if (l1 != null_literal) { ctx.mark_as_relevant(l1); lits.push_back(l1); } - if (l2 != null_literal) { ctx.mark_as_relevant(l2); lits.push_back(l2); } - if (l3 != null_literal) { ctx.mark_as_relevant(l3); lits.push_back(l3); } - if (l4 != null_literal) { ctx.mark_as_relevant(l4); lits.push_back(l4); } + if (l1 == true_literal || l2 == true_literal || l3 == true_literal || l4 == true_literal) return; + if (l1 != null_literal && l1 != false_literal) { ctx.mark_as_relevant(l1); lits.push_back(l1); } + if (l2 != null_literal && l2 != false_literal) { ctx.mark_as_relevant(l2); lits.push_back(l2); } + if (l3 != null_literal && l3 != false_literal) { ctx.mark_as_relevant(l3); lits.push_back(l3); } + if (l4 != null_literal && l4 != false_literal) { ctx.mark_as_relevant(l4); lits.push_back(l4); } TRACE("seq", ctx.display_literals_verbose(tout << "axiom: ", lits.size(), lits.c_ptr()); tout << "\n";); m_new_propagation = true; ++m_stats.m_add_axiom; @@ -2117,8 +2146,8 @@ void theory_seq::propagate_eq(literal lit, expr* e1, expr* e2, bool add_to_eqs) } TRACE("seq", - tout << mk_pp(ctx.bool_var2expr(lit.var()), m) << " => " - << mk_pp(e1, m) << " = " << mk_pp(e2, m) << "\n";); + ctx.display_literals_verbose(tout, 1, &lit); + tout << " => " << mk_pp(e1, m) << " = " << mk_pp(e2, m) << "\n";); justification* js = ctx.mk_justification( ext_theory_eq_propagation_justification( @@ -2161,7 +2190,7 @@ void theory_seq::assign_eh(bool_var v, bool is_true) { propagate_non_empty(lit, e1); // lit => e1 = first ++ (unit last) - expr_ref f1 = mk_skolem(m_seq_first, e1); + expr_ref f1 = mk_first(e1); expr_ref f2 = mk_last(e1); f = mk_concat(f1, m_util.str.mk_unit(f2)); propagate_eq(lit, e1, f, true); @@ -2271,6 +2300,7 @@ void theory_seq::push_scope_eh() { } void theory_seq::pop_scope_eh(unsigned num_scopes) { + context& ctx = get_context(); m_trail_stack.pop_scope(num_scopes); theory::pop_scope_eh(num_scopes); m_dm.pop_scope(num_scopes); @@ -2280,6 +2310,10 @@ void theory_seq::pop_scope_eh(unsigned num_scopes) { m_nqs.pop_scope(num_scopes); m_atoms.resize(m_atoms_lim[m_atoms_lim.size()-num_scopes]); m_atoms_lim.shrink(m_atoms_lim.size()-num_scopes); + m_rewrite.reset(); + if (ctx.get_base_level() > ctx.get_scope_level() - num_scopes) { + m_replay.reset(); + } } void theory_seq::restart_eh() { @@ -2606,7 +2640,8 @@ bool theory_seq::add_prefix2prefix(expr* e) { return false; } expr_ref emp(m_util.str.mk_empty(m.get_sort(e1)), m); - switch (assume_equality(e2, emp)) { + literal e2_is_emp = mk_eq_empty(e2); + switch (ctx.get_assignment(e2_is_emp)) { case l_true: return false; // done case l_undef: @@ -2614,16 +2649,19 @@ bool theory_seq::add_prefix2prefix(expr* e) { default: break; } - expr_ref head1(m), tail1(m), head2(m), tail2(m); + + expr_ref head1(m), tail1(m), head2(m), tail2(m), conc(m); mk_decompose(e1, head1, tail1); mk_decompose(e2, head2, tail2); + conc = mk_concat(head2, tail2); + propagate_eq(~e2_is_emp, e2, conc, true); literal lit = mk_eq(head1, head2, false); switch (ctx.get_assignment(lit)) { case l_true: { literal_vector lits; lits.push_back(~ctx.get_literal(e)); - lits.push_back(~mk_eq(e2, emp, false)); + lits.push_back(~e2_is_emp); lits.push_back(lit); propagate_lit(0, lits.size(), lits.c_ptr(), ~mk_literal(m_util.str.mk_prefix(tail1, tail2))); return false; @@ -2650,28 +2688,32 @@ bool theory_seq::add_suffix2suffix(expr* e) { } expr_ref emp(m_util.str.mk_empty(m.get_sort(e1)), m); - - switch (assume_equality(e2, emp)) { + literal e2_is_emp = mk_eq_empty(e2); + switch (ctx.get_assignment(e2_is_emp)) { case l_true: + TRACE("seq", tout << mk_pp(e, m) << " " << mk_pp(e2, m) << " is empty\n";); return false; // done case l_undef: - ctx.force_phase(mk_eq(e2, emp, false)); + TRACE("seq", tout << mk_pp(e, m) << " " << mk_pp(e2, m) << " is unassigned\n";); + ctx.force_phase(e2_is_emp); return true; // retry case l_false: break; } - expr_ref first2 = mk_skolem(m_seq_first, e2); + expr_ref first2 = mk_first(e2); expr_ref last2 = mk_last(e2); - expr_ref first1 = mk_skolem(m_seq_first, e1); + expr_ref first1 = mk_first(e1); expr_ref last1 = mk_last(e1); expr_ref conc = mk_concat(first2, m_util.str.mk_unit(last2)); - propagate_eq(~mk_eq(e2, emp, false), e2, conc); + propagate_eq(~e2_is_emp, e2, conc, true); literal last_eq = mk_eq(last1, last2, false); switch (ctx.get_assignment(last_eq)) { case l_false: + TRACE("seq", tout << mk_pp(e, m) << " " << last1 << " = " << last2 << " is false\n";); return false; // done case l_undef: + TRACE("seq", tout << mk_pp(e, m) << " " << last1 << " = " << last2 << " is unassigned\n";); ctx.force_phase(~last_eq); return true; case l_true: @@ -2680,9 +2722,10 @@ bool theory_seq::add_suffix2suffix(expr* e) { literal_vector lits; lits.push_back(~ctx.get_literal(e)); - lits.push_back(~mk_eq(e2, emp, false)); + lits.push_back(~e2_is_emp); lits.push_back(last_eq); propagate_lit(0, lits.size(), lits.c_ptr(), ~mk_literal(m_util.str.mk_suffix(first1, first2))); + TRACE("seq", tout << mk_pp(e, m) << " saturate\n";); return false; } diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index fd1219d4b..8ad9e7caf 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -192,6 +192,7 @@ namespace smt { expr_ref m_e; public: replay_length_coherence(ast_manager& m, expr* e) : m_e(e, m) {} + virtual ~replay_length_coherence() {} virtual void operator()(theory_seq& th) { th.check_length_coherence(m_e); m_e.reset(); @@ -202,6 +203,7 @@ namespace smt { expr_ref m_e; public: replay_axiom(ast_manager& m, expr* e) : m_e(e, m) {} + virtual ~replay_axiom() {} virtual void operator()(theory_seq& th) { th.enque_axiom(m_e); m_e.reset(); @@ -336,7 +338,7 @@ namespace smt { void propagate_lit(dependency* dep, literal lit) { propagate_lit(dep, 0, 0, lit); } void propagate_lit(dependency* dep, unsigned n, literal const* lits, literal lit); void propagate_eq(dependency* dep, enode* n1, enode* n2); - void propagate_eq(literal lit, expr* e1, expr* e2, bool add_to_eqs = false); + void propagate_eq(literal lit, expr* e1, expr* e2, bool add_to_eqs); void set_conflict(dependency* dep, literal_vector const& lits = literal_vector()); u_map m_branch_start; @@ -355,6 +357,7 @@ namespace smt { bool is_tail(expr* a, expr*& s, unsigned& idx) const; expr_ref mk_nth(expr* s, expr* idx); expr_ref mk_last(expr* e); + expr_ref mk_first(expr* e); expr_ref canonize(expr* e, dependency*& eqs); bool canonize(expr* e, expr_ref_vector& es, dependency*& eqs); bool canonize(expr_ref_vector const& es, expr_ref_vector& result, dependency*& eqs); From 1f872e720d99b37d0775098382b17928f8160ffc Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 19 Jan 2016 15:19:00 +0000 Subject: [PATCH 14/17] remove m_replay_stack from API context since it's never used Signed-off-by: Nuno Lopes --- src/api/api_context.cpp | 12 ------------ src/api/api_context.h | 1 - 2 files changed, 13 deletions(-) diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 75782a28d..47a25f313 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -76,7 +76,6 @@ namespace api { m_sutil(m()), m_last_result(m()), m_ast_trail(m()), - m_replay_stack(), m_pmanager(m_limit) { m_error_code = Z3_OK; @@ -100,23 +99,12 @@ namespace api { m_fpa_fid = m().mk_family_id("fpa"); m_seq_fid = m().mk_family_id("seq"); m_dt_plugin = static_cast(m().get_plugin(m_dt_fid)); - - if (!m_user_ref_count) { - m_replay_stack.push_back(0); - } install_tactics(*this); } context::~context() { - m_last_obj = 0; - if (!m_user_ref_count) { - for (unsigned i = 0; i < m_replay_stack.size(); ++i) { - dealloc(m_replay_stack[i]); - } - m_ast_trail.reset(); - } reset_parser(); } diff --git a/src/api/api_context.h b/src/api/api_context.h index 23c8d3fd2..de492bb45 100644 --- a/src/api/api_context.h +++ b/src/api/api_context.h @@ -68,7 +68,6 @@ namespace api { ast_ref_vector m_last_result; //!< used when m_user_ref_count == true ast_ref_vector m_ast_trail; //!< used when m_user_ref_count == false unsigned_vector m_ast_lim; - ptr_vector m_replay_stack; ref m_last_obj; //!< reference to the last API object returned by the APIs From 23cc8258fe2ade1bd56f9a7a12d5456cc999d07d Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 19 Jan 2016 15:37:58 +0000 Subject: [PATCH 15/17] remove m_ast_lim from API context since that one isn't used either Signed-off-by: Nuno Lopes --- src/api/api_context.h | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/src/api/api_context.h b/src/api/api_context.h index de492bb45..fa6754120 100644 --- a/src/api/api_context.h +++ b/src/api/api_context.h @@ -58,7 +58,7 @@ namespace api { bv_util m_bv_util; datalog::dl_decl_util m_datalog_util; fpa_util m_fpa_util; - datatype_util m_dtutil; + datatype_util m_dtutil; seq_util m_sutil; // Support for old solver API @@ -67,7 +67,6 @@ namespace api { ast_ref_vector m_last_result; //!< used when m_user_ref_count == true ast_ref_vector m_ast_trail; //!< used when m_user_ref_count == false - unsigned_vector m_ast_lim; ref m_last_obj; //!< reference to the last API object returned by the APIs @@ -122,7 +121,7 @@ namespace api { bv_util & bvutil() { return m_bv_util; } datalog::dl_decl_util & datalog_util() { return m_datalog_util; } fpa_util & fpautil() { return m_fpa_util; } - datatype_util& dtutil() { return m_dtutil; } + datatype_util& dtutil() { return m_dtutil; } seq_util& sutil() { return m_sutil; } family_id get_basic_fid() const { return m_basic_fid; } family_id get_array_fid() const { return m_array_fid; } @@ -180,8 +179,6 @@ namespace api { void interrupt(); void invoke_error_handler(Z3_error_code c); - - static void out_of_memory_handler(void * _ctx); void check_sorts(ast * n); From a021e51a9c38590accc96054218ffd81503484de Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 19 Jan 2016 19:09:41 +0100 Subject: [PATCH 16/17] make parse error a bit more informative Signed-off-by: Nikolaj Bjorner --- src/parsers/smt2/smt2parser.cpp | 43 ++++++++++++++++++--------------- 1 file changed, 23 insertions(+), 20 deletions(-) diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index f23207f66..91be93c0e 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -432,8 +432,10 @@ namespace smt2 { } } - void unknown_sort(symbol id) { - std::string msg = "unknown sort '"; + void unknown_sort(symbol id, char const* context = "") { + std::string msg = context; + if (context[0]) msg += ": "; + msg += "unknown sort '"; msg += id.str() + "'"; throw parser_exception(msg.c_str()); } @@ -528,12 +530,12 @@ namespace smt2 { SASSERT(sexpr_stack().size() == stack_pos + 1); } - sort * parse_sort_name() { + sort * parse_sort_name(char const* context = "") { SASSERT(curr_is_identifier()); symbol id = curr_id(); psort_decl * d = m_ctx.find_psort_decl(id); if (d == 0) - unknown_sort(id); + unknown_sort(id, context); if (!d->has_var_params() && d->get_num_params() != 0) throw parser_exception("sort constructor expects parameters"); sort * r = d->instantiate(pm()); @@ -689,23 +691,24 @@ namespace smt2 { next(); } - void parse_sort() { + void parse_sort(char const* context) { unsigned stack_pos = sort_stack().size(); unsigned num_frames = 0; do { if (curr_is_identifier()) { - sort_stack().push_back(parse_sort_name()); + sort_stack().push_back(parse_sort_name(context)); } else if (curr_is_rparen()) { - if (num_frames == 0) - throw parser_exception("invalid sort, unexpected ')'"); + if (num_frames == 0) { + throw parser_exception(std::string(context) + " invalid sort, unexpected ')'"); + } pop_sort_app_frame(); num_frames--; } else { check_lparen_next("invalid sort, symbol, '_' or '(' expected"); if (!curr_is_identifier()) - throw parser_exception("invalid sort, symbol or '_' expected"); + throw parser_exception(std::string(context) + " invalid sort, symbol or '_' expected"); if (curr_id_is_underscore()) { sort_stack().push_back(parse_indexed_sort()); } @@ -723,7 +726,7 @@ namespace smt2 { unsigned sz = 0; check_lparen_next(context); while (!curr_is_rparen()) { - parse_sort(); + parse_sort(context); sz++; } next(); @@ -1151,7 +1154,7 @@ namespace smt2 { symbol_stack().push_back(curr_id()); TRACE("parse_sorted_vars", tout << "push_back curr_id(): " << curr_id() << "\n";); next(); - parse_sort(); + parse_sort("invalid sorted variables"); check_rparen_next("invalid sorted variable, ')' expected"); num++; } @@ -1243,7 +1246,7 @@ namespace smt2 { has_as = true; next(); symbol r = parse_indexed_identifier(); - parse_sort(); + parse_sort("Invalid qualified identifier"); check_rparen_next("invalid qualified identifier, ')' expected"); return r; } @@ -1848,7 +1851,7 @@ namespace smt2 { unsigned sort_spos = sort_stack().size(); unsigned expr_spos = expr_stack().size(); unsigned num_vars = parse_sorted_vars(); - parse_sort(); + parse_sort("Invalid function definition"); parse_expr(); if (m().get_sort(expr_stack().back()) != sort_stack().back()) throw parser_exception("invalid function/constant definition, sort mismatch"); @@ -1936,7 +1939,7 @@ namespace smt2 { unsigned expr_spos = expr_stack().size(); unsigned num_vars = parse_sorted_vars(); SASSERT(num_vars == m_num_bindings); - parse_sort(); + parse_sort("Invalid recursive function definition"); f = m().mk_func_decl(id, num_vars, sort_stack().c_ptr() + sort_spos, sort_stack().back()); bindings.append(num_vars, expr_stack().c_ptr() + expr_spos); ids.append(num_vars, symbol_stack().c_ptr() + sym_spos); @@ -1999,7 +2002,7 @@ namespace smt2 { check_identifier("invalid constant definition, symbol expected"); symbol id = curr_id(); next(); - parse_sort(); + parse_sort("Invalid constant definition"); parse_expr(); if (m().get_sort(expr_stack().back()) != sort_stack().back()) throw parser_exception("invalid constant definition, sort mismatch"); @@ -2020,7 +2023,7 @@ namespace smt2 { next(); unsigned spos = sort_stack().size(); unsigned num_params = parse_sorts("Parsing function declaration. Expecting sort list '('"); - parse_sort(); + parse_sort("Invalid function declaration"); func_decl_ref f(m()); f = m().mk_func_decl(id, num_params, sort_stack().c_ptr() + spos, sort_stack().back()); sort_stack().shrink(spos); @@ -2037,7 +2040,7 @@ namespace smt2 { check_identifier("invalid constant declaration, symbol expected"); symbol id = curr_id(); next(); - parse_sort(); + parse_sort("Invalid constant declaration"); SASSERT(!sort_stack().empty()); func_decl_ref c(m()); c = m().mk_const_decl(id, sort_stack().back()); @@ -2300,9 +2303,9 @@ namespace smt2 { next(); } unsigned spos = sort_stack().size(); - parse_sorts("Parsing function name. Expecting sort list startig with '(' to disambiguate function name"); + parse_sorts("Invalid function name. Expecting sort list startig with '(' to disambiguate function name"); unsigned domain_size = sort_stack().size() - spos; - parse_sort(); + parse_sort("Invalid function name"); func_decl * d = m_ctx.find_func_decl(id, indices.size(), indices.c_ptr(), domain_size, sort_stack().c_ptr() + spos, sort_stack().back()); sort_stack().shrink(spos); check_rparen_next("invalid function declaration reference, ')' expected"); @@ -2375,7 +2378,7 @@ namespace smt2 { break; } case CPK_SORT: - parse_sort(); + parse_sort("invalid command argument, sort expected"); m_curr_cmd->set_next_arg(m_ctx, sort_stack().back()); return; case CPK_SORT_LIST: { From 993a0434b442c92e4e84103490722c5428be5ecd Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 19 Jan 2016 23:47:35 -0500 Subject: [PATCH 17/17] fix warning message for unused variable Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index cc84388d3..71f1b03ea 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -568,7 +568,6 @@ bool theory_seq::check_extensionality() { context& ctx = get_context(); unsigned sz = get_num_vars(); unsigned_vector seqs; - bool added_assumption = false; for (unsigned v = 0; v < sz; ++v) { enode* n = get_enode(v); expr* o1 = n->get_owner();