diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h index 08fd36505..d1a4be21c 100644 --- a/src/math/lp/lp_settings.h +++ b/src/math/lp/lp_settings.h @@ -128,8 +128,12 @@ struct statistics { unsigned m_grobner_conflicts; unsigned m_offset_eqs; unsigned m_fixed_eqs; + ::statistics m_st; statistics() { reset(); } - void reset() { memset(this, 0, sizeof(*this)); } + void reset() { + memset(this, 0, sizeof(*this)); + m_st.reset(); + } void collect_statistics(::statistics& st) const { st.update("arith-factorizations", m_num_factorizations); st.update("arith-make-feasible", m_make_feasible); @@ -157,7 +161,7 @@ struct statistics { st.update("arith-nla-lemmas", m_nla_lemmas); st.update("arith-nra-calls", m_nra_calls); st.update("arith-bounds-improvements", m_nla_bounds_improvements); - + st.copy(m_st); } }; diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp index 4c1b2b3ee..be4395f0e 100644 --- a/src/math/lp/nra_solver.cpp +++ b/src/math/lp/nra_solver.cpp @@ -34,7 +34,7 @@ struct solver::imp { scoped_ptr m_values; // values provided by LRA solver scoped_ptr m_tmp1, m_tmp2; nla::core& m_nla_core; - + imp(lp::lar_solver& s, reslimit& lim, params_ref const& p, nla::core& nla_core): lra(s), m_limit(lim), @@ -180,6 +180,7 @@ struct solver::imp { } lbool r = l_undef; + statistics& st = m_nla_core.lp_settings().stats().m_st; try { r = m_nlsat->check(); } @@ -188,9 +189,11 @@ struct solver::imp { r = l_undef; } else { + m_nlsat->collect_statistics(st); throw; } } + m_nlsat->collect_statistics(st); TRACE("nra", m_nlsat->display(tout << r << "\n"); display(tout); @@ -234,6 +237,7 @@ struct solver::imp { return r; } + void add_monic_eq_bound(mon_eq const& m) { if (!lra.column_has_lower_bound(m.var()) && !lra.column_has_upper_bound(m.var())) @@ -374,6 +378,7 @@ struct solver::imp { } lbool r = l_undef; + statistics& st = m_nla_core.lp_settings().stats().m_st; try { r = m_nlsat->check(); } @@ -382,9 +387,11 @@ struct solver::imp { r = l_undef; } else { + m_nlsat->collect_statistics(st); throw; } } + m_nlsat->collect_statistics(st); switch (r) { case l_true: @@ -665,7 +672,7 @@ nlsat::anum_manager& solver::am() { scoped_anum& solver::tmp1() { return m_imp->tmp1(); } scoped_anum& solver::tmp2() { return m_imp->tmp2(); } - + void solver::updt_params(params_ref& p) { m_imp->updt_params(p); diff --git a/src/math/polynomial/algebraic_numbers.cpp b/src/math/polynomial/algebraic_numbers.cpp index a10e0dc98..b546df706 100644 --- a/src/math/polynomial/algebraic_numbers.cpp +++ b/src/math/polynomial/algebraic_numbers.cpp @@ -2594,27 +2594,28 @@ namespace algebraic_numbers { void int_lt(numeral const & a, numeral & b) { scoped_mpz v(qm()); + if (!a.is_basic()) + refine_until_prec(const_cast(a), 1); if (a.is_basic()) { qm().floor(basic_value(a), v); qm().dec(v); } - else { - refine_until_prec(const_cast(a), 1); - bqm().floor(qm(), lower(a.to_algebraic()), v); - } + else + bqm().floor(qm(), lower(a.to_algebraic()), v); m_wrapper.set(b, v); } void int_gt(numeral const & a, numeral & b) { scoped_mpz v(qm()); + if (!a.is_basic()) + refine_until_prec(const_cast(a), 1); if (a.is_basic()) { qm().ceil(basic_value(a), v); qm().inc(v); } - else { - refine_until_prec(const_cast(a), 1); + else bqm().ceil(qm(), upper(a.to_algebraic()), v); - } + m_wrapper.set(b, v); } diff --git a/src/math/polynomial/polynomial.cpp b/src/math/polynomial/polynomial.cpp index 97f0e25e5..74c5e05d7 100644 --- a/src/math/polynomial/polynomial.cpp +++ b/src/math/polynomial/polynomial.cpp @@ -2504,30 +2504,139 @@ namespace polynomial { return p; } - void gcd_simplify(polynomial * p) { - if (m_manager.finite()) return; + void gcd_simplify(polynomial_ref& p, manager::ineq_type t) { auto& m = m_manager.m(); unsigned sz = p->size(); if (sz == 0) return; unsigned g = 0; - for (unsigned i = 0; i < sz; i++) { + for (unsigned i = 0; i < sz; i++) { if (!m.is_int(p->a(i))) { + gcd_simplify_slow(p, t); return; } + if (t != EQ && is_unit(p->m(i))) + continue; int j = m.get_int(p->a(i)); - if (j == INT_MIN || j == 1 || j == -1) + if (j == INT_MIN) { + gcd_simplify_slow(p, t); + return; + } + if (j == 1 || j == -1) return; g = u_gcd(abs(j), g); if (g == 1) return; } - scoped_mpz r(m), gg(m); + scoped_mpz gg(m); m.set(gg, g); - for (unsigned i = 0; i < sz; ++i) { - m.div_gcd(p->a(i), gg, r); - m.set(p->a(i), r); + apply_gcd_simplify(gg, p, t); + } + + void apply_gcd_simplify(mpz & g, polynomial_ref& p, manager::ineq_type t) { + + auto& m = m_manager.m(); + +#if 0 + m.display(verbose_stream() << "gcd ", g); + p->display(verbose_stream() << "\n", m_manager, false); + char const* tt = ""; + switch (t) { + case ineq_type::GT: tt = ">"; break; + case ineq_type::LT: tt = "<"; break; + case ineq_type::EQ: tt = "="; break; } + verbose_stream() << " " << tt << " 0\n ->\n"; +#endif + scoped_mpz r(m); + unsigned sz = p->size(); + m_som_buffer.reset(); + for (unsigned i = 0; i < sz; ++i) { + if (t != EQ && is_unit(p->m(i))) { + scoped_mpz one(m); + m.set(one, 1); + if (t == GT) { + // p - 2 - 1 >= 0 + // p div 2 + floor((-2 - 1 ) / 2) >= 0 + // p div 2 + floor(-3 / 2) >= 0 + // p div 2 - 2 >= 0 + // p div 2 - 1 > 0 + // + // p + k > 0 + // p + k - 1 >= 0 + // p div g + (k - 1) div g >= 0 + // p div g + (k - 1) div g + 1 > 0 + m.sub(p->a(i), one, r); + bool is_neg = m.is_neg(r); + if (is_neg) { + m.neg(r); + m.add(r, g, r); + m.sub(r, one, r); + m.div_gcd(r, g, r); + m.neg(r); + } + else { + m.div_gcd(r, g, r); + } + m.add(r, one, r); + } + else { + // p + k < 0 + // p + k + 1 <= 0 + // p div g + (k + 1 + g - 1) div g <= 0 + // p div g + (k + 1 + g - 1) div g - 1 < 0 + + m.add(p->a(i), one, r); + bool is_neg = m.is_neg(r); + + if (is_neg) { + // p - k <= 0 + // p <= k + // p div g <= k div g + // p div g - k div g <= 0 + // p div g - k div g - 1 < 0 + m.neg(r); + m.div_gcd(r, g, r); + m.neg(r); + m.sub(r, one, r); + } + else { + m.div_gcd(p->a(i), g, r); + m.add(p->a(i), g, r); + m.div_gcd(r, g, r); + m.sub(r, one, r); + } + + } + } + else { + m.div_gcd(p->a(i), g, r); + } + if (!m.is_zero(r)) + m_som_buffer.add(r, p->m(i)); + } + p = m_som_buffer.mk(); + + // p->display(verbose_stream(), m_manager, false); + // verbose_stream() << " " << tt << " 0\n"; + } + + void gcd_simplify_slow(polynomial_ref& p, manager::ineq_type t) { + auto& m = m_manager.m(); + unsigned sz = p->size(); + scoped_mpz g(m); + m.set(g, 0); + for (unsigned i = 0; i < sz; i++) { + auto const& a = p->a(i); + if (m.is_one(a) || m.is_minus_one(a)) + return; + if (t != EQ && is_unit(p->m(i))) + continue; + m.gcd(a, g, g); + if (m.is_one(g)) + return; + } + apply_gcd_simplify(g, p, t); } polynomial * mk_zero() { @@ -6087,9 +6196,11 @@ namespace polynomial { } return false; } - if (!m_manager.ge(a1, a2)) - return false; - ++i, ++j; + if (m_manager.eq(a1, a2) || (m1->is_square() && m_manager.ge(a1, a2))) { + ++i, ++j; + continue; + } + return false; } return i == sz1 && j == sz2; } @@ -6971,8 +7082,8 @@ namespace polynomial { return m_imp->hash(p); } - void manager::gcd_simplify(polynomial * p) { - m_imp->gcd_simplify(p); + void manager::gcd_simplify(polynomial_ref& p, ineq_type t) { + m_imp->gcd_simplify(p, t); } polynomial * manager::coeff(polynomial const * p, var x, unsigned k) { diff --git a/src/math/polynomial/polynomial.h b/src/math/polynomial/polynomial.h index 48fe5ffeb..5774e6e13 100644 --- a/src/math/polynomial/polynomial.h +++ b/src/math/polynomial/polynomial.h @@ -285,7 +285,8 @@ namespace polynomial { /** \brief Normalize coefficients by dividing by their gcd */ - void gcd_simplify(polynomial* p); + enum ineq_type { EQ, LT, GT }; + void gcd_simplify(polynomial_ref& p, ineq_type t); /** \brief Return true if \c m is the unit monomial. diff --git a/src/math/polynomial/polynomial_cache.cpp b/src/math/polynomial/polynomial_cache.cpp index 9f5f014e4..d5953243c 100644 --- a/src/math/polynomial/polynomial_cache.cpp +++ b/src/math/polynomial/polynomial_cache.cpp @@ -117,20 +117,14 @@ namespace polynomial { } void reset_psc_chain_cache() { - psc_chain_cache::iterator it = m_psc_chain_cache.begin(); - psc_chain_cache::iterator end = m_psc_chain_cache.end(); - for (; it != end; ++it) { - del_psc_chain_entry(*it); - } + for (auto & k : m_psc_chain_cache) + del_psc_chain_entry(k); m_psc_chain_cache.reset(); } void reset_factor_cache() { - factor_cache::iterator it = m_factor_cache.begin(); - factor_cache::iterator end = m_factor_cache.end(); - for (; it != end; ++it) { - del_factor_entry(*it); - } + for (auto & e : m_factor_cache) + del_factor_entry(e); m_factor_cache.reset(); } @@ -139,7 +133,6 @@ namespace polynomial { polynomial * mk_unique(polynomial * p) { if (m_in_cache.get(pid(p), false)) return p; - // m.gcd_simplify(p); polynomial * p_prime = m_poly_table.insert_if_not_there(p); if (p == p_prime) { m_cached_polys.push_back(p_prime); diff --git a/src/nlsat/CMakeLists.txt b/src/nlsat/CMakeLists.txt index d0c1379e5..cd073f0d5 100644 --- a/src/nlsat/CMakeLists.txt +++ b/src/nlsat/CMakeLists.txt @@ -4,6 +4,7 @@ z3_add_component(nlsat nlsat_evaluator.cpp nlsat_explain.cpp nlsat_interval_set.cpp + nlsat_simplify.cpp nlsat_solver.cpp nlsat_types.cpp COMPONENT_DEPENDENCIES diff --git a/src/nlsat/nlsat_simplify.cpp b/src/nlsat/nlsat_simplify.cpp new file mode 100644 index 000000000..8148d721f --- /dev/null +++ b/src/nlsat/nlsat_simplify.cpp @@ -0,0 +1,824 @@ +#include "nlsat/nlsat_simplify.h" +#include "nlsat/nlsat_solver.h" +#include "nlsat/nlsat_scoped_literal_vector.h" +#include "util/dependency.h" +#include "util/map.h" + +namespace nlsat { + + struct simplify::imp { + + solver& s; + atom_vector& m_atoms; + clause_vector& m_clauses, m_learned; + pmanager& m_pm; + literal_vector m_lemma; + vector> m_var_occurs; + + + imp(solver& s, atom_vector& atoms, clause_vector& clauses, clause_vector& learned, pmanager& pm): + s(s), + m_atoms(atoms), + m_clauses(clauses), + m_learned(learned), + m_pm(pm) {} + + void operator()() { + + // for now just remove all learned clauses. + // TODO; check if main clauses are subsumed by learned, + // then promote learned to main. + for (auto c : m_learned) + s.del_clause(c); + m_learned.reset(); + + IF_VERBOSE(3, s.display(verbose_stream() << "before\n")); + unsigned sz = m_clauses.size(); + while (true) { + + subsumption_simplify(); + + while (elim_uncnstr()) + ; + + simplify_literals(); + + while (fm()) + ; + + if (m_clauses.size() >= sz) + break; + + split_factors(); + + sz = m_clauses.size(); + } + + IF_VERBOSE(3, s.display(verbose_stream() << "after\n")); + } + + // + // Apply gcd simplification to literals + // + void simplify_literals() { + u_map b2l; + scoped_literal_vector lits(s); + polynomial_ref p(m_pm); + ptr_buffer ps; + buffer is_even; + unsigned num_atoms = m_atoms.size(); + for (unsigned j = 0; j < num_atoms; ++j) { + atom* a1 = m_atoms[j]; + if (a1 && a1->is_ineq_atom()) { + ineq_atom const& a = *to_ineq_atom(a1); + ps.reset(); + is_even.reset(); + for (unsigned i = 0; i < a.size(); ++i) { + p = a.p(i); + ps.push_back(p); + is_even.push_back(a.is_even(i)); + } + literal l = s.mk_ineq_literal(a.get_kind(), ps.size(), ps.data(), is_even.data(), true); + if (l == null_literal) + continue; + lits.push_back(l); + if (a.m_bool_var != l.var()) { + IF_VERBOSE(3, s.display(verbose_stream() << "simplify ", a) << " -> "; + s.display(verbose_stream(), l) << "\n"); + b2l.insert(a.m_bool_var, l); + } + } + } + update_clauses(b2l); + } + + void update_clauses(u_map const& b2l) { + bool is_sat = true; + literal_vector lits; + unsigned n = m_clauses.size(); + + for (unsigned i = 0; i < n; ++i) { + clause* c = m_clauses[i]; + lits.reset(); + bool changed = false; + bool is_tautology = false; + for (literal l : *c) { + literal lit = null_literal; + if (b2l.find(l.var(), lit)) { + lit = l.sign() ? ~lit : lit; + if (lit == true_literal) + is_tautology = true; + else if (lit != false_literal) + lits.push_back(lit); + changed = true; + } + else + lits.push_back(l); + } + if (changed) { + c->set_removed(); + if (is_tautology) + continue; + s.mk_clause(lits.size(), lits.data(), c->is_learned(), c->assumptions()); + } + } + cleanup_removed(); + } + + // + // Replace unit literals p*q > 0 by clauses. + // + void split_factors() { + auto sz = m_clauses.size(); + for (unsigned i = 0; i < sz; ++i) { + auto& c = *m_clauses[i]; + if (c.size() != 1) + continue; + auto lit = c[0]; + auto a1 = m_atoms[lit.var()]; + if (!a1) + continue; + auto& a = *to_ineq_atom(a1); + if (a.size() != 2) + continue; + + auto* p = a.p(0); + auto* q = a.p(1); + auto is_evenp = a.is_even(0); + auto is_evenq = a.is_even(1); + + auto asum = c.assumptions(); + literal lits[2]; + clause* c1 = nullptr, * c2 = nullptr; + + c.set_removed(); + s.inc_simplify(); + switch (a.get_kind()) { + case atom::EQ: { + auto l1 = s.mk_ineq_literal(atom::EQ, 1, &p, &is_evenp, false); + auto l2 = s.mk_ineq_literal(atom::EQ, 1, &q, &is_evenq, false); + if (lit.sign()) { + lits[0] = ~l1; + c1 = s.mk_clause(1, lits, false, asum); + lits[0] = ~l2; + c2 = s.mk_clause(1, lits, false, asum); + } + else { + lits[0] = l1; + lits[1] = l2; + c1 = s.mk_clause(2, lits, false, asum); + } + break; + } + case atom::LT: { + auto pgt = s.mk_ineq_literal(atom::GT, 1, &p, &is_evenp, false); + auto plt = s.mk_ineq_literal(atom::LT, 1, &p, &is_evenp, false); + auto qgt = s.mk_ineq_literal(atom::GT, 1, &q, &is_evenq, false); + auto qlt = s.mk_ineq_literal(atom::LT, 1, &q, &is_evenq, false); + if (lit.sign()) { + // p*q >= 0 <=> (p < 0 => q <= 0) & (q < 0 => p <= 0) + // (!(p < 0) or !(q > 0)) & (!(q < 0) or !(p > 0)) + + lits[0] = ~plt; + lits[1] = ~qgt; + c1 = s.mk_clause(2, lits, false, asum); + lits[0] = ~qlt; + lits[1] = ~pgt; + c2 = s.mk_clause(2, lits, false, asum); + } + else { + // p*q < 0 + // (p > 0 & q < 0) or (q > 0 & p < 0) + // (p > 0 or q > 0) and (p < 0 or q < 0) + + lits[0] = pgt; + lits[1] = qgt; + c1 = s.mk_clause(2, lits, false, asum); + lits[0] = plt; + lits[1] = qlt; + c2 = s.mk_clause(2, lits, false, asum); + } + break; + } + case atom::GT: { + auto pgt = s.mk_ineq_literal(atom::GT, 1, &p, &is_evenp, false); + auto plt = s.mk_ineq_literal(atom::LT, 1, &p, &is_evenp, false); + auto qgt = s.mk_ineq_literal(atom::GT, 1, &q, &is_evenq, false); + auto qlt = s.mk_ineq_literal(atom::LT, 1, &q, &is_evenq, false); + if (lit.sign()) { + // p*q <= 0 + // (p > 0 => q <= 0) & (p < 0 => q >= 0) + // (!(p > 0) or !(q > 0)) & (!(p < 0) or !(q < 0)) + + lits[0] = ~pgt; + lits[1] = ~qgt; + c1 = s.mk_clause(2, lits, false, asum); + lits[0] = ~qlt; + lits[1] = ~plt; + c2 = s.mk_clause(2, lits, false, asum); + } + else { + // p*q > 0 + // (p > 0 or q < 0) & (p < 0 or q > 0) + lits[0] = plt; + lits[1] = qgt; + c1 = s.mk_clause(2, lits, false, asum); + lits[0] = qlt; + lits[1] = pgt; + c2 = s.mk_clause(2, lits, false, asum); + } + break; + } + } + IF_VERBOSE(3, + s.display(verbose_stream(), c) << " ->\n"; + if (c1) s.display(verbose_stream(), *c1) << "\n"; + if (c2) s.display(verbose_stream(), *c2) << "\n"); + } + cleanup_removed(); + } + + bool elim_uncnstr() { + // compute variable occurrences + if (any_of(m_clauses, [&](clause* c) { return s.has_root_atom(*c); })) + return false; + compute_occurs(); + // for each variable occurrence, figure out if it is unconstrained. + bool has_removed = false; + for (unsigned v = m_var_occurs.size(); v-- > 0; ) { + auto& clauses = m_var_occurs[v]; + if (clauses.size() != 1) + continue; + auto& c = *clauses[0]; + if (c.is_removed()) + continue; + if (!is_unconstrained(v, c)) + continue; + s.inc_simplify(); + c.set_removed(); + has_removed = true; + } + cleanup_removed(); + + return has_removed; + } + + bool is_unconstrained(var x, clause& c) { + poly* p; + polynomial_ref A(m_pm), B(m_pm); + for (auto lit : c) { + bool_var b = lit.var(); + if (!m_atoms[b]) + continue; + auto& a = *to_ineq_atom(m_atoms[b]); + if (!is_single_poly(a, p)) + continue; + + if (1 != m_pm.degree(p, x)) + continue; + + A = m_pm.coeff(p, x, 1, B); + + if (a.is_eq() && !lit.sign()) { + // A*x + B = 0 + if (s.is_int(x) && is_unit(A)) { + s.add_bound(bound_constraint(x, A, B, false, nullptr)); + return true; + } + + if (!s.is_int(x) && m_pm.is_const(A)) { + s.add_bound(bound_constraint(x, A, B, false, nullptr)); + return true; + } + } + // TODO: add other cases for LT and GT atoms + } + return false; + } + + void compute_occurs() { + m_var_occurs.reset(); + for (auto c : m_clauses) + compute_occurs(*c); + } + + void compute_occurs(clause& c) { + var_vector vars; + m_pm.begin_vars_incremental(); + for (auto lit : c) { + bool_var b = lit.var(); + atom* a = m_atoms[b]; + if (!a) + continue; + if (a->is_ineq_atom()) { + auto sz = to_ineq_atom(a)->size(); + for (unsigned i = 0; i < sz; ++i) { + auto* p = to_ineq_atom(a)->p(i); + m_pm.vars_incremental(p, vars); + } + } + } + m_pm.end_vars_incremental(vars); + unsigned h = 0; + for (auto v : vars) { + m_var_occurs.reserve(v + 1); + m_var_occurs[v].push_back(&c); + h |= (1ul << (v % 32ul)); + } + c.set_var_hash(h); + } + + bool cleanup_removed() { + unsigned j = 0, sz = m_clauses.size(); + for (unsigned i = 0; i < sz; ++i) { + auto c = m_clauses[i]; + if (c->is_removed()) + s.del_clause(c); + else + m_clauses[j++] = c; + } + m_clauses.shrink(j); + return j < sz; + } + + bool unit_subsumption_simplify(clause& src, clause& c) { + if (src.size() != 1) + return false; + auto u = src[0]; + for (auto lit : c) { + if (subsumes(u, ~lit)) { + + literal_vector lits; + for (auto lit2 : c) + if (lit2 != lit) + lits.push_back(lit2); + if (lits.empty()) + return false; + auto a = s.join(c.assumptions(), src.assumptions()); + auto cls = s.mk_clause(lits.size(), lits.data(), false, a); + if (cls) + compute_occurs(*cls); + return true; + } + } + return false; + } + + // + // Subsumption simplification + // + // Remove D if C subsumes D + // + // Unit subsumption resolution + // u is a unit literal (lit or C) is a clause + // u => ~lit, then simplify (lit or C) to C + // + void subsumption_simplify() { + compute_occurs(); + for (unsigned v = m_var_occurs.size(); v-- > 0; ) { + auto& clauses = m_var_occurs[v]; + unsigned sz = clauses.size(); + for (unsigned i = 0; i < sz; ++i) { + auto c = clauses[i]; + if (c->is_marked() || c->is_removed()) + continue; + c->mark(); + for (unsigned j = 0; j < sz; ++j) { + auto c2 = clauses[j]; + if (c == c2 || c2->is_removed()) + continue; + if (subsumes(*c, *c2) || unit_subsumption_simplify(*c, *c2)) { + IF_VERBOSE(3, s.display(verbose_stream() << "subsumes ", *c); + s.display(verbose_stream() << " ", *c2) << "\n"); + s.inc_simplify(); + c2->set_removed(); + } + } + } + } + for (auto c : m_clauses) + c->unmark(); + + cleanup_removed(); + } + + // does c1 subsume c2? + bool subsumes(clause const& c1, clause const& c2) { + if (c1.size() > c2.size()) + return false; + if ((c1.var_hash() & c2.var_hash()) != c1.var_hash()) + return false; + for (auto lit1 : c1) { + if (!any_of(c2, [&](auto lit2) { return subsumes(lit1, lit2); })) + return false; + } + return true; + } + + bool subsumes(literal lit1, literal lit2) { + if (lit1 == lit2) + return true; + + atom* a1 = m_atoms[lit1.var()]; + atom* a2 = m_atoms[lit2.var()]; + if (!a1 || !a2) + return false; + + // use m_pm.ge(p1, p2) + // whenever lit1 = p1 < 0, lit2 = p2 < 0 + // or lit1 = p1 < 0, lit2 = !(p2 > 0) + // or lit1 = !(p1 > 0), lit2 = !(p2 > 0) + // use m_pm.ge(p2, p1) + // whenever lit1 = p1 > 0, lit2 = p2 > 0 + // or lit1 = !(p1 < 0), lit2 = !(p2 < 0) + // or lit1 = p1 > 0, lit2 = !(p2 < 0) + // or lit1 = !(p1 > 0), lit2 = p2 < 0 + // + if (a1->is_ineq_atom() && a2->is_ineq_atom()) { + auto& i1 = *to_ineq_atom(a1); + auto& i2 = *to_ineq_atom(a2); + auto is_lt1 = !lit1.sign() && a1->get_kind() == atom::kind::LT; + auto is_le1 = lit1.sign() && a1->get_kind() == atom::kind::GT; + auto is_gt1 = !lit1.sign() && a1->get_kind() == atom::kind::GT; + auto is_ge1 = lit1.sign() && a1->get_kind() == atom::kind::LT; + + auto is_lt2 = !lit2.sign() && a2->get_kind() == atom::kind::LT; + auto is_le2 = lit2.sign() && a2->get_kind() == atom::kind::GT; + auto is_gt2 = !lit2.sign() && a2->get_kind() == atom::kind::GT; + auto is_ge2 = lit2.sign() && a2->get_kind() == atom::kind::LT; + + auto check_ge = (is_lt1 && (is_lt2 || is_le2)) || (is_le1 && is_le2); + auto check_le = (is_gt1 && (is_gt2 || is_ge2)) || (is_ge1 && is_ge2); + + if (i1.size() != i2.size()) + ; + else if (check_ge) { + for (unsigned i = 0; i < i1.size(); ++i) + if (!m_pm.ge(i1.p(i), i2.p(i))) + return false; + return true; + } + else if (check_le) { + for (unsigned i = 0; i < i1.size(); ++i) + if (!m_pm.ge(i2.p(i), i1.p(i))) + return false; + return true; + } + } + return false; + } + + // +// Fourier Motzkin elimination +// + + bool fm() { + if (any_of(m_clauses, [&](clause* c) { return s.has_root_atom(*c); })) + return false; + compute_occurs(); + + for (unsigned v = m_var_occurs.size(); v-- > 0; ) + apply_fm(v, m_var_occurs[v]); + + return cleanup_removed(); + } + + // progression of possible features: + // . Current: unit literals + // . Either lower or upper bound is unit coefficient + // . single occurrence of x in C + // . (x <= t or x <= s or C) == (x <= max(s, t) or C) + // + + bool is_invertible(var x, polynomial_ref& A) { + if (!m_pm.is_const(A)) + return false; + if (s.is_int(x) && !is_unit(A)) + return false; + return true; + } + + bool apply_fm(var x, ptr_vector& clauses) { + polynomial_ref A(m_pm), B(m_pm); + vector lo, hi; + poly* p = nullptr; + bool all_solved = true; + for (auto c : clauses) { + if (c->is_removed()) + continue; + if (c->size() != 1) { + all_solved = false; + continue; + } + literal lit = (*c)[0]; + bool sign = lit.sign(); + ineq_atom const& a = *to_ineq_atom(m_atoms[lit.var()]); + if (sign && a.is_eq()) { + all_solved = false; + continue; + } + if (!is_single_poly(a, p)) { + all_solved = false; + continue; + } + if (1 != m_pm.degree(p, x)) { + all_solved = false; + continue; + } + A = m_pm.coeff(p, x, 1, B); + if (!is_invertible(x, A)) { + all_solved = false; + continue; + } + auto const& A_value = m_pm.coeff(A, 0); + bool is_pos = m_pm.m().is_pos(A_value); + bool is_strict = false; + switch (a.get_kind()) { + case atom::LT: + // !(Ax + B < 0) == Ax + B >= 0 + if (sign) + is_strict = false; + else { + // Ax + B < 0 == -Ax - B > 0 + A = -A; + B = -B; + is_pos = !is_pos; + if (s.is_int(x)) { + // Ax + B > 0 == Ax + B - |A| >= 0 + if (is_pos) + B = m_pm.sub(B, A); + else + B = m_pm.add(B, A); + is_strict = false; + } + else + is_strict = true; + } + break; + case atom::GT: + // !(Ax + B > 0) == -Ax + -B >= 0 + if (sign) { + A = -A; + B = -B; + is_pos = !is_pos; + is_strict = false; + } + else { + // Ax + B > 0 + if (s.is_int(x)) { + // Ax + B - |A| >= 0 + if (is_pos) + B = m_pm.sub(B, A); + else + B = m_pm.add(B, A); + is_strict = false; + } + else + is_strict = true; + } + break; + case atom::EQ: { + all_solved = false; + if (sign) + continue; + bound_constraint l(x, A, B, false, c); + A = -A; + B = -B; + bound_constraint h(x, A, B, false, c); + apply_fm_equality(x, clauses, l, h); + return true; + } + default: + UNREACHABLE(); + break; + } + auto& set = is_pos ? hi : lo; + bool found = false; + for (auto const& bound : set) { + if (is_strict == bound.is_strict && m_pm.eq(A, bound.A) && m_pm.eq(B, bound.B)) + found = true; + } + if (found) + continue; + + set.push_back(bound_constraint(x, A, B, is_strict, c)); + + } + + if (lo.empty() && hi.empty()) + return false; + + if (apply_fm_equality(x, clauses, lo, hi)) + return true; + + + if (!all_solved) + return false; + + IF_VERBOSE(3, + verbose_stream() << "x" << x << " lo " << lo.size() << " hi " << hi.size() << "\n"; + for (auto c : clauses) + if (!c->is_removed()) + s.display(verbose_stream(), *c) << "\n"; + ); + + auto num_lo = lo.size(), num_hi = hi.size(); + if (num_lo >= 2 && num_hi >= 2 && (num_lo > 2 || num_hi > 2)) + return false; + + apply_fm_inequality(x, clauses, lo, hi); + + return true; + } + + void apply_fm_inequality( + var x, ptr_vector& clauses, + vector& lo, vector& hi) { + + polynomial_ref C(m_pm), D(m_pm); + for (auto c : clauses) + c->set_removed(); + + for (auto const& l : lo) { + // l.A * x + l.B, l.is_strict;, l.A < 0 + for (auto const& h : hi) { + // h.A * x + h.B, h.is_strict; h.A > 0 + // (l.A x + l.B)*h.A + (h.A x + h.B)*|l.A| >= 0 + C = m_pm.mul(l.B, h.A); + D = m_pm.mul(h.B, l.A); + C = m_pm.sub(C, D); + poly* p = C.get(); + bool is_even = false; + m_lemma.reset(); + if (l.is_strict || h.is_strict) + m_lemma.push_back(s.mk_ineq_literal(atom::GT, 1, &p, &is_even, true)); + else + m_lemma.push_back(~s.mk_ineq_literal(atom::LT, 1, &p, &is_even, true)); + if (m_lemma[0] == true_literal) + continue; + auto a = s.join(l.c->assumptions(), h.c->assumptions()); + auto cls = s.mk_clause(m_lemma.size(), m_lemma.data(), false, a); + if (cls) + compute_occurs(*cls); + IF_VERBOSE(3, s.display(verbose_stream() << "add resolvent ", *cls) << "\n"); + } + } + + // track updates for model reconstruction + for (auto const& l : lo) + s.add_bound(l); + for (auto const& h : hi) + s.add_bound(h); + } + + literal substitute_var(var x, poly* p, poly* q, literal lit) { + auto b = lit.var(); + auto a = m_atoms[b]; + if (!a) + return lit; + SASSERT(a->is_ineq_atom()); + auto& a1 = *to_ineq_atom(a); + auto r = substitute_var(x, p, q, a1); + if (r == null_literal) + r = lit; + else if (lit.sign()) + r.neg(); + return r; + } + + literal substitute_var(var x, poly* p, poly* q, ineq_atom const& a) { + unsigned sz = a.size(); + bool_vector even; + polynomial_ref pr(m_pm), qq(q, m_pm); + qq = -qq; + polynomial_ref_vector ps(m_pm); + bool change = false; + auto k = a.get_kind(); + for (unsigned i = 0; i < sz; ++i) { + poly* po = a.p(i); + m_pm.substitute(po, x, qq, p, pr); + change |= pr != po; + TRACE("nlsat", tout << pr << "\n";); + if (m_pm.is_zero(pr)) { + ps.reset(); + even.reset(); + ps.push_back(pr); + even.push_back(false); + break; + } + if (m_pm.is_const(pr)) { + if (!a.is_even(i) && m_pm.m().is_neg(m_pm.coeff(pr, 0))) + k = atom::flip(k); + continue; + } + ps.push_back(pr); + even.push_back(a.is_even(i)); + } + if (!change) + return null_literal; + return s.mk_ineq_literal(k, ps.size(), ps.data(), even.data(), true); + } + + bool apply_fm_equality( + var x, ptr_vector& clauses, + vector& lo, vector& hi) { + for (auto& l : lo) { + if (l.is_strict) + continue; + l.A = -l.A; + l.B = -l.B; + for (auto& h : hi) { + if (h.is_strict) + continue; + if (!m_pm.eq(l.B, h.B)) + continue; + if (!m_pm.eq(l.A, h.A)) + continue; + l.A = -l.A; + l.B = -l.B; + apply_fm_equality(x, clauses, l, h); + s.inc_simplify(); + return true; + } + l.A = -l.A; + l.B = -l.B; + } + return false; + } + + void apply_fm_equality( + var x, ptr_vector& clauses, + bound_constraint& l, bound_constraint& h) { + auto a1 = s.join(l.c->assumptions(), h.c->assumptions()); + s.inc_ref(a1); + + polynomial_ref A(l.A), B(l.B); + + if (m_pm.is_neg(l.A)) { + A = -A; + B = -B; + } + + for (auto c : clauses) { + if (c->is_removed()) + continue; + c->set_removed(); + if (c == l.c || c == h.c) + continue; + m_lemma.reset(); + bool is_tautology = false; + for (literal lit : *c) { + lit = substitute_var(x, A, B, lit); + m_lemma.push_back(lit); + if (lit == true_literal) + is_tautology = true; + } + if (is_tautology) + continue; + auto a = s.join(c->assumptions(), a1); + auto cls = s.mk_clause(m_lemma.size(), m_lemma.data(), false, a); + + IF_VERBOSE(3, + if (cls) { + s.display_proc()(verbose_stream(), x) << " * " << l.A << " = " << l.B << "\n"; + s.display(verbose_stream(), *c) << " -> "; + s.display(verbose_stream(), *cls) << " - "; + s.display(verbose_stream(), *l.c) << " "; + s.display(verbose_stream(), *h.c) << "\n"; + }); + if (cls) + compute_occurs(*cls); + } + s.dec_ref(a1); + // track updates for model reconstruction + s.add_bound(l); + s.add_bound(h); + s.inc_simplify(); + } + + bool is_single_poly(ineq_atom const& a, poly*& p) { + unsigned sz = a.size(); + return sz == 1 && a.is_odd(0) && (p = a.p(0), true); + } + + bool is_unit(polynomial_ref const& p) { + if (!m_pm.is_const(p)) + return false; + auto const& c = m_pm.coeff(p, 0); + return m_pm.m().is_one(c) || m_pm.m().is_minus_one(c); + } + }; + + simplify::simplify(solver& s, atom_vector& atoms, clause_vector& clauses, clause_vector& learned, pmanager& pm) { + m_imp = alloc(imp, s, atoms, clauses, learned, pm); + } + + simplify::~simplify() { + dealloc(m_imp); + } + + void simplify::operator()() { + (*m_imp)(); + } + +}; diff --git a/src/nlsat/nlsat_simplify.h b/src/nlsat/nlsat_simplify.h new file mode 100644 index 000000000..407dc4489 --- /dev/null +++ b/src/nlsat/nlsat_simplify.h @@ -0,0 +1,16 @@ +#pragma once + +#include "nlsat/nlsat_types.h" +#include "nlsat/nlsat_clause.h" + +namespace nlsat { + class simplify { + struct imp; + imp * m_imp; + public: + simplify(solver& s, atom_vector& atoms, clause_vector& clauses, clause_vector& learned, pmanager & pm); + ~simplify(); + + void operator()(); + }; +} \ No newline at end of file diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index eed908617..ca057afef 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -33,6 +33,7 @@ Revision History: #include "nlsat/nlsat_evaluator.h" #include "nlsat/nlsat_explain.h" #include "nlsat/nlsat_params.hpp" +#include "nlsat/nlsat_simplify.h" #define NLSAT_EXTRA_VERBOSE @@ -44,6 +45,7 @@ Revision History: namespace nlsat { + typedef chashtable ineq_atom_table; typedef chashtable root_atom_table; @@ -71,28 +73,24 @@ namespace nlsat { }; struct solver::imp { + + struct dconfig { typedef imp value_manager; typedef small_object_allocator allocator; - typedef void * value; - static const bool ref_count = false; + typedef void* value; + static const bool ref_count = false; }; + typedef dependency_manager assumption_manager; - typedef assumption_manager::dependency * _assumption_set; + typedef assumption_manager::dependency* _assumption_set; + typedef obj_ref assumption_set_ref; typedef polynomial::cache cache; typedef ptr_vector interval_set_vector; - struct bound_constraint { - var x; - polynomial_ref A, B; - bool is_strict; - clause* c; - bound_constraint(var x, polynomial_ref& A, polynomial_ref& B, bool is_strict, clause* c): - x(x), A(A), B(B), is_strict(is_strict), c(c) {} - }; ctx& m_ctx; @@ -111,6 +109,7 @@ namespace nlsat { ineq_atom_table m_ineq_atoms; root_atom_table m_root_atoms; + vector m_bounds; id_gen m_cid_gen; @@ -127,6 +126,8 @@ namespace nlsat { bool_vector m_dead; // mark dead boolean variables id_gen m_bid_gen; + simplify m_simplify; + bool_vector m_is_int; // m_is_int[x] is true if variable is integer vector m_watches; // var -> clauses where variable is maximal interval_set_vector m_infeasible; // var -> to a set of interval where the variable cannot be assigned to. @@ -220,12 +221,19 @@ namespace nlsat { unsigned m_max_conflicts; unsigned m_lemma_count; + struct stats { + unsigned m_simplifications; + unsigned m_restarts; + unsigned m_conflicts; + unsigned m_propagations; + unsigned m_decisions; + unsigned m_stages; + unsigned m_irrational_assignments; // number of irrational witnesses + void reset() { memset(this, 0, sizeof(*this)); } + stats() { reset(); } + }; // statistics - unsigned m_conflicts; - unsigned m_propagations; - unsigned m_decisions; - unsigned m_stages; - unsigned m_irrational_assignments; // number of irrational witnesses + stats m_stats; imp(solver& s, ctx& c): m_ctx(c), @@ -242,6 +250,7 @@ namespace nlsat { m_evaluator(s, m_assignment, m_pm, m_allocator), m_ism(m_evaluator.ism()), m_num_bool_vars(0), + m_simplify(s, m_atoms, m_clauses, m_learned, m_pm), m_display_var(m_perm), m_display_assumption(nullptr), m_explain(s, m_assignment, m_cache, m_atoms, m_var2eq, m_evaluator), @@ -336,10 +345,10 @@ namespace nlsat { void dec_ref(assumption) {} - void inc_ref(_assumption_set a) { + void inc_ref(_assumption_set a) { if (a != nullptr) m_asm.inc_ref(a); } - + void dec_ref(_assumption_set a) { if (a != nullptr) m_asm.dec_ref(a); } @@ -594,7 +603,7 @@ namespace nlsat { } - ineq_atom* mk_ineq_atom(atom::kind k, unsigned sz, poly * const * ps, bool const * is_even, bool& is_new) { + ineq_atom* mk_ineq_atom(atom::kind k, unsigned sz, poly * const * ps, bool const * is_even, bool& is_new, bool simplify) { SASSERT(sz >= 1); SASSERT(k == atom::LT || k == atom::GT || k == atom::EQ); int sign = 1; @@ -609,8 +618,27 @@ namespace nlsat { var curr_max = max_var(p.get()); if (curr_max > max || max == null_var) max = curr_max; + if (sz == 1 && simplify) { + if (sign < 0) + k = atom::flip(k); + sign = 1; + polynomial::manager::ineq_type t; + switch (k) { + case atom::EQ: t = polynomial::manager::ineq_type::EQ; break; + case atom::LT: t = polynomial::manager::ineq_type::LT; break; + case atom::GT: t = polynomial::manager::ineq_type::GT; break; + default: UNREACHABLE(); break; + } + polynomial::var_vector vars; + m_pm.vars(p, vars); + bool all_int = all_of(vars, [&](var x) { return is_int(x); }); + if (!all_int) + t = polynomial::manager::ineq_type::EQ; + m_pm.gcd_simplify(p, t); + } uniq_ps.push_back(m_cache.mk_unique(p)); TRACE("nlsat_table_bug", tout << "p: " << p << ", uniq: " << uniq_ps.back() << "\n";); + //verbose_stream() << "p: " << p.get() << ", uniq: " << uniq_ps.back() << "\n"; } void * mem = m_allocator.allocate(ineq_atom::get_obj_size(sz)); if (sign < 0) @@ -633,9 +661,9 @@ namespace nlsat { return atom; } - bool_var mk_ineq_atom(atom::kind k, unsigned sz, poly * const * ps, bool const * is_even) { + bool_var mk_ineq_atom(atom::kind k, unsigned sz, poly * const * ps, bool const * is_even, bool simplify = false) { bool is_new = false; - ineq_atom* atom = mk_ineq_atom(k, sz, ps, is_even, is_new); + ineq_atom* atom = mk_ineq_atom(k, sz, ps, is_even, is_new, simplify); if (!is_new) { return atom->bvar(); } @@ -648,7 +676,7 @@ namespace nlsat { } } - literal mk_ineq_literal(atom::kind k, unsigned sz, poly * const * ps, bool const * is_even) { + literal mk_ineq_literal(atom::kind k, unsigned sz, poly * const * ps, bool const * is_even, bool simplify = false) { SASSERT(k == atom::LT || k == atom::GT || k == atom::EQ); bool is_const = true; polynomial::manager::scoped_numeral cnst(m_pm.m()); @@ -676,7 +704,7 @@ namespace nlsat { if (m_pm.m().is_zero(cnst) && k == atom::EQ) return true_literal; return false_literal; } - return literal(mk_ineq_atom(k, sz, ps, is_even), false); + return literal(mk_ineq_atom(k, sz, ps, is_even, simplify), false); } bool_var mk_root_atom(atom::kind k, var x, unsigned i, poly * p) { @@ -879,13 +907,13 @@ namespace nlsat { for (literal lit : *c) { lits.push_back(literal(tr[lit.var()], lit.sign())); } - checker.mk_clause(lits.size(), lits.data(), nullptr); + checker.mk_external_clause(lits.size(), lits.data(), nullptr); } } for (unsigned i = 0; i < n; ++i) { literal lit = cls[i]; literal nlit(tr[lit.var()], !lit.sign()); - checker.mk_clause(1, &nlit, nullptr); + checker.mk_external_clause(1, &nlit, nullptr); } lbool r = checker.check(); if (r == l_true) { @@ -954,6 +982,10 @@ namespace nlsat { } clause * mk_clause(unsigned num_lits, literal const * lits, bool learned, _assumption_set a) { + if (num_lits == 0) { + num_lits = 1; + lits = &false_literal; + } SASSERT(num_lits > 0); clause * cls = mk_clause_core(num_lits, lits, learned, a); TRACE("nlsat_sort", display(tout << "mk_clause:\n", *cls) << "\n";); @@ -973,7 +1005,7 @@ namespace nlsat { return cls; } - void mk_clause(unsigned num_lits, literal const * lits, assumption a) { + void mk_external_clause(unsigned num_lits, literal const * lits, assumption a) { _assumption_set as = nullptr; if (a != nullptr) as = m_asm.mk_leaf(a); @@ -1170,9 +1202,9 @@ namespace nlsat { SASSERT(j != null_justification); SASSERT(!j.is_null()); if (j.is_decision()) - m_decisions++; + m_stats.m_decisions++; else - m_propagations++; + m_stats.m_propagations++; bool_var b = l.var(); m_bvalues[b] = to_lbool(!l.sign()); m_levels[b] = m_scope_lvl; @@ -1472,7 +1504,7 @@ namespace nlsat { \brief Create a new stage. See Dejan and Leo's paper. */ void new_stage() { - m_stages++; + m_stats.m_stages++; save_new_stage_trail(); if (m_xk == null_var) m_xk = 0; @@ -1492,7 +1524,7 @@ namespace nlsat { tout << "assigning "; m_display_var(tout, m_xk) << "(x" << m_xk << ") -> " << w << "\n";); TRACE("nlsat_root", tout << "value as root object: "; m_am.display_root(tout, w); tout << "\n";); if (!m_am.is_rational(w)) - m_irrational_assignments++; + m_stats.m_irrational_assignments++; m_assignment.set_core(m_xk, w); } @@ -1524,6 +1556,17 @@ namespace nlsat { m_xk = null_var; while (true) { + if (should_reorder()) + do_reorder(); + +#if 0 + if (should_gc()) + do_gc(); +#endif + + if (should_simplify()) + do_simplify(); + CASSERT("nlsat", check_satisfied()); if (m_xk == null_var) { peek_next_bool_var(); @@ -1556,7 +1599,7 @@ namespace nlsat { break; if (!resolve(*conflict_clause)) return l_false; - if (m_conflicts >= m_max_conflicts) + if (m_stats.m_conflicts >= m_max_conflicts) return l_undef; log(); } @@ -1593,22 +1636,72 @@ namespace nlsat { reattach_arith_clauses(m_learned); } + + bool should_gc() { + return m_learned.size() > 10 * m_clauses.size(); + } + + void do_gc() { + undo_to_base(); + gc(); + } + + void undo_to_base() { + init_search(); + m_bk = 0; + m_xk = null_var; + } + + unsigned m_restart_threshold = 10000; + bool should_reorder() { + return m_stats.m_conflicts > 0 && m_stats.m_conflicts % m_restart_threshold == 0; + } + + void do_reorder() { + undo_to_base(); + m_stats.m_restarts++; + m_stats.m_conflicts++; + if (m_reordered) + restore_order(); + apply_reorder(); + } + + bool m_did_simplify = false; + bool should_simplify() { + return + !m_did_simplify && m_inline_vars && + !m_incremental && m_stats.m_conflicts > 100; + } + + void do_simplify() { + undo_to_base(); + m_did_simplify = true; + m_simplify(); + } + unsigned m_next_conflict = 100; void log() { - if (m_conflicts != 1 && m_conflicts < m_next_conflict) + if (m_stats.m_conflicts != 1 && m_stats.m_conflicts < m_next_conflict) return; m_next_conflict += 100; - IF_VERBOSE(2, verbose_stream() << "(nlsat :conflicts " << m_conflicts << " :decisions " << m_decisions << " :propagations " << m_propagations << " :clauses " << m_clauses.size() << " :learned " << m_learned.size() << ")\n"); + IF_VERBOSE(2, verbose_stream() << "(nlsat :conflicts " << m_stats.m_conflicts + << " :decisions " << m_stats.m_decisions + << " :propagations " << m_stats.m_propagations + << " :clauses " << m_clauses.size() + << " :learned " << m_learned.size() << ")\n"); } lbool search_check() { lbool r = l_undef; - m_conflicts = 0; + m_stats.m_conflicts = 0; + m_stats.m_restarts = 0; m_next_conflict = 0; while (true) { r = search(); - if (r != l_true) break; + if (r != l_true) + break; + ++m_stats.m_restarts; vector> bounds; for (var x = 0; x < num_vars(); x++) { @@ -1631,11 +1724,22 @@ namespace nlsat { bounds.push_back(std::make_pair(x, lo)); } } - if (bounds.empty()) break; + if (bounds.empty()) + break; gc(); + if (m_stats.m_restarts % 10 == 0) { + if (m_reordered) + restore_order(); + apply_reorder(); + } + init_search(); - IF_VERBOSE(2, verbose_stream() << "(nlsat-b&b :conflicts " << m_conflicts << " :decisions " << m_decisions << " :propagations " << m_propagations << " :clauses " << m_clauses.size() << " :learned " << m_learned.size() << ")\n"); + IF_VERBOSE(2, verbose_stream() << "(nlsat-b&b :conflicts " << m_stats.m_conflicts + << " :decisions " << m_stats.m_decisions + << " :propagations " << m_stats.m_propagations + << " :clauses " << m_clauses.size() + << " :learned " << m_learned.size() << ")\n"); for (auto const& b : bounds) { var x = b.first; rational lo = b.second; @@ -1653,6 +1757,7 @@ namespace nlsat { // perform branch and bound clause * cls = mk_clause(m_lemma.size(), m_lemma.data(), true, nullptr); + IF_VERBOSE(4, display(verbose_stream(), *cls) << "\n"); if (cls) { TRACE("nlsat", display(tout << "conflict " << lo << " " << hi, *cls); tout << "\n";); } @@ -1661,35 +1766,42 @@ namespace nlsat { return r; } + bool m_reordered = false; + + void apply_reorder() { + m_reordered = false; + if (!can_reorder()) + ; + else if (m_random_order) { + shuffle_vars(); + m_reordered = true; + } + else if (m_reorder) { + heuristic_reorder(); + m_reordered = true; + } + } + lbool check() { TRACE("nlsat_smt2", display_smt2(tout);); TRACE("nlsat_fd", tout << "is_full_dimensional: " << is_full_dimensional() << "\n";); init_search(); m_explain.set_full_dimensional(is_full_dimensional()); - bool reordered = false; + apply_reorder(); + +#if 0 if (!m_incremental && m_inline_vars) { - if (!simplify()) + if (!m_simplify()) return l_false; } - - if (!can_reorder()) { - - } - else if (m_random_order) { - shuffle_vars(); - reordered = true; - } - else if (m_reorder) { - heuristic_reorder(); - reordered = true; - } +#endif + IF_VERBOSE(3, verbose_stream() << "search\n"); sort_watched_clauses(); lbool r = search_check(); CTRACE("nlsat_model", r == l_true, tout << "model before restore order\n"; display_assignment(tout);); - if (reordered) { - restore_order(); - } + if (m_reordered) + restore_order(); CTRACE("nlsat_model", r == l_true, tout << "model\n"; display_assignment(tout);); CTRACE("nlsat", r == l_false, display(tout << "unsat\n");); SASSERT(r != l_true || check_satisfied(m_clauses)); @@ -1713,7 +1825,7 @@ namespace nlsat { unsigned sz = assumptions.size(); literal const* ptr = assumptions.data(); for (unsigned i = 0; i < sz; ++i) { - mk_clause(1, ptr+i, (assumption)(ptr+i)); + mk_external_clause(1, ptr+i, (assumption)(ptr+i)); } display_literal_assumption dla(*this, assumptions); scoped_display_assumptions _scoped_display(*this, dla); @@ -1910,6 +2022,8 @@ namespace nlsat { for (unsigned i = 0; i < sz; i++) { literal l = m_lazy_clause[i]; if (l.var() != b) { + if (value(l) != l_false) + display(verbose_stream() << value(l) << " ", 1, &l); SASSERT(value(l) == l_false || m_rlimit.is_canceled()); } else { @@ -2052,7 +2166,7 @@ namespace nlsat { SASSERT(check_marks()); TRACE("nlsat_proof", tout << "STARTING RESOLUTION\n";); TRACE("nlsat_proof_sk", tout << "STARTING RESOLUTION\n";); - m_conflicts++; + m_stats.m_conflicts++; TRACE("nlsat", tout << "resolve, conflicting clause:\n"; display(tout, *conflict_clause) << "\n"; tout << "xk: "; if (m_xk != null_var) m_display_var(tout, m_xk); else tout << ""; tout << "\n"; tout << "scope_lvl: " << scope_lvl() << "\n"; @@ -2197,8 +2311,7 @@ namespace nlsat { VERIFY(process_clause(*conflict_clause, true)); return true; } - new_cls = mk_clause(sz, m_lemma.data(), true, m_lemma_assumptions.get()); - + new_cls = mk_clause(sz, m_lemma.data(), true, m_lemma_assumptions.get()); } NLSAT_VERBOSE(display(verbose_stream(), *new_cls) << "\n";); if (!process_clause(*new_cls, true)) { @@ -2303,19 +2416,17 @@ namespace nlsat { // ----------------------- void collect_statistics(statistics & st) { - st.update("nlsat conflicts", m_conflicts); - st.update("nlsat propagations", m_propagations); - st.update("nlsat decisions", m_decisions); - st.update("nlsat stages", m_stages); - st.update("nlsat irrational assignments", m_irrational_assignments); + st.update("nlsat conflicts", m_stats.m_conflicts); + st.update("nlsat propagations", m_stats.m_propagations); + st.update("nlsat decisions", m_stats.m_decisions); + st.update("nlsat restarts", m_stats.m_restarts); + st.update("nlsat stages", m_stats.m_stages); + st.update("nlsat simplifications", m_stats.m_simplifications); + st.update("nlsat irrational assignments", m_stats.m_irrational_assignments); } void reset_statistics() { - m_conflicts = 0; - m_propagations = 0; - m_decisions = 0; - m_stages = 0; - m_irrational_assignments = 0; + m_stats.reset(); } // ----------------------- @@ -2327,6 +2438,7 @@ namespace nlsat { struct var_info_collector { pmanager & pm; atom_vector const & m_atoms; + var_vector m_shuffle; unsigned_vector m_max_degree; unsigned_vector m_num_occs; @@ -2402,7 +2514,7 @@ namespace nlsat { return false; if (m_info.m_num_occs[x] > m_info.m_num_occs[y]) return true; - return x < y; + return m_info.m_shuffle[x] < m_info.m_shuffle[y]; } }; @@ -2412,11 +2524,12 @@ namespace nlsat { var_info_collector collector(m_pm, m_atoms, num); collector.collect(m_clauses); collector.collect(m_learned); + init_shuffle(collector.m_shuffle); TRACE("nlsat_reorder", collector.display(tout, m_display_var);); var_vector new_order; - for (var x = 0; x < num; x++) { + for (var x = 0; x < num; x++) new_order.push_back(x); - } + std::sort(new_order.begin(), new_order.end(), reorder_lt(collector)); TRACE("nlsat_reorder", tout << "new order: "; for (unsigned i = 0; i < num; i++) tout << new_order[i] << " "; tout << "\n";); @@ -2429,20 +2542,23 @@ namespace nlsat { SASSERT(check_invariant()); } - void shuffle_vars() { - var_vector p; + void init_shuffle(var_vector& p) { unsigned num = num_vars(); - for (var x = 0; x < num; x++) { + for (var x = 0; x < num; x++) p.push_back(x); - } + random_gen r(++m_random_seed); shuffle(p.size(), p.data(), r); + } + + void shuffle_vars() { + var_vector p; + init_shuffle(p); reorder(p.size(), p.data()); } bool can_reorder() const { - return m_bounds.empty() - && all_of(m_learned, [&](clause* c) { return !has_root_atom(*c); }) + return all_of(m_learned, [&](clause* c) { return !has_root_atom(*c); }) && all_of(m_clauses, [&](clause* c) { return !has_root_atom(*c); }); } @@ -2450,7 +2566,10 @@ namespace nlsat { \brief Reorder variables using the giving permutation. p maps internal variables to their new positions */ + + void reorder(unsigned sz, var const * p) { + remove_learned_roots(); SASSERT(can_reorder()); TRACE("nlsat_reorder", tout << "solver before variable reorder\n"; display(tout); @@ -2458,6 +2577,8 @@ namespace nlsat { tout << "\npermutation:\n"; for (unsigned i = 0; i < sz; i++) tout << p[i] << " "; tout << "\n"; ); + // verbose_stream() << "\npermutation: " << p[0] << " count " << count << " " << m_rlimit.is_canceled() << "\n"; + reinit_cache(); SASSERT(num_vars() == sz); TRACE("nlsat_bool_assignment_bug", tout << "before reset watches\n"; display_bool_assignment(tout);); reset_watches(); @@ -2499,6 +2620,8 @@ namespace nlsat { } #endif m_pm.rename(sz, p); + for (auto& b : m_bounds) + b.x = p[b.x]; TRACE("nlsat_bool_assignment_bug", tout << "before reinit cache\n"; display_bool_assignment(tout);); reinit_cache(); m_assignment.swap(new_assignment); @@ -2734,552 +2857,7 @@ namespace nlsat { The method ignores lemmas and assumes constraints don't use roots. */ - vector> m_var_occurs; - bool simplify() { - unsigned sz = m_clauses.size(); - while (true) { - - while (elim_uncnstr()) - ; - while (fm()) - ; - if (!solve_eqs()) - return false; - - subsumption_simplify(); - if (m_clauses.size() >= sz) - break; - sz = m_clauses.size(); - } - - IF_VERBOSE(3, display(verbose_stream())); - - return true; - } - - // - // Remove unconstrained assertions. - // - bool elim_uncnstr() { - // compute variable occurrences - if (any_of(m_clauses, [&](clause* c) { return has_root_atom(*c); })) - return false; - compute_occurs(); - // for each variable occurrence, figure out if it is unconstrained. - ptr_vector to_delete; - for (unsigned v = m_var_occurs.size(); v-- > 0; ) { - auto& clauses = m_var_occurs[v]; - if (clauses.size() != 1) - continue; - auto& c = *clauses[0]; - if (c.is_removed()) - continue; - if (!is_unconstrained(v, c)) - continue; - c.set_removed(); - to_delete.push_back(&c); - } - for (auto* c : to_delete) - del_clause(c, m_clauses); - - return !to_delete.empty(); - } - - void compute_occurs(clause& c) { - var_vector vars; - m_pm.begin_vars_incremental(); - for (auto lit : c) { - bool_var b = lit.var(); - atom* a = m_atoms[b]; - if (!a) - continue; - if (a->is_ineq_atom()) { - auto sz = to_ineq_atom(a)->size(); - for (unsigned i = 0; i < sz; ++i) { - auto* p = to_ineq_atom(a)->p(i); - m_pm.vars_incremental(p, vars); - } - } - } - m_pm.end_vars_incremental(vars); - unsigned h = 0; - for (auto v : vars) { - m_var_occurs.reserve(v + 1); - m_var_occurs[v].push_back(&c); - h |= (1ul << (v % 32ul)); - } - c.set_var_hash(h); - } - - void compute_occurs() { - m_var_occurs.reset(); - for (auto c : m_clauses) - compute_occurs(*c); - } - - bool is_unconstrained(var x, clause& c) { - poly* p; - polynomial_ref A(m_pm), B(m_pm); - for (auto lit : c) { - bool_var b = lit.var(); - if (!m_atoms[b]) - continue; - auto& a = *to_ineq_atom(m_atoms[b]); - if (!is_single_poly(a, p)) - continue; - - if (1 != m_pm.degree(p, x)) - continue; - - A = m_pm.coeff(p, x, 1, B); - - if (a.is_eq() && !lit.sign()) { - // A*x + B = 0 - if (is_int(x) && is_unit(A)) { - m_bounds.push_back(bound_constraint(x, A, B, false, nullptr)); - return true; - } - - if (!is_int(x) && m_pm.is_const(A)) { - m_bounds.push_back(bound_constraint(x, A, B, false, nullptr)); - return true; - } - } - // TODO: add other cases for LT and GT atoms - } - return false; - } - - bool cleanup_removed() { - unsigned j = 0, sz = m_clauses.size(); - for (unsigned i = 0; i < sz; ++i) { - auto c = m_clauses[i]; - if (c->is_removed()) - del_clause(c); - else - m_clauses[j++] = c; - } - m_clauses.shrink(j); - return j < sz; - } - - // - // Fourier Motzkin elimination - // - - bool fm() { - if (any_of(m_clauses, [&](clause* c) { return has_root_atom(*c); })) - return false; - compute_occurs(); - - for (unsigned v = m_var_occurs.size(); v-- > 0; ) - apply_fm(v, m_var_occurs[v]); - - return cleanup_removed(); - } - - // progression of features - // unit literals - // single occurrence of x in C - // (x <= t or x <= s or C) == (x <= max(s, t) or C) - - - bool is_invertible(var x, polynomial_ref & A) { - if (!m_pm.is_const(A)) - return false; - if (is_int(x) && !is_unit(A)) - return false; - return true; - } - - bool apply_fm(var x, ptr_vector& clauses) { - polynomial_ref A(m_pm), B(m_pm); - vector lo, hi; - poly* p = nullptr; - bool all_solved = true; - for (auto c : clauses) { - if (c->is_removed()) - continue; - if (c->size() != 1) { - all_solved = false; - continue; - } - literal lit = (*c)[0]; - bool sign = lit.sign(); - ineq_atom const& a = *to_ineq_atom(m_atoms[lit.var()]); - if (sign && a.is_eq()) { - all_solved = false; - continue; - } - if (!is_single_poly(a, p)) { - all_solved = false; - continue; - } - if (1 != m_pm.degree(p, x)) { - all_solved = false; - continue; - } - A = m_pm.coeff(p, x, 1, B); - if (!is_invertible(x, A)) { - all_solved = false; - continue; - } - auto const& A_value = m_pm.coeff(A, 0); - bool is_pos = m_pm.m().is_pos(A_value); - bool is_strict = false; - switch (a.get_kind()) { - case atom::LT: - // !(Ax + B < 0) == Ax + B >= 0 - if (sign) - is_strict = false; - else { - // Ax + B < 0 == -Ax - B > 0 - A = -A; - B = -B; - is_pos = !is_pos; - if (is_int(x)) { - // Ax + B > 0 == Ax + B - |A| >= 0 - if (is_pos) - B = m_pm.add(B, A); - else - B = m_pm.sub(B, A); - is_strict = false; - } - else - is_strict = true; - } - break; - case atom::GT: - // !(Ax + B > 0) == -Ax + -B >= 0 - if (sign) { - A = -A; - B = -B; - is_pos = !is_pos; - is_strict = false; - } - else { - // Ax + B > 0 - if (is_int(x)) { - // Ax + B - |A| >= 0 - if (is_pos) - B = m_pm.sub(B, A); - else - B = m_pm.add(B, A); - is_strict = false; - } - else - is_strict = true; - } - break; - case atom::EQ: { - all_solved = false; - continue; - // unsound: - m_display_var(verbose_stream(), x); - display(verbose_stream() << " ", *c) << "\n"; - bound_constraint l(x, A, B, false, c); - A = -A; - B = -B; - bound_constraint h(x, A, B, false, c); - apply_fm_equality(x, clauses, l, h); - return true; - } - default: - UNREACHABLE(); - break; - } - auto& set = is_pos ? hi : lo; - bool found = false; - for (auto const& bound : set) { - if (is_strict == bound.is_strict && m_pm.eq(A, bound.A) && m_pm.eq(B, bound.B)) - found = true; - } - if (found) - continue; - - set.push_back(bound_constraint(x, A, B, is_strict, c)); - - } - - if (lo.empty() && hi.empty()) - return false; - - IF_VERBOSE(3, - verbose_stream() << "x" << x << " lo " << lo.size() << " hi " << hi.size() << "\n"; - for (auto c : clauses) - if (!c->is_removed()) - display(verbose_stream(), *c) << "\n"; - ); - - if (apply_fm_equality(x, clauses, lo, hi)) - return true; - - // return false; - - if (!all_solved) - return false; - - auto num_lo = lo.size(), num_hi = hi.size(); - if (num_lo >= 2 && num_hi >= 2 && (num_lo > 2 || num_hi > 2)) - return false; - - apply_fm_inequality(x, clauses, lo, hi); - - return true; - } - - void apply_fm_inequality( - var x, ptr_vector& clauses, - vector& lo, vector& hi) { - - polynomial_ref C(m_pm), D(m_pm); - for (auto c : clauses) - c->set_removed(); - - for (auto const& l : lo) { - // l.A * x + l.B, l.is_strict;, l.A < 0 - for (auto const& h : hi) { - // h.A * x + h.B, h.is_strict; h.A > 0 - // (l.A x + l.B)*h.A + (h.A x + h.B)*|l.A| >= 0 - C = m_pm.mul(l.B, h.A); - D = m_pm.mul(h.B, l.A); - C = m_pm.sub(C, D); - poly* p = C.get(); - bool is_even = false; - m_lemma.reset(); - if (l.is_strict || h.is_strict) - m_lemma.push_back(mk_ineq_literal(atom::GT, 1, &p, &is_even)); - else - m_lemma.push_back(~mk_ineq_literal(atom::LT, 1, &p, &is_even)); - if (m_lemma[0] == true_literal) - continue; - auto a1 = static_cast<_assumption_set>(l.c->assumptions()); - auto a2 = static_cast<_assumption_set>(h.c->assumptions()); - auto cls = mk_clause(m_lemma.size(), m_lemma.data(), false, m_asm.mk_join(a1, a2)); - if (cls) - compute_occurs(*cls); - IF_VERBOSE(3, display(verbose_stream() << "add resolvent ", *cls) << "\n"); - } - } - - // track updates for model reconstruction - for (auto const& l : lo) - m_bounds.push_back(l); - for (auto const& h : hi) - m_bounds.push_back(h); - } - - bool apply_fm_equality( - var x, ptr_vector& clauses, - vector& lo, vector& hi) { - for (auto& l : lo) { - if (l.is_strict) - continue; - l.A = -l.A; - l.B = -l.B; - for (auto& h : hi) { - if (h.is_strict) - continue; - if (!m_pm.eq(l.B, h.B)) - continue; - if (!m_pm.eq(l.A, h.A)) - continue; - l.A = -l.A; - l.B = -l.B; - apply_fm_equality(x, clauses, l, h); - return true; - } - l.A = -l.A; - l.B = -l.B; - } - return false; - } - - void apply_fm_equality( - var x, ptr_vector& clauses, - bound_constraint& l, bound_constraint& h) { - auto a1 = static_cast<_assumption_set>(l.c->assumptions()); - auto a2 = static_cast<_assumption_set>(h.c->assumptions()); - a1 = m_asm.mk_join(a1, a2); - m_lemma_assumptions = a1; - - polynomial_ref A(l.A), B(l.B); - - if (m_pm.is_neg(l.A)) { - A = -A; - B = -B; - } - - // TODO: this can also replace solve_eqs - for (auto c : clauses) { - if (c->is_removed()) - continue; - c->set_removed(); - if (c == l.c || c == h.c) - continue; - m_lemma.reset(); - bool is_tautology = false; - for (literal lit : *c) { - lit = substitute_var(x, A, B, lit); - m_lemma.push_back(lit); - if (lit == true_literal) - is_tautology = true; - } - if (is_tautology) - continue; - a2 = static_cast<_assumption_set>(c->assumptions()); - auto cls = mk_clause(m_lemma.size(), m_lemma.data(), false, m_asm.mk_join(a1, a2)); - - IF_VERBOSE(3, - if (cls) { - m_display_var(verbose_stream(), x) << " * " << l.A << " = " << l.B << "\n"; - display(verbose_stream(), *c) << " -> "; - display(verbose_stream(), *cls) << "\n"; - }); - if (cls) - compute_occurs(*cls); - } - // track updates for model reconstruction - m_bounds.push_back(l); - m_bounds.push_back(h); - } - - // - // Subsumption simplification - // - void subsumption_simplify() { - compute_occurs(); - for (unsigned v = m_var_occurs.size(); v-- > 0; ) { - auto& clauses = m_var_occurs[v]; - for (auto c : clauses) { - if (c->is_marked() || c->is_removed()) - continue; - c->mark(); - for (auto c2 : clauses) { - if (c == c2 || c2->is_removed()) - continue; - if (subsumes(*c, *c2)) { - IF_VERBOSE(3, display(verbose_stream() << "subsumes ", *c); - display(verbose_stream() << " ", *c2) << "\n"); - c2->set_removed(); - } - } - } - } - for (auto c : m_clauses) - c->unmark(); - - cleanup_removed(); - } - - // does c1 subsume c2? - bool subsumes(clause const& c1, clause const& c2) { - if (c1.size() > c2.size()) - return false; - if ((c1.var_hash() & c2.var_hash()) != c1.var_hash()) - return false; - for (auto lit1 : c1) { - if (!any_of(c2, [&](auto lit2) { return subsumes(lit1, lit2); })) - return false; - } - return true; - } - - bool subsumes(literal lit1, literal lit2) { - if (lit1 == lit2) - return true; - - atom* a1 = m_atoms[lit1.var()]; - atom* a2 = m_atoms[lit2.var()]; - if (!a1 || !a2) - return false; - - // use m_pm.ge(p1, p2) - // whenever lit1 = p1 < 0, lit2 = p2 < 0 - // or lit1 = p1 < 0, lit2 = !(p2 > 0) - // or lit1 = !(p1 > 0), lit2 = !(p2 > 0) - // use m_pm.ge(p2, p1) - // whenever lit1 = p1 > 0, lit2 = p2 > 0 - // or lit1 = !(p1 < 0), lit2 = !(p2 < 0) - // or lit1 = p1 > 0, lit2 = !(p2 < 0) - // or lit1 = !(p1 > 0), lit2 = p2 < 0 - // - if (a1->is_ineq_atom() && a2->is_ineq_atom()) { - auto& i1 = *to_ineq_atom(a1); - auto& i2 = *to_ineq_atom(a2); - auto is_lt1 = !lit1.sign() && a1->get_kind() == atom::kind::LT; - auto is_le1 = lit1.sign() && a1->get_kind() == atom::kind::GT; - auto is_gt1 = !lit1.sign() && a1->get_kind() == atom::kind::GT; - auto is_ge1 = lit1.sign() && a1->get_kind() == atom::kind::LT; - - auto is_lt2 = !lit2.sign() && a2->get_kind() == atom::kind::LT; - auto is_le2 = lit2.sign() && a2->get_kind() == atom::kind::GT; - auto is_gt2 = !lit2.sign() && a2->get_kind() == atom::kind::GT; - auto is_ge2 = lit2.sign() && a2->get_kind() == atom::kind::LT; - - auto check_ge = (is_lt1 && (is_lt2 || is_le2)) || (is_le1 && is_le2); - auto check_le = (is_gt1 && (is_gt2 || is_ge2)) || (is_ge1 && is_ge2); - - if (i1.size() != i2.size()) - ; - else if (check_ge) { - for (unsigned i = 0; i < i1.size(); ++i) - if (!m_pm.ge(i1.p(i), i2.p(i))) - return false; - return true; - } - else if (check_le) { - for (unsigned i = 0; i < i1.size(); ++i) - if (!m_pm.ge(i2.p(i), i1.p(i))) - return false; - return true; - } - } - return false; - } - - // - // Equality simplificadtion (TODO, this should is deprecated by fm) - // - bool solve_eqs() { - polynomial_ref p(m_pm), q(m_pm); - var v; - init_var_signs(); - SASSERT(m_learned.empty()); - bool change = true; - while (change) { - change = false; - for (clause* c : m_clauses) { - if (solve_var(*c, v, p, q)) { - if (!m_pm.is_const(p)) - continue; - // optional throttles to restrict where solved variables are used - if (false && !m_pm.is_linear(q)) - continue; - if (false && !m_pm.is_univariate(q)) - continue; - bool is_small = true; - for (unsigned i = 0; i < m_pm.size(q) && is_small ; ++i) { - auto const& c = m_pm.coeff(q, i); - is_small &= m_pm.m().is_small(c); - } - if (!is_small && false) - continue; - TRACE("nlsat", tout << "p: " << p << "\nq: " << q << "\n x" << v << "\n";); - m_bounds.push_back(bound_constraint(v, p, q, false, nullptr)); - - if (!substitute_var(v, p, q, *c)) - return false; - del_clause(c, m_clauses); - TRACE("nlsat", display(tout << "simplified\n");); - change = true; - break; - } - } - } - return true; - } // Eliminated variables are tracked in m_bounds. // Each element in m_bounds tracks the eliminated variable and an upper or lower bound @@ -3380,126 +2958,7 @@ namespace nlsat { m_hi.set_core(x, val); } } - - literal substitute_var(var x, poly* p, poly* q, literal lit) { - auto b = lit.var(); - auto a = m_atoms[b]; - if (!a) - return lit; - SASSERT(a->is_ineq_atom()); - auto& a1 = *to_ineq_atom(a); - auto r = substitute_var(x, p, q, a1); - if (r == null_literal) - r = lit; - else if (lit.sign()) - r.neg(); - return r; - } - - literal substitute_var(var x, poly* p, poly* q, ineq_atom const& a) { - unsigned sz = a.size(); - bool_vector even; - polynomial_ref pr(m_pm), qq(q, m_pm); - qq = -qq; - polynomial_ref_vector ps(m_pm); - bool change = false; - auto k = a.get_kind(); - for (unsigned i = 0; i < sz; ++i) { - poly* po = a.p(i); - m_pm.substitute(po, x, qq, p, pr); - change |= pr != po; - TRACE("nlsat", tout << pr << "\n";); - if (m_pm.is_zero(pr)) { - ps.reset(); - even.reset(); - ps.push_back(pr); - even.push_back(false); - break; - } - if (m_pm.is_const(pr)) { - if (!a.is_even(i) && m_pm.m().is_neg(m_pm.coeff(pr, 0))) - k = atom::flip(k); - continue; - } - ps.push_back(pr); - even.push_back(a.is_even(i)); - } - if (!change) - return null_literal; - return mk_ineq_literal(k, ps.size(), ps.data(), even.data()); - } - - bool substitute_var(var x, poly* p, poly* q, clause& src) { - u_map b2l; - scoped_literal_vector lits(m_solver); - unsigned num_atoms = m_atoms.size(); - for (unsigned j = 0; j < num_atoms; ++j) { - atom* a = m_atoms[j]; - if (a && a->is_ineq_atom()) { - ineq_atom const& a1 = *to_ineq_atom(a); - literal l = substitute_var(x, p, q, a1); - if (l == null_literal) - continue; - lits.push_back(l); - if (a1.m_bool_var != l.var()) { - b2l.insert(a1.m_bool_var, l); - } - } - } - return update_clauses(b2l, src); - } - - - bool update_clauses(u_map const& b2l, clause& src) { - bool is_sat = true; - literal_vector lits; - clause_vector to_delete; - unsigned n = m_clauses.size(); - auto a1 = static_cast<_assumption_set>(src.assumptions()); - for (unsigned i = 0; i < n; ++i) { - clause* c = m_clauses[i]; - if (c == &src) - continue; - lits.reset(); - bool changed = false; - bool is_tautology = false; - for (literal l : *c) { - literal lit = null_literal; - if (b2l.find(l.var(), lit)) { - lit = l.sign() ? ~lit : lit; - if (lit == true_literal) { - is_tautology = true; - } - else if (lit != false_literal) { - lits.push_back(lit); - } - changed = true; - } - else { - lits.push_back(l); - } - } - if (changed) { - to_delete.push_back(c); - if (is_tautology) { - continue; - } - if (lits.empty()) { - is_sat = false; - } - else { - auto a2 = static_cast<_assumption_set>(c->assumptions()); - auto a = m_asm.mk_join(a1, a2); - mk_clause(lits.size(), lits.data(), c->is_learned(), a); - } - } - } - for (clause* c : to_delete) { - del_clause(c, m_clauses); - } - return is_sat; - } - + bool is_unit_ineq(clause const& c) const { return c.size() == 1 && @@ -3560,65 +3019,7 @@ namespace nlsat { bool is_single_poly(ineq_atom const& a, poly*& p) { unsigned sz = a.size(); return sz == 1 && a.is_odd(0) && (p = a.p(0), true); - } - - svector m_var_signs; - - void init_var_signs() { - m_var_signs.reset(); - for (clause* cp : m_clauses) { - clause& c = *cp; - var x = 0; - lbool cmp = is_cmp0(c, x); - switch (cmp) { - case l_true: - m_var_signs.setx(x, l_true, l_undef); - break; - case l_false: - m_var_signs.setx(x, l_false, l_undef); - break; - default: - break; - } - } - } - - /** - \brief returns true then c is an equality that is equivalent to v*p + q, - and p > 0, v does not occur in p, q. - */ - bool solve_var(clause& c, var& v, polynomial_ref& p, polynomial_ref& q) { - poly* p0; - if (!is_unit_eq(c)) - return false; - ineq_atom & a = *to_ineq_atom(m_atoms[c[0].var()]); - if (!is_single_poly(a, p0)) - return false; - var mx = max_var(p0); - if (mx >= m_is_int.size()) - return false; - for (var x = 0; x <= mx; ++x) { - if (1 == m_pm.degree(p0, x)) { - p = m_pm.coeff(p0, x, 1, q); - if (!is_invertible(x, p)) - continue; - switch (m_pm.sign(p, m_var_signs)) { - case l_true: - v = x; - return true; - case l_false: - v = x; - p = -p; - q = -q; - return true; - default: - break; - } - } - } - return false; - } - + } bool is_unit(polynomial_ref const& p) { if (!m_pm.is_const(p)) @@ -3892,6 +3293,7 @@ namespace nlsat { case atom::ROOT_LE: out << "(<= "; proc(out, a.x()); out << " " << yn << ")"; break; case atom::ROOT_GE: out << "(>= "; proc(out, a.x()); out << " " << yn << ")"; break; case atom::ROOT_EQ: out << "(= "; proc(out, a.x()); out << " " << yn << ")"; NOT_IMPLEMENTED_YET(); break; + default: UNREACHABLE(); break; } out << "))"; return out; @@ -4058,12 +3460,14 @@ namespace nlsat { } std::ostream& display_assumptions(std::ostream & out, _assumption_set s) const { + if (!m_display_assumption) + return out; vector deps; m_asm.linearize(s, deps); bool first = true; for (auto dep : deps) { if (first) first = false; else out << " "; - if (m_display_assumption) (*m_display_assumption)(out, dep); + (*m_display_assumption)(out, dep); } return out; } @@ -4475,6 +3879,10 @@ namespace nlsat { #endif TRACE("nlsat", display(tout);); } + + void solver::del_clause(clause* c) { + m_imp->del_clause(c); + } var solver::mk_var(bool is_int) { return m_imp->mk_var(is_int); @@ -4484,8 +3892,8 @@ namespace nlsat { return m_imp->mk_ineq_atom(k, sz, ps, is_even); } - literal solver::mk_ineq_literal(atom::kind k, unsigned sz, poly * const * ps, bool const * is_even) { - return m_imp->mk_ineq_literal(k, sz, ps, is_even); + literal solver::mk_ineq_literal(atom::kind k, unsigned sz, poly * const * ps, bool const * is_even, bool simplify) { + return m_imp->mk_ineq_literal(k, sz, ps, is_even, simplify); } bool_var solver::mk_root_atom(atom::kind k, var x, unsigned i, poly * p) { @@ -4499,9 +3907,17 @@ namespace nlsat { void solver::dec_ref(bool_var b) { m_imp->dec_ref(b); } + + void solver::inc_ref(assumption a) { + m_imp->inc_ref(static_cast(a)); + } + + void solver::dec_ref(assumption a) { + m_imp->dec_ref(static_cast(a)); + } void solver::mk_clause(unsigned num_lits, literal * lits, assumption a) { - return m_imp->mk_clause(num_lits, lits, a); + return m_imp->mk_external_clause(num_lits, lits, a); } std::ostream& solver::display(std::ostream & out) const { @@ -4536,6 +3952,10 @@ namespace nlsat { return out; } + std::ostream& solver::display(std::ostream& out, clause const& c) const { + return m_imp->display(out, c); + } + std::ostream& solver::display_smt2(std::ostream & out) const { return m_imp->display_smt2(out); } @@ -4582,5 +4002,24 @@ namespace nlsat { return m_imp->collect_statistics(st); } + clause* solver::mk_clause(unsigned n, literal const* lits, bool learned, internal_assumption a) { + return m_imp->mk_clause(n, lits, learned, static_cast(a)); + } + + void solver::inc_simplify() { + m_imp->m_stats.m_simplifications++; + } + + bool solver::has_root_atom(clause const& c) const { + return m_imp->has_root_atom(c); + } + + void solver::add_bound(bound_constraint const& c) { + m_imp->m_bounds.push_back(c); + } + + assumption solver::join(assumption a, assumption b) { + return (m_imp->m_asm.mk_join(static_cast(a), static_cast(b))); + } }; diff --git a/src/nlsat/nlsat_solver.h b/src/nlsat/nlsat_solver.h index 15764150d..e3a57f653 100644 --- a/src/nlsat/nlsat_solver.h +++ b/src/nlsat/nlsat_solver.h @@ -24,6 +24,7 @@ Revision History: #include "util/params.h" #include "util/statistics.h" #include "util/rlimit.h" +#include "util/dependency.h" namespace nlsat { @@ -36,6 +37,15 @@ namespace nlsat { virtual std::ostream& operator()(std::ostream& out, assumption a) const = 0; }; + struct bound_constraint { + var x; + polynomial_ref A, B; + bool is_strict; + clause* c; + bound_constraint(var x, polynomial_ref& A, polynomial_ref& B, bool is_strict, clause* c) : + x(x), A(A), B(B), is_strict(is_strict), c(c) {} + }; + class solver { struct imp; struct ctx; @@ -103,7 +113,7 @@ namespace nlsat { e[i] = 1 if is_even[i] is false e[i] = 2 if is_even[i] is true */ - literal mk_ineq_literal(atom::kind k, unsigned sz, poly * const * ps, bool const * is_even); + literal mk_ineq_literal(atom::kind k, unsigned sz, poly * const * ps, bool const * is_even, bool simplify = false); /** \brief Create an atom of the form: x=root[i](p), xroot[i](p) @@ -114,6 +124,9 @@ namespace nlsat { void inc_ref(literal l) { inc_ref(l.var()); } void dec_ref(bool_var b); void dec_ref(literal l) { dec_ref(l.var()); } + void inc_ref(assumption a); + void dec_ref(assumption a); + /** \brief Create a new clause. @@ -172,6 +185,17 @@ namespace nlsat { void get_bvalues(svector const& bvars, svector& vs); void set_bvalues(svector const& vs); + /** + * \brief Access functions for simplify module. + */ + void del_clause(clause* c); + clause* mk_clause(unsigned n, literal const* lits, bool learned, internal_assumption a); + bool has_root_atom(clause const& c) const; + assumption join(assumption a, assumption b); + + void inc_simplify(); + void add_bound(bound_constraint const& c); + /** \brief reorder variables. */ @@ -244,6 +268,8 @@ namespace nlsat { std::ostream& display(std::ostream & out, unsigned n, literal const* ls) const; + std::ostream& display(std::ostream& out, clause const& c) const; + std::ostream& display(std::ostream & out, literal_vector const& ls) const; std::ostream& display(std::ostream & out, atom const& a) const; @@ -254,9 +280,10 @@ namespace nlsat { std::ostream& display_smt2(std::ostream & out, literal_vector const& ls) const; - std::ostream& display_smt2(std::ostream & out) const; + std::ostream& display_smt2(std::ostream & out) const; + /** \brief Display variable */ diff --git a/src/nlsat/nlsat_types.h b/src/nlsat/nlsat_types.h index a6071cdba..76999e9d4 100644 --- a/src/nlsat/nlsat_types.h +++ b/src/nlsat/nlsat_types.h @@ -32,6 +32,7 @@ namespace nlsat { #define NLSAT_VB_LVL 10 typedef void * assumption; typedef void * assumption_set; + typedef void * internal_assumption; typedef sat::bool_var bool_var; typedef sat::bool_var_vector bool_var_vector; @@ -74,6 +75,7 @@ namespace nlsat { } protected: friend class solver; + friend class simplify; kind m_kind; unsigned m_ref_count; bool_var m_bool_var; diff --git a/src/util/small_object_allocator.cpp b/src/util/small_object_allocator.cpp index bd980df34..879168721 100644 --- a/src/util/small_object_allocator.cpp +++ b/src/util/small_object_allocator.cpp @@ -28,6 +28,7 @@ Revision History: # include #endif + small_object_allocator::small_object_allocator(char const * id) { for (unsigned i = 0; i < NUM_SLOTS; i++) { m_chunks[i] = nullptr; @@ -98,7 +99,9 @@ void small_object_allocator::deallocate(size_t size, void * p) { void * small_object_allocator::allocate(size_t size) { - if (size == 0) return nullptr; + if (size == 0) + return nullptr; + #if defined(Z3DEBUG) && !defined(_WINDOWS) @@ -109,6 +112,8 @@ void * small_object_allocator::allocate(size_t size) { if (size >= SMALL_OBJ_SIZE - (1 << PTR_ALIGNMENT)) { return memory::allocate(size); } + + #ifdef Z3DEBUG size_t osize = size; #endif