mirror of
https://github.com/Z3Prover/z3
synced 2026-02-08 01:57:59 +00:00
Remove deprecated project_original and cell_sample parameter
- Remove project_original() function from nlsat_explain.cpp - Remove m_sample_cell_project member variable - Simplify project() to just call project_cdcac() - Remove cell_sample parameter from nlsat_params.pyg - Update nlsat_solver.cpp to remove cell_sample() references - Update nlsat_explain.h constructor signature
This commit is contained in:
Lev Nachmanson
parent
c4bc251aef
commit
831a02a1dd
6 changed files with 259 additions and 48 deletions
|
|
@ -270,6 +270,8 @@ namespace nlsat {
|
|||
tout << "Level " << m_level << " SECTOR: rfunc.size=" << m_rel.m_rfunc.size()
|
||||
<< " < 2, using default heuristic\n";
|
||||
);
|
||||
// Clear m_omit_lc to avoid using stale values from a previous level
|
||||
m_omit_lc.clear();
|
||||
return m_sector_relation_mode;
|
||||
}
|
||||
|
||||
|
|
@ -331,6 +333,8 @@ namespace nlsat {
|
|||
tout << "Level " << m_level << " SECTION: rfunc.size=" << m_rel.m_rfunc.size()
|
||||
<< " < 2, using default heuristic\n";
|
||||
);
|
||||
// Clear m_omit_lc to avoid using stale values from a previous level
|
||||
m_omit_lc.clear();
|
||||
return m_section_relation_mode;
|
||||
}
|
||||
|
||||
|
|
@ -504,6 +508,11 @@ namespace nlsat {
|
|||
|
||||
void request_factorized(polynomial_ref const& poly, inv_req req) {
|
||||
for_each_distinct_factor(poly, [&](polynomial_ref const& f) {
|
||||
TRACE(lws,
|
||||
tout << " request_factorized: factor=";
|
||||
m_pm.display(tout, f);
|
||||
tout << " at level " << m_pm.max_var(f) << "\n";
|
||||
);
|
||||
request(f.get(), req); // inherit tag across factorization (SMT-RAT appendOnCorrectLevel)
|
||||
});
|
||||
}
|
||||
|
|
@ -577,6 +586,11 @@ namespace nlsat {
|
|||
}
|
||||
|
||||
void add_projections_for(polynomial_ref const& p, unsigned x, polynomial_ref const& nonzero_coeff, bool add_leading_coeff, bool add_discriminant) {
|
||||
TRACE(lws,
|
||||
tout << " add_projections_for: p=";
|
||||
m_pm.display(tout, p);
|
||||
tout << " x=" << x << " add_lc=" << add_leading_coeff << " add_disc=" << add_discriminant << "\n";
|
||||
);
|
||||
// Line 11 (non-null witness coefficient)
|
||||
if (nonzero_coeff && !is_const(nonzero_coeff))
|
||||
request_factorized(nonzero_coeff, inv_req::sign);
|
||||
|
|
@ -588,6 +602,11 @@ namespace nlsat {
|
|||
unsigned deg = m_pm.degree(p, x);
|
||||
polynomial_ref lc(m_pm);
|
||||
lc = m_pm.coeff(p, x, deg);
|
||||
TRACE(lws,
|
||||
tout << " adding lc: ";
|
||||
m_pm.display(tout, lc);
|
||||
tout << "\n";
|
||||
);
|
||||
request_factorized(lc, inv_req::sign);
|
||||
}
|
||||
}
|
||||
|
|
@ -774,18 +793,29 @@ namespace nlsat {
|
|||
|
||||
// Relation construction heuristics (same intent as previous implementation).
|
||||
void fill_relation_with_biggest_cell_heuristic() {
|
||||
TRACE(lws,
|
||||
tout << " fill_biggest_cell: m_l_rf=" << m_l_rf << ", m_u_rf=" << m_u_rf << ", rfunc.size=" << m_rel.m_rfunc.size() << "\n";
|
||||
);
|
||||
if (is_set(m_l_rf))
|
||||
for (unsigned j = 0; j < m_l_rf; ++j)
|
||||
for (unsigned j = 0; j < m_l_rf; ++j) {
|
||||
TRACE(lws, tout << " add_pair(" << j << ", " << m_l_rf << ")\n";);
|
||||
m_rel.add_pair(j, m_l_rf);
|
||||
}
|
||||
|
||||
if (is_set(m_u_rf))
|
||||
for (unsigned j = m_u_rf + 1; j < m_rel.m_rfunc.size(); ++j)
|
||||
for (unsigned j = m_u_rf + 1; j < m_rel.m_rfunc.size(); ++j) {
|
||||
TRACE(lws, tout << " add_pair(" << m_u_rf << ", " << j << ")\n";);
|
||||
m_rel.add_pair(m_u_rf, j);
|
||||
}
|
||||
|
||||
if (is_set(m_l_rf) && is_set(m_u_rf)) {
|
||||
SASSERT(m_l_rf + 1 == m_u_rf);
|
||||
TRACE(lws, tout << " add_pair(" << m_l_rf << ", " << m_u_rf << ")\n";);
|
||||
m_rel.add_pair(m_l_rf, m_u_rf);
|
||||
}
|
||||
TRACE(lws,
|
||||
tout << " fill_biggest_cell done: pairs.size=" << m_rel.m_pairs.size() << "\n";
|
||||
);
|
||||
}
|
||||
|
||||
void fill_relation_with_chain_heuristic() {
|
||||
|
|
@ -1338,10 +1368,31 @@ namespace nlsat {
|
|||
|
||||
|
||||
void add_relation_resultants() {
|
||||
TRACE(lws,
|
||||
tout << " add_relation_resultants: " << m_rel.m_pairs.size() << " pairs\n";
|
||||
);
|
||||
for (auto const& pr : m_rel.m_pairs) {
|
||||
poly* p1 = m_level_ps.get(pr.first);
|
||||
poly* p2 = m_level_ps.get(pr.second);
|
||||
request_factorized(psc_resultant(p1, p2, m_level), inv_req::ord);
|
||||
TRACE(lws,
|
||||
tout << " resultant(" << pr.first << ", " << pr.second << "): ";
|
||||
m_pm.display(tout, p1);
|
||||
tout << " and ";
|
||||
m_pm.display(tout, p2);
|
||||
tout << "\n";
|
||||
);
|
||||
polynomial_ref res = psc_resultant(p1, p2, m_level);
|
||||
TRACE(lws,
|
||||
tout << " resultant poly: ";
|
||||
if (res) {
|
||||
m_pm.display(tout, res);
|
||||
tout << "\n resultant sign at sample: " << m_am.eval_sign_at(res, sample());
|
||||
} else {
|
||||
tout << "(null)";
|
||||
}
|
||||
tout << "\n";
|
||||
);
|
||||
request_factorized(res, inv_req::ord);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -1393,6 +1444,20 @@ namespace nlsat {
|
|||
}
|
||||
|
||||
void add_level_projections_sector() {
|
||||
TRACE(lws,
|
||||
tout << "\n add_level_projections_sector at level " << m_level << "\n";
|
||||
tout << " Lower bound rf=" << m_l_rf << ", Upper bound rf=" << m_u_rf << "\n";
|
||||
if (is_set(m_l_rf)) {
|
||||
tout << " lower poly idx=" << m_rel.m_rfunc[m_l_rf].ps_idx << ": ";
|
||||
m_pm.display(tout, m_level_ps.get(m_rel.m_rfunc[m_l_rf].ps_idx));
|
||||
tout << "\n";
|
||||
}
|
||||
if (is_set(m_u_rf)) {
|
||||
tout << " upper poly idx=" << m_rel.m_rfunc[m_u_rf].ps_idx << ": ";
|
||||
m_pm.display(tout, m_level_ps.get(m_rel.m_rfunc[m_u_rf].ps_idx));
|
||||
tout << "\n";
|
||||
}
|
||||
);
|
||||
// Lines 11-12 (Algorithm 1): add projections for each p
|
||||
// Note: Algorithm 1 adds disc + ldcf for ALL polynomials (classical delineability)
|
||||
// We additionally omit leading coefficients for rootless polynomials when possible
|
||||
|
|
@ -1407,6 +1472,19 @@ namespace nlsat {
|
|||
lc = m_pm.coeff(p, m_level, deg);
|
||||
|
||||
bool add_lc = (i >= m_omit_lc.size() || !m_omit_lc[i]);
|
||||
bool is_lower_bound = is_set(m_l_rf) && i == m_rel.m_rfunc[m_l_rf].ps_idx;
|
||||
bool is_upper_bound = is_set(m_u_rf) && i == m_rel.m_rfunc[m_u_rf].ps_idx;
|
||||
|
||||
// Per Algorithm 2, Line 13 of projective_delineability.pdf:
|
||||
// Bound-defining polynomials MUST have their LC projected for delineability
|
||||
if (is_lower_bound || is_upper_bound)
|
||||
add_lc = true;
|
||||
|
||||
TRACE(lws,
|
||||
tout << " poly[" << i << "] is_lower=" << is_lower_bound << " is_upper=" << is_upper_bound;
|
||||
tout << " omit_lc[i]=" << (i < m_omit_lc.size() ? (m_omit_lc[i] ? "true" : "false") : "N/A");
|
||||
tout << " add_lc=" << add_lc << "\n";
|
||||
);
|
||||
|
||||
if (add_lc && i < usize(m_poly_has_roots) && !m_poly_has_roots[i])
|
||||
if (lc && !is_zero(lc) && m_am.eval_sign_at(lc, sample()) != 0)
|
||||
|
|
@ -1559,6 +1637,16 @@ namespace nlsat {
|
|||
}
|
||||
|
||||
void process_level() {
|
||||
TRACE(lws,
|
||||
tout << "\n--- process_level: level=" << m_level << " ---\n";
|
||||
tout << "Polynomials at this level (" << m_level_ps.size() << "):\n";
|
||||
for (unsigned i = 0; i < m_level_ps.size(); ++i) {
|
||||
tout << " ps[" << i << "]: ";
|
||||
m_pm.display(tout, m_level_ps.get(i));
|
||||
tout << "\n";
|
||||
}
|
||||
);
|
||||
|
||||
// Line 10/11: detect nullification + pick a non-zero coefficient witness per p.
|
||||
m_witnesses.clear();
|
||||
m_witnesses.reserve(m_level_ps.size());
|
||||
|
|
@ -1572,6 +1660,20 @@ namespace nlsat {
|
|||
|
||||
// Lines 3-8: Θ + I_level + relation ≼
|
||||
bool have_interval = build_interval();
|
||||
|
||||
TRACE(lws,
|
||||
tout << "Interval: ";
|
||||
display(tout, m_solver, m_I[m_level]);
|
||||
tout << "\n";
|
||||
tout << "Section? " << (m_I[m_level].section ? "yes" : "no") << "\n";
|
||||
tout << "have_interval=" << have_interval << ", rfunc.size=" << m_rel.m_rfunc.size() << "\n";
|
||||
for (unsigned i = 0; i < m_rel.m_rfunc.size(); ++i) {
|
||||
tout << " rfunc[" << i << "]: ps_idx=" << m_rel.m_rfunc[i].ps_idx << ", val=";
|
||||
m_am.display(tout, m_rel.m_rfunc[i].val);
|
||||
tout << "\n";
|
||||
}
|
||||
);
|
||||
|
||||
if (m_I[m_level].section)
|
||||
process_level_section(have_interval);
|
||||
else
|
||||
|
|
@ -1579,6 +1681,16 @@ namespace nlsat {
|
|||
}
|
||||
|
||||
void process_top_level() {
|
||||
TRACE(lws,
|
||||
tout << "\n--- process_top_level: level=" << m_n << " ---\n";
|
||||
tout << "Polynomials at top level (" << m_level_ps.size() << "):\n";
|
||||
for (unsigned i = 0; i < m_level_ps.size(); ++i) {
|
||||
tout << " ps[" << i << "]: ";
|
||||
m_pm.display(tout, m_level_ps.get(i));
|
||||
tout << "\n";
|
||||
}
|
||||
);
|
||||
|
||||
m_witnesses.clear();
|
||||
m_witnesses.reserve(m_level_ps.size());
|
||||
for (unsigned i = 0; i < m_level_ps.size(); ++i) {
|
||||
|
|
@ -1619,6 +1731,21 @@ namespace nlsat {
|
|||
}
|
||||
|
||||
std_vector<root_function_interval> single_cell_work() {
|
||||
TRACE(lws,
|
||||
tout << "Input polynomials (" << m_P.size() << "):\n";
|
||||
for (unsigned i = 0; i < m_P.size(); ++i) {
|
||||
tout << " p[" << i << "]: ";
|
||||
m_pm.display(tout, m_P.get(i));
|
||||
tout << "\n";
|
||||
}
|
||||
tout << "Sample values:\n";
|
||||
for (unsigned j = 0; j < m_n; ++j) {
|
||||
tout << " x" << j << " = ";
|
||||
m_am.display(tout, sample().value(j));
|
||||
tout << "\n";
|
||||
}
|
||||
);
|
||||
|
||||
if (m_n == 0)
|
||||
return m_I;
|
||||
|
||||
|
|
@ -1646,8 +1773,21 @@ namespace nlsat {
|
|||
extract_max_tagged();
|
||||
SASSERT(m_level < m_n);
|
||||
process_level();
|
||||
TRACE(lws,
|
||||
tout << "After level " << m_level << ": m_todo.empty()=" << m_todo.empty();
|
||||
if (!m_todo.empty()) tout << ", m_todo.max_var()=" << m_todo.max_var();
|
||||
tout << "\n";
|
||||
);
|
||||
}
|
||||
|
||||
TRACE(lws,
|
||||
for (unsigned i = 0; i < m_I.size(); ++i) {
|
||||
tout << "I[" << i << "]: ";
|
||||
display(tout, m_solver, m_I[i]);
|
||||
tout << "\n";
|
||||
}
|
||||
);
|
||||
|
||||
return m_I;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -50,7 +50,6 @@ namespace nlsat {
|
|||
bool m_factor;
|
||||
bool m_add_all_coeffs;
|
||||
bool m_add_zero_disc;
|
||||
bool m_sample_cell_project;
|
||||
|
||||
assignment const & sample() const { return m_solver.sample(); }
|
||||
assignment & sample() { return m_solver.sample(); }
|
||||
|
|
@ -142,7 +141,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, bool sample_cell_project, bool canonicalize):
|
||||
evaluator & ev, bool canonicalize):
|
||||
m_solver(s),
|
||||
m_atoms(atoms),
|
||||
m_x2eq(x2eq),
|
||||
|
|
@ -155,7 +154,6 @@ namespace nlsat {
|
|||
m_factors(m_pm),
|
||||
m_factors_save(m_pm),
|
||||
m_roots_tmp(m_am),
|
||||
m_sample_cell_project(sample_cell_project),
|
||||
m_todo(u, canonicalize),
|
||||
m_core1(s),
|
||||
m_core2(s),
|
||||
|
|
@ -1083,35 +1081,6 @@ namespace nlsat {
|
|||
\brief Apply model-based projection operation defined in our paper.
|
||||
*/
|
||||
|
||||
void project_original(polynomial_ref_vector & ps, var max_x) {
|
||||
if (ps.empty())
|
||||
return;
|
||||
m_todo.reset();
|
||||
for (poly* p : ps) {
|
||||
m_todo.insert(p);
|
||||
}
|
||||
var x = m_todo.extract_max_polys(ps);
|
||||
// Remark: after vanishing coefficients are eliminated, ps may not contain max_x anymore
|
||||
if (x < max_x)
|
||||
add_cell_lits(ps, x);
|
||||
while (true) {
|
||||
if (all_univ(ps, x) && m_todo.empty()) {
|
||||
m_todo.reset();
|
||||
break;
|
||||
}
|
||||
TRACE(nlsat_explain, tout << "project loop, processing var "; m_solver.display_var(tout, x);
|
||||
tout << "\npolynomials\n";
|
||||
display(tout, m_solver, ps); tout << "\n";);
|
||||
add_lcs(ps, x);
|
||||
psc_discriminant(ps, x);
|
||||
psc_resultant(ps, x);
|
||||
if (m_todo.empty())
|
||||
break;
|
||||
x = m_todo.extract_max_polys(ps);
|
||||
add_cell_lits(ps, x);
|
||||
}
|
||||
}
|
||||
|
||||
bool levelwise_single_cell(polynomial_ref_vector & ps, var max_x, polynomial::cache & cache) {
|
||||
levelwise lws(m_solver, ps, max_x, sample(), m_pm, m_am, cache);
|
||||
auto cell = lws.single_cell();
|
||||
|
|
@ -1208,12 +1177,7 @@ namespace nlsat {
|
|||
}
|
||||
|
||||
void project(polynomial_ref_vector & ps, var max_x) {
|
||||
if (m_sample_cell_project) {
|
||||
project_cdcac(ps, max_x);
|
||||
}
|
||||
else {
|
||||
project_original(ps, max_x);
|
||||
}
|
||||
project_cdcac(ps, max_x);
|
||||
}
|
||||
|
||||
bool check_already_added() const {
|
||||
|
|
@ -1906,8 +1870,8 @@ namespace nlsat {
|
|||
};
|
||||
|
||||
explain::explain(solver & s, assignment const & x2v, polynomial::cache & u,
|
||||
atom_vector const& atoms, atom_vector const& x2eq, evaluator & ev, bool use_cell_sample, bool canonicalize) {
|
||||
m_imp = alloc(imp, s, x2v, u, atoms, x2eq, ev, use_cell_sample, canonicalize);
|
||||
atom_vector const& atoms, atom_vector const& x2eq, evaluator & ev, bool canonicalize) {
|
||||
m_imp = alloc(imp, s, x2v, u, atoms, x2eq, ev, canonicalize);
|
||||
}
|
||||
|
||||
explain::~explain() {
|
||||
|
|
|
|||
|
|
@ -35,7 +35,7 @@ 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, bool use_cell_sample_proj, bool canonicalize);
|
||||
atom_vector const& atoms, atom_vector const& x2eq, evaluator & ev, bool canonicalize);
|
||||
|
||||
~explain();
|
||||
|
||||
|
|
|
|||
|
|
@ -5,7 +5,6 @@ def_module_params('nlsat',
|
|||
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"),
|
||||
|
|
|
|||
|
|
@ -231,7 +231,6 @@ namespace nlsat {
|
|||
unsigned m_lemma_count;
|
||||
unsigned m_variable_ordering_strategy;
|
||||
bool m_set_0_more;
|
||||
bool m_cell_sample;
|
||||
|
||||
struct stats {
|
||||
unsigned m_simplifications;
|
||||
|
|
@ -277,7 +276,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, nlsat_params(c.m_params).cell_sample(), nlsat_params(c.m_params).canonicalize()),
|
||||
m_explain(s, m_assignment, m_cache, m_atoms, m_var2eq, m_evaluator, nlsat_params(c.m_params).canonicalize()),
|
||||
m_scope_lvl(0),
|
||||
m_lemma(s),
|
||||
m_lazy_clause(s),
|
||||
|
|
@ -327,7 +326,6 @@ namespace nlsat {
|
|||
m_lws_dynamic_heuristic = p.lws_dynamic_heuristic();
|
||||
m_lws_spt_threshold = std::max(2u, p.lws_spt_threshold());
|
||||
m_check_lemmas |= !(m_debug_known_solution_file_name.empty());
|
||||
m_cell_sample = p.cell_sample();
|
||||
|
||||
m_ism.set_seed(m_random_seed);
|
||||
m_explain.set_simplify_cores(m_simplify_cores);
|
||||
|
|
|
|||
|
|
@ -1056,7 +1056,117 @@ static void tst_nullified_polynomial() {
|
|||
ENSURE(lws.failed());
|
||||
}
|
||||
|
||||
// Test case for unsound lemma lws2380 - comparing standard projection vs levelwise
|
||||
// The issue: x7 is unconstrained in levelwise output but affects the section polynomial
|
||||
static void tst_unsound_lws2380() {
|
||||
enable_trace("nlsat_explain");
|
||||
|
||||
auto run_test = [](bool use_lws) {
|
||||
std::cout << "=== tst_unsound_lws2380: " << (use_lws ? "Levelwise" : "Standard") << " projection (lws=" << use_lws << ") ===\n";
|
||||
params_ref ps;
|
||||
ps.set_bool("lws", use_lws);
|
||||
reslimit rlim;
|
||||
nlsat::solver s(rlim, ps, false);
|
||||
anum_manager & am = s.am();
|
||||
nlsat::pmanager & pm = s.pm();
|
||||
nlsat::assignment as(am);
|
||||
nlsat::explain& ex = s.get_explain();
|
||||
|
||||
// Create 14 variables x0-x13
|
||||
nlsat::var x0 = s.mk_var(false);
|
||||
nlsat::var x1 = s.mk_var(false);
|
||||
nlsat::var x2 = s.mk_var(false);
|
||||
nlsat::var x3 = s.mk_var(false);
|
||||
nlsat::var x4 = s.mk_var(false);
|
||||
nlsat::var x5 = s.mk_var(false);
|
||||
nlsat::var x6 = s.mk_var(false);
|
||||
nlsat::var x7 = s.mk_var(false);
|
||||
nlsat::var x8 = s.mk_var(false);
|
||||
nlsat::var x9 = s.mk_var(false);
|
||||
nlsat::var x10 = s.mk_var(false);
|
||||
nlsat::var x11 = s.mk_var(false);
|
||||
nlsat::var x12 = s.mk_var(false);
|
||||
nlsat::var x13 = s.mk_var(false);
|
||||
|
||||
polynomial_ref _x0(pm), _x1(pm), _x2(pm), _x3(pm), _x4(pm), _x5(pm), _x6(pm);
|
||||
polynomial_ref _x7(pm), _x8(pm), _x9(pm), _x10(pm), _x11(pm), _x12(pm), _x13(pm);
|
||||
_x0 = pm.mk_polynomial(x0);
|
||||
_x1 = pm.mk_polynomial(x1);
|
||||
_x2 = pm.mk_polynomial(x2);
|
||||
_x3 = pm.mk_polynomial(x3);
|
||||
_x4 = pm.mk_polynomial(x4);
|
||||
_x5 = pm.mk_polynomial(x5);
|
||||
_x6 = pm.mk_polynomial(x6);
|
||||
_x7 = pm.mk_polynomial(x7);
|
||||
_x8 = pm.mk_polynomial(x8);
|
||||
_x9 = pm.mk_polynomial(x9);
|
||||
_x10 = pm.mk_polynomial(x10);
|
||||
_x11 = pm.mk_polynomial(x11);
|
||||
_x12 = pm.mk_polynomial(x12);
|
||||
_x13 = pm.mk_polynomial(x13);
|
||||
|
||||
// p[0]: x13
|
||||
polynomial_ref p0(pm);
|
||||
p0 = _x13;
|
||||
|
||||
// p[1]: 170*x8*x13 + x10*x11*x12 - x11*x12 - x7*x8*x12 + x5*x10*x11 + 184*x1*x10*x11
|
||||
// - x0*x10*x11 - x5*x11 - 184*x1*x11 + x0*x11 - x3*x8*x10 + x2*x8*x10
|
||||
// - 2*x10 - 184*x1*x7*x8 - x2*x8 + 2
|
||||
polynomial_ref p1(pm);
|
||||
p1 = (170 * _x8 * _x13) +
|
||||
(_x10 * _x11 * _x12) -
|
||||
(_x11 * _x12) -
|
||||
(_x7 * _x8 * _x12) +
|
||||
(_x5 * _x10 * _x11) +
|
||||
(184 * _x1 * _x10 * _x11) -
|
||||
(_x0 * _x10 * _x11) -
|
||||
(_x5 * _x11) -
|
||||
(184 * _x1 * _x11) +
|
||||
(_x0 * _x11) -
|
||||
(_x3 * _x8 * _x10) +
|
||||
(_x2 * _x8 * _x10) -
|
||||
(2 * _x10) -
|
||||
(184 * _x1 * _x7 * _x8) -
|
||||
(_x2 * _x8) +
|
||||
2;
|
||||
|
||||
std::cout << "p0: " << p0 << "\n";
|
||||
std::cout << "p1: " << p1 << "\n";
|
||||
|
||||
// Set sample: x0=-1, x1=-1, x2=0, x3=-1, x5=0, x7=0, x8=2, x10=0, x11=0, x12=2
|
||||
scoped_anum val(am);
|
||||
am.set(val, -1); as.set(x0, val);
|
||||
am.set(val, -1); as.set(x1, val);
|
||||
am.set(val, 0); as.set(x2, val);
|
||||
am.set(val, -1); as.set(x3, val);
|
||||
am.set(val, 0); as.set(x4, val);
|
||||
am.set(val, 0); as.set(x5, val);
|
||||
am.set(val, 0); as.set(x6, val);
|
||||
am.set(val, 0); as.set(x7, val);
|
||||
am.set(val, 2); as.set(x8, val);
|
||||
am.set(val, 0); as.set(x9, val);
|
||||
am.set(val, 0); as.set(x10, val);
|
||||
am.set(val, 0); as.set(x11, val);
|
||||
am.set(val, 2); as.set(x12, val);
|
||||
am.set(val, 1); as.set(x13, val);
|
||||
s.set_rvalues(as);
|
||||
|
||||
// Create literals for the two polynomials
|
||||
nlsat::scoped_literal_vector lits(s);
|
||||
lits.push_back(mk_gt(s, p0.get())); // x13 > 0
|
||||
lits.push_back(mk_gt(s, p1.get())); // p1 > 0
|
||||
|
||||
project_fa(s, ex, x13, lits.size(), lits.data());
|
||||
std::cout << "\n";
|
||||
};
|
||||
|
||||
run_test(false); // Standard projection
|
||||
run_test(true); // Levelwise projection
|
||||
}
|
||||
|
||||
void tst_nlsat() {
|
||||
tst_unsound_lws2380();
|
||||
std::cout << "------------------\n";
|
||||
tst_polynomial_cache_mk_unique();
|
||||
std::cout << "------------------\n";
|
||||
tst_nullified_polynomial();
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue