From 9eee544366e88f0b747d85ab31cbb9bd0c6c7bdf Mon Sep 17 00:00:00 2001
From: Lev <levnach@hotmail.com>
Date: Wed, 10 Oct 2018 12:18:13 -0700
Subject: [PATCH] add a unit test
basic_lemma_for_mon_zero_from_monomial_to_factor
Signed-off-by: Lev <levnach@hotmail.com>
---
src/test/lp/lp.cpp | 16 +++++
src/util/lp/nla_solver.cpp | 130 +++++++++++++++++++++++++++++++++++--
src/util/lp/nla_solver.h | 3 +-
3 files changed, 142 insertions(+), 7 deletions(-)
diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp
index db5346d79..cfd9f28cf 100644
--- a/src/test/lp/lp.cpp
+++ b/src/test/lp/lp.cpp
@@ -1896,6 +1896,8 @@ void test_replace_column() {
void setup_args_parser(argument_parser & parser) {
+ parser.add_option_with_help_string("-nla_blfmz_mf", "test_basic_lemma_for_mon_zero_from_factor_to_monomial");
+ parser.add_option_with_help_string("-nla_blfmz_fm", "test_basic_lemma_for_mon_zero_from_monomials_to_factor");
parser.add_option_with_help_string("-nla_fact", "test nla_solver");
parser.add_option_with_help_string("-nla_bslwct", "test_basic_sign_lemma_with_constraints");
parser.add_option_with_help_string("-hnf", "test hermite normal form");
@@ -3583,6 +3585,20 @@ void test_lp_local(int argn, char**argv) {
return finalize(0);
}
+ if (args_parser.option_is_used("-nla_blfmz_mf")) {
+#ifdef Z3DEBUG
+ nla::solver::test_basic_lemma_for_mon_zero_from_monomial_to_factor();
+#endif
+ return finalize(0);
+ }
+
+ if (args_parser.option_is_used("-nla_blfmz_fm")) {
+#ifdef Z3DEBUG
+ nla::solver::test_basic_lemma_for_mon_zero_from_factors_to_monomial();
+#endif
+ return finalize(0);
+ }
+
if (args_parser.option_is_used("-hnf")) {
#ifdef Z3DEBUG
diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp
index 250ae4c4c..57a48d40e 100644
--- a/src/util/lp/nla_solver.cpp
+++ b/src/util/lp/nla_solver.cpp
@@ -1038,15 +1038,16 @@ struct solver::imp {
// here we use the fact
// xy = 0 -> x = 0 or y = 0
- bool basic_lemma_for_mon_zero_from_monomial_to_factor(lpvar i_mon, const factorization& factorization) {
- if (!vvr(i_mon).is_zero() )
+ bool basic_lemma_for_mon_zero_from_monomial_to_factor(unsigned i_mon, const factorization& factorization) {
+ lpvar mon_var = m_monomials[i_mon].var();
+ if (!vvr(mon_var).is_zero() )
return false;
for (lpvar j : factorization) {
if (vvr(j).is_zero())
return false;
}
lp::lar_term t;
- t.add_coeff_var(rational::one(), i_mon);
+ t.add_coeff_var(rational::one(), mon_var);
SASSERT(m_lemma->empty());
m_lemma->push_back(ineq(lp::lconstraint_kind::NE, t, rational::zero()));
for (lpvar j : factorization) {
@@ -1069,7 +1070,7 @@ struct solver::imp {
}
bool basic_lemma_for_mon_zero_from_factors_to_monomial(lpvar i_mon, const factorization& factorization) {
- NOT_IMPLEMENTED_YET();
+ // NOT_IMPLEMENTED_YET();
return false;
}
@@ -1081,12 +1082,12 @@ struct solver::imp {
}
bool basic_lemma_for_mon_neutral(const factorization& factorization) {
- NOT_IMPLEMENTED_YET();
+ // NOT_IMPLEMENTED_YET();
return false;
}
bool basic_lemma_for_mon_proportionality(const factorization& factorization) {
- NOT_IMPLEMENTED_YET();
+ // NOT_IMPLEMENTED_YET();
return false;
}
@@ -1275,6 +1276,28 @@ struct solver::imp {
return check(exp, lemma);
}
+
+ lbool test_basic_lemma_for_mon_zero_from_monomial_to_factor(
+ vector<ineq>& lemma,
+ lp::explanation& exp )
+ {
+ m_lar_solver.set_status(lp::lp_status::OPTIMAL);
+ m_lemma = & lemma;
+ m_expl = & exp;
+
+ return check(exp, lemma);
+ }
+
+ lbool test_basic_lemma_for_mon_zero_from_factors_to_monomial(
+ vector<ineq>& lemma,
+ lp::explanation& exp )
+ {
+ m_lar_solver.set_status(lp::lp_status::OPTIMAL);
+ m_lemma = & lemma;
+ m_expl = & exp;
+
+ return check(exp, lemma);
+ }
}; // end of imp
@@ -1389,6 +1412,101 @@ void solver::test_factorization() {
}
+
+void solver::test_basic_lemma_for_mon_zero_from_monomial_to_factor() {
+ lp::lar_solver s;
+ unsigned a = 0, b = 1, c = 2, d = 3, e = 4,
+ abcde = 5, ac = 6, bde = 7, acd = 8, be = 9;
+ lpvar lp_a = s.add_var(a, true);
+ lpvar lp_b = s.add_var(b, true);
+ lpvar lp_c = s.add_var(c, true);
+ lpvar lp_d = s.add_var(d, true);
+ lpvar lp_e = s.add_var(e, true);
+ lpvar lp_abcde = s.add_var(abcde, true);
+ lpvar lp_ac = s.add_var(ac, true);
+ lpvar lp_bde = s.add_var(bde, true);
+ lpvar lp_acd = s.add_var(acd, true);
+ lpvar lp_be = s.add_var(be, true);
+
+ reslimit l;
+ params_ref p;
+ solver nla(s, l, p);
+
+ create_abcde(nla,
+ lp_a,
+ lp_b,
+ lp_c,
+ lp_d,
+ lp_e,
+ lp_abcde,
+ lp_ac,
+ lp_bde,
+ lp_acd,
+ lp_be);
+ vector<ineq> lemma;
+ 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_c, rational(1));
+ s.set_column_value(lp_d, 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
+ s.set_column_value(lp_bde, rational(0));
+
+ SASSERT(nla.m_imp->test_basic_lemma_for_mon_zero_from_monomial_to_factor(lemma, exp) == l_false);
+
+ nla.m_imp->print_explanation_and_lemma(std::cout << "expl & lemma: ");
+
+}
+
+void solver::test_basic_lemma_for_mon_zero_from_factors_to_monomial() {
+ lp::lar_solver s;
+ unsigned a = 0, b = 1, c = 2, d = 3, e = 4,
+ abcde = 5, ac = 6, bde = 7, acd = 8, be = 9;
+ lpvar lp_a = s.add_var(a, true);
+ lpvar lp_b = s.add_var(b, true);
+ lpvar lp_c = s.add_var(c, true);
+ lpvar lp_d = s.add_var(d, true);
+ lpvar lp_e = s.add_var(e, true);
+ lpvar lp_abcde = s.add_var(abcde, true);
+ lpvar lp_ac = s.add_var(ac, true);
+ lpvar lp_bde = s.add_var(bde, true);
+ lpvar lp_acd = s.add_var(acd, true);
+ lpvar lp_be = s.add_var(be, true);
+
+ reslimit l;
+ params_ref p;
+ solver nla(s, l, p);
+
+ create_abcde(nla,
+ lp_a,
+ lp_b,
+ lp_c,
+ lp_d,
+ lp_e,
+ lp_abcde,
+ lp_ac,
+ lp_bde,
+ lp_acd,
+ lp_be);
+ vector<ineq> lemma;
+ lp::explanation exp;
+
+ SASSERT(nla.m_imp->test_basic_lemma_for_mon_zero_from_factors_to_monomial(lemma, exp) == l_false);
+
+ nla.m_imp->print_explanation_and_lemma(std::cout << "expl & lemma: ");
+
+}
+
void solver::test_basic_sign_lemma_with_constraints() {
lp::lar_solver s;
unsigned a = 0, b = 1, c = 2, d = 3, e = 4,
diff --git a/src/util/lp/nla_solver.h b/src/util/lp/nla_solver.h
index 199d689e6..0f3ff27a5 100644
--- a/src/util/lp/nla_solver.h
+++ b/src/util/lp/nla_solver.h
@@ -48,6 +48,7 @@ public:
lbool check(lp::explanation&, lemma&);
static void test_factorization();
static void test_basic_sign_lemma_with_constraints();
-
+ static void test_basic_lemma_for_mon_zero_from_monomial_to_factor();
+ static void test_basic_lemma_for_mon_zero_from_factors_to_monomial();
};
}