mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-21 13:23:39 +00:00
Code Activity

fix test_basic_lemma_for_mon_zero_from_factors_to_monomial

Browse source 
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
Lev 2018-10-11 14:03:45 -07:00 • committed by Lev Nachmanson
parent c64abb2351
commit 743e918914
2 changed files with 20 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/test/lp/lp.cpp
View file

@ -3603,14 +3603,14 @@ void test_lp_local(int argn, char**argv) {
if (args_parser.option_is_used("-nla_blnt_mf")) { if (args_parser.option_is_used("-nla_blnt_mf")) {
#ifdef Z3DEBUG #ifdef Z3DEBUG
nla::solver::test_basic_lemma_for_mon_zero_from_monomial_to_factors(); nla::solver::test_basic_lemma_for_mon_neutral_from_monomial_to_factors();
#endif #endif
return finalize(0); return finalize(0);
} }
if (args_parser.option_is_used("-nla_bnt_fm")) { if (args_parser.option_is_used("-nla_bnt_fm")) {
#ifdef Z3DEBUG #ifdef Z3DEBUG
nla::solver::test_basic_lemma_for_mon_zero_from_factors_to_monomial(); nla::solver::test_basic_lemma_for_mon_neutral_from_factors_to_monomial();
#endif #endif
return finalize(0); return finalize(0);
} }

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

@ -1486,6 +1486,7 @@ void solver::test_basic_lemma_for_mon_neutral_from_factors_to_monomial() {
} }
void solver::test_basic_lemma_for_mon_zero_from_factors_to_monomial() { void solver::test_basic_lemma_for_mon_zero_from_factors_to_monomial() {
std::cout << "test_basic_lemma_for_mon_zero_from_factors_to_monomial\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;
@ -1531,8 +1532,8 @@ void solver::test_basic_lemma_for_mon_zero_from_factors_to_monomial() {
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 to zero // set b to zero
s.set_column_value(lp_bde, rational(0)); s.set_column_value(lp_b, rational(0));
SASSERT(nla.m_imp->test_check(lemma, exp) == l_false); SASSERT(nla.m_imp->test_check(lemma, exp) == l_false);
@ -1541,6 +1542,7 @@ void solver::test_basic_lemma_for_mon_zero_from_factors_to_monomial() {
} }
void solver::test_basic_lemma_for_mon_zero_from_monomial_to_factors() { void solver::test_basic_lemma_for_mon_zero_from_monomial_to_factors() {
std::cout << "test_basic_lemma_for_mon_zero_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;
@ -1628,22 +1630,22 @@ void solver::test_basic_lemma_for_mon_neutral_from_monomial_to_factors() {
vector<ineq> lemma; vector<ineq> lemma;
lp::explanation exp; lp::explanation exp;
// set all vars to 0 // set all vars to 1
s.set_column_value(lp_a, rational(0)); s.set_column_value(lp_a, rational(1));
s.set_column_value(lp_b, rational(0));
s.set_column_value(lp_c, rational(0));
s.set_column_value(lp_d, rational(0));
s.set_column_value(lp_e, rational(0));
s.set_column_value(lp_abcde, rational(0));
s.set_column_value(lp_ac, rational(0));
s.set_column_value(lp_bde, rational(0));
s.set_column_value(lp_acd, rational(0));
s.set_column_value(lp_be, rational(0));
// set bde, b, and e to one
s.set_column_value(lp_bde, 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_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 te 2, b to minus 2
s.set_column_value(lp_bde, rational(2));
s.set_column_value(lp_b, - rational(2));
// we have bde = -b, therefore d = +-1 and c = +-1
SASSERT(nla.m_imp->test_check(lemma, exp) == l_false); SASSERT(nla.m_imp->test_check(lemma, exp) == l_false);