mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-06 03:10:25 +00:00
Code Activity

generate lemmas for lar_solver bounds

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-03-07 11:46:29 -10:00
parent 720fb55387
commit 50fd572e66
4 changed files with 16 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/math/lp/dioph_eq.cpp
View file

@ -176,7 +176,8 @@ namespace lp {
} }
}; };
class dioph_eq::imp { class dioph_eq::imp {
int deb_count = 0; int m_n_of_lemmas = 0;
// This class represents a term with an added constant number c, in form sum // This class represents a term with an added constant number c, in form sum
// {x_i*a_i} + c. // {x_i*a_i} + c.
class term_o : public lar_term { class term_o : public lar_term {
@ -1490,7 +1491,6 @@ namespace lp {
// h is the entry that is ready to be moved to S // h is the entry that is ready to be moved to S
lia_move tighten_bounds(unsigned h) { lia_move tighten_bounds(unsigned h) {
TRACE("dio", tout <<"deb_count:" << ++deb_count << "\n";);
SASSERT(entry_invariant(h)); SASSERT(entry_invariant(h));
protected_queue q; protected_queue q;
copy_row_to_espace(h); copy_row_to_espace(h);
@ -1777,6 +1777,7 @@ namespace lp {
return out; return out;
} }
// return true iff the column bound has been changed // return true iff the column bound has been changed
bool update_bound(const prop_bound& pb) { bool update_bound(const prop_bound& pb) {
TRACE("dio", tout << "pb: " << "x" << pb.m_j << ", low:" << pb.m_is_low << " , strict:" << pb.m_strict << " , bound:" << pb.m_bound << "\n"; lra.print_column_info(pb.m_j, tout, true);); TRACE("dio", tout << "pb: " << "x" << pb.m_j << ", low:" << pb.m_is_low << " , strict:" << pb.m_strict << " , bound:" << pb.m_bound << "\n"; lra.print_column_info(pb.m_j, tout, true););
@ -1784,6 +1785,10 @@ namespace lp {
CTRACE("dio", r, tout << "change in lar_solver: "; tout << "was updating with " << (pb.m_is_low? "lower" : "upper") << " bound " << pb.m_bound << "\n"; CTRACE("dio", r, tout << "change in lar_solver: "; tout << "was updating with " << (pb.m_is_low? "lower" : "upper") << " bound " << pb.m_bound << "\n";
tout << "the column became:\n"; tout << "the column became:\n";
lra.print_column_info(pb.m_j, tout);tout <<"return " << r << "\n";); lra.print_column_info(pb.m_j, tout);tout <<"return " << r << "\n";);
if (lra.settings().dump_bound_lemmas()) {
std::string lemma_name = "lemma" + std::to_string(m_n_of_lemmas++);
lra.write_bound_lemma_to_file(pb.m_j, pb.m_is_low, lemma_name, std::string( __FILE__)+ ","+ std::to_string(__LINE__));
}
return r; return r;
} }

13
src/math/lp/lar_solver.cpp
View file

@ -2504,7 +2504,7 @@ namespace lp {
// Otherwise the new asserted lower bound is is greater than the existing upper bound. // Otherwise the new asserted lower bound is is greater than the existing upper bound.
// dep is the reason for the new bound // dep is the reason for the new bound
void lar_solver::write_bound_lemma_to_file(unsigned j, bool is_low, const std::string & file_name) const { void lar_solver::write_bound_lemma_to_file(unsigned j, bool is_low, const std::string & file_name, const std::string& location) const {
std::ofstream file(file_name); std::ofstream file(file_name);
if (!file.is_open()) { if (!file.is_open()) {
// Handle file open error // Handle file open error
@ -2512,7 +2512,7 @@ namespace lp {
return; return;
} }
write_bound_lemma(j, is_low, file); write_bound_lemma(j, is_low, location, file);
file.close(); file.close();
if (file.fail()) { if (file.fail()) {
@ -2566,7 +2566,7 @@ namespace lp {
} }
} }
void lar_solver::write_bound_lemma(unsigned j, bool is_low, std::ostream & out) const { void lar_solver::write_bound_lemma(unsigned j, bool is_low, const std::string& location, std::ostream & out) const {
// Get the bound value and dependency // Get the bound value and dependency
mpq bound_val; mpq bound_val;
bool is_strict = false; bool is_strict = false;
@ -2586,10 +2586,9 @@ namespace lp {
} }
// Start SMT2 file // Start SMT2 file
out << "(set-info :source |\n"; out << "(set-info : \"generated at " << location;
out << " Z3 bound lemma for " << (is_low ? "lower" : "upper") << " bound of variable " << j << "\n"; out << " for " << (is_low ? "lower" : "upper") << " bound of variable " << j << ",";
out << " bound value: " << bound_val << (is_strict ? (is_low ? " < " : " > ") : (is_low ? " <= " : " >= ")) << "x" << j << "\n"; out << " bound value: " << bound_val << (is_strict ? (is_low ? " < " : " > ") : (is_low ? " <= " : " >= ")) << "x" << j << "\")\n";
out << "|)\n\n";
// Collect all variables used in dependencies // Collect all variables used in dependencies
std::unordered_set<unsigned> vars_used; std::unordered_set<unsigned> vars_used;

4
src/math/lp/lar_solver.h
View file

@ -723,9 +723,9 @@ public:
return m_usage_in_terms[j]; return m_usage_in_terms[j];
} }
void write_bound_lemma_to_file(unsigned j, bool is_low, const std::string & file_name) const; void write_bound_lemma_to_file(unsigned j, bool is_low, const std::string & file_name, const std::string & location) const;
void write_bound_lemma(unsigned j, bool is_low, std::ostream & out) const; void write_bound_lemma(unsigned j, bool is_low, const std::string & location, std::ostream & out) const;
std::function<void (const indexed_uint_set& columns_with_changed_bound)> m_find_monics_with_changed_bounds_func = nullptr; std::function<void (const indexed_uint_set& columns_with_changed_bound)> m_find_monics_with_changed_bounds_func = nullptr;
friend int_solver; friend int_solver;

2
src/math/lp/lp_settings.h
View file

@ -279,7 +279,7 @@ public:
return m_bound_propagation; return m_bound_propagation;
} }
bool dump_bounds_as_lemmas() { return m_dump_bound_lemmas; } bool dump_bound_lemmas() { return m_dump_bound_lemmas; }
bool& bound_propagation() { return m_bound_propagation; } bool& bound_propagation() { return m_bound_propagation; }