diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp new file mode 100644 index 000000000..d50752460 --- /dev/null +++ b/src/nlsat/nlsat_solver.cpp @@ -0,0 +1,4219 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + nlsat_solver.cpp + +Abstract: + + Nonlinear arithmetic satisfiability procedure. The procedure is + complete for nonlinear real arithmetic, but it also has limited + support for integers. + +Author: + + Leonardo de Moura (leonardo) 2012-01-02. + +Revision History: + +--*/ +#include "util/z3_exception.h" +#include "util/chashtable.h" +#include "util/id_gen.h" +#include "util/map.h" +#include "util/dependency.h" +#include "util/permutation.h" +#include "math/polynomial/algebraic_numbers.h" +#include "math/polynomial/polynomial_cache.h" +#include "nlsat/nlsat_solver.h" +#include "nlsat/nlsat_clause.h" +#include "nlsat/nlsat_assignment.h" +#include "nlsat/nlsat_justification.h" +#include "nlsat/nlsat_evaluator.h" +#include "nlsat/nlsat_explain.h" +#include "nlsat/nlsat_params.hpp" +#include "nlsat/nlsat_simplify.h" +#include "nlsat/nlsat_simple_checker.h" +#include "nlsat/nlsat_variable_ordering_strategy.h" +#include "nlsat/nlsat_symmetry_checker.h" + +#define NLSAT_EXTRA_VERBOSE + +#ifdef NLSAT_EXTRA_VERBOSE +#define NLSAT_VERBOSE(CODE) IF_VERBOSE(10, CODE) +#else +#define NLSAT_VERBOSE(CODE) ((void)0) +#endif + +namespace nlsat { + + + typedef chashtable ineq_atom_table; + typedef chashtable root_atom_table; + + // for apply_permutation procedure + void swap(clause * & c1, clause * & c2) noexcept { + std::swap(c1, c2); + } + + struct solver::ctx { + params_ref m_params; + reslimit& m_rlimit; + small_object_allocator m_allocator; + unsynch_mpq_manager m_qm; + pmanager m_pm; + anum_manager m_am; + bool m_incremental; + ctx(reslimit& rlim, params_ref const & p, bool incremental): + m_params(p), + m_rlimit(rlim), + m_allocator("nlsat"), + m_pm(rlim, m_qm, &m_allocator), + m_am(rlim, m_qm, p, &m_allocator), + m_incremental(incremental) + {} + }; + + struct solver::imp { + + + struct dconfig { + typedef imp value_manager; + typedef small_object_allocator allocator; + typedef void* value; + static const bool ref_count = false; + }; + + typedef dependency_manager assumption_manager; + typedef assumption_manager::dependency* _assumption_set; + + typedef obj_ref assumption_set_ref; + + + typedef polynomial::cache cache; + typedef ptr_vector interval_set_vector; + + + + ctx& m_ctx; + solver& m_solver; + reslimit& m_rlimit; + small_object_allocator& m_allocator; + bool m_incremental; + unsynch_mpq_manager& m_qm; + pmanager& m_pm; + cache m_cache; + anum_manager& m_am; + mutable assumption_manager m_asm; + assignment m_assignment, m_lo, m_hi; // partial interpretation + evaluator m_evaluator; + interval_set_manager & m_ism; + ineq_atom_table m_ineq_atoms; + root_atom_table m_root_atoms; + + + vector m_bounds; + + id_gen m_cid_gen; + clause_vector m_clauses; // set of clauses + clause_vector m_learned; // set of learned clauses + clause_vector m_valids; + + unsigned m_num_bool_vars; + atom_vector m_atoms; // bool_var -> atom + svector m_bvalues; // boolean assignment + unsigned_vector m_levels; // bool_var -> level + svector m_justifications; + vector m_bwatches; // bool_var (that are not attached to atoms) -> clauses where it is maximal + 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. + atom_vector m_var2eq; // var -> to asserted equality + var_vector m_perm; // var -> var permutation of the variables + var_vector m_inv_perm; + // m_perm: internal -> external + // m_inv_perm: external -> internal + struct perm_display_var_proc : public display_var_proc { + var_vector & m_perm; + display_var_proc m_default_display_var; + display_var_proc const * m_proc; // display external var ids + perm_display_var_proc(var_vector & perm): + m_perm(perm), + m_proc(nullptr) { + } + std::ostream& operator()(std::ostream & out, var x) const override { + if (m_proc == nullptr) + m_default_display_var(out, x); + else + (*m_proc)(out, m_perm[x]); + return out; + } + }; + perm_display_var_proc m_display_var; + + display_assumption_proc const* m_display_assumption; + struct display_literal_assumption : public display_assumption_proc { + imp& i; + literal_vector const& lits; + display_literal_assumption(imp& i, literal_vector const& lits): i(i), lits(lits) {} + std::ostream& operator()(std::ostream& out, assumption a) const override { + if (lits.begin() <= a && a < lits.end()) { + out << *((literal const*)a); + } + else if (i.m_display_assumption) { + (*i.m_display_assumption)(out, a); + } + return out; + } + + }; + struct scoped_display_assumptions { + imp& i; + display_assumption_proc const* m_save; + scoped_display_assumptions(imp& i, display_assumption_proc const& p): i(i), m_save(i.m_display_assumption) { + i.m_display_assumption = &p; + } + ~scoped_display_assumptions() { + i.m_display_assumption = m_save; + } + }; + + explain m_explain; + + bool_var m_bk; // current Boolean variable we are processing + var m_xk; // current arith variable we are processing + + 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; + union { + bool_var m_b; + interval_set * m_old_set; + atom * m_old_eq; + }; + 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 s, stage):m_kind(s ? NEW_STAGE : NEW_LEVEL) {} + trail(atom * a):m_kind(UPDT_EQ), m_old_eq(a) {} + }; + svector m_trail; + + anum m_zero; + + // configuration + unsigned long long m_max_memory; + unsigned m_lazy; // how lazy the solver is: 0 - satisfy all learned clauses, 1 - process only unit and empty learned clauses, 2 - use only conflict clauses for resolving conflicts + bool m_simplify_cores; + bool m_reorder; + bool m_randomize; + bool m_random_order; + unsigned m_random_seed; + bool m_inline_vars; + bool m_log_lemmas; + bool m_check_lemmas; + unsigned m_max_conflicts; + unsigned m_lemma_count; +//#linxi begin + bool m_linxi_simple_check; + unsigned m_linxi_variable_ordering_strategy; + bool m_linxi_symmetry_check; + bool m_linxi_set_0_more; + bool m_cell_sample; +//#linxi end + + 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 + stats m_stats; + + imp(solver& s, ctx& c): + m_ctx(c), + m_solver(s), + m_rlimit(c.m_rlimit), + m_allocator(c.m_allocator), + m_incremental(c.m_incremental), + m_qm(c.m_qm), + m_pm(c.m_pm), + m_cache(m_pm), + m_am(c.m_am), + m_asm(*this, m_allocator), + m_assignment(m_am), m_lo(m_am), m_hi(m_am), + 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, nlsat_params(c.m_params).cell_sample()), + m_scope_lvl(0), + m_lemma(s), + m_lazy_clause(s), + m_lemma_assumptions(m_asm) { + updt_params(c.m_params); + reset_statistics(); + mk_true_bvar(); + m_lemma_count = 0; + } + + ~imp() { + clear(); + } + + void mk_true_bvar() { + bool_var b = mk_bool_var(); + SASSERT(b == true_bool_var); + literal true_lit(b, false); + mk_clause(1, &true_lit, false, nullptr); + } + + void updt_params(params_ref const & _p) { + nlsat_params p(_p); + m_max_memory = p.max_memory(); + m_lazy = p.lazy(); + m_simplify_cores = p.simplify_conflicts(); + bool min_cores = p.minimize_conflicts(); + m_reorder = p.reorder(); + m_randomize = p.randomize(); + m_max_conflicts = p.max_conflicts(); + m_random_order = p.shuffle_vars(); + m_random_seed = p.seed(); + m_inline_vars = p.inline_vars(); + m_log_lemmas = p.log_lemmas(); + m_check_lemmas = p.check_lemmas(); +//#linxi begin + m_linxi_simple_check = p.linxi_simple_check(); + m_linxi_variable_ordering_strategy = p.linxi_variable_ordering_strategy(); + m_linxi_symmetry_check = p.linxi_symmetry_check(); +//#linxi end + + + m_cell_sample = p.cell_sample(); + + + m_ism.set_seed(m_random_seed); + m_explain.set_simplify_cores(m_simplify_cores); + m_explain.set_minimize_cores(min_cores); + m_explain.set_factor(p.factor()); + m_am.updt_params(p.p); + } + + void reset() { + m_explain.reset(); + m_lemma.reset(); + m_lazy_clause.reset(); + undo_until_size(0); + del_clauses(); + del_unref_atoms(); + m_cache.reset(); + m_assignment.reset(); + m_lo.reset(); + m_hi.reset(); + } + + void clear() { + m_explain.reset(); + m_lemma.reset(); + m_lazy_clause.reset(); + undo_until_size(0); + del_clauses(); + del_unref_atoms(); + } + + void checkpoint() { + if (!m_rlimit.inc()) throw solver_exception(m_rlimit.get_cancel_msg()); + if (memory::get_allocation_size() > m_max_memory) throw solver_exception(Z3_MAX_MEMORY_MSG); + } + + // ----------------------- + // + // Basic + // + // ----------------------- + + unsigned num_bool_vars() const { + return m_num_bool_vars; + } + + unsigned num_vars() const { + return m_is_int.size(); + } + + bool is_int(var x) const { + return m_is_int[x]; + } + + void inc_ref(assumption) {} + + void dec_ref(assumption) {} + + 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); + } + + void inc_ref(bool_var b) { + if (b == null_bool_var) + return; + atom * a = m_atoms[b]; + if (a == nullptr) + return; + TRACE("ref", display(tout << "inc: " << b << " " << a->ref_count() << " ", *a) << "\n";); + a->inc_ref(); + } + + void inc_ref(literal l) { + inc_ref(l.var()); + } + + void dec_ref(bool_var b) { + if (b == null_bool_var) + return; + atom * a = m_atoms[b]; + if (a == nullptr) + return; + SASSERT(a->ref_count() > 0); + a->dec_ref(); + TRACE("ref", display(tout << "dec: " << b << " " << a->ref_count() << " ", *a) << "\n";); + if (a->ref_count() == 0) + del(a); + } + + void dec_ref(literal l) { + dec_ref(l.var()); + } + + bool is_arith_atom(bool_var b) const { return m_atoms[b] != nullptr; } + + bool is_arith_literal(literal l) const { return is_arith_atom(l.var()); } + + var max_var(poly const * p) const { + return m_pm.max_var(p); + } + + var max_var(bool_var b) const { + if (!is_arith_atom(b)) + return null_var; + else + return m_atoms[b]->max_var(); + } + + var max_var(literal l) const { + return max_var(l.var()); + } + + /** + \brief Return the maximum variable occurring in cls. + */ + var max_var(unsigned sz, literal const * cls) const { + var x = null_var; + for (unsigned i = 0; i < sz; i++) { + literal l = cls[i]; + if (is_arith_literal(l)) { + var y = max_var(l); + if (x == null_var || y > x) + x = y; + } + } + return x; + } + + var max_var(clause const & cls) const { + return max_var(cls.size(), cls.data()); + } + + /** + \brief Return the maximum Boolean variable occurring in cls. + */ + bool_var max_bvar(clause const & cls) const { + bool_var b = null_bool_var; + for (literal l : cls) { + if (b == null_bool_var || l.var() > b) + b = l.var(); + } + return b; + } + + /** + \brief Return the degree of the maximal variable of the given atom + */ + unsigned degree(atom const * a) const { + if (a->is_ineq_atom()) { + unsigned max = 0; + unsigned sz = to_ineq_atom(a)->size(); + var x = a->max_var(); + for (unsigned i = 0; i < sz; i++) { + unsigned d = m_pm.degree(to_ineq_atom(a)->p(i), x); + if (d > max) + max = d; + } + return max; + } + else { + return m_pm.degree(to_root_atom(a)->p(), a->max_var()); + } + } + + /** + \brief Return the degree of the maximal variable in c + */ + unsigned degree(clause const & c) const { + var x = max_var(c); + if (x == null_var) + return 0; + unsigned max = 0; + for (literal l : c) { + atom const * a = m_atoms[l.var()]; + if (a == nullptr) + continue; + unsigned d = degree(a); + if (d > max) + max = d; + } + return max; + } + + // ----------------------- + // + // Variable, Atoms, Clauses & Assumption creation + // + // ----------------------- + + bool_var mk_bool_var_core() { + bool_var b = m_bid_gen.mk(); + m_num_bool_vars++; + m_atoms .setx(b, nullptr, nullptr); + m_bvalues .setx(b, l_undef, l_undef); + m_levels .setx(b, UINT_MAX, UINT_MAX); + m_justifications.setx(b, null_justification, null_justification); + m_bwatches .setx(b, clause_vector(), clause_vector()); + m_dead .setx(b, false, true); + return b; + } + + bool_var mk_bool_var() { + return mk_bool_var_core(); + } + + var mk_var(bool is_int) { + var x = m_pm.mk_var(); + register_var(x, is_int); + return x; + } + void register_var(var x, bool is_int) { + SASSERT(x == num_vars()); + m_is_int. push_back(is_int); + m_watches. push_back(clause_vector()); + m_infeasible.push_back(nullptr); + m_var2eq. push_back(nullptr); + m_perm. push_back(x); + m_inv_perm. push_back(x); + SASSERT(m_is_int.size() == m_watches.size()); + SASSERT(m_is_int.size() == m_infeasible.size()); + SASSERT(m_is_int.size() == m_var2eq.size()); + SASSERT(m_is_int.size() == m_perm.size()); + SASSERT(m_is_int.size() == m_inv_perm.size()); + } + + bool_vector m_found_vars; + void vars(literal l, var_vector& vs) { + vs.reset(); + atom * a = m_atoms[l.var()]; + if (a == nullptr) { + + } + else if (a->is_ineq_atom()) { + unsigned sz = to_ineq_atom(a)->size(); + var_vector new_vs; + for (unsigned j = 0; j < sz; j++) { + m_found_vars.reset(); + m_pm.vars(to_ineq_atom(a)->p(j), new_vs); + for (unsigned i = 0; i < new_vs.size(); ++i) { + if (!m_found_vars.get(new_vs[i], false)) { + m_found_vars.setx(new_vs[i], true, false); + vs.push_back(new_vs[i]); + } + } + } + } + else { + m_pm.vars(to_root_atom(a)->p(), vs); + //vs.erase(max_var(to_root_atom(a)->p())); + vs.push_back(to_root_atom(a)->x()); + } + } + + void deallocate(ineq_atom * a) { + unsigned obj_sz = ineq_atom::get_obj_size(a->size()); + a->~ineq_atom(); + m_allocator.deallocate(obj_sz, a); + } + + void deallocate(root_atom * a) { + a->~root_atom(); + m_allocator.deallocate(sizeof(root_atom), a); + } + + void del(bool_var b) { + SASSERT(m_bwatches[b].empty()); + //SASSERT(m_bvalues[b] == l_undef); + m_num_bool_vars--; + m_dead[b] = true; + m_atoms[b] = nullptr; + m_bvalues[b] = l_undef; + m_bid_gen.recycle(b); + } + + void del(ineq_atom * a) { + CTRACE("nlsat_solver", a->ref_count() > 0, display(tout, *a) << "\n";); + // this triggers in too many benign cases: + // SASSERT(a->ref_count() == 0); + m_ineq_atoms.erase(a); + del(a->bvar()); + unsigned sz = a->size(); + for (unsigned i = 0; i < sz; i++) + m_pm.dec_ref(a->p(i)); + deallocate(a); + } + + void del(root_atom * a) { + SASSERT(a->ref_count() == 0); + m_root_atoms.erase(a); + del(a->bvar()); + m_pm.dec_ref(a->p()); + deallocate(a); + } + + void del(atom * a) { + if (a == nullptr) + return; + TRACE("nlsat_verbose", display(tout << "del: b" << a->m_bool_var << " " << a->ref_count() << " ", *a) << "\n";); + if (a->is_ineq_atom()) + del(to_ineq_atom(a)); + else + del(to_root_atom(a)); + } + + // Delete atoms with ref_count == 0 + void del_unref_atoms() { + for (auto* a : m_atoms) { + del(a); + } + } + + + 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; + polynomial_ref p(m_pm); + ptr_buffer uniq_ps; + var max = null_var; + for (unsigned i = 0; i < sz; i++) { + p = m_pm.flip_sign_if_lm_neg(ps[i]); + if (p.get() != ps[i] && !is_even[i]) { + sign = -sign; + } + 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) + k = atom::flip(k); + ineq_atom * tmp_atom = new (mem) ineq_atom(k, sz, uniq_ps.data(), is_even, max); + ineq_atom * atom = m_ineq_atoms.insert_if_not_there(tmp_atom); + CTRACE("nlsat_table_bug", tmp_atom != atom, ineq_atom::hash_proc h; + tout << "mk_ineq_atom hash: " << h(tmp_atom) << "\n"; display(tout, *tmp_atom, m_display_var) << "\n";); + CTRACE("nlsat_table_bug", atom->max_var() != max, display(tout << "nonmax: ", *atom, m_display_var) << "\n";); + SASSERT(atom->max_var() == max); + is_new = (atom == tmp_atom); + if (is_new) { + for (unsigned i = 0; i < sz; i++) { + m_pm.inc_ref(atom->p(i)); + } + } + else { + deallocate(tmp_atom); + } + return atom; + } + + 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, simplify); + if (!is_new) { + return atom->bvar(); + } + else { + bool_var b = mk_bool_var_core(); + m_atoms[b] = atom; + atom->m_bool_var = b; + TRACE("nlsat_verbose", display(tout << "create: b" << atom->m_bool_var << " ", *atom) << "\n";); + return b; + } + } + + 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()); + m_pm.m().set(cnst, 1); + for (unsigned i = 0; i < sz; ++i) { + if (m_pm.is_const(ps[i])) { + if (m_pm.is_zero(ps[i])) { + m_pm.m().set(cnst, 0); + is_const = true; + break; + } + auto const& c = m_pm.coeff(ps[i], 0); + m_pm.m().mul(cnst, c, cnst); + if (is_even[i] && m_pm.m().is_neg(c)) { + m_pm.m().neg(cnst); + } + } + else { + is_const = false; + } + } + if (is_const) { + if (m_pm.m().is_pos(cnst) && k == atom::GT) return true_literal; + if (m_pm.m().is_neg(cnst) && k == atom::LT) return true_literal; + 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, simplify), false); + } + + bool_var mk_root_atom(atom::kind k, var x, unsigned i, poly * p) { + polynomial_ref p1(m_pm), uniq_p(m_pm); + p1 = m_pm.flip_sign_if_lm_neg(p); // flipping the sign of the polynomial will not change its roots. + uniq_p = m_cache.mk_unique(p1); + TRACE("nlsat_solver", tout << x << " " << p1 << " " << uniq_p << "\n";); + SASSERT(i > 0); + SASSERT(x >= max_var(p)); + SASSERT(k == atom::ROOT_LT || k == atom::ROOT_GT || k == atom::ROOT_EQ || k == atom::ROOT_LE || k == atom::ROOT_GE); + + void * mem = m_allocator.allocate(sizeof(root_atom)); + root_atom * new_atom = new (mem) root_atom(k, x, i, uniq_p); + root_atom * old_atom = m_root_atoms.insert_if_not_there(new_atom); + SASSERT(old_atom->max_var() == x); + if (old_atom != new_atom) { + deallocate(new_atom); + return old_atom->bvar(); + } + bool_var b = mk_bool_var_core(); + m_atoms[b] = new_atom; + new_atom->m_bool_var = b; + m_pm.inc_ref(new_atom->p()); + return b; + } + + void attach_clause(clause & cls) { + var x = max_var(cls); + if (x != null_var) { + m_watches[x].push_back(&cls); + } + else { + bool_var b = max_bvar(cls); + m_bwatches[b].push_back(&cls); + } + } + + void deattach_clause(clause & cls) { + var x = max_var(cls); + if (x != null_var) { + m_watches[x].erase(&cls); + } + else { + bool_var b = max_bvar(cls); + m_bwatches[b].erase(&cls); + } + } + + void deallocate(clause * cls) { + size_t obj_sz = clause::get_obj_size(cls->size()); + cls->~clause(); + m_allocator.deallocate(obj_sz, cls); + } + + void del_clause(clause * cls) { + deattach_clause(*cls); + m_cid_gen.recycle(cls->id()); + unsigned sz = cls->size(); + for (unsigned i = 0; i < sz; i++) + dec_ref((*cls)[i]); + _assumption_set a = static_cast<_assumption_set>(cls->assumptions()); + dec_ref(a); + deallocate(cls); + } + + void del_clause(clause * cls, clause_vector& clauses) { + clauses.erase(cls); + del_clause(cls); + } + + void del_clauses(ptr_vector & cs) { + for (clause* cp : cs) + del_clause(cp); + cs.reset(); + } + + void del_clauses() { + del_clauses(m_clauses); + del_clauses(m_learned); + del_clauses(m_valids); + } + + // We use a simple heuristic to sort literals + // - bool literals < arith literals + // - sort literals based on max_var + // - sort literal with the same max_var using degree + // break ties using the fact that ineqs are usually cheaper to process than eqs. + struct lit_lt { + imp & m; + lit_lt(imp & _m):m(_m) {} + + bool operator()(literal l1, literal l2) const { + atom * a1 = m.m_atoms[l1.var()]; + atom * a2 = m.m_atoms[l2.var()]; + if (a1 == nullptr && a2 == nullptr) + return l1.index() < l2.index(); + if (a1 == nullptr) + return true; + if (a2 == nullptr) + return false; + var x1 = a1->max_var(); + var x2 = a2->max_var(); + if (x1 < x2) + return true; + if (x1 > x2) + return false; + SASSERT(x1 == x2); + unsigned d1 = m.degree(a1); + unsigned d2 = m.degree(a2); + if (d1 < d2) + return true; + if (d1 > d2) + return false; + if (!a1->is_eq() && a2->is_eq()) + return true; + if (a1->is_eq() && !a2->is_eq()) + return false; + return l1.index() < l2.index(); + } + }; + + class scoped_bool_vars { + imp& s; + svector vec; + public: + scoped_bool_vars(imp& s):s(s) {} + ~scoped_bool_vars() { + for (bool_var v : vec) { + s.dec_ref(v); + } + } + void push_back(bool_var v) { + s.inc_ref(v); + vec.push_back(v); + } + bool_var const* begin() const { return vec.begin(); } + bool_var const* end() const { return vec.end(); } + bool_var operator[](bool_var v) const { return vec[v]; } + }; + + void check_lemma(unsigned n, literal const* cls, bool is_valid, assumption_set a) { + TRACE("nlsat", display(tout << "check lemma: ", n, cls) << "\n"; + display(tout);); + IF_VERBOSE(2, display(verbose_stream() << "check lemma " << (is_valid?"valid: ":"consequence: "), n, cls) << "\n"); + for (clause* c : m_learned) IF_VERBOSE(1, display(verbose_stream() << "lemma: ", *c) << "\n"); + scoped_suspend_rlimit _limit(m_rlimit); + ctx c(m_rlimit, m_ctx.m_params, m_ctx.m_incremental); + solver solver2(c); + imp& checker = *(solver2.m_imp); + checker.m_check_lemmas = false; + checker.m_log_lemmas = false; + checker.m_inline_vars = false; + + auto pconvert = [&](poly* p) { + return convert(m_pm, p, checker.m_pm); + }; + + // need to translate Boolean variables and literals + scoped_bool_vars tr(checker); + for (var x = 0; x < m_is_int.size(); ++x) { + checker.register_var(x, is_int(x)); + } + bool_var bv = 0; + tr.push_back(bv); + for (bool_var b = 1; b < m_atoms.size(); ++b) { + atom* a = m_atoms[b]; + if (a == nullptr) { + bv = checker.mk_bool_var(); + } + else if (a->is_ineq_atom()) { + ineq_atom& ia = *to_ineq_atom(a); + unsigned sz = ia.size(); + polynomial_ref_vector ps(checker.m_pm); + bool_vector is_even; + for (unsigned i = 0; i < sz; ++i) { + ps.push_back(pconvert(ia.p(i))); + is_even.push_back(ia.is_even(i)); + } + bv = checker.mk_ineq_atom(ia.get_kind(), sz, ps.data(), is_even.data()); + } + else if (a->is_root_atom()) { + root_atom& r = *to_root_atom(a); + if (r.x() >= max_var(r.p())) { + // permutation may be reverted after check completes, + // but then root atoms are not used in lemmas. + bv = checker.mk_root_atom(r.get_kind(), r.x(), r.i(), pconvert(r.p())); + } + } + else { + UNREACHABLE(); + } + tr.push_back(bv); + } + if (!is_valid) { + for (clause* c : m_clauses) { + if (!a && c->assumptions()) { + continue; + } + literal_vector lits; + for (literal lit : *c) { + lits.push_back(literal(tr[lit.var()], lit.sign())); + } + 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_external_clause(1, &nlit, nullptr); + } + lbool r = checker.check(); + if (r == l_true) { + for (bool_var b : tr) { + literal lit(b, false); + IF_VERBOSE(0, checker.display(verbose_stream(), lit) << " := " << checker.value(lit) << "\n"); + TRACE("nlsat", checker.display(tout, lit) << " := " << checker.value(lit) << "\n";); + } + for (clause* c : m_learned) { + bool found = false; + for (literal lit: *c) { + literal tlit(tr[lit.var()], lit.sign()); + found |= checker.value(tlit) == l_true; + } + if (!found) { + IF_VERBOSE(0, display(verbose_stream() << "violdated clause: ", *c) << "\n"); + TRACE("nlsat", display(tout << "violdated clause: ", *c) << "\n";); + } + } + for (clause* c : m_valids) { + bool found = false; + for (literal lit: *c) { + literal tlit(tr[lit.var()], lit.sign()); + found |= checker.value(tlit) == l_true; + } + if (!found) { + IF_VERBOSE(0, display(verbose_stream() << "violdated tautology clause: ", *c) << "\n"); + TRACE("nlsat", display(tout << "violdated tautology clause: ", *c) << "\n";); + } + } + throw default_exception("lemma did not check"); + UNREACHABLE(); + } + } + + void log_lemma(std::ostream& out, clause const& cls) { + log_lemma(out, cls.size(), cls.data(), false); + } + + void log_lemma(std::ostream& out, unsigned n, literal const* cls, bool is_valid) { + ++m_lemma_count; + out << "(set-logic NRA)\n"; + if (is_valid) { + display_smt2_bool_decls(out); + display_smt2_arith_decls(out); + } + else + display_smt2(out); + for (unsigned i = 0; i < n; ++i) + display_smt2(out << "(assert ", ~cls[i]) << ")\n"; + display(out << "(echo \"#" << m_lemma_count << " ", n, cls) << "\")\n"; + out << "(check-sat)\n(reset)\n"; + + TRACE("nlsat", display(tout << "(echo \"#" << m_lemma_count << " ", n, cls) << "\")\n"); + } + + clause * mk_clause_core(unsigned num_lits, literal const * lits, bool learned, _assumption_set a) { + SASSERT(num_lits > 0); + unsigned cid = m_cid_gen.mk(); + void * mem = m_allocator.allocate(clause::get_obj_size(num_lits)); + clause * cls = new (mem) clause(cid, num_lits, lits, learned, a); + for (unsigned i = 0; i < num_lits; i++) + inc_ref(lits[i]); + inc_ref(a); + return cls; + } + + 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";); + std::sort(cls->begin(), cls->end(), lit_lt(*this)); + TRACE("nlsat", display(tout << " after sort:\n", *cls) << "\n";); + if (learned && m_log_lemmas) { + log_lemma(verbose_stream(), *cls); + } + if (learned && m_check_lemmas && false) { + check_lemma(cls->size(), cls->data(), false, cls->assumptions()); + } + if (learned) + m_learned.push_back(cls); + else + m_clauses.push_back(cls); + attach_clause(*cls); + return cls; + } + + 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); + if (num_lits == 0) { + num_lits = 1; + lits = &false_literal; + } + mk_clause(num_lits, lits, false, as); + } + + // ----------------------- + // + // Search + // + // ----------------------- + + void save_assign_trail(bool_var b) { + m_trail.push_back(trail(b, bvar_assignment())); + } + + void save_set_updt_trail(interval_set * old_set) { + m_trail.push_back(trail(old_set)); + } + + void save_updt_eq_trail(atom * old_eq) { + m_trail.push_back(trail(old_eq)); + } + + void save_new_stage_trail() { + m_trail.push_back(trail(true, stage())); + } + + void save_new_level_trail() { + m_trail.push_back(trail(false, stage())); + } + + void undo_bvar_assignment(bool_var b) { + m_bvalues[b] = l_undef; + m_levels[b] = UINT_MAX; + del_jst(m_allocator, m_justifications[b]); + m_justifications[b] = null_justification; + if (m_atoms[b] == nullptr && b < m_bk) + m_bk = b; + } + + void undo_set_updt(interval_set * old_set) { + if (m_xk == null_var) + return; + var x = m_xk; + if (x < m_infeasible.size()) { + m_ism.dec_ref(m_infeasible[x]); + m_infeasible[x] = old_set; + } + } + + void undo_new_stage() { + if (m_xk == 0) { + m_xk = null_var; + } + else if (m_xk != null_var) { + m_xk--; + m_assignment.reset(m_xk); + } + } + + void undo_new_level() { + SASSERT(m_scope_lvl > 0); + m_scope_lvl--; + m_evaluator.pop(1); + } + + void undo_updt_eq(atom * a) { + if (m_var2eq.size() > m_xk) + m_var2eq[m_xk] = a; + } + + template + void undo_until(Predicate const & pred) { + while (pred() && !m_trail.empty()) { + trail & t = m_trail.back(); + switch (t.m_kind) { + case trail::BVAR_ASSIGNMENT: + undo_bvar_assignment(t.m_b); + break; + case trail::INFEASIBLE_UPDT: + undo_set_updt(t.m_old_set); + break; + case trail::NEW_STAGE: + undo_new_stage(); + break; + case trail::NEW_LEVEL: + undo_new_level(); + break; + case trail::UPDT_EQ: + undo_updt_eq(t.m_old_eq); + break; + default: + break; + } + m_trail.pop_back(); + } + } + + struct size_pred { + svector & m_trail; + unsigned m_old_size; + size_pred(svector & trail, unsigned old_size):m_trail(trail), m_old_size(old_size) {} + bool operator()() const { return m_trail.size() > m_old_size; } + }; + + // Keep undoing until trail has the given size + void undo_until_size(unsigned old_size) { + SASSERT(m_trail.size() >= old_size); + undo_until(size_pred(m_trail, old_size)); + } + + struct stage_pred { + var const & m_xk; + var m_target; + stage_pred(var const & xk, var target):m_xk(xk), m_target(target) {} + bool operator()() const { return m_xk != m_target; } + }; + + // Keep undoing until stage is new_xk + void undo_until_stage(var new_xk) { + undo_until(stage_pred(m_xk, new_xk)); + } + + struct level_pred { + unsigned const & m_scope_lvl; + unsigned m_new_lvl; + level_pred(unsigned const & scope_lvl, unsigned new_lvl):m_scope_lvl(scope_lvl), m_new_lvl(new_lvl) {} + bool operator()() const { return m_scope_lvl > m_new_lvl; } + }; + + // Keep undoing until level is new_lvl + void undo_until_level(unsigned new_lvl) { + undo_until(level_pred(m_scope_lvl, new_lvl)); + } + + struct unassigned_pred { + bool_var m_b; + svector const & m_bvalues; + unassigned_pred(svector const & bvalues, bool_var b): + m_b(b), + m_bvalues(bvalues) {} + bool operator()() const { return m_bvalues[m_b] != l_undef; } + }; + + // Keep undoing until b is unassigned + void undo_until_unassigned(bool_var b) { + undo_until(unassigned_pred(m_bvalues, b)); + SASSERT(m_bvalues[b] == l_undef); + } + + struct true_pred { + bool operator()() const { return true; } + }; + + void undo_until_empty() { + undo_until(true_pred()); + } + + /** + \brief Create a new scope level + */ + void new_level() { + m_evaluator.push(); + m_scope_lvl++; + save_new_level_trail(); + } + + /** + \brief Return the value of the given literal that was assigned by the search + engine. + */ + lbool assigned_value(literal l) const { + bool_var b = l.var(); + if (l.sign()) + return ~m_bvalues[b]; + else + return m_bvalues[b]; + } + + /** + \brief Assign literal using the given justification + */ + void assign(literal l, justification j) { + TRACE("nlsat_assign", + display(tout << "assigning literal: ", l); + display(tout << " <- ", j);); + + SASSERT(assigned_value(l) == l_undef); + SASSERT(j != null_justification); + SASSERT(!j.is_null()); + if (j.is_decision()) + m_stats.m_decisions++; + else + m_stats.m_propagations++; + bool_var b = l.var(); + m_bvalues[b] = to_lbool(!l.sign()); + m_levels[b] = m_scope_lvl; + m_justifications[b] = j; + save_assign_trail(b); + updt_eq(b, j); + TRACE("nlsat_assign", tout << "b" << b << " -> " << m_bvalues[b] << "\n";); + } + + /** + \brief Create a "case-split" + */ + void decide(literal l) { + new_level(); + assign(l, decided_justification); + } + + /** + \brief Return the value of a literal as defined in Dejan and Leo's paper. + */ + lbool value(literal l) { + lbool val = assigned_value(l); + if (val != l_undef) { + TRACE("nlsat_verbose", display(tout << " assigned value " << val << " for ", l) << "\n";); + return val; + } + bool_var b = l.var(); + atom * a = m_atoms[b]; + if (a == nullptr) { + TRACE("nlsat_verbose", display(tout << " no atom for ", l) << "\n";); + return l_undef; + } + var max = a->max_var(); + if (!m_assignment.is_assigned(max)) { + TRACE("nlsat_verbose", display(tout << " maximal variable not assigned ", l) << "\n";); + return l_undef; + } + val = to_lbool(m_evaluator.eval(a, l.sign())); + TRACE("nlsat_verbose", display(tout << " evaluated value " << val << " for ", l) << "\n";); + TRACE("value_bug", tout << "value of: "; display(tout, l); tout << " := " << val << "\n"; + tout << "xk: " << m_xk << ", a->max_var(): " << a->max_var() << "\n"; + display_assignment(tout);); + return val; + } + + /** + \brief Return true if the given clause is already satisfied in the current partial interpretation. + */ + bool is_satisfied(clause const & cls) const { + for (literal l : cls) { + if (const_cast(this)->value(l) == l_true) { + TRACE("value_bug:", tout << l << " := true\n";); + return true; + } + } + return false; + } + + /** + \brief Return true if the given clause is false in the current partial interpretation. + */ + bool is_inconsistent(unsigned sz, literal const * cls) { + for (unsigned i = 0; i < sz; i++) { + if (value(cls[i]) != l_false) { + TRACE("is_inconsistent", tout << "literal is not false:\n"; display(tout, cls[i]); tout << "\n";); + return false; + } + } + return true; + } + + /** + \brief Process a clauses that contains only Boolean literals. + */ + bool process_boolean_clause(clause const & cls) { + SASSERT(m_xk == null_var); + unsigned num_undef = 0; + unsigned first_undef = UINT_MAX; + unsigned sz = cls.size(); + for (unsigned i = 0; i < sz; i++) { + literal l = cls[i]; + SASSERT(m_atoms[l.var()] == nullptr); + SASSERT(value(l) != l_true); + if (value(l) == l_false) + continue; + SASSERT(value(l) == l_undef); + num_undef++; + if (first_undef == UINT_MAX) + first_undef = i; + } + if (num_undef == 0) + return false; + SASSERT(first_undef != UINT_MAX); + if (num_undef == 1) + assign(cls[first_undef], mk_clause_jst(&cls)); // unit clause + else + decide(cls[first_undef]); + return true; + } + + /** + \brief assign l to true, because l + (justification of) s is infeasible in RCF in the current interpretation. + */ + literal_vector core; + ptr_vector clauses; + void R_propagate(literal l, interval_set const * s, bool include_l = true) { + m_ism.get_justifications(s, core, clauses); + if (include_l) + core.push_back(~l); + auto j = mk_lazy_jst(m_allocator, core.size(), core.data(), clauses.size(), clauses.data()); + TRACE("nlsat_resolve", display(tout, j); display_eval(tout << "evaluated:", j)); + assign(l, j); + SASSERT(value(l) == l_true); + } + + /** + \brief m_infeasible[m_xk] <- m_infeasible[m_xk] Union s + */ + void updt_infeasible(interval_set const * s) { + SASSERT(m_xk != null_var); + interval_set * xk_set = m_infeasible[m_xk]; + save_set_updt_trail(xk_set); + interval_set_ref new_set(m_ism); + TRACE("nlsat_inf_set", tout << "updating infeasible set\n"; m_ism.display(tout, xk_set) << "\n"; m_ism.display(tout, s) << "\n";); + new_set = m_ism.mk_union(s, xk_set); + TRACE("nlsat_inf_set", tout << "new infeasible set:\n"; m_ism.display(tout, new_set) << "\n";); + SASSERT(!m_ism.is_full(new_set)); + m_ism.inc_ref(new_set); + m_infeasible[m_xk] = new_set; + } + + /** + \brief Update m_var2eq mapping. + */ + void updt_eq(bool_var b, justification j) { + if (!m_simplify_cores) + return; + if (m_bvalues[b] != l_true) + return; + atom * a = m_atoms[b]; + if (a == nullptr || a->get_kind() != atom::EQ || to_ineq_atom(a)->size() > 1 || to_ineq_atom(a)->is_even(0)) + return; + switch (j.get_kind()) { + case justification::CLAUSE: + if (j.get_clause()->assumptions() != nullptr) return; + break; + case justification::LAZY: + if (j.get_lazy()->num_clauses() > 0) return; + if (j.get_lazy()->num_lits() > 0) return; + break; + default: + break; + } + var x = m_xk; + SASSERT(a->max_var() == x); + 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("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; + } + + /** + \brief Process a clause that contains nonlinear arithmetic literals + + If satisfy_learned is true, then learned clauses are satisfied even if m_lazy > 0 + */ + bool process_arith_clause(clause const & cls, bool satisfy_learned) { + if (!satisfy_learned && m_lazy >= 2 && cls.is_learned()) { + TRACE("nlsat", tout << "skip learned\n";); + return true; // ignore lemmas in super lazy mode + } + SASSERT(m_xk == max_var(cls)); + unsigned num_undef = 0; // number of undefined literals + unsigned first_undef = UINT_MAX; // position of the first undefined literal + interval_set_ref first_undef_set(m_ism); // infeasible region of the first undefined literal + interval_set * xk_set = m_infeasible[m_xk]; // current set of infeasible interval for current variable + SASSERT(!m_ism.is_full(xk_set)); + for (unsigned idx = 0; idx < cls.size(); ++idx) { + literal l = cls[idx]; + checkpoint(); + if (value(l) == l_false) + continue; + if (value(l) == l_true) + return true; // could happen if clause is a tautology + CTRACE("nlsat", max_var(l) != m_xk || value(l) != l_undef, display(tout); + tout << "xk: " << m_xk << ", max_var(l): " << max_var(l) << ", l: "; display(tout, l) << "\n"; + display(tout, cls) << "\n";); + SASSERT(value(l) == l_undef); + SASSERT(max_var(l) == m_xk); + bool_var b = l.var(); + atom * a = m_atoms[b]; + SASSERT(a != nullptr); + interval_set_ref curr_set(m_ism); + curr_set = m_evaluator.infeasible_intervals(a, l.sign(), &cls); + TRACE("nlsat_inf_set", tout << "infeasible set for literal: "; display(tout, l); tout << "\n"; m_ism.display(tout, curr_set); tout << "\n"; + display(tout, cls) << "\n";); + if (m_ism.is_empty(curr_set)) { + TRACE("nlsat_inf_set", tout << "infeasible set is empty, found literal\n";); + R_propagate(l, nullptr); + SASSERT(is_satisfied(cls)); + return true; + } + if (m_ism.is_full(curr_set)) { + TRACE("nlsat_inf_set", tout << "infeasible set is R, skip literal\n";); + R_propagate(~l, nullptr); + continue; + } + if (m_ism.subset(curr_set, xk_set)) { + TRACE("nlsat_inf_set", tout << "infeasible set is a subset of current set, found literal\n";); + R_propagate(l, xk_set); + return true; + } + interval_set_ref tmp(m_ism); + tmp = m_ism.mk_union(curr_set, xk_set); + if (m_ism.is_full(tmp)) { + TRACE("nlsat_inf_set", tout << "infeasible set + current set = R, skip literal\n"; + display(tout, cls) << "\n"; + m_ism.display(tout, tmp); tout << "\n"; + ); + R_propagate(~l, tmp, false); + continue; + } + num_undef++; + if (first_undef == UINT_MAX) { + first_undef = idx; + first_undef_set = curr_set; + } + } + TRACE("nlsat_inf_set", tout << "num_undef: " << num_undef << "\n";); + if (num_undef == 0) + return false; + SASSERT(first_undef != UINT_MAX); + if (num_undef == 1) { + // unit clause + assign(cls[first_undef], mk_clause_jst(&cls)); + updt_infeasible(first_undef_set); + } + else if ( satisfy_learned || + !cls.is_learned() /* must always satisfy input clauses */ || + m_lazy == 0 /* if not in lazy mode, we also satiffy lemmas */) { + decide(cls[first_undef]); + updt_infeasible(first_undef_set); + } + else { + TRACE("nlsat_lazy", tout << "skipping clause, satisfy_learned: " << satisfy_learned << ", cls.is_learned(): " << cls.is_learned() + << ", lazy: " << m_lazy << "\n";); + } + return true; + } + + /** + \brief Try to satisfy the given clause. Return true if succeeded. + + If satisfy_learned is true, then (arithmetic) learned clauses are satisfied even if m_lazy > 0 + */ + bool process_clause(clause const & cls, bool satisfy_learned) { + if (is_satisfied(cls)) + return true; + if (m_xk == null_var) + return process_boolean_clause(cls); + else + return process_arith_clause(cls, satisfy_learned); + } + + /** + \brief Try to satisfy the given "set" of clauses. + Return 0, if the set was satisfied, or the violating clause otherwise + */ + clause * process_clauses(clause_vector const & cs) { + for (clause* c : cs) { + if (!process_clause(*c, false)) + return c; + } + return nullptr; // succeeded + } + + /** + \brief Make sure m_bk is the first unassigned pure Boolean variable. + Set m_bk == null_bool_var if there is no unassigned pure Boolean variable. + */ + void peek_next_bool_var() { + while (m_bk < m_atoms.size()) { + if (!m_dead[m_bk] && m_atoms[m_bk] == nullptr && m_bvalues[m_bk] == l_undef) { + return; + } + m_bk++; + } + m_bk = null_bool_var; + } + + /** + \brief Create a new stage. See Dejan and Leo's paper. + */ + void new_stage() { + m_stats.m_stages++; + save_new_stage_trail(); + if (m_xk == null_var) + m_xk = 0; + else + m_xk++; + } + + /** + \brief Assign m_xk + */ + void select_witness() { + scoped_anum w(m_am); + SASSERT(!m_ism.is_full(m_infeasible[m_xk])); + m_ism.pick_in_complement(m_infeasible[m_xk], is_int(m_xk), w, m_randomize); + TRACE("nlsat", + tout << "infeasible intervals: "; m_ism.display(tout, m_infeasible[m_xk]); tout << "\n"; + 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_stats.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 + */ + lbool search() { + TRACE("nlsat", tout << "starting search...\n"; display(tout); tout << "\nvar order:\n"; display_vars(tout);); + 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; + + 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(); + if (m_bk == null_bool_var) + new_stage(); // move to arith vars + } + else { + new_stage(); // peek next arith var + } + TRACE("nlsat_bug", tout << "xk: x" << m_xk << " bk: b" << m_bk << "\n";); + if (is_satisfied()) { + return l_true; + } + while (true) { + 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";); + checkpoint(); + clause * conflict_clause; + if (m_xk == null_var) + conflict_clause = process_clauses(m_bwatches[m_bk]); + else + conflict_clause = process_clauses(m_watches[m_xk]); + if (conflict_clause == nullptr) + break; + if (!resolve(*conflict_clause)) + return l_false; + if (m_stats.m_conflicts >= m_max_conflicts) + return l_undef; + log(); + } + + if (m_xk == null_var) { + if (m_bvalues[m_bk] == l_undef) { + decide(literal(m_bk, true)); + m_bk++; + } + } + else { + select_witness(); + } + } + } + + void gc() { + if (m_learned.size() <= 4*m_clauses.size()) + return; + reset_watches(); + reinit_cache(); + unsigned j = 0; + for (unsigned i = 0; i < m_learned.size(); ++i) { + auto cls = m_learned[i]; + if (i - j < m_clauses.size() && cls->size() > 1 && !cls->is_active()) + del_clause(cls); + else { + m_learned[j++] = cls; + cls->set_active(false); + } + } + m_learned.shrink(j); + reattach_arith_clauses(m_clauses); + 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_stats.m_conflicts != 1 && m_stats.m_conflicts < m_next_conflict) + return; + m_next_conflict += 100; + 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_stats.m_conflicts = 0; + m_stats.m_restarts = 0; + m_next_conflict = 0; + while (true) { + r = search(); + if (r != l_true) + break; + ++m_stats.m_restarts; + vector> bounds; + + for (var x = 0; x < num_vars(); x++) { + if (is_int(x) && m_assignment.is_assigned(x) && !m_am.is_int(m_assignment.value(x))) { + scoped_anum v(m_am), vlo(m_am); + v = m_assignment.value(x); + rational lo; + m_am.int_lt(v, vlo); + if (!m_am.is_int(vlo)) + continue; + m_am.to_rational(vlo, lo); + // derive tight bounds. + while (true) { + lo++; + if (!m_am.gt(v, lo.to_mpq())) { + lo--; + break; + } + } + bounds.push_back(std::make_pair(x, lo)); + } + } + 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_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; + rational hi = lo + 1; // rational::one(); + bool is_even = false; + polynomial_ref p(m_pm); + rational one(1); + m_lemma.reset(); + p = m_pm.mk_linear(1, &one, &x, -lo); + poly* p1 = p.get(); + m_lemma.push_back(~mk_ineq_literal(atom::GT, 1, &p1, &is_even)); + p = m_pm.mk_linear(1, &one, &x, -hi); + poly* p2 = p.get(); + m_lemma.push_back(~mk_ineq_literal(atom::LT, 1, &p2, &is_even)); + + // 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";); + } + } + } + return r; + } + + bool m_reordered = false; +//#linxi begin Simple Check +// test + void test_anum() { + scoped_anum x(m_am), y(m_am); + m_am.set(x, 3); + m_am.set(y, 5); + TRACE("linxi_simple_checker", + tout << x << " " << y << std::endl; + ); + } + bool simple_check() { + // test_anum(); + literal_vector learned_unit; + // Simple_Checker checker(m_solver, m_pm, m_am, m_clauses, m_learned, m_atoms, m_is_int.size()); + Simple_Checker checker(m_pm, m_am, m_clauses, learned_unit, m_atoms, m_is_int.size()); + // TRACE("linxi_simple_checker", + // tout << "here" << std::endl; + // ); + if (!checker()) + return false; + for (unsigned i = 0, sz = learned_unit.size(); i < sz; ++i) { + clause *cla = mk_clause(1, &learned_unit[i], true, nullptr); + if (m_atoms[learned_unit[i].var()] == nullptr) { + assign(learned_unit[i], mk_clause_jst(cla)); + } + // decide(learned_unit[i]); + } + return true; + } + +//#linxi end Simple Check + +//#linxi begin Variable Ordering Strategy + void run_variable_ordering_strategy() { + TRACE("linxi_reorder", tout << "runing vos: " << m_linxi_variable_ordering_strategy << '\n';); + + unsigned num = num_vars(); + VOS_Var_Info_Collector vos_collector(m_pm, m_atoms, num, m_linxi_variable_ordering_strategy); + vos_collector.collect(m_clauses); + vos_collector.collect(m_learned); + // TRACE("linxi_reorder", vos_collector.display(tout, m_display_var);); + + var_vector perm; + vos_collector(perm); + reorder(perm.size(), perm.data()); + } + +//#linxi end Variable Ordering Strategy + +//#linxi begin symmetry check + void symmetry_check() { + std::cout << "sym called\n"; + unsigned arith_num = m_is_int.size(); + if (arith_num > 10000) + return ; + Symmetry_Checker checker(m_pm, m_qm, m_clauses, m_atoms, m_is_int, arith_num); + for (var x = 0; x < arith_num; ++x) { + for (var y = x + 1; y < arith_num; ++y) { + if (checker.check_symmetry(x, y)) { + TRACE("linxi_symmetry_checker", + tout << "symmetry: " << x << ", " << y << "\n"; + ); + + rational zero(0); + vector as; + vector xs; + as.push_back(rational(1)); + xs.push_back(x); + as.push_back(rational(-1)); + xs.push_back(y); + polynomial_ref pr(m_pm); + pr = m_pm.mk_linear(2, as.data(), xs.data(), zero); + poly* p = pr.get(); + bool is_even = false; + literal lit = ~mk_ineq_literal(atom::GT, 1, &p, &is_even); + clause *cla = mk_clause(1, &lit, true, nullptr); + } + } + } + TRACE("linxi_symmetry_checker", + display(tout); + ); + + } +//#linxi end symmetry check + 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() { + +//#linxi begin symmetry check + if (m_linxi_symmetry_check) { + symmetry_check(); + } + // exit(0); +//#linxi end symmetry check + +//#linxi begin simple check + if (m_linxi_simple_check) { + if (!simple_check()) { + TRACE("linxi_simple_check", tout << "real unsat\n";); + return l_false; + } + TRACE("linxi_simple_checker_learned", + tout << "simple check done\n"; + ); + // exit(0); + // return l_undef; + } + // exit(0); + // return l_false; +//#linxi end simple 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; + + + if (!can_reorder()) { + + } +//#linxi begin Variable Ordering Strategy + else if (m_linxi_variable_ordering_strategy > 0) { + std::cout << "m_linxi_variable_ordering_strategy=" << m_linxi_variable_ordering_strategy << "\n"; + run_variable_ordering_strategy(); + reordered = true; + } +//#linxi end Variable Ordering Strategy + else if (m_random_order) { + shuffle_vars(); + reordered = true; + } + else if (m_reorder) { + heuristic_reorder(); + reordered = true; + } + 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(); + } + 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)); + return r; + } + + void init_search() { + undo_until_empty(); + while (m_scope_lvl > 0) { + undo_new_level(); + } + m_xk = null_var; + for (unsigned i = 0; i < m_bvalues.size(); ++i) { + m_bvalues[i] = l_undef; + } + m_assignment.reset(); + } + + lbool check(literal_vector& assumptions) { + literal_vector result; + unsigned sz = assumptions.size(); + literal const* ptr = assumptions.data(); + for (unsigned i = 0; i < sz; ++i) { + mk_external_clause(1, ptr+i, (assumption)(ptr+i)); + } + display_literal_assumption dla(*this, assumptions); + scoped_display_assumptions _scoped_display(*this, dla); + lbool r = check(); + + if (r == l_false) { + // collect used literals from m_lemma_assumptions + vector deps; + get_core(deps); + for (unsigned i = 0; i < deps.size(); ++i) { + literal const* lp = (literal const*)(deps[i]); + if (ptr <= lp && lp < ptr + sz) { + result.push_back(*lp); + } + } + } + collect(assumptions, m_clauses); + collect(assumptions, m_learned); + del_clauses(m_valids); + if (m_check_lemmas) { + for (clause* c : m_learned) { + check_lemma(c->size(), c->data(), false, nullptr); + } + } + +#if 0 + for (clause* c : m_learned) { + IF_VERBOSE(0, display(verbose_stream() << "KEEP: ", c->size(), c->c_ptr()) << "\n"); + } +#endif + assumptions.reset(); + assumptions.append(result); + return r; + } + + void get_core(vector& deps) { + m_asm.linearize(m_lemma_assumptions.get(), deps); + } + + void collect(literal_vector const& assumptions, clause_vector& clauses) { + unsigned j = 0; + for (clause * c : clauses) { + if (collect(assumptions, *c)) { + del_clause(c); + } + else { + clauses[j++] = c; + } + } + clauses.shrink(j); + } + + bool collect(literal_vector const& assumptions, clause const& c) { + unsigned sz = assumptions.size(); + literal const* ptr = assumptions.data(); + _assumption_set asms = static_cast<_assumption_set>(c.assumptions()); + if (asms == nullptr) { + return false; + } + vector deps; + m_asm.linearize(asms, deps); + for (auto dep : deps) { + if (ptr <= dep && dep < ptr + sz) { + return true; + } + } + return false; + } + + // ----------------------- + // + // Conflict Resolution + // + // ----------------------- + svector m_marks; // bool_var -> bool temp mark used during conflict resolution + unsigned m_num_marks; + scoped_literal_vector m_lemma; + scoped_literal_vector m_lazy_clause; + assumption_set_ref m_lemma_assumptions; // assumption tracking + + // Conflict resolution invariant: a marked literal is in m_lemma or on the trail stack. + + bool check_marks() { + for (unsigned m : m_marks) { + (void)m; + SASSERT(m == 0); + } + return true; + } + + unsigned scope_lvl() const { return m_scope_lvl; } + + bool is_marked(bool_var b) const { return m_marks.get(b, 0) == 1; } + + void mark(bool_var b) { m_marks.setx(b, 1, 0); } + + void reset_mark(bool_var b) { m_marks[b] = 0; } + + void reset_marks() { + for (auto const& l : m_lemma) { + reset_mark(l.var()); + } + } + + void process_antecedent(literal antecedent) { + checkpoint(); + bool_var b = antecedent.var(); + TRACE("nlsat_resolve", display(tout << "resolving antecedent: ", antecedent) << "\n";); + if (assigned_value(antecedent) == l_undef) { + checkpoint(); + // antecedent must be false in the current arith interpretation + SASSERT(value(antecedent) == l_false || m_rlimit.is_canceled()); + if (!is_marked(b)) { + 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); + m_lemma.push_back(antecedent); + } + return; + } + + unsigned b_lvl = m_levels[b]; + TRACE("nlsat_resolve", tout << "b_lvl: " << b_lvl << ", is_marked(b): " << is_marked(b) << ", m_num_marks: " << m_num_marks << "\n";); + if (!is_marked(b)) { + mark(b); + if (b_lvl == scope_lvl() /* same level */ && max_var(b) == m_xk /* same stage */) { + TRACE("nlsat_resolve", tout << "literal is in the same level and stage, increasing marks\n";); + m_num_marks++; + } + else { + TRACE("nlsat_resolve", tout << "previous level or stage, adding literal to lemma\n"; + tout << "max_var(b): " << max_var(b) << ", m_xk: " << m_xk << ", lvl: " << b_lvl << ", scope_lvl: " << scope_lvl() << "\n";); + m_lemma.push_back(antecedent); + } + } + } + + void resolve_clause(bool_var b, unsigned sz, literal const * c) { + TRACE("nlsat_proof", tout << "resolving "; if (b != null_bool_var) display_atom(tout, b) << "\n"; display(tout, sz, c); tout << "\n";); + TRACE("nlsat_proof_sk", tout << "resolving "; if (b != null_bool_var) tout << "b" << b; tout << "\n"; display_abst(tout, sz, c); tout << "\n";); + + for (unsigned i = 0; i < sz; i++) { + if (c[i].var() != b) + process_antecedent(c[i]); + } + } + + void resolve_clause(bool_var b, clause & c) { + TRACE("nlsat_resolve", tout << "resolving clause "; if (b != null_bool_var) tout << "for b: " << b << "\n"; display(tout, c) << "\n";); + c.set_active(true); + resolve_clause(b, c.size(), c.data()); + m_lemma_assumptions = m_asm.mk_join(static_cast<_assumption_set>(c.assumptions()), m_lemma_assumptions); + } + + void resolve_lazy_justification(bool_var b, lazy_justification const & jst) { + TRACE("nlsat_resolve", tout << "resolving lazy_justification for b" << b << "\n";); + unsigned sz = jst.num_lits(); + + // Dump lemma as Mathematica formula that must be true, + // if the current interpretation (really) makes the core in jst infeasible. + TRACE("nlsat_mathematica", + tout << "assignment lemma\n"; + literal_vector core; + for (unsigned i = 0; i < sz; i++) { + core.push_back(~jst.lit(i)); + } + display_mathematica_lemma(tout, core.size(), core.data(), true);); + + m_lazy_clause.reset(); + m_explain(jst.num_lits(), jst.lits(), m_lazy_clause); + for (unsigned i = 0; i < sz; i++) + m_lazy_clause.push_back(~jst.lit(i)); + + // lazy clause is a valid clause + TRACE("nlsat_mathematica", display_mathematica_lemma(tout, m_lazy_clause.size(), m_lazy_clause.data());); + TRACE("nlsat_proof_sk", tout << "theory lemma\n"; display_abst(tout, m_lazy_clause.size(), m_lazy_clause.data()); tout << "\n";); + TRACE("nlsat_resolve", + tout << "m_xk: " << m_xk << ", "; m_display_var(tout, m_xk) << "\n"; + tout << "new valid clause:\n"; + display(tout, m_lazy_clause.size(), m_lazy_clause.data()) << "\n";); + + + if (m_log_lemmas) + log_lemma(verbose_stream(), m_lazy_clause.size(), m_lazy_clause.data(), true); + + if (m_check_lemmas) { + check_lemma(m_lazy_clause.size(), m_lazy_clause.data(), true, nullptr); + m_valids.push_back(mk_clause_core(m_lazy_clause.size(), m_lazy_clause.data(), false, nullptr)); + } + +#ifdef Z3DEBUG + { + unsigned sz = m_lazy_clause.size(); + 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 { + SASSERT(value(l) == l_true || m_rlimit.is_canceled()); + SASSERT(!l.sign() || m_bvalues[b] == l_false); + SASSERT(l.sign() || m_bvalues[b] == l_true); + } + } + } +#endif + checkpoint(); + resolve_clause(b, m_lazy_clause.size(), m_lazy_clause.data()); + + for (unsigned i = 0; i < jst.num_clauses(); ++i) { + clause const& c = jst.clause(i); + TRACE("nlsat", display(tout << "adding clause assumptions ", c) << "\n";); + m_lemma_assumptions = m_asm.mk_join(static_cast<_assumption_set>(c.assumptions()), m_lemma_assumptions); + } + } + + /** + \brief Return true if all literals in ls are from previous stages. + */ + bool only_literals_from_previous_stages(unsigned num, literal const * ls) const { + for (unsigned i = 0; i < num; i++) { + if (max_var(ls[i]) == m_xk) + return false; + } + return true; + } + + /** + \brief Return the maximum scope level in ls. + + \pre This method assumes value(ls[i]) is l_false for i in [0, num) + */ + unsigned max_scope_lvl(unsigned num, literal const * ls) { + unsigned max = 0; + for (unsigned i = 0; i < num; i++) { + literal l = ls[i]; + bool_var b = l.var(); + SASSERT(value(ls[i]) == l_false); + if (assigned_value(l) == l_false) { + unsigned lvl = m_levels[b]; + if (lvl > max) + max = lvl; + } + else { + // l must be a literal from a previous stage that is false in the current interpretation + SASSERT(assigned_value(l) == l_undef); + SASSERT(max_var(b) != null_var); + SASSERT(m_xk != null_var); + SASSERT(max_var(b) < m_xk); + } + } + return max; + } + + /** + \brief Remove literals of the given lvl (that are in the current stage) from lemma. + + \pre This method assumes value(ls[i]) is l_false for i in [0, num) + */ + void remove_literals_from_lvl(scoped_literal_vector & lemma, unsigned lvl) { + TRACE("nlsat_resolve", tout << "removing literals from lvl: " << lvl << " and stage " << m_xk << "\n";); + unsigned sz = lemma.size(); + unsigned j = 0; + for (unsigned i = 0; i < sz; i++) { + literal l = lemma[i]; + bool_var b = l.var(); + SASSERT(is_marked(b)); + SASSERT(value(lemma[i]) == l_false); + if (assigned_value(l) == l_false && m_levels[b] == lvl && max_var(b) == m_xk) { + m_num_marks++; + continue; + } + lemma.set(j, l); + j++; + } + lemma.shrink(j); + } + + /** + \brief Return true if it is a Boolean lemma. + */ + bool is_bool_lemma(unsigned sz, literal const * ls) const { + for (unsigned i = 0; i < sz; i++) { + if (m_atoms[ls[i].var()] != nullptr) + return false; + } + return true; + } + + + /** + Return the maximal decision level in lemma for literals in the first sz-1 positions that + are at the same stage. If all these literals are from previous stages, + we just backtrack the current level. + */ + unsigned find_new_level_arith_lemma(unsigned sz, literal const * lemma) { + SASSERT(!is_bool_lemma(sz, lemma)); + unsigned new_lvl = 0; + bool found_lvl = false; + for (unsigned i = 0; i < sz - 1; i++) { + literal l = lemma[i]; + if (max_var(l) == m_xk) { + bool_var b = l.var(); + if (!found_lvl) { + found_lvl = true; + new_lvl = m_levels[b]; + } + else { + if (m_levels[b] > new_lvl) + new_lvl = m_levels[b]; + } + } + } + SASSERT(!found_lvl || new_lvl < scope_lvl()); + if (!found_lvl) { + TRACE("nlsat_resolve", tout << "fail to find new lvl, using previous one\n";); + new_lvl = scope_lvl() - 1; + } + return new_lvl; + } + + struct scoped_reset_marks { + imp& i; + scoped_reset_marks(imp& i):i(i) {} + ~scoped_reset_marks() { if (i.m_num_marks > 0) { i.m_num_marks = 0; for (char& m : i.m_marks) m = 0; } } + }; + + + /** + \brief Return true if the conflict was solved. + */ + bool resolve(clause & conflict) { + clause * conflict_clause = &conflict; + m_lemma_assumptions = nullptr; + start: + SASSERT(check_marks()); + TRACE("nlsat_proof", tout << "STARTING RESOLUTION\n";); + TRACE("nlsat_proof_sk", tout << "STARTING RESOLUTION\n";); + 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"; + tout << "current assignment\n"; display_assignment(tout);); + + m_num_marks = 0; + m_lemma.reset(); + m_lemma_assumptions = nullptr; + scoped_reset_marks _sr(*this); + resolve_clause(null_bool_var, *conflict_clause); + + unsigned top = m_trail.size(); + bool found_decision; + while (true) { + found_decision = false; + while (m_num_marks > 0) { + checkpoint(); + SASSERT(top > 0); + trail & t = m_trail[top-1]; + SASSERT(t.m_kind != trail::NEW_STAGE); // we only mark literals that are in the same stage + if (t.m_kind == trail::BVAR_ASSIGNMENT) { + bool_var b = t.m_b; + if (is_marked(b)) { + TRACE("nlsat_resolve", tout << "found marked: b" << b << "\n"; display_atom(tout, b) << "\n";); + m_num_marks--; + reset_mark(b); + justification jst = m_justifications[b]; + switch (jst.get_kind()) { + case justification::CLAUSE: + resolve_clause(b, *(jst.get_clause())); + break; + case justification::LAZY: + resolve_lazy_justification(b, *(jst.get_lazy())); + break; + case justification::DECISION: + SASSERT(m_num_marks == 0); + found_decision = true; + TRACE("nlsat_resolve", tout << "found decision\n";); + m_lemma.push_back(literal(b, m_bvalues[b] == l_true)); + break; + default: + UNREACHABLE(); + break; + } + } + } + top--; + } + + // m_lemma is an implicating clause after backtracking current scope level. + if (found_decision) + break; + + // If lemma only contains literals from previous stages, then we can stop. + // We make progress by returning to a previous stage with additional information (new lemma) + // that forces us to select a new partial interpretation + if (only_literals_from_previous_stages(m_lemma.size(), m_lemma.data())) + break; + + // Conflict does not depend on the current decision, and it is still in the current stage. + // We should find + // - the maximal scope level in the lemma + // - remove literal assigned in the scope level from m_lemma + // - backtrack to this level + // - and continue conflict resolution from there + // - we must bump m_num_marks for literals removed from m_lemma + unsigned max_lvl = max_scope_lvl(m_lemma.size(), m_lemma.data()); + TRACE("nlsat_resolve", tout << "conflict does not depend on current decision, backtracking to level: " << max_lvl << "\n";); + SASSERT(max_lvl < scope_lvl()); + remove_literals_from_lvl(m_lemma, max_lvl); + undo_until_level(max_lvl); + top = m_trail.size(); + TRACE("nlsat_resolve", tout << "scope_lvl: " << scope_lvl() << " num marks: " << m_num_marks << "\n";); + SASSERT(scope_lvl() == max_lvl); + } + + TRACE("nlsat_proof", tout << "New lemma\n"; display(tout, m_lemma); tout << "\n=========================\n";); + TRACE("nlsat_proof_sk", tout << "New lemma\n"; display_abst(tout, m_lemma); tout << "\n=========================\n";); + + if (m_lemma.empty()) { + TRACE("nlsat", tout << "empty clause generated\n";); + return false; // problem is unsat, empty clause was generated + } + + reset_marks(); // remove marks from the literals in m_lemmas. + TRACE("nlsat", tout << "new lemma:\n"; display(tout, m_lemma.size(), m_lemma.data()); tout << "\n"; + tout << "found_decision: " << found_decision << "\n";); + + if (m_check_lemmas) { + check_lemma(m_lemma.size(), m_lemma.data(), false, m_lemma_assumptions.get()); + } + + if (m_log_lemmas) + log_lemma(verbose_stream(), m_lemma.size(), m_lemma.data(), false); + + // There are two possibilities: + // 1) m_lemma contains only literals from previous stages, and they + // are false in the current interpretation. We make progress + // by returning to a previous stage with additional information (new clause) + // that forces us to select a new partial interpretation + // >>> Return to some previous stage (we may also backjump many decisions and stages). + // + // 2) m_lemma contains at most one literal from the current level (the last literal). + // Moreover, this literal was a decision, but the new lemma forces it to + // be assigned to a different value. + // >>> In this case, we remain in the same stage but, we add a new asserted literal + // in a previous scope level. We may backjump many decisions. + // + unsigned sz = m_lemma.size(); + clause * new_cls = nullptr; + if (!found_decision) { + // Case 1) + // We just have to find the maximal variable in m_lemma, and return to that stage + // Remark: the lemma may contain only boolean literals, in this case new_max_var == null_var; + var new_max_var = max_var(sz, m_lemma.data()); + TRACE("nlsat_resolve", tout << "backtracking to stage: " << new_max_var << ", curr: " << m_xk << "\n";); + undo_until_stage(new_max_var); + SASSERT(m_xk == new_max_var); + new_cls = mk_clause(sz, m_lemma.data(), true, m_lemma_assumptions.get()); + TRACE("nlsat", tout << "new_level: " << scope_lvl() << "\nnew_stage: " << new_max_var << "\n"; + if (new_max_var != null_var) m_display_var(tout, new_max_var) << "\n";); + } + else { + SASSERT(scope_lvl() >= 1); + // Case 2) + if (is_bool_lemma(m_lemma.size(), m_lemma.data())) { + // boolean lemma, we just backtrack until the last literal is unassigned. + bool_var max_bool_var = m_lemma[m_lemma.size()-1].var(); + undo_until_unassigned(max_bool_var); + } + else { + // We must find the maximal decision level in literals in the first sz-1 positions that + // are at the same stage. If all these literals are from previous stages, + // we just backtrack the current level. + unsigned new_lvl = find_new_level_arith_lemma(m_lemma.size(), m_lemma.data()); + TRACE("nlsat", tout << "backtracking to new level: " << new_lvl << ", curr: " << m_scope_lvl << "\n";); + undo_until_level(new_lvl); + } + + if (lemma_is_clause(*conflict_clause)) { + TRACE("nlsat", tout << "found decision literal in conflict clause\n";); + VERIFY(process_clause(*conflict_clause, true)); + return true; + } + 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)) { + TRACE("nlsat", tout << "new clause triggered another conflict, restarting conflict resolution...\n"; + display(tout, *new_cls) << "\n"; + ); + // we are still in conflict + conflict_clause = new_cls; + goto start; + } + TRACE("nlsat_resolve_done", display_assignment(tout);); + return true; + } + + bool lemma_is_clause(clause const& cls) const { + bool same = (m_lemma.size() == cls.size()); + for (unsigned i = 0; same && i < m_lemma.size(); ++i) { + same = m_lemma[i] == cls[i]; + } + return same; + } + + + // ----------------------- + // + // Debugging + // + // ----------------------- + + bool check_watches() const { +#ifdef Z3DEBUG + for (var x = 0; x < num_vars(); x++) { + clause_vector const & cs = m_watches[x]; + unsigned sz = cs.size(); + for (unsigned i = 0; i < sz; i++) { + SASSERT(max_var(*(cs[i])) == x); + } + } +#endif + return true; + } + + bool check_bwatches() const { +#ifdef Z3DEBUG + for (bool_var b = 0; b < m_bwatches.size(); b++) { + clause_vector const & cs = m_bwatches[b]; + unsigned sz = cs.size(); + for (unsigned i = 0; i < sz; i++) { + clause const & c = *(cs[i]); + SASSERT(max_var(c) == null_var); + SASSERT(max_bvar(c) == b); + } + } +#endif + return true; + } + + bool check_invariant() const { + SASSERT(check_watches()); + SASSERT(check_bwatches()); + return true; + } + + bool check_satisfied(clause_vector const & cs) const { + unsigned sz = cs.size(); + for (unsigned i = 0; i < sz; i++) { + clause const & c = *(cs[i]); + if (!is_satisfied(c)) { + TRACE("nlsat", tout << "not satisfied\n"; display(tout, c); tout << "\n";); + return false; + } + } + return true; + } + + bool check_satisfied() const { + TRACE("nlsat", tout << "bk: b" << m_bk << ", xk: x" << m_xk << "\n"; if (m_xk != null_var) { m_display_var(tout, m_xk); tout << "\n"; }); + unsigned num = m_atoms.size(); + if (m_bk != null_bool_var) + num = m_bk; + for (bool_var b = 0; b < num; b++) { + if (!check_satisfied(m_bwatches[b])) { + UNREACHABLE(); + return false; + } + } + if (m_xk != null_var) { + for (var x = 0; x < m_xk; x++) { + if (!check_satisfied(m_watches[x])) { + UNREACHABLE(); + return false; + } + } + } + return true; + } + + // ----------------------- + // + // Statistics + // + // ----------------------- + + void collect_statistics(statistics & st) { + 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_stats.reset(); + } + + // ----------------------- + // + // Variable reordering + // + // ----------------------- + + 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; + + var_info_collector(pmanager & _pm, atom_vector const & atoms, unsigned num_vars): + pm(_pm), + m_atoms(atoms) { + m_max_degree.resize(num_vars, 0); + m_num_occs.resize(num_vars, 0); + } + + var_vector m_vars; + void collect(poly * p) { + m_vars.reset(); + pm.vars(p, m_vars); + unsigned sz = m_vars.size(); + for (unsigned i = 0; i < sz; i++) { + var x = m_vars[i]; + unsigned k = pm.degree(p, x); + m_num_occs[x]++; + if (k > m_max_degree[x]) + m_max_degree[x] = k; + } + } + + void collect(literal l) { + bool_var b = l.var(); + atom * a = m_atoms[b]; + if (a == nullptr) + return; + if (a->is_ineq_atom()) { + unsigned sz = to_ineq_atom(a)->size(); + for (unsigned i = 0; i < sz; i++) { + collect(to_ineq_atom(a)->p(i)); + } + } + else { + collect(to_root_atom(a)->p()); + } + } + + void collect(clause const & c) { + unsigned sz = c.size(); + for (unsigned i = 0; i < sz; i++) + collect(c[i]); + } + + void collect(clause_vector const & cs) { + unsigned sz = cs.size(); + for (unsigned i = 0; i < sz; i++) + collect(*(cs[i])); + } + + std::ostream& display(std::ostream & out, display_var_proc const & proc) { + unsigned sz = m_num_occs.size(); + for (unsigned i = 0; i < sz; i++) { + proc(out, i); out << " -> " << m_max_degree[i] << " : " << m_num_occs[i] << "\n"; + } + return out; + } + }; + + struct reorder_lt { + var_info_collector const & m_info; + reorder_lt(var_info_collector const & info):m_info(info) {} + bool operator()(var x, var y) const { + // high degree first + if (m_info.m_max_degree[x] < m_info.m_max_degree[y]) + return false; + if (m_info.m_max_degree[x] > m_info.m_max_degree[y]) + return true; + // more constrained first + if (m_info.m_num_occs[x] < m_info.m_num_occs[y]) + return false; + if (m_info.m_num_occs[x] > m_info.m_num_occs[y]) + return true; + return m_info.m_shuffle[x] < m_info.m_shuffle[y]; + } + }; + + // Order variables by degree and number of occurrences + void heuristic_reorder() { + unsigned num = num_vars(); + 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++) + 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";); + var_vector perm; + perm.resize(num, 0); + for (var x = 0; x < num; x++) { + perm[new_order[x]] = x; + } + reorder(perm.size(), perm.data()); + SASSERT(check_invariant()); + } + + void init_shuffle(var_vector& p) { + unsigned num = num_vars(); + 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 all_of(m_learned, [&](clause* c) { return !has_root_atom(*c); }) + && all_of(m_clauses, [&](clause* c) { return !has_root_atom(*c); }); + } + + /** + \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); + display_vars(tout); + 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(); + assignment new_assignment(m_am); + for (var x = 0; x < num_vars(); x++) { + if (m_assignment.is_assigned(x)) + new_assignment.set(p[x], m_assignment.value(x)); + } + var_vector new_inv_perm; + new_inv_perm.resize(sz); + // the undo_until_size(0) statement erases the Boolean assignment. + // undo_until_size(0) + undo_until_stage(null_var); + m_cache.reset(); +#ifdef Z3DEBUG + for (var x = 0; x < num_vars(); x++) { + SASSERT(m_watches[x].empty()); + } +#endif + // update m_perm mapping + for (unsigned ext_x = 0; ext_x < sz; ext_x++) { + // p: internal -> new pos + // m_perm: internal -> external + // m_inv_perm: external -> internal + new_inv_perm[ext_x] = p[m_inv_perm[ext_x]]; + m_perm.set(new_inv_perm[ext_x], ext_x); + } + bool_vector is_int; + is_int.swap(m_is_int); + for (var x = 0; x < sz; x++) { + m_is_int.setx(p[x], is_int[x], false); + SASSERT(m_infeasible[x] == 0); + } + m_inv_perm.swap(new_inv_perm); +#ifdef Z3DEBUG + for (var x = 0; x < num_vars(); x++) { + SASSERT(x == m_inv_perm[m_perm[x]]); + SASSERT(m_watches[x].empty()); + } +#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); + reattach_arith_clauses(m_clauses); + reattach_arith_clauses(m_learned); + TRACE("nlsat_reorder", tout << "solver after variable reorder\n"; display(tout); display_vars(tout);); + } + + + /** + \brief Restore variable order. + */ + void restore_order() { + // m_perm: internal -> external + // m_inv_perm: external -> internal + var_vector p; + p.append(m_perm); + reorder(p.size(), p.data()); +#ifdef Z3DEBUG + for (var x = 0; x < num_vars(); x++) { + SASSERT(m_perm[x] == x); + SASSERT(m_inv_perm[x] == x); + } +#endif + } + + /** + \brief After variable reordering some lemmas containing root atoms may be ill-formed. + */ + void remove_learned_roots() { + unsigned j = 0; + for (clause* c : m_learned) { + if (has_root_atom(*c)) { + del_clause(c); + } + else { + m_learned[j++] = c; + } + } + m_learned.shrink(j); + } + + /** + \brief Return true if the clause contains an ill formed root atom + */ + bool has_root_atom(clause const & c) const { + for (literal lit : c) { + bool_var b = lit.var(); + atom * a = m_atoms[b]; + if (a && a->is_root_atom()) + return true; + } + return false; + } + + /** + \brief reinsert all polynomials in the unique cache + */ + void reinit_cache() { + reinit_cache(m_clauses); + reinit_cache(m_learned); + for (atom* a : m_atoms) + reinit_cache(a); + } + void reinit_cache(clause_vector const & cs) { + for (clause* c : cs) + reinit_cache(*c); + } + void reinit_cache(clause const & c) { + for (literal l : c) + reinit_cache(l); + } + void reinit_cache(literal l) { + bool_var b = l.var(); + reinit_cache(m_atoms[b]); + } + void reinit_cache(atom* a) { + if (a == nullptr) { + + } + else if (a->is_ineq_atom()) { + var max = 0; + unsigned sz = to_ineq_atom(a)->size(); + for (unsigned i = 0; i < sz; i++) { + poly * p = to_ineq_atom(a)->p(i); + VERIFY(m_cache.mk_unique(p) == p); + var x = m_pm.max_var(p); + if (x > max) + max = x; + } + a->m_max_var = max; + } + else { + poly * p = to_root_atom(a)->p(); + VERIFY(m_cache.mk_unique(p) == p); + a->m_max_var = m_pm.max_var(p); + } + } + + void reset_watches() { + unsigned num = num_vars(); + for (var x = 0; x < num; x++) { + m_watches[x].reset(); + } + } + + void reattach_arith_clauses(clause_vector const & cs) { + for (clause* cp : cs) { + var x = max_var(*cp); + if (x != null_var) + m_watches[x].push_back(cp); + } + } + + // ----------------------- + // + // Solver initialization + // + // ----------------------- + + struct degree_lt { + unsigned_vector & m_degrees; + degree_lt(unsigned_vector & ds):m_degrees(ds) {} + bool operator()(unsigned i1, unsigned i2) const { + if (m_degrees[i1] < m_degrees[i2]) + return true; + if (m_degrees[i1] > m_degrees[i2]) + return false; + return i1 < i2; + } + }; + + unsigned_vector m_cs_degrees; + unsigned_vector m_cs_p; + void sort_clauses_by_degree(unsigned sz, clause ** cs) { + if (sz <= 1) + return; + TRACE("nlsat_reorder_clauses", tout << "before:\n"; for (unsigned i = 0; i < sz; i++) { display(tout, *(cs[i])); tout << "\n"; }); + m_cs_degrees.reset(); + m_cs_p.reset(); + for (unsigned i = 0; i < sz; i++) { + m_cs_p.push_back(i); + m_cs_degrees.push_back(degree(*(cs[i]))); + } + std::sort(m_cs_p.begin(), m_cs_p.end(), degree_lt(m_cs_degrees)); + TRACE("nlsat_reorder_clauses", tout << "permutation: "; ::display(tout, m_cs_p.begin(), m_cs_p.end()); tout << "\n";); + apply_permutation(sz, cs, m_cs_p.data()); + TRACE("nlsat_reorder_clauses", tout << "after:\n"; for (unsigned i = 0; i < sz; i++) { display(tout, *(cs[i])); tout << "\n"; }); + } + +//#linxi begin + + struct degree_lit_num_lt { + unsigned_vector & m_degrees; + unsigned_vector & m_lit_num; + degree_lit_num_lt(unsigned_vector & ds, unsigned_vector ln) : + m_degrees(ds), + m_lit_num(ln) { + } + bool operator()(unsigned i1, unsigned i2) const { + if (m_lit_num[i1] == 1 && m_lit_num[i2] > 1) + return true; + if (m_lit_num[i1] > 1 && m_lit_num[i2] == 1) + return false; + if (m_degrees[i1] != m_degrees[i2]) + return m_degrees[i1] < m_degrees[i2]; + if (m_lit_num[i1] != m_lit_num[i2]) + return m_lit_num[i1] < m_lit_num[i2]; + return i1 < i2; + } + }; + + unsigned_vector m_dl_degrees; + unsigned_vector m_dl_lit_num; + unsigned_vector m_dl_p; + void sort_clauses_by_degree_lit_num(unsigned sz, clause ** cs) { + if (sz <= 1) + return; + TRACE("nlsat_reorder_clauses", tout << "before:\n"; for (unsigned i = 0; i < sz; i++) { display(tout, *(cs[i])); tout << "\n"; }); + m_dl_degrees.reset(); + m_dl_lit_num.reset(); + m_dl_p.reset(); + for (unsigned i = 0; i < sz; i++) { + m_dl_degrees.push_back(degree(*(cs[i]))); + m_dl_lit_num.push_back(cs[i]->size()); + m_dl_p.push_back(i); + } + std::sort(m_dl_p.begin(), m_dl_p.end(), degree_lit_num_lt(m_dl_degrees, m_dl_lit_num)); + TRACE("nlsat_reorder_clauses", tout << "permutation: "; ::display(tout, m_dl_p.begin(), m_dl_p.end()); tout << "\n";); + apply_permutation(sz, cs, m_dl_p.data()); + TRACE("nlsat_reorder_clauses", tout << "after:\n"; for (unsigned i = 0; i < sz; i++) { display(tout, *(cs[i])); tout << "\n"; }); + } + +//#linxi end + void sort_watched_clauses() { + unsigned num = num_vars(); + for (unsigned i = 0; i < num; i++) { + clause_vector & ws = m_watches[i]; +//#linxi begin + // sort_clauses_by_degree(ws.size(), ws.data()); + if (m_linxi_simple_check) { + sort_clauses_by_degree_lit_num(ws.size(), ws.data()); + } + else { + sort_clauses_by_degree(ws.size(), ws.data()); + } +//#linxi end + } + } + + // ----------------------- + // + // Full dimensional + // + // A problem is in the full dimensional fragment if it does + // not contain equalities or non-strict inequalities. + // + // ----------------------- + + bool is_full_dimensional(literal l) const { + atom * a = m_atoms[l.var()]; + if (a == nullptr) + return true; + switch (a->get_kind()) { + case atom::EQ: return l.sign(); + case atom::LT: return !l.sign(); + case atom::GT: return !l.sign(); + case atom::ROOT_EQ: return l.sign(); + case atom::ROOT_LT: return !l.sign(); + case atom::ROOT_GT: return !l.sign(); + case atom::ROOT_LE: return l.sign(); + case atom::ROOT_GE: return l.sign(); + default: + UNREACHABLE(); + return false; + } + } + + bool is_full_dimensional(clause const & c) const { + for (literal l : c) { + if (!is_full_dimensional(l)) + return false; + } + return true; + } + + bool is_full_dimensional(clause_vector const & cs) const { + for (clause* c : cs) { + if (!is_full_dimensional(*c)) + return false; + } + return true; + } + + bool is_full_dimensional() const { + return is_full_dimensional(m_clauses); + } + + + // ----------------------- + // + // Simplification + // + // ----------------------- + + // solve simple equalities + // TBD WU-Reit decomposition? + + // - elim_unconstrained + // - solve_eqs + // - fm + + /** + \brief isolate variables in unit equalities. + Assume a clause is c == v*p + q + and the context implies p > 0 + + replace v by -q/p + remove clause c, + The for other occurrences of v, + replace v*r + v*v*r' > 0 by + by p*p*v*r + p*p*v*v*r' > 0 + by p*q*r + q*q*r' > 0 + + The method ignores lemmas and assumes constraints don't use roots. + */ + + + + // Eliminated variables are tracked in m_bounds. + // Each element in m_bounds tracks the eliminated variable and an upper or lower bound + // that has to be satisfied. Variables that are eliminated through equalities are tracked + // by non-strict bounds. A satisfiable solution is required to provide an evaluation that + // is consistent with the bounds. For equalities, the non-strict lower or upper bound can + // always be assigned as a value to the variable. + + void fix_patch() { + m_lo.reset(); m_hi.reset(); + for (auto& b : m_bounds) + m_assignment.reset(b.x); + for (unsigned i = m_bounds.size(); i-- > 0; ) + fix_patch(m_bounds[i]); + } + + // x is unassigned, lo < x -> x <- lo + 1 + // x is unassigned, x < hi -> x <- hi - 1 + // x is unassigned, lo <= x -> x <- lo + // x is unassigned, x <= hi -> x <- hi + // x is assigned above hi, lo is strict lo < x < hi -> set x <- (lo + hi)/2 + // x is assigned below hi, above lo -> no-op + // x is assigned below lo, hi is strict lo < x < hi -> set x <-> (lo + hi)/2 + // x is assigned above hi, x <= hi -> x <- hi + // x is assigned blow lo, lo <= x -> x <- lo + void fix_patch(bound_constraint& b) { + var x = b.x; + scoped_anum Av(m_am), Bv(m_am), val(m_am); + m_pm.eval(b.A, m_assignment, Av); + m_pm.eval(b.B, m_assignment, Bv); + m_am.neg(Bv); + val = Bv / Av; + // Ax >= B + // is-lower : A > 0 + // is-upper: A < 0 + // x <- B / A + bool is_lower = m_am.is_pos(Av); + TRACE("nlsat", + m_display_var(tout << "patch v" << x << " ", x) << "\n"; + if (m_assignment.is_assigned(x)) m_am.display(tout << "previous value: ", m_assignment.value(x)); tout << "\n"; + m_am.display(tout << "updated value: ", val); tout << "\n"; + ); + + if (!m_assignment.is_assigned(x)) { + if (!b.is_strict) + m_assignment.set_core(x, val); + else if (is_lower) + m_assignment.set_core(x, val + 1); + else + m_assignment.set_core(x, val - 1); + } + else { + auto& aval = m_assignment.value(x); + if (is_lower) { + // lo < value(x), lo < x -> x is unchanged + if (b.is_strict && m_am.lt(val, aval)) + ; + else if (!b.is_strict && m_am.le(val, aval)) + ; + else if (!b.is_strict) + m_assignment.set_core(x, val); + // aval < lo < x, hi is unassigned: x <- lo + 1 + else if (!m_hi.is_assigned(x)) + m_assignment.set_core(x, val + 1); + // aval < lo < x, hi is assigned: x <- (lo + hi) / 2 + else { + scoped_anum mid(m_am); + m_am.add(m_hi.value(x), val, mid); + mid = mid / 2; + m_assignment.set_core(x, mid); + } + } + else { + // dual to lower bounds + if (b.is_strict && m_am.lt(aval, val)) + ; + else if (!b.is_strict && m_am.le(aval, val)) + ; + else if (!b.is_strict) + m_assignment.set_core(x, val); + else if (!m_lo.is_assigned(x)) + m_assignment.set_core(x, val - 1); + else { + scoped_anum mid(m_am); + m_am.add(m_lo.value(x), val, mid); + mid = mid / 2; + m_assignment.set_core(x, mid); + } + } + } + + if (is_lower) { + if (!m_lo.is_assigned(x) || m_am.lt(m_lo.value(x), val)) + m_lo.set_core(x, val); + } + else { + if (!m_hi.is_assigned(x) || m_am.gt(m_hi.value(x), val)) + m_hi.set_core(x, val); + } + } + + bool is_unit_ineq(clause const& c) const { + return + c.size() == 1 && + m_atoms[c[0].var()] && + m_atoms[c[0].var()]->is_ineq_atom(); + } + + bool is_unit_eq(clause const& c) const { + return + is_unit_ineq(c) && + !c[0].sign() && + m_atoms[c[0].var()]->is_eq(); + } + + /** + \brief determine whether the clause is a comparison v > k or v < k', where k >= 0 or k' <= 0. + */ + lbool is_cmp0(clause const& c, var& v) { + if (!is_unit_ineq(c)) + return l_undef; + literal lit = c[0]; + ineq_atom const& a = *to_ineq_atom(m_atoms[lit.var()]); + bool sign = lit.sign(); + poly * p0; + if (!is_single_poly(a, p0)) + return l_undef; + if (m_pm.is_var(p0, v)) { + if (!sign && a.get_kind() == atom::GT) { + return l_true; + } + if (!sign && a.get_kind() == atom::LT) { + return l_false; + } + return l_undef; + } + polynomial::scoped_numeral n(m_pm.m()); + if (m_pm.is_var_num(p0, v, n)) { + // x - k > 0 + if (!sign && a.get_kind() == atom::GT && m_pm.m().is_nonneg(n)) { + return l_true; + } + // x + k < 0 + if (!sign && a.get_kind() == atom::LT && m_pm.m().is_nonpos(n)) { + return l_false; + } + // !(x + k > 0) + if (sign && a.get_kind() == atom::GT && m_pm.m().is_pos(n)) { + return l_false; + } + // !(x - k < 0) + if (sign && a.get_kind() == atom::LT && m_pm.m().is_neg(n)) { + return l_true; + } + } + return l_undef; + } + + 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); + } + + // ----------------------- + // + // Pretty printing + // + // ----------------------- + + std::ostream& display_num_assignment(std::ostream & out, display_var_proc const & proc) const { + for (var x = 0; x < num_vars(); x++) { + if (m_assignment.is_assigned(x)) { + proc(out, x); + out << " -> "; + m_am.display_decimal(out, m_assignment.value(x)); + out << "\n"; + } + } + return out; + } + + std::ostream& display_bool_assignment(std::ostream & out) const { + unsigned sz = m_atoms.size(); + for (bool_var b = 0; b < sz; b++) { + if (m_atoms[b] == nullptr && m_bvalues[b] != l_undef) { + out << "b" << b << " -> " << (m_bvalues[b] == l_true ? "true" : "false") << " @" << m_levels[b] << "\n"; + } + else if (m_atoms[b] != nullptr && m_bvalues[b] != l_undef) { + display(out << "b" << b << " ", *m_atoms[b]) << " -> " << (m_bvalues[b] == l_true ? "true" : "false") << " @" << m_levels[b] << "\n"; + } + } + TRACE("nlsat_bool_assignment", + for (bool_var b = 0; b < sz; b++) { + out << "b" << b << " -> " << m_bvalues[b] << " "; + if (m_atoms[b]) display(out, *m_atoms[b]); + out << "\n"; + }); + return out; + } + + bool display_mathematica_assignment(std::ostream & out) const { + bool first = true; + for (var x = 0; x < num_vars(); x++) { + if (m_assignment.is_assigned(x)) { + if (first) + first = false; + else + out << " && "; + out << "x" << x << " == "; + m_am.display_mathematica(out, m_assignment.value(x)); + } + } + return !first; + } + + std::ostream& display_num_assignment(std::ostream & out) const { + return display_num_assignment(out, m_display_var); + } + + std::ostream& display_assignment(std::ostream& out) const { + display_bool_assignment(out); + 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_not(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; + } + + bool m_display_eval = false; + std::ostream& display_eval(std::ostream& out, justification j) { + flet _display(m_display_eval, true); + return display(out, j); + } + + std::ostream& display_ineq(std::ostream & out, ineq_atom const & a, display_var_proc const & proc, bool use_star = false) const { + unsigned sz = a.size(); + for (unsigned i = 0; i < sz; i++) { + if (use_star && i > 0) + out << "*"; + bool is_even = a.is_even(i); + if (is_even || sz > 1) + out << "("; + display_polynomial(out, a.p(i), proc, use_star); + if (is_even || sz > 1) + out << ")"; + if (is_even) + out << "^2"; + } + switch (a.get_kind()) { + case atom::LT: out << " < 0"; break; + case atom::GT: out << " > 0"; break; + case atom::EQ: out << " = 0"; break; + default: UNREACHABLE(); break; + } + return out; + } + + std::ostream& display_mathematica(std::ostream & out, ineq_atom const & a) const { + unsigned sz = a.size(); + for (unsigned i = 0; i < sz; i++) { + if (i > 0) + out << "*"; + bool is_even = a.is_even(i); + if (sz > 1) + out << "("; + if (is_even) + out << "("; + m_pm.display(out, a.p(i), display_var_proc(), true); + if (is_even) + out << "^2)"; + if (sz > 1) + out << ")"; + } + switch (a.get_kind()) { + case atom::LT: out << " < 0"; break; + case atom::GT: out << " > 0"; break; + case atom::EQ: out << " == 0"; break; + default: UNREACHABLE(); break; + } + return out; + } + + std::ostream& display_polynomial_smt2(std::ostream & out, poly const* p, display_var_proc const & proc) const { + return m_pm.display_smt2(out, p, proc); + } + + std::ostream& display_ineq_smt2(std::ostream & out, ineq_atom const & a, display_var_proc const & proc) const { + switch (a.get_kind()) { + case atom::LT: out << "(< "; break; + case atom::GT: out << "(> "; break; + case atom::EQ: out << "(= "; break; + default: UNREACHABLE(); break; + } + unsigned sz = a.size(); + if (sz > 1) + out << "(* "; + for (unsigned i = 0; i < sz; i++) { + if (i > 0) out << " "; + if (a.is_even(i)) { + out << "(* "; + display_polynomial_smt2(out, a.p(i), proc); + out << " "; + display_polynomial_smt2(out, a.p(i), proc); + out << ")"; + } + else { + display_polynomial_smt2(out, a.p(i), proc); + } + } + if (sz > 1) + out << ")"; + out << " 0)"; + return out; + } + + std::ostream& display_poly_root(std::ostream& out, char const* y, root_atom const& a, display_var_proc const& proc) const { + out << "(exists (("; proc(out,a.x()); out << " Real))\n"; + out << "(and (= " << y << " "; + proc(out, a.x()); + out << ") (= 0 "; + display_polynomial_smt2(out, a.p(), proc); + out << ")))\n"; + return out; + } + + std::ostream& display_binary_smt2(std::ostream& out, poly const* p1, char const* rel, poly const* p2, display_var_proc const& proc) const { + out << "(" << rel << " "; + display_polynomial_smt2(out, p1, proc); + out << " "; + display_polynomial_smt2(out, p2, proc); + out << ")"; + return out; + } + + + std::ostream& display_linear_root_smt2(std::ostream & out, root_atom const & a, display_var_proc const & proc) const { + polynomial_ref A(m_pm), B(m_pm), Z(m_pm), Ax(m_pm); + polynomial::scoped_numeral zero(m_qm); + m_pm.m().set(zero, 0); + A = m_pm.derivative(a.p(), a.x()); + B = m_pm.neg(m_pm.substitute(a.p(), a.x(), zero)); + Z = m_pm.mk_zero(); + + Ax = m_pm.mul(m_pm.mk_polynomial(a.x()), A); + + // x < root[1](ax + b) == (a > 0 => ax + b < 0) & (a < 0 => ax + b > 0) + // x < root[1](ax + b) == (a > 0 => ax < -b) & (a < 0 => ax > -b) + + char const* rel1 = "<", *rel2 = ">"; + switch (a.get_kind()) { + case atom::ROOT_LT: rel1 = "<"; rel2 = ">"; break; + case atom::ROOT_GT: rel1 = ">"; rel2 = "<"; break; + case atom::ROOT_LE: rel1 = "<="; rel2 = ">="; break; + case atom::ROOT_GE: rel1 = ">="; rel2 = "<="; break; + case atom::ROOT_EQ: rel1 = rel2 = "="; break; + default: UNREACHABLE(); break; + } + + out << "(and "; + out << "(=> "; display_binary_smt2(out, A, ">", Z, proc); display_binary_smt2(out, Ax, rel1, B, proc); out << ") "; + out << "(=> "; display_binary_smt2(out, A, "<", Z, proc); display_binary_smt2(out, Ax, rel2, B, proc); out << ") "; + out << ")"; + + return out; + } + + + std::ostream& display_root_smt2(std::ostream& out, root_atom const& a, display_var_proc const& proc) const { + if (a.i() == 1 && m_pm.degree(a.p(), a.x()) == 1) + return display_linear_root_smt2(out, a, proc); +#if 1 + out << "(exists ("; + for (unsigned j = 0; j < a.i(); ++j) { + std::string y = std::string("y") + std::to_string(j); + out << "(" << y << " Real) "; + } + out << ")\n"; + out << "(and\n"; + for (unsigned j = 0; j < a.i(); ++j) { + std::string y = std::string("y") + std::to_string(j); + display_poly_root(out, y.c_str(), a, proc); + } + for (unsigned j = 0; j + 1 < a.i(); ++j) { + std::string y1 = std::string("y") + std::to_string(j); + std::string y2 = std::string("y") + std::to_string(j+1); + out << "(< " << y1 << " " << y2 << ")\n"; + } + + std::string yn = "y" + std::to_string(a.i() - 1); + + // TODO we need (forall z : z < yn . p(z) => z = y1 or ... z = y_{n-1}) + // to say y1, .., yn are the first n distinct roots. + // + out << "(forall ((z Real)) (=> (and (< z " << yn << ") "; display_poly_root(out, "z", a, proc) << ") "; + if (a.i() == 1) { + out << "false))\n"; + } + else { + out << "(or "; + for (unsigned j = 0; j + 1 < a.i(); ++j) { + std::string y1 = std::string("y") + std::to_string(j); + out << "(= z " << y1 << ") "; + } + out << ")))\n"; + } + switch (a.get_kind()) { + case atom::ROOT_LT: out << "(< "; proc(out, a.x()); out << " " << yn << ")"; break; + case atom::ROOT_GT: out << "(> "; proc(out, a.x()); out << " " << yn << ")"; break; + 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; +#endif + + + return display_root(out, a, proc); + } + + std::ostream& display_root(std::ostream & out, root_atom const & a, display_var_proc const & proc) const { + proc(out, a.x()); + switch (a.get_kind()) { + case atom::ROOT_LT: out << " < "; break; + case atom::ROOT_GT: out << " > "; break; + case atom::ROOT_LE: out << " <= "; break; + case atom::ROOT_GE: out << " >= "; break; + case atom::ROOT_EQ: out << " = "; break; + default: UNREACHABLE(); break; + } + out << "root[" << a.i() << "]("; + display_polynomial(out, a.p(), proc); + out << ")"; + return out; + } + + struct mathematica_var_proc : public display_var_proc { + var m_x; + public: + mathematica_var_proc(var x):m_x(x) {} + std::ostream& operator()(std::ostream & out, var x) const override { + if (m_x == x) + return out << "#1"; + else + return out << "x" << x; + } + }; + + std::ostream& display_mathematica(std::ostream & out, root_atom const & a) const { + out << "x" << a.x(); + switch (a.get_kind()) { + case atom::ROOT_LT: out << " < "; break; + case atom::ROOT_GT: out << " > "; break; + case atom::ROOT_LE: out << " <= "; break; + case atom::ROOT_GE: out << " >= "; break; + case atom::ROOT_EQ: out << " == "; break; + default: UNREACHABLE(); break; + } + out << "Root["; + display_polynomial(out, a.p(), mathematica_var_proc(a.x()), true); + out << " &, " << a.i() << "]"; + return out; + } + + std::ostream& display(std::ostream & out, atom const & a, display_var_proc const & proc) const { + if (a.is_ineq_atom()) + return display_ineq(out, static_cast(a), proc); + else + return display_root(out, static_cast(a), proc); + } + + std::ostream& display(std::ostream & out, atom const & a) const { + return display(out, a, m_display_var); + } + + std::ostream& display_mathematica(std::ostream & out, atom const & a) const { + if (a.is_ineq_atom()) + return display_mathematica(out, static_cast(a)); + else + return display_mathematica(out, static_cast(a)); + } + + std::ostream& display_smt2(std::ostream & out, atom const & a, display_var_proc const & proc) const { + if (a.is_ineq_atom()) + return display_ineq_smt2(out, static_cast(a), proc); + else + return display_root_smt2(out, static_cast(a), proc); + } + + std::ostream& display_atom(std::ostream & out, bool_var b, display_var_proc const & proc) const { + if (b == 0) + out << "true"; + else if (m_atoms[b] == 0) + out << "b" << b; + else + display(out, *(m_atoms[b]), proc); + return out; + } + + std::ostream& display_atom(std::ostream & out, bool_var b) const { + return display_atom(out, b, m_display_var); + } + + std::ostream& display_mathematica_atom(std::ostream & out, bool_var b) const { + if (b == 0) + out << "(0 < 1)"; + else if (m_atoms[b] == 0) + out << "b" << b; + else + display_mathematica(out, *(m_atoms[b])); + return out; + } + + std::ostream& display_smt2_atom(std::ostream & out, bool_var b, display_var_proc const & proc) const { + if (b == 0) + out << "true"; + else if (m_atoms[b] == 0) + out << "b" << b; + else + display_smt2(out, *(m_atoms[b]), proc); + return out; + } + + std::ostream& display(std::ostream & out, literal l, display_var_proc const & proc) const { + if (l.sign()) { + bool_var b = l.var(); + out << "!"; + if (m_atoms[b] != 0) + out << "("; + display_atom(out, b, proc); + if (m_atoms[b] != 0) + out << ")"; + } + else { + display_atom(out, l.var(), proc); + } + return out; + } + + std::ostream& display(std::ostream & out, literal l) const { + 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(); + out << "!"; + if (m_atoms[b] != 0) + out << "("; + display_mathematica_atom(out, b); + if (m_atoms[b] != 0) + out << ")"; + } + else { + display_mathematica_atom(out, l.var()); + } + return out; + } + + std::ostream& display_smt2(std::ostream & out, literal l, display_var_proc const & proc) const { + if (l.sign()) { + bool_var b = l.var(); + out << "(not "; + display_smt2_atom(out, b, proc); + out << ")"; + } + else { + display_smt2_atom(out, l.var(), proc); + } + return out; + } + + 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 << " "; + (*m_display_assumption)(out, dep); + } + return out; + } + + std::ostream& display(std::ostream & out, unsigned num, literal const * ls, display_var_proc const & proc) const { + for (unsigned i = 0; i < num; i++) { + if (i > 0) + out << " or "; + display(out, ls[i], proc); + } + return out; + } + + std::ostream& display(std::ostream & out, unsigned num, literal const * ls) const { + return display(out, num, ls, m_display_var); + } + + std::ostream& display_not(std::ostream & out, unsigned num, literal const * ls, display_var_proc const & proc) const { + for (unsigned i = 0; i < num; i++) { + if (i > 0) + out << " or "; + display(out, ~ls[i], proc); + } + return out; + } + + std::ostream& display_not(std::ostream & out, unsigned num, literal const * ls) const { + return display_not(out, num, ls, m_display_var); + } + + std::ostream& display(std::ostream & out, scoped_literal_vector const & cs) { + return display(out, cs.size(), cs.data(), m_display_var); + } + + std::ostream& display(std::ostream & out, clause const & c, display_var_proc const & proc) const { + if (c.assumptions() != nullptr) { + display_assumptions(out, static_cast<_assumption_set>(c.assumptions())); + out << " |- "; + } + return display(out, c.size(), c.data(), proc); + } + + std::ostream& display(std::ostream & out, clause const & c) const { + return display(out, c, m_display_var); + } + + + std::ostream& display_polynomial(std::ostream& out, poly* p, display_var_proc const & proc, bool use_star = false) const { + if (m_display_eval) { + polynomial_ref q(m_pm); + q = p; + for (var x = 0; x < num_vars(); x++) + if (m_assignment.is_assigned(x)) { + auto& a = m_assignment.value(x); + if (!m_am.is_rational(a)) + continue; + mpq r; + m_am.to_rational(a, r); + q = m_pm.substitute(q, 1, &x, &r); + } + m_pm.display(out, q, proc, use_star); + } + else + m_pm.display(out, p, proc, use_star); + return out; + } + + // -- + + std::ostream& display_smt2(std::ostream & out, unsigned n, literal const* ls) const { + return display_smt2(out, n, ls, display_var_proc()); + } + + + std::ostream& display_smt2(std::ostream & out, unsigned num, literal const * ls, display_var_proc const & proc) const { + if (num == 0) { + out << "false"; + } + else if (num == 1) { + display_smt2(out, ls[0], proc); + } + else { + out << "(or"; + for (unsigned i = 0; i < num; i++) { + out << " "; + display_smt2(out, ls[i], proc); + } + out << ")"; + } + return out; + } + + std::ostream& display_smt2(std::ostream & out, clause const & c, display_var_proc const & proc = display_var_proc()) const { + return display_smt2(out, c.size(), c.data(), proc); + } + + std::ostream& display_abst(std::ostream & out, literal l) const { + if (l.sign()) { + bool_var b = l.var(); + out << "!"; + if (b == true_bool_var) + out << "true"; + else + out << "b" << b; + } + else { + out << "b" << l.var(); + } + return out; + } + + std::ostream& display_abst(std::ostream & out, unsigned num, literal const * ls) const { + for (unsigned i = 0; i < num; i++) { + if (i > 0) + out << " or "; + display_abst(out, ls[i]); + } + return out; + } + + std::ostream& display_abst(std::ostream & out, scoped_literal_vector const & cs) const { + return display_abst(out, cs.size(), cs.data()); + } + + std::ostream& display_abst(std::ostream & out, clause const & c) const { + return display_abst(out, c.size(), c.data()); + } + + std::ostream& display_mathematica(std::ostream & out, clause const & c) const { + out << "("; + unsigned sz = c.size(); + for (unsigned i = 0; i < sz; i++) { + if (i > 0) + out << " || "; + display_mathematica(out, c[i]); + } + out << ")"; + return out; + } + + // Debugging support: + // Display generated lemma in Mathematica format. + // Mathematica must reduce lemma to True (modulo resource constraints). + std::ostream& display_mathematica_lemma(std::ostream & out, unsigned num, literal const * ls, bool include_assignment = false) const { + out << "Resolve[ForAll[{"; + // var definition + for (unsigned i = 0; i < num_vars(); i++) { + if (i > 0) + out << ", "; + out << "x" << i; + } + out << "}, "; + if (include_assignment) { + out << "!("; + if (!display_mathematica_assignment(out)) + out << "0 < 1"; // nothing was printed + out << ") || "; + } + for (unsigned i = 0; i < num; i++) { + if (i > 0) + out << " || "; + display_mathematica(out, ls[i]); + } + out << "], Reals]\n"; // end of exists + return out; + } + + std::ostream& display(std::ostream & out, clause_vector const & cs, display_var_proc const & proc) const { + for (clause* c : cs) { + display(out, *c, proc) << "\n"; + } + return out; + } + + std::ostream& display(std::ostream & out, clause_vector const & cs) const { + return display(out, cs, m_display_var); + } + + std::ostream& display_mathematica(std::ostream & out, clause_vector const & cs) const { + unsigned sz = cs.size(); + for (unsigned i = 0; i < sz; i++) { + if (i > 0) out << ",\n"; + display_mathematica(out << " ", *(cs[i])); + } + return out; + } + + std::ostream& display_abst(std::ostream & out, clause_vector const & cs) const { + for (clause* c : cs) { + display_abst(out, *c) << "\n"; + } + return out; + } + + std::ostream& display(std::ostream & out, display_var_proc const & proc) const { + display(out, m_clauses, proc); + if (!m_learned.empty()) { + display(out << "Lemmas:\n", m_learned, proc); + } + return out; + } + + std::ostream& display_mathematica(std::ostream & out) const { + return display_mathematica(out << "{\n", m_clauses) << "}\n"; + } + + std::ostream& display_abst(std::ostream & out) const { + display_abst(out, m_clauses); + if (!m_learned.empty()) { + display_abst(out << "Lemmas:\n", m_learned); + } + return out; + } + + std::ostream& display(std::ostream & out) const { + display(out, m_display_var); + display_assignment(out << "assignment:\n"); + return out << "---\n"; + } + + std::ostream& display_vars(std::ostream & out) const { + for (unsigned i = 0; i < num_vars(); i++) { + out << i << " -> "; m_display_var(out, i); out << "\n"; + } + return out; + } + + std::ostream& display_smt2_arith_decls(std::ostream & out) const { + unsigned sz = m_is_int.size(); + for (unsigned i = 0; i < sz; i++) { + if (is_int(i)) { + out << "(declare-fun "; m_display_var(out, i) << " () Int)\n"; + } + else { + out << "(declare-fun "; m_display_var(out, i) << " () Real)\n"; + } + } + return out; + } + + std::ostream& display_smt2_bool_decls(std::ostream & out) const { + unsigned sz = m_atoms.size(); + for (unsigned i = 0; i < sz; i++) { + if (m_atoms[i] == nullptr) + out << "(declare-fun b" << i << " () Bool)\n"; + } + return out; + } + + std::ostream& display_smt2(std::ostream & out) const { + display_smt2_bool_decls(out); + display_smt2_arith_decls(out); + out << "(assert (and true\n"; + for (clause* c : m_clauses) { + display_smt2(out, *c, m_display_var) << "\n"; + } + out << "))\n" << std::endl; + return out; + } + }; + + solver::solver(reslimit& rlim, params_ref const & p, bool incremental) { + m_ctx = alloc(ctx, rlim, p, incremental); + m_imp = alloc(imp, *this, *m_ctx); + } + + solver::solver(ctx& ctx) { + m_ctx = nullptr; + m_imp = alloc(imp, *this, ctx); + } + + solver::~solver() { + dealloc(m_imp); + dealloc(m_ctx); + } + + lbool solver::check() { + return m_imp->check(); + } + + lbool solver::check(literal_vector& assumptions) { + return m_imp->check(assumptions); + } + + void solver::get_core(vector& assumptions) { + return m_imp->get_core(assumptions); + } + + void solver::reset() { + m_imp->reset(); + } + + + void solver::updt_params(params_ref const & p) { + m_imp->updt_params(p); + } + + + void solver::collect_param_descrs(param_descrs & d) { + algebraic_numbers::manager::collect_param_descrs(d); + nlsat_params::collect_param_descrs(d); + } + + unsynch_mpq_manager & solver::qm() { + return m_imp->m_qm; + } + + anum_manager & solver::am() { + return m_imp->m_am; + } + + pmanager & solver::pm() { + return m_imp->m_pm; + } + + void solver::set_display_var(display_var_proc const & proc) { + m_imp->m_display_var.m_proc = &proc; + } + + void solver::set_display_assumption(display_assumption_proc const& proc) { + m_imp->m_display_assumption = &proc; + } + + + unsigned solver::num_vars() const { + return m_imp->num_vars(); + } + + bool solver::is_int(var x) const { + return m_imp->is_int(x); + } + + bool_var solver::mk_bool_var() { + return m_imp->mk_bool_var(); + } + + literal solver::mk_true() { + return literal(0, false); + } + + atom * solver::bool_var2atom(bool_var b) { + return m_imp->m_atoms[b]; + } + + void solver::vars(literal l, var_vector& vs) { + m_imp->vars(l, vs); + } + + atom_vector const& solver::get_atoms() { + return m_imp->m_atoms; + } + + atom_vector const& solver::get_var2eq() { + return m_imp->m_var2eq; + } + + evaluator& solver::get_evaluator() { + return m_imp->m_evaluator; + } + + explain& solver::get_explain() { + return m_imp->m_explain; + } + + void solver::reorder(unsigned sz, var const* p) { + m_imp->reorder(sz, p); + } + + void solver::restore_order() { + m_imp->restore_order(); + } + + void solver::set_rvalues(assignment const& as) { + m_imp->m_assignment.copy(as); + } + + void solver::get_rvalues(assignment& as) { + as.copy(m_imp->m_assignment); + } + + void solver::get_bvalues(svector const& bvars, svector& vs) { + vs.reset(); + for (bool_var b : bvars) { + vs.reserve(b + 1, l_undef); + if (!m_imp->m_atoms[b]) { + vs[b] = m_imp->m_bvalues[b]; + } + } + TRACE("nlsat", display(tout);); + } + + void solver::set_bvalues(svector const& vs) { + TRACE("nlsat", display(tout);); + for (bool_var b = 0; b < vs.size(); ++b) { + if (vs[b] != l_undef) { + m_imp->m_bvalues[b] = vs[b]; + SASSERT(!m_imp->m_atoms[b]); + } + } +#if 0 + m_imp->m_bvalues.reset(); + m_imp->m_bvalues.append(vs); + m_imp->m_bvalues.resize(m_imp->m_atoms.size(), l_undef); + for (unsigned i = 0; i < m_imp->m_atoms.size(); ++i) { + atom* a = m_imp->m_atoms[i]; + SASSERT(!a); + if (a) { + m_imp->m_bvalues[i] = to_lbool(m_imp->m_evaluator.eval(a, false)); + } + } +#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); + } + + bool_var solver::mk_ineq_atom(atom::kind k, unsigned sz, poly * const * ps, bool const * is_even) { + 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, 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) { + return m_imp->mk_root_atom(k, x, i, p); + } + + void solver::inc_ref(bool_var b) { + m_imp->inc_ref(b); + } + + 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_external_clause(num_lits, lits, a); + } + + std::ostream& solver::display(std::ostream & out) const { + return m_imp->display(out); + } + + std::ostream& solver::display(std::ostream & out, literal l) const { + return m_imp->display(out, l); + } + + std::ostream& solver::display(std::ostream & out, unsigned n, literal const* ls) const { + for (unsigned i = 0; i < n; ++i) { + display(out, ls[i]); + out << "; "; + } + return out; + } + + std::ostream& solver::display(std::ostream & out, literal_vector const& ls) const { + return display(out, ls.size(), ls.data()); + } + + 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(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); + } + + std::ostream& solver::display_smt2(std::ostream & out, literal_vector const& ls) const { + return display_smt2(out, ls.size(), ls.data()); + } + + std::ostream& solver::display(std::ostream & out, var x) const { + return m_imp->m_display_var(out, x); + } + + std::ostream& solver::display(std::ostream & out, atom const& a) const { + return m_imp->display(out, a, m_imp->m_display_var); + } + + display_var_proc const & solver::display_proc() const { + return m_imp->m_display_var; + } + + anum const & solver::value(var x) const { + if (m_imp->m_assignment.is_assigned(x)) + return m_imp->m_assignment.value(x); + return m_imp->m_zero; + } + + lbool solver::bvalue(bool_var b) const { + return m_imp->m_bvalues[b]; + } + + lbool solver::value(literal l) const { + return m_imp->value(l); + } + + bool solver::is_interpreted(bool_var b) const { + return m_imp->m_atoms[b] != 0; + } + + void solver::reset_statistics() { + return m_imp->reset_statistics(); + } + + void solver::collect_statistics(statistics & st) { + 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))); + } + +};