add more test stubs

src/test/lp/lp.cpp

@@ -1900,6 +1900,8 @@ void setup_args_parser(argument_parser & parser) {
     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("-nla_blnt_mf", "test_basic_lemma_for_mon_neutral_from_monomial_to_factors");
+    parser.add_option_with_help_string("-nla_blnt_fm", "test_basic_lemma_for_mon_neutral_from_factors_to_monomial");
     parser.add_option_with_help_string("-hnf", "test hermite normal form");
     parser.add_option_with_help_string("-gomory", "gomory");
     parser.add_option_with_help_string("-intd", "test integer_domain");
@@ -3587,7 +3589,7 @@ void test_lp_local(int argn, char**argv) {
 
     if (args_parser.option_is_used("-nla_blfmz_mf")) { 
 #ifdef Z3DEBUG
-        nla::solver::test_basic_lemma_for_mon_zero_from_monomial_to_factor();
+        nla::solver::test_basic_lemma_for_mon_zero_from_monomial_to_factors();
 #endif
         return finalize(0);
     }
@@ -3599,7 +3601,20 @@ void test_lp_local(int argn, char**argv) {
         return finalize(0);
     }
 
-    
+    if (args_parser.option_is_used("-nla_blnt_mf")) { 
+#ifdef Z3DEBUG
+        nla::solver::test_basic_lemma_for_mon_zero_from_monomial_to_factors();
+#endif
+        return finalize(0);
+    }
+
+    if (args_parser.option_is_used("-nla_bnt_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
         test_hnf();

src/util/lp/nla_solver.cpp

@@ -1104,18 +1104,28 @@ struct solver::imp {
     }
 
     
-    bool basic_lemma_for_mon_zero(lpvar i_mon, const factorization& factorization) {
+    bool basic_lemma_for_mon_zero(unsigned i_mon, const factorization& factorization) {
         return 
             basic_lemma_for_mon_zero_from_monomial_to_factor(i_mon, factorization) || 
             basic_lemma_for_mon_zero_from_factors_to_monomial(i_mon, factorization);
     }
-            
+
-    bool basic_lemma_for_mon_neutral(const factorization& factorization) {
+    bool basic_lemma_for_mon_neutral_monomial_to_factor(unsigned i_mon, const factorization& factorization) {
-        // NOT_IMPLEMENTED_YET();
+        return false;
+    }
+
+    bool basic_lemma_for_mon_neutral_from_factors_to_monomial(unsigned i_mon, const factorization& factorization) {
+        return false;
+    }
+    
+    bool basic_lemma_for_mon_neutral(unsigned i_mon, const factorization& factorization) {
+        return
+            basic_lemma_for_mon_neutral_monomial_to_factor(i_mon, factorization) || 
+            basic_lemma_for_mon_neutral_from_factors_to_monomial(i_mon, factorization);
         return false;
     }
             
-    bool basic_lemma_for_mon_proportionality(const factorization& factorization) {
+    bool basic_lemma_for_mon_proportionality(unsigned i_mon, const factorization& factorization) {
         // NOT_IMPLEMENTED_YET();
         return false;
     }
@@ -1125,8 +1135,8 @@ struct solver::imp {
     bool basic_lemma_for_mon(unsigned i_mon) {
         for (auto factorization : factorization_factory_imp(i_mon, *this)) {
             if (basic_lemma_for_mon_zero(i_mon, factorization) ||
-                basic_lemma_for_mon_neutral(factorization) ||
+                basic_lemma_for_mon_neutral(i_mon, factorization) ||
-                basic_lemma_for_mon_proportionality(factorization))
+                basic_lemma_for_mon_proportionality(i_mon, factorization))
                 return true;
             
         }
@@ -1295,29 +1305,7 @@ struct solver::imp {
         SASSERT(found_factorizations == number_of_factorizations);
     }
     
-    lbool test_basic_sign_lemma_with_constraints(
+    lbool test_check(
-        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_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 )
     {
@@ -1442,7 +1430,7 @@ void solver::test_factorization() {
     
 }
 
-void solver::test_basic_lemma_for_mon_zero_from_monomial_to_factor() {
+void solver::test_basic_lemma_for_mon_neutral_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;
@@ -1491,7 +1479,7 @@ void solver::test_basic_lemma_for_mon_zero_from_monomial_to_factor() {
     // 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);
+    SASSERT(nla.m_imp->test_check(lemma, exp) == l_false);
     
     nla.m_imp->print_explanation_and_lemma(std::cout << "expl & lemma: ");
     
@@ -1530,6 +1518,116 @@ void solver::test_basic_lemma_for_mon_zero_from_factors_to_monomial() {
     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_check(lemma, exp) == l_false);
+    
+    nla.m_imp->print_explanation_and_lemma(std::cout << "expl & lemma: ");
+    
+}
+
+void solver::test_basic_lemma_for_mon_zero_from_monomial_to_factors() {
+    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_check(lemma, exp) == l_false);
+    
+    nla.m_imp->print_explanation_and_lemma(std::cout << "expl & lemma: ");
+    
+}
+
+void solver::test_basic_lemma_for_mon_neutral_from_monomial_to_factors() {
+    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 0
     s.set_column_value(lp_a, rational(0));
     s.set_column_value(lp_b, rational(0));
@@ -1542,10 +1640,12 @@ void solver::test_basic_lemma_for_mon_zero_from_factors_to_monomial() {
     s.set_column_value(lp_acd, rational(0));
     s.set_column_value(lp_be, rational(0));
 
-    // set bde to one
+    // 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_e, rational(1));
     
-    SASSERT(nla.m_imp->test_basic_lemma_for_mon_zero_from_factors_to_monomial(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: ");
     
@@ -1606,7 +1706,7 @@ void solver::test_basic_sign_lemma_with_constraints() {
     vector<ineq> lemma;
     lp::explanation exp;
     
-    SASSERT(nla.m_imp->test_basic_sign_lemma_with_constraints(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: ");
     

src/util/lp/nla_solver.h

@@ -48,7 +48,9 @@ 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_monomial_to_factors();
     static void test_basic_lemma_for_mon_zero_from_factors_to_monomial();
+    static void test_basic_lemma_for_mon_neutral_from_monomial_to_factors();
+    static void test_basic_lemma_for_mon_neutral_from_factors_to_monomial();
 };
 }