mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-26 04:56:03 +00:00
Code Activity

fix write_bound_lemma to include term definitions

Browse source
This commit is contained in:
Lev Nachmanson 2025-03-07 15:51:12 -10:00
parent 76b82318b8
commit 939091e2b5
2 changed files with 63 additions and 21 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1848,10 +1848,8 @@ namespace lp {
SASSERT((upper && bound < lra.get_upper_bound(j).x) ||
(!upper && bound > lra.get_lower_bound(j).x));
lconstraint_kind kind = upper ? lconstraint_kind::LE : lconstraint_kind::GE;
u_dependency* dep = lra.get_bound_constraint_witnesses_for_column(j);
u_dependency* dep = upper ? lra.get_column_upper_bound_witness(j) : lra.get_column_lower_bound_witness(j);
dep = lra.join_deps(dep, explain_fixed_in_meta_term(m_lspace.m_data));
u_dependency* j_bound_dep = upper ? lra.get_column_upper_bound_witness(j) : lra.get_column_lower_bound_witness(j);
dep = lra.join_deps(dep, j_bound_dep);
dep = lra.join_deps(dep, explain_fixed(lra.get_term(j)));
TRACE("dio", tout << "jterm:";
print_lar_term_L(lra.get_term(j), tout) << "\ndep:";

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

@ -2584,20 +2584,20 @@ namespace lp {
return;
}
}
// Start SMT2 file
// Start SMT2 file
out << "(set-info : \"generated at " << location;
out << " for " << (is_low ? "lower" : "upper") << " bound of variable " << j << ",";
out << " bound value: " << bound_val << (is_strict ? (is_low ? " < " : " > ") : (is_low ? " <= " : " >= ")) << "x" << j << "\")\n";
// Collect all variables used in dependencies
std::unordered_set<unsigned> vars_used;
vars_used.insert(j);
bool is_int = column_is_int(j);
// Linearize the dependencies
svector<constraint_index> deps;
m_dependencies.linearize(bound_dep, deps);
// Collect variables from constraints
for (auto ci : deps) {
const auto& c = m_constraints[ci];
@ -2607,31 +2607,75 @@ namespace lp {
is_int = false;
}
}
// Collect variables from terms
std::unordered_set<unsigned> term_variables;
for (unsigned var : vars_used) {
if (column_has_term(var)) {
const lar_term& term = get_term(var);
for (const auto& p : term) {
term_variables.insert(p.j());
if (!column_is_int(p.j()))
is_int = false;
}
}
}
// Add term variables to vars_used
vars_used.insert(term_variables.begin(), term_variables.end());
if (is_int) {
out << "(set-logic QF_LIA)\n\n";
}
// Declare variables
out << "; Variable declarations\n";
for (unsigned var : vars_used) {
out << "(declare-const x" << var << " " << (column_is_int(var) ? "Int" : "Real") << ")\n";
}
out << "\n";
// Define term relationships
out << "; Term definitions\n";
for (unsigned var : vars_used) {
if (column_has_term(var)) {
const lar_term& term = get_term(var);
out << "(assert (= x" << var << " ";
if (term.size() == 0) {
out << "0";
} else {
if (term.size() > 1) out << "(+ ";
bool first = true;
for (const auto& p : term) {
if (first) first = false;
else out << " ";
if (p.coeff().is_one()) {
out << "x" << p.j();
} else {
out << "(* " << format_smt2_constant(p.coeff()) << " x" << p.j() << ")";
}
}
if (term.size() > 1) out << ")";
}
out << "))\n";
}
}
out << "\n";
// Add assertions for the dependencies
out << "; Bound dependencies\n";
for (auto ci : deps) {
const auto& c = m_constraints[ci];
out << "(assert ";
// Handle the constraint type and expression
auto k = c.kind();
// Handle empty constraint (just constant)
SASSERT(c.coeffs().size());
// Normal constraint with variables
switch (k) {
case LE: out << "(<= "; break;
@ -2641,7 +2685,7 @@ namespace lp {
case EQ: out << "(= "; break;
default: out << "(unknown-constraint-type "; break;
}
// Left-hand side (variables)
if (c.coeffs().size() == 1) {
// Single variable
@ -2663,13 +2707,13 @@ namespace lp {
}
out << ") ";
}
// Right-hand side (constant)
out << format_smt2_constant(c.rhs());
out << "))\n";
}
out << "\n";
// Now add the assertion that contradicts the bound
out << "; Negation of the derived bound\n";
if (is_low) {
@ -2686,11 +2730,11 @@ namespace lp {
}
}
out << "\n";
// Check sat and get model if available
out << "(check-sat)\n";
out << "(exit)\n";
}
}
} // namespace lp