mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-05 13:56:03 +00:00
Code Activity

generate more proper proof format

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-09-30 07:42:27 -07:00
parent fdac93fff3
commit 018cb3c734
2 changed files with 9 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/math/lp/nla_stellensatz.cpp
View file

@ -547,13 +547,14 @@ namespace nla {
insert_monomials_from_constraint(ci);
auto &constraints = m_solver.lra().constraints();
unsigned initial_false_constraints = m_false_constraints.size();
for (unsigned it = 0; it < m_false_constraints.size(); ++it) {
if (it > 10 * initial_false_constraints)
break;
auto ci1 = m_false_constraints[it];
auto const &con = constraints[ci1];
auto [j, coeff] = find_max_lex_monomial(con.lhs());
lpvar j = find_max_lex_monomial(con.lhs());
if (j == lp::null_lpvar)
continue;
auto vars = m_mon2vars[j];
@ -987,13 +988,6 @@ namespace nla {
multiplication_justification just{old_ci, mi, j2};
// compute bounds constraints and sign of vars
lbool sign = add_bounds(vars, just.assumptions);
#if 1
// just skip vacuous lemmas?
if (l_undef == sign)
return lp::null_ci;
#endif
lp::lar_term new_lhs;
rational new_rhs(rhs);
for (auto const & cv : lhs) {
@ -1168,6 +1162,7 @@ namespace nla {
SASSERT(k < factors.size());
auto v = mk_term(factors[k].first);
bound_assumptions bounds{"factor = 0"};
bound_assumption b(v, lp::lconstraint_kind::EQ, rational(0));
bounds.bounds.push_back(b);

6
src/math/lp/nla_stellensatz.h
View file

@ -135,6 +135,7 @@ namespace nla {
external_justification,
internal_justification,
multiplication_justification,
resolvent_justification,
bound_assumptions>;
@ -171,6 +172,7 @@ namespace nla {
polynomial::manager m_pm;
hashtable<multiplication, multiplication::hash, multiplication::eq> m_multiplications;
hashtable<resolvent, resolvent::hash, resolvent::eq> m_resolvents;
hashtable<ineq_sig, ineq_sig::hash, ineq_sig::eq> m_inequality_table;
@ -189,12 +191,14 @@ namespace nla {
// additional variables and monomials and constraints
using term_offset = std::pair<lp::lar_term, rational>; // term and its offset
lpvar mk_monomial(svector<lp::lpvar> const& vars);
lpvar mk_monomial(svector<lp::lpvar> const &vars, lp::lpvar j);
lpvar mk_term(term_offset &t);
void gcd_normalize(vector<std::pair<rational, lpvar>> &t, lp::lconstraint_kind k, rational &rhs);
lp::constraint_index add_ineq(justification const& just, lp::lar_term &t, lp::lconstraint_kind k, rational const &rhs);
lp::constraint_index add_ineq(justification const &just, lpvar j, lp::lconstraint_kind k,
rational const &rhs);
@ -206,10 +210,12 @@ namespace nla {
lpvar add_var(bool is_int);
lbool add_bounds(svector<lpvar> const &vars, vector<bound_assumption> &bounds);
void saturate_constraints();
void saturate_constraints2();
void eliminate(lpvar mi);
void ext_resolve(lpvar j, lp::constraint_index lo, lp::constraint_index hi);
std::tuple<rational, bool, bool> compute_bound(svector<lpvar> const &vars, svector<lpvar>& quot, lpvar j, rational const& coeff, lp::constraint_index ci);
lp::constraint_index saturate_multiply(lp::constraint_index con_id, lpvar j1, lpvar j2);
void resolve(lpvar j, lp::constraint_index ci1, lp::constraint_index ci2);