From 67c47775140921bf9b9136a0d8b169b1e077cac1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 13 Sep 2019 13:54:51 +0200 Subject: [PATCH] fix #2548 fix #2530 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 2 +- src/math/polynomial/polynomial.cpp | 14 +- src/muz/spacer/spacer_arith_generalizers.cpp | 43 +------ src/nlsat/nlsat_explain.cpp | 42 +++--- src/nlsat/nlsat_params.pyg | 1 + src/nlsat/nlsat_solver.cpp | 129 +++++++++++++++---- src/nlsat/nlsat_solver.h | 7 + src/qe/nlqsat.cpp | 15 ++- src/smt/theory_seq.cpp | 77 ++++++----- src/util/rational.cpp | 45 +++++++ src/util/rational.h | 2 + 11 files changed, 251 insertions(+), 126 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 94a15e7f432..49957a01fe2 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -1902,7 +1902,7 @@ br_status seq_rewriter::mk_re_opt(expr* a, expr_ref& result) { } br_status seq_rewriter::mk_eq_core(expr * l, expr * r, expr_ref & result) { - TRACE("seq", tout << mk_pp(l, m()) << " = " << mk_pp(r, m()) << "\n";); + TRACE("seq", tout << mk_bounded_pp(l, m(), 2) << " = " << mk_bounded_pp(r, m(), 2) << "\n";); expr_ref_vector lhs(m()), rhs(m()), res(m()); bool changed = false; if (!reduce_eq(l, r, lhs, rhs, changed)) { diff --git a/src/math/polynomial/polynomial.cpp b/src/math/polynomial/polynomial.cpp index c8c204620c2..2026df36c03 100644 --- a/src/math/polynomial/polynomial.cpp +++ b/src/math/polynomial/polynomial.cpp @@ -410,8 +410,8 @@ namespace polynomial { proc(out, x); } } + out << ")"; } - out << ")"; } bool is_unit() const { return m_size == 0; } @@ -1576,12 +1576,20 @@ namespace polynomial { display_num_smt2(out, nm, a_i); } else if (nm.is_one(a_i)) { - m_i->display(out, proc); + if (m_i->size() == 1) { + m_i->display_smt2(out, proc); + } + else { + out << "(* "; + m_i->display_smt2(out, proc); + out << ")"; + } } else { out << "(* "; display_num_smt2(out, nm, a_i); - m_i->display(out, proc); + out << " "; + m_i->display_smt2(out, proc); out << ")"; } } diff --git a/src/muz/spacer/spacer_arith_generalizers.cpp b/src/muz/spacer/spacer_arith_generalizers.cpp index 0e0f72558b7..6c09d454e33 100644 --- a/src/muz/spacer/spacer_arith_generalizers.cpp +++ b/src/muz/spacer/spacer_arith_generalizers.cpp @@ -45,48 +45,7 @@ struct limit_denominator_rewriter_cfg : public default_rewriter_cfg { } bool limit_denominator(rational &num) { - rational n, d; - n = numerator(num); - d = denominator(num); - if (d < m_limit) return false; - - /* - Iteratively computes approximation using continuous fraction - decomposition - - p(-1) = 0, p(0) = 1 - p(j) = t(j)*p(j-1) + p(j-2) - - q(-1) = 1, q(0) = 0 - q(j) = t(j)*q(j-1) + q(j-2) - - cf[t1; t2, ..., tr] = p(r) / q(r) for r >= 1 - reference: https://www.math.u-bordeaux.fr/~pjaming/M1/exposes/MA2.pdf - */ - - rational p0(0), p1(1); - rational q0(1), q1(0); - - while (d != rational(0)) { - rational tj(0), rem(0); - rational p2(0), q2(0); - tj = div(n, d); - - q2 = tj * q1 + q0; - p2 = tj * p1 + p0; - if (q2 >= m_limit) { - num = p2 / q2; - return true; - } - rem = n - tj * d; - p0 = p1; - p1 = p2; - q0 = q1; - q1 = q2; - n = d; - d = rem; - } - return false; + return rational::limit_denominator(num, m_limit); } br_status reduce_app(func_decl *f, unsigned num, expr *const *args, diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index 608d4200532..a2da3b31612 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/src/nlsat/nlsat_explain.cpp @@ -1162,18 +1162,21 @@ namespace nlsat { new_lit = m_solver.mk_ineq_literal(new_k, new_factors.size(), new_factors.c_ptr(), new_factors_even.c_ptr()); if (l.sign()) new_lit.neg(); - TRACE("nlsat_simplify_core", tout << "simplified literal:\n"; display(tout, new_lit); tout << "\n";); + TRACE("nlsat_simplify_core", tout << "simplified literal:\n"; display(tout, new_lit); tout << " " << m_solver.value(new_lit) << "\n";); + if (max_var(new_lit) < max) { - // The conflicting core may have redundant literals. - // We should check whether new_lit is true in the current model, and discard it if that is the case - VERIFY(m_solver.value(new_lit) != l_undef); - if (m_solver.value(new_lit) == l_false) + if (m_solver.value(new_lit) == l_true) { + new_lit = l; + } + else { add_literal(new_lit); - new_lit = true_literal; - return; + new_lit = true_literal; + } + } + else { + new_lit = normalize(new_lit, max); + TRACE("nlsat_simplify_core", tout << "simplified literal after normalization:\n"; display(tout, new_lit); tout << " " << m_solver.value(new_lit) << "\n";); } - new_lit = normalize(new_lit, max); - TRACE("nlsat_simplify_core", tout << "simplified literal after normalization:\n"; display(tout, new_lit); tout << "\n";); } else { new_lit = l; @@ -1333,6 +1336,7 @@ namespace nlsat { poly * eq_p = eq->p(0); VERIFY(simplify(C, eq_p, max)); // add equation as an assumption + TRACE("nlsat_simpilfy_core", display(tout << "adding equality as assumption ", literal(eq->bvar(), true)); tout << "\n";); add_literal(literal(eq->bvar(), true)); } } @@ -1511,7 +1515,7 @@ namespace nlsat { result.set(i, ~result[i]); } DEBUG_CODE( - TRACE("nlsat", m_solver.display(tout, result.size(), result.c_ptr()); ); + TRACE("nlsat", m_solver.display(tout, result.size(), result.c_ptr()) << "\n"; ); for (literal l : result) { CTRACE("nlsat", l_true != m_solver.value(l), m_solver.display(tout, l) << " " << m_solver.value(l) << "\n";); SASSERT(l_true == m_solver.value(l)); @@ -1619,12 +1623,12 @@ namespace nlsat { unsigned glb_index = 0, lub_index = 0; scoped_anum lub(m_am), glb(m_am), x_val(m_am); x_val = m_assignment.value(x); + bool glb_valid = false, lub_valid = false; for (unsigned i = 0; i < ps.size(); ++i) { p = ps.get(i); scoped_anum_vector & roots = m_roots_tmp; roots.reset(); m_am.isolate_roots(p, undef_var_assignment(m_assignment, x), roots); - bool glb_valid = false, lub_valid = false; for (auto const& r : roots) { int s = m_am.compare(x_val, r); SASSERT(s != 0); @@ -1632,23 +1636,19 @@ namespace nlsat { if (s < 0 && (!lub_valid || m_am.lt(r, lub))) { lub_index = i; m_am.set(lub, r); + lub_valid = true; } if (s > 0 && (!glb_valid || m_am.lt(glb, r))) { glb_index = i; - m_am.set(glb, r); + m_am.set(glb, r); + glb_valid = true; } - lub_valid |= s < 0; - glb_valid |= s > 0; - } - if (glb_valid) { - ++num_glb; - } - if (lub_valid) { - ++num_lub; + if (s < 0) ++num_lub; + if (s > 0) ++num_glb; } } - TRACE("nlsat_explain", tout << ps << "\n";); + TRACE("nlsat_explain", tout << "glb: " << num_glb << " lub: " << num_lub << "\n" << lub_index << "\n" << glb_index << "\n" << ps << "\n";); if (num_lub == 0) { project_plus_infinity(x, ps); diff --git a/src/nlsat/nlsat_params.pyg b/src/nlsat/nlsat_params.pyg index 0f2e0306952..9bb001d2da8 100644 --- a/src/nlsat/nlsat_params.pyg +++ b/src/nlsat/nlsat_params.pyg @@ -5,6 +5,7 @@ def_module_params('nlsat', params=(max_memory_param(), ('lazy', UINT, 0, "how lazy the solver is."), ('reorder', BOOL, True, "reorder variables."), + ('log_lemmas', BOOL, False, "display lemmas as self-contained SMT formulas"), ('simplify_conflicts', BOOL, True, "simplify conflicts using equalities before resolving them in nlsat solver."), ('minimize_conflicts', BOOL, False, "minimize conflicts"), ('randomize', BOOL, True, "randomize selection of a witness in nlsat."), diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 0193a0f4d5e..312f28572c3 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -156,6 +156,8 @@ namespace nlsat { unsigned m_scope_lvl; + struct bvar_assignment {}; + struct stage {}; struct trail { enum kind { BVAR_ASSIGNMENT, INFEASIBLE_UPDT, NEW_LEVEL, NEW_STAGE, UPDT_EQ }; kind m_kind; @@ -164,9 +166,9 @@ namespace nlsat { interval_set * m_old_set; atom * m_old_eq; }; - trail(bool_var b):m_kind(BVAR_ASSIGNMENT), m_b(b) {} + trail(bool_var b, bvar_assignment):m_kind(BVAR_ASSIGNMENT), m_b(b) {} trail(interval_set * old_set):m_kind(INFEASIBLE_UPDT), m_old_set(old_set) {} - trail(bool stage):m_kind(stage ? NEW_STAGE : NEW_LEVEL) {} + trail(bool s, stage):m_kind(s ? NEW_STAGE : NEW_LEVEL) {} trail(atom * a):m_kind(UPDT_EQ), m_old_eq(a) {} }; svector m_trail; @@ -182,6 +184,7 @@ namespace nlsat { bool m_random_order; unsigned m_random_seed; bool m_inline_vars; + bool m_log_lemmas; unsigned m_max_conflicts; // statistics @@ -240,6 +243,7 @@ namespace nlsat { m_random_order = p.shuffle_vars(); m_random_seed = p.seed(); m_inline_vars = p.inline_vars(); + m_log_lemmas = p.log_lemmas(); m_ism.set_seed(m_random_seed); m_explain.set_simplify_cores(m_simplify_cores); m_explain.set_minimize_cores(min_cores); @@ -730,6 +734,14 @@ namespace nlsat { } }; + void log_lemma(std::ostream& out, clause const& cls) { + display_smt2(out); + out << "(assert (not "; + display_smt2(out, cls) << "))\n"; + display(out << "(echo \"", cls) << "\")\n"; + out << "(check-sat)\n(reset)\n"; + } + clause * mk_clause(unsigned num_lits, literal const * lits, bool learned, _assumption_set a) { SASSERT(num_lits > 0); unsigned cid = m_cid_gen.mk(); @@ -741,6 +753,9 @@ namespace nlsat { TRACE("nlsat_sort", tout << "mk_clause:\n"; display(tout, *cls); tout << "\n";); std::sort(cls->begin(), cls->end(), lit_lt(*this)); TRACE("nlsat_sort", tout << "after sort:\n"; display(tout, *cls); tout << "\n";); + if (learned && m_log_lemmas) { + log_lemma(std::cout, *cls); + } if (learned) m_learned.push_back(cls); else @@ -764,7 +779,7 @@ namespace nlsat { // ----------------------- void save_assign_trail(bool_var b) { - m_trail.push_back(trail(b)); + m_trail.push_back(trail(b, bvar_assignment())); } void save_set_updt_trail(interval_set * old_set) { @@ -776,11 +791,11 @@ namespace nlsat { } void save_new_stage_trail() { - m_trail.push_back(trail(true)); + m_trail.push_back(trail(true, stage())); } void save_new_level_trail() { - m_trail.push_back(trail(false)); + m_trail.push_back(trail(false, stage())); } void undo_bvar_assignment(bool_var b) { @@ -934,8 +949,10 @@ namespace nlsat { \brief Assign literal using the given justification */ void assign(literal l, justification j) { - TRACE("nlsat", tout << "assigning literal: "; display(tout, l); - tout << "\njustification kind: " << j.get_kind() << "\n";); + TRACE("nlsat", + display(tout << "assigning literal: ", l); + display(tout << " <- ", j);); + SASSERT(assigned_value(l) == l_undef); SASSERT(j != null_justification); SASSERT(!j.is_null()); @@ -1086,9 +1103,10 @@ namespace nlsat { switch (j.get_kind()) { case justification::CLAUSE: if (j.get_clause()->assumptions() != nullptr) return; - break; + break; case justification::LAZY: if (j.get_lazy()->num_clauses() > 0) return; + if (j.get_lazy()->num_lits() > 0) return; break; default: break; @@ -1098,8 +1116,10 @@ namespace nlsat { SASSERT(x != null_var); if (m_var2eq[x] != 0 && degree(m_var2eq[x]) <= degree(a)) return; // we only update m_var2eq if the new equality has smaller degree - TRACE("simplify_core", tout << "Saving equality for "; m_display_var(tout, x) << " (x" << x << ") "; - tout << "scope-lvl: " << scope_lvl() << "\n"; display(tout, literal(b, false)) << "\n";); + TRACE("nlsat_simplify_core", tout << "Saving equality for "; m_display_var(tout, x) << " (x" << x << ") "; + tout << "scope-lvl: " << scope_lvl() << "\n"; display(tout, literal(b, false)) << "\n"; + display(tout, j); + ); save_updt_eq_trail(m_var2eq[x]); m_var2eq[x] = a; } @@ -1125,7 +1145,7 @@ namespace nlsat { checkpoint(); if (value(l) == l_false) continue; - TRACE("nlsat_inf_set", tout << "xk: " << m_xk << ", max_var(l): " << max_var(l) << ", l: "; display(tout, l); tout << "\n";); + CTRACE("nlsat", max_var(l) != m_xk, display(tout); tout << "xk: " << m_xk << ", max_var(l): " << max_var(l) << ", l: "; display(tout, l); tout << "\n";); SASSERT(value(l) == l_undef); SASSERT(max_var(l) == m_xk); bool_var b = l.var(); @@ -1195,7 +1215,6 @@ namespace nlsat { bool process_clause(clause const & cls, bool satisfy_learned) { if (is_satisfied(cls)) return true; - TRACE("nlsat", display(tout << "processing clause: ", cls) << "\n";); if (m_xk == null_var) return process_boolean_clause(cls); else @@ -1255,7 +1274,22 @@ namespace nlsat { m_irrational_assignments++; m_assignment.set_core(m_xk, w); } + + + bool is_satisfied() { + if (m_bk == null_bool_var && m_xk >= num_vars()) { + TRACE("nlsat", tout << "found model\n"; display_assignment(tout);); + fix_patch(); + SASSERT(check_satisfied(m_clauses)); + return true; // all variables were assigned, and all clauses were satisfied. + } + else { + return false; + } + } + + /** \brief main procedure */ @@ -1264,8 +1298,11 @@ namespace nlsat { TRACE("nlsat_proof", tout << "ASSERTED\n"; display(tout);); TRACE("nlsat_proof_sk", tout << "ASSERTED\n"; display_abst(tout);); TRACE("nlsat_mathematica", display_mathematica(tout);); + TRACE("nlsat", display_smt2(tout);); m_bk = 0; m_xk = null_var; + m_conflicts = 0; + while (true) { CASSERT("nlsat", check_satisfied()); if (m_xk == null_var) { @@ -1277,22 +1314,18 @@ namespace nlsat { new_stage(); // peek next arith var } TRACE("nlsat_bug", tout << "xk: x" << m_xk << " bk: b" << m_bk << "\n";); - if (m_bk == null_bool_var && m_xk >= num_vars()) { - TRACE("nlsat", tout << "found model\n"; display_assignment(tout);); - fix_patch(); - SASSERT(check_satisfied(m_clauses)); - return l_true; // all variables were assigned, and all clauses were satisfied. + if (is_satisfied()) { + return l_true; } while (true) { - TRACE("nlsat", tout << "processing variable "; + TRACE("nlsat_verbose", tout << "processing variable "; if (m_xk != null_var) { m_display_var(tout, m_xk); tout << " " << m_watches[m_xk].size(); } else { tout << m_bwatches[m_bk].size() << " boolean b" << m_bk; } - tout << "\n"; - ); + tout << "\n";); checkpoint(); clause * conflict_clause; if (m_xk == null_var) @@ -1301,12 +1334,12 @@ namespace nlsat { conflict_clause = process_clauses(m_watches[m_xk]); if (conflict_clause == nullptr) break; - if (!resolve(*conflict_clause)) - return l_false; + if (!resolve(*conflict_clause)) + return l_false; if (m_conflicts >= m_max_conflicts) return l_undef; } - + if (m_xk == null_var) { if (m_bvalues[m_bk] == l_undef) { decide(literal(m_bk, true)); @@ -1319,6 +1352,7 @@ namespace nlsat { } } + lbool search_check() { lbool r = l_undef; while (true) { @@ -1521,6 +1555,7 @@ namespace nlsat { // antecedent must be false in the current arith interpretation SASSERT(value(antecedent) == l_false); if (!is_marked(b)) { + TRACE("nlsat_resolve", tout << max_var(b) << " " << m_xk << "\n";); SASSERT(is_arith_atom(b) && max_var(b) < m_xk); // must be in a previous stage TRACE("nlsat_resolve", tout << "literal is unassigned, but it is false in arithmetic interpretation, adding it to lemma\n";); mark(b); @@ -2692,6 +2727,26 @@ namespace nlsat { display_num_assignment(out); return out; } + + std::ostream& display(std::ostream& out, justification j) const { + switch (j.get_kind()) { + case justification::CLAUSE: + display(out, *j.get_clause()) << "\n"; + break; + case justification::LAZY: { + lazy_justification const& lz = *j.get_lazy(); + display(out, lz.num_lits(), lz.lits()) << "\n"; + for (unsigned i = 0; i < lz.num_clauses(); ++i) { + display(out, lz.clause(i)) << "\n"; + } + break; + } + default: + out << j.get_kind() << "\n"; + break; + } + return out; + } std::ostream& display(std::ostream & out, ineq_atom const & a, display_var_proc const & proc, bool use_star = false) const { unsigned sz = a.size(); @@ -2769,6 +2824,10 @@ namespace nlsat { out << " 0)"; return out; } + + std::ostream& display_smt2(std::ostream & out, root_atom const & a, display_var_proc const & proc) const { + return display(out, a, proc); + } std::ostream& display(std::ostream & out, root_atom const & a, display_var_proc const & proc) const { proc(out, a.x()); @@ -2898,6 +2957,10 @@ namespace nlsat { return display(out, l, m_display_var); } + std::ostream& display_smt2(std::ostream & out, literal l) const { + return display_smt2(out, l, m_display_var); + } + std::ostream& display_mathematica(std::ostream & out, literal l) const { if (l.sign()) { bool_var b = l.var(); @@ -2947,7 +3010,7 @@ namespace nlsat { return out; } - std::ostream& display(std::ostream & out, unsigned num, literal const * ls) { + std::ostream& display(std::ostream & out, unsigned num, literal const * ls) const { return display(out, num, ls, m_display_var); } @@ -3147,7 +3210,7 @@ namespace nlsat { for (clause* c : m_clauses) { display_smt2(out, *c) << "\n"; } - out << "))\n(check-sat)" << std::endl; + out << "))\n" << std::endl; return out; } }; @@ -3346,6 +3409,22 @@ namespace nlsat { return display(out, ls.size(), ls.c_ptr()); } + std::ostream& solver::display_smt2(std::ostream & out, literal l) const { + return m_imp->display_smt2(out, l); + } + + std::ostream& solver::display_smt2(std::ostream & out, unsigned n, literal const* ls) const { + for (unsigned i = 0; i < n; ++i) { + display_smt2(out, ls[i]); + out << " "; + } + return out; + } + + std::ostream& solver::display_smt2(std::ostream & out, literal_vector const& ls) const { + return display_smt2(out, ls.size(), ls.c_ptr()); + } + std::ostream& solver::display(std::ostream & out, var x) const { return m_imp->m_display_var(out, x); } diff --git a/src/nlsat/nlsat_solver.h b/src/nlsat/nlsat_solver.h index 5047012b870..f720e3e487f 100644 --- a/src/nlsat/nlsat_solver.h +++ b/src/nlsat/nlsat_solver.h @@ -245,6 +245,13 @@ namespace nlsat { std::ostream& display(std::ostream & out, atom const& a) const; + std::ostream& display_smt2(std::ostream & out, literal l) const; + + std::ostream& display_smt2(std::ostream & out, unsigned n, literal const* ls) const; + + std::ostream& display_smt2(std::ostream & out, literal_vector const& ls) const; + + /** \brief Display variable */ diff --git a/src/qe/nlqsat.cpp b/src/qe/nlqsat.cpp index 6bb1dfaf8d5..a0084e071c5 100644 --- a/src/qe/nlqsat.cpp +++ b/src/qe/nlqsat.cpp @@ -350,6 +350,16 @@ namespace qe { } } + void display_project(std::ostream& out, nlsat::var v, nlsat::scoped_literal_vector const& r1, nlsat::scoped_literal_vector const& r2) { + for (auto const& kv : s.m_x2t) { + out << "(declare-const x" << kv.m_key << " Real)\n"; + } + s.m_solver.display(out << "(assert (not (exists ((", v) << " Real)) \n"; + s.m_solver.display_smt2(out << "(and ", r1.size(), r1.c_ptr()) << "))))\n"; + s.m_solver.display_smt2(out << "(assert (and ", r2.size(), r2.c_ptr()); out << "))\n"; + out << "(check-sat)\n(reset)\n"; + } + void mbp(nlsat::var_vector const& vars, uint_set const& fvars, clause& result) { // // Also project auxiliary variables from clausification. @@ -370,11 +380,10 @@ namespace qe { // renaming variables. for (unsigned i = vars.size(); i-- > 0;) { new_result.reset(); - TRACE("qe", s.m_solver.display(tout << "project: ", vars[i]) << "\n";); ex.project(vars[i], result.size(), result.c_ptr(), new_result); + TRACE("qe", display_project(tout, vars[i], result, new_result);); + TRACE("qe", display_project(std::cout, vars[i], result, new_result);); result.swap(new_result); - TRACE("qe", s.m_solver.display(tout, vars[i]) << ": "; - s.m_solver.display(tout, result.size(), result.c_ptr()); tout << "\n";); } negate_clause(result); } diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index af81a6e3622..860d0ec9987 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -140,7 +140,6 @@ void theory_seq::solution_map::update(expr* e, expr* r, dependency* d) { value.first = r; value.second = d; m_map.insert(e, value); - // std::cout << mk_pp(e, m) << " -> " << mk_pp(r, m) << "\n"; add_trail(INS, e, r, d); } @@ -225,7 +224,7 @@ void theory_seq::solution_map::pop_scope(unsigned num_scopes) { void theory_seq::solution_map::display(std::ostream& out) const { for (auto const& kv : m_map) { - out << mk_bounded_pp(kv.m_key, m) << " |-> " << mk_bounded_pp(kv.m_value.first, m) << "\n"; + out << mk_bounded_pp(kv.m_key, m, 2) << " |-> " << mk_bounded_pp(kv.m_value.first, m, 2) << "\n"; } } @@ -260,7 +259,7 @@ void theory_seq::exclusion_table::pop_scope(unsigned num_scopes) { void theory_seq::exclusion_table::display(std::ostream& out) const { for (auto const& kv : m_table) { - out << mk_pp(kv.first, m) << " != " << mk_pp(kv.second, m) << "\n"; + out << mk_bounded_pp(kv.first, m, 2) << " != " << mk_bounded_pp(kv.second, m, 2) << "\n"; } } @@ -555,20 +554,20 @@ void theory_seq::branch_unit_variable(dependency* dep, expr* X, expr_ref_vector context& ctx = get_context(); rational lenX; if (!get_length(X, lenX)) { - TRACE("seq", tout << "enforce length on " << mk_pp(X, m) << "\n";); + TRACE("seq", tout << "enforce length on " << mk_bounded_pp(X, m, 2) << "\n";); enforce_length(X); return; } if (lenX > rational(units.size())) { expr_ref le(m_autil.mk_le(mk_len(X), m_autil.mk_int(units.size())), m); - TRACE("seq", tout << "propagate length on " << mk_pp(X, m) << "\n";); + TRACE("seq", tout << "propagate length on " << mk_bounded_pp(X, m, 2) << "\n";); propagate_lit(dep, 0, nullptr, mk_literal(le)); return; } SASSERT(lenX.is_unsigned()); unsigned lX = lenX.get_unsigned(); if (lX == 0) { - TRACE("seq", tout << "set empty length " << mk_pp(X, m) << "\n";); + TRACE("seq", tout << "set empty length " << mk_bounded_pp(X, m, 2) << "\n";); set_empty(X); } else { @@ -2223,17 +2222,29 @@ bool theory_seq::is_solved() { return false; } } - if (false && !m_nqs.empty()) { - TRACE("seq", display_disequation(tout << "(seq.giveup ", m_nqs[0]); tout << " is unsolved)\n";); - IF_VERBOSE(10, display_disequation(verbose_stream() << "(seq.giveup ", m_nqs[0]); verbose_stream() << " is unsolved)\n";); - return false; - } if (!m_ncs.empty()) { TRACE("seq", display_nc(tout << "(seq.giveup ", m_ncs[0]); tout << " is unsolved)\n";); IF_VERBOSE(10, display_nc(verbose_stream() << "(seq.giveup ", m_ncs[0]); verbose_stream() << " is unsolved)\n";); return false; } + context& ctx = get_context(); + for (enode* n : ctx.enodes()) { + expr* e = nullptr; + rational len1, len2; + if (m_util.str.is_length(n->get_owner(), e)) { + VERIFY(get_length(e, len1)); + dependency* dep = nullptr; + expr_ref r = canonize(e, dep); + if (get_length(r, len2)) { + SASSERT(len1 == len2); + } + else { + std::cout << r << "does not have a length\n"; + } + } + } + return true; } @@ -2615,7 +2626,7 @@ bool theory_seq::add_solution(expr* l, expr* r, dependency* deps) { m_rep.update(l, r, deps); enode* n1 = ensure_enode(l); enode* n2 = ensure_enode(r); - TRACE("seq", tout << mk_pp(l, m) << " ==> " << mk_bounded_pp(r, m) << "\n"; display_deps(tout, deps); + TRACE("seq", tout << mk_bounded_pp(l, m, 2) << " ==> " << mk_bounded_pp(r, m, 2) << "\n"; display_deps(tout, deps); tout << (n1->get_root() == n2->get_root()) << "\n";); propagate_eq(deps, n1, n2); return true; @@ -3609,7 +3620,7 @@ bool theory_seq::internalize_term(app* term) { } void theory_seq::add_length(expr* e, expr* l) { - TRACE("seq", tout << get_context().get_scope_level() << " " << mk_pp(e, m) << "\n";); + TRACE("seq", tout << get_context().get_scope_level() << " " << mk_bounded_pp(e, m, 2) << "\n";); SASSERT(!m_length.contains(l)); m_length.push_back(l); m_has_length.insert(e); @@ -3878,7 +3889,7 @@ void theory_seq::display(std::ostream & out) const { } std::ostream& theory_seq::display_nc(std::ostream& out, nc const& nc) const { - out << "not " << mk_pp(nc.contains(), m) << "\n"; + out << "not " << mk_bounded_pp(nc.contains(), m, 2) << "\n"; display_deps(out << " <- ", nc.deps()) << "\n"; return out; } @@ -3891,7 +3902,11 @@ std::ostream& theory_seq::display_equations(std::ostream& out) const { } std::ostream& theory_seq::display_equation(std::ostream& out, eq const& e) const { - out << e.ls() << " = " << e.rs() << " <- \n"; + bool first = true; + for (expr* a : e.ls()) { if (first) first = false; else out << "\n"; out << mk_bounded_pp(a, m, 2); } + out << " = "; + for (expr* a : e.rs()) { if (first) first = false; else out << "\n"; out << mk_bounded_pp(a, m, 2); } + out << " <- \n"; return display_deps(out, e.dep()); } @@ -3914,11 +3929,11 @@ std::ostream& theory_seq::display_disequation(std::ostream& out, ne const& e) co } for (unsigned j = 0; j < e.ls().size(); ++j) { for (expr* t : e.ls(j)) { - out << mk_bounded_pp(t, m) << " "; + out << mk_bounded_pp(t, m, 2) << " "; } out << " != "; for (expr* t : e.rs(j)) { - out << mk_bounded_pp(t, m) << " "; + out << mk_bounded_pp(t, m, 2) << " "; } out << "\n"; } @@ -3933,8 +3948,8 @@ std::ostream& theory_seq::display_deps(std::ostream& out, literal_vector const& smt2_pp_environment_dbg env(m); params_ref p; for (auto const& eq : eqs) { - out << " (= " << mk_bounded_pp(eq.first->get_owner(), m) - << "\n " << mk_bounded_pp(eq.second->get_owner(), m) + out << " (= " << mk_bounded_pp(eq.first->get_owner(), m, 2) + << "\n " << mk_bounded_pp(eq.second->get_owner(), m, 2) << ")\n"; } for (literal l : lits) { @@ -4283,9 +4298,9 @@ bool theory_seq::can_propagate() { expr_ref theory_seq::canonize(expr* e, dependency*& eqs) { expr_ref result = expand(e, eqs); - TRACE("seq", tout << mk_pp(e, m) << " expands to\n" << result << "\n";); + TRACE("seq", tout << mk_bounded_pp(e, m, 2) << " expands to\n" << mk_bounded_pp(result, m, 2) << "\n";); m_rewrite(result); - TRACE("seq", tout << mk_pp(e, m) << " rewrites to\n" << result << "\n";); + TRACE("seq", tout << mk_bounded_pp(e, m, 2) << " rewrites to\n" << mk_bounded_pp(result, m, 2) << "\n";); return result; } @@ -4436,7 +4451,7 @@ expr_ref theory_seq::expand1(expr* e0, dependency*& eqs) { case l_undef: result = e; m_reset_cache = true; - TRACE("seq", tout << "undef: " << result << "\n"; + TRACE("seq", tout << "undef: " << mk_bounded_pp(result, m, 2) << "\n"; tout << lit << "@ level: " << ctx.get_scope_level() << "\n";); break; } @@ -4444,9 +4459,9 @@ expr_ref theory_seq::expand1(expr* e0, dependency*& eqs) { } else if (m_util.str.is_itos(e, e1)) { rational val; - TRACE("seq", tout << mk_pp(e, m) << "\n";); + TRACE("seq", tout << mk_bounded_pp(e, m, 2) << "\n";); if (get_num_value(e1, val)) { - TRACE("seq", tout << mk_pp(e, m) << " -> " << val << "\n";); + TRACE("seq", tout << mk_bounded_pp(e, m, 2) << " -> " << val << "\n";); expr_ref num(m), res(m); num = m_autil.mk_numeral(val, true); if (!ctx.e_internalized(num)) { @@ -4536,7 +4551,7 @@ void theory_seq::enque_axiom(expr* e) { } void theory_seq::deque_axiom(expr* n) { - TRACE("seq", tout << "deque: " << mk_pp(n, m) << "\n";); + TRACE("seq", tout << "deque: " << mk_bounded_pp(n, m, 2) << "\n";); if (m_util.str.is_length(n)) { add_length_axiom(n); } @@ -5141,7 +5156,7 @@ this translates to: void theory_seq::add_extract_axiom(expr* e) { - TRACE("seq", tout << mk_pp(e, m) << "\n";); + TRACE("seq", tout << mk_bounded_pp(e, m, 2) << "\n";); expr* s = nullptr, *i = nullptr, *l = nullptr; VERIFY(m_util.str.is_extract(e, s, i, l)); if (is_tail(s, i, l)) { @@ -5247,7 +5262,7 @@ bool theory_seq::is_extract_suffix(expr* s, expr* i, expr* l) { l < 0 => e = empty */ void theory_seq::add_extract_prefix_axiom(expr* e, expr* s, expr* l) { - TRACE("seq", tout << mk_pp(e, m) << " " << mk_pp(s, m) << " " << mk_pp(l, m) << "\n";); + TRACE("seq", tout << mk_bounded_pp(e, m, 2) << " " << mk_bounded_pp(s, m, 2) << " " << mk_bounded_pp(l, m, 2) << "\n";); expr_ref le = mk_len(e); expr_ref ls = mk_len(s); expr_ref ls_minus_l(mk_sub(ls, l), m); @@ -5362,7 +5377,7 @@ void theory_seq::add_nth_axiom(expr* e) { lit => s = (nth s 0) ++ (nth s 1) ++ ... ++ (nth s idx) ++ (tail s idx) */ void theory_seq::ensure_nth(literal lit, expr* s, expr* idx) { - TRACE("seq", tout << "ensure-nth: " << lit << " " << mk_pp(s, m) << " " << mk_pp(idx, m) << "\n";); + TRACE("seq", tout << "ensure-nth: " << lit << " " << mk_bounded_pp(s, m, 2) << " " << mk_bounded_pp(idx, m, 2) << "\n";); rational r; SASSERT(get_context().get_assignment(lit) == l_true); VERIFY(m_autil.is_numeral(idx, r) && r.is_unsigned()); @@ -5587,7 +5602,7 @@ bool theory_seq::propagate_eq(dependency* deps, literal_vector const& _lits, exp if (!lits.empty()) { ctx.display_literals_verbose(tout, lits) << "\n"; }); TRACE("seq", - tout << "assert: " << mk_bounded_pp(e1, m) << " = " << mk_bounded_pp(e2, m) << " <- \n"; + tout << "assert: " << mk_bounded_pp(e1, m, 2) << " = " << mk_bounded_pp(e2, m, 2) << " <- \n"; tout << lits << "\n";); justification* js = @@ -5806,7 +5821,7 @@ void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) { } m_exclude.update(e1, e2); expr_ref eq(m.mk_eq(e1, e2), m); - TRACE("seq", tout << "new disequality " << get_context().get_scope_level() << ": " << eq << "\n";); + TRACE("seq", tout << "new disequality " << get_context().get_scope_level() << ": " << mk_bounded_pp(eq, m, 2) << "\n";); m_rewrite(eq); if (!m.is_false(eq)) { literal lit = mk_eq(e1, e2, false); @@ -6207,7 +6222,7 @@ bool theory_seq::canonizes(bool sign, expr* e) { context& ctx = get_context(); dependency* deps = nullptr; expr_ref cont = canonize(e, deps); - TRACE("seq", tout << mk_pp(e, m) << " -> " << cont << "\n"; + TRACE("seq", tout << mk_bounded_pp(e, m, 2) << " -> " << mk_bounded_pp(cont, m, 2) << "\n"; if (deps) display_deps(tout, deps);); if ((m.is_true(cont) && !sign) || (m.is_false(cont) && sign)) { diff --git a/src/util/rational.cpp b/src/util/rational.cpp index 10268d98adf..dcbf09969d8 100644 --- a/src/util/rational.cpp +++ b/src/util/rational.cpp @@ -85,3 +85,48 @@ void rational::finalize() { DEALLOC_MUTEX(g_powers_of_two); } +bool rational::limit_denominator(rational &num, rational const& limit) { + rational n, d; + n = numerator(num); + d = denominator(num); + if (d < limit) return false; + + /* + Iteratively computes approximation using continuous fraction + decomposition + + p(-1) = 0, p(0) = 1 + p(j) = t(j)*p(j-1) + p(j-2) + + q(-1) = 1, q(0) = 0 + q(j) = t(j)*q(j-1) + q(j-2) + + cf[t1; t2, ..., tr] = p(r) / q(r) for r >= 1 + reference: https://www.math.u-bordeaux.fr/~pjaming/M1/exposes/MA2.pdf + */ + + rational p0(0), p1(1); + rational q0(1), q1(0); + + while (!d.is_zero()) { + rational tj(0), rem(0); + rational p2(0), q2(0); + tj = div(n, d); + + q2 = tj * q1 + q0; + p2 = tj * p1 + p0; + if (q2 >= limit) { + num = p2/q2; + return true; + } + rem = n - tj * d; + p0 = p1; + p1 = p2; + q0 = q1; + q1 = q2; + n = d; + d = rem; + } + return false; +} + diff --git a/src/util/rational.h b/src/util/rational.h index f343ee019be..a158639badf 100644 --- a/src/util/rational.h +++ b/src/util/rational.h @@ -421,6 +421,8 @@ class rational { } return num_bits; } + + static bool limit_denominator(rational &num, rational const& limit); }; inline bool operator!=(rational const & r1, rational const & r2) {