mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

abbreviate

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-05-09 21:54:58 -07:00
parent 086331a24b
commit 0a6908cd15
1 changed files with 21 additions and 60 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -318,35 +318,21 @@ bool basics::basic_lemma_for_mon_neutral_monic_to_factor_derived(const monic& rm
return false; return false;
} }
bool mon_var_is_sep_from_zero = c().var_is_separated_from_zero(mon_var); bool mon_var_is_sep_from_zero = c().var_is_separated_from_zero(mon_var);
lpvar jl = null_lpvar; lpvar jl = null_lpvar, not_one_j = null_lpvar;
for (auto fc : f ) { for (auto fc : f) {
lpvar j = var(fc); lpvar j = var(fc);
if (j == null_lpvar && abs(val(j)) == abs_mv && if (j == null_lpvar && abs(val(j)) == abs_mv &&
c().vars_are_equiv(j, mon_var) && c().vars_are_equiv(j, mon_var) &&
(mon_var_is_sep_from_zero || c().var_is_separated_from_zero(j))) { (mon_var_is_sep_from_zero || c().var_is_separated_from_zero(j)))
jl = j; jl = j;
}
else if (j == jl) else if (j == jl)
return false; return false;
else if (abs(val(j)) != rational(1))
not_one_j = j;
} }
if (jl == null_lpvar) if (jl == null_lpvar || not_one_j = null_lpvar)
return false; return false;
lpvar not_one_j = null_lpvar;
for (auto j : f ) {
if (var(j) == jl) {
continue;
}
if (abs(val(j)) != rational(1)) {
not_one_j = var(j);
break;
}
}
if (not_one_j == null_lpvar) {
return false;
}
new_lemma lemma(c(), "|xa| = |x| & x != 0 -> |a| = 1"); new_lemma lemma(c(), "|xa| = |x| & x != 0 -> |a| = 1");
// mon_var = 0 // mon_var = 0
if (mon_var_is_sep_from_zero) if (mon_var_is_sep_from_zero)
@ -533,30 +519,17 @@ bool basics::basic_lemma_for_mon_neutral_monic_to_factor_model_based_fm(const mo
return false; return false;
} }
lpvar jl = null_lpvar; lpvar jl = null_lpvar;
for (auto j : m.vars() ) {
if (jl == null_lpvar && abs(val(j)) == abs_mv) {
jl = j;
}
else if (jl == j)
return false;
}
if (jl == null_lpvar)
return false;
lpvar not_one_j = null_lpvar; lpvar not_one_j = null_lpvar;
for (auto j : m.vars() ) { for (auto j : m.vars() ) {
if (j == jl) { if (jl == null_lpvar && abs(val(j)) == abs_mv)
continue; jl = j;
} else if (jl == j)
if (abs(val(j)) != rational(1)) { return false;
else if (abs(val(j)) != rational(1))
not_one_j = j; not_one_j = j;
break;
}
} }
if (jl == null_lpvar || not_one_j = null_lpvar)
if (not_one_j == null_lpvar) {
return false; return false;
}
new_lemma lemma(c(), __FUNCTION__); new_lemma lemma(c(), __FUNCTION__);
// mon_var = 0 // mon_var = 0
@ -644,32 +617,20 @@ bool basics::basic_lemma_for_mon_neutral_monic_to_factor_model_based(const monic
return false; return false;
} }
lpvar jl = null_lpvar; lpvar jl = null_lpvar;
lpvar not_one_j = null_lpvar;
for (auto fc : f) { for (auto fc : f) {
lpvar j = var(fc); lpvar j = var(fc);
if (j == null_lpvar && abs(val(fc)) == abs_mv) { if (j == null_lpvar && abs(val(fc)) == abs_mv)
jl = j; jl = j;
}
else if (j == jl) else if (j == jl)
return false; return false;
else if (abs(val(fc)) != rational(1))
not_one_j = j;
} }
if (jl == null_lpvar) if (jl == null_lpvar || not_one_j = null_lpvar)
return false; return false;
lpvar not_one_j = null_lpvar;
for (auto fc : f) {
if (var(fc) == jl) {
continue;
}
if (abs(val(fc)) != rational(1)) {
not_one_j = var(fc);
break;
}
}
if (not_one_j == null_lpvar) {
return false;
}
new_lemma lemma(c(), __FUNCTION__); new_lemma lemma(c(), __FUNCTION__);
// mon_var = 0 // mon_var = 0
c().mk_ineq(mon_var, llc::EQ); c().mk_ineq(mon_var, llc::EQ);