From 8bd0407adfc00b8f1b1b3f8b79319285d39df824 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 31 Jul 2017 09:13:50 -0700 Subject: [PATCH 01/10] fix #1177 Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.cpp | 11 ++++++----- src/smt/smt_justification.h | 1 + 2 files changed, 7 insertions(+), 5 deletions(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index b5789a597..1b428520e 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -2406,7 +2406,7 @@ namespace smt { if (m_manager.has_trace_stream()) m_manager.trace_stream() << "[pop] " << num_scopes << " " << m_scope_lvl << "\n"; - TRACE("context", tout << "backtracking: " << num_scopes << "\n";); + TRACE("context", tout << "backtracking: " << num_scopes << " from " << m_scope_lvl << "\n";); TRACE("pop_scope_detail", display(tout);); SASSERT(num_scopes > 0); SASSERT(num_scopes <= m_scope_lvl); @@ -2901,10 +2901,10 @@ namespace smt { } push_scope(); m_base_scopes.push_back(base_scope()); - base_scope & bs = m_base_scopes.back(); - bs.m_lemmas_lim = m_lemmas.size(); - bs.m_inconsistent = inconsistent(); - bs.m_simp_qhead_lim = m_simp_qhead; + base_scope & bs = m_base_scopes.back(); + bs.m_lemmas_lim = m_lemmas.size(); + bs.m_inconsistent = inconsistent(); + bs.m_simp_qhead_lim = m_simp_qhead; m_base_lvl++; m_search_lvl++; // Not really necessary. But, it is useful to enforce the invariant m_search_lvl >= m_base_lvl SASSERT(m_base_lvl <= m_scope_lvl); @@ -2912,6 +2912,7 @@ namespace smt { void context::pop(unsigned num_scopes) { SASSERT (num_scopes > 0); + if (num_scopes > m_scope_lvl) return; pop_to_base_lvl(); pop_scope(num_scopes); } diff --git a/src/smt/smt_justification.h b/src/smt/smt_justification.h index ea969d1db..5bfa8bbf0 100644 --- a/src/smt/smt_justification.h +++ b/src/smt/smt_justification.h @@ -148,6 +148,7 @@ namespace smt { m_node1(n1), m_node2(n2), m_js(js) { + SASSERT(n1 != n2); } virtual void get_antecedents(conflict_resolution & cr); From ceca9fbef0a35e3b554a267f82f2cb105ec25e6f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 31 Jul 2017 09:23:55 -0700 Subject: [PATCH 02/10] fixes #1176 Signed-off-by: Nikolaj Bjorner --- src/smt/smt_justification.h | 1 - src/smt/smt_model_finder.cpp | 15 +++++++-------- 2 files changed, 7 insertions(+), 9 deletions(-) diff --git a/src/smt/smt_justification.h b/src/smt/smt_justification.h index 5bfa8bbf0..ea969d1db 100644 --- a/src/smt/smt_justification.h +++ b/src/smt/smt_justification.h @@ -148,7 +148,6 @@ namespace smt { m_node1(n1), m_node2(n2), m_js(js) { - SASSERT(n1 != n2); } virtual void get_antecedents(conflict_resolution & cr); diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index ff84992e1..eb113b484 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -760,7 +760,7 @@ namespace smt { ptr_vector const & exceptions = n->get_exceptions(); ptr_vector const & avoid_set = n->get_avoid_set(); obj_map const & elems = s->get_elems(); - SASSERT(!elems.empty()); + if (elems.empty()) return; if (!exceptions.empty() || !avoid_set.empty()) { ptr_buffer ex_vals; collect_exceptions_values(n, ex_vals); @@ -927,15 +927,14 @@ namespace smt { ptr_buffer values; get_instantiation_set_values(n, values); sort * s = n->get_sort(); - expr * else_val = eval(n->get_else(), true); - func_decl * p = m_manager.mk_fresh_func_decl(1, &s, s); + func_decl * p = m_manager.mk_fresh_func_decl(1, &s, s); func_interp * pi = alloc(func_interp, m_manager, 1); - pi->set_else(else_val); m_model->register_aux_decl(p, pi); - ptr_buffer::const_iterator it = values.begin(); - ptr_buffer::const_iterator end = values.end(); - for (; it != end; ++it) { - expr * v = *it; + if (n->get_else()) { + expr * else_val = eval(n->get_else(), true); + pi->set_else(else_val); + } + for (expr * v : values) { pi->insert_new_entry(&v, v); } n->set_proj(p); From 74890ca1c8fe625e6a45d4e45fc6e7a6940fad58 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 31 Jul 2017 09:37:25 -0700 Subject: [PATCH 03/10] fixes #1180 Signed-off-by: Nikolaj Bjorner --- src/cmd_context/eval_cmd.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/cmd_context/eval_cmd.cpp b/src/cmd_context/eval_cmd.cpp index 86078a13c..3b00179c6 100644 --- a/src/cmd_context/eval_cmd.cpp +++ b/src/cmd_context/eval_cmd.cpp @@ -58,6 +58,8 @@ public: virtual void execute(cmd_context & ctx) { if (!ctx.is_model_available()) throw cmd_exception("model is not available"); + if (!m_target) + throw cmd_exception("no arguments passed to eval"); model_ref md; unsigned index = m_params.get_uint("model_index", 0); check_sat_result * last_result = ctx.get_check_sat_result(); From 62b8394bdd6fdb4dcdb634aa2055692095265786 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 31 Jul 2017 09:52:45 -0700 Subject: [PATCH 04/10] fixes #1179 Signed-off-by: Nikolaj Bjorner --- src/smt/smt_justification.h | 1 + src/smt/theory_seq.cpp | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/src/smt/smt_justification.h b/src/smt/smt_justification.h index ea969d1db..f4b3ecb12 100644 --- a/src/smt/smt_justification.h +++ b/src/smt/smt_justification.h @@ -181,6 +181,7 @@ namespace smt { enode * m_node2; public: eq_propagation_justification(enode * n1, enode * n2):m_node1(n1), m_node2(n2) { + SASSERT(n1 != n2); } virtual void get_antecedents(conflict_resolution & cr); diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 832995994..76d8a5a74 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -1891,7 +1891,7 @@ bool theory_seq::solve_ne(unsigned idx) { new_ls.push_back(ls); new_rs.push_back(rs); } - else { + else if (nl != nr) { literal lit(mk_eq(nl, nr, false)); ctx.mark_as_relevant(lit); new_lits.push_back(lit); From be1df279ecac4bb3a9a07008368540d1b860faba Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Mon, 31 Jul 2017 14:11:07 -0400 Subject: [PATCH 05/10] make proof_checker less verbose --- src/ast/proof_checker/proof_checker.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/ast/proof_checker/proof_checker.cpp b/src/ast/proof_checker/proof_checker.cpp index 45223cdb7..df4a8e344 100644 --- a/src/ast/proof_checker/proof_checker.cpp +++ b/src/ast/proof_checker/proof_checker.cpp @@ -1299,7 +1299,7 @@ bool proof_checker::check_arith_literal(bool is_pos, app* lit0, rational const& is_pos = !is_pos; } if (!a.is_le(lit) && !a.is_lt(lit) && !a.is_ge(lit) && !a.is_gt(lit) && !m.is_eq(lit)) { - IF_VERBOSE(0, verbose_stream() << mk_pp(lit, m) << "\n";); + IF_VERBOSE(2, verbose_stream() << "Not arith literal: " << mk_pp(lit, m) << "\n";); return false; } SASSERT(lit->get_num_args() == 2); @@ -1363,7 +1363,7 @@ bool proof_checker::check_arith_literal(bool is_pos, app* lit0, rational const& rw(sum); } - IF_VERBOSE(0, verbose_stream() << coeff << "\n" << mk_pp(lit0, m) << "\n" << mk_pp(sum, m) << "\n";); + IF_VERBOSE(2, verbose_stream() << "coeff,lit,sum " << coeff << "\n" << mk_pp(lit0, m) << "\n" << mk_pp(sum, m) << "\n";); #endif return true; From 15451ae8580a8bf230ce2d1257bc7f0a64b19d80 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Mon, 31 Jul 2017 14:13:08 -0400 Subject: [PATCH 06/10] extra flags to control quant_hoist --- src/ast/rewriter/quant_hoist.cpp | 80 ++++++++++++++++++-------------- src/ast/rewriter/quant_hoist.h | 8 ++-- 2 files changed, 50 insertions(+), 38 deletions(-) diff --git a/src/ast/rewriter/quant_hoist.cpp b/src/ast/rewriter/quant_hoist.cpp index e59a079e7..9c345851a 100644 --- a/src/ast/rewriter/quant_hoist.cpp +++ b/src/ast/rewriter/quant_hoist.cpp @@ -41,9 +41,9 @@ public: m_rewriter(m) {} - void operator()(expr* fml, app_ref_vector& vars, bool& is_fa, expr_ref& result) { + void operator()(expr* fml, app_ref_vector& vars, bool& is_fa, expr_ref& result, bool use_fresh, bool rewrite_ok) { quantifier_type qt = Q_none_pos; - pull_quantifier(fml, qt, vars, result); + pull_quantifier(fml, qt, vars, result, use_fresh, rewrite_ok); TRACE("qe_verbose", tout << mk_pp(fml, m) << "\n"; tout << mk_pp(result, m) << "\n";); @@ -51,36 +51,38 @@ public: is_fa = (Q_forall_pos == qt); } - void pull_exists(expr* fml, app_ref_vector& vars, expr_ref& result) { + void pull_exists(expr* fml, app_ref_vector& vars, expr_ref& result, bool use_fresh, bool rewrite_ok) { quantifier_type qt = Q_exists_pos; - pull_quantifier(fml, qt, vars, result); + pull_quantifier(fml, qt, vars, result, use_fresh, rewrite_ok); TRACE("qe_verbose", tout << mk_pp(fml, m) << "\n"; tout << mk_pp(result, m) << "\n";); } - void pull_quantifier(bool is_forall, expr_ref& fml, app_ref_vector& vars) { + void pull_quantifier(bool is_forall, expr_ref& fml, app_ref_vector& vars, bool use_fresh, bool rewrite_ok) { quantifier_type qt = is_forall?Q_forall_pos:Q_exists_pos; expr_ref result(m); - pull_quantifier(fml, qt, vars, result); + pull_quantifier(fml, qt, vars, result, use_fresh, rewrite_ok); TRACE("qe_verbose", tout << mk_pp(fml, m) << "\n"; tout << mk_pp(result, m) << "\n";); fml = result; } - void extract_quantifier(quantifier* q, app_ref_vector& vars, expr_ref& result) { + void extract_quantifier(quantifier* q, app_ref_vector& vars, expr_ref& result, bool use_fresh) { unsigned nd = q->get_num_decls(); for (unsigned i = 0; i < nd; ++i) { sort* s = q->get_decl_sort(i); - app* a = m.mk_fresh_const(q->get_decl_name(i).str().c_str(), s); + symbol const& sym = q->get_decl_name (i); + app* a = use_fresh ? m.mk_fresh_const(sym.str ().c_str (), s) + : m.mk_const (sym, s); vars.push_back(a); } expr * const * exprs = (expr* const*) (vars.c_ptr() + vars.size()- nd); instantiate(m, q, exprs, result); } - unsigned pull_quantifier(bool is_forall, expr_ref& fml, ptr_vector* sorts, svector* names) { + unsigned pull_quantifier(bool is_forall, expr_ref& fml, ptr_vector* sorts, svector* names, bool use_fresh, bool rewrite_ok) { unsigned index = var_counter().get_next_var(fml); while (is_quantifier(fml) && (is_forall == to_quantifier(fml)->is_forall())) { quantifier* q = to_quantifier(fml); @@ -97,7 +99,7 @@ public: return index; } app_ref_vector vars(m); - pull_quantifier(is_forall, fml, vars); + pull_quantifier(is_forall, fml, vars, use_fresh, rewrite_ok); if (vars.empty()) { return index; } @@ -192,7 +194,7 @@ private: } - void pull_quantifier(expr* fml, quantifier_type& qt, app_ref_vector& vars, expr_ref& result) { + void pull_quantifier(expr* fml, quantifier_type& qt, app_ref_vector& vars, expr_ref& result, bool use_fresh, bool rewrite_ok) { if (!has_quantifiers(fml)) { result = fml; @@ -209,38 +211,48 @@ private: if (m.is_and(fml)) { num_args = a->get_num_args(); for (unsigned i = 0; i < num_args; ++i) { - pull_quantifier(a->get_arg(i), qt, vars, tmp); + pull_quantifier(a->get_arg(i), qt, vars, tmp, use_fresh, rewrite_ok); args.push_back(tmp); } + if (rewrite_ok) { m_rewriter.mk_and(args.size(), args.c_ptr(), result); + } + else { + result = m.mk_and (args.size (), args.c_ptr ()); + } } else if (m.is_or(fml)) { num_args = to_app(fml)->get_num_args(); for (unsigned i = 0; i < num_args; ++i) { - pull_quantifier(to_app(fml)->get_arg(i), qt, vars, tmp); + pull_quantifier(to_app(fml)->get_arg(i), qt, vars, tmp, use_fresh, rewrite_ok); args.push_back(tmp); } + if (rewrite_ok) { m_rewriter.mk_or(args.size(), args.c_ptr(), result); + } + else { + result = m.mk_or (args.size (), args.c_ptr ()); + } } else if (m.is_not(fml)) { - pull_quantifier(to_app(fml)->get_arg(0), negate(qt), vars, tmp); + pull_quantifier(to_app(fml)->get_arg(0), negate(qt), vars, tmp, use_fresh, rewrite_ok); negate(qt); result = m.mk_not(tmp); } else if (m.is_implies(fml, t1, t2)) { - pull_quantifier(t1, negate(qt), vars, tmp); + pull_quantifier(t1, negate(qt), vars, tmp, use_fresh, rewrite_ok); negate(qt); - pull_quantifier(t2, qt, vars, result); + pull_quantifier(t2, qt, vars, result, use_fresh, rewrite_ok); result = m.mk_implies(tmp, result); } else if (m.is_ite(fml, t1, t2, t3)) { expr_ref tt1(m), tt2(m), tt3(m), ntt1(m), nt1(m); - pull_quantifier(t2, qt, vars, tt2); - pull_quantifier(t3, qt, vars, tt3); + pull_quantifier(t2, qt, vars, tt2, use_fresh, rewrite_ok); + pull_quantifier(t3, qt, vars, tt3, use_fresh, rewrite_ok); if (has_quantifiers(t1)) { - pull_quantifier(t1, qt, vars, tt1); + pull_quantifier(t1, qt, vars, tt1, use_fresh, rewrite_ok); nt1 = m.mk_not(t1); - pull_quantifier(nt1, qt, vars, ntt1); + pull_quantifier(nt1, qt, vars, ntt1, use_fresh, rewrite_ok); result = m.mk_and(m.mk_or(ntt1, tt2), m.mk_or(tt1, tt3)); } else { @@ -249,12 +261,12 @@ private: } else if ((m.is_eq(fml, t1, t2) && m.is_bool(t1)) || m.is_iff(fml, t1, t2)) { expr_ref tt1(m), tt2(m), ntt1(m), ntt2(m), nt1(m), nt2(m); - pull_quantifier(t1, qt, vars, tt1); - pull_quantifier(t2, qt, vars, tt2); + pull_quantifier(t1, qt, vars, tt1, use_fresh, rewrite_ok); + pull_quantifier(t2, qt, vars, tt2, use_fresh, rewrite_ok); nt1 = m.mk_not(t1); nt2 = m.mk_not(t2); - pull_quantifier(nt1, qt, vars, ntt1); - pull_quantifier(nt2, qt, vars, ntt2); + pull_quantifier(nt1, qt, vars, ntt1, use_fresh, rewrite_ok); + pull_quantifier(nt2, qt, vars, ntt2, use_fresh, rewrite_ok); result = m.mk_and(m.mk_or(ntt1, tt2), m.mk_or(ntt2, tt1)); } else { @@ -271,8 +283,8 @@ private: break; } set_quantifier_type(qt, q->is_forall()); - extract_quantifier(q, vars, tmp); - pull_quantifier(tmp, qt, vars, result); + extract_quantifier(q, vars, tmp, use_fresh); + pull_quantifier(tmp, qt, vars, result, use_fresh, rewrite_ok); break; } case AST_VAR: @@ -295,18 +307,18 @@ quantifier_hoister::~quantifier_hoister() { dealloc(m_impl); } -void quantifier_hoister::operator()(expr* fml, app_ref_vector& vars, bool& is_fa, expr_ref& result) { - (*m_impl)(fml, vars, is_fa, result); +void quantifier_hoister::operator()(expr* fml, app_ref_vector& vars, bool& is_fa, expr_ref& result, bool use_fresh, bool rewrite_ok) { + (*m_impl)(fml, vars, is_fa, result, use_fresh, rewrite_ok); } -void quantifier_hoister::pull_exists(expr* fml, app_ref_vector& vars, expr_ref& result) { - m_impl->pull_exists(fml, vars, result); +void quantifier_hoister::pull_exists(expr* fml, app_ref_vector& vars, expr_ref& result, bool use_fresh, bool rewrite_ok) { + m_impl->pull_exists(fml, vars, result, use_fresh, rewrite_ok); } -void quantifier_hoister::pull_quantifier(bool is_forall, expr_ref& fml, app_ref_vector& vars) { - m_impl->pull_quantifier(is_forall, fml, vars); +void quantifier_hoister::pull_quantifier(bool is_forall, expr_ref& fml, app_ref_vector& vars, bool use_fresh, bool rewrite_ok) { + m_impl->pull_quantifier(is_forall, fml, vars, use_fresh, rewrite_ok); } -unsigned quantifier_hoister::pull_quantifier(bool is_forall, expr_ref& fml, ptr_vector* sorts, svector* names) { - return m_impl->pull_quantifier(is_forall, fml, sorts, names); +unsigned quantifier_hoister::pull_quantifier(bool is_forall, expr_ref& fml, ptr_vector* sorts, svector* names, bool use_fresh, bool rewrite_ok) { + return m_impl->pull_quantifier(is_forall, fml, sorts, names, use_fresh, rewrite_ok); } diff --git a/src/ast/rewriter/quant_hoist.h b/src/ast/rewriter/quant_hoist.h index 90e6ec7ad..52a2fcda1 100644 --- a/src/ast/rewriter/quant_hoist.h +++ b/src/ast/rewriter/quant_hoist.h @@ -43,14 +43,14 @@ public: or, and, implies, ite (then and else branch only). */ - void operator()(expr* fml, app_ref_vector& vars, bool& is_fa, expr_ref& result); + void operator()(expr* fml, app_ref_vector& vars, bool& is_fa, expr_ref& result, bool use_fresh = true, bool rewrite_ok = true); /** \brief Pull top-most existential quantifier up. The list of variables is empty if there are no top-level existential quantifier. */ - void pull_exists(expr* fml, app_ref_vector& vars, expr_ref& result); + void pull_exists(expr* fml, app_ref_vector& vars, expr_ref& result, bool use_fresh = true, bool rewrite_ok = true); /** @@ -58,7 +58,7 @@ public: The list of variables is empty if there are no top-level universal/existential quantifier. */ - void pull_quantifier(bool is_forall, expr_ref& fml, app_ref_vector& vars); + void pull_quantifier(bool is_forall, expr_ref& fml, app_ref_vector& vars, bool use_fresh = true, bool rewrite_ok = true); /** \brief Pull top-most universal (is_forall true) or existential (is_forall=false) quantifier up. @@ -66,7 +66,7 @@ public: Return index of maximal variable. */ - unsigned pull_quantifier(bool is_forall, expr_ref& fml, ptr_vector* sorts, svector* names); + unsigned pull_quantifier(bool is_forall, expr_ref& fml, ptr_vector* sorts, svector* names, bool use_fresh = true, bool rewrite_ok = true); }; From 7670b49ada29df98776a15fdebf2a85be4de3631 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Mon, 31 Jul 2017 14:14:35 -0400 Subject: [PATCH 07/10] mark mk_true() and mk_false() const --- src/ast/ast.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/ast/ast.h b/src/ast/ast.h index f71d5135c..75d3eb0f2 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -2021,8 +2021,8 @@ public: app * mk_not(expr * n) { return mk_app(m_basic_family_id, OP_NOT, n); } app * mk_distinct(unsigned num_args, expr * const * args); app * mk_distinct_expanded(unsigned num_args, expr * const * args); - app * mk_true() { return m_true; } - app * mk_false() { return m_false; } + app * mk_true() const { return m_true; } + app * mk_false() const { return m_false; } app * mk_bool_val(bool b) { return b?m_true:m_false; } app * mk_interp(expr * arg) { return mk_app(m_basic_family_id, OP_INTERP, arg); } From 331eec8a05e857773e196dcbafbd4aff589c87a2 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Mon, 31 Jul 2017 14:19:16 -0400 Subject: [PATCH 08/10] option to control array_der in qe_lite --- src/qe/qe_lite.cpp | 15 +++++++++------ src/qe/qe_lite.h | 5 ++++- 2 files changed, 13 insertions(+), 7 deletions(-) diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp index ce182a97b..ff2abde75 100644 --- a/src/qe/qe_lite.cpp +++ b/src/qe/qe_lite.cpp @@ -2342,6 +2342,7 @@ private: elim_star m_elim_star; th_rewriter m_rewriter; + bool m_use_array_der; bool has_unique_non_ground(expr_ref_vector const& fmls, unsigned& index) { index = fmls.size(); if (index <= 1) { @@ -2359,13 +2360,14 @@ private: } public: - impl(ast_manager & m, params_ref const & p): + impl(ast_manager & m, params_ref const & p, bool use_array_der): m(m), m_der(m, p), m_fm(m), m_array_der(m), m_elim_star(*this), - m_rewriter(m) {} + m_rewriter(m), + m_use_array_der(use_array_der) {} void operator()(app_ref_vector& vars, expr_ref& fml) { if (vars.empty()) { @@ -2445,14 +2447,15 @@ public: m_array_der.set_is_variable_proc(is_var); m_der(fmls); m_fm(fmls); - m_array_der(fmls); + // AG: disalble m_array_der() since it interferes with other array handling + if (m_use_array_der) m_array_der(fmls); TRACE("qe_lite", for (unsigned i = 0; i < fmls.size(); ++i) tout << mk_pp(fmls[i].get(), m) << "\n";); } }; -qe_lite::qe_lite(ast_manager & m, params_ref const & p) { - m_impl = alloc(impl, m, p); +qe_lite::qe_lite(ast_manager & m, params_ref const & p, bool use_array_der) { + m_impl = alloc(impl, m, p, use_array_der); } qe_lite::~qe_lite() { @@ -2484,7 +2487,7 @@ class qe_lite_tactic : public tactic { imp(ast_manager& m, params_ref const & p): m(m), - m_qe(m, p) + m_qe(m, p, true) {} void checkpoint() { diff --git a/src/qe/qe_lite.h b/src/qe/qe_lite.h index cff547f36..a918ab33d 100644 --- a/src/qe/qe_lite.h +++ b/src/qe/qe_lite.h @@ -31,7 +31,10 @@ class qe_lite { class impl; impl * m_impl; public: - qe_lite(ast_manager & m, params_ref const & p); + /** + use_array_der controls whether equalities over array reads are simplified + */ + qe_lite(ast_manager& m, params_ref const & p, bool use_array_der = true); ~qe_lite(); From 1d5713c3764a6f9fb62f2fff39d5dc727c4d2321 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Mon, 31 Jul 2017 14:21:30 -0400 Subject: [PATCH 09/10] move semantics for ref --- src/util/ref.h | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/src/util/ref.h b/src/util/ref.h index d9663f9a4..811aba9af 100644 --- a/src/util/ref.h +++ b/src/util/ref.h @@ -50,6 +50,7 @@ public: inc_ref(); } + ref (ref && r): m_ptr (r.detach ()) {} ~ref() { dec_ref(); } @@ -89,6 +90,14 @@ public: return *this; } + ref & operator=(ref &&r) { + if (this != &r) { + dec_ref (); + m_ptr = r.detach (); + } + return *this; + } + void reset() { dec_ref(); m_ptr = 0; @@ -107,6 +116,11 @@ public: friend bool operator!=(const ref & r1, const ref & r2) { return r1.m_ptr != r2.m_ptr; } + friend void swap (ref &r1, ref &r2) { + T* tmp = r1.m_ptr; + r1.m_ptr = r2.m_ptr; + r2.m_ptr = tmp; + } }; /** From 71d80ab47f21a07a54cdf61366a7028df82488d3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 31 Jul 2017 11:54:11 -0700 Subject: [PATCH 10/10] fix build break based on new assertion in smt-eq-justification Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 76d8a5a74..e72cd3f6d 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -1681,6 +1681,7 @@ bool theory_seq::solve_binary_eq(expr_ref_vector const& ls, expr_ref_vector cons bool has_conflict = false; for (unsigned j = 0; !has_conflict && j < sz; ++j) { unsigned j1 = (offset + j) % sz; + if (xs[j] == ys[j1]) continue; literal eq = mk_eq(xs[j], ys[j1], false); switch (ctx.get_assignment(eq)) { case l_false: