updates

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/math/lp/nla_stellensatz.cpp

@@ -709,12 +709,9 @@ namespace nla {
         while (m_constraints.size() > max_ci) {
             auto const& [_p, _k, _j] = m_constraints.back();
             m_constraint_index.erase({_p.index(), _k});
-            m_constraints.pop_back();
+            auto ci = m_constraints.size() - 1;            
-            auto ci = m_constraints.size();
-            if (!m_occurs_trail.empty() && m_occurs_trail.back() == ci) {
             remove_occurs(ci);            
-                m_occurs_trail.pop_back();
+            m_constraints.pop_back();
-            }
         }
         for (auto const &[_p, _k, _j] : replay) {
             auto ci = add_constraint(_p, _k, _j);
@@ -937,13 +934,18 @@ namespace nla {
             return;
         m_occurs_trail.push_back(ci);
         auto const &con = m_constraints[ci];
+        verbose_stream() << "init-occurs " << ci << " vars: " << con.p.free_vars() << "\n"; 
         for (auto v : con.p.free_vars())
             m_occurs[v].push_back(ci);
         
     }
 
     void stellensatz::remove_occurs(lp::constraint_index ci) {
+        if (m_occurs_trail.empty() || m_occurs_trail.back() != ci)
+            return;
+        m_occurs_trail.pop_back();
         auto const &con = m_constraints[ci];
+        verbose_stream() << "remove-occurs " << ci << " vars: " << con.p.free_vars() << "\n"; 
         for (auto v : con.p.free_vars())
             m_occurs[v].pop_back();
     }

src/math/lp/nra_solver.cpp

@@ -161,6 +161,35 @@ struct solver::imp {
         }
     }
 
+    void add_tangent_lemmas() {
+        for (auto const mi : m_nla_core.to_refine()) {
+            auto const& m = m_nla_core.emon(mi);
+            if (m.size() != 2)
+                continue;
+            auto x = m.vars()[0];
+            auto y = m.vars()[1];
+            rational xv = m_nla_core.val(x);
+            rational yv = m_nla_core.val(y);
+            rational mv = m_nla_core.val(m.var());
+            SASSERT(xv * yv != mv);
+            // a := xv - 1, b := yv - 1
+            // mv < xv * yv
+            // (x - a)(y - b) = 1
+            // (x - a)(y - b) = xy - bx - ay + ab = 1
+            // mv - bx - ay + ab < 1
+            // lemma: x > a, y > b  => xy - bx - ay + ab >= 1
+            // 
+            // mv > xv * yv
+            // a := xv - 1, b := yv + 1
+            // x > a, y < b => xy - by - ax + ab <= -1
+            // 
+            // other lemmas around a < x, b < y and a < x, b > y
+            //
+
+
+        }
+    }
+
     /**
        \brief one-shot nlsat check.
        A one shot checker is the least functionality that can 

src/nlsat/nlsat_solver.cpp

@@ -1876,6 +1876,7 @@ namespace nlsat {
             m_stats.m_conflicts = 0;
             m_stats.m_restarts = 0;
             m_next_conflict = 0;
+            random_gen rand(++m_random_seed);
             while (true) {
                 r = search();
                 if (r != l_true) 
@@ -1925,12 +1926,10 @@ namespace nlsat {
                 // cut on the first model value
                 if (!m_model_values.empty()) {
                     bool found = false;
-                    random_gen r(++m_random_seed);
+
-                    auto const &[x, value] = bounds[r(bounds.size())];
+                    auto const &[x, value] = bounds[rand(bounds.size())];
                     for (auto const &[ext_x, mvalue, lo, hi] : m_model_values) {
                         if (ext_x == m_perm[x]) {
-                            verbose_stream() << x << " " << ext_x << " bound: " << mvalue << " value " << value
-                                             << "\n ";
                             TRACE(nla_solver, tout << "x" << ext_x << " bound " << mvalue << "\n");
                             polynomial_ref p(m_pm);
                             rational one(1);
@@ -1955,20 +1954,32 @@ namespace nlsat {
                     }
                     continue;
                 }
-                for (auto const& b : bounds) {
+                for (auto const& [x, lo] : bounds) {
-                    var x = b.first;
-                    rational lo = b.second;
                     rational hi = lo + 1; // rational::one();
                     bool is_even = false;                        
                     polynomial_ref p(m_pm);
                     rational one(1);
                     m_lemma.reset();
+                    auto add_gt = [&]() {
                         p = m_pm.mk_linear(1, &one, &x, -lo);
                         poly *p1 = p.get();
                         m_lemma.push_back(~mk_ineq_literal(atom::GT, 1, &p1, &is_even));
+                    };
+                    auto add_lt = [&]() {
                         p = m_pm.mk_linear(1, &one, &x, -hi);
                         poly *p2 = p.get();
                         m_lemma.push_back(~mk_ineq_literal(atom::LT, 1, &p2, &is_even));
+                    };
+
+
+                    if (rand(2) == 0) {
+                        add_gt();
+                        add_lt();
+                    }
+                    else {
+                        add_lt();
+                        add_gt();
+                    }
                     
                     // perform branch and bound
                     clause * cls = mk_clause(m_lemma.size(), m_lemma.data(), true, nullptr);