mirror of
https://github.com/Z3Prover/z3
synced 2025-04-26 18:45:33 +00:00
build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
e74faf42ad
commit
caee936af5
3 changed files with 64 additions and 59 deletions
|
|
@ -70,6 +70,9 @@ public:
|
|||
lar_term(lpvar v1) {
|
||||
add_monomial(rational::one(), v1);
|
||||
}
|
||||
lar_term(rational const& a, lpvar v1) {
|
||||
add_monomial(a, v1);
|
||||
}
|
||||
lar_term(lpvar v1, rational const& b, lpvar v2) {
|
||||
add_monomial(rational::one(), v1);
|
||||
add_monomial(b, v2);
|
||||
|
|
|
|||
|
|
@ -290,7 +290,7 @@ bool basics::basic_lemma_for_mon_derived(const monic& rm) {
|
|||
// x = 0 or y = 0 -> xy = 0
|
||||
bool basics::basic_lemma_for_mon_non_zero_derived(const monic& rm, const factorization& f) {
|
||||
TRACE("nla_solver", c().trace_print_monic_and_factorization(rm, f, tout););
|
||||
if (! c().var_is_separated_from_zero(var(rm)))
|
||||
if (!c().var_is_separated_from_zero(var(rm)))
|
||||
return false;
|
||||
lpvar zero_j = null_lpvar;
|
||||
for (auto j : f) {
|
||||
|
|
@ -309,6 +309,7 @@ bool basics::basic_lemma_for_mon_non_zero_derived(const monic& rm, const factori
|
|||
explain(rm);
|
||||
return true;
|
||||
}
|
||||
|
||||
// use the fact that
|
||||
// |xabc| = |x| and x != 0 -> |a| = |b| = |c| = 1
|
||||
// it holds for integers, and for reals for a pair of factors
|
||||
|
|
@ -423,8 +424,8 @@ NSB review:
|
|||
|
||||
sign_m*m < 0 or f_j = 0 or \/_{i != j} sign_m*m >= sign_i*f_i
|
||||
|
||||
- or even without reference to factor index:
|
||||
sign_m*m < 0 or \/_{i} sign_m*m >= sign_i*f_i
|
||||
- or even, without reference to factor index:
|
||||
sign_m*m < 0 or \/_i sign_m*m >= sign_i*f_i
|
||||
|
||||
*/
|
||||
void basics::generate_pl_on_mon(const monic& m, unsigned factor_index) {
|
||||
|
|
@ -448,9 +449,15 @@ void basics::generate_pl_on_mon(const monic& m, unsigned factor_index) {
|
|||
}
|
||||
}
|
||||
}
|
||||
|
||||
// none of the factors is zero and the product is not zero
|
||||
// -> |fc[factor_index]| <= |rm|
|
||||
|
||||
/**
|
||||
none of the factors is zero and the product is not zero
|
||||
-> |fc[factor_index]| <= |rm|
|
||||
|
||||
m := f1 * .. * f_n
|
||||
|
||||
sign_m*m < 0 or f_i = 0 or \/_{j != i} sign_m*m >= sign_j*f_j
|
||||
*/
|
||||
void basics::generate_pl(const monic& m, const factorization& fc, int factor_index) {
|
||||
if (factorization_has_real(fc))
|
||||
return;
|
||||
|
|
@ -467,23 +474,21 @@ void basics::generate_pl(const monic& m, const factorization& fc, int factor_ind
|
|||
rational mv = var_val(m);
|
||||
rational sm = rational(nla::rat_sign(mv));
|
||||
unsigned mon_var = var(m);
|
||||
c().mk_ineq(sm, mon_var, llc::LT);
|
||||
lemma |= ineq(term(sm, mon_var), llc::LT, 0);
|
||||
for (factor f : fc) {
|
||||
if (fi++ != factor_index) {
|
||||
c().mk_ineq(var(f), llc::EQ);
|
||||
lemma |= ineq(var(f), llc::EQ, 0);
|
||||
} else {
|
||||
lpvar j = var(f);
|
||||
rational jv = val(j);
|
||||
rational sj = rational(nla::rat_sign(jv));
|
||||
SASSERT(sm*mv < sj*jv);
|
||||
c().mk_ineq(sj, j, llc::LT);
|
||||
c().mk_ineq(sm, mon_var, -sj, j, llc::GE);
|
||||
// NSB review: removed SASSERT(sm*mv < sj*jv);
|
||||
// NSB review: removed lemma |= ineq(term(sj, j), llc::LT, 0);
|
||||
lemma |= ineq(term(sm, mon_var, -sj, j), llc::GE, 0);
|
||||
}
|
||||
}
|
||||
if (!fc.is_mon()) {
|
||||
explain(fc);
|
||||
explain(m);
|
||||
}
|
||||
explain(fc);
|
||||
explain(m);
|
||||
}
|
||||
|
||||
bool basics::is_separated_from_zero(const factorization& f) const {
|
||||
|
|
@ -520,12 +525,12 @@ void basics::basic_lemma_for_mon_zero_model_based(const monic& rm, const factori
|
|||
SASSERT(var_val(rm).is_zero() && !c().rm_check(rm));
|
||||
new_lemma lemma(c(), "xy = 0 -> x = 0 or y = 0");
|
||||
if (!is_separated_from_zero(f)) {
|
||||
c().mk_ineq(var(rm), llc::NE);
|
||||
lemma |= ineq(var(rm), llc::NE, 0);
|
||||
for (auto j : f) {
|
||||
c().mk_ineq(var(j), llc::EQ);
|
||||
lemma |= ineq(var(j), llc::EQ, 0);
|
||||
}
|
||||
} else {
|
||||
c().mk_ineq(var(rm), llc::NE);
|
||||
lemma |= ineq(var(rm), llc::NE, 0);
|
||||
for (auto j : f) {
|
||||
c().explain_separation_from_zero(var(j));
|
||||
}
|
||||
|
|
@ -583,19 +588,19 @@ bool basics::basic_lemma_for_mon_neutral_monic_to_factor_model_based_fm(const mo
|
|||
|
||||
new_lemma lemma(c(), __FUNCTION__);
|
||||
// mon_var = 0
|
||||
c().mk_ineq(mon_var, llc::EQ);
|
||||
lemma |= ineq(mon_var, llc::EQ, 0);
|
||||
|
||||
// negate abs(jl) == abs()
|
||||
if (val(jl) == - val(mon_var))
|
||||
c().mk_ineq(jl, mon_var, llc::NE, rational::zero());
|
||||
lemma |= ineq(term(jl, mon_var), llc::NE, 0);
|
||||
else // jl == mon_var
|
||||
c().mk_ineq(jl, -rational(1), mon_var, llc::NE);
|
||||
lemma |= ineq(term(jl, -rational(1), mon_var), llc::NE, 0);
|
||||
|
||||
// not_one_j = 1
|
||||
c().mk_ineq(not_one_j, llc::EQ, rational(1));
|
||||
lemma |= ineq(not_one_j, llc::EQ, 1);
|
||||
|
||||
// not_one_j = -1
|
||||
c().mk_ineq(not_one_j, llc::EQ, -rational(1));
|
||||
lemma |= ineq(not_one_j, llc::EQ, -1);
|
||||
return true;
|
||||
}
|
||||
|
||||
|
|
@ -641,14 +646,13 @@ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monic_model_based_fm(co
|
|||
new_lemma lemma(c(), __FUNCTION__);
|
||||
for (auto j : m.vars()) {
|
||||
if (not_one == j) continue;
|
||||
c().mk_ineq(j, llc::NE, val(j));
|
||||
lemma |= ineq(j, llc::NE, val(j));
|
||||
}
|
||||
|
||||
if (not_one == null_lpvar) {
|
||||
c().mk_ineq(m.var(), llc::EQ, sign);
|
||||
} else {
|
||||
c().mk_ineq(m.var(), -sign, not_one, llc::EQ);
|
||||
}
|
||||
if (not_one == null_lpvar)
|
||||
lemma |= ineq(m.var(), llc::EQ, sign);
|
||||
else
|
||||
lemma |= ineq(term(m.var(), -sign, not_one), llc::EQ, 0);
|
||||
return true;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -197,14 +197,14 @@ void test_basic_lemma_for_mon_neutral_from_factors_to_monomial_0() {
|
|||
|
||||
nla.get_core().print_lemma(std::cout);
|
||||
|
||||
ineq i0(llc::NE, lp::lar_term(), rational(1));
|
||||
i0.m_term.add_var(lp_ac);
|
||||
ineq i1(llc::EQ, lp::lar_term(), rational(0));
|
||||
i1.m_term.add_var(lp_bde);
|
||||
i1.m_term.add_monomial(-rational(1), lp_abcde);
|
||||
ineq i2(llc::EQ, lp::lar_term(), rational(0));
|
||||
i2.m_term.add_var(lp_abcde);
|
||||
i2.m_term.add_monomial(-rational(1), lp_bde);
|
||||
ineq i0(lp_ac, llc::NE, 1);
|
||||
lp::lar_term t1, t2;
|
||||
t1.add_var(lp_bde);
|
||||
t1.add_monomial(-rational(1), lp_abcde);
|
||||
ineq i1(llc::EQ, t1, rational(0));
|
||||
t2.add_var(lp_abcde);
|
||||
t2.add_monomial(-rational(1), lp_bde);
|
||||
ineq i2(llc::EQ, t2, rational(0));
|
||||
bool found0 = false;
|
||||
bool found1 = false;
|
||||
bool found2 = false;
|
||||
|
|
@ -263,14 +263,15 @@ void test_basic_lemma_for_mon_neutral_from_factors_to_monomial_1() {
|
|||
SASSERT(lemma[0].size() == 4);
|
||||
nla.get_core().print_lemma(std::cout);
|
||||
|
||||
ineq i0(llc::NE, lp::lar_term(), rational(1));
|
||||
i0.m_term.add_var(lp_b);
|
||||
ineq i1(llc::NE, lp::lar_term(), rational(1));
|
||||
i1.m_term.add_var(lp_d);
|
||||
ineq i2(llc::NE, lp::lar_term(), rational(1));
|
||||
i2.m_term.add_var(lp_e);
|
||||
ineq i3(llc::EQ, lp::lar_term(), rational(1));
|
||||
i3.m_term.add_var(lp_bde);
|
||||
lp::lar_term t0, t1, t2, t3;
|
||||
t0.add_var(lp_b);
|
||||
t1.add_var(lp_d);
|
||||
t2.add_var(lp_e);
|
||||
t3.add_var(lp_bde);
|
||||
ineq i0(llc::NE, t0, rational(1));
|
||||
ineq i1(llc::NE, t1, rational(1));
|
||||
ineq i2(llc::NE, t2, rational(1));
|
||||
ineq i3(llc::EQ, t3, rational(1));
|
||||
bool found0 = false;
|
||||
bool found1 = false;
|
||||
bool found2 = false;
|
||||
|
|
@ -346,10 +347,12 @@ void test_basic_lemma_for_mon_zero_from_factors_to_monomial() {
|
|||
SASSERT(nla.get_core().test_check(lemma) == l_false);
|
||||
nla.get_core().print_lemma(std::cout);
|
||||
SASSERT(lemma.size() == 1 && lemma[0].size() == 2);
|
||||
ineq i0(llc::NE, lp::lar_term(), rational(0));
|
||||
i0.m_term.add_var(lp_b);
|
||||
ineq i1(llc::EQ, lp::lar_term(), rational(0));
|
||||
i1.m_term.add_var(lp_be);
|
||||
lp::lar_term t0, t1;
|
||||
t0.add_var(lp_b);
|
||||
t1.add_var(lp_be);
|
||||
|
||||
ineq i0(llc::NE, t0, rational(0));
|
||||
ineq i1(llc::EQ, t1, rational(0));
|
||||
bool found0 = false;
|
||||
bool found1 = false;
|
||||
|
||||
|
|
@ -396,12 +399,9 @@ void test_basic_lemma_for_mon_zero_from_monomial_to_factors() {
|
|||
|
||||
nla.get_core().print_lemma(std::cout);
|
||||
|
||||
ineq i0(llc::EQ, lp::lar_term(), rational(0));
|
||||
i0.m_term.add_var(lp_a);
|
||||
ineq i1(llc::EQ, lp::lar_term(), rational(0));
|
||||
i1.m_term.add_var(lp_c);
|
||||
ineq i2(llc::EQ, lp::lar_term(), rational(0));
|
||||
i2.m_term.add_var(lp_d);
|
||||
ineq i0(lp_a, llc::EQ, 0);
|
||||
ineq i1(lp_c, llc::EQ, 0);
|
||||
ineq i2(lp_d, llc::EQ, 0);
|
||||
bool found0 = false;
|
||||
bool found1 = false;
|
||||
bool found2 = false;
|
||||
|
|
@ -475,10 +475,8 @@ void test_basic_lemma_for_mon_neutral_from_monomial_to_factors() {
|
|||
|
||||
|
||||
nla.get_core().print_lemma(std::cout);
|
||||
ineq i0(llc::EQ, lp::lar_term(), rational(1));
|
||||
i0.m_term.add_var(lp_d);
|
||||
ineq i1(llc::EQ, lp::lar_term(), -rational(1));
|
||||
i1.m_term.add_var(lp_d);
|
||||
ineq i0(lp_d, llc::EQ, 1);
|
||||
ineq i1(lp_d, llc::EQ, -1);
|
||||
bool found0 = false;
|
||||
bool found1 = false;
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue