mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-28 17:08:45 +00:00
Code Activity

dampen order lemmas

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-06-12 11:30:54 -07:00
parent 3927fdb55f
commit bba10c7a88
2 changed files with 6 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/math/lp/nla_order_lemmas.cpp
View file

@ -83,6 +83,9 @@ void order::order_lemma_on_binomial(const monic& ac) {
void order::order_lemma_on_binomial_sign(const monic& xy, lpvar x, lpvar y, int sign) { void order::order_lemma_on_binomial_sign(const monic& xy, lpvar x, lpvar y, int sign) {
if (!c().var_is_int(x) && val(x).is_big()) if (!c().var_is_int(x) && val(x).is_big())
return; return;
if (&xy == m_last_binom)
return;
c().trail().push(value_trail(m_last_binom, &xy));
SASSERT(!_().mon_has_zero(xy.vars())); SASSERT(!_().mon_has_zero(xy.vars()));
int sy = rat_sign(val(y)); int sy = rat_sign(val(y));
new_lemma lemma(c(), __FUNCTION__); new_lemma lemma(c(), __FUNCTION__);

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

@ -18,7 +18,9 @@ public:
order(core *c) : common(c) {} order(core *c) : common(c) {}
void order_lemma(); void order_lemma();
private: monic const* m_last_binom = nullptr;
private:
bool order_lemma_on_ac_and_bc_and_factors(const monic& ac, bool order_lemma_on_ac_and_bc_and_factors(const monic& ac,
const factor& a, const factor& a,