mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

cleanup

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2024-08-09 08:16:35 -10:00 committed by Lev Nachmanson
parent f81303f2f3
commit 752c999e0a
5 changed files with 95 additions and 621 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/nlsat/nlsat_params.pyg
View file

@ -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.")
))

564
src/nlsat/nlsat_simple_checker.cpp
View file

@ -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<vector<special_ineq_kind>> 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<scoped_anum> &as, vector<var> &xs, vector<unsigned> &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<scoped_anum> &as, vector<var> &xs, vector<unsigned> &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<scoped_anum> &as, vector<var> &xs, vector<unsigned> &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<unsigned> 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()();
}
}

59
src/nlsat/nlsat_solver.cpp
View file

@ -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
}
}

2
src/nlsat/nlsat_variable_ordering_strategy.cpp
View file

@ -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] << " ";

86
src/tactic/smtlogics/qfnra_tactic.cpp
View file

@ -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<tactic> 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<tactic> 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<tactic> 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<tactic> 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<tactic> 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)
);
}