mirror of
https://github.com/Z3Prover/z3
synced 2025-11-24 14:41:28 +00:00
unsound lemma
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson
parent
11fb5c7dc4
commit
c5b2347fda
4 changed files with 188 additions and 13 deletions
|
|
@ -21,6 +21,7 @@ Revision History:
|
|||
#include "nlsat/nlsat_evaluator.h"
|
||||
#include "math/polynomial/algebraic_numbers.h"
|
||||
#include "util/ref_buffer.h"
|
||||
extern int ttt;
|
||||
|
||||
namespace nlsat {
|
||||
|
||||
|
|
@ -839,7 +840,6 @@ namespace nlsat {
|
|||
!mk_quadratic_root(k, y, i, p)) {
|
||||
bool_var b = m_solver.mk_root_atom(k, y, i, p);
|
||||
literal l(b, true);
|
||||
TRACE(nlsat_explain, tout << "adding literal\n"; display(tout, l); tout << "\n";);
|
||||
add_literal(l);
|
||||
}
|
||||
}
|
||||
|
|
@ -1013,6 +1013,13 @@ namespace nlsat {
|
|||
// Otherwise, the isolate_roots procedure will assume p is a constant polynomial.
|
||||
m_am.isolate_roots(p, undef_var_assignment(m_assignment, y), roots);
|
||||
unsigned num_roots = roots.size();
|
||||
TRACE(nlsat_explain,
|
||||
tout << "isolated roots for "; display_var(tout, y);
|
||||
tout << " with polynomial: " << p << "\n";
|
||||
for (unsigned ri = 0; ri < num_roots; ++ri) {
|
||||
m_am.display_decimal(tout << " root[" << (ri+1) << "] = ", roots[ri]);
|
||||
tout << "\n";
|
||||
});
|
||||
bool all_lt = true;
|
||||
for (unsigned i = 0; i < num_roots; i++) {
|
||||
int s = m_am.compare(y_val, roots[i]);
|
||||
|
|
@ -1648,7 +1655,7 @@ namespace nlsat {
|
|||
var max_x = max_var(m_ps);
|
||||
TRACE(nlsat_explain, tout << "polynomials in the conflict:\n"; display(tout, m_ps); tout << "\n";);
|
||||
elim_vanishing(m_ps);
|
||||
TRACE(nlsat_explain, tout << "elim vanishing\n"; display(tout, m_ps); tout << "\n";);
|
||||
TRACE(nlsat_explain, tout << "after elim_vanishing m_ps:\n"; display(tout, m_ps); tout << "\n";);
|
||||
project(m_ps, max_x);
|
||||
TRACE(nlsat_explain, tout << "after projection\n"; display(tout, m_ps); tout << "\n";);
|
||||
}
|
||||
|
|
@ -1659,6 +1666,7 @@ namespace nlsat {
|
|||
m_core2.append(num, ls);
|
||||
var max = max_var(num, ls);
|
||||
SASSERT(max != null_var);
|
||||
TRACE(nlsat_explain, display(tout << "core before normalization\n", m_core2) << "\n";);
|
||||
normalize(m_core2, max);
|
||||
TRACE(nlsat_explain, display(tout << "core after normalization\n", m_core2) << "\n";);
|
||||
simplify(m_core2, max);
|
||||
|
|
@ -1667,6 +1675,7 @@ namespace nlsat {
|
|||
m_core2.reset();
|
||||
}
|
||||
else {
|
||||
TRACE(nlsat_explain, display(tout << "core befor normalization\n", m_core2) << "\n";);
|
||||
main(num, ls);
|
||||
}
|
||||
}
|
||||
|
|
@ -1751,8 +1760,9 @@ namespace nlsat {
|
|||
process2(num, ls);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
void operator()(unsigned num, literal const * ls, scoped_literal_vector & result) {
|
||||
ttt++;
|
||||
SASSERT(check_already_added());
|
||||
SASSERT(num > 0);
|
||||
TRACE(nlsat_explain,
|
||||
|
|
@ -1760,6 +1770,11 @@ namespace nlsat {
|
|||
display(tout, num, ls) << "\n";
|
||||
m_solver.display_assignment(tout);
|
||||
);
|
||||
if (max_var(num, ls) == 0 && !m_assignment.is_assigned(0)) {
|
||||
TRACE(nlsat_explain, tout << "all literals use unassigned max var; returning justification\n";);
|
||||
result.reset();
|
||||
return;
|
||||
}
|
||||
m_result = &result;
|
||||
process(num, ls);
|
||||
reset_already_added();
|
||||
|
|
|
|||
|
|
@ -40,6 +40,8 @@ Revision History:
|
|||
#include "nlsat/nlsat_simple_checker.h"
|
||||
#include "nlsat/nlsat_variable_ordering_strategy.h"
|
||||
|
||||
int ttt = 0;
|
||||
|
||||
#define NLSAT_EXTRA_VERBOSE
|
||||
|
||||
#ifdef NLSAT_EXTRA_VERBOSE
|
||||
|
|
@ -750,6 +752,14 @@ namespace nlsat {
|
|||
m_atoms[b] = new_atom;
|
||||
new_atom->m_bool_var = b;
|
||||
m_pm.inc_ref(new_atom->p());
|
||||
TRACE(nlsat_solver,
|
||||
tout << "created root literal b" << b << ": ";
|
||||
display(tout, literal(b, false)) << "\n";
|
||||
tout << " kind: " << k << ", index: " << i << ", variable: x" << x << "\n";
|
||||
tout << " polynomial: ";
|
||||
display_polynomial(tout, new_atom->p(), m_display_var);
|
||||
tout << "\n";
|
||||
);
|
||||
return b;
|
||||
}
|
||||
|
||||
|
|
@ -1115,20 +1125,47 @@ namespace nlsat {
|
|||
}
|
||||
|
||||
void log_lemma(std::ostream& out, unsigned n, literal const* cls, bool is_valid) {
|
||||
++m_lemma_count;
|
||||
out << "(set-logic ALL)\n";
|
||||
if (is_valid) {
|
||||
display_smt2_bool_decls(out);
|
||||
display_smt2_arith_decls(out);
|
||||
if (!is_valid)
|
||||
return;
|
||||
if (false && ttt != 219)
|
||||
return;
|
||||
|
||||
// Collect arithmetic variables referenced by cls.
|
||||
std::vector<unsigned> arith_vars = collect_vars_on_clause(n, cls);
|
||||
|
||||
// Collect uninterpreted Boolean variables referenced by cls.
|
||||
bool_vector seen_bool;
|
||||
svector<bool_var> bool_vars;
|
||||
for (unsigned i = 0; i < n; ++i) {
|
||||
bool_var b = cls[i].var();
|
||||
if (seen_bool.get(b, false))
|
||||
continue;
|
||||
seen_bool.setx(b, true, false);
|
||||
if (b != 0 && m_atoms[b] == nullptr)
|
||||
bool_vars.push_back(b);
|
||||
}
|
||||
else
|
||||
display_smt2(out);
|
||||
|
||||
out << "(set-logic ALL)\n";
|
||||
|
||||
for (bool_var b : bool_vars) {
|
||||
out << "(declare-fun b" << b << " () Bool)\n";
|
||||
}
|
||||
for (unsigned x : arith_vars) {
|
||||
out << "(declare-fun ";
|
||||
m_display_var(out, x);
|
||||
out << " () " << (is_int(x) ? "Int" : "Real") << ")\n";
|
||||
}
|
||||
|
||||
for (unsigned i = 0; i < n; ++i)
|
||||
display_smt2(out << "(assert ", ~cls[i]) << ")\n";
|
||||
display(out << "(echo \"#" << m_lemma_count << " ", n, cls) << "\")\n";
|
||||
display(out << "(echo \"#" << ttt << " ", n, cls) << "\")\n";
|
||||
out << "(check-sat)\n(reset)\n";
|
||||
|
||||
TRACE(nlsat, display(tout << "(echo \"#" << m_lemma_count << " ", n, cls) << "\")\n");
|
||||
TRACE(nlsat, display(tout << "(echo \"#" << ttt << " ", n, cls) << "\")\n");
|
||||
if (false && ttt == 219) {
|
||||
std::cout << "early exit()\n";
|
||||
exit(0);
|
||||
}
|
||||
}
|
||||
|
||||
clause * mk_clause_core(unsigned num_lits, literal const * lits, bool learned, _assumption_set a) {
|
||||
|
|
@ -1599,7 +1636,16 @@ namespace nlsat {
|
|||
TRACE(nlsat_inf_set, tout << "infeasible set + current set = R, skip literal\n";
|
||||
display(tout, cls) << "\n";
|
||||
display_assignment_for_clause(tout, cls);
|
||||
m_ism.display(tout, tmp); tout << "\n";
|
||||
m_ism.display(tout, tmp) << "\n";
|
||||
literal_vector inf_lits;
|
||||
ptr_vector<clause> inf_clauses;
|
||||
m_ism.get_justifications(tmp, inf_lits, inf_clauses);
|
||||
if (!inf_lits.empty()) {
|
||||
tout << "Interval witnesses:\n";
|
||||
for (literal inf_lit : inf_lits) {
|
||||
display(tout << " ", inf_lit) << "\n";
|
||||
}
|
||||
}
|
||||
);
|
||||
R_propagate(~l, tmp, false);
|
||||
continue;
|
||||
|
|
@ -2408,6 +2454,15 @@ namespace nlsat {
|
|||
unsigned top = m_trail.size();
|
||||
bool found_decision;
|
||||
while (true) {
|
||||
if (ttt >= 10) {
|
||||
enable_trace("nlsat_explain");
|
||||
enable_trace("nlsat");
|
||||
enable_trace("nlsat_resolve");
|
||||
enable_trace("nlsat_interval");
|
||||
enable_trace("nlsat_solver");
|
||||
enable_trace("nlsat_mathematica");
|
||||
enable_trace("nlsat_inf_set");
|
||||
}
|
||||
found_decision = false;
|
||||
while (m_num_marks > 0) {
|
||||
checkpoint();
|
||||
|
|
@ -2427,6 +2482,10 @@ namespace nlsat {
|
|||
break;
|
||||
case justification::LAZY:
|
||||
resolve_lazy_justification(b, *(jst.get_lazy()));
|
||||
if (ttt == 48) {
|
||||
TRACE(nlsat_solver, tout << "early exit\n";);
|
||||
exit(0);
|
||||
}
|
||||
break;
|
||||
case justification::DECISION:
|
||||
SASSERT(m_num_marks == 0);
|
||||
|
|
|
|||
|
|
@ -227,6 +227,7 @@ int main(int argc, char ** argv) {
|
|||
TST(prime_generator);
|
||||
TST(permutation);
|
||||
TST(nlsat);
|
||||
TST(nlsat_mv);
|
||||
TST(zstring);
|
||||
if (test_all) return 0;
|
||||
TST(ext_numeral);
|
||||
|
|
|
|||
|
|
@ -717,6 +717,104 @@ static void tst10() {
|
|||
std::cout << "\n";
|
||||
}
|
||||
|
||||
void tst_nlsat_mv() {
|
||||
params_ref ps;
|
||||
reslimit rlim;
|
||||
nlsat::solver s(rlim, ps, false);
|
||||
anum_manager & am = s.am();
|
||||
nlsat::pmanager & pm = s.pm();
|
||||
nlsat::assignment assignment(am);
|
||||
nlsat::explain& ex = s.get_explain();
|
||||
|
||||
// Regression: reproduce lemma 114 where main_operator adds spurious bounds.
|
||||
nlsat::var x0 = s.mk_var(false);
|
||||
nlsat::var x1 = s.mk_var(false);
|
||||
|
||||
polynomial_ref _x0(pm), _x1(pm);
|
||||
_x0 = pm.mk_polynomial(x0);
|
||||
_x1 = pm.mk_polynomial(x1);
|
||||
|
||||
polynomial_ref x0_sq(pm), x0_cu(pm), x0_4(pm), x0_5(pm);
|
||||
x0_sq = _x0 * _x0;
|
||||
x0_cu = x0_sq * _x0;
|
||||
x0_4 = x0_cu * _x0;
|
||||
x0_5 = x0_4 * _x0;
|
||||
|
||||
polynomial_ref x1_sq(pm), x1_cu(pm), x1_4(pm), x1_5(pm);
|
||||
x1_sq = _x1 * _x1;
|
||||
x1_cu = x1_sq * _x1;
|
||||
x1_4 = x1_cu * _x1;
|
||||
x1_5 = x1_4 * _x1;
|
||||
|
||||
polynomial_ref root_arg(pm);
|
||||
root_arg =
|
||||
x1_5 +
|
||||
(_x0 * x1_4) -
|
||||
(18 * x1_4) -
|
||||
(2 * x0_sq * x1_cu) -
|
||||
(2 * x0_cu * x1_sq) +
|
||||
(36 * x0_sq * x1_sq) +
|
||||
(1296 * _x0 * x1_sq) +
|
||||
(864 * x1_sq) +
|
||||
(x0_4 * _x1) +
|
||||
(1296 * x0_sq * _x1) +
|
||||
(6048 * _x0 * _x1) +
|
||||
x0_5 -
|
||||
(18 * x0_4) +
|
||||
(864 * x0_sq);
|
||||
// should be (x1^5 + x0 x1^4 - 18 x1^4 - 2 x0^2 x1^3 - 2 x0^3 x1^2 + 36 x0^2 x1^2 + 1296 x0 x1^2 + 864 x1^2 + x0^4 x1 + 1296 x0^2 x1 + 6048 x0 x1 + x0^5 - 18 x0^4 + 864 x0^2)
|
||||
std::cout << "big poly:" << root_arg << std::endl;
|
||||
nlsat::literal x1_gt_0 = mk_gt(s, _x1);
|
||||
nlsat::bool_var root_gt = s.mk_root_atom(nlsat::atom::ROOT_GT, x1, 3, root_arg.get());
|
||||
nlsat::literal x1_gt_root(root_gt, false);
|
||||
|
||||
nlsat::scoped_literal_vector lits(s);
|
||||
lits.push_back(x1_gt_0);
|
||||
lits.push_back(~x1_gt_root); // !(x1 > root[3](root_arg))
|
||||
|
||||
scoped_anum one(am), one_dup(am);
|
||||
am.set(one, 1);
|
||||
assignment.set(x0, one);
|
||||
s.set_rvalues(assignment);
|
||||
|
||||
nlsat::scoped_literal_vector result(s);
|
||||
ex.main_operator(lits.size(), lits.data(), result);
|
||||
|
||||
std::cout << "main_operator root regression core:\n";
|
||||
s.display(std::cout, lits.size(), lits.data());
|
||||
s.display(std::cout << "\n==>\n", result.size(), result.data());
|
||||
std::cout << "\n";
|
||||
|
||||
// Assign x1 only after the lemma is produced.
|
||||
am.set(one_dup, 1);
|
||||
assignment.set(x1, one_dup);
|
||||
s.set_rvalues(assignment);
|
||||
|
||||
small_object_allocator allocator;
|
||||
nlsat::evaluator eval(s, assignment, pm, allocator);
|
||||
std::cout << "input literal values at x0 = 1, x1 = 1:\n";
|
||||
for (nlsat::literal l : lits) {
|
||||
nlsat::atom* a = s.bool_var2atom(l.var());
|
||||
if (!a) {
|
||||
std::cout << "conversion bug\n";
|
||||
}
|
||||
bool value = a ? eval.eval(a, l.sign()) : false;
|
||||
s.display(std::cout << " ", l);
|
||||
std::cout << " -> " << (value ? "true" : "false") << "\n";
|
||||
}
|
||||
std::cout << "new literal values at x0 = 1, x1 = 1:\n";
|
||||
for (nlsat::literal l : result) {
|
||||
nlsat::atom* a = s.bool_var2atom(l.var());
|
||||
bool value = a ? eval.eval(a, l.sign()) : false;
|
||||
if (!a) {
|
||||
std::cout << "conversion bug\n";
|
||||
}
|
||||
s.display(std::cout << " ", l);
|
||||
std::cout << " -> " << (value ? "true" : "false") << "\n";
|
||||
}
|
||||
std::cout << "\n";
|
||||
}
|
||||
|
||||
static void tst11() {
|
||||
params_ref ps;
|
||||
reslimit rlim;
|
||||
|
|
@ -791,6 +889,8 @@ x7 := 1
|
|||
}
|
||||
|
||||
void tst_nlsat() {
|
||||
std::cout << "tst_mv\n"; exit(1);
|
||||
std::cout << "------------------\n";
|
||||
tst11();
|
||||
std::cout << "------------------\n";
|
||||
return;
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue