mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

enable shorterter mathematica printouts in nlsat

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-03-27 12:23:32 -07:00
parent e86a918ae7
commit 39df8999c8
1 changed files with 4155 additions and 4134 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

39
src/nlsat/nlsat_solver.cpp
View file

@ -464,6 +464,7 @@ namespace nlsat {
} }
else { else {
return m_pm.degree(to_root_atom(a)->p(), a->max_var()); return m_pm.degree(to_root_atom(a)->p(), a->max_var());
} }
} }
@ -528,8 +529,8 @@ namespace nlsat {
SASSERT(m_is_int.size() == m_inv_perm.size()); SASSERT(m_is_int.size() == m_inv_perm.size());
} }
bool_vector m_found_vars; mutable bool_vector m_found_vars;
void vars(literal l, var_vector& vs) { void vars(literal l, var_vector& vs) const {
vs.reset(); vs.reset();
atom * a = m_atoms[l.var()]; atom * a = m_atoms[l.var()];
if (a == nullptr) { if (a == nullptr) {
@ -3719,26 +3720,46 @@ namespace nlsat {
// Display generated lemma in Mathematica format. // Display generated lemma in Mathematica format.
// Mathematica must reduce lemma to True (modulo resource constraints). // Mathematica must reduce lemma to True (modulo resource constraints).
std::ostream& display_mathematica_lemma(std::ostream & out, unsigned num, literal const * ls, bool include_assignment = false) const { std::ostream& display_mathematica_lemma(std::ostream & out, unsigned num, literal const * ls, bool include_assignment = false) const {
out << "Resolve[ForAll[{"; bool_vector used_vars(num_vars(), false);
// var definition var_vector vars;
for (unsigned i = 0; i < num_vars(); i++) { for (unsigned i = 0; i < num; i++) {
if (i > 0) vars.reset();
out << ", "; this->vars(ls[i], vars);
out << "x" << i; for (var v : vars)
used_vars[v] = true;
}
if (include_assignment) {
for (var x = 0; x < num_vars(); x++) {
if (m_assignment.is_assigned(x))
used_vars[x] = true;
}
}
out << "Resolve[Exists[{";
bool first = true;
for (var x = 0; x < num_vars(); x++) {
if (used_vars[x]) {
if (!first) out << ", ";
first = false;
m_display_var(out, x);
}
} }
out << "}, "; out << "}, ";
if (include_assignment) { if (include_assignment) {
out << "!("; out << "!(";
if (!display_mathematica_assignment(out)) if (!display_mathematica_assignment(out))
out << "0 < 1"; // nothing was printed out << "0 < 1"; // nothing was printed
out << ") || "; out << ") || ";
} }
for (unsigned i = 0; i < num; i++) { for (unsigned i = 0; i < num; i++) {
if (i > 0) if (i > 0)
out << " || "; out << " || ";
display_mathematica(out, ls[i]); display_mathematica(out, ls[i]);
} }
out << "], Reals]\n"; // end of exists out << "], Reals]";
return out; return out;
} }