diff --git a/src/nlsat/CMakeLists.txt b/src/nlsat/CMakeLists.txt index cd073f0d5dc..077c420f9d9 100644 --- a/src/nlsat/CMakeLists.txt +++ b/src/nlsat/CMakeLists.txt @@ -7,7 +7,9 @@ z3_add_component(nlsat nlsat_simplify.cpp nlsat_solver.cpp nlsat_types.cpp - COMPONENT_DEPENDENCIES + nlsat_simple_checker.cpp + nlsat_variable_ordering_strategy.cpp + COMPONENT_DEPENDENCIES polynomial sat PYG_FILES diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index 618394ac1d6..49842100dba 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/src/nlsat/nlsat_explain.cpp @@ -45,6 +45,8 @@ namespace nlsat { bool m_minimize_cores; bool m_factor; bool m_signed_project; + bool m_cell_sample; + struct todo_set { polynomial::cache & m_cache; @@ -130,7 +132,7 @@ namespace nlsat { evaluator & m_evaluator; imp(solver & s, assignment const & x2v, polynomial::cache & u, atom_vector const & atoms, atom_vector const & x2eq, - evaluator & ev): + evaluator & ev, bool is_sample): m_solver(s), m_assignment(x2v), m_atoms(atoms), @@ -148,6 +150,9 @@ namespace nlsat { m_core1(s), m_core2(s), m_result(nullptr), + + m_cell_sample(is_sample), + m_evaluator(ev) { m_simplify_cores = false; m_full_dimensional = false; @@ -646,6 +651,45 @@ namespace nlsat { m_todo.insert(p); } } + + void add_sample_coeff(polynomial_ref_vector &ps, var x){ + polynomial_ref p(m_pm); + polynomial_ref lc(m_pm); + unsigned sz = ps.size(); + for (unsigned i = 0; i < sz; i++){ + p = ps.get(i); + unsigned k = degree(p, x); + SASSERT(k > 0); + TRACE("nlsat_explain", tout << "add_lc, x: "; display_var(tout, x); tout << "\nk: " << k << "\n"; display(tout, p); tout << "\n";); + for(; k > 0; k--){ + lc = m_pm.coeff(p, x, k); + add_factors(lc); + if (m_pm.nonzero_const_coeff(p, x, k)){ + TRACE("nlsat_explain", tout << "constant coefficient, skipping...\n";); + break; + } + } + SASSERT(sign(lc) != 0); + SASSERT(!is_const(lc)); + } + } + + void psc_resultant_sample(polynomial_ref_vector &ps, var x, polynomial_ref_vector & samples){ + polynomial_ref p(m_pm); + polynomial_ref q(m_pm); + SASSERT(samples.size() <= 2); + + for (unsigned i = 0; i < ps.size(); i++){ + p = ps.get(i); + for (unsigned j = 0; j < samples.size(); j++){ + q = samples.get(j); + if (!m_pm.eq(p, q)) { + psc(p, q, x); + } + } + } + } + /** \brief Add leading coefficients of the polynomials in ps. @@ -689,7 +733,6 @@ namespace nlsat { bool have_zero = false; for (unsigned i = 0; i < num_factors; i++) { f = m_factors.get(i); - // std::cout << "f=";display(std::cout, f) << "\n"; if (coeffs_are_zeroes_in_factor(f)) { have_zero = true; break; @@ -973,6 +1016,92 @@ namespace nlsat { add_simple_assumption(k, p, lsign); } + void cac_add_cell_lits(polynomial_ref_vector & ps, var y, polynomial_ref_vector & res) { + res.reset(); + SASSERT(m_assignment.is_assigned(y)); + bool lower_inf = true; + bool upper_inf = true; + scoped_anum_vector & roots = m_roots_tmp; + scoped_anum lower(m_am); + scoped_anum upper(m_am); + anum const & y_val = m_assignment.value(y); + TRACE("nlsat_explain", tout << "adding literals for "; display_var(tout, y); tout << " -> "; + m_am.display_decimal(tout, y_val); tout << "\n";); + polynomial_ref p_lower(m_pm); + unsigned i_lower = UINT_MAX; + polynomial_ref p_upper(m_pm); + unsigned i_upper = UINT_MAX; + polynomial_ref p(m_pm); + unsigned sz = ps.size(); + for (unsigned k = 0; k < sz; k++) { + p = ps.get(k); + if (max_var(p) != y) + continue; + roots.reset(); + // Variable y is assigned in m_assignment. We must temporarily unassign it. + // Otherwise, the isolate_roots procedure will assume p is a constant polynomial. + m_am.isolate_roots(p, undef_var_assignment(m_assignment, y), roots); + unsigned num_roots = roots.size(); + bool all_lt = true; + for (unsigned i = 0; i < num_roots; i++) { + int s = m_am.compare(y_val, roots[i]); + TRACE("nlsat_explain", + m_am.display_decimal(tout << "comparing root: ", roots[i]); tout << "\n"; + m_am.display_decimal(tout << "with y_val:", y_val); + tout << "\nsign " << s << "\n"; + tout << "poly: " << p << "\n"; + ); + if (s == 0) { + // y_val == roots[i] + // add literal + // ! (y = root_i(p)) + add_root_literal(atom::ROOT_EQ, y, i+1, p); + res.push_back(p); + return; + } + else if (s < 0) { + // y_val < roots[i] + if (i > 0) { + // y_val > roots[j] + int j = i - 1; + if (lower_inf || m_am.lt(lower, roots[j])) { + lower_inf = false; + m_am.set(lower, roots[j]); + p_lower = p; + i_lower = j + 1; + } + } + if (upper_inf || m_am.lt(roots[i], upper)) { + upper_inf = false; + m_am.set(upper, roots[i]); + p_upper = p; + i_upper = i + 1; + } + all_lt = false; + break; + } + } + if (all_lt && num_roots > 0) { + int j = num_roots - 1; + if (lower_inf || m_am.lt(lower, roots[j])) { + lower_inf = false; + m_am.set(lower, roots[j]); + p_lower = p; + i_lower = j + 1; + } + } + } + + if (!lower_inf) { + res.push_back(p_lower); + add_root_literal(m_full_dimensional ? atom::ROOT_GE : atom::ROOT_GT, y, i_lower, p_lower); + } + if (!upper_inf) { + res.push_back(p_upper); + add_root_literal(m_full_dimensional ? atom::ROOT_LE : atom::ROOT_LT, y, i_upper, p_upper); + } + } + /** Add one or two literals that specify in which cell of variable y the current interpretation is. One literal is added for the cases: @@ -1016,6 +1145,7 @@ namespace nlsat { // Otherwise, the isolate_roots procedure will assume p is a constant polynomial. m_am.isolate_roots(p, undef_var_assignment(m_assignment, y), roots); unsigned num_roots = roots.size(); + bool all_lt = true; for (unsigned i = 0; i < num_roots; i++) { int s = m_am.compare(y_val, roots[i]); TRACE("nlsat_explain", @@ -1033,25 +1163,33 @@ namespace nlsat { } else if (s < 0) { // y_val < roots[i] - - // check if roots[i] is a better upper bound + if (i > 0) { + // y_val > roots[j] + int j = i - 1; + if (lower_inf || m_am.lt(lower, roots[j])) { + lower_inf = false; + m_am.set(lower, roots[j]); + p_lower = p; + i_lower = j + 1; + } + } if (upper_inf || m_am.lt(roots[i], upper)) { upper_inf = false; m_am.set(upper, roots[i]); p_upper = p; - i_upper = i+1; + i_upper = i + 1; } + all_lt = false; + break; } - else if (s > 0) { - // roots[i] < y_val - - // check if roots[i] is a better lower bound - if (lower_inf || m_am.lt(lower, roots[i])) { - lower_inf = false; - m_am.set(lower, roots[i]); - p_lower = p; - i_lower = i+1; - } + } + if (all_lt && num_roots > 0) { + int j = num_roots - 1; + if (lower_inf || m_am.lt(lower, roots[j])) { + lower_inf = false; + m_am.set(lower, roots[j]); + p_lower = p; + i_lower = j + 1; } } } @@ -1064,6 +1202,7 @@ namespace nlsat { } } + /** \brief Return true if all polynomials in ps are univariate in x. */ @@ -1082,7 +1221,8 @@ namespace nlsat { /** \brief Apply model-based projection operation defined in our paper. */ - void project(polynomial_ref_vector & ps, var max_x) { + + void project_original(polynomial_ref_vector & ps, var max_x) { if (ps.empty()) return; m_todo.reset(); @@ -1094,12 +1234,12 @@ namespace nlsat { if (x < max_x) add_cell_lits(ps, x); while (true) { - TRACE("nlsat_explain", tout << "project loop, processing var "; display_var(tout, x); tout << "\npolynomials\n"; - display(tout, ps); tout << "\n";); if (all_univ(ps, x) && m_todo.empty()) { m_todo.reset(); break; } + TRACE("nlsat_explain", tout << "project loop, processing var "; display_var(tout, x); tout << "\npolynomials\n"; + display(tout, ps); tout << "\n";); add_lc(ps, x); psc_discriminant(ps, x); psc_resultant(ps, x); @@ -1110,6 +1250,68 @@ namespace nlsat { } } + /** + * Sample Projection + * Reference: + * Haokun Li and Bican Xia. + * "Solving Satisfiability of Polynomial Formulas By Sample - Cell Projection" + * https://arxiv.org/abs/2003.00409 + */ + void project_cdcac(polynomial_ref_vector & ps, var max_x) { + if (ps.empty()) + return; + bool first = true; + m_todo.reset(); + for (poly* p : ps) { + m_todo.insert(p); + } + var x = m_todo.remove_max_polys(ps); + // Remark: after vanishing coefficients are eliminated, ps may not contain max_x anymore + + polynomial_ref_vector samples(m_pm); + + + if (x < max_x){ + cac_add_cell_lits(ps, x, samples); + } + + while (true) { + if (all_univ(ps, x) && m_todo.empty()) { + m_todo.reset(); + break; + } + TRACE("nlsat_explain", tout << "project loop, processing var "; display_var(tout, x); tout << "\npolynomials\n"; + display(tout, ps); tout << "\n";); + + if (first) { + add_lc(ps, x); + psc_discriminant(ps, x); + psc_resultant(ps, x); + first = false; + } + else { + add_lc(ps, x); + // add_sample_coeff(ps, x); + psc_discriminant(ps, x); + psc_resultant_sample(ps, x, samples); + } + + if (m_todo.empty()) + break; + x = m_todo.remove_max_polys(ps); + cac_add_cell_lits(ps, x, samples); + } + } + + void project(polynomial_ref_vector & ps, var max_x) { + if (m_cell_sample) { + project_cdcac(ps, max_x); + } + else { + project_original(ps, max_x); + } + } + bool check_already_added() const { for (bool b : m_already_added_literal) { (void)b; @@ -1474,7 +1676,7 @@ namespace nlsat { var max_x = max_var(m_ps); TRACE("nlsat_explain", tout << "polynomials in the conflict:\n"; display(tout, m_ps); tout << "\n";); elim_vanishing(m_ps); - TRACE("nlsat_explain", tout << "elim vanishing x" << max_x << "\n"; display(tout, m_ps); tout << "\n";); + TRACE("nlsat_explain", tout << "elim vanishing\n"; display(tout, m_ps); tout << "\n";); project(m_ps, max_x); TRACE("nlsat_explain", tout << "after projection\n"; display(tout, m_ps); tout << "\n";); } @@ -1936,8 +2138,8 @@ namespace nlsat { }; explain::explain(solver & s, assignment const & x2v, polynomial::cache & u, - atom_vector const& atoms, atom_vector const& x2eq, evaluator & ev) { - m_imp = alloc(imp, s, x2v, u, atoms, x2eq, ev); + atom_vector const& atoms, atom_vector const& x2eq, evaluator & ev, bool use_cell_sample) { + m_imp = alloc(imp, s, x2v, u, atoms, x2eq, ev, use_cell_sample); } explain::~explain() { diff --git a/src/nlsat/nlsat_explain.h b/src/nlsat/nlsat_explain.h index 20322a680aa..2fdb76b1150 100644 --- a/src/nlsat/nlsat_explain.h +++ b/src/nlsat/nlsat_explain.h @@ -34,7 +34,8 @@ namespace nlsat { imp * m_imp; public: explain(solver & s, assignment const & x2v, polynomial::cache & u, - atom_vector const& atoms, atom_vector const& x2eq, evaluator & ev); + atom_vector const& atoms, atom_vector const& x2eq, evaluator & ev, bool use_cell_sample_proj); + ~explain(); void reset(); diff --git a/src/nlsat/nlsat_interval_set.cpp b/src/nlsat/nlsat_interval_set.cpp index f928fd5b6cc..76a310f00f9 100644 --- a/src/nlsat/nlsat_interval_set.cpp +++ b/src/nlsat/nlsat_interval_set.cpp @@ -684,34 +684,51 @@ namespace nlsat { return new_set; } - void interval_set_manager::peek_in_complement(interval_set const * s, bool is_int, anum & w, bool randomize) { + int compare_interval_with_zero(const interval &now, const scoped_anum &zero, anum_manager & m) { + if (!now.m_upper_inf) { + int sgn = m.compare(now.m_upper, zero); + if (sgn < 0) + return -1; + if (sgn == 0 && now.m_upper_open) + return -1; + } + if (!now.m_lower_inf) { + int sgn = m.compare(now.m_lower, zero); + if (sgn > 0) + return 1; + if (sgn == 0 && now.m_lower_open) + return 1; + } + return 0; + } + + + void interval_set_manager::pick_in_complement(interval_set const * s, bool is_int, anum & w, bool randomize) { SASSERT(!is_full(s)); if (s == nullptr) { - if (randomize) { - int num = m_rand() % 2 == 0 ? 1 : -1; -#define MAX_RANDOM_DEN_K 4 - int den_k = (m_rand() % MAX_RANDOM_DEN_K); - int den = is_int ? 1 : (1 << den_k); - scoped_mpq _w(m_am.qm()); - m_am.qm().set(_w, num, den); - m_am.set(w, _w); - } - else { - m_am.set(w, 0); - } + m_am.set(w, 0); return; } - unsigned n = 0; - unsigned num = num_intervals(s); - if (!s->m_intervals[0].m_lower_inf) { - // lower is not -oo - n++; - m_am.int_lt(s->m_intervals[0].m_lower, w); - if (!randomize) - return; + // try to assign w to zero first to simplify the polynomials + scoped_anum zero(m_am); + m_am.set(zero, 0); + bool available = true; + for (unsigned i = 0; i < num; ++i) { + int sgn = compare_interval_with_zero(s->m_intervals[i], zero, m_am); + if (sgn == 0) { + available = false; + break; + } + if (sgn > 0) + break; + } + if (available) { + m_am.set(w, 0); + return ; } + // cannot assign w to zero if (!s->m_intervals[num-1].m_upper_inf) { // upper is not oo n++; @@ -720,6 +737,16 @@ namespace nlsat { if (!randomize) return; } + + if (!s->m_intervals[0].m_lower_inf) { + // lower is not -oo + n++; + m_am.int_lt(s->m_intervals[0].m_lower, w); + if (!randomize) + return; + } + + // Try to find a gap that is not an unit. for (unsigned i = 1; i < num; i++) { @@ -770,5 +797,4 @@ namespace nlsat { out << "*"; return out; } - }; diff --git a/src/nlsat/nlsat_interval_set.h b/src/nlsat/nlsat_interval_set.h index f1055118f5d..2e74f33c623 100644 --- a/src/nlsat/nlsat_interval_set.h +++ b/src/nlsat/nlsat_interval_set.h @@ -21,7 +21,7 @@ Revision History: #include "nlsat/nlsat_types.h" namespace nlsat { - + class interval_set; class interval_set_manager { @@ -29,6 +29,7 @@ namespace nlsat { small_object_allocator & m_allocator; svector m_already_visited; random_gen m_rand; + void del(interval_set * s); public: interval_set_manager(anum_manager & m, small_object_allocator & a); @@ -107,7 +108,7 @@ namespace nlsat { \pre !is_full(s) */ - void peek_in_complement(interval_set const * s, bool is_int, anum & w, bool randomize); + void pick_in_complement(interval_set const * s, bool is_int, anum & w, bool randomize); }; typedef obj_ref interval_set_ref; diff --git a/src/nlsat/nlsat_params.pyg b/src/nlsat/nlsat_params.pyg index cac33fe8717..01229a527bc 100644 --- a/src/nlsat/nlsat_params.pyg +++ b/src/nlsat/nlsat_params.pyg @@ -3,6 +3,9 @@ def_module_params('nlsat', description='nonlinear solver', export=True, params=(max_memory_param(), + ('simple_check', BOOL, False, "precheck polynomials using variables sign"), + ('variable_ordering_strategy', UINT, 0, "Variable Ordering Strategy, 0 for none, 1 for BROWN, 2 for TRIANGULAR, 3 for ONLYPOLY"), + ('cell_sample', BOOL, True, "cell sample projection"), ('lazy', UINT, 0, "how lazy the solver is."), ('reorder', BOOL, True, "reorder variables."), ('log_lemmas', BOOL, False, "display lemmas as self-contained SMT formulas"), @@ -14,6 +17,5 @@ def_module_params('nlsat', ('shuffle_vars', BOOL, False, "use a random variable order."), ('inline_vars', BOOL, False, "inline variables that can be isolated from equations (not supported in incremental mode)"), ('seed', UINT, 0, "random seed."), - ('factor', BOOL, True, "factor polynomials produced during conflict resolution.") + ('factor', BOOL, True, "factor polynomials produced during conflict resolution.") )) - diff --git a/src/nlsat/nlsat_simple_checker.cpp b/src/nlsat/nlsat_simple_checker.cpp new file mode 100644 index 00000000000..3e1e8dd1c36 --- /dev/null +++ b/src/nlsat/nlsat_simple_checker.cpp @@ -0,0 +1,1581 @@ +#include "nlsat/nlsat_simple_checker.h" + +struct Debug_Tracer { + std::string tag_str; + Debug_Tracer(std::string _tag_str) { + tag_str = _tag_str; + TRACE("simple_checker", + tout << "Debug_Tracer begin\n"; + tout << tag_str << "\n"; + ); + } + ~Debug_Tracer() { + TRACE("simple_checker", + tout << "Debug_Tracer end\n"; + tout << tag_str << "\n"; + ); + } +}; + + +namespace nlsat { + struct Simple_Checker::imp { + // solver / + pmanager ± + anum_manager &am; + const clause_vector &clauses; + literal_vector &learned_unit; + const atom_vector &atoms; + const unsigned arith_var_num; + // unsigned all_var_num; + enum sign_kind { EQ = 0, LT, GT, NONE, LE, GE, NEQ}; + void display(std::ostream & out, const sign_kind &sk) { + if (sk == EQ) + out << "=="; + else if (sk == LT) + out << "<"; + else if (sk == GT) + out << ">"; + else if (sk == NONE) + out << "<=>"; + else if (sk == LE) + out << "<="; + else if (sk == GE) + out << ">="; + else if (sk == NEQ) + out << "!="; + else + UNREACHABLE(); + } + struct Endpoint { + anum_manager &m_am; + unsigned m_open:1; + unsigned m_inf:1; + unsigned m_is_lower:1; + scoped_anum m_val; + Endpoint(anum_manager &_am) : + m_am(_am), + m_open(1), + m_inf(1), + m_is_lower(1), + m_val(_am) { + } + Endpoint(anum_manager &_am, unsigned _open, unsigned _inf, unsigned _islower) : + m_am(_am), + m_open(_open), + m_inf(_inf), + m_is_lower(_islower), + m_val(_am) { + } + Endpoint(anum_manager &_am, unsigned _open, unsigned _inf, unsigned _islower, const scoped_anum &_val) : + m_am(_am), + m_open(_open), + m_inf(_inf), + m_is_lower(_islower), + m_val(_am) { + m_am.set(m_val, _val); + } + bool operator== (const Endpoint &rhs) const { + if (m_inf && rhs.m_inf && m_is_lower == rhs.m_is_lower) + return true; + if (!m_inf && !rhs.m_inf && m_open == rhs.m_open && m_val == rhs.m_val) { + if (!m_open) + return true; + if (m_is_lower == rhs.m_is_lower) + return true; + } + return false; + } + bool operator< (const Endpoint &rhs) const { + if (m_inf) { + if (m_is_lower) { + if (rhs.m_inf && rhs.m_is_lower) + return false; + else + return true; + } + else { + return false; + } + } + else { + if (rhs.m_inf) { + if (rhs.m_is_lower) + return false; + else + return true; + } + else { + if (m_val == rhs.m_val) { + if (!m_open && !rhs.m_open) { // {[, [} + // {[, [} {[, ]} {], [} {], ]} + return false; + } + else if (!m_open) { // {[, (} + // [ < (, [ > ), ] < (, ] > ) + if (rhs.m_is_lower) + return true; + else + return false; + } + else if (!rhs.m_open) { // {(, [} + if (m_is_lower) // x + EPS + return false; + else // x - EPS + return true; + } + else { // {(, (} + // ( == (, ( > ), ) < (, ) == ) + if (!m_is_lower && rhs.m_is_lower) + return true; + else + return false; + } + } + else { + return m_val < rhs.m_val; + } + } + } + } + void copy(const Endpoint &ep) { + m_inf = ep.m_inf; + m_open = ep.m_open; + m_is_lower = ep.m_is_lower; + if (!m_inf) + m_am.set(m_val, ep.m_val); + } + void set_num(const scoped_anum &num, unsigned is_lower) { + m_open = 0; + m_inf = 0; + m_is_lower = is_lower; + m_am.set(m_val, num); + } + void set_num(int num, unsigned is_lower) { + m_open = 0; + m_inf = 0; + m_is_lower = is_lower; + m_am.set(m_val, num); + } + bool is_neg() const { + if (m_inf) { + if (m_is_lower) + return true; + else + return false; + } + else { + if (m_am.is_zero(m_val)) { + if (m_open) { + if (m_is_lower) + return false; + else + return true; + } + else { + return false; + } + } + else { + return m_am.is_neg(m_val); + } + } + } + bool is_zero(unsigned is_open = 0) const { + return !m_inf && m_open == is_open && m_am.is_zero(m_val); + } + }; + struct Domain_Interval { + anum_manager &m_am; + Endpoint m_lower; + Endpoint m_upper; + Domain_Interval(anum_manager &_am) : + m_am(_am), + m_lower(_am, 1, 1, 1), + m_upper(_am, 1, 1, 0) { + // (-oo, +oo) + } + Domain_Interval(anum_manager &_am, + unsigned _lower_open, unsigned _lower_inf, + unsigned _upper_open, unsigned _upper_inf) : + m_am(_am), + m_lower(_am, _lower_open, _lower_inf, 1), + m_upper(_am, _upper_open, _upper_inf, 0) { + } + void copy(const Domain_Interval &di) { + m_lower.copy(di.m_lower); + m_upper.copy(di.m_upper); + } + void set_num(const scoped_anum &num) { + m_lower.set_num(num, 1); + m_upper.set_num(num, 0); + } + void set_num(int num) { + m_lower.set_num(num, 1); + m_upper.set_num(num, 0); + } + }; + + void display(std::ostream & out, anum_manager & am, Domain_Interval const & curr) { + if (curr.m_lower.m_inf) { + out << "(-oo, "; + } + else { + if (curr.m_lower.m_open) + out << "("; + else + out << "["; + am.display_decimal(out, curr.m_lower.m_val); + out << ", "; + } + if (curr.m_upper.m_inf) { + out << "oo)"; + } + else { + am.display_decimal(out, curr.m_upper.m_val); + if (curr.m_upper.m_open) + out << ")"; + else + out << "]"; + } + } + + struct Var_Domain { + Domain_Interval ori_val; // original, ext sign + Domain_Interval mag_val; // magnitude + Var_Domain(anum_manager &am) : + ori_val(am), + mag_val(am) { + mag_val.m_lower.set_num(0, 1); + } + void copy(const Var_Domain &vd) { + ori_val.copy(vd.ori_val); + mag_val.copy(vd.mag_val); + } + }; + vector vars_domain; + struct Clause_Visit_Tag { + bool visited; + bool_vector literal_visited; + Clause_Visit_Tag() : visited(false) {} + }; + vector clauses_visited; + bool improved; + enum special_ineq_kind {UNK = 0, AXBC, AXBSC, NK}; // None Kind + vector> literal_special_kind; + imp(pmanager &_pm, anum_manager &_am, const clause_vector &_clauses, literal_vector &_learned_unit, const atom_vector &_atoms, const unsigned &_arith_var_num) : + // sol(_sol), + pm(_pm), + am(_am), + clauses(_clauses), + learned_unit(_learned_unit), + atoms(_atoms), + arith_var_num(_arith_var_num) { + // all_var_num = atoms.size(); + for (unsigned i = 0; i < arith_var_num; ++i) { + vars_domain.push_back(Var_Domain(am)); + } + clauses_visited.resize(clauses.size()); + literal_special_kind.resize(clauses.size()); + } + sign_kind to_sign_kind(atom::kind kd) { + if (kd == atom::EQ) + return EQ; + if (kd == atom::LT) + return LT; + if (kd == atom::GT) + return GT; + UNREACHABLE(); + return EQ; + } + bool update_interval_intersection(Domain_Interval &ia, const Domain_Interval &ib) { + TRACE("simple_checker", + tout << "ia: "; + display(tout, am, ia); + tout << "\nib: "; + display(tout, am, ib); + tout << "\n"; + tout << "ia.lower < ib.lower: " << (ia.m_lower < ib.m_lower) << '\n'; + tout << "ia.m_upper < ib.m_upper: " << (ia.m_upper < ib.m_upper) << '\n'; + ); + if (ia.m_lower < ib.m_lower) { + ia.m_lower.copy(ib.m_lower); + improved = true; + } + + if (ib.m_upper < ia.m_upper) { + ia.m_upper.copy(ib.m_upper); + improved = true; + } + if (ia.m_upper < ia.m_lower) + return false; + + + + TRACE("simple_checker", + tout << "after update: "; + display(tout, am, ia); + tout << "\n"; + ); + return true; + } + + bool update_var_ori_domain_interval(Var_Domain &vd, const Domain_Interval &di) { + return update_interval_intersection(vd.ori_val, di); + } + bool update_var_mag_domain_interval_by_ori(Var_Domain &vd, const Domain_Interval &di) { + TRACE("simple_checker", + tout << "vd mag val: "; + display(tout, am, vd.mag_val); + tout << "\n"; + tout << "di: "; + display(tout, am, di); + tout << "\n"; + ); + Domain_Interval mag_di(am, 0, 0, 1, 1); + + if (di.m_lower.m_inf) { + mag_di.m_upper.m_inf = 1; + mag_di.m_upper.m_open = 1; + if (am.is_neg(di.m_upper.m_val)) { + // am.neg(di.m_upper); + am.set(mag_di.m_lower.m_val, di.m_upper.m_val*-1); + mag_di.m_lower.m_open = di.m_upper.m_open; + } + else if (am.is_zero(di.m_upper.m_val)) { + mag_di.m_lower.m_open = di.m_upper.m_open; + } + else { + return true; + } + } + else if (di.m_upper.m_inf) { + mag_di.m_upper.m_inf = 1; + mag_di.m_upper.m_open = 1; + if (am.is_neg(di.m_lower.m_val)) { + return true; + } + else if (am.is_zero(di.m_lower.m_val)) { + mag_di.m_lower.m_open = di.m_lower.m_open; + } + else { + am.set(mag_di.m_lower.m_val, di.m_lower.m_val); + mag_di.m_lower.m_open = di.m_lower.m_open; + } + } + else { + mag_di.m_lower.m_inf = 0; + mag_di.m_upper.m_inf = 0; + if (!am.is_neg(di.m_lower.m_val)) { + mag_di.m_lower.m_open = di.m_lower.m_open; + mag_di.m_upper.m_open = di.m_upper.m_open; + am.set(mag_di.m_lower.m_val, di.m_lower.m_val); + am.set(mag_di.m_upper.m_val, di.m_upper.m_val); + } + else if (!am.is_pos(di.m_upper.m_val)) { + mag_di.m_lower.m_open = di.m_upper.m_open; + mag_di.m_upper.m_open = di.m_lower.m_open; + + am.set(mag_di.m_lower.m_val, di.m_upper.m_val*-1); + am.set(mag_di.m_upper.m_val, di.m_lower.m_val*-1); + } + else { + scoped_anum nl(am); + am.set(nl, di.m_lower.m_val); + am.neg(nl); + am.set(mag_di.m_lower.m_val, 0); + mag_di.m_lower.m_open = 0; + if (nl < di.m_upper.m_val) { + mag_di.m_upper.m_open = di.m_upper.m_open; + am.set(mag_di.m_upper.m_val, di.m_upper.m_val); + } + else if (nl == di.m_upper.m_val) { + mag_di.m_upper.m_open = (di.m_lower.m_open | di.m_upper.m_open); + am.set(mag_di.m_upper.m_val, di.m_upper.m_val); + } + else { + mag_di.m_upper.m_open = di.m_lower.m_open; + am.set(mag_di.m_upper.m_val, nl); + } + } + } + TRACE("simple_checker", + tout << "mag di: "; + display(tout, am, mag_di); + tout << "\n"; + ); + return update_interval_intersection(vd.mag_val, mag_di); + } + void calc_formula(scoped_anum &num, const scoped_anum &a, unsigned b, const scoped_anum &c) { + scoped_anum frac(am); + am.div(c, a, frac); + am.neg(frac); + if (b > 1) + am.root(frac, b, num); + else + am.set(num, frac); + } + bool process_odd_degree_formula(Var_Domain &vd, sign_kind nsk, const scoped_anum &a, unsigned b, const scoped_anum &c) { + Domain_Interval now_di(am); + scoped_anum num(am); + calc_formula(num, a, b, c); + TRACE("simple_checker", + tout << "nsk: "; + display(tout, nsk); + tout << '\n'; + tout << "num: " << num << '\n'; + ); + if (nsk == EQ) { + now_di.set_num(num); + // am.set(now_di.m_lower.m_val, num); + // am.set(now_di.m_upper.m_val, num); + // now_di.m_lower.m_inf = 0; + // now_di.m_upper.m_inf = 0; + // now_di.m_lower.m_open = 0; + // now_di.m_upper.m_open = 0; + } + else if (nsk == LT) { + am.set(now_di.m_upper.m_val, num); + now_di.m_upper.m_inf = 0; + now_di.m_upper.m_open = 1; + } + else if (nsk == GT) { + am.set(now_di.m_lower.m_val, num); + now_di.m_lower.m_inf = 0; + now_di.m_lower.m_open = 1; + } + else if (nsk == LE) { + am.set(now_di.m_upper.m_val, num); + now_di.m_upper.m_inf = 0; + now_di.m_upper.m_open = 0; + } + else if (nsk == GE) { + am.set(now_di.m_lower.m_val, num); + now_di.m_lower.m_inf = 0; + now_di.m_lower.m_open = 0; + } + else { + UNREACHABLE(); + } + TRACE("simple_checker", + tout << "now_di: "; + display(tout, am, now_di); + tout << "\n"; + ); + if (!update_var_ori_domain_interval(vd, now_di)) + return false; + if (!update_var_mag_domain_interval_by_ori(vd, vd.ori_val)) + return false; + return true; + } + + bool process_even_degree_formula(Var_Domain &vd, sign_kind nsk, const scoped_anum &a, unsigned b, const scoped_anum &c) { + scoped_anum num(am), frac(am); + am.div(c, a, frac); + am.neg(frac); + + if (frac < 0) { + if (nsk == EQ || nsk == LT || nsk == LE) { + return false; + } + else if (nsk == GT || nsk == GE) { + return true; + } + else { + UNREACHABLE(); + } + } + else if (frac == 0) { + if (nsk == EQ || nsk == LE) { + Domain_Interval di(am); + di.set_num(0); + if (!update_interval_intersection(vd.ori_val, di)) + return false; + if (!update_interval_intersection(vd.mag_val, di)) + return false; + } + else if (nsk == LT) { + return false; + } + else if (nsk == GT) { + Domain_Interval di(am); + di.m_lower.set_num(0, 1); + if (!update_interval_intersection(vd.mag_val, di)) + return false; + } + else if (nsk == GE) { + return true; + } + else { + UNREACHABLE(); + } + } + else { + scoped_anum num(am); + am.root(frac, b, num); + if (nsk == EQ) { + Domain_Interval di(am); + di.set_num(num); + // di.m_lower_open = 0; + // di.m_upper_open = 0; + // di.m_lower_inf = 0; + // di.m_upper_inf = 0; + // am.set(di.m_lower, num); + // am.set(di.m_upper, num); + if (!update_interval_intersection(vd.mag_val, di)) + return false; + } + else if (nsk == LT) { + Domain_Interval di(am, 0, 0, 1, 0); + // [0, num) + am.set(di.m_lower.m_val, 0); + am.set(di.m_upper.m_val, num); + if (!update_interval_intersection(vd.mag_val, di)) + return false; + + // (-num, num) + di.m_lower.m_open = 1; + // am.set(di.m_upper, num); + am.neg(num); + am.set(di.m_lower.m_val, num); + if (!update_interval_intersection(vd.ori_val, di)) + return false; + } + else if (nsk == GT) { + // (num, inf) + Domain_Interval di(am, 1, 0, 1, 1); + // di.m_lower_open = 1; + // di.m_upper_open = 1; + // di.m_lower_inf = 0; + // di.m_upper_inf = 1; + am.set(di.m_lower.m_val, num); + if (!update_interval_intersection(vd.mag_val, di)) + return false; + } + else if (nsk == LE) { + Domain_Interval di(am, 0, 0, 0, 0); + // [0, num] + // di.m_lower_open = 0; + // di.m_upper_open = 0; + // di.m_lower_inf = 0; + // di.m_upper_inf = 0; + am.set(di.m_lower.m_val, 0); + am.set(di.m_upper.m_val, num); + if (!update_interval_intersection(vd.mag_val, di)) + return false; + // [-num, num] + // am.set(di.m_upper, num); + am.neg(num); + am.set(di.m_lower.m_val, num); + if (!update_interval_intersection(vd.ori_val, di)) + return false; + } + else if (nsk == GE) { + // [num, inf) + Domain_Interval di(am, 0, 0, 1, 1); + // di.m_lower_open = 0; + // di.m_upper_open = 1; + // di.m_lower_inf = 0; + // di.m_upper_inf = 1; + am.set(di.m_lower.m_val, num); + if (!update_interval_intersection(vd.mag_val, di)) + return false; + } + else { + UNREACHABLE(); + } + } + return true; + } + + bool update_var_domain(sign_kind nsk, const scoped_anum &a, var x, unsigned b, const scoped_anum &c) { + Var_Domain &vd = vars_domain[x]; + if (am.is_neg(a)) { + if (nsk == LT) + nsk = GT; + else if (nsk == GT) + nsk = LT; + else if (nsk == LE) + nsk = GE; + else if (nsk == GE) + nsk = LE; + } + if (nsk == NEQ) { + if (am.is_zero(c)) { + Domain_Interval di(am, 1, 0, 1, 1); + am.set(di.m_lower.m_val, 0); + return update_interval_intersection(vd.mag_val, di); + } + else { + return true; + } + } + if ((b & 1) == 1) + return process_odd_degree_formula(vd, nsk, a, b, c); + else + return process_even_degree_formula(vd, nsk, a, b, c); + } + + bool check_is_axbc(const poly *p, scoped_anum &a, var &x, unsigned &b, scoped_anum& c) { + // is a*(x^b) + c*1 form + if (pm.size(p) == 1 && pm.is_var(pm.get_monomial(p, 0), x)) { + am.set(a, 1); + b = 1; + am.set(c, 0); + return true; + } + if (pm.size(p) != 2) + return false; + if (!pm.is_unit(pm.get_monomial(p, 1))) + return false; + monomial *m = pm.get_monomial(p, 0); + if (pm.size(m) != 1) + return false; + x = pm.get_var(m, 0); + b = pm.degree(m, 0); + + am.set(a, pm.coeff(p, 0)); + am.set(c, pm.coeff(p, 1)); + return true; + } + + bool collect_domain_axbc_form(unsigned cid, unsigned lid) { + // is_var_num, a*(x^b) + c form + literal lit = (*clauses[cid])[lid]; + bool s = lit.sign(); + ineq_atom *ia = to_ineq_atom(atoms[lit.var()]); + if (ia->size() > 1) { + // clauses_visited[cid].visited = true; + return true; + } + poly *p = ia->p(0); + if (literal_special_kind[cid][lid] != UNK && + literal_special_kind[cid][lid] != AXBC) + return true; + var x; + scoped_anum a(am), c(am); + unsigned b; + + if (!check_is_axbc(p, a, x, b, c)) { + // vec_id.push_back(cid); + return true; + } + clauses_visited[cid].visited = true; + literal_special_kind[cid][lid] = AXBC; + sign_kind nsk = to_sign_kind(ia->get_kind()); + if (s) { + if (nsk == EQ) + nsk = NEQ; + else if (nsk == LT) + nsk = GE; + else if (nsk == GT) + nsk = LE; + } + TRACE("simple_checker", + tout << a << "x[" << x << "]^" << b << " + " << c << " "; + display(tout, nsk); + tout << " 0 \n"; + ); + if (!update_var_domain(nsk, a, x, b, c)) + return false; + TRACE("simple_checker", + tout << "original: "; + display(tout, am, vars_domain[x].ori_val); + tout << "\nmagnitude: "; + display(tout, am, vars_domain[x].mag_val); + tout << "\n"; + ); + return true; + } + bool check_is_axbsc(const poly *p, vector &as, vector &xs, vector &bs, scoped_anum& c, unsigned &cnt) { + // [a*(x^b)] + ... + [a*(x^b)] + c form + unsigned psz = pm.size(p); + am.set(c, 0); + for (unsigned i = 0; i < psz; ++i) { + monomial *m = pm.get_monomial(p, i); + if (pm.size(m) > 1) + return false; + } + cnt = 0; + for (unsigned i = 0; i < psz; ++i) { + monomial *m = pm.get_monomial(p, i); + if (pm.size(m) == 0) { + am.set(c, pm.coeff(p, i)); + } + else { + // as.push_back(scoped_anum(am)); + am.set(as[cnt++], pm.coeff(p, i)); + xs.push_back(pm.get_var(m, 0)); + bs.push_back(pm.degree(m, 0)); + } + } + return true; + } + + sign_kind get_axb_sign(const scoped_anum &a, var x, unsigned b) { + Var_Domain &vd = vars_domain[x]; + if (vd.ori_val.m_lower.is_zero() && + vd.ori_val.m_upper.is_zero()) + return EQ; + if ((b & 1) == 0) { + if (am.is_pos(a)) { // a > 0 + if (vd.mag_val.m_lower.is_zero(0)) + return GE; + else + return GT; + } + else { + if (vd.mag_val.m_lower.is_zero(0)) + return LE; + else + return LT; + } + } else { + sign_kind ret = NONE; + if (!vd.ori_val.m_lower.m_inf && !vd.ori_val.m_upper.m_inf) { + if (am.is_zero(vd.ori_val.m_lower.m_val)) { + if (vd.ori_val.m_lower.m_open) + ret = GT; + else + ret = GE; + } + else if (am.is_pos(vd.ori_val.m_lower.m_val)) { + ret = GT; + } + if (am.is_zero(vd.ori_val.m_upper.m_val)) { + if (vd.ori_val.m_upper.m_open) + ret = LT; + else + ret = LE; + } + else if (am.is_neg(vd.ori_val.m_upper.m_val)) { + ret = LT; + } + } + else if (!vd.ori_val.m_lower.m_inf) { + if (am.is_pos(vd.ori_val.m_lower.m_val)) { + ret = GT; + } + else if (am.is_zero(vd.ori_val.m_lower.m_val)) { + if (vd.ori_val.m_lower.m_open) + ret = GT; + else + ret = GE; + } + } + else if (!vd.ori_val.m_upper.m_inf) { + if (am.is_neg(vd.ori_val.m_upper.m_val)) { + ret = LT; + } + else if (am.is_zero(vd.ori_val.m_upper.m_val)) { + if (vd.ori_val.m_upper.m_open) + ret = LT; + else + ret = LE; + } + } + if (a < 0) { + if (ret == LT) + ret = GT; + else if (ret == LE) + ret = GE; + else if (ret == GT) + ret = LT; + else if (ret == GE) + ret = LE; + } + return ret; + } + } + + bool check_is_sign_ineq_consistent(sign_kind &nsk, vector &as, vector &xs, vector &bs, scoped_anum& c, bool &is_conflict) { + sign_kind sta = get_axb_sign(as[0], xs[0], bs[0]); + if (sta == NONE) + return false; + unsigned sz = as.size(); + for (unsigned i = 1; i < sz; ++i) { + sign_kind now = get_axb_sign(as[i], xs[i], bs[i]); + TRACE("simple_checker", + tout << "sta: "; + display(tout, sta); + tout << "\n"; + tout << "now: "; + display(tout, now); + tout << "\n"; + ); + if (now == NONE) + return false; + if (sta == EQ) { + sta = now; + } + else if (sta == LT || sta == LE) { + if (now != LT && now != LE) + return false; + if (sta != now) + sta = LT; + } + else { + if (now != GT && now != GE) + return false; + if (sta != now) + sta = GT; + } + TRACE("simple_checker", + tout << "after merge\n"; + tout << "sta: "; + display(tout, sta); + tout << "\n"; + ); + } + TRACE("simple_checker", + tout << "sta: "; + display(tout, sta); + tout << "\n"; + tout << "nsk: "; + display(tout, nsk); + tout << "\n"; + tout << "c: "; + am.display(tout, c); + tout << "\n"; + ); +/* +if (am.is_neg(c)) { // ( == 0) + (c < 0) -> < 0 + +} +else if (am.is_zero(c)) { // ( == 0) + (c == 0) -> == 0 + +} +else { // ( == 0) + (c > 0) -> > 0 + +} +*/ + if (sta == EQ) { + if (am.is_neg(c)) { // ( == 0) + (c < 0) -> < 0 + if (nsk == EQ || nsk == GE || nsk == GT) { + is_conflict = true; + return true; + } + else { + return false; + } + } + else if (am.is_zero(c)) { // ( == 0) + (c == 0) -> == 0 + if (nsk == GT || nsk == LT) { + is_conflict = true; + return true; + } + else { + return false; + } + } + else { // ( == 0) + (c > 0) -> > 0 + if (nsk == EQ || nsk == LE || nsk == LT) { + is_conflict = true; + return true; + } + else { + return false; + } + } + } + else if (sta == LT) { + if (am.is_neg(c)) { // ( < 0) + (c < 0) -> < 0 + if (nsk == EQ || nsk == GE || nsk == GT) { + is_conflict = true; + return true; + } + else { + return false; + } + } + else if (am.is_zero(c)) { // ( < 0) + (c == 0) -> < 0 + if (nsk == EQ || nsk == GE || nsk == GT) { + is_conflict = true; + return true; + } + else { + return false; + } + } + else { // [(t0 <= 0 + .. + tn <= 0) + (c > 0) >/>= 0] -> t > -c + if (nsk == LE || nsk == LT) + return false; + if (sz > 1 && nsk == EQ) + nsk = GE; + return true; + } + } + else if (sta == LE) { + if (am.is_neg(c)) { // ( <= 0) + (c < 0) -> < 0 + if (nsk == EQ || nsk == GE || nsk == GT) { + is_conflict = true; + return true; + } + else { + return false; + } + } + else if (am.is_zero(c)) { // ( <= 0) + (c == 0) -> <= 0 + if (nsk == GT) { + is_conflict = true; + return true; + } + else { + return false; + } + } + else { // [(t0 <= 0 + .. + tn <= 0) + (c > 0) >/>= 0] -> t > -c + if (nsk == LE || nsk == LT) + return false; + if (sz > 1 && nsk == EQ) + nsk = GE; + return true; + } + } + else if (sta == GT) { + if (am.is_neg(c)) { // [(t0 > 0 + .. + tn > 0) + (c < 0) t < -c + if (nsk == GE || nsk == GT) + return false; + if (sz > 1 && nsk == EQ) + nsk = LE; + return true; + } + else if (am.is_zero(c)) { // ( > 0) + (c == 0) -> > 0 + if (nsk == EQ || nsk == LE || nsk == LT) { + is_conflict = true; + return true; + } + else { + return false; + } + } + else { // (t > 0) + (c > 0) -> > 0 + if (nsk == EQ || nsk == LE || nsk == LT) { + is_conflict = true; + return true; + } + else { + return false; + } + } + } + else if (sta == GE) { + if (am.is_neg(c)) { // [(t0 >= 0 + .. + tn >= 0) + (c < 0) t < -c + if (nsk == GE || nsk == GT) + return false; + if (sz > 1 && nsk == EQ) + nsk = LE; + return true; + } + else if (am.is_zero(c)) { // ( >= 0) + (c == 0) -> >= 0 + if (nsk == LT) { + is_conflict = true; + return true; + } + else { + return false; + } + } + else { // (t >= 0) + (c > 0) -> > 0 + if (nsk == EQ || nsk == LE || nsk == LT) { + is_conflict = true; + return true; + } + else { + return false; + } + } + } + return false; + } + bool collect_domain_sign_ineq_consistent_form(sign_kind nsk, vector &as, vector &xs, vector &bs, scoped_anum& c) { + for (unsigned i = 0, sz = as.size(); i < sz; ++i) { + if (!update_var_domain(nsk, as[i], xs[i], bs[i], c)) + return false; + } + return true; + } + bool process_axbsc_form(sign_kind nsk, unsigned cid, vector &as, vector &xs, vector &bs, scoped_anum& c) { + bool is_conflict(false); + TRACE("simple_checker", + for (unsigned i = 0, sz = as.size(); i < sz; ++i) { + if (i > 0) + tout << "+ "; + tout << as[i] << "x[" << xs[i] << "]^" << bs[i] << " "; + } + tout << "+ " << c << " "; + display(tout, nsk); + tout << " 0\n"; + ); + if (!check_is_sign_ineq_consistent(nsk, as, xs, bs, c, is_conflict)) + return true; + TRACE("simple_checker", + tout << "is conflict: " << is_conflict << "\n" + ); + if (is_conflict) + return false; + clauses_visited[cid].visited = true; + if (!collect_domain_sign_ineq_consistent_form(nsk, as, xs, bs, c)) + return false; + return true; + } + bool collect_domain_axbsc_form(unsigned cid, unsigned lid) { + // [a*(x^k)] + ... + [a*(x^b)] + k form + literal lit = (*clauses[cid])[lid]; + bool s = lit.sign(); + ineq_atom *iat = to_ineq_atom(atoms[lit.var()]); + if (iat->size() > 1) + return true; + if (literal_special_kind[cid][lid] != UNK && + literal_special_kind[cid][lid] != AXBSC) + return true; + + poly *p = iat->p(0); + vector as; + for (unsigned i = 0, sz = pm.size(p); i < sz; ++i) { + as.push_back(scoped_anum(am)); + } + vector xs; + vector bs; + scoped_anum c(am); + unsigned cnt; + if (!check_is_axbsc(p, as, xs, bs, c, cnt)) { + literal_special_kind[cid][lid] = NK; + return true; + } + literal_special_kind[cid][lid] = AXBSC; + TRACE("simple_checker", + tout << "as size: " << as.size() << '\n'; + ); + while (as.size() > cnt) + as.pop_back(); + + sign_kind nsk = to_sign_kind(iat->get_kind()); + if (s) { + if (nsk == EQ) + return true; + else if (nsk == LT) + nsk = GE; + else if (nsk == GT) + nsk = LE; + } + TRACE("simple_checker", + tout << "ineq atom: " << '\n'; + for (unsigned i = 0, sz = iat->size(); i < sz; ++i) { + pm.display(tout, iat->p(i)); + tout << " is even: " << iat->is_even(i) << "\n"; + } + display(tout, nsk); + tout << " 0\n"; + tout << "\n"; + tout << "as size: " << as.size() << '\n'; + for (unsigned i = 0, sz = as.size(); i < sz; ++i) { + if (i > 0) + tout << "+ "; + tout << as[i] << "x[" << xs[i] << "]^" << bs[i] << " "; + } + tout << "+ " << c << " "; + display(tout, nsk); + tout << " 0\n"; + ); + if (!process_axbsc_form(nsk, cid, as, xs, bs, c)) + return false; + return true; + } + + bool collect_var_domain() { + // vector vec_id; + for (unsigned i = 0, sz = clauses.size(); i < sz; ++i) { + if (clauses_visited[i].visited) + continue; + if (clauses[i]->size() > 1) + continue; + literal lit = (*clauses[i])[0]; + atom *tmp_atom = atoms[lit.var()]; + if (tmp_atom == nullptr) { + clauses_visited[i].visited = true; + continue; + } + if (!tmp_atom->is_ineq_atom()) { + clauses_visited[i].visited = true; + continue; + } + ineq_atom *tmp_ineq_atom = to_ineq_atom(tmp_atom); + if (tmp_ineq_atom->size() > 1) + continue; + if (!collect_domain_axbc_form(i, 0)) + return false; + } + TRACE("simple_checker", + for (unsigned i = 0; i < arith_var_num; ++i) { + tout << "====== arith[" << i << "] ======\n"; + tout << "original value: "; + display(tout, am, vars_domain[i].ori_val); + tout << "\nmagitude value: "; + display(tout, am, vars_domain[i].mag_val); + tout << "\n"; + tout << "====== arith[" << i << "] ======\n"; + } + ); + for (unsigned i = 0, sz = clauses.size(); i < sz; ++i) { + // unsigned id = vec_id[i]; + if (!collect_domain_axbsc_form(i, 0)) + return false; + } + return true; + } + void endpoint_multiply(const Endpoint &a, const Endpoint &b, Endpoint &c) { + if (a.is_zero() || b.is_zero()) { + c.set_num(0, 0); + return ; + } + bool a_neg = a.is_neg(), b_neg = b.is_neg(); + if (a.m_inf || b.m_inf) { + c.m_inf = 1; + c.m_open = 1; + if (a_neg == b_neg) + c.m_is_lower = 0; + else + c.m_is_lower = 1; + } + else { + c.m_inf = 0; + c.m_open = (a.m_open | b.m_open); + am.set(c.m_val, a.m_val*b.m_val); + } + } + void get_max_min_endpoint(const ptr_vector &pev, Endpoint *&pmi, Endpoint *&pmx) { + pmi = pmx = pev[0]; + for (unsigned i = 1, sz = pev.size(); i < sz; ++i) { + if (*pmx < *pev[i]) + pmx = pev[i]; + if (*pev[i] < *pmi) + pmi = pev[i]; + } + } + void merge_mul_domain(Domain_Interval &pre, const Domain_Interval &now) { + TRACE("simple_checker", + tout << "dom: "; + display(tout, am, pre); + tout << "\n"; + tout << "di: "; + display(tout, am, now); + tout << "\n"; + ); + Endpoint plnl(am), plnu(am), punl(am), punu(am); + endpoint_multiply(pre.m_lower, now.m_lower, plnl); + endpoint_multiply(pre.m_lower, now.m_upper, plnu); + endpoint_multiply(pre.m_upper, now.m_lower, punl); + endpoint_multiply(pre.m_upper, now.m_upper, punu); + ptr_vector pev; + pev.push_back(&plnl); + pev.push_back(&plnu); + pev.push_back(&punl); + pev.push_back(&punu); + Endpoint *pmi, *pmx; + get_max_min_endpoint(pev, pmi, pmx); + pre.m_lower.copy(*pmi); + pre.m_lower.m_is_lower = 1; + pre.m_upper.copy(*pmx); + pre.m_upper.m_is_lower = 0; + } + + void get_monomial_domain(monomial *m, const scoped_anum &a, Domain_Interval &dom) { + TRACE("simple_checker", + tout << "monomial: "; + pm.display(tout, m); + tout << '\n'; + tout << "coefficient: " << a << "\n"; + tout << "# "; + for (unsigned i = 0, sz = pm.size(m); i < sz; ++i) { + var v = pm.get_var(m, i); + tout << " (" << i << ", " << pm.degree_of(m, v) << ")"; + } + tout << "\n"; + ); + + // [a, a] + dom.set_num(a); + for (unsigned i = 0, sz = pm.size(m); i < sz; ++i) { + var v = pm.get_var(m, i); + unsigned deg = pm.degree_of(m, v); + const Domain_Interval &di = ((deg & 1) == 0 ? vars_domain[v].mag_val : vars_domain[v].ori_val); + TRACE("simple_checker", + tout << "dom: "; + display(tout, am, dom); + tout << "\n"; + tout << "var: " << v; + tout << ", di: "; + display(tout, am, di); + tout << "\n"; + ); + for (unsigned j = 0; j < deg; ++j) { + merge_mul_domain(dom, di); + } + TRACE("simple_checker", + tout << "after merge mul: "; + display(tout, am, dom); + tout << "\n"; + ); + // mul 0 + // if (dom.m_lower_inf && dom.m_upper_inf) + // return ; + } + } + void endpoint_add(Endpoint &a, const Endpoint &b) { + a.m_inf = (a.m_inf | b.m_inf); + if (a.m_inf == 0) { + am.set(a.m_val, a.m_val + b.m_val); + a.m_open = (a.m_open | b.m_open); + } + } + + void merge_add_domain(Domain_Interval &pre, const Domain_Interval &now) { + endpoint_add(pre.m_lower, now.m_lower); + endpoint_add(pre.m_upper, now.m_upper); + } + + sign_kind get_poly_sign(const poly *p) { + scoped_anum a(am); + am.set(a, pm.coeff(p, 0)); + Domain_Interval pre(am); + get_monomial_domain(pm.get_monomial(p, 0), a, pre); + TRACE("simple_checker", + tout << "poly: "; + pm.display(tout, p); + tout << "\n"; + ); + TRACE("simple_checker", + tout << "pre: "; + display(tout, am, pre); + tout << "\n"; + ); + for (unsigned i = 1, sz = pm.size(p); i < sz; ++i) { + am.set(a, pm.coeff(p, i)); + Domain_Interval now(am); + get_monomial_domain(pm.get_monomial(p, i), a, now); + TRACE("simple_checker", + tout << "pre: "; + display(tout, am, pre); + tout << "\n"; + tout << "now: "; + display(tout, am, now); + tout << "\n"; + ); + if (now.m_lower.m_inf && now.m_upper.m_inf) + return NONE; + merge_add_domain(pre, now); + TRACE("simple_checker", + tout << "after merge: "; + display(tout, am, pre); + tout << "\n"; + ); + if (pre.m_lower.m_inf && pre.m_upper.m_inf) + return NONE; + } + if (pre.m_lower.m_inf) { + if (am.is_neg(pre.m_upper.m_val)) { + // (-inf, -} + return LT; + } + else if (am.is_zero(pre.m_upper.m_val)) { + // (-inf, 0} + if (pre.m_upper.m_open) + return LT; + else + return LE; + } + else { + // (-inf, +} + return NONE; + } + } + else if (pre.m_upper.m_inf) { + if (am.is_neg(pre.m_lower.m_val)) { + // {-, +inf) + return NONE; + } + else if (am.is_zero(pre.m_lower.m_val)) { + // {0, +inf) + if (pre.m_lower.m_open) + return GT; + else + return GE; + } + else { + // {+, +inf) + return GT; + } + } + else { + // [0, 0] + if (am.is_zero(pre.m_lower.m_val) && am.is_zero(pre.m_upper.m_val)) + return EQ; + else if (am.is_zero(pre.m_lower.m_val)) { + // {0, +} + if (pre.m_lower.m_open) + return GT; + else + return GE; + } + else if (am.is_zero(pre.m_upper.m_val)) { + // {-, 0} + if (pre.m_upper.m_open) + return LT; + else + return LE; + } + else { + if (am.is_pos(pre.m_lower.m_val)) + return GT; + else if (am.is_neg(pre.m_upper.m_val)) + return LT; + else + return NONE; + } + } + return NONE; + } + + sign_kind get_poly_sign_degree(const poly *p, bool is_even) { + sign_kind ret = get_poly_sign(p); + if (is_even) { + if (ret == GE || ret == LE || ret == NONE) + ret = GE; + else if (ret != EQ) + ret = GT; + } + TRACE("simple_checker", + tout << "ret sign: "; + display(tout, ret); + tout << "\n"; + tout << "is even: " << is_even << "\n"; + ); + return ret; + } + void merge_mul_sign(sign_kind &pre, sign_kind now) { + if (pre == EQ) + return ; + if (now == EQ) { + pre = EQ; + return ; + } + if (pre == NONE) + return ; + + if (now == NONE) { + pre = NONE; + } + // else if (now == EQ) { + // pre = EQ; + // } + else if (now == LT) { + if (pre == GE) + pre = LE; + else if (pre == GT) + pre = LT; + else if (pre == LE) + pre = GE; + else if (pre == LT) + pre = GT; + } + else if (now == GT) { + // if (pre == LE) + // pre = LE; + // else if (pre == LT) + // pre = LT; + // else if (pre == GT) + // pre = GT; + // else if (pre == GE) + // pre = GE; + } + else if (now == LE) { + if (pre == GE) + pre = LE; + else if (pre == GT) + pre = LE; + else if (pre == LE) + pre = GE; + else if (pre == LT) + pre = GE; + } + else if (now == GE) { + // if (pre == LE) + // pre = LE; + if (pre == LT) + pre = LE; + else if (pre == GT) + pre = GE; + // else if (pre == GE) + // pre = GE; + } + } + bool check_ineq_atom_satisfiable(const ineq_atom *iat, bool s) { + TRACE("simple_checker", + tout << "s: " << s << "\n"; + tout << "kd: " << iat->get_kind() << "\n"; + ); + sign_kind nsk = to_sign_kind(iat->get_kind()); + if (s) { + if (nsk == EQ) + return true; + else if (nsk == GT) + nsk = LE; + else + nsk = GE; + } + TRACE("simple_checker", + tout << "ineq atom: " << '\n'; + for (unsigned i = 0, sz = iat->size(); i < sz; ++i) { + pm.display(tout, iat->p(i)); + tout << " is even: " << iat->is_even(i) << "\n"; + } + display(tout, nsk); + tout << " 0\n"; + ); + // return true; + + sign_kind pre = get_poly_sign_degree(iat->p(0), iat->is_even(0)); + + for (unsigned i = 1, sz = iat->size(); i < sz; ++i) { + sign_kind now = get_poly_sign_degree(iat->p(i), iat->is_even(i)); + merge_mul_sign(pre, now); + if (pre == NONE) + return true; + if ((nsk == EQ || nsk == GE || nsk == LE) && + (pre == EQ || pre == GE || pre == LE)) + return true; + } + TRACE("simple_checker", + tout << "pre: "; + display(tout, pre); + tout << ", nsk: "; + display(tout, nsk); + tout << "\n"; + ); + if (pre == NONE) + return true; + if (pre == EQ && (nsk == LT || nsk == GT)) + return false; + if (pre == GE && nsk == LT) + return false; + if (pre == GT && (nsk == LT || nsk == LE || nsk == EQ)) + return false; + if (pre == LE && nsk == GT) + return false; + if (pre == LT && (nsk == GT || nsk == GE || nsk == EQ)) + return false; + return true; + } + bool check_literal_satisfiable(unsigned cid, unsigned lit_id) { + literal lit = (*clauses[cid])[lit_id]; + const var &v = lit.var(); + atom *at = atoms[v]; + if (at == nullptr) { + clauses_visited[cid].visited = true; + return true; + } + if (!at->is_ineq_atom()) { + clauses_visited[cid].visited = true; + return true; + } + // TRACE("sign", + // tout << "literal: " << lit << '\n'; + // ); + bool s = lit.sign(); + return check_ineq_atom_satisfiable(to_ineq_atom(at), s); + } + bool check_clause_satisfiable(unsigned cid) { + const clause *cla = clauses[cid]; + TRACE("simple_checker", + tout << "clause size: " << cla->size() << '\n'; + ); + unsigned sz = cla->size(); + if (clauses_visited[cid].literal_visited.size() == 0) { + clauses_visited[cid].literal_visited.resize(sz, false); + literal_special_kind[cid].resize(sz, UNK); + } + unsigned sat_lit_id = sz; + for (unsigned i = 0; i < sz; ++i) { + if (clauses_visited[cid].literal_visited[i]) + continue; + if (check_literal_satisfiable(cid, i)) { + if (clauses_visited[cid].visited) + return true; + if (sat_lit_id == sz) + sat_lit_id = i; + else + return true; + } else { + clauses_visited[cid].literal_visited[i] = true; + literal lit = (*clauses[cid])[i]; + lit.neg(); + learned_unit.push_back(lit); + TRACE("simple_checker_learned", + tout << "making new clauses!\n"; + tout << "sign: " << lit.sign() << '\n'; + if (atoms[lit.var()] != nullptr && atoms[lit.var()]->is_ineq_atom()) { + ineq_atom *iat = to_ineq_atom(atoms[lit.var()]); + tout << "ineq atom: " << '\n'; + sign_kind nsk = to_sign_kind(iat->get_kind()); + for (unsigned i = 0, sz = iat->size(); i < sz; ++i) { + pm.display(tout, iat->p(i)); + tout << " is even: " << iat->is_even(i) << "\n"; + } + display(tout, nsk); + tout << " 0\n"; + } + ); + } + } + if (sat_lit_id != sz) { + if (!collect_domain_axbc_form(cid, sat_lit_id)) + return false; + if (!collect_domain_axbsc_form(cid, sat_lit_id)) + return false; + return true; + } + return false; + } + bool check() { + for (unsigned i = 0, sz = clauses.size(); i < sz; ++i) { + if (clauses_visited[i].visited) + continue; + if (!check_clause_satisfiable(i)) { + return false; + } + } + return true; + } + bool operator()() { + + improved = true; + while (improved) { + improved = false; + if (!check()) + return false; + TRACE("simple_checker", + for (unsigned i = 0; i < arith_var_num; ++i) { + tout << "====== arith[" << i << "] ======\n"; + tout << "original value: "; + display(tout, am, vars_domain[i].ori_val); + tout << "\nmagitude value: "; + display(tout, am, vars_domain[i].mag_val); + tout << "\n"; + tout << "====== arith[" << i << "] ======\n"; + } + ); + } + return true; + } + }; + Simple_Checker::Simple_Checker(pmanager &_pm, anum_manager &_am, const clause_vector &_clauses, literal_vector &_learned_unit, const atom_vector &_atoms, const unsigned &_arith_var_num) { + m_imp = alloc(imp, _pm, _am, _clauses, _learned_unit, _atoms, _arith_var_num); + } + Simple_Checker::~Simple_Checker() { + dealloc(m_imp); + } + bool Simple_Checker::operator()() { + return m_imp->operator()(); + } +} diff --git a/src/nlsat/nlsat_simple_checker.h b/src/nlsat/nlsat_simple_checker.h new file mode 100644 index 00000000000..1a854e85544 --- /dev/null +++ b/src/nlsat/nlsat_simple_checker.h @@ -0,0 +1,14 @@ +#include "math/polynomial/algebraic_numbers.h" +#include "nlsat/nlsat_clause.h" + + +namespace nlsat { + class Simple_Checker { + struct imp; + imp * m_imp; + public: + Simple_Checker(pmanager &_pm, anum_manager &_am, const clause_vector &_clauses, literal_vector &_learned_unit, const atom_vector &_atoms, const unsigned &_arith_var_num); + ~Simple_Checker(); + bool operator()(); + }; +} \ No newline at end of file diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index bb169a05e48..1c4aabe50ec 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -34,6 +34,8 @@ Revision History: #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" #define NLSAT_EXTRA_VERBOSE @@ -220,6 +222,10 @@ namespace nlsat { bool m_check_lemmas; unsigned m_max_conflicts; unsigned m_lemma_count; + bool m_simple_check; + unsigned m_variable_ordering_strategy; + bool m_set_0_more; + bool m_cell_sample; struct stats { unsigned m_simplifications; @@ -253,7 +259,7 @@ namespace nlsat { 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), + 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), @@ -289,6 +295,12 @@ namespace nlsat { m_inline_vars = p.inline_vars(); m_log_lemmas = p.log_lemmas(); m_check_lemmas = p.check_lemmas(); + m_variable_ordering_strategy = p.variable_ordering_strategy(); + + + 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); @@ -1518,7 +1530,7 @@ namespace nlsat { void select_witness() { scoped_anum w(m_am); SASSERT(!m_ism.is_full(m_infeasible[m_xk])); - m_ism.peek_in_complement(m_infeasible[m_xk], is_int(m_xk), w, m_randomize); + 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";); @@ -1767,6 +1779,35 @@ namespace nlsat { } bool m_reordered = false; + 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()); + 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)); + } + } + return true; + } + + + void run_variable_ordering_strategy() { + TRACE("reorder", tout << "runing vos: " << m_variable_ordering_strategy << '\n';); + + unsigned num = num_vars(); + VOS_Var_Info_Collector vos_collector(m_pm, m_atoms, num, m_variable_ordering_strategy); + vos_collector.collect(m_clauses); + vos_collector.collect(m_learned); + + var_vector perm; + vos_collector(perm); + reorder(perm.size(), perm.data()); + } void apply_reorder() { m_reordered = false; @@ -1783,25 +1824,45 @@ namespace nlsat { } lbool check() { + + if (m_simple_check) { + if (!simple_check()) { + TRACE("simple_check", tout << "real unsat\n";); + return l_false; + } + TRACE("simple_checker_learned", + tout << "simple check done\n"; + ); + } + TRACE("nlsat_smt2", display_smt2(tout);); TRACE("nlsat_fd", tout << "is_full_dimensional: " << is_full_dimensional() << "\n";); init_search(); m_explain.set_full_dimensional(is_full_dimensional()); + bool reordered = false; - apply_reorder(); + + if (!can_reorder()) { -#if 0 - if (!m_incremental && m_inline_vars) { - if (!m_simplify()) - return l_false; } -#endif - IF_VERBOSE(3, verbose_stream() << "search\n"); + else if (m_variable_ordering_strategy > 0) { + run_variable_ordering_strategy(); + reordered = true; + } + 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 (m_reordered) - restore_order(); + 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)); @@ -2772,11 +2833,59 @@ namespace nlsat { TRACE("nlsat_reorder_clauses", tout << "after:\n"; for (unsigned i = 0; i < sz; i++) { display(tout, *(cs[i])); tout << "\n"; }); } + + 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"; }); + } + void sort_watched_clauses() { unsigned num = num_vars(); for (unsigned i = 0; i < num; i++) { clause_vector & ws = m_watches[i]; - sort_clauses_by_degree(ws.size(), ws.data()); + // sort_clauses_by_degree(ws.size(), ws.data()); + if (m_simple_check) { + sort_clauses_by_degree_lit_num(ws.size(), ws.data()); + } + else { + sort_clauses_by_degree(ws.size(), ws.data()); + } } } diff --git a/src/nlsat/nlsat_variable_ordering_strategy.cpp b/src/nlsat/nlsat_variable_ordering_strategy.cpp new file mode 100644 index 00000000000..dfcc1420117 --- /dev/null +++ b/src/nlsat/nlsat_variable_ordering_strategy.cpp @@ -0,0 +1,282 @@ +#include "nlsat/nlsat_variable_ordering_strategy.h" + +namespace nlsat { + struct VOS_Var_Info_Collector::imp { + pmanager & pm; + atom_vector const & m_atoms; + unsigned num_vars; + Variable_Ordering_Strategy_Type m_vos_type; + + /** Maximum degree of this variable. */ + unsigned_vector m_max_degree; + /** Sum of degrees of this variable within all polynomials. */ + unsigned_vector m_sum_poly_degree; + /** Number of polynomials that contain this variable. */ + unsigned_vector m_num_polynomials; + + /** Maximum degree of the leading coefficient of this variable. */ + unsigned_vector m_max_lc_degree; + /** Maximum of total degrees of terms that contain this variable. */ + unsigned_vector m_max_terms_tdegree; + /** Sum of degrees of this variable within all terms. */ + unsigned_vector m_sum_term_degree; + /** Number of terms that contain this variable. */ + unsigned_vector m_num_terms; + + + unsigned_vector m_num_uni; + numeral_vector m_coeffs; + + + imp(pmanager & _pm, atom_vector const & atoms, unsigned _num_vars, unsigned _vos_type): + pm(_pm), + m_atoms(atoms), + num_vars(_num_vars), + m_vos_type(Variable_Ordering_Strategy_Type(_vos_type)) { + + m_max_degree.resize(num_vars, 0); + m_sum_poly_degree.resize(num_vars, 0); + m_num_polynomials.resize(num_vars, 0); + + if (m_vos_type != ONLYPOLY) { + m_max_lc_degree.resize(num_vars, 0); + m_max_terms_tdegree.resize(num_vars, 0); + m_sum_term_degree.resize(num_vars, 0); + m_num_terms.resize(num_vars, 0); + + + m_num_uni.resize(num_vars, 0); + m_coeffs.resize(num_vars, 0); + + } + } + + void collect(monomial * m) { + unsigned mdeg = 0; + for (unsigned i = 0, sz = pm.size(m); i < sz; ++i) { + var x = pm.get_var(m, i); + mdeg += pm.degree_of(m, x); + ++m_num_terms[x]; + } + + for (unsigned i = 0, sz = pm.size(m); i < sz; ++i) { + var x = pm.get_var(m, i); + m_sum_term_degree[x] += mdeg; + if (mdeg > m_max_terms_tdegree[x]) + m_max_terms_tdegree[x] = mdeg; + unsigned lc_deg = mdeg - pm.degree_of(m, x); + if (lc_deg > m_max_lc_degree[x]) + m_max_lc_degree[x] = lc_deg; + } + } + + void collect(poly * p) { + var_vector vec_vars; + pm.vars(p, vec_vars); + + if (m_vos_type == UNIVARIATE) { + if (vec_vars.size() == 1) + ++m_num_uni[vec_vars[0]]; + } + + for (unsigned i = 0, sz = vec_vars.size(); i < sz; ++i) { + var x = vec_vars[i]; + unsigned k = pm.degree(p, x); + ++m_num_polynomials[x]; + m_sum_poly_degree[x] += k; + if (k > m_max_degree[x]) + m_max_degree[x] = k; + + if (m_vos_type == FEATURE){ + for (unsigned kl = 0; kl <= k; kl++) { + scoped_numeral curr(pm.m()); + if (pm.const_coeff(p, x, kl, curr)) { + pm.m().abs(curr); + if (pm.m().gt(curr, m_coeffs[x])) { + pm.m().set(m_coeffs[x], curr); + } + } + } + } + + } + + if (m_vos_type != ONLYPOLY && m_vos_type != UNIVARIATE){ + for (unsigned i = 0, sz = pm.size(p); i < sz; ++i) { + collect(pm.get_monomial(p, i)); + } + } + } + + 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])); + } + + + struct univariate_reorder_lt { + VOS_Var_Info_Collector::imp const *m_info; + univariate_reorder_lt(VOS_Var_Info_Collector::imp const *info):m_info(info) {} + bool operator()(var x, var y) const { + if (m_info->m_num_uni[x] != m_info->m_num_uni[y]) + return m_info->m_num_uni[x] > m_info->m_num_uni[y]; + return x < y; + } + }; + + struct feature_reorder_lt { + VOS_Var_Info_Collector::imp const *m_info; + feature_reorder_lt(VOS_Var_Info_Collector::imp const * info): m_info(info){} + bool operator()(var x, var y) const { + if (m_info->m_max_degree[x] != m_info->m_max_degree[y]) + return m_info->m_max_degree[x] > m_info->m_max_degree[y]; + if (m_info->m_max_terms_tdegree[x] != m_info->m_max_terms_tdegree[y]) + return m_info->m_max_terms_tdegree[x] > m_info->m_max_terms_tdegree[y]; + if (!m_info->pm.m().eq(m_info->m_coeffs[x], m_info->m_coeffs[y])) { + return m_info->pm.m().lt(m_info->m_coeffs[x], m_info->m_coeffs[y]); + } + return x < y; + } + }; + struct brown_reorder_lt { + VOS_Var_Info_Collector::imp const *m_info; + brown_reorder_lt(VOS_Var_Info_Collector::imp const *info):m_info(info) {} + bool operator()(var x, var y) const { + // if (a.max_degree != b.max_degree) + // return a.max_degree > b.max_degree; + // if (a.max_terms_tdegree != b.max_terms_tdegree) + // return a.max_terms_tdegree > b.max_terms_tdegree; + // return a.num_terms > b.num_terms; + if (m_info->m_max_degree[x] != m_info->m_max_degree[y]) + return m_info->m_max_degree[x] > m_info->m_max_degree[y]; + if (m_info->m_max_terms_tdegree[x] != m_info->m_max_terms_tdegree[y]) + return m_info->m_max_terms_tdegree[x] > m_info->m_max_terms_tdegree[y]; + if (m_info->m_num_terms[x] != m_info->m_num_terms[y]) + return m_info->m_num_terms[x] > m_info->m_num_terms[y]; + return x < y; + } + }; + struct triangular_reorder_lt { + const VOS_Var_Info_Collector::imp *m_info; + triangular_reorder_lt(VOS_Var_Info_Collector::imp const *info):m_info(info) {} + bool operator()(var x, var y) const { + // if (a.max_degree != b.max_degree) + // return a.max_degree > b.max_degree; + // if (a.max_lc_degree != b.max_lc_degree) + // return a.max_lc_degree > b.max_lc_degree; + // return a.sum_poly_degree > b.sum_poly_degree; + if (m_info->m_max_degree[x] != m_info->m_max_degree[y]) + return m_info->m_max_degree[x] > m_info->m_max_degree[y]; + if (m_info->m_max_lc_degree[x] != m_info->m_max_lc_degree[y]) + return m_info->m_max_lc_degree[x] > m_info->m_max_lc_degree[y]; + if (m_info->m_sum_poly_degree[x] != m_info->m_sum_poly_degree[y]) + return m_info->m_sum_poly_degree[x] > m_info->m_sum_poly_degree[y]; + return x < y; + } + }; + struct onlypoly_reorder_lt { + const VOS_Var_Info_Collector::imp *m_info; + onlypoly_reorder_lt(VOS_Var_Info_Collector::imp 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 m_info->m_max_degree[x] > m_info->m_max_degree[y]; + // + if (m_info->m_sum_poly_degree[x] != m_info->m_sum_poly_degree[y]) + return m_info->m_sum_poly_degree[x] > m_info->m_sum_poly_degree[y]; + // more constrained first + if (m_info->m_num_polynomials[x] != m_info->m_num_polynomials[y]) + return m_info->m_num_polynomials[x] > m_info->m_num_polynomials[y]; + return x < y; + } + }; + bool check_invariant() const {return true;} // what is the invariant + void operator()(var_vector &perm) { + var_vector new_order; + for (var x = 0; x < num_vars; x++) { + new_order.push_back(x); + } + if (m_vos_type == BROWN) { + std::sort(new_order.begin(), new_order.end(), brown_reorder_lt(this)); + } + else if (m_vos_type == TRIANGULAR) { + std::sort(new_order.begin(), new_order.end(), triangular_reorder_lt(this)); + } + else if (m_vos_type == ONLYPOLY) { + std::sort(new_order.begin(), new_order.end(), onlypoly_reorder_lt(this)); + } + + else if(m_vos_type == UNIVARIATE){ + std::sort(new_order.begin(), new_order.end(), univariate_reorder_lt(this)); + } + else if(m_vos_type == FEATURE){ + std::sort(new_order.begin(), new_order.end(), feature_reorder_lt(this)); + } + + else { + UNREACHABLE(); + } + TRACE("reorder", + tout << "new order: "; + for (unsigned i = 0; i < num_vars; i++) + tout << new_order[i] << " "; + tout << "\n"; + ); + perm.resize(num_vars, 0); + for (var x = 0; x < num_vars; x++) { + perm[new_order[x]] = x; + } + + SASSERT(check_invariant()); + } + // 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; + // } + + // std::ostream& display(std::ostream & out, display_var_proc const & proc) { + // for (unsigned i = 0; i < num_vars; ++i) { + // proc(out, i); out << " -> " << m_max_degree[i] << " : " << m_sum_poly_degree[i] << "\n"; + // } + // return out; + // } + }; + VOS_Var_Info_Collector::VOS_Var_Info_Collector(pmanager & _pm, atom_vector const & _atoms, unsigned _num_vars, unsigned _vos_type) { + m_imp = alloc(imp, _pm, _atoms, _num_vars, _vos_type); + } + VOS_Var_Info_Collector::~VOS_Var_Info_Collector() { + dealloc(m_imp); + } + void VOS_Var_Info_Collector::collect(clause_vector const & cs) { + m_imp->collect(cs); + } + void VOS_Var_Info_Collector::operator()(var_vector &perm) { + m_imp->operator()(perm); + } +} diff --git a/src/nlsat/nlsat_variable_ordering_strategy.h b/src/nlsat/nlsat_variable_ordering_strategy.h new file mode 100644 index 00000000000..6e01825c391 --- /dev/null +++ b/src/nlsat/nlsat_variable_ordering_strategy.h @@ -0,0 +1,27 @@ +#include "nlsat/nlsat_clause.h" + + +#include "math/polynomial/algebraic_numbers.h" +#include "math/polynomial/polynomial.h" + + +namespace nlsat { + + typedef polynomial::manager::scoped_numeral scoped_numeral; + typedef polynomial::manager::numeral_vector numeral_vector; + + + // enum Variable_Ordering_Strategy_Type {NONE = 0, BROWN, TRIANGULAR, ONLYPOLY}; + + enum Variable_Ordering_Strategy_Type {NONE = 0, BROWN, TRIANGULAR, ONLYPOLY, UNIVARIATE, FEATURE, ROOT}; + + class VOS_Var_Info_Collector { + struct imp; + imp * m_imp; + public: + VOS_Var_Info_Collector(pmanager & _pm, atom_vector const & atoms, unsigned _num_vars, unsigned _vos_type); + ~VOS_Var_Info_Collector(); + void operator()(var_vector &perm); + void collect(clause_vector const & cs); + }; +} \ No newline at end of file diff --git a/src/tactic/smtlogics/qfnra_tactic.cpp b/src/tactic/smtlogics/qfnra_tactic.cpp index b9fec436600..f95ae8a8c05 100644 --- a/src/tactic/smtlogics/qfnra_tactic.cpp +++ b/src/tactic/smtlogics/qfnra_tactic.cpp @@ -23,6 +23,8 @@ Module Name: #include "nlsat/tactic/qfnra_nlsat_tactic.h" #include "tactic/smtlogics/smt_tactic.h" +#include "tactic/smtlogics/qflra_tactic.h" + static tactic * mk_qfnra_sat_solver(ast_manager& m, params_ref const& p, unsigned bv_size) { params_ref nra2sat_p = p; nra2sat_p.set_uint("nla2bv_max_bv_size", p.get_uint("nla2bv_max_bv_size", bv_size)); @@ -32,24 +34,299 @@ static tactic * mk_qfnra_sat_solver(ast_manager& m, params_ref const& p, unsigne mk_fail_if_undecided_tactic()); } +tactic * mk_multilinear_ls_tactic(ast_manager & m, params_ref const & p, unsigned ls_time = 60) { + params_ref p_mls = p; + p_mls.set_bool("use_ls", true); + p_mls.set_uint("ls_time",ls_time); + return using_params(mk_smt_tactic(m), p_mls); +} + +tactic * mk_qfnra_very_small_solver(ast_manager& m, params_ref const& p) { + ptr_vector ts; + { + params_ref p_sc = p; + p_sc.set_bool("simple_check", true); + // p_sc.set_uint("seed", 997); + ts.push_back(try_for(and_then(mk_qfnra_nlsat_tactic(m, p_sc), mk_fail_if_undecided_tactic()), 10 * 1000)); + } + { + params_ref p_heuristic = p; + // p_heuristic.set_uint("seed", 233); + ts.push_back(try_for(mk_qfnra_nlsat_tactic(m, p_heuristic), 4 * 1000)); + + params_ref p_order_4 = p; + p_order_4.set_uint("variable_ordering_strategy", 4); + ts.push_back(try_for(mk_qfnra_nlsat_tactic(m, p_order_4), 4 * 1000)); + + params_ref p_order_3 = p; + p_order_3.set_uint("variable_ordering_strategy", 3); + // p_order_3.set_uint("seed", 17); + ts.push_back(try_for(mk_qfnra_nlsat_tactic(m, p_order_3), 6 * 1000)); + + params_ref p_order_1 = p; + p_order_1.set_uint("variable_ordering_strategy", 1); + ts.push_back(try_for(mk_qfnra_nlsat_tactic(m, p_order_1), 8 * 1000)); + + params_ref p_order_5 = p; + p_order_5.set_uint("variable_ordering_strategy", 5); + ts.push_back(try_for(mk_qfnra_nlsat_tactic(m, p_order_5), 8 * 1000)); + + params_ref p_order_2 = p; + p_order_2.set_uint("variable_ordering_strategy", 2); + ts.push_back(try_for(mk_qfnra_nlsat_tactic(m, p_order_2), 10 * 1000)); + } + { + ts.push_back(mk_multilinear_ls_tactic(m, p, 60)); + } + { + params_ref p_l = p; + p_l.set_bool("arith.greatest_error_pivot", true); + ts.push_back(and_then(try_for(using_params(mk_smt_tactic(m), p_l), 300 * 1000), mk_fail_if_undecided_tactic())); + } + for (unsigned i = 0; i < 200; ++i) { // 3s * 200 = 600s + params_ref p_i = p; + p_i.set_uint("seed", i); + p_i.set_bool("shuffle_vars", true); + // if ((i & 1) == 0) + // p_i.set_bool("randomize", false); + ts.push_back(try_for(mk_qfnra_nlsat_tactic(m, p_i), 3 * 1000)); + } + { + ts.push_back(mk_qfnra_nlsat_tactic(m, p)); + } + return or_else(ts.size(), ts.data()); +} + +tactic * mk_qfnra_small_solver(ast_manager& m, params_ref const& p) { + ptr_vector ts; + { + params_ref p_sc = p; + p_sc.set_bool("simple_check", true); + // p_sc.set_uint("seed", 997); + ts.push_back(try_for(and_then(mk_qfnra_nlsat_tactic(m, p_sc), mk_fail_if_undecided_tactic()), 20 * 1000)); + } + { + params_ref p_heuristic = p; + // p_heuristic.set_uint("seed", 233); + ts.push_back(try_for(mk_qfnra_nlsat_tactic(m, p_heuristic), 5 * 1000)); + + params_ref p_order_4 = p; + p_order_4.set_uint("variable_ordering_strategy", 4); + ts.push_back(try_for(mk_qfnra_nlsat_tactic(m, p_order_4), 5 * 1000)); + + params_ref p_order_3 = p; + p_order_3.set_uint("variable_ordering_strategy", 3); + // p_order_3.set_uint("seed", 17); + ts.push_back(try_for(mk_qfnra_nlsat_tactic(m, p_order_3), 10 * 1000)); + + params_ref p_order_1 = p; + p_order_1.set_uint("variable_ordering_strategy", 1); + ts.push_back(try_for(mk_qfnra_nlsat_tactic(m, p_order_1), 15 * 1000)); + + + params_ref p_order_5 = p; + p_order_5.set_uint("variable_ordering_strategy", 5); + ts.push_back(try_for(mk_qfnra_nlsat_tactic(m, p_order_5), 15 * 1000)); + + + params_ref p_order_2 = p; + p_order_2.set_uint("variable_ordering_strategy", 2); + ts.push_back(try_for(mk_qfnra_nlsat_tactic(m, p_order_2), 20 * 1000)); + } + { + ts.push_back(mk_multilinear_ls_tactic(m, p, 70)); + } + { + params_ref p_l = p; + p_l.set_bool("arith.greatest_error_pivot", true); + ts.push_back(and_then(try_for(using_params(mk_smt_tactic(m), p_l), 350 * 1000), mk_fail_if_undecided_tactic())); + } + for (unsigned i = 0; i < 100; ++i) { // 5s * 100 = 500s + params_ref p_i = p; + p_i.set_uint("seed", i); + p_i.set_bool("shuffle_vars", true); + // if ((i & 1) == 0) + // p_i.set_bool("randomize", false); + ts.push_back(try_for(mk_qfnra_nlsat_tactic(m, p_i), 5 * 1000)); + } + { + ts.push_back(mk_qfnra_nlsat_tactic(m, p)); + } + return or_else(ts.size(), ts.data()); +} + +tactic * mk_qfnra_middle_solver(ast_manager& m, params_ref const& p) { + ptr_vector ts; + { + params_ref p_sc = p; + p_sc.set_bool("simple_check", true); + ts.push_back(try_for(and_then(mk_qfnra_nlsat_tactic(m, p_sc), mk_fail_if_undecided_tactic()), 30 * 1000)); + } + { + params_ref p_heuristic = p; + // p_heuristic.set_uint("seed", 233); + ts.push_back(try_for(mk_qfnra_nlsat_tactic(m, p_heuristic), 10 * 1000)); + + + params_ref p_order_4 = p; + p_order_4.set_uint("variable_ordering_strategy", 4); + ts.push_back(try_for(mk_qfnra_nlsat_tactic(m, p_order_4), 15 * 1000)); + + + params_ref p_order_3 = p; + p_order_3.set_uint("variable_ordering_strategy", 3); + ts.push_back(try_for(mk_qfnra_nlsat_tactic(m, p_order_3), 15 * 1000)); + + params_ref p_order_1 = p; + p_order_1.set_uint("variable_ordering_strategy", 1); + ts.push_back(try_for(mk_qfnra_nlsat_tactic(m, p_order_1), 20 * 1000)); + + + params_ref p_order_5 = p; + p_order_5.set_uint("variable_ordering_strategy", 5); + ts.push_back(try_for(mk_qfnra_nlsat_tactic(m, p_order_5), 20 * 1000)); + + + params_ref p_order_2 = p; + p_order_2.set_uint("variable_ordering_strategy", 2); + ts.push_back(try_for(mk_qfnra_nlsat_tactic(m, p_order_2), 25 * 1000)); + } + { + ts.push_back(mk_multilinear_ls_tactic(m, p, 80)); + } + { + params_ref p_l = p; + p_l.set_bool("arith.greatest_error_pivot", true); + ts.push_back(and_then(try_for(using_params(mk_smt_tactic(m), p_l), 375 * 1000), mk_fail_if_undecided_tactic())); + } + for (unsigned i = 0; i < 40; ++i) { // 10s * 40 = 400s + params_ref p_i = p; + p_i.set_uint("seed", i); + p_i.set_bool("shuffle_vars", true); + // if ((i & 1) == 0) + // p_i.set_bool("randomize", false); + ts.push_back(try_for(mk_qfnra_nlsat_tactic(m, p_i), 10 * 1000)); + } + { + ts.push_back(mk_qfnra_nlsat_tactic(m, p)); + } + return or_else(ts.size(), ts.data()); +} + +tactic * mk_qfnra_large_solver(ast_manager& m, params_ref const& p) { + ptr_vector ts; + { + params_ref p_sc = p; + p_sc.set_bool("simple_check", true); + ts.push_back(try_for(and_then(mk_qfnra_nlsat_tactic(m, p_sc), mk_fail_if_undecided_tactic()), 50 * 1000)); + } + { + + params_ref p_order_4 = p; + p_order_4.set_uint("variable_ordering_strategy", 4); + ts.push_back(try_for(mk_qfnra_nlsat_tactic(m, p_order_4), 15 * 1000)); + + + params_ref p_order_3 = p; + p_order_3.set_uint("variable_ordering_strategy", 3); + ts.push_back(try_for(mk_qfnra_nlsat_tactic(m, p_order_3), 30 * 1000)); + + params_ref p_order_1 = p; + p_order_1.set_uint("variable_ordering_strategy", 1); + ts.push_back(try_for(mk_qfnra_nlsat_tactic(m, p_order_1), 40 * 1000)); + + + params_ref p_order_5 = p; + p_order_5.set_uint("variable_ordering_strategy", 5); + ts.push_back(try_for(mk_qfnra_nlsat_tactic(m, p_order_5), 40 * 1000)); + + + params_ref p_order_2 = p; + p_order_2.set_uint("variable_ordering_strategy", 2); + ts.push_back(try_for(mk_qfnra_nlsat_tactic(m, p_order_2), 50 * 1000)); + } + { + ts.push_back(mk_multilinear_ls_tactic(m, p, 90)); + } + { + params_ref p_l = p; + p_l.set_bool("arith.greatest_error_pivot", true); + ts.push_back(and_then(try_for(using_params(mk_smt_tactic(m), p_l), 400 * 1000), mk_fail_if_undecided_tactic())); + } + for (unsigned i = 0; i < 10; ++i) { // 20s * 10 = 200s + params_ref p_i = p; + p_i.set_uint("seed", i); + p_i.set_bool("shuffle_vars", true); + // if ((i & 1) == 0) + // p_i.set_bool("randomize", false); + ts.push_back(try_for(mk_qfnra_nlsat_tactic(m, p_i), 20 * 1000)); + } + { + ts.push_back(mk_qfnra_nlsat_tactic(m, p)); + } + return or_else(ts.size(), ts.data()); +} + +tactic * mk_qfnra_very_large_solver(ast_manager& m, params_ref const& p) { + ptr_vector ts; + { + params_ref p_sc = p; + p_sc.set_bool("simple_check", true); + ts.push_back(try_for(and_then(mk_qfnra_nlsat_tactic(m, p_sc), mk_fail_if_undecided_tactic()), 100 * 1000)); + } + { + params_ref p_order_1 = p; + p_order_1.set_uint("variable_ordering_strategy", 1); + ts.push_back(try_for(mk_qfnra_nlsat_tactic(m, p_order_1), 80 * 1000)); + + + params_ref p_order_5 = p; + p_order_5.set_uint("variable_ordering_strategy", 5); + ts.push_back(try_for(mk_qfnra_nlsat_tactic(m, p_order_5), 80 * 1000)); + + + params_ref p_order_2 = p; + p_order_2.set_uint("variable_ordering_strategy", 2); + ts.push_back(try_for(mk_qfnra_nlsat_tactic(m, p_order_2), 100 * 1000)); + } + { + ts.push_back(mk_multilinear_ls_tactic(m, p, 100)); + } + { + params_ref p_l = p; + p_l.set_bool("arith.greatest_error_pivot", true); + ts.push_back(and_then(try_for(using_params(mk_smt_tactic(m), p_l), 425 * 1000), mk_fail_if_undecided_tactic())); + } + { + ts.push_back(mk_qfnra_nlsat_tactic(m, p)); + } + return or_else(ts.size(), ts.data()); +} + +const double VERY_SMALL_THRESHOLD = 30.0; +const double SMALL_THRESHOLD = 80.0; +const double MIDDLE_THRESHOLD = 300.0; +const double LARGE_THRESHOLD = 600.0; +tactic * mk_qfnra_mixed_solver(ast_manager& m, params_ref const& p) { + return cond(mk_lt(mk_memory_probe(), mk_const_probe(VERY_SMALL_THRESHOLD)), + mk_qfnra_very_small_solver(m, p), + cond(mk_lt(mk_memory_probe(), mk_const_probe(SMALL_THRESHOLD)), + mk_qfnra_small_solver(m, p), + cond(mk_lt(mk_memory_probe(), mk_const_probe(MIDDLE_THRESHOLD)), + mk_qfnra_middle_solver(m, p), + cond(mk_lt(mk_memory_probe(), mk_const_probe(LARGE_THRESHOLD)), + mk_qfnra_large_solver(m, p), + mk_qfnra_very_large_solver(m, p) + ) + ) + ) + ); +} + tactic * mk_qfnra_tactic(ast_manager & m, params_ref const& p) { - params_ref p0 = p; - p0.set_bool("inline_vars", true); - params_ref p1 = p; - p1.set_uint("seed", 11); - p1.set_bool("factor", false); - params_ref p2 = p; - p2.set_uint("seed", 13); - p2.set_bool("factor", false); return and_then(mk_simplify_tactic(m, p), mk_propagate_values_tactic(m, p), - or_else(try_for(mk_qfnra_nlsat_tactic(m, p0), 5000), - try_for(mk_qfnra_nlsat_tactic(m, p1), 10000), - mk_qfnra_sat_solver(m, p, 4), - and_then(try_for(mk_smt_tactic(m), 5000), mk_fail_if_undecided_tactic()), - mk_qfnra_sat_solver(m, p, 6), - mk_qfnra_nlsat_tactic(m, p2))); + mk_qfnra_mixed_solver(m, p) + ); } - -