change the signature of nla_solver::check() to accept lemma and explanation as vectors

Signed-off-by: Lev <levnach@hotmail.com>

src/smt/theory_lra.cpp

@@ -2145,37 +2145,46 @@ public:
         return term;
     }
 
-    lbool check_aftermath_nla(lbool r) {
+    void false_case_of_check_nla() {
-        switch (r) {
+        literal_vector core;
-        case l_false: {            
+        for (auto const& ineq : m_lemma) {
-            literal_vector core;
+            bool is_lower = true, pos = true, is_eq = false;
-            for (auto const& ineq : m_lemma) {
+            switch (ineq.m_cmp) {
-                bool is_lower = true, pos = true, is_eq = false;
+            case lp::LE: is_lower = false; pos = false;  break;
-                
+            case lp::LT: is_lower = true;  pos = true; break;
-                switch (ineq.m_cmp) {
+            case lp::GE: is_lower = true;  pos = false;  break;
-                case lp::LE: is_lower = false; pos = false;  break;
+            case lp::GT: is_lower = false; pos = true; break;
-                case lp::LT: is_lower = true;  pos = true; break;
+            case lp::EQ: is_eq = true; pos = false; break;
-                case lp::GE: is_lower = true;  pos = false;  break;
+            case lp::NE: is_eq = true; pos = true; break;
-                case lp::GT: is_lower = false; pos = true; break;
+            default: UNREACHABLE();
-                case lp::EQ: is_eq = true; pos = false; break;
+            }
-                case lp::NE: is_eq = true; pos = true; break;
+            TRACE("arith", tout << "is_lower: " << is_lower << " pos " << pos << "\n";);
-                default: UNREACHABLE();
+            app_ref atom(m);
-                }
+            // TBD utility: lp::lar_term term = mk_term(ineq.m_poly);
-                TRACE("arith", tout << "is_lower: " << is_lower << " pos " << pos << "\n";);
+            // then term is used instead of ineq.m_term
-                app_ref atom(m);
+            if (is_eq) {
-                // TBD utility: lp::lar_term term = mk_term(ineq.m_poly);
+                atom = mk_eq(ineq.m_term, ineq.m_rs);
-                // then term is used instead of ineq.m_term
+            }
-                if (is_eq) {
+            else {
-                    atom = mk_eq(ineq.m_term, ineq.m_rs);
+                // create term >= 0 (or term <= 0)
-                }
+                atom = mk_bound(ineq.m_term, ineq.m_rs, is_lower);
-                else {
+            }
-                    // create term >= 0 (or term <= 0)
+            literal lit(ctx().get_bool_var(atom), pos);
-                    atom = mk_bound(ineq.m_term, ineq.m_rs, is_lower);
+            core.push_back(~lit);
-                }
+        }
-                literal lit(ctx().get_bool_var(atom), pos);
+        set_conflict_or_lemma(core, false);
-                core.push_back(~lit);
+    }
+    
+    lbool check_aftermath_nla(lbool r, const vector<nla::lemma>& l,
+        const vector<lp::explanation>& e) {
+        switch (r) {
+        case l_false: {
+            SASSERT(l.size() == e.size());
+            for(unsigned i = 0; i < l.size(); i++) {
+                m_lemma = l[i];
+                m_explanation = e[i];
+                false_case_of_check_nla();
             }
-            set_conflict_or_lemma(core, false);
             break;
         }
         case l_true:
@@ -2198,9 +2207,13 @@ public:
         if (!m_nra && !m_nla) return l_true;
         if (!m_switcher.need_check()) return l_true;
         m_a1 = nullptr; m_a2 = nullptr;
-        m_explanation.clear();
+        if (m_nra) {
-        lbool r = m_nra? m_nra->check(m_explanation): m_nla->check(m_explanation, m_lemma);
+            m_explanation.clear();
-        return m_nra? check_aftermath_nra(r) : check_aftermath_nla(r);
+            return check_aftermath_nra(m_nra->check(m_explanation));
+        }
+        vector<nla::lemma> l;
+        vector<lp::explanation> e;
+        return check_aftermath_nla(m_nla->check(e, l), l, e);
     }
 
     /**

src/test/lp/lp.cpp

@@ -1901,6 +1901,7 @@ void setup_args_parser(argument_parser & parser) {
     parser.add_option_with_help_string("-nla_fact", "test nla_solver factorization");
     parser.add_option_with_help_string("-nla_order", "test nla_solver order lemma");
     parser.add_option_with_help_string("-nla_monot", "test nla_solver order lemma");
+    parser.add_option_with_help_string("-nla_tan", "test_tangent_lemma");
     parser.add_option_with_help_string("-nla_bsl", "test_basic_sign_lemma");
     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");
@@ -3612,6 +3613,13 @@ void test_lp_local(int argn, char**argv) {
         return finalize(0);
     }
 
+    if (args_parser.option_is_used("-nla_tan")) { 
+#ifdef Z3DEBUG
+        nla::solver::test_tangent_lemma();
+#endif
+        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_factors();

src/util/lp/equiv_monomials.h

@@ -19,93 +19,93 @@
   --*/
 namespace nla {
 struct const_iterator_equiv_mon {
-        // fields
+    // fields
-        vector<const unsigned_vector*>                      m_same_abs_vals;
+    vector<const unsigned_vector*>                      m_same_abs_vals;
-        vector<unsigned_vector::const_iterator>             m_its;
+    vector<unsigned_vector::const_iterator>             m_its;
-        bool                                                m_done;
+    bool                                                m_done;
-        std::function<unsigned (const unsigned_vector&)>    m_find_monomial;
+    std::function<unsigned (const unsigned_vector&)>    m_find_monomial;
-        // constructor for begin()
+    // constructor for begin()
-        const_iterator_equiv_mon(vector<const unsigned_vector*> abs_vals,
+    const_iterator_equiv_mon(vector<const unsigned_vector*> abs_vals,
-                                 std::function<unsigned (const unsigned_vector&)> find_monomial)
+                             std::function<unsigned (const unsigned_vector&)> find_monomial)
-            : m_same_abs_vals(abs_vals),
+        : m_same_abs_vals(abs_vals),
-              m_done(false),
+          m_done(false),
-              m_find_monomial(find_monomial) {
+          m_find_monomial(find_monomial) {
-            for (auto it: abs_vals){
+        for (auto it: abs_vals){
-                m_its.push_back(it->begin());
+            m_its.push_back(it->begin());
+        }
+    }
+    // constructor for end()
+    const_iterator_equiv_mon() : m_done(true) {}
+        
+    //typedefs
+    typedef const_iterator_equiv_mon self_type;
+    typedef unsigned value_type;
+    typedef unsigned reference;
+    typedef int difference_type;
+    typedef std::forward_iterator_tag iterator_category;
+
+    void advance() {
+        if (m_done)
+            return;
+        unsigned k = 0;
+        for (; k < m_its.size(); k++) {
+            auto & it = m_its[k];
+            it++;
+            const auto & evars = *(m_same_abs_vals[k]);
+            if (it == evars.end()) {
+                it = evars.begin();
+            } else {
+                break;
             }
         }
-        // constructor for end()
-        const_iterator_equiv_mon() : m_done(true) {}
-        
-        //typedefs
-        typedef const_iterator_equiv_mon self_type;
-        typedef unsigned value_type;
-        typedef unsigned reference;
-        typedef int difference_type;
-        typedef std::forward_iterator_tag iterator_category;
-
-        void advance() {
-            if (m_done)
-                return;
-            unsigned k = 0;
-            for (; k < m_its.size(); k++) {
-                auto & it = m_its[k];
-                it++;
-                const auto & evars = *(m_same_abs_vals[k]);
-                if (it == evars.end()) {
-                    it = evars.begin();
-                } else {
-                    break;
-                }
-            }
             
-            if (k == m_its.size()) {
+        if (k == m_its.size()) {
-                m_done = true;
+            m_done = true;
-            }
         }
+    }
 
-        unsigned_vector get_key() const {
+    unsigned_vector get_key() const {
-            unsigned_vector r;
+        unsigned_vector r;
-            for(const auto& it : m_its){
+        for(const auto& it : m_its){
-                r.push_back(*it);
+            r.push_back(*it);
-            }
-            std::sort(r.begin(), r.end());
-            return r;
         }
+        std::sort(r.begin(), r.end());
+        return r;
+    }
         
-        self_type operator++() {self_type i = *this; operator++(1); return i;}
+    self_type operator++() {self_type i = *this; operator++(1); return i;}
-        self_type operator++(int) { advance(); return *this; }
+    self_type operator++(int) { advance(); return *this; }
 
-        bool operator==(const self_type &other) const { return m_done == other.m_done;}
+    bool operator==(const self_type &other) const { return m_done == other.m_done;}
-        bool operator!=(const self_type &other) const { return ! (*this == other); }
+    bool operator!=(const self_type &other) const { return ! (*this == other); }
-        reference operator*() const {
+    reference operator*() const {
-            return m_find_monomial(get_key());
+        return m_find_monomial(get_key());
-        }
+    }
-    };
+};
 
-    struct equiv_monomials {
+struct equiv_monomials {
-        const monomial &                                    m_mon;
+    const monomial &                                    m_mon;
-        std::function<const unsigned_vector*(lpvar)>        m_abs_eq_vars;
+    std::function<const unsigned_vector*(lpvar)>        m_abs_eq_vars;
-        std::function<unsigned (const unsigned_vector&)>    m_find_monomial;
+    std::function<unsigned (const unsigned_vector&)>    m_find_monomial;
-        equiv_monomials(const monomial & m,
+    equiv_monomials(const monomial & m,
-                        std::function<const unsigned_vector*(lpvar)> abs_eq_vars,
+                    std::function<const unsigned_vector*(lpvar)> abs_eq_vars,
-                        std::function<unsigned (const unsigned_vector&)> find_monomial) :
+                    std::function<unsigned (const unsigned_vector&)> find_monomial) :
-                            m_mon(m),
+        m_mon(m),
-                            m_abs_eq_vars(abs_eq_vars),
+        m_abs_eq_vars(abs_eq_vars),
-                            m_find_monomial(find_monomial) {}
+        m_find_monomial(find_monomial) {}
 
-        vector<const unsigned_vector*> vars_eqs() const {
+    vector<const unsigned_vector*> vars_eqs() const {
-            vector<const unsigned_vector*> r;
+        vector<const unsigned_vector*> r;
-            for(lpvar j : m_mon.vars()) {
+        for(lpvar j : m_mon.vars()) {
-                r.push_back(m_abs_eq_vars(j));
+            r.push_back(m_abs_eq_vars(j));
-            }
-            return r;
-        } 
-        const_iterator_equiv_mon begin() const {
-            return const_iterator_equiv_mon(vars_eqs(), m_find_monomial);
         }
-        const_iterator_equiv_mon end() const {
+        return r;
-            return const_iterator_equiv_mon();
+    } 
-        }
+    const_iterator_equiv_mon begin() const {
-    };
+        return const_iterator_equiv_mon(vars_eqs(), m_find_monomial);
+    }
+    const_iterator_equiv_mon end() const {
+        return const_iterator_equiv_mon();
+    }
+};
 } // end of namespace nla

src/util/lp/nla_solver.cpp

@@ -30,6 +30,42 @@ namespace nla {
 typedef lp::lconstraint_kind llc;
 
 struct solver::imp {
+    struct fr_interval {
+        rational m_l;
+        rational m_u;
+        fr_interval() {}
+        fr_interval(const rational& l, const rational& u) : m_l(l), m_u(u) {
+            SASSERT(l <= u);
+        }
+    };
+    
+    struct frontier {
+        fr_interval m_intervals[2];
+    };
+
+    struct binfac {
+        lpvar x, y;
+        binfac() {}
+        binfac(lpvar a, lpvar b) {
+            if (a < b) {
+                x = a; y = b;
+            } else {
+                x = b; y = a;
+            }
+        }
+        bool operator==(const binfac& b) const {
+            return x == b.x && y == b.y;
+        } 
+    };
+    struct hash_binfac {
+        inline size_t operator()(const binfac& b) const {
+            size_t seed = 0;
+            hash_combine(seed, b.x);
+            hash_combine(seed, b.y);
+            return seed;
+        }
+    };
+
     //fields    
     vars_equivalence                                                 m_vars_equivalence;
     vector<monomial>                                                 m_monomials;
@@ -42,12 +78,15 @@ struct solver::imp {
     
     // m_var_to_its_monomial[m_monomials[i].var()] = i
     std::unordered_map<lpvar, unsigned>                              m_var_to_its_monomial;
+    vector<lp::explanation>  *                                       m_expl_vec;                                  
     lp::explanation *                                                m_expl;
+    vector<lemma> *                                                  m_lemma_vec;
     lemma *                                                          m_lemma;
     unsigned_vector                                                  m_to_refine;
     std::unordered_map<unsigned_vector, unsigned, hash_svector>      m_mkeys; // the key is the sorted vars of a monomial
-
+    std::unordered_map<binfac, frontier, hash_binfac>             m_tang_frontier;   
-
+    
+    
     unsigned find_monomial(const unsigned_vector& k) const {
         TRACE("nla_solver", tout << "k = "; print_product_with_vars(k, tout););
         auto it = m_mkeys.find(k);
@@ -72,7 +111,6 @@ struct solver::imp {
         // m_params(p)
     {
     }
-
     
     bool compare_holds(const rational& ls, llc cmp, const rational& rs) const {
         switch(cmp) {
@@ -118,7 +156,7 @@ struct solver::imp {
 
     rational vvr(const rooted_mon& rm) const { return vvr(m_monomials[rm.m_orig.m_i].var()) * rm.m_orig.m_sign; }
 
-    rational vvr(const factor& f) const { return f.is_var()? vvr(f.index()) : vvr(m_rm_table.vec()[f.index()]); }
+    rational vvr(const factor& f) const { return vvr(var(f)); }
 
     lpvar var(const factor& f) const {
         return f.is_var()?
@@ -188,9 +226,10 @@ struct solver::imp {
     }
 
     rational mon_value_by_vars(unsigned i) const {
-        return mon_value_by_vars(m_monomials[i]);
+        return product_value(m_monomials[i]);
     }
-    rational mon_value_by_vars(const monomial & m) const {
+    template <typename T>
+    rational product_value(const T & m) const {
         rational r(1);
         for (auto j : m) {
             r *= m_lar_solver.get_column_value_rational(j);
@@ -201,7 +240,7 @@ struct solver::imp {
     // return true iff the monomial value is equal to the product of the values of the factors
     bool check_monomial(const monomial& m) const {
         SASSERT(m_lar_solver.get_column_value(m.var()).is_int());
-        return mon_value_by_vars(m) == m_lar_solver.get_column_value_rational(m.var());
+        return product_value(m) == m_lar_solver.get_column_value_rational(m.var());
     }
     
     void explain(const monomial& m) const {
@@ -259,6 +298,22 @@ struct solver::imp {
         return out;
     }
 
+    std::ostream& print_fr_interval(const fr_interval& m, std::ostream& out) const {
+        out << "(" << m.m_l <<  ", " << m.m_u << ")";
+        return out;
+    }
+    
+    std::ostream& print_frontier(const frontier& m, std::ostream& out) const {
+        out << "("; print_fr_interval(m.m_intervals[0], out);
+        out <<  ", "; print_fr_interval(m.m_intervals[1], out); out <<  ")";
+        return out;
+    }
+
+    std::ostream& print_binfac(const binfac& m, std::ostream& out) const {
+        out << "( x = "; print_var(m.x, out); out <<  ", y = "; print_var(m.y, out); out <<  ")";
+        return out;
+    }
+
     std::ostream& print_monomial(unsigned i, std::ostream& out) const {
         return print_monomial(m_monomials[i], out);
     }
@@ -1223,6 +1278,7 @@ struct solver::imp {
         m_monomials_containing_var.clear();
         m_expl->clear();
         m_lemma->clear();
+        m_tang_frontier.clear();
     }
     
     void init_search() {
@@ -1552,7 +1608,6 @@ struct solver::imp {
         out <<  "}";
     }
     
-    
     // Returns rooted monomials by arity
     std::unordered_map<unsigned, unsigned_vector> get_rm_by_arity() {
         std::unordered_map<unsigned, unsigned_vector> m;
@@ -1789,14 +1844,77 @@ struct solver::imp {
         return false;
     }
 
-    bool tangent_lemma() {
+    bool find_binfac_on_monomial(const rooted_mon& rm, binfac & bf) {
+        for (auto factorization : factorization_factory_imp(rm.m_vars, *this)) {
+            if (factorization.size() == 2) {
+                lpvar a = var(factorization[0]);
+                lpvar b = var(factorization[1]);
+                if (vvr(rm) != vvr(a) * vvr(b)) {
+                    bf = binfac(a, b);
+                    return true;
+                }
+            }
+        }
         return false;
     }
     
-    lbool check(lp::explanation & exp, lemma& l) {
+    bool find_binfac_to_refine(binfac& bf){
+        for (const auto& rm : m_rm_table.vec()) {
+            if (check_monomial(m_monomials[rm.orig_index()]))
+                continue;
+            if (find_binfac_on_monomial(rm, bf)) {
+                TRACE("nla_solver", tout << "found binfac"; print_binfac(bf, tout);
+                      tout << " product = " << vvr(rm) << ", but should be =" << vvr(bf.x)*vvr(bf.y)<< "\n"; );
+                return true;
+            } 
+        }
+        return false;
+    }
+    
+    bool tangent_lemma() {
+        return false;
+        binfac bf;
+        if (!find_binfac_to_refine(bf)) {
+            return false;
+        }
+        return tangent_lemma_bf(bf);
+    }
+
+    bool tangent_lemma_bf(const binfac& bf){
+        auto& fr = get_frontier(bf);
+        TRACE("nla_solver", tout << "front = "; print_frontier(fr, tout); tout << std::endl;);
+        SASSERT(false);
+        return false;
+    }
+
+    frontier get_initial_frontier(const binfac& bf) const {
+        frontier f;
+        rational a = vvr(bf.x);
+        f.m_intervals[0] = fr_interval(a - rational(1), a + rational(1));
+        rational b = vvr(bf.y);
+        f.m_intervals[1] = fr_interval(b - rational(1), b + rational(1));
+        return f;
+    }
+    
+    frontier& get_frontier(const binfac& bf) {
+        auto it = m_tang_frontier.find(bf);
+        if (it != m_tang_frontier.end()){
+            SASSERT(false);
+        } else {
+            it = m_tang_frontier.insert(it, std::make_pair(bf, get_initial_frontier(bf)));
+        }
+        return it->second;
+    }
+    
+    lbool check(vector<lp::explanation> & expl_vec, vector<lemma>& l_vec) {
+        
         TRACE("nla_solver", tout << "check of nla";);
-        m_expl =   &exp;
+        m_expl_vec =   &expl_vec;
-        m_lemma =  &l;
+        m_lemma_vec =  &l_vec;
+        m_expl_vec->push_back(lp::explanation());
+        m_expl = m_expl_vec->begin();
+        m_lemma_vec->push_back(lemma());
+        m_lemma = m_lemma_vec->begin();
        
         if (!(m_lar_solver.get_status() == lp::lp_status::OPTIMAL || m_lar_solver.get_status() == lp::lp_status::FEASIBLE )) {
             TRACE("nla_solver", tout << "unknown because of the m_lar_solver.m_status = " << lp_status_to_string(m_lar_solver.get_status()) << "\n";);
@@ -1820,11 +1938,7 @@ struct solver::imp {
                     ret = l_false;
                 }
             } else { // search_level == 3
-                if (monotonicity_lemma()) {
+                if (monotonicity_lemma() || tangent_lemma()) {
-                    ret = l_false;
-                }
-                                
-                if (tangent_lemma()) {
                     ret = l_false;
                 }
             }
@@ -1860,13 +1974,10 @@ struct solver::imp {
     }
     
     lbool test_check(
-        vector<ineq>& lemma,
+        vector<vector<ineq>>& lemma,
-        lp::explanation& exp )
+        vector<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
@@ -1878,7 +1989,7 @@ unsigned solver::add_monomial(lpvar v, unsigned sz, lpvar const* vs) {
 
 bool solver::need_check() { return true; }
 
-lbool solver::check(lp::explanation & ex, lemma& l) {
+lbool solver::check(vector<lp::explanation> & ex, vector<lemma>& l) {
     return m_imp->check(ex, l);
 }
 
@@ -2016,8 +2127,8 @@ void solver::test_basic_lemma_for_mon_neutral_from_factors_to_monomial_0() {
     v.push_back(lp_a);v.push_back(lp_c);
     nla.add_monomial(lp_ac, v.size(), v.begin());
      
-    vector<ineq> lemma;
+    vector<lemma> lemma;
-    lp::explanation exp;
+    vector<lp::explanation> exp;
 
     // set abcde = ac * bde
     // ac = 1 then abcde = bde, but we have abcde < bde
@@ -2046,7 +2157,7 @@ void solver::test_basic_lemma_for_mon_neutral_from_factors_to_monomial_0() {
     bool found0 = false;
     bool found1 = false;
     bool found2 = false;
-    for (const auto& k : lemma){
+    for (const auto& k : lemma[0]){
         if (k == i0) {
             found0 = true;
         } else if (k == i1) {
@@ -2080,8 +2191,8 @@ void solver::test_basic_lemma_for_mon_neutral_from_factors_to_monomial_1() {
     svector<lpvar> v; v.push_back(lp_b);v.push_back(lp_d);v.push_back(lp_e);
     nla.add_monomial(lp_bde, v.size(), v.begin());
 
-    vector<ineq> lemma;
+    vector<lemma> lemma;
-    lp::explanation exp;
+    vector<lp::explanation> exp;
 
     s.set_column_value(lp_a, rational(1));
     s.set_column_value(lp_b, rational(1));
@@ -2091,7 +2202,7 @@ void solver::test_basic_lemma_for_mon_neutral_from_factors_to_monomial_1() {
     s.set_column_value(lp_bde, rational(3));
 
     SASSERT(nla.m_imp->test_check(lemma, exp) == l_false);
-    SASSERT(lemma.size() == 4);
+    SASSERT(lemma[0].size() == 4);
     nla.m_imp->print_lemma(std::cout << "expl & lemma: ");
 
     ineq i0(llc::NE, lp::lar_term(), rational(1));
@@ -2106,7 +2217,7 @@ void solver::test_basic_lemma_for_mon_neutral_from_factors_to_monomial_1() {
     bool found1 = false;
     bool found2 = false;
     bool found3 = false;
-    for (const auto& k : lemma){
+    for (const auto& k : lemma[0]){
         if (k == i0) {
             found0 = true;
         } else if (k == i1) {
@@ -2154,8 +2265,8 @@ void solver::test_basic_lemma_for_mon_zero_from_factors_to_monomial() {
                  lp_bde,
                  lp_acd,
                  lp_be);
-    vector<ineq> lemma;
+    vector<lemma> lemma;
-    lp::explanation exp;
+    vector<lp::explanation> exp;
 
 
     // set vars
@@ -2172,7 +2283,7 @@ void solver::test_basic_lemma_for_mon_zero_from_factors_to_monomial() {
 
     SASSERT(nla.m_imp->test_check(lemma, exp) == l_false);
     nla.m_imp->print_lemma(std::cout << "expl & lemma: ");
-    SASSERT(lemma.size() == 2);
+    SASSERT(lemma.size() == 1 && lemma[0].size() == 2);
     ineq i0(llc::NE, lp::lar_term(), rational(0));
     i0.m_term.add_coeff_var(lp_b);
     ineq i1(llc::EQ, lp::lar_term(), rational(0));
@@ -2180,7 +2291,7 @@ void solver::test_basic_lemma_for_mon_zero_from_factors_to_monomial() {
     bool found0 = false;
     bool found1 = false;
 
-    for (const auto& k : lemma){
+    for (const auto& k : lemma[0]){
         if (k == i0) {
             found0 = true;
         } else if (k == i1) {
@@ -2222,8 +2333,8 @@ void solver::test_basic_lemma_for_mon_zero_from_monomial_to_factors() {
                  lp_bde,
                  lp_acd,
                  lp_be);
-    vector<ineq> lemma;
+    vector<lemma> lemma;
-    lp::explanation exp;
+    vector<lp::explanation> exp;
 
 
     s.set_column_value(lp_b, rational(1));
@@ -2247,7 +2358,7 @@ void solver::test_basic_lemma_for_mon_zero_from_monomial_to_factors() {
     bool found1 = false;
     bool found2 = false;
 
-    for (const auto& k : lemma){
+    for (const auto& k : lemma[0]){
         if (k == i0) {
             found0 = true;
         } else if (k == i1) {
@@ -2292,8 +2403,8 @@ void solver::test_basic_lemma_for_mon_neutral_from_monomial_to_factors() {
                  lp_bde,
                  lp_acd,
                  lp_be);
-    vector<ineq> lemma;
+    vector<lemma> lemma;
-    lp::explanation exp;
+    vector<lp::explanation> exp;
 
     // set all vars to 1
     s.set_column_value(lp_a, rational(1));
@@ -2321,7 +2432,7 @@ void solver::test_basic_lemma_for_mon_neutral_from_monomial_to_factors() {
     bool found0 = false;
     bool found1 = false;
 
-    for (const auto& k : lemma){
+    for (const auto& k : lemma[0]){
         if (k == i0) {
             found0 = true;
         } else if (k == i1) {
@@ -2380,9 +2491,9 @@ void solver::test_basic_sign_lemma() {
     s.set_column_value(lp_bde, lp::impq(rational(5)));
     s.set_column_value(lp_acd, lp::impq(rational(3)));
    
-    vector<ineq> lemma;
+    vector<lemma> lemma;
-    lp::explanation exp;
+    vector<lp::explanation> exp;
-    
+
     SASSERT(nla.m_imp->test_check(lemma, exp) == l_false);
 
     lp::lar_term t;
@@ -2391,12 +2502,12 @@ void solver::test_basic_sign_lemma() {
     ineq q(llc::EQ, t, rational(0));
    
     nla.m_imp->print_lemma(std::cout << "expl & lemma: ");
-    SASSERT(q == lemma.back());
+    SASSERT(q == lemma[0].back());
     ineq i0(llc::EQ, lp::lar_term(), rational(0));
     i0.m_term.add_coeff_var(lp_bde);
     i0.m_term.add_coeff_var(rational(1), lp_acd);
     bool found = false;
-    for (const auto& k : lemma){
+    for (const auto& k : lemma[0]){
         if (k == i0) {
             found = true;
         } 
@@ -2517,9 +2628,9 @@ void solver::test_order_lemma_params(bool var_equiv, int sign) {
         s.set_column_value(lp_abef, nla.m_imp->mon_value_by_vars(mon_cdij)
                            + rational(1));
     }
-    vector<ineq> lemma;
+    vector<lemma> lemma;
-    lp::explanation exp;
+    vector<lp::explanation> exp;
-    
+
     SASSERT(nla.m_imp->test_check(lemma, exp) == l_false);
     SASSERT(!var_equiv || !exp.empty());
     // lp::lar_term t;
@@ -2561,7 +2672,6 @@ void solver::test_monotone_lemma() {
     lpvar lp_cd = s.add_named_var(cd, true, "cd");
     lpvar lp_ef = s.add_named_var(ef, true, "ef");
     lpvar lp_ij = s.add_named_var(ij, true, "ij");
-    //    lpvar lp_abef = s.add_named_var(abef, true, "abef");
     for (unsigned j = 0; j < s.number_of_vars(); j++) {
         s.set_column_value(j, rational((j + 2)*(j + 2)));
     }
@@ -2603,8 +2713,45 @@ void solver::test_monotone_lemma() {
     // set ef = ij while it has to be ef > ij
     s.set_column_value(lp_ef, s.get_column_value(lp_ij));
 
-    vector<ineq> lemma;
+    vector<lemma> lemma;
-    lp::explanation exp;
+    vector<lp::explanation> exp;
+    SASSERT(nla.m_imp->test_check(lemma, exp) == l_false);
+    nla.m_imp->print_lemma(std::cout << "lemma: ");
+}
+
+void solver::test_tangent_lemma() {
+    enable_trace("nla_solver");
+    lp::lar_solver s;
+    unsigned a = 0, b = 1, ab = 10;
+    
+    lpvar lp_a = s.add_named_var(a, true, "a");
+    lpvar lp_b = s.add_named_var(b, true, "b");
+    //    lpvar lp_c = s.add_named_var(c, true, "c");
+    //    lpvar lp_d = s.add_named_var(d, true, "d");
+    // lpvar lp_e = s.add_named_var(e, true, "e");
+    // lpvar lp_f = s.add_named_var(f, true, "f");
+    // lpvar lp_i = s.add_named_var(i, true, "i");
+    // lpvar lp_j = s.add_named_var(j, true, "j");
+    lpvar lp_ab = s.add_named_var(ab, true, "ab");
+    int sign = 1;
+    for (unsigned j = 0; j < s.number_of_vars(); j++) {
+        sign *= -1;
+        s.set_column_value(j, sign * rational((j + 2) * (j + 2)));
+    }
+    
+    reslimit l;
+    params_ref p;
+    solver nla(s, l, p);
+    // create monomial ab
+    vector<unsigned> vec;
+    vec.push_back(lp_a);
+    vec.push_back(lp_b);
+    int mon_ab = nla.add_monomial(lp_ab, vec.size(), vec.begin());
+    
+    s.set_column_value(lp_ab, nla.m_imp->mon_value_by_vars(mon_ab) + rational(1)); // greater by one than the correct value
+    vector<lemma> lemma;
+    vector<lp::explanation> exp;
+
     SASSERT(nla.m_imp->test_check(lemma, exp) == l_false);
     nla.m_imp->print_lemma(std::cout << "lemma: ");
 }

src/util/lp/nla_solver.h

@@ -62,7 +62,7 @@ public:
     void push();
     void pop(unsigned scopes);
     bool need_check();
-    lbool check(lp::explanation&, lemma&);
+    lbool check(vector<lp::explanation>&, vector<lemma>&);
     static void test_factorization();
     static void test_basic_sign_lemma();
     static void test_basic_lemma_for_mon_zero_from_monomial_to_factors();
@@ -74,5 +74,6 @@ public:
     static void test_order_lemma();
     static void test_order_lemma_params(bool, int sign);
     static void test_monotone_lemma();
+    static void test_tangent_lemma();
 };
 }