adding nra

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

src/smt/params/smt_params_helper.pyg

@@ -36,7 +36,7 @@ def_module_params(module_name='smt',
                           ('bv.reflect', BOOL, True, 'create enode for every bit-vector term'),
                           ('bv.enable_int2bv', BOOL, True, 'enable support for int2bv and bv2int operators'),
                           ('arith.random_initial_value', BOOL, False, 'use random initial values in the simplex-based procedure for linear arithmetic'),
-                          ('arith.solver', UINT, 2, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination'),
+                          ('arith.solver', UINT, 2, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver'),
                           ('arith.nl', BOOL, True, '(incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation'),
                           ('arith.nl.gb', BOOL, True, 'groebner Basis computation, this option is ignored when arith.nl=false'),
                           ('arith.nl.branching', BOOL, True, 'branching on integer variables in non linear clusters'),

src/smt/params/theory_arith_params.h

@@ -23,12 +23,13 @@ Revision History:
 #include"params.h"
 
 enum arith_solver_id {
-    AS_NO_ARITH,
+    AS_NO_ARITH,              // 0
-    AS_DIFF_LOGIC,
+    AS_DIFF_LOGIC,            // 1
-    AS_ARITH,
+    AS_ARITH,                 // 2
-    AS_DENSE_DIFF_LOGIC,
+    AS_DENSE_DIFF_LOGIC,      // 3
-    AS_UTVPI,
+    AS_UTVPI,                 // 4
-    AS_OPTINF
+    AS_OPTINF,                // 5
+    AS_LRA                    // 6
 };
 
 enum bound_prop_mode {

src/smt/smt_setup.cpp

@@ -724,8 +724,6 @@ namespace smt {
     }
 
     void setup::setup_r_arith() {
-        // to disable theory lra
-        // m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));        
         m_context.register_plugin(alloc(smt::theory_lra, m_manager, m_params));
     }
 
@@ -789,6 +787,9 @@ namespace smt {
         case AS_OPTINF:
             m_context.register_plugin(alloc(smt::theory_inf_arith, m_manager, m_params));            
             break;
+        case AS_LRA:
+            setup_r_arith();
+            break;
         default:
             if (m_params.m_arith_int_only && int_only)
                 m_context.register_plugin(alloc(smt::theory_i_arith, m_manager, m_params));

src/smt/theory_lra.cpp

@@ -366,6 +366,14 @@ namespace smt {
                     terms[index] = n1;
                     st.terms_to_internalize().push_back(n2);
                 }
+                else if (a.is_mul(n)) {
+                    theory_var v;
+                    internalize_mul(to_app(n), v, r);
+                    coeffs[index] *= r;
+                    coeffs[vars.size()] = coeffs[index];
+                    vars.push_back(v);
+                    ++index;
+                }
                 else if (a.is_numeral(n, r)) {
                     coeff += coeffs[index]*r;
                     ++index;
@@ -415,10 +423,13 @@ namespace smt {
             }
         }
 
-        void internalize_mul(app* t) {
+        void internalize_mul(app* t, theory_var& v, rational& r) {
             SASSERT(a.is_mul(t));
+            internalize_args(t);
             mk_enode(t);
-            theory_var v = mk_var(t);
+            r = rational::one();
+            rational r1;
+            v = mk_var(t);
             svector<lean::var_index> vars;
             ptr_vector<expr> todo;
             todo.push_back(t);
@@ -430,6 +441,9 @@ namespace smt {
                     todo.push_back(n1);
                     todo.push_back(n2);
                 }
+                else if (a.is_numeral(n, r1)) {
+                    r *= r1;
+                }
                 else {
                     if (!ctx().e_internalized(n)) {
                         ctx().internalize(n, false);
@@ -437,7 +451,7 @@ namespace smt {
                     vars.push_back(get_var_index(mk_var(n)));
                 }
             }
-            // m_solver->add_monomial(get_var_index(v), vars);
+            m_solver->add_monomial(get_var_index(v), vars);
         }
 
         enode * mk_enode(app * n) {
@@ -1245,7 +1259,7 @@ namespace smt {
 
         lbool check_nra() {
             if (m.canceled()) return l_undef;
-            return l_true;
+            // return l_true;
             // TBD:
             switch (m_solver->check_nra(m_variable_values, m_explanation)) {
             case lean::final_check_status::DONE:

src/util/lp/nra_solver.cpp

@@ -21,8 +21,8 @@ namespace nra {
         u_map<polynomial::var> m_lp2nl;  // map from lar_solver variables to nlsat::solver variables
 
         struct mon_eq {
-            mon_eq(lean::var_index v, svector<lean::var_index> const& vs):
+            mon_eq(lean::var_index v, unsigned sz, lean::var_index const* vs):
-                m_v(v), m_vs(vs) {}
+                m_v(v), m_vs(sz, vs) {}
             lean::var_index          m_v;
             svector<lean::var_index> m_vs;
         };
@@ -44,14 +44,14 @@ namespace nra {
             }
             switch (check_nlsat(m, ex)) {
             case l_undef: return lean::final_check_status::GIVEUP;
-            case l_true: lean::final_check_status::DONE;
+            case l_true: return lean::final_check_status::DONE;
-            case l_false: lean::final_check_status::UNSAT;
+            case l_false: return lean::final_check_status::UNSAT;
             }
             return lean::final_check_status::DONE;
         }
 
         void add(lean::var_index v, unsigned sz, lean::var_index const* vs) {
-            m_monomials.push_back(mon_eq(v, svector<lean::var_index>(sz, vs)));
+            m_monomials.push_back(mon_eq(v, sz, vs));
         }
 
         void push() {
@@ -60,7 +60,6 @@ namespace nra {
 
         void pop(unsigned n) {
             if (n == 0) return;
-            SASSERT(n < m_lim.size());
             m_monomials.shrink(m_lim[m_lim.size() - n]);
             m_lim.shrink(m_lim.size() - n);       
         }
@@ -112,7 +111,9 @@ namespace nra {
             }
             // TBD: add variable bounds?
 
+
             lbool r = solver.check(); 
+            TRACE("arith", solver.display(tout << r << "\n"););
             switch (r) {
             case l_true: {
                 nlsat::anum_manager& am = solver.am();
@@ -143,6 +144,7 @@ namespace nra {
                 for (auto c : core) {
                     unsigned idx = static_cast<unsigned>(static_cast<imp*>(c) - this);
                     ex.push_back(std::pair<rational, unsigned>(rational(1), idx));
+                    TRACE("arith", tout << "ex: " << idx << "\n";);
                 }
                 break;
             }
@@ -172,12 +174,12 @@ namespace nra {
         }
 
         void add_constraint(nlsat::solver& solver, unsigned idx) {
-            lean::lar_base_constraint const& c = s.get_constraint(idx);
+            auto& c = s.get_constraint(idx);
-            polynomial::manager& pm = solver.pm();
+            auto& pm = solver.pm();
             auto k = c.m_kind;
             auto rhs = c.m_right_side;
             auto lhs = c.get_left_side_coefficients();
-            unsigned sz = lhs.size();
+            auto sz = lhs.size();
             svector<polynomial::var> vars;
             rational den = denominator(rhs);
             for (auto kv : lhs) {
@@ -229,6 +231,17 @@ namespace nra {
             return r;
         }
 
+        std::ostream& display(std::ostream& out) const {
+            for (auto m : m_monomials) {
+                out << "v" << m.m_v << " = ";
+                for (auto v : m.m_vs) {
+                    out << "v" << v << " ";
+                }
+                out << "\n";
+            }
+            return out;
+        }
+
     };
 
     solver::solver(lean::lar_solver& s) {
@@ -254,4 +267,9 @@ namespace nra {
     void solver::pop(unsigned n) {
         m_imp->pop(n);
     }
+
+    std::ostream& solver::display(std::ostream& out) const {
+        return m_imp->display(out);
+    }
+
 }

src/util/lp/nra_solver.h

@@ -42,5 +42,10 @@ namespace nra {
         void push();
         
         void pop(unsigned n);
+
+        /*
+          \brief display state
+         */
+        std::ostream& display(std::ostream& out) const;
     };
 }