diff --git a/src/nlsat/nlsat_params.pyg b/src/nlsat/nlsat_params.pyg index 00d1799013..01229a527b 100644 --- a/src/nlsat/nlsat_params.pyg +++ b/src/nlsat/nlsat_params.pyg @@ -3,8 +3,8 @@ def_module_params('nlsat', description='nonlinear solver', export=True, params=(max_memory_param(), - ('linxi_simple_check', BOOL, False, "linxi precheck about variables sign"), - ('linxi_variable_ordering_strategy', UINT, 0, "linxi Variable Ordering Strategy, 0 for none, 1 for BROWN, 2 for TRIANGULAR, 3 for ONLYPOLY"), + ('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."), @@ -19,4 +19,3 @@ def_module_params('nlsat', ('seed', UINT, 0, "random seed."), ('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 index f4bb5e6482..3e1e8dd1c3 100644 --- a/src/nlsat/nlsat_simple_checker.cpp +++ b/src/nlsat/nlsat_simple_checker.cpp @@ -4,33 +4,19 @@ struct Debug_Tracer { std::string tag_str; Debug_Tracer(std::string _tag_str) { tag_str = _tag_str; - TRACE("linxi_simple_checker", + TRACE("simple_checker", tout << "Debug_Tracer begin\n"; tout << tag_str << "\n"; ); } ~Debug_Tracer() { - TRACE("linxi_simple_checker", + TRACE("simple_checker", tout << "Debug_Tracer end\n"; tout << tag_str << "\n"; ); } }; -// #define _LINXI_DEBUG - -#ifdef _LINXI_DEBUG -// #define LINXI_DEBUG std::stringstream DEBUG_ss; DEBUG_ss << __FUNCTION__ << " " << __FILE__ << ":" << __LINE__; Debug_Tracer DEBUG_dt(DEBUG_ss.str()); -// #define LINXI_HERE TRACE("linxi_simple_checker", tout << "here\n";); -#define LINXI_DEBUG { }((void) 0 ); -#define LINXI_HERE { }((void) 0 ); - -#else -#define LINXI_DEBUG { }((void) 0 ); -#define LINXI_HERE { }((void) 0 ); -#endif - - namespace nlsat { struct Simple_Checker::imp { @@ -277,7 +263,6 @@ namespace nlsat { bool improved; enum special_ineq_kind {UNK = 0, AXBC, AXBSC, NK}; // None Kind vector> literal_special_kind; - // imp(solver &_sol, pmanager &_pm, anum_manager &_am, const clause_vector &_clauses, clause_vector &_learned, const atom_vector &_atoms, const unsigned &_arith_var_num) : 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), @@ -304,7 +289,7 @@ namespace nlsat { return EQ; } bool update_interval_intersection(Domain_Interval &ia, const Domain_Interval &ib) { - TRACE("linxi_simple_checker", + TRACE("simple_checker", tout << "ia: "; display(tout, am, ia); tout << "\nib: "; @@ -326,70 +311,8 @@ namespace nlsat { return false; - // if (ia.m_lower_inf == 0 && ib.m_upper_inf == 0) { - // if (ia.m_lower > ib.m_upper) - // return false; - // if (ia.m_lower == ib.m_upper && (ia.m_lower_open || ib.m_upper_open)) - // return false; - // } - // if (ib.m_lower_inf == 0 && ia.m_upper_inf == 0) { - // if (ib.m_lower > ia.m_upper) - // return false; - // if (ib.m_lower == ia.m_upper && (ib.m_lower_open || ia.m_upper_open)) - // return false; - // } - // if (ia.m_lower_inf && ib.m_lower_inf) { - // // do nothing - // } - // else { - // if (ia.m_lower_inf) { - // ia.m_lower_inf = 0; - // ia.m_lower_open = ib.m_lower_open; - // am.set(ia.m_lower, ib.m_lower); - // } - // else if (ib.m_lower_inf) { - // // do nothing - // } - // else { - // if (ia.m_lower == ib.m_lower) { - // ia.m_lower_open = (ia.m_lower_open | ib.m_lower_open); - // } - // else if (ia.m_lower < ib.m_lower) { - // ia.m_lower_open = ib.m_lower_open; - // am.set(ia.m_lower, ib.m_lower); - // } - // else { - // // do nothing - // } - // } - // } - // if (ia.m_upper_inf && ib.m_upper_inf) { - // // do nothing - // } - // else { - // if (ia.m_upper_inf) { - // ia.m_upper_inf = 0; - // ia.m_upper_open = ib.m_upper_open; - // am.set(ia.m_upper, ib.m_upper); - // } - // else if (ib.m_upper_inf) { - // // do nothing - // } - // else { - // if (ia.m_upper == ib.m_upper) { - // ia.m_upper_open = (ia.m_upper_open | ib.m_upper_open); - // } - // else if (ia.m_upper < ib.m_upper) { - // // do nothing - // } - // else { - // ia.m_upper_open = ib.m_upper_open; - // am.set(ia.m_upper, ib.m_upper); - // } - // } - // } - TRACE("linxi_simple_checker", + TRACE("simple_checker", tout << "after update: "; display(tout, am, ia); tout << "\n"; @@ -401,7 +324,7 @@ namespace nlsat { return update_interval_intersection(vd.ori_val, di); } bool update_var_mag_domain_interval_by_ori(Var_Domain &vd, const Domain_Interval &di) { - TRACE("linxi_simple_checker", + TRACE("simple_checker", tout << "vd mag val: "; display(tout, am, vd.mag_val); tout << "\n"; @@ -410,8 +333,7 @@ namespace nlsat { tout << "\n"; ); Domain_Interval mag_di(am, 0, 0, 1, 1); - // am.set(mag_di.m_lower.m_val, 0); - + if (di.m_lower.m_inf) { mag_di.m_upper.m_inf = 1; mag_di.m_upper.m_open = 1; @@ -477,7 +399,7 @@ namespace nlsat { } } } - TRACE("linxi_simple_checker", + TRACE("simple_checker", tout << "mag di: "; display(tout, am, mag_di); tout << "\n"; @@ -485,7 +407,6 @@ namespace nlsat { 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) { - LINXI_DEBUG; scoped_anum frac(am); am.div(c, a, frac); am.neg(frac); @@ -495,11 +416,10 @@ namespace nlsat { 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) { - LINXI_DEBUG; Domain_Interval now_di(am); scoped_anum num(am); calc_formula(num, a, b, c); - TRACE("linxi_simple_checker", + TRACE("simple_checker", tout << "nsk: "; display(tout, nsk); tout << '\n'; @@ -537,7 +457,7 @@ namespace nlsat { else { UNREACHABLE(); } - TRACE("linxi_simple_checker", + TRACE("simple_checker", tout << "now_di: "; display(tout, am, now_di); tout << "\n"; @@ -548,29 +468,8 @@ namespace nlsat { return false; return true; } -/* -if (nsk == EQ) { -return false; -} -else if (nsk == LT) { -return false; -} -else if (nsk == GT) { -return true; -} -else if (nsk == LE) { -return false; -} -else if (nsk == GE) { -return true; -} -else { -UNREACHABLE(); -} -*/ - bool process_even_degree_formula(Var_Domain &vd, sign_kind nsk, const scoped_anum &a, unsigned b, const scoped_anum &c) { - LINXI_DEBUG; + 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); @@ -623,8 +522,6 @@ UNREACHABLE(); // di.m_upper_inf = 0; // am.set(di.m_lower, num); // am.set(di.m_upper, num); - // if (!update_interval_intersection(vd.ori_val, di)) - // return false; if (!update_interval_intersection(vd.mag_val, di)) return false; } @@ -692,7 +589,6 @@ UNREACHABLE(); } bool update_var_domain(sign_kind nsk, const scoped_anum &a, var x, unsigned b, const scoped_anum &c) { - LINXI_DEBUG; Var_Domain &vd = vars_domain[x]; if (am.is_neg(a)) { if (nsk == LT) @@ -722,22 +618,12 @@ UNREACHABLE(); bool check_is_axbc(const poly *p, scoped_anum &a, var &x, unsigned &b, scoped_anum& c) { // is a*(x^b) + c*1 form - // LINXI_DEBUG; - // LINXI_HERE; - // TRACE("linxi_simple_checker", - // tout << a << "x[" << x << "]^" << b << " "; - // tout << "+ " << c << " "; - // // display(tout, nsk); - // // tout << " 0\n"; - // ); if (pm.size(p) == 1 && pm.is_var(pm.get_monomial(p, 0), x)) { - LINXI_HERE; am.set(a, 1); b = 1; am.set(c, 0); return true; } - // LINXI_HERE; if (pm.size(p) != 2) return false; if (!pm.is_unit(pm.get_monomial(p, 1))) @@ -747,7 +633,7 @@ UNREACHABLE(); return false; x = pm.get_var(m, 0); b = pm.degree(m, 0); - // LINXI_HERE; + am.set(a, pm.coeff(p, 0)); am.set(c, pm.coeff(p, 1)); return true; @@ -755,7 +641,6 @@ UNREACHABLE(); bool collect_domain_axbc_form(unsigned cid, unsigned lid) { // is_var_num, a*(x^b) + c form - LINXI_DEBUG; literal lit = (*clauses[cid])[lid]; bool s = lit.sign(); ineq_atom *ia = to_ineq_atom(atoms[lit.var()]); @@ -786,14 +671,14 @@ UNREACHABLE(); else if (nsk == GT) nsk = LE; } - TRACE("linxi_simple_checker", + 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("linxi_simple_checker", + TRACE("simple_checker", tout << "original: "; display(tout, am, vars_domain[x].ori_val); tout << "\nmagnitude: "; @@ -804,7 +689,6 @@ UNREACHABLE(); } 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 - LINXI_DEBUG; unsigned psz = pm.size(p); am.set(c, 0); for (unsigned i = 0; i < psz; ++i) { @@ -812,23 +696,9 @@ UNREACHABLE(); if (pm.size(m) > 1) return false; } - LINXI_HERE; cnt = 0; for (unsigned i = 0; i < psz; ++i) { monomial *m = pm.get_monomial(p, i); - // TRACE("linxi_simple_checker", - // tout << "monomial: "; - // pm.display(tout, m); - // tout << '\n'; - // // tout << "coefficient: " << pm.coeff(p, i) << "\n"; - // tout << "m size: " << pm.size(m) << '\n'; - // tout << "# "; - // for (unsigned j = 0, sz = pm.size(m); j < sz; ++j) { - // var v = pm.get_var(m, j); - // tout << " (" << j << ", " << pm.degree_of(m, v) << ")"; - // } - // tout << "\n"; - // ); if (pm.size(m) == 0) { am.set(c, pm.coeff(p, i)); } @@ -837,9 +707,6 @@ UNREACHABLE(); am.set(as[cnt++], pm.coeff(p, i)); xs.push_back(pm.get_var(m, 0)); bs.push_back(pm.degree(m, 0)); - // TRACE("linxi_simple_checker", - // tout << as.back() << "x[" << xs.back() << "]^" << bs.back() << "\n"; - // ); } } return true; @@ -875,9 +742,6 @@ UNREACHABLE(); else if (am.is_pos(vd.ori_val.m_lower.m_val)) { ret = GT; } - // else { - // ret = NONE; - // } if (am.is_zero(vd.ori_val.m_upper.m_val)) { if (vd.ori_val.m_upper.m_open) ret = LT; @@ -886,10 +750,7 @@ UNREACHABLE(); } else if (am.is_neg(vd.ori_val.m_upper.m_val)) { ret = LT; - } - // else { - // ret = NONE; - // } + } } else if (!vd.ori_val.m_lower.m_inf) { if (am.is_pos(vd.ori_val.m_lower.m_val)) { @@ -934,7 +795,7 @@ UNREACHABLE(); unsigned sz = as.size(); for (unsigned i = 1; i < sz; ++i) { sign_kind now = get_axb_sign(as[i], xs[i], bs[i]); - TRACE("linxi_simple_checker", + TRACE("simple_checker", tout << "sta: "; display(tout, sta); tout << "\n"; @@ -959,43 +820,14 @@ UNREACHABLE(); if (sta != now) sta = GT; } - TRACE("linxi_simple_checker", + TRACE("simple_checker", tout << "after merge\n"; tout << "sta: "; display(tout, sta); tout << "\n"; ); } - // if (am.is_zero(c)) { - // // sta = sta; - // } - // else if (am.is_neg(c)) { - // if (sta == EQ) - // sta = LT; - // // else if (sta == LT) - // // sta = LT; - // else if (sta == LE) - // sta = LT; - // else if (sta == GT) - // sta = NONE; - // else if (sta == GE) - // sta = NONE; - // } - // else { // a > 0 - // if (sta == EQ) - // sta = GT; - // else if (sta == LT) - // sta = NONE; - // else if (sta == LE) - // sta = NONE; - // // else if (sta == GT) - // // sta = GT; - // else if (sta == GE) - // sta = GT; - // } - // if (sta == NONE) - // return false; - TRACE("linxi_simple_checker", + TRACE("simple_checker", tout << "sta: "; display(tout, sta); tout << "\n"; @@ -1016,7 +848,6 @@ 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 @@ -1158,7 +989,6 @@ else { // ( == 0) + (c > 0) -> > 0 return false; } bool collect_domain_sign_ineq_consistent_form(sign_kind nsk, vector &as, vector &xs, vector &bs, scoped_anum& c) { - LINXI_DEBUG; for (unsigned i = 0, sz = as.size(); i < sz; ++i) { if (!update_var_domain(nsk, as[i], xs[i], bs[i], c)) return false; @@ -1166,9 +996,8 @@ else { // ( == 0) + (c > 0) -> > 0 return true; } bool process_axbsc_form(sign_kind nsk, unsigned cid, vector &as, vector &xs, vector &bs, scoped_anum& c) { - LINXI_DEBUG; bool is_conflict(false); - TRACE("linxi_simple_checker", + TRACE("simple_checker", for (unsigned i = 0, sz = as.size(); i < sz; ++i) { if (i > 0) tout << "+ "; @@ -1180,7 +1009,7 @@ else { // ( == 0) + (c > 0) -> > 0 ); if (!check_is_sign_ineq_consistent(nsk, as, xs, bs, c, is_conflict)) return true; - TRACE("linxi_simple_checker", + TRACE("simple_checker", tout << "is conflict: " << is_conflict << "\n" ); if (is_conflict) @@ -1191,7 +1020,6 @@ else { // ( == 0) + (c > 0) -> > 0 return true; } bool collect_domain_axbsc_form(unsigned cid, unsigned lid) { - LINXI_DEBUG; // [a*(x^k)] + ... + [a*(x^b)] + k form literal lit = (*clauses[cid])[lid]; bool s = lit.sign(); @@ -1216,7 +1044,7 @@ else { // ( == 0) + (c > 0) -> > 0 return true; } literal_special_kind[cid][lid] = AXBSC; - TRACE("linxi_simple_checker", + TRACE("simple_checker", tout << "as size: " << as.size() << '\n'; ); while (as.size() > cnt) @@ -1231,7 +1059,7 @@ else { // ( == 0) + (c > 0) -> > 0 else if (nsk == GT) nsk = LE; } - TRACE("linxi_simple_checker", + TRACE("simple_checker", tout << "ineq atom: " << '\n'; for (unsigned i = 0, sz = iat->size(); i < sz; ++i) { pm.display(tout, iat->p(i)); @@ -1254,16 +1082,8 @@ else { // ( == 0) + (c > 0) -> > 0 return false; return true; } - // bool update_all_mag_domain_by_ori() { - // LINXI_HERE; - // for (unsigned i = 0; i < arith_var_num; ++i) { - // if (!update_var_mag_domain_interval_by_ori(vars_domain[i], vars_domain[i].ori_val)) - // return false; - // } - // return true; - // } + bool collect_var_domain() { - LINXI_DEBUG; // vector vec_id; for (unsigned i = 0, sz = clauses.size(); i < sz; ++i) { if (clauses_visited[i].visited) @@ -1286,9 +1106,7 @@ else { // ( == 0) + (c > 0) -> > 0 if (!collect_domain_axbc_form(i, 0)) return false; } - // if (!update_all_mag_domain_by_ori()) - // return false; - TRACE("linxi_simple_checker", + TRACE("simple_checker", for (unsigned i = 0; i < arith_var_num; ++i) { tout << "====== arith[" << i << "] ======\n"; tout << "original value: "; @@ -1299,16 +1117,11 @@ else { // ( == 0) + (c > 0) -> > 0 tout << "====== arith[" << i << "] ======\n"; } ); - // TRACE("linxi_simple_checker", - // tout << "vec_id.size(): " << vec_id.size() << "\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; } - // if (!update_all_mag_domain_by_ori()) - // return false; return true; } void endpoint_multiply(const Endpoint &a, const Endpoint &b, Endpoint &c) { @@ -1341,7 +1154,7 @@ else { // ( == 0) + (c > 0) -> > 0 } } void merge_mul_domain(Domain_Interval &pre, const Domain_Interval &now) { - TRACE("linxi_simple_checker", + TRACE("simple_checker", tout << "dom: "; display(tout, am, pre); tout << "\n"; @@ -1365,241 +1178,10 @@ else { // ( == 0) + (c > 0) -> > 0 pre.m_lower.m_is_lower = 1; pre.m_upper.copy(*pmx); pre.m_upper.m_is_lower = 0; - - // if (pre.m_lower_inf && pre.m_upper_inf) { - // if ((!now.m_lower_inf && am.is_zero(now.m_lower)) && - // (!now.m_upper_inf && am.is_zero(now.m_upper))) { - - // } - // else { - // return ; - // } - // } - // if ((!pre.m_lower_inf && am.is_zero(pre.m_lower)) && - // (!pre.m_upper_inf && am.is_zero(pre.m_upper))) - // return ; - // if (now.m_lower_inf && now.m_upper_inf) { - // pre.m_lower_inf = 1; - // pre.m_upper_inf = 1; - // return ; - // } - // if (pre.m_lower_inf == 0 && !am.is_neg(pre.m_lower)) { - // // {+, +/inf} - // if (now.m_lower_inf == 0 && !am.is_neg(now.m_lower)) { - // // {+, +/inf} * {+, +/inf} - // // {a, b} * {c, d} -> {ac, bd/inf} - // pre.m_lower_open = (pre.m_lower_open | now.m_lower_open); - // am.set(pre.m_lower, now.m_lower * pre.m_lower); - - // pre.m_upper_inf = (pre.m_upper_inf | now.m_upper_inf); - // if (pre.m_upper_inf == 0) { - // pre.m_upper_open = (pre.m_upper_open | now.m_upper_open); - // am.set(pre.m_upper, now.m_upper * pre.m_upper); - // } - // } - // else if (now.m_upper_inf == 0 && !am.is_pos(now.m_upper)) { - // // {+, +/inf} * {-/inf, -} - // // {a, b} * {c, d} -> {bc, ad} - // Domain_Interval tmp_di(am, false); - // tmp_di.m_lower_inf = (pre.m_upper_inf | now.m_lower_inf); - // if (tmp_di.m_lower_inf == 0) { - // tmp_di.m_lower_open = (pre.m_upper_open | now.m_lower_open); - // am.set(tmp_di.m_lower, pre.m_upper * now.m_lower); - // } - - // tmp_di.m_upper_inf = 0; - // tmp_di.m_upper_open = (pre.m_lower_open | now.m_upper_open); - // am.set(tmp_di.m_upper, pre.m_lower * now.m_upper); - - // pre.copy(tmp_di); - // } - // else { - // // {+, +/inf} * {-/inf, +/inf} - // if (pre.m_upper_inf) { - // // {+, +inf) * {-/inf, +/inf} -> (-inf, +inf) - // pre.m_lower_inf = 1; - // } - // else { - // // {+, +} * {-/inf, +/inf} - // // {a, b} * {c, d} -> {bc, bd} - // // order matters! - // pre.m_lower_inf = now.m_lower_inf; - // if (pre.m_lower_inf == 0) { - // pre.m_lower_open = (pre.m_upper_open | now.m_lower_open); - // am.set(pre.m_lower, now.m_lower * pre.m_upper); - // } - // pre.m_upper_inf = now.m_upper_inf; - // if (pre.m_upper_inf == 0) { - // pre.m_upper_open = (pre.m_upper_open | now.m_upper_open); - // am.set(pre.m_upper, now.m_upper * pre.m_upper); - // } - // } - // } - // } - // else if (pre.m_upper_inf == 0 && !am.is_pos(pre.m_upper)) { - // LINXI_HERE; - // // {-/inf, -} - // if (now.m_upper_inf == 0 && !am.is_pos(now.m_upper)) { - // LINXI_HERE; - // // {-/inf, -} * {-/inf, -} - // if (pre.m_lower_inf || now.m_lower_inf) { - // // (-inf, b} * {c, d} -> {bd, +inf) - // // {a, b} * (-inf, d} -> {bd, +inf) - // pre.m_upper_inf = 1; - - // pre.m_lower_open = (pre.m_upper_open | now.m_upper_open); - // am.set(pre.m_lower, now.m_upper * pre.m_upper); - // } - // else { - // // {a, b} * {c, d} -> {bd, ac} - // Domain_Interval tmp_di(am, false); - // tmp_di.m_lower_inf = 0; - // tmp_di.m_upper_inf = 0; - // tmp_di.m_lower_open = (pre.m_upper_open | now.m_upper_open); - // tmp_di.m_upper_open = (pre.m_lower_open | now.m_lower_open); - // am.set(tmp_di.m_lower, pre.m_upper * now.m_upper); - // am.set(tmp_di.m_upper, pre.m_lower * now.m_lower); - // pre.copy(tmp_di); - // } - // } - // else if (now.m_lower_inf == 0 && !am.is_neg(now.m_lower)) { - // LINXI_HERE; - // // {-/inf, -} * {+, +/inf} - // // {a, b} * {c, d} -> {ad, bc} - // Domain_Interval tmp_di(am, false); - // tmp_di.m_lower_inf = (pre.m_lower_inf | now.m_upper_inf); - // if (tmp_di.m_lower_inf == 0) { - // tmp_di.m_lower_open = (pre.m_lower_open | now.m_upper_open); - // am.set(tmp_di.m_lower, pre.m_lower * now.m_upper); - // } - - // tmp_di.m_upper_inf = 0; - // tmp_di.m_upper_open = (pre.m_upper_open | now.m_lower_open); - // am.set(tmp_di.m_upper, pre.m_upper * now.m_lower); - // TRACE("linxi_simple_checker", - // tout << "tmp_di: "; - // display(tout, am, tmp_di); - // tout << "\n"; - // ); - // pre.copy(tmp_di); - // } - // else { - // LINXI_HERE; - // // {-/inf, -} * {-/inf, +/inf} - // if (pre.m_lower_inf) { - // // (-inf, -} * {-/inf, +/inf} -> (-inf, +inf) - // pre.m_upper_inf = 1; - // } - // else { - // // {-, -} * {-/inf, +/inf} - // // {pl, pu} * {nl, nu} -> {pl nu, pl nl} - // // order matters! - // pre.m_lower_inf = now.m_upper_inf; - // if (pre.m_lower_inf == 0) { - // pre.m_lower_open = (pre.m_lower_open | now.m_upper_open); - // am.set(pre.m_lower, now.m_upper * pre.m_lower); - // } - // pre.m_upper_inf = now.m_lower_inf; - // if (pre.m_upper_inf == 0) { - // pre.m_upper_open = (pre.m_lower_open | now.m_lower_open); - // am.set(pre.m_upper, now.m_lower * pre.m_lower); - // } - // } - // } - // } - // else { - // // {-/inf, +/inf} - // if (now.m_lower_inf == 0 && !am.is_neg(now.m_lower)) { - // // {-/inf, +/inf} * {+, +/inf} - // if (now.m_upper_inf) { - // // {-/inf, +/inf} * {+, +inf) -> (-inf, +inf) - // pre.m_lower_inf = 1; - // pre.m_upper_inf = 1; - // } - // else { - // // {a, b} * {c, d} -> {ad, bd} - // // {-/inf, +/inf} * {+, +} - // if (pre.m_lower_inf == 0) { - // pre.m_lower_open = (now.m_upper_open | pre.m_lower_open); - // am.set(pre.m_lower, now.m_upper * pre.m_lower); - // } - // if (pre.m_upper_inf == 0) { - // pre.m_upper_open = (now.m_upper_open | pre.m_upper_open); - // am.set(pre.m_upper, now.m_upper * pre.m_upper); - // } - // } - // } - // else if (now.m_upper_inf == 0 && !am.is_pos(now.m_upper)) { - // // {-/inf, +/inf} * {-/inf, -} - // if (now.m_lower_inf) { - // // {-/inf, +/inf} * (-inf, -} -> (-inf, +inf) - // pre.m_lower_inf = 1; - // pre.m_upper_inf = 1; - // } - // else { - // // {-/inf, +/inf} * {-, -} - // // {pl, pu} * {nl, nu} -> {pu nl, pl nl} - // // order matters! - // if (pre.m_lower_inf == 0) { - // pre.m_lower_open = (pre.m_upper_open | now.m_lower_open); - // am.set(pre.m_lower, now.m_lower * pre.m_upper); - // } - // if (pre.m_upper_inf == 0) { - // pre.m_upper_open = (pre.m_lower_open | now.m_lower_open); - // am.set(pre.m_upper, now.m_lower * pre.m_lower); - // } - // } - // } - // else { - // // {-/inf, +/inf} * {-/inf, +/inf} - // if (pre.m_lower_inf || pre.m_upper_inf || - // now.m_lower_inf || now.m_upper_inf) { - // pre.m_lower_inf = 1; - // pre.m_upper_inf = 1; - // } - // else { - // // {-, +} * {-, +} - // scoped_anum plnl(am), punu(am); - // unsigned plo, puo; - // am.set(plnl, pre.m_lower * now.m_lower); - // am.set(punu, pre.m_upper * now.m_upper); - // scoped_anum plnu(am), punl(am); - // am.set(plnu, pre.m_lower * now.m_upper); - // am.set(punl, pre.m_upper * now.m_lower); - // if (plnl > punu) { - // puo = (pre.m_lower_open | now.m_lower_open); - // am.set(pre.m_upper, plnl); - // } - // else if (plnl == punu) { - // puo = ((pre.m_lower_open | now.m_lower_open) & - // (pre.m_upper_open | now.m_upper_open)); - // am.set(pre.m_upper, plnl); - // } - // else { - // puo = (pre.m_upper_open | now.m_upper_open); - // am.set(pre.m_upper, punu); - // } - // if (plnu < punl) { - // plo = (pre.m_lower_open | now.m_upper_open); - // am.set(pre.m_lower, plnu); - // } - // else if (plnu == punl) { - // plo = ((pre.m_lower_open | now.m_upper_open) & - // (pre.m_upper_open | now.m_lower_open)); - // am.set(pre.m_lower, plnu); - // } - // else { - // plo = (pre.m_upper_open | now.m_lower_open); - // am.set(pre.m_lower, punl); - // } - // } - // } - // } } void get_monomial_domain(monomial *m, const scoped_anum &a, Domain_Interval &dom) { - LINXI_DEBUG; - TRACE("linxi_simple_checker", + TRACE("simple_checker", tout << "monomial: "; pm.display(tout, m); tout << '\n'; @@ -1618,7 +1200,7 @@ else { // ( == 0) + (c > 0) -> > 0 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("linxi_simple_checker", + TRACE("simple_checker", tout << "dom: "; display(tout, am, dom); tout << "\n"; @@ -1630,7 +1212,7 @@ else { // ( == 0) + (c > 0) -> > 0 for (unsigned j = 0; j < deg; ++j) { merge_mul_domain(dom, di); } - TRACE("linxi_simple_checker", + TRACE("simple_checker", tout << "after merge mul: "; display(tout, am, dom); tout << "\n"; @@ -1647,32 +1229,23 @@ else { // ( == 0) + (c > 0) -> > 0 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); - // pre.m_lower_inf = (pre.m_lower_inf | now.m_lower_inf); - // if (pre.m_lower_inf == 0) { - // am.set(pre.m_lower, pre.m_lower + now.m_lower); - // pre.m_lower_open = (pre.m_lower_open | now.m_lower_open); - // } - // pre.m_upper_inf = (pre.m_upper_inf | now.m_upper_inf); - // if (pre.m_upper_inf == 0) { - // am.set(pre.m_upper, pre.m_upper + now.m_upper); - // pre.m_upper_open = (pre.m_upper_open | now.m_upper_open); - // } } + sign_kind get_poly_sign(const poly *p) { - LINXI_DEBUG; 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("linxi_simple_checker", + TRACE("simple_checker", tout << "poly: "; pm.display(tout, p); tout << "\n"; ); - TRACE("linxi_simple_checker", + TRACE("simple_checker", tout << "pre: "; display(tout, am, pre); tout << "\n"; @@ -1681,7 +1254,7 @@ else { // ( == 0) + (c > 0) -> > 0 am.set(a, pm.coeff(p, i)); Domain_Interval now(am); get_monomial_domain(pm.get_monomial(p, i), a, now); - TRACE("linxi_simple_checker", + TRACE("simple_checker", tout << "pre: "; display(tout, am, pre); tout << "\n"; @@ -1692,7 +1265,7 @@ else { // ( == 0) + (c > 0) -> > 0 if (now.m_lower.m_inf && now.m_upper.m_inf) return NONE; merge_add_domain(pre, now); - TRACE("linxi_simple_checker", + TRACE("simple_checker", tout << "after merge: "; display(tout, am, pre); tout << "\n"; @@ -1700,8 +1273,6 @@ else { // ( == 0) + (c > 0) -> > 0 if (pre.m_lower.m_inf && pre.m_upper.m_inf) return NONE; } - // if (pre.m_lower_inf && pre.m_upper_inf) - // return NONE; if (pre.m_lower.m_inf) { if (am.is_neg(pre.m_upper.m_val)) { // (-inf, -} @@ -1767,7 +1338,6 @@ else { // ( == 0) + (c > 0) -> > 0 } sign_kind get_poly_sign_degree(const poly *p, bool is_even) { - LINXI_DEBUG; sign_kind ret = get_poly_sign(p); if (is_even) { if (ret == GE || ret == LE || ret == NONE) @@ -1775,7 +1345,7 @@ else { // ( == 0) + (c > 0) -> > 0 else if (ret != EQ) ret = GT; } - TRACE("linxi_simple_checker", + TRACE("simple_checker", tout << "ret sign: "; display(tout, ret); tout << "\n"; @@ -1841,8 +1411,7 @@ else { // ( == 0) + (c > 0) -> > 0 } } bool check_ineq_atom_satisfiable(const ineq_atom *iat, bool s) { - LINXI_DEBUG; - TRACE("linxi_simple_checker", + TRACE("simple_checker", tout << "s: " << s << "\n"; tout << "kd: " << iat->get_kind() << "\n"; ); @@ -1855,7 +1424,7 @@ else { // ( == 0) + (c > 0) -> > 0 else nsk = GE; } - TRACE("linxi_simple_checker", + TRACE("simple_checker", tout << "ineq atom: " << '\n'; for (unsigned i = 0, sz = iat->size(); i < sz; ++i) { pm.display(tout, iat->p(i)); @@ -1870,25 +1439,14 @@ else { // ( == 0) + (c > 0) -> > 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)); - // TRACE("linxi_simple_checker", - // tout << "pre: "; - // display(tout, pre); - // tout << ", now: "; - // display(tout, now); - // tout << "\n"; - // ); merge_mul_sign(pre, now); - // TRACE("linxi_simple_checker", - // tout << "==> "; - // display(tout, pre); - // ); if (pre == NONE) return true; if ((nsk == EQ || nsk == GE || nsk == LE) && (pre == EQ || pre == GE || pre == LE)) return true; } - TRACE("linxi_simple_checker", + TRACE("simple_checker", tout << "pre: "; display(tout, pre); tout << ", nsk: "; @@ -1910,7 +1468,6 @@ else { // ( == 0) + (c > 0) -> > 0 return true; } bool check_literal_satisfiable(unsigned cid, unsigned lit_id) { - LINXI_DEBUG; literal lit = (*clauses[cid])[lit_id]; const var &v = lit.var(); atom *at = atoms[v]; @@ -1922,16 +1479,15 @@ else { // ( == 0) + (c > 0) -> > 0 clauses_visited[cid].visited = true; return true; } - // TRACE("linxi_sign", + // 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) { - LINXI_DEBUG; const clause *cla = clauses[cid]; - TRACE("linxi_simple_checker", + TRACE("simple_checker", tout << "clause size: " << cla->size() << '\n'; ); unsigned sz = cla->size(); @@ -1954,15 +1510,8 @@ else { // ( == 0) + (c > 0) -> > 0 clauses_visited[cid].literal_visited[i] = true; literal lit = (*clauses[cid])[i]; lit.neg(); - // if (atoms[lit.var()] != nullptr && atoms[lit.var()]->is_ineq_atom()) { - // ineq_atom *iat = to_ineq_atom(atoms[lit.var()]); - // if (to_sign_kind(iat->get_kind()) == EQ && lit.sign()) { - // continue; - // } - // } learned_unit.push_back(lit); - // sol.mk_clause(1, &lit); - TRACE("linxi_simple_checker_learned", + 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()) { @@ -1989,7 +1538,6 @@ else { // ( == 0) + (c > 0) -> > 0 return false; } bool check() { - LINXI_DEBUG; for (unsigned i = 0, sz = clauses.size(); i < sz; ++i) { if (clauses_visited[i].visited) continue; @@ -1999,14 +1547,6 @@ else { // ( == 0) + (c > 0) -> > 0 } return true; } - void test_anum() { - scoped_anum x(am), y(am); - am.set(x, 3); - am.set(y, 5); - TRACE("linxi_simple_checker", - tout << x << " " << y << std::endl; - ); - } bool operator()() { improved = true; @@ -2014,7 +1554,7 @@ else { // ( == 0) + (c > 0) -> > 0 improved = false; if (!check()) return false; - TRACE("linxi_simple_checker", + TRACE("simple_checker", for (unsigned i = 0; i < arith_var_num; ++i) { tout << "====== arith[" << i << "] ======\n"; tout << "original value: "; @@ -2026,38 +1566,16 @@ else { // ( == 0) + (c > 0) -> > 0 } ); } - // LINXI_DEBUG; - // // test_anum(); - // if (!collect_var_domain()) - // return false; - // TRACE("linxi_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"; - // } - // ); - // if (!check()) - // return false; return true; } }; - // Simple_Checker::Simple_Checker(solver &_sol, pmanager &_pm, anum_manager &_am, const clause_vector &_clauses, clause_vector &_learned, const atom_vector &_atoms, const unsigned &_arith_var_num) { 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) { - LINXI_DEBUG; - // m_imp = alloc(imp, _sol, _pm, _am, _clauses, _learned, _atoms, _arith_var_num); m_imp = alloc(imp, _pm, _am, _clauses, _learned_unit, _atoms, _arith_var_num); } Simple_Checker::~Simple_Checker() { - LINXI_DEBUG; dealloc(m_imp); } bool Simple_Checker::operator()() { - LINXI_DEBUG; return m_imp->operator()(); } } diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 30ca55e31c..1c4aabe50e 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -222,12 +222,10 @@ namespace nlsat { 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_set_0_more; + bool m_simple_check; + unsigned m_variable_ordering_strategy; + bool m_set_0_more; bool m_cell_sample; -//#linxi end struct stats { unsigned m_simplifications; @@ -297,10 +295,7 @@ namespace nlsat { 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(); -//#linxi end + m_variable_ordering_strategy = p.variable_ordering_strategy(); m_cell_sample = p.cell_sample(); @@ -1784,24 +1779,11 @@ namespace nlsat { } 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) { @@ -1809,31 +1791,24 @@ namespace nlsat { 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';); + 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_linxi_variable_ordering_strategy); + 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); - // 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 - - void apply_reorder() { m_reordered = false; if (!can_reorder()) @@ -1850,21 +1825,15 @@ namespace nlsat { lbool check() { -//#linxi begin simple check - if (m_linxi_simple_check) { + if (m_simple_check) { if (!simple_check()) { - TRACE("linxi_simple_check", tout << "real unsat\n";); + TRACE("simple_check", tout << "real unsat\n";); return l_false; } - TRACE("linxi_simple_checker_learned", + TRACE("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";); @@ -1876,12 +1845,10 @@ namespace nlsat { if (!can_reorder()) { } -//#linxi begin Variable Ordering Strategy - else if (m_linxi_variable_ordering_strategy > 0) { + else if (m_variable_ordering_strategy > 0) { run_variable_ordering_strategy(); reordered = true; } -//#linxi end Variable Ordering Strategy else if (m_random_order) { shuffle_vars(); reordered = true; @@ -2866,7 +2833,6 @@ namespace nlsat { 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; @@ -2909,20 +2875,17 @@ namespace nlsat { 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) { + if (m_simple_check) { sort_clauses_by_degree_lit_num(ws.size(), ws.data()); } else { sort_clauses_by_degree(ws.size(), ws.data()); } -//#linxi end } } diff --git a/src/nlsat/nlsat_variable_ordering_strategy.cpp b/src/nlsat/nlsat_variable_ordering_strategy.cpp index 8c4723fd30..dfcc142011 100644 --- a/src/nlsat/nlsat_variable_ordering_strategy.cpp +++ b/src/nlsat/nlsat_variable_ordering_strategy.cpp @@ -239,7 +239,7 @@ namespace nlsat { else { UNREACHABLE(); } - TRACE("linxi_reorder", + TRACE("reorder", tout << "new order: "; for (unsigned i = 0; i < num_vars; i++) tout << new_order[i] << " "; diff --git a/src/tactic/smtlogics/qfnra_tactic.cpp b/src/tactic/smtlogics/qfnra_tactic.cpp index 5ecfa24265..f95ae8a8c0 100644 --- a/src/tactic/smtlogics/qfnra_tactic.cpp +++ b/src/tactic/smtlogics/qfnra_tactic.cpp @@ -41,11 +41,11 @@ tactic * mk_multilinear_ls_tactic(ast_manager & m, params_ref const & p, unsigne return using_params(mk_smt_tactic(m), p_mls); } -tactic * linxi_mk_qfnra_very_small_solver(ast_manager& m, params_ref const& p) { +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("linxi_simple_check", true); + 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)); } @@ -55,24 +55,24 @@ tactic * linxi_mk_qfnra_very_small_solver(ast_manager& m, params_ref const& p) { 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("linxi_variable_ordering_strategy", 4); + 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("linxi_variable_ordering_strategy", 3); + 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("linxi_variable_ordering_strategy", 1); + 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("linxi_variable_ordering_strategy", 5); + 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("linxi_variable_ordering_strategy", 2); + p_order_2.set_uint("variable_ordering_strategy", 2); ts.push_back(try_for(mk_qfnra_nlsat_tactic(m, p_order_2), 10 * 1000)); } { @@ -97,11 +97,11 @@ tactic * linxi_mk_qfnra_very_small_solver(ast_manager& m, params_ref const& p) { return or_else(ts.size(), ts.data()); } -tactic * linxi_mk_qfnra_small_solver(ast_manager& m, params_ref const& p) { +tactic * mk_qfnra_small_solver(ast_manager& m, params_ref const& p) { ptr_vector ts; { params_ref p_sc = p; - p_sc.set_bool("linxi_simple_check", true); + 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)); } @@ -111,26 +111,26 @@ tactic * linxi_mk_qfnra_small_solver(ast_manager& m, params_ref const& p) { 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("linxi_variable_ordering_strategy", 4); + 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("linxi_variable_ordering_strategy", 3); + 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("linxi_variable_ordering_strategy", 1); + 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("linxi_variable_ordering_strategy", 5); + 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("linxi_variable_ordering_strategy", 2); + p_order_2.set_uint("variable_ordering_strategy", 2); ts.push_back(try_for(mk_qfnra_nlsat_tactic(m, p_order_2), 20 * 1000)); } { @@ -155,12 +155,11 @@ tactic * linxi_mk_qfnra_small_solver(ast_manager& m, params_ref const& p) { return or_else(ts.size(), ts.data()); } -tactic * linxi_mk_qfnra_middle_solver(ast_manager& m, params_ref const& p) { +tactic * mk_qfnra_middle_solver(ast_manager& m, params_ref const& p) { ptr_vector ts; { params_ref p_sc = p; - p_sc.set_bool("linxi_simple_check", true); - // p_sc.set_uint("seed", 997); + 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)); } { @@ -170,27 +169,26 @@ tactic * linxi_mk_qfnra_middle_solver(ast_manager& m, params_ref const& p) { params_ref p_order_4 = p; - p_order_4.set_uint("linxi_variable_ordering_strategy", 4); + 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("linxi_variable_ordering_strategy", 3); - // p_order_3.set_uint("seed", 17); + 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("linxi_variable_ordering_strategy", 1); + 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("linxi_variable_ordering_strategy", 5); + 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("linxi_variable_ordering_strategy", 2); + p_order_2.set_uint("variable_ordering_strategy", 2); ts.push_back(try_for(mk_qfnra_nlsat_tactic(m, p_order_2), 25 * 1000)); } { @@ -215,38 +213,36 @@ tactic * linxi_mk_qfnra_middle_solver(ast_manager& m, params_ref const& p) { return or_else(ts.size(), ts.data()); } -tactic * linxi_mk_qfnra_large_solver(ast_manager& m, params_ref const& p) { +tactic * mk_qfnra_large_solver(ast_manager& m, params_ref const& p) { ptr_vector ts; { params_ref p_sc = p; - p_sc.set_bool("linxi_simple_check", true); - // p_sc.set_uint("seed", 997); + 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("linxi_variable_ordering_strategy", 4); + 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("linxi_variable_ordering_strategy", 3); - // p_order_3.set_uint("seed", 17); + 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("linxi_variable_ordering_strategy", 1); + 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("linxi_variable_ordering_strategy", 5); + 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("linxi_variable_ordering_strategy", 2); + p_order_2.set_uint("variable_ordering_strategy", 2); ts.push_back(try_for(mk_qfnra_nlsat_tactic(m, p_order_2), 50 * 1000)); } { @@ -271,27 +267,26 @@ tactic * linxi_mk_qfnra_large_solver(ast_manager& m, params_ref const& p) { return or_else(ts.size(), ts.data()); } -tactic * linxi_mk_qfnra_very_large_solver(ast_manager& m, params_ref const& p) { +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("linxi_simple_check", true); - // p_sc.set_uint("seed", 997); + 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("linxi_variable_ordering_strategy", 1); + 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("linxi_variable_ordering_strategy", 5); + 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("linxi_variable_ordering_strategy", 2); + p_order_2.set_uint("variable_ordering_strategy", 2); ts.push_back(try_for(mk_qfnra_nlsat_tactic(m, p_order_2), 100 * 1000)); } { @@ -312,16 +307,16 @@ 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 * linxi_mk_qfnra_mixed_solver(ast_manager& m, params_ref const& p) { +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)), - linxi_mk_qfnra_very_small_solver(m, p), + mk_qfnra_very_small_solver(m, p), cond(mk_lt(mk_memory_probe(), mk_const_probe(SMALL_THRESHOLD)), - linxi_mk_qfnra_small_solver(m, p), + mk_qfnra_small_solver(m, p), cond(mk_lt(mk_memory_probe(), mk_const_probe(MIDDLE_THRESHOLD)), - linxi_mk_qfnra_middle_solver(m, p), + mk_qfnra_middle_solver(m, p), cond(mk_lt(mk_memory_probe(), mk_const_probe(LARGE_THRESHOLD)), - linxi_mk_qfnra_large_solver(m, p), - linxi_mk_qfnra_very_large_solver(m, p) + mk_qfnra_large_solver(m, p), + mk_qfnra_very_large_solver(m, p) ) ) ) @@ -332,7 +327,6 @@ tactic * mk_qfnra_tactic(ast_manager & m, params_ref const& p) { return and_then(mk_simplify_tactic(m, p), mk_propagate_values_tactic(m, p), - // mk_multilinear_ls_tactic(m, p) - linxi_mk_qfnra_mixed_solver(m, p) + mk_qfnra_mixed_solver(m, p) ); }