add a hook to add new multiplication definitions in nla_core

src/math/lp/nla_core.cpp

@@ -1577,7 +1577,10 @@ lbool core::check() {
         lp_settings().stats().m_nra_calls++;
     }
     
-    if (ret == l_undef && !no_effect() && m_reslim.inc()) 
+    if (ret == l_undef)
+        return l_undef;
+
+    if (!no_effect() && m_reslim.inc()) 
         ret = l_false;
 
     lp_settings().stats().m_nla_lemmas += m_lemmas.size();

src/math/lp/nla_core.h

@@ -94,6 +94,8 @@ class core {
     emonics                  m_emons;
     svector<lpvar>           m_add_buffer;
     mutable indexed_uint_set m_active_var_set;
+    // hook installed by theory_lra for creating a multiplication definition
+    std::function<lpvar(unsigned, lpvar const*)> m_add_mul_def_hook;
 
     reslimit                 m_nra_lim;
 
@@ -208,6 +210,8 @@ public:
     void add_idivision(lpvar q, lpvar x, lpvar y) { m_divisions.add_idivision(q, x, y); }
     void add_rdivision(lpvar q, lpvar x, lpvar y) { m_divisions.add_rdivision(q, x, y); }
     void add_bounded_division(lpvar q, lpvar x, lpvar y) { m_divisions.add_bounded_division(q, x, y); }
+    void set_add_mul_def_hook(std::function<lpvar(unsigned, lpvar const*)> const& f) { m_add_mul_def_hook = f; }
+    lpvar add_mul_def(unsigned sz, lpvar const* vs) { SASSERT(m_add_mul_def_hook); lpvar v = m_add_mul_def_hook(sz, vs); add_monic(v, sz, vs); return v; }
 
     void set_relevant(std::function<bool(lpvar)>& is_relevant) { m_relevant = is_relevant; }
     bool is_relevant(lpvar v) const { return !m_relevant || m_relevant(v); }

src/math/lp/nra_solver.cpp

@@ -289,17 +289,9 @@ struct solver::imp {
                 if (mon) 
                     v = mon->var();                                
                 else {
-                    NOT_IMPLEMENTED_YET();
+                    v = m_nla_core.add_mul_def(vars.size(), vars.data());
-                    // this one is for Lev Nachmanson: lar_solver relies on internal variables
-                    // to have terms from outside. The solver doesn't get to create
-                    // its own monomials. 
-                    // v = ...
-                    // It is not a use case if the nlsat solver only provides linear
-                    // polynomials so punt for now.
-                    m_nla_core.add_monic(v, vars.size(), vars.data());
                 }
                 TRACE(nra,
-                      tout << "process_polynomial_check_assignment:"; 
                       tout << " vars="; 
                       for (auto _w : vars) tout << _w << ' '; 
                       tout << " s=" << s
@@ -325,7 +317,6 @@ struct solver::imp {
         lbool r = l_undef;
     statistics &st = m_nla_core.lp_settings().stats().m_st;
     nlsat::literal_vector clause;
-        polynomial::manager &pm = m_nlsat->pm();
         try {
             nlsat::assignment rvalues(m_nlsat->am());
             for (auto [j, x] : m_lp2nl) {
@@ -373,7 +364,10 @@ struct solver::imp {
             SASSERT(!a->is_root_atom());
             SASSERT(a->is_ineq_atom());
             auto &ia = *to_ineq_atom(a);
-            VERIFY(ia.size() == 1);  // deal with factored polynomials later
+            if (ia.size() != 1) {
+                return l_undef; // levnach: not sure what to do here
+            }
+            // VERIFY(ia.size() == 1);  // deal with factored polynomials later
             // a is an inequality atom, i.e., p > 0, p < 0, or p = 0.
             polynomial::polynomial const *p = ia.p(0);
             TRACE(nra, tout << "polynomial: "; pm.display(tout, p); tout << "\n";);
@@ -404,6 +398,7 @@ struct solver::imp {
             lemma |= inq;
         }
         IF_VERBOSE(1, verbose_stream() << "linear lemma: " << lemma << "\n");
+        this->m_nla_core.m_check_feasible = true;
         return l_false;
     }
 

src/smt/theory_lra.cpp

@@ -155,6 +155,7 @@ class theory_lra::imp {
     ptr_vector<expr>       m_not_handled;
     ptr_vector<app>        m_underspecified;
     ptr_vector<app>        m_bv_terms;
+    ptr_vector<expr>       m_mul_defs; // fresh multiplication definition vars
     vector<ptr_vector<api_bound> > m_use_list;        // bounds where variables are used.
 
     // attributes for incremental version:
@@ -269,10 +270,27 @@ class theory_lra::imp {
                 return ctx().is_relevant(th.get_enode(u));
             };
             m_nla->set_relevant(is_relevant);
+            // install hook for creating multiplication definitions from nra_solver
+            m_nla->get_core().set_add_mul_def_hook([&](unsigned sz, lpvar const* vs) { return add_mul_def(sz, vs); });
 
         }
     }
 
+    lpvar add_mul_def(unsigned sz, lpvar const* vs) { // under 10 lines
+        bool is_int = true;
+        for (unsigned i = 0; i < sz; ++i) {
+            theory_var tv = lp().local_to_external(vs[i]);
+            is_int &= this->is_int(tv);
+        }
+        sort* srt = is_int ? a.mk_int() : a.mk_real();
+        app_ref c(m.mk_fresh_const("mul!", srt), m);
+        mk_enode(c);
+        theory_var v = mk_var(c);
+        ctx().push_trail(push_back_vector<ptr_vector<expr>>(m_mul_defs));
+        m_mul_defs.push_back(c);
+        return register_theory_var_in_lar_solver(v);
+    }
+
     void found_unsupported(expr* n) {
         ctx().push_trail(push_back_vector<ptr_vector<expr>>(m_not_handled));
         TRACE(arith, tout << "unsupported " << mk_pp(n, m) << "\n");