mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-25 15:23:41 +00:00
Code Activity

dump lemmas from nla_core

Browse source
This commit is contained in:
Lev Nachmanson 2025-06-24 07:40:06 -07:00
parent 8babdb32ef
commit e64aabafe8
4 changed files with 232 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

227
src/math/lp/nla_core.cpp
View file

@ -1,4 +1,4 @@
/*++
/*++
Copyright (c) 2017 Microsoft Corporation
Module Name:
@ -17,6 +17,9 @@ Author:
#include "math/grobner/pdd_solver.h"
#include "math/dd/pdd_interval.h"
#include "math/dd/pdd_eval.h"
#include "ast/ast_pp.h"
#include <fstream>
#include <sstream>
using namespace nla;
typedef lp::lar_term term;
@ -1062,9 +1065,18 @@ new_lemma::~new_lemma() {
if (current().is_conflict()) {
c.m_conflicts++;
}
// Dump NLA lemma as SMT2 if parameter is enabled
if (c.params().arith_nl_dump_lemmas()) {
dump_lemma_as_smt2();
std::cout << name << " " << (++i) << "\n" << *this;
}
IF_VERBOSE(4, verbose_stream() << name << "\n");
IF_VERBOSE(4, verbose_stream() << *this << "\n");
TRACE(nla_solver, tout << name << " " << (++i) << "\n" << *this; );
std::cout << "i:" << ++i << "\n";
}
lemma& new_lemma::current() const {
@ -1175,6 +1187,219 @@ std::ostream& new_lemma::display(std::ostream & out) const {
return out;
}
void new_lemma::dump_lemma_as_smt2() const {
if (!c.params().arith_nl_dump_lemmas()) return;
static unsigned lemma_id = 0;
std::ostringstream filename;
filename << "nla_lemma_" << (++lemma_id) << ".smt2";
std::ofstream out(filename.str());
if (!out.is_open()) {
return; // silently fail if we can't open the file
}
// Delegate to the display method for actual dumping
c.display_new_lemma_as_smt2(out, *this);
out.close();
// Print notification
// TRACE("nl_dump", tout << "Dumped NLA lemma to " << filename.str() << std::endl;);
}
// Helper function to format rational numbers in SMT2 format
void core::print_rational_smt2(std::ostream& out, const rational& r) const {
if (r.is_int()) {
out << r;
} else {
// Format as (/ numerator denominator) for SMT2
out << "(/ " << numerator(r) << " " << denominator(r) << ")";
}
}
// Display a lemma as SMT2 to the given output stream
std::ostream& core::display_new_lemma_as_smt2(std::ostream& out, const new_lemma& l) const {
// SMT2 header
out << "(set-info :source |NLA lemma from Z3|)\n";
out << "(set-logic QF_NRA)\n";
// Collect all variables used in the lemma
std::unordered_set<lpvar> vars = collect_vars(l());
// Declare variables
for (lpvar j : vars) {
std::string var_name = lra.get_variable_name(j);
if (var_name.empty()) {
var_name = "x" + std::to_string(j);
}
std::string sort = "Real";
out << "(declare-fun " << var_name << " () " << sort << ")\n";
}
// Add monic definitions (nonlinear constraints)
std::unordered_set<lpvar> monic_vars;
for (lpvar j : vars) {
if (is_monic_var(j)) {
monic_vars.insert(j);
}
}
for (lpvar j : monic_vars) {
const auto& m = emon(j);
std::string monic_var_name = lra.get_variable_name(j);
if (monic_var_name.empty()) monic_var_name = "x" + std::to_string(j);
out << "(assert ; monic definition\n (= " << monic_var_name << " ";
if (m.vars().size() == 0) {
out << "1"; // empty product = 1
} else if (m.vars().size() == 1) {
lpvar factor_var = m.vars()[0];
std::string factor_name = lra.get_variable_name(factor_var);
if (factor_name.empty()) factor_name = "x" + std::to_string(factor_var);
out << factor_name;
} else {
out << "(* ";
bool first_factor = true;
for (lpvar factor_var : m.vars()) {
if (!first_factor) out << " ";
first_factor = false;
std::string factor_name = lra.get_variable_name(factor_var);
if (factor_name.empty()) factor_name = "x" + std::to_string(factor_var);
out << factor_name;
}
out << ")";
}
out << "))\n";
}
// Add explanation constraints as assumptions
for (auto p : l().expl()) {
out << "(assert ; explanation constraint " << p.ci() << "\n ";
const auto& constraint = lra.constraints()[p.ci()];
out << "(";
// Comparison operator
switch (constraint.kind()) {
case llc::LE: out << "<="; break;
case llc::LT: out << "<"; break;
case llc::GE: out << ">="; break;
case llc::GT: out << ">"; break;
case llc::EQ: out << "="; break;
case llc::NE: out << "distinct"; break;
default: out << "unknown_cmp"; break;
}
out << " ";
auto coeffs = constraint.coeffs();
if (coeffs.empty()) {
out << "0";
} else if (coeffs.size() == 1) {
const auto& coeff_var = coeffs[0];
std::string var_name = lra.get_variable_name(coeff_var.second);
if (var_name.empty()) var_name = "x" + std::to_string(coeff_var.second);
if (coeff_var.first == rational::one()) {
out << var_name;
} else {
out << "(* ";
print_rational_smt2(out, coeff_var.first);
out << " " << var_name << ")";
}
} else {
out << "(+ ";
bool first_term = true;
for (const auto& coeff_var : coeffs) {
if (!first_term) out << " ";
first_term = false;
std::string var_name = lra.get_variable_name(coeff_var.second);
if (var_name.empty()) var_name = "x" + std::to_string(coeff_var.second);
if (coeff_var.first == rational::one()) {
out << var_name;
} else if (coeff_var.first == rational::minus_one()) {
out << "(- " << var_name << ")";
} else {
out << "(* ";
print_rational_smt2(out, coeff_var.first);
out << " " << var_name << ")";
}
}
out << ")";
}
// Free coefficient
rational free_coeff = constraint.get_free_coeff_of_left_side();
if (!free_coeff.is_zero()) {
out << " + ";
print_rational_smt2(out, free_coeff);
}
// Right side
out << " ";
print_rational_smt2(out, constraint.rhs());
out << ")\n";
out << ")\n";
}
// Add lemma as a negated assertion (to check unsatisfiability)
if (l().ineqs().empty()) {
out << "(assert false)\n";
} else {
out << "(assert (not (or\n";
bool first = true;
for (auto const& ineq : l().ineqs()) {
if (!first) out << "\n";
first = false;
out << " (";
switch (ineq.cmp()) {
case llc::LE: out << "<="; break;
case llc::LT: out << "<"; break;
case llc::GE: out << ">="; break;
case llc::GT: out << ">"; break;
case llc::EQ: out << "="; break;
case llc::NE: out << "distinct"; break;
default: out << "unknown_cmp"; break;
}
out << " ";
if (ineq.term().size() == 0) {
out << "0";
} else if (ineq.term().size() == 1) {
const auto& coeff_var = *ineq.term().begin();
std::string var_name = lra.get_variable_name(coeff_var.j());
if (var_name.empty()) var_name = "x" + std::to_string(coeff_var.j());
if (coeff_var.coeff() == rational::one()) {
out << var_name;
} else {
out << "(* ";
print_rational_smt2(out, coeff_var.coeff());
out << " " << var_name << ")";
}
} else {
out << "(+ ";
bool first_term = true;
for (const auto& coeff_var : ineq.term()) {
if (!first_term) out << " ";
first_term = false;
std::string var_name = lra.get_variable_name(coeff_var.j());
if (var_name.empty()) var_name = "x" + std::to_string(coeff_var.j());
if (coeff_var.coeff() == rational::one()) {
out << var_name;
} else if (coeff_var.coeff() == rational::minus_one()) {
out << "(- " << var_name << ")";
} else {
out << "(* ";
print_rational_smt2(out, coeff_var.coeff());
out << " " << var_name << ")";
}
}
out << ")";
}
out << " ";
print_rational_smt2(out, ineq.rs());
out << ")";
}
out << ")))\n";
}
out << "(check-sat)\n(exit)\n";
return out;
}
void core::negate_relation(new_lemma& lemma, unsigned j, const rational& a) {
SASSERT(val(j) != a);
lemma |= ineq(j, val(j) < a ? llc::GE : llc::LE, a);

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

@ -241,6 +241,8 @@ public:
std::ostream& print_product_with_vars(const T& m, std::ostream& out) const;
std::ostream& print_monic_with_vars(const monic& m, std::ostream& out) const;
std::ostream& print_explanation(const lp::explanation& exp, std::ostream& out) const;
std::ostream& display_new_lemma_as_smt2(std::ostream& out, const new_lemma& l) const;
void print_rational_smt2(std::ostream& out, const rational& r) const;
std::ostream& diagnose_pdd_miss(std::ostream& out);
template <typename T>
void trace_print_rms(const T& p, std::ostream& out);

3
src/math/lp/nla_types.h
View file

@ -78,6 +78,7 @@ namespace nla {
new_lemma(core& c, char const* name);
~new_lemma();
lemma& operator()() { return current(); }
const lemma& operator()() const { return current(); }
std::ostream& display(std::ostream& out) const;
new_lemma& operator&=(lp::explanation const& e);
new_lemma& operator&=(const monic& m);
@ -91,6 +92,8 @@ namespace nla {
new_lemma& explain_existing_lower_bound(lpvar j);
new_lemma& explain_existing_upper_bound(lpvar j);
void dump_lemma_as_smt2() const;
lp::explanation& expl() { return current().expl(); }
unsigned num_ineqs() const { return current().ineqs().size(); }

1
src/params/smt_params_helper.pyg
View file

@ -85,6 +85,7 @@ def_module_params(module_name='smt',
('arith.nl.optimize_bounds', BOOL, True, 'enable bounds optimization'),
('arith.nl.cross_nested', BOOL, True, 'enable cross-nested consistency checking'),
('arith.nl.log', BOOL, False, 'Log lemmas sent to nra solver'),
('arith.nl.dump_lemmas', BOOL, False, 'dump nl lemmas to files in smt2 format'),
('arith.propagate_eqs', BOOL, True, 'propagate (cheap) equalities'),
('arith.propagation_mode', UINT, 1, '0 - no propagation, 1 - propagate existing literals, 2 - refine finite bounds'),
('arith.branch_cut_ratio', UINT, 2, 'branch/cut ratio for linear integer arithmetic'),