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

do not produce proportional lemma for non-integral vars

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-03-05 17:24:46 -08:00
parent 0ee541204f
commit 2ad94026a0
3 changed files with 14 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -390,6 +390,8 @@ bool basics::basic_lemma_for_mon_neutral_derived(const monic& rm, const factoriz
// x != 0 or y = 0 => |xy| >= |y| // x != 0 or y = 0 => |xy| >= |y|
void basics::proportion_lemma_model_based(const monic& rm, const factorization& factorization) { void basics::proportion_lemma_model_based(const monic& rm, const factorization& factorization) {
if (factorization_has_real(factorization)) // todo: handle the situaiton when all factors are greater than 1,
return; // or smaller than 1
rational rmv = abs(val(rm)); rational rmv = abs(val(rm));
if (rmv.is_zero()) { if (rmv.is_zero()) {
SASSERT(c().has_zero_factor(factorization)); SASSERT(c().has_zero_factor(factorization));
@ -490,6 +492,15 @@ bool basics::is_separated_from_zero(const factorization& f) const {
return true; return true;
} }
bool basics::factorization_has_real(const factorization& f) const {
for (const factor& fc: f) {
lpvar j = var(fc);
if (!c().var_is_int(j))
return true;
}
return false;
}
// here we use the fact xy = 0 -> x = 0 or y = 0 // here we use the fact xy = 0 -> x = 0 or y = 0
void basics::basic_lemma_for_mon_zero_model_based(const monic& rm, const factorization& f) { void basics::basic_lemma_for_mon_zero_model_based(const monic& rm, const factorization& f) {

1
src/math/lp/nla_basics_lemmas.h
View file

@ -103,5 +103,6 @@ struct basics: common {
// -> |fc[factor_index]| <= |rm| // -> |fc[factor_index]| <= |rm|
void generate_pl(const monic& rm, const factorization& fc, int factor_index); void generate_pl(const monic& rm, const factorization& fc, int factor_index);
bool is_separated_from_zero(const factorization&) const; bool is_separated_from_zero(const factorization&) const;
bool factorization_has_real(const factorization&) const;
}; };
} }

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

@ -283,8 +283,8 @@ public:
const rational& get_upper_bound(unsigned j) const; const rational& get_upper_bound(unsigned j) const;
const rational& get_lower_bound(unsigned j) const; const rational& get_lower_bound(unsigned j) const;
bool zero_is_an_inner_point_of_bounds(lpvar j) const; bool zero_is_an_inner_point_of_bounds(lpvar j) const;
bool var_is_int(lpvar j) const { return m_lar_solver.column_is_int(j); }
int rat_sign(const monic& m) const; int rat_sign(const monic& m) const;
inline int rat_sign(lpvar j) const { return nla::rat_sign(val(j)); } inline int rat_sign(lpvar j) const { return nla::rat_sign(val(j)); }