mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

strengthening test cases

Browse source 
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
Lev 2018-10-30 16:57:58 -07:00 committed by Lev Nachmanson
parent 36587e4e91
commit 29710020a5
3 changed files with 53 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/util/lp/lar_term.h
View file

@ -57,7 +57,7 @@ public:
return m_coeffs; return m_coeffs;
} }
bool operator==(const lar_term & a) const { return false; } // take care not to create identical terms bool operator==(const lar_term & a) const { return m_coeffs == a.m_coeffs; }
bool operator!=(const lar_term & a) const { return ! (*this == a);} bool operator!=(const lar_term & a) const { return ! (*this == a);}
// some terms get used in add constraint // some terms get used in add constraint
// it is the same as the offset in the m_constraints // it is the same as the offset in the m_constraints

62
src/util/lp/nla_solver.cpp
View file

@ -1199,17 +1199,9 @@ void solver::test_basic_lemma_for_mon_zero_from_monomial_to_factors() {
lp::explanation exp; lp::explanation exp;
// set all vars to 1
s.set_column_value(lp_a, rational(1));
s.set_column_value(lp_b, rational(1)); s.set_column_value(lp_b, rational(1));
s.set_column_value(lp_c, rational(1));
s.set_column_value(lp_d, rational(1)); s.set_column_value(lp_d, rational(1));
s.set_column_value(lp_e, rational(1)); s.set_column_value(lp_e, rational(1));
s.set_column_value(lp_abcde, rational(1));
s.set_column_value(lp_ac, rational(1));
s.set_column_value(lp_bde, rational(1));
s.set_column_value(lp_acd, rational(1));
s.set_column_value(lp_be, rational(1));
// set bde to zero // set bde to zero
s.set_column_value(lp_bde, rational(0)); s.set_column_value(lp_bde, rational(0));
@ -1217,10 +1209,33 @@ void solver::test_basic_lemma_for_mon_zero_from_monomial_to_factors() {
SASSERT(nla.m_imp->test_check(lemma, exp) == l_false); SASSERT(nla.m_imp->test_check(lemma, exp) == l_false);
nla.m_imp->print_explanation_and_lemma(std::cout << "expl & lemma: "); nla.m_imp->print_explanation_and_lemma(std::cout << "expl & lemma: ");
ineq i0(lp::lconstraint_kind::EQ, lp::lar_term(), rational(0));
i0.m_term.add_coeff_var(lp_b);
ineq i1(lp::lconstraint_kind::EQ, lp::lar_term(), rational(0));
i1.m_term.add_coeff_var(lp_d);
ineq i2(lp::lconstraint_kind::EQ, lp::lar_term(), rational(0));
i2.m_term.add_coeff_var(lp_e);
bool found0 = false;
bool found1 = false;
bool found2 = false;
for (const auto& k : lemma){
if (k == i0) {
found0 = true;
} else if (k == i1) {
found1 = true;
} else if (k == i2){
found2 = true;
}
}
SASSERT(found0 && found1 && found2);
} }
void solver::test_basic_lemma_for_mon_neutral_from_monomial_to_factors() { void solver::test_basic_lemma_for_mon_neutral_from_monomial_to_factors() {
std::cout << "test_basic_lemma_for_mon_neutral_from_monomial_to_factors\n";
lp::lar_solver s; lp::lar_solver s;
unsigned a = 0, b = 1, c = 2, d = 3, e = 4, unsigned a = 0, b = 1, c = 2, d = 3, e = 4,
abcde = 5, ac = 6, bde = 7, acd = 8, be = 9; abcde = 5, ac = 6, bde = 7, acd = 8, be = 9;
@ -1265,15 +1280,29 @@ void solver::test_basic_lemma_for_mon_neutral_from_monomial_to_factors() {
s.set_column_value(lp_acd, rational(1)); s.set_column_value(lp_acd, rational(1));
s.set_column_value(lp_be, rational(1)); s.set_column_value(lp_be, rational(1));
// set bde te 2, b to minus 2 // set bde to 2, b to minus 2
s.set_column_value(lp_bde, rational(2)); s.set_column_value(lp_bde, rational(2));
s.set_column_value(lp_b, - rational(2)); s.set_column_value(lp_b, - rational(2));
// we have bde = -b, therefore d = +-1 and c = +-1 // we have bde = -b, therefore d = +-1 and e = +-1
SASSERT(nla.m_imp->test_check(lemma, exp) == l_false); SASSERT(nla.m_imp->test_check(lemma, exp) == l_false);
nla.m_imp->print_explanation_and_lemma(std::cout << "expl & lemma: "); nla.m_imp->print_explanation_and_lemma(std::cout << "expl & lemma: ");
ineq i0(lp::lconstraint_kind::EQ, lp::lar_term(), rational(1));
i0.m_term.add_coeff_var(lp_b);
ineq i1(lp::lconstraint_kind::EQ, lp::lar_term(), -rational(1));
i1.m_term.add_coeff_var(lp_b);
bool found0 = false;
bool found1 = false;
for (const auto& k : lemma){
if (k == i0) {
found0 = true;
} else if (k == i1) {
found1 = true;
}
}
SASSERT(found0 && found1);
} }
void solver::test_basic_sign_lemma() { void solver::test_basic_sign_lemma() {
@ -1327,8 +1356,13 @@ void solver::test_basic_sign_lemma() {
lp::explanation exp; lp::explanation exp;
SASSERT(nla.m_imp->test_check(lemma, exp) == l_false); SASSERT(nla.m_imp->test_check(lemma, exp) == l_false);
lp::lar_term t;
t.add_coeff_var(lp_bde);
t.add_coeff_var(lp_acd);
ineq q(lp::lconstraint_kind::EQ, t, rational(0));
nla.m_imp->print_explanation_and_lemma(std::cout << "expl & lemma: "); nla.m_imp->print_explanation_and_lemma(std::cout << "expl & lemma: ");
SASSERT(q == lemma.back());
} }
} }

5
src/util/lp/nla_solver.h
View file

@ -29,7 +29,10 @@ struct ineq {
lp::lconstraint_kind m_cmp; lp::lconstraint_kind m_cmp;
lp::lar_term m_term; lp::lar_term m_term;
rational m_rs; rational m_rs;
ineq(lp::lconstraint_kind cmp, const lp::lar_term& term, const rational& rs) : m_cmp(cmp), m_term(term), m_rs(rs) {} ineq(lp::lconstraint_kind cmp, const lp::lar_term& term, const rational& rs) : m_cmp(cmp), m_term(term), m_rs(rs) {}
bool operator==(const ineq& a) const {
return m_cmp == a.m_cmp && m_term == a.m_term && m_rs == a.m_rs;
}
}; };
typedef vector<ineq> lemma; typedef vector<ineq> lemma;