From 1b503b888710b4bf14bbd5f409bdeb2b3f74beac Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 6 Apr 2021 20:09:42 -0700 Subject: [PATCH] na --- src/ast/rewriter/seq_rewriter.cpp | 12 +++++++++++- src/ast/rewriter/th_rewriter.cpp | 9 +++++++++ src/smt/theory_lra.cpp | 29 ++++++++++++++++------------- 3 files changed, 36 insertions(+), 14 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 2c04d962f..75c0d9daf 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -4853,7 +4853,17 @@ bool seq_rewriter::reduce_itos(expr_ref_vector& ls, expr_ref_vector& rs, bool seq_rewriter::reduce_eq_empty(expr* l, expr* r, expr_ref& result) { if (str().is_empty(r)) - std::swap(l,r); + std::swap(l, r); + if (str().is_length(r)) + std::swap(l, r); +#if 0 + rational n; + if (str().is_length(l) && m_autil.is_numeral(r, n) && n.is_zero()) { + VERIFY(str().is_length(l, l)); + result = m().mk_eq(l, str().mk_empty(l->get_sort())); + return true; + } +#endif if (!str().is_empty(l)) return false; expr* s = nullptr, *offset = nullptr, *len = nullptr; diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index 77a648202..ed60971b6 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -176,6 +176,8 @@ struct th_rewriter_cfg : public default_rewriter_cfg { // theory dispatch for = SASSERT(num == 2); family_id s_fid = args[0]->get_sort()->get_family_id(); + family_id op_fid = s_fid; + try_mk_eq: if (s_fid == m_a_rw.get_fid()) st = m_a_rw.mk_eq_core(args[0], args[1], result); else if (s_fid == m_bv_rw.get_fid()) @@ -190,6 +192,13 @@ struct th_rewriter_cfg : public default_rewriter_cfg { st = m_seq_rw.mk_eq_core(args[0], args[1], result); if (st != BR_FAILED) return st; + op_fid = s_fid; + if (is_app(args[0])) + op_fid = to_app(args[0])->get_family_id(); + if (op_fid != s_fid) { + s_fid = op_fid; + goto try_mk_eq; + } } if (k == OP_EQ) { SASSERT(num == 2); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 1bde8005d..ec66cdcfd 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -989,7 +989,7 @@ public: } void assign_eh(bool_var v, bool is_true) { - TRACE("arith", tout << mk_pp(ctx().bool_var2expr(v), m) << " " << (is_true?"true":"false") << "\n";); + TRACE("arith", tout << mk_pp(ctx().bool_var2expr(v), m) << " " << (literal(v, !is_true)) << "\n";); m_asserted_atoms.push_back(delayed_atom(v, is_true)); } @@ -2270,7 +2270,7 @@ public: theory_var vv = lp().local_to_external(v); // so maybe better to have them already transformed to external form enode* n1 = get_enode(uv); enode* n2 = get_enode(vv); - TRACE("arith", tout << "add-eq " << mk_pp(n1->get_expr(), m) << " == " << mk_pp(n2->get_expr(), m) << "\n";); + TRACE("arith", tout << "add-eq " << mk_pp(n1->get_expr(), m) << " == " << mk_pp(n2->get_expr(), m) << " " << n1->get_expr_id() << " == " << n2->get_expr_id() << "\n";); if (n1->get_root() == n2->get_root()) return; expr* e1 = n1->get_expr(); @@ -2313,27 +2313,21 @@ public: literal is_bound_implied(lp::lconstraint_kind k, rational const& value, api_bound const& b) const { if ((k == lp::LE || k == lp::LT) && b.get_bound_kind() == lp_api::upper_t && value <= b.get_value()) { - TRACE("arith", tout << "v <= value <= b.get_value() => v <= b.get_value() \n";); return b.get_lit(); } if ((k == lp::GE || k == lp::GT) && b.get_bound_kind() == lp_api::lower_t && b.get_value() <= value) { - TRACE("arith", tout << "b.get_value() <= value <= v => b.get_value() <= v \n";); return b.get_lit(); } if (k == lp::LE && b.get_bound_kind() == lp_api::lower_t && value < b.get_value()) { - TRACE("arith", tout << "v <= value < b.get_value() => v < b.get_value()\n";); return ~b.get_lit(); } if (k == lp::LT && b.get_bound_kind() == lp_api::lower_t && value <= b.get_value()) { - TRACE("arith", tout << "v < value <= b.get_value() => v < b.get_value()\n";); return ~b.get_lit(); } if (k == lp::GE && b.get_bound_kind() == lp_api::upper_t && b.get_value() < value) { - TRACE("arith", tout << "b.get_value() < value <= v => b.get_value() < v\n";); return ~b.get_lit(); } if (k == lp::GT && b.get_bound_kind() == lp_api::upper_t && b.get_value() <= value) { - TRACE("arith", tout << "b.get_value() <= value < v => b.get_value() < v\n";); return ~b.get_lit(); } @@ -3047,7 +3041,7 @@ public: TRACE("arith", for (auto c : m_core) - ctx().display_detailed_literal(tout, c) << "\n"; + ctx().display_detailed_literal(tout << ctx().get_assign_level(c.var()) << " " << c << " ", c) << "\n"; for (auto e : m_eqs) tout << pp(e.first, m) << " = " << pp(e.second, m) << "\n"; tout << " ==> "; @@ -3057,8 +3051,8 @@ public: std::function fn = [&]() { return m.mk_eq(x->get_expr(), y->get_expr()); }; scoped_trace_stream _sts(th, fn); - // parameters are TBD. - // SASSERT(validate_eq(x, y)); + + // SASSERT(validate_eq(x, y)); ctx().assign_eq(x, y, eq_justification(js)); } @@ -3422,13 +3416,22 @@ public: } bool validate_eq(enode* x, enode* y) { - if (params().m_arith_mode == arith_solver_id::AS_NEW_ARITH) return true; + static bool s_validating = false; + static unsigned s_count = 0; + if (s_validating) + return true; + ++s_count; + flet _svalid(s_validating, true); context nctx(m, ctx().get_fparams(), ctx().get_params()); add_background(nctx); nctx.assert_expr(m.mk_not(m.mk_eq(x->get_expr(), y->get_expr()))); cancel_eh eh(m.limit()); scoped_timer timer(1000, &eh); - return l_true != nctx.check(); + lbool r = nctx.check(); + if (r == l_true) { + nctx.display_asserted_formulas(std::cout); + } + return l_true != r; } void add_background(context& nctx) {