mirror of
https://github.com/Z3Prover/z3
synced 2025-11-23 06:01:26 +00:00
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson
parent
90e0c2a880
commit
111aa44dc5
1 changed files with 52 additions and 68 deletions
|
|
@ -1125,31 +1125,24 @@ namespace nlsat {
|
||||||
}
|
}
|
||||||
|
|
||||||
void log_lemma(std::ostream& out, unsigned n, literal const* cls, bool is_valid) {
|
void log_lemma(std::ostream& out, unsigned n, literal const* cls, bool is_valid) {
|
||||||
|
bool_vector used_vars(num_vars(), false);
|
||||||
// Collect arithmetic variables referenced by cls.
|
bool_vector used_bools(usize(m_atoms), false);
|
||||||
std::vector<unsigned> arith_vars = collect_vars_on_clause(n, cls);
|
var_vector vars;
|
||||||
|
for (unsigned j = 0; j < n; j++) {
|
||||||
// Collect uninterpreted Boolean variables referenced by cls.
|
literal lit = cls[j];
|
||||||
bool_vector seen_bool;
|
bool_var b = lit.var();
|
||||||
svector<bool_var> bool_vars;
|
if (b != null_bool_var && b < used_bools.size())
|
||||||
for (unsigned i = 0; i < n; ++i) {
|
used_bools[b] = true;
|
||||||
bool_var b = cls[i].var();
|
vars.reset();
|
||||||
if (seen_bool.get(b, false))
|
this->vars(lit, vars);
|
||||||
continue;
|
for (var v : vars)
|
||||||
seen_bool.setx(b, true, false);
|
used_vars[v] = true;
|
||||||
if (b != 0 && m_atoms[b] == nullptr)
|
|
||||||
bool_vars.push_back(b);
|
|
||||||
}
|
}
|
||||||
TRACE(nlsat, display(tout << "(echo \"#" << ++ttt << " expl lemma ", n, cls) << "\")\n");
|
TRACE(nlsat, display(tout << "(echo \"#" << ++ttt << " expl lemma ", n, cls) << "\")\n");
|
||||||
out << "(set-logic ALL)\n";
|
out << "(set-logic ALL)\n";
|
||||||
|
if (is_valid) {
|
||||||
for (bool_var b : bool_vars) {
|
display_smt2_bool_decls(out, used_bools);
|
||||||
out << "(declare-fun b" << b << " () Bool)\n";
|
display_smt2_arith_decls(out, used_vars);
|
||||||
}
|
|
||||||
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)
|
for (unsigned i = 0; i < n; ++i)
|
||||||
|
|
@ -1184,6 +1177,12 @@ namespace nlsat {
|
||||||
TRACE(nlsat_sort, display(tout << "mk_clause:\n", *cls) << "\n";);
|
TRACE(nlsat_sort, display(tout << "mk_clause:\n", *cls) << "\n";);
|
||||||
std::sort(cls->begin(), cls->end(), lit_lt(*this));
|
std::sort(cls->begin(), cls->end(), lit_lt(*this));
|
||||||
TRACE(nlsat, display(tout << " after sort:\n", *cls) << "\n";);
|
TRACE(nlsat, display(tout << " after sort:\n", *cls) << "\n";);
|
||||||
|
if (learned && m_log_lemmas) {
|
||||||
|
log_lemma(verbose_stream(), *cls);
|
||||||
|
}
|
||||||
|
if (learned && m_check_lemmas) {
|
||||||
|
check_lemma(cls->size(), cls->data(), false, cls->assumptions());
|
||||||
|
}
|
||||||
if (learned)
|
if (learned)
|
||||||
m_learned.push_back(cls);
|
m_learned.push_back(cls);
|
||||||
else
|
else
|
||||||
|
|
@ -2237,6 +2236,7 @@ namespace nlsat {
|
||||||
literal_vector core;
|
literal_vector core;
|
||||||
bool_vector used_vars(num_vars(), false);
|
bool_vector used_vars(num_vars(), false);
|
||||||
bool_vector used_bools(usize(m_atoms), false);
|
bool_vector used_bools(usize(m_atoms), false);
|
||||||
|
|
||||||
var_vector vars;
|
var_vector vars;
|
||||||
for (unsigned i = 0; i < jst.num_lits(); ++i) {
|
for (unsigned i = 0; i < jst.num_lits(); ++i) {
|
||||||
literal lit = ~jst.lit(i);
|
literal lit = ~jst.lit(i);
|
||||||
|
|
@ -2253,7 +2253,8 @@ namespace nlsat {
|
||||||
out << "(set-logic ALL)\n";
|
out << "(set-logic ALL)\n";
|
||||||
display_smt2_bool_decls(out, used_bools);
|
display_smt2_bool_decls(out, used_bools);
|
||||||
display_smt2_arith_decls(out, used_vars);
|
display_smt2_arith_decls(out, used_vars);
|
||||||
display_assignment_smt2(out, used_vars);
|
display_bool_assignment(out, false, &used_bools);
|
||||||
|
display_num_assignment(out, &used_vars);
|
||||||
for (literal lit : core) {
|
for (literal lit : core) {
|
||||||
literal asserted = ~lit;
|
literal asserted = ~lit;
|
||||||
bool is_root = asserted.var() != null_bool_var &&
|
bool is_root = asserted.var() != null_bool_var &&
|
||||||
|
|
@ -2511,10 +2512,6 @@ namespace nlsat {
|
||||||
break;
|
break;
|
||||||
case justification::LAZY:
|
case justification::LAZY:
|
||||||
resolve_lazy_justification(b, *(jst.get_lazy()));
|
resolve_lazy_justification(b, *(jst.get_lazy()));
|
||||||
if (ttt == 4800) {
|
|
||||||
TRACE(nlsat_solver, tout << "early exit\n";);
|
|
||||||
exit(0);
|
|
||||||
}
|
|
||||||
break;
|
break;
|
||||||
case justification::DECISION:
|
case justification::DECISION:
|
||||||
SASSERT(m_num_marks == 0);
|
SASSERT(m_num_marks == 0);
|
||||||
|
|
@ -2896,7 +2893,7 @@ namespace nlsat {
|
||||||
// verbose_stream() << "\npermutation: " << p[0] << " count " << count << " " << m_rlimit.is_canceled() << "\n";
|
// verbose_stream() << "\npermutation: " << p[0] << " count " << count << " " << m_rlimit.is_canceled() << "\n";
|
||||||
reinit_cache();
|
reinit_cache();
|
||||||
SASSERT(num_vars() == sz);
|
SASSERT(num_vars() == sz);
|
||||||
TRACE(nlsat_bool_assignment_bug, tout << "before reset watches\n"; display_bool_assignment(tout););
|
TRACE(nlsat_bool_assignment_bug, tout << "before reset watches\n"; display_bool_assignment(tout, false, nullptr););
|
||||||
reset_watches();
|
reset_watches();
|
||||||
assignment new_assignment(m_am);
|
assignment new_assignment(m_am);
|
||||||
for (var x = 0; x < num_vars(); x++) {
|
for (var x = 0; x < num_vars(); x++) {
|
||||||
|
|
@ -2938,7 +2935,7 @@ namespace nlsat {
|
||||||
m_pm.rename(sz, p);
|
m_pm.rename(sz, p);
|
||||||
for (auto& b : m_bounds)
|
for (auto& b : m_bounds)
|
||||||
b.x = p[b.x];
|
b.x = p[b.x];
|
||||||
TRACE(nlsat_bool_assignment_bug, tout << "before reinit cache\n"; display_bool_assignment(tout););
|
TRACE(nlsat_bool_assignment_bug, tout << "before reinit cache\n"; display_bool_assignment(tout, false, nullptr););
|
||||||
reinit_cache();
|
reinit_cache();
|
||||||
m_assignment.swap(new_assignment);
|
m_assignment.swap(new_assignment);
|
||||||
reattach_arith_clauses(m_clauses);
|
reattach_arith_clauses(m_clauses);
|
||||||
|
|
@ -3349,23 +3346,24 @@ namespace nlsat {
|
||||||
//
|
//
|
||||||
// -----------------------
|
// -----------------------
|
||||||
|
|
||||||
std::ostream& display_num_assignment(std::ostream & out, display_var_proc const & proc) const {
|
std::ostream& display_num_assignment(std::ostream & out, display_var_proc const & proc, const bool_vector* used_vars=nullptr) const {
|
||||||
for (var x = 0; x < num_vars(); x++) {
|
for (var x = 0; x < num_vars(); x++) {
|
||||||
if (m_assignment.is_assigned(x)) {
|
if (used_vars && (*used_vars)[x])
|
||||||
proc(out, x);
|
if (m_assignment.is_assigned(x)) {
|
||||||
out << " -> ";
|
proc(out, x);
|
||||||
m_am.display_decimal(out, m_assignment.value(x));
|
out << " -> ";
|
||||||
out << "\n";
|
m_am.display_decimal(out, m_assignment.value(x));
|
||||||
}
|
out << "\n";
|
||||||
|
}
|
||||||
}
|
}
|
||||||
return out;
|
return out;
|
||||||
}
|
}
|
||||||
|
|
||||||
std::ostream& display_bool_assignment(std::ostream & out, bool eval_atoms = false) const {
|
std::ostream& display_bool_assignment(std::ostream & out, bool eval_atoms, const bool_vector* used) const {
|
||||||
unsigned sz = usize(m_atoms);
|
unsigned sz = usize(m_atoms);
|
||||||
if (!eval_atoms) {
|
if (!eval_atoms) {
|
||||||
for (bool_var b = 0; b < sz; b++) {
|
for (bool_var b = 0; b < sz; b++) {
|
||||||
if (m_bvalues[b] == l_undef)
|
if (m_bvalues[b] == l_undef || (used && !(*used)[b]))
|
||||||
continue;
|
continue;
|
||||||
if (m_atoms[b] == nullptr)
|
if (m_atoms[b] == nullptr)
|
||||||
out << "b" << b << " -> " << (m_bvalues[b] == l_true ? "true" : "false") << " @" << m_levels[b] << "pure \n";
|
out << "b" << b << " -> " << (m_bvalues[b] == l_true ? "true" : "false") << " @" << m_levels[b] << "pure \n";
|
||||||
|
|
@ -3407,37 +3405,13 @@ namespace nlsat {
|
||||||
return !first;
|
return !first;
|
||||||
}
|
}
|
||||||
|
|
||||||
std::ostream& display_num_assignment(std::ostream & out) const {
|
std::ostream& display_num_assignment(std::ostream & out, const bool_vector* used_vars=nullptr) const {
|
||||||
return display_num_assignment(out, m_display_var);
|
return display_num_assignment(out, m_display_var, used_vars);
|
||||||
}
|
}
|
||||||
|
|
||||||
std::ostream& display_assignment(std::ostream& out, bool eval_atoms = false) const {
|
std::ostream& display_assignment(std::ostream& out, bool eval_atoms = false) const {
|
||||||
display_bool_assignment(out, eval_atoms);
|
display_bool_assignment(out, eval_atoms, nullptr);
|
||||||
display_num_assignment(out);
|
display_num_assignment(out, nullptr);
|
||||||
return out;
|
|
||||||
}
|
|
||||||
|
|
||||||
std::ostream& display_assignment_smt2(std::ostream& out, bool_vector const& used_vars) const {
|
|
||||||
bool has = false;
|
|
||||||
for (var x = 0; x < num_vars(); ++x) {
|
|
||||||
if (!used_vars.get(x, false))
|
|
||||||
continue;
|
|
||||||
if (!m_assignment.is_assigned(x))
|
|
||||||
continue;
|
|
||||||
if (!has) {
|
|
||||||
out << "(assert (and\n";
|
|
||||||
has = true;
|
|
||||||
}
|
|
||||||
out << " (= ";
|
|
||||||
m_display_var(out, x);
|
|
||||||
out << " ";
|
|
||||||
m_am.display_root_smt2(out, m_assignment.value(x));
|
|
||||||
out << ")\n";
|
|
||||||
}
|
|
||||||
if (has)
|
|
||||||
out << "))\n";
|
|
||||||
else
|
|
||||||
out << "(assert true)\n";
|
|
||||||
return out;
|
return out;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -3589,6 +3563,16 @@ namespace nlsat {
|
||||||
return out;
|
return out;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
std::ostream& display_poly_root(std::ostream& out, char const* y, root_atom const& a, display_var_proc const& proc) const {
|
||||||
|
out << "(exists (("; proc(out,a.x()); out << " Real))\n";
|
||||||
|
out << "(and (= " << y << " ";
|
||||||
|
proc(out, a.x());
|
||||||
|
out << ") (= 0 ";
|
||||||
|
display_polynomial_smt2(out, a.p(), proc);
|
||||||
|
out << ")))\n";
|
||||||
|
return out;
|
||||||
|
}
|
||||||
|
|
||||||
std::ostream& display_binary_smt2(std::ostream& out, poly const* p1, char const* rel, poly const* p2, display_var_proc const& proc) const {
|
std::ostream& display_binary_smt2(std::ostream& out, poly const* p1, char const* rel, poly const* p2, display_var_proc const& proc) const {
|
||||||
out << "(" << rel << " ";
|
out << "(" << rel << " ";
|
||||||
display_polynomial_smt2(out, p1, proc);
|
display_polynomial_smt2(out, p1, proc);
|
||||||
|
|
@ -4154,7 +4138,7 @@ namespace nlsat {
|
||||||
return out;
|
return out;
|
||||||
}
|
}
|
||||||
|
|
||||||
std::ostream& display_smt2_bool_decls(std::ostream & out, bool_vector& used_bools) const {
|
std::ostream& display_smt2_bool_decls(std::ostream & out, const bool_vector& used_bools) const {
|
||||||
unsigned sz = usize(m_atoms);
|
unsigned sz = usize(m_atoms);
|
||||||
for (unsigned i = 0; i < sz; i++) {
|
for (unsigned i = 0; i < sz; i++) {
|
||||||
if (m_atoms[i] == nullptr && used_bools[i])
|
if (m_atoms[i] == nullptr && used_bools[i])
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue