merge

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

contrib/cmake/src/CMakeLists.txt

@@ -35,10 +35,10 @@ endforeach()
 # raised if you try to declare a component is dependent on another component
 # that has not yet been declared.
 add_subdirectory(util)
-add_subdirectory(util/lp)
 add_subdirectory(math/polynomial)
 add_subdirectory(sat)
 add_subdirectory(nlsat)
+add_subdirectory(util/lp)
 add_subdirectory(math/hilbert)
 add_subdirectory(math/simplex)
 add_subdirectory(math/automata)

contrib/cmake/src/smt/CMakeLists.txt

@@ -70,6 +70,7 @@ z3_add_component(smt
     euclid
     fpa
     grobner
+    nlsat
     lp
     macros
     normal_forms

contrib/cmake/src/test/CMakeLists.txt

@@ -1,4 +1,5 @@
 add_subdirectory(fuzzing)
+add_subdirectory(lp)
 ################################################################################
 # z3-test executable
 ################################################################################
@@ -119,7 +120,7 @@ add_executable(test-z3
   upolynomial.cpp
   var_subst.cpp
   vector.cpp
-  lp.cpp
+  lp/lp.cpp
   ${z3_test_extra_object_files}
 )
 z3_add_install_tactic_rule(${z3_test_deps})

contrib/cmake/src/test/lp/CMakeLists.txt

@@ -0,0 +1,6 @@
+add_executable(lp_tst lp_main.cpp lp.cpp $<TARGET_OBJECTS:util> $<TARGET_OBJECTS:polynomial> $<TARGET_OBJECTS:nlsat>  $<TARGET_OBJECTS:lp> )
+target_compile_definitions(lp_tst PRIVATE ${Z3_COMPONENT_CXX_DEFINES})
+target_compile_options(lp_tst PRIVATE ${Z3_COMPONENT_CXX_FLAGS})
+target_include_directories(lp_tst PRIVATE ${Z3_COMPONENT_EXTRA_INCLUDE_DIRS})
+target_link_libraries(lp_tst PRIVATE ${Z3_DEPENDENT_LIBS})
+z3_append_linker_flag_list_to_target(lp_tst ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS})

contrib/cmake/src/util/lp/CMakeLists.txt

@@ -8,6 +8,7 @@ z3_add_component(lp
     dense_matrix_instances.cpp
     eta_matrix_instances.cpp
     indexed_vector_instances.cpp
+    lar_solver_instances.cpp
     lar_core_solver_instances.cpp
     lp_core_solver_base_instances.cpp
     lp_dual_core_solver_instances.cpp
@@ -18,8 +19,9 @@ z3_add_component(lp
     lp_solver_instances.cpp
     lu_instances.cpp
     matrix_instances.cpp
+    nra_solver.cpp
     permutation_matrix_instances.cpp
-	quick_xplain.cpp
+    quick_xplain.cpp
     row_eta_matrix_instances.cpp
     scaler_instances.cpp
     sparse_matrix_instances.cpp
@@ -28,6 +30,8 @@ z3_add_component(lp
     random_updater_instances.cpp      
   COMPONENT_DEPENDENCIES
     util
+    polynomial
+    nlsat
   PYG_FILES
     lp_params.pyg
 )

src/ast/ast.cpp

@@ -1727,7 +1727,6 @@ ast * ast_manager::register_node_core(ast * n) {
 
     n->m_id   = is_decl(n) ? m_decl_id_gen.mk() : m_expr_id_gen.mk();
 
-
     TRACE("ast", tout << "Object " << n->m_id << " was created.\n";);
     TRACE("mk_var_bug", tout << "mk_ast: " << n->m_id << "\n";);
     // increment reference counters

src/ast/rewriter/arith_rewriter.cpp

@@ -738,9 +738,54 @@ br_status arith_rewriter::mk_idiv_core(expr * arg1, expr * arg2, expr_ref & resu
         result = m_util.mk_idiv0(arg1);
         return BR_REWRITE1;
     }
+    expr_ref quot(m());
+    if (divides(arg1, arg2, quot)) {
+        result = m_util.mk_mul(quot, m_util.mk_idiv(arg1, arg1));
+        return BR_REWRITE2;
+    }
     return BR_FAILED;
 }
 
+bool arith_rewriter::divides(expr* d, expr* n, expr_ref& quot) {
+    if (d == n) {
+        quot = m_util.mk_numeral(rational(1), m_util.is_int(d));
+        return true;
+    }
+    if (m_util.is_mul(n)) {
+        expr_ref_vector muls(m());
+        muls.push_back(n);
+        expr* n1, *n2;
+        rational r1, r2;
+        for (unsigned i = 0; i < muls.size(); ++i) {
+            if (m_util.is_mul(muls[i].get(), n1, n2)) {
+                muls[i] = n1;
+                muls.push_back(n2);
+                --i;
+            }
+        }
+        if (m_util.is_numeral(d, r1) && !r1.is_zero()) {
+            for (unsigned i = 0; i < muls.size(); ++i) {
+                if (m_util.is_numeral(muls[i].get(), r2) && (r2 / r1).is_int()) {
+                    muls[i] = m_util.mk_numeral(r2 / r1, m_util.is_int(d));
+                    quot = m_util.mk_mul(muls.size(), muls.c_ptr());
+                    return true;
+                }            
+            }
+        }
+        else {
+            for (unsigned i = 0; i < muls.size(); ++i) {
+                if (d == muls[i].get()) {
+                    muls[i] = muls.back();
+                    muls.pop_back();
+                    quot = m_util.mk_mul(muls.size(), muls.c_ptr());
+                    return true;
+                }            
+            }
+        }
+    }
+    return false;
+}
+
 br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & result) {
     set_curr_sort(m().get_sort(arg1));
     numeral v1, v2;

src/ast/rewriter/arith_rewriter.h

@@ -90,6 +90,7 @@ class arith_rewriter : public poly_rewriter<arith_rewriter_core> {
     bool is_pi_integer_offset(expr * t, expr * & m);
     expr * mk_sin_value(rational const & k);
     app * mk_sqrt(rational const & k);
+    bool divides(expr* d, expr* n, expr_ref& quot);
 
 public:
     arith_rewriter(ast_manager & m, params_ref const & p = params_ref()):

src/ast/simplifier/arith_simplifier_plugin.cpp

@@ -267,10 +267,55 @@ void arith_simplifier_plugin::mk_idiv(expr * arg1, expr * arg2, expr_ref & resul
     bool is_int;
     if (m_util.is_numeral(arg1, v1, is_int) && m_util.is_numeral(arg2, v2, is_int) && !v2.is_zero())
         result = m_util.mk_numeral(div(v1, v2), is_int);
+    else if (divides(arg2, arg1, result)) {
+        result = m_util.mk_mul(result, m_util.mk_idiv(arg2, arg2));
+    }
     else 
         result = m_util.mk_idiv(arg1, arg2);
 }
 
+bool arith_simplifier_plugin::divides(expr* d, expr* n, expr_ref& quot) {
+    ast_manager& m = m_manager;
+    if (d == n) {
+        quot = m_util.mk_numeral(rational(1), m_util.is_int(d));
+        return true;
+    }
+    if (m_util.is_mul(n)) {
+        expr_ref_vector muls(m);
+        muls.push_back(n);
+        expr* n1, *n2;
+        rational r1, r2;
+        for (unsigned i = 0; i < muls.size(); ++i) {
+            if (m_util.is_mul(muls[i].get(), n1, n2)) {
+                muls[i] = n1;
+                muls.push_back(n2);
+                --i;
+            }
+        }
+        if (m_util.is_numeral(d, r1) && !r1.is_zero()) {
+            for (unsigned i = 0; i < muls.size(); ++i) {
+                if (m_util.is_numeral(muls[i].get(), r2) && (r2 / r1).is_int()) {
+                    muls[i] = m_util.mk_numeral(r2 / r1, m_util.is_int(d));
+                    quot = m_util.mk_mul(muls.size(), muls.c_ptr());
+                    return true;
+                }            
+            }
+        }
+        else {
+            for (unsigned i = 0; i < muls.size(); ++i) {
+                if (d == muls[i].get()) {
+                    muls[i] = muls.back();
+                    muls.pop_back();
+                    quot = m_util.mk_mul(muls.size(), muls.c_ptr());
+                    return true;
+                }            
+            }
+        }
+    }
+    return false;
+}
+
+
 void arith_simplifier_plugin::prop_mod_const(expr * e, unsigned depth, numeral const& k, expr_ref& result) {
     SASSERT(m_util.is_int(e));
     SASSERT(k.is_int() && k.is_pos());

src/ast/simplifier/arith_simplifier_plugin.h

@@ -48,6 +48,7 @@ protected:
 
     void div_monomial(expr_ref_vector& monomials, numeral const& g);
     void get_monomial_gcd(expr_ref_vector& monomials, numeral& g);
+    bool divides(expr* d, expr* n, expr_ref& quot);
 
 public:
     arith_simplifier_plugin(ast_manager & m, basic_simplifier_plugin & b, arith_simplifier_params & p);

src/math/polynomial/polynomial.h

@@ -19,16 +19,16 @@ Notes:
 #ifndef POLYNOMIAL_H_
 #define POLYNOMIAL_H_
 
-#include"mpz.h"
+#include"util/mpz.h"
-#include"rational.h"
+#include"util/rational.h"
-#include"obj_ref.h"
+#include"util/obj_ref.h"
-#include"ref_vector.h"
+#include"util/ref_vector.h"
-#include"z3_exception.h"
+#include"util/z3_exception.h"
-#include"scoped_numeral.h"
+#include"util/scoped_numeral.h"
-#include"scoped_numeral_vector.h"
+#include"util/scoped_numeral_vector.h"
-#include"params.h"
+#include"util/params.h"
-#include"mpbqi.h"
+#include"util/mpbqi.h"
-#include"rlimit.h"
+#include"util/rlimit.h"
 
 class small_object_allocator;
 

src/nlsat/nlsat_solver.h

@@ -21,10 +21,10 @@ Revision History:
 #ifndef NLSAT_SOLVER_H_
 #define NLSAT_SOLVER_H_
 
-#include"nlsat_types.h"
+#include"nlsat/nlsat_types.h"
-#include"params.h"
+#include"util/params.h"
-#include"statistics.h"
+#include"util/statistics.h"
-#include"rlimit.h"
+#include"util/rlimit.h"
 
 namespace nlsat {
 

src/nlsat/nlsat_types.h

@@ -19,10 +19,10 @@ Revision History:
 #ifndef NLSAT_TYPES_H_
 #define NLSAT_TYPES_H_
 
-#include"polynomial.h"
+#include"math/polynomial/polynomial.h"
-#include"buffer.h"
+#include"util/buffer.h"
-#include"sat_types.h"
+#include"sat/sat_types.h"
-#include"z3_exception.h"
+#include"util/z3_exception.h"
 
 namespace algebraic_numbers {
     class anum;

src/sat/sat_types.h

@@ -19,13 +19,13 @@ Revision History:
 #ifndef SAT_TYPES_H_
 #define SAT_TYPES_H_
 
-#include"debug.h"
+#include"util/debug.h"
-#include"approx_set.h"
+#include"util/approx_set.h"
-#include"lbool.h"
+#include"util/lbool.h"
-#include"z3_exception.h"
+#include"util/z3_exception.h"
-#include"common_msgs.h"
+#include"util/common_msgs.h"
-#include"vector.h"
+#include"util/vector.h"
-#include"uint_set.h"
+#include"util/uint_set.h"
 #include<iomanip>
 
 namespace sat {

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_model_generator.cpp

@@ -388,6 +388,7 @@ namespace smt {
             enode * n = *it3;
             if (is_uninterp_const(n->get_owner()) && m_context->is_relevant(n)) {
                 func_decl * d = n->get_owner()->get_decl();
+                TRACE("mg_top_sort", tout << d->get_name() << " " << (m_hidden_ufs.contains(d)?"hidden":"visible") << "\n";);
                 if (m_hidden_ufs.contains(d)) continue;
                 expr * val    = get_value(n);
                 m_model->register_decl(d, val);

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

@@ -35,6 +35,7 @@ Revision History:
 #include "smt/smt_model_generator.h"
 #include "smt/arith_eq_adapter.h"
 #include "util/nat_set.h"
+#include "util/lp/nra_solver.h"
 #include "tactic/filter_model_converter.h"
 
 namespace lp {
@@ -144,10 +145,10 @@ namespace smt {
         ast_manager&         m;
         theory_arith_params& m_arith_params;
         arith_util           a;
-
         arith_eq_adapter     m_arith_eq_adapter;
+        vector<rational>     m_columns;
+      
 
-        vector<rational>    m_columns;
         // temporary values kept during internalization
         struct internalize_state {
             expr_ref_vector     m_terms;                     
@@ -248,6 +249,8 @@ namespace smt {
 
         unsigned               m_num_conflicts;
 
+        scoped_ptr<nra::solver> m_nra;
+        bool                    m_use_nra_model;
 
         struct var_value_eq {
             imp & m_th;
@@ -291,6 +294,16 @@ namespace smt {
             //m_solver->settings().set_ostream(0);
         }
 
+        void ensure_nra() {
+            if (!m_nra) {
+                m_nra = alloc(nra::solver, *m_solver.get(), m.limit(), ctx().get_params());
+                for (unsigned i = 0; i < m_scopes.size(); ++i) {
+                    m_nra->push();
+                }
+            }
+        }
+
+
         void found_not_handled(expr* n) {
             m_not_handled = n;
             if (is_app(n) && is_underspecified(to_app(n))) {
@@ -366,6 +379,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,6 +436,44 @@ namespace smt {
             }
         }
 
+        void internalize_mul(app* t, theory_var& v, rational& r) {
+            SASSERT(a.is_mul(t));
+            bool _has_var = has_var(t);
+            if (!_has_var) {
+                internalize_args(t);
+                mk_enode(t);
+            }
+            r = rational::one();
+            rational r1;
+            v = mk_var(t);
+            svector<lean::var_index> vars;
+            ptr_vector<expr> todo;
+            todo.push_back(t);
+            while (!todo.empty()) {
+                expr* n = todo.back();
+                todo.pop_back();
+                expr* n1, *n2;
+                if (a.is_mul(n, n1, n2)) {
+                    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);
+                    }
+                    vars.push_back(get_var_index(mk_var(n)));
+                }
+            }
+            TRACE("arith", tout << mk_pp(t, m) << "\n";);
+            if (!_has_var) {
+                ensure_nra();
+                m_nra->add_monomial(get_var_index(v), vars.size(), vars.c_ptr());
+            }
+        }
+
         enode * mk_enode(app * n) {
             if (ctx().e_internalized(n)) {
                 return get_enode(n);
@@ -459,6 +518,14 @@ namespace smt {
             return m_arith_params.m_arith_reflect || is_underspecified(n);          
         }
 
+        bool has_var(expr* n) {
+            if (!ctx().e_internalized(n)) {
+                return false;
+            }
+            enode* e = get_enode(n);
+            return th.is_attached_to_var(e);
+        }
+
         theory_var mk_var(expr* n, bool internalize = true) {
             if (!ctx().e_internalized(n)) {
                 ctx().internalize(n, false);                
@@ -487,7 +554,7 @@ namespace smt {
                 result = m_theory_var2var_index[v];
             }
             if (result == UINT_MAX) {
-                result = m_solver->add_var(v);
+                result = m_solver->add_var(v, false);
                 m_theory_var2var_index.setx(v, result, UINT_MAX);
                 m_var_index2theory_var.setx(result, v, UINT_MAX);
                 m_var_trail.push_back(v);
@@ -658,7 +725,8 @@ namespace smt {
             m_num_conflicts(0),
             m_model_eqs(DEFAULT_HASHTABLE_INITIAL_CAPACITY, var_value_hash(*this), var_value_eq(*this)),
             m_solver(0),
-            m_resource_limit(*this) {
+            m_resource_limit(*this),
+            m_use_nra_model(false) {
         }
         
         ~imp() {
@@ -815,6 +883,7 @@ namespace smt {
             s.m_underspecified_lim = m_underspecified.size();
             s.m_var_trail_lim = m_var_trail.size();
             if (!m_delay_constraints) m_solver->push();
+            if (m_nra) m_nra->push();
         }
 
         void pop_scope_eh(unsigned num_scopes) {
@@ -847,6 +916,7 @@ namespace smt {
             // VERIFY(l_false != make_feasible());
             m_new_bounds.reset();
             m_to_check.reset();
+            if (m_nra) m_nra->pop(num_scopes);
             TRACE("arith", tout << "num scopes: " << num_scopes << " new scope level: " << m_scopes.size() << "\n";);
         }
 
@@ -1166,18 +1236,41 @@ namespace smt {
             else if (m_solver->get_status() != lean::lp_status::OPTIMAL) {
                 is_sat = make_feasible();
             }
+            final_check_status st = FC_DONE;
             switch (is_sat) {
             case l_true:
+                
                 if (delayed_assume_eqs()) {
                     return FC_CONTINUE;
                 }
                 if (assume_eqs()) {
                     return FC_CONTINUE;
                 }
-                if (m_not_handled != 0) {                    
+
-                    return FC_GIVEUP;
+                switch (check_lia()) {
+                case l_true:
+                    break;
+                case l_false:
+                    return FC_CONTINUE;
+                case l_undef:
+                    st = FC_GIVEUP;
+                    break;
                 }
-                return FC_DONE;
+                
+                switch (check_nra()) {
+                case l_true:
+                    break;
+                case l_false:
+                    return FC_CONTINUE;
+                case l_undef:
+                    st = FC_GIVEUP;
+                    break;
+                }
+                if (m_not_handled != 0) {                    
+                    st = FC_GIVEUP;
+                }
+
+                return st;
             case l_false:
                 set_conflict();
                 return FC_CONTINUE;
@@ -1190,6 +1283,30 @@ namespace smt {
             return FC_GIVEUP;
         }
 
+        lbool check_lia() {
+            if (m.canceled()) return l_undef;
+            return l_true;
+        }
+
+        lbool check_nra() {
+            m_use_nra_model = false;
+            if (m.canceled()) return l_undef;
+            if (!m_nra) return l_true;
+            if (!m_nra->need_check()) return l_true;
+            lbool r = m_nra->check(m_explanation);
+            switch (r) {
+            case l_false:
+                set_conflict1();
+                break;
+            case l_true:
+                m_use_nra_model = true;
+                // TBD: check equalities
+                break;
+            default:
+                break;
+            }
+            return r;
+        }
 
         /**
            \brief We must redefine this method, because theory of arithmetic contains
@@ -2197,11 +2314,15 @@ namespace smt {
         }
 
         void set_conflict() {
+            m_explanation.clear();
+            m_solver->get_infeasibility_explanation(m_explanation);
+            set_conflict1();
+        }
+
+        void set_conflict1() {
             m_eqs.reset();
             m_core.reset();
             m_params.reset();
-            m_explanation.clear();
-            m_solver->get_infeasibility_explanation(m_explanation);
             // m_solver->shrink_explanation_to_minimum(m_explanation); // todo, enable when perf is fixed
             /*
             static unsigned cn = 0;
@@ -2252,7 +2373,17 @@ namespace smt {
 
         model_value_proc * mk_value(enode * n, model_generator & mg) {
             theory_var v = n->get_th_var(get_id());
-            return alloc(expr_wrapper_proc, m_factory->mk_value(get_value(v), m.get_sort(n->get_owner())));
+            expr* o = n->get_owner();
+            if (m_use_nra_model) {
+                SASSERT(m_nra);
+                app* e = a.mk_numeral(m_nra->value(m_theory_var2var_index[v]), a.is_int(o));
+                return alloc(expr_wrapper_proc, e);
+            }
+            else {
+                rational r = get_value(v);
+                if (a.is_int(o) && !r.is_int()) r = floor(r);
+                return alloc(expr_wrapper_proc, m_factory->mk_value(r,  m.get_sort(o)));
+            }
         }
 
         bool get_value(enode* n, expr_ref& r) {
@@ -2278,6 +2409,7 @@ namespace smt {
             if (dump_lemmas()) {
                 ctx().display_lemma_as_smt_problem(m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), false_literal);
             }
+            if (m_arith_params.m_arith_mode == AS_LRA) return true;
             context nctx(m, ctx().get_fparams(), ctx().get_params());
             add_background(nctx);
             bool result = l_true != nctx.check();
@@ -2290,6 +2422,7 @@ namespace smt {
             if (dump_lemmas()) {                
                 ctx().display_lemma_as_smt_problem(m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), lit);
             }
+            if (m_arith_params.m_arith_mode == AS_LRA) return true;
             context nctx(m, ctx().get_fparams(), ctx().get_params());
             m_core.push_back(~lit);
             add_background(nctx);
@@ -2301,6 +2434,7 @@ namespace smt {
         }
 
         bool validate_eq(enode* x, enode* y) {
+            if (m_arith_params.m_arith_mode == AS_LRA) return true;
             context nctx(m, ctx().get_fparams(), ctx().get_params());
             add_background(nctx);
             nctx.assert_expr(m.mk_not(m.mk_eq(x->get_owner(), y->get_owner())));

src/test/lp/lp.cpp

@@ -2695,8 +2695,8 @@ void test_term() {
     lar_solver solver;
     unsigned _x = 0;
     unsigned _y = 1;
-    var_index x = solver.add_var(_x);
+    var_index x = solver.add_var(_x, false);
-    var_index y = solver.add_var(_y);
+    var_index y = solver.add_var(_y, false);
 
     vector<std::pair<mpq, var_index>> term_ls;
     term_ls.push_back(std::pair<mpq, var_index>((int)1, x));
@@ -2709,9 +2709,16 @@ void test_term() {
     ls.push_back(std::pair<mpq, var_index>((int)1, z));
     
     solver.add_constraint(ls, lconstraint_kind::EQ, mpq(0));
+    ls.clear();
+    ls.push_back(std::pair<mpq, var_index>((int)1, x));
+    solver.add_constraint(ls, lconstraint_kind::LT, mpq(0));
+    ls.push_back(std::pair<mpq, var_index>((int)2, y));
+    solver.add_constraint(ls, lconstraint_kind::GT, mpq(0));
     auto status = solver.solve();
     std::cout << lp_status_to_string(status) << std::endl;
     std::unordered_map<var_index, mpq> model;
+    if (status != OPTIMAL)
+        return;
     solver.get_model(model);
     
     for (auto & t : model) {
@@ -2723,8 +2730,8 @@ void test_term() {
 
 void test_evidence_for_total_inf_simple(argument_parser & args_parser) {
     lar_solver solver;
-    var_index x = solver.add_var(0);
+    var_index x = solver.add_var(0, false);
-    var_index y = solver.add_var(1);
+    var_index y = solver.add_var(1, false);
     solver.add_var_bound(x, LE, -mpq(1));
     solver.add_var_bound(y, GE, mpq(0));
     vector<std::pair<mpq, var_index>> ls;
@@ -2758,9 +2765,9 @@ If b becomes basic variable, then it is likely the old solver ends up with a row
             return true; 
         };   
     lar_solver ls;
-    unsigned a = ls.add_var(0);
+    unsigned a = ls.add_var(0, false);
-    unsigned b = ls.add_var(1);
+    unsigned b = ls.add_var(1, false);
-    unsigned c = ls.add_var(2);
+    unsigned c = ls.add_var(2, false);
     vector<std::pair<mpq, var_index>> coeffs;
     coeffs.push_back(std::pair<mpq, var_index>(1, a));
     coeffs.push_back(std::pair<mpq, var_index>(-1, c));
@@ -2823,8 +2830,8 @@ If x9 becomes basic variable, then it is likely the old solver ends up with a ro
 }
 void test_bound_propagation_one_row() {
     lar_solver ls;
-    unsigned x0 = ls.add_var(0);
+    unsigned x0 = ls.add_var(0, false);
-    unsigned x1 = ls.add_var(1);
+    unsigned x1 = ls.add_var(1, false);
     vector<std::pair<mpq, var_index>> c;
     c.push_back(std::pair<mpq, var_index>(1, x0));
     c.push_back(std::pair<mpq, var_index>(-1, x1));
@@ -2837,8 +2844,8 @@ void test_bound_propagation_one_row() {
 } 
 void test_bound_propagation_one_row_with_bounded_vars() {
     lar_solver ls;
-    unsigned x0 = ls.add_var(0);
+    unsigned x0 = ls.add_var(0, false);
-    unsigned x1 = ls.add_var(1);
+    unsigned x1 = ls.add_var(1, false);
     vector<std::pair<mpq, var_index>> c;
     c.push_back(std::pair<mpq, var_index>(1, x0));
     c.push_back(std::pair<mpq, var_index>(-1, x1));
@@ -2853,8 +2860,8 @@ void test_bound_propagation_one_row_with_bounded_vars() {
 }
 void test_bound_propagation_one_row_mixed() {
     lar_solver ls;
-    unsigned x0 = ls.add_var(0);
+    unsigned x0 = ls.add_var(0, false);
-    unsigned x1 = ls.add_var(1);
+    unsigned x1 = ls.add_var(1, false);
     vector<std::pair<mpq, var_index>> c;
     c.push_back(std::pair<mpq, var_index>(1, x0));
     c.push_back(std::pair<mpq, var_index>(-1, x1));
@@ -2868,9 +2875,9 @@ void test_bound_propagation_one_row_mixed() {
 
 void test_bound_propagation_two_rows() {
     lar_solver ls;
-    unsigned x = ls.add_var(0);
+    unsigned x = ls.add_var(0, false);
-    unsigned y = ls.add_var(1);
+    unsigned y = ls.add_var(1, false);
-    unsigned z = ls.add_var(2);
+    unsigned z = ls.add_var(2, false);
     vector<std::pair<mpq, var_index>> c;
     c.push_back(std::pair<mpq, var_index>(1, x));
     c.push_back(std::pair<mpq, var_index>(2, y));
@@ -2892,9 +2899,9 @@ void test_bound_propagation_two_rows() {
 void test_total_case_u() {
     std::cout << "test_total_case_u\n";
     lar_solver ls;
-    unsigned x = ls.add_var(0);
+    unsigned x = ls.add_var(0, false);
-    unsigned y = ls.add_var(1);
+    unsigned y = ls.add_var(1, false);
-    unsigned z = ls.add_var(2);
+    unsigned z = ls.add_var(2, false);
     vector<std::pair<mpq, var_index>> c;
     c.push_back(std::pair<mpq, var_index>(1, x));
     c.push_back(std::pair<mpq, var_index>(2, y));
@@ -2918,9 +2925,9 @@ bool contains_j_kind(unsigned j, lconstraint_kind kind, const mpq & rs, const ve
 void test_total_case_l(){
     std::cout << "test_total_case_l\n";
     lar_solver ls;
-    unsigned x = ls.add_var(0);
+    unsigned x = ls.add_var(0, false);
-    unsigned y = ls.add_var(1);
+    unsigned y = ls.add_var(1, false);
-    unsigned z = ls.add_var(2);
+    unsigned z = ls.add_var(2, false);
     vector<std::pair<mpq, var_index>> c;
     c.push_back(std::pair<mpq, var_index>(1, x));
     c.push_back(std::pair<mpq, var_index>(2, y));

src/test/lp/lp_main.cpp

@@ -0,0 +1,14 @@
+void        gparams_register_modules(){}
+void mem_initialize() {}
+void mem_finalize() {}
+#include "util/rational.h"
+namespace lean {
+void test_lp_local(int argc, char**argv);
+}
+int main(int argn, char**argv){
+    rational::initialize();
+    lean::test_lp_local(argn, argv);
+    rational::finalize();
+    return 0;
+}
+

src/test/lp/smt_reader.h

@@ -376,7 +376,7 @@ namespace lean {
         void add_constraint_to_solver(lar_solver * solver, formula_constraint & fc) {
             vector<std::pair<mpq, var_index>> ls;
             for (auto & it : fc.m_coeffs) {
-                ls.push_back(std::make_pair(it.first, solver->add_var(register_name(it.second))));
+                ls.push_back(std::make_pair(it.first, solver->add_var(register_name(it.second), false)));
             }
             solver->add_constraint(ls, fc.m_kind, fc.m_right_side);
         }

src/util/lp/init_lar_solver.cpp

@@ -2,40 +2,44 @@
   Copyright (c) 2017 Microsoft Corporation
   Author: Lev Nachmanson
 */
+// this file represents the intiialization functionality of lar_solver
 
-// here we are inside lean::lar_solver class
 
-bool strategy_is_undecided() const {
+#include "util/lp/lar_solver.h"
+namespace lean {
+
+bool lar_solver::strategy_is_undecided() const {
     return m_settings.simplex_strategy() == simplex_strategy_enum::undecided;
 }
 
-var_index add_var(unsigned ext_j) {
+var_index lar_solver::add_var(unsigned ext_j, bool is_integer) {
     var_index i;
     lean_assert (ext_j < m_terms_start_index); 
 
     if (ext_j >= m_terms_start_index)
         throw 0; // todo : what is the right way to exit?
-            
+    auto it = m_ext_vars_to_columns.find(ext_j);
-    if (try_get_val(m_ext_vars_to_columns, ext_j, i)) {
+    if (it != m_ext_vars_to_columns.end()) {
-        return i;
+        return it->second.ext_j();
     }
     lean_assert(m_vars_to_ul_pairs.size() == A_r().column_count());
     i = A_r().column_count();
     m_vars_to_ul_pairs.push_back (ul_pair(static_cast<unsigned>(-1)));
     add_non_basic_var_to_core_fields(ext_j);
     lean_assert(sizes_are_correct());
+    lean_assert(!column_is_integer(i));
     return i;
 }
 
-void register_new_ext_var_index(unsigned ext_v) {
+void lar_solver::register_new_ext_var_index(unsigned ext_v) {
     lean_assert(!contains(m_ext_vars_to_columns, ext_v));
     unsigned j = static_cast<unsigned>(m_ext_vars_to_columns.size());
-    m_ext_vars_to_columns[ext_v] = j;
+    m_ext_vars_to_columns.insert(std::make_pair(ext_v, ext_var_info(j)));
     lean_assert(m_columns_to_ext_vars_or_term_indices.size() == j);
     m_columns_to_ext_vars_or_term_indices.push_back(ext_v);
 }
 
-void add_non_basic_var_to_core_fields(unsigned ext_j) {
+void lar_solver::add_non_basic_var_to_core_fields(unsigned ext_j) {
     register_new_ext_var_index(ext_j);
     m_mpq_lar_core_solver.m_column_types.push_back(column_type::free_column);
     m_columns_with_changed_bound.increase_size_by_one();
@@ -44,7 +48,7 @@ void add_non_basic_var_to_core_fields(unsigned ext_j) {
         add_new_var_to_core_fields_for_doubles(false);
 }
 
-void add_new_var_to_core_fields_for_doubles(bool register_in_basis) {
+void lar_solver::add_new_var_to_core_fields_for_doubles(bool register_in_basis) {
     unsigned j = A_d().column_count();
     A_d().add_column();
     lean_assert(m_mpq_lar_core_solver.m_d_x.size() == j);
@@ -63,7 +67,7 @@ void add_new_var_to_core_fields_for_doubles(bool register_in_basis) {
     }
 }
 
-void add_new_var_to_core_fields_for_mpq(bool register_in_basis) {
+void lar_solver::add_new_var_to_core_fields_for_mpq(bool register_in_basis) {
     unsigned j = A_r().column_count();
     A_r().add_column();
     lean_assert(m_mpq_lar_core_solver.m_r_x.size() == j);
@@ -88,25 +92,23 @@ void add_new_var_to_core_fields_for_mpq(bool register_in_basis) {
 }
 
 
-var_index add_term_undecided(const vector<std::pair<mpq, var_index>> & coeffs,
+var_index lar_solver::add_term_undecided(const vector<std::pair<mpq, var_index>> & coeffs,
                              const mpq &m_v) {
     m_terms.push_back(new lar_term(coeffs, m_v));
-    m_orig_terms.push_back(new lar_term(coeffs, m_v));
     return m_terms_start_index +  m_terms.size() - 1;
 }
 
 // terms
-var_index add_term(const vector<std::pair<mpq, var_index>> & coeffs,
+var_index lar_solver::add_term(const vector<std::pair<mpq, var_index>> & coeffs,
                    const mpq &m_v) {
     if (strategy_is_undecided())
         return add_term_undecided(coeffs, m_v);
 
     m_terms.push_back(new lar_term(coeffs, m_v));
-    m_orig_terms.push_back(new lar_term(coeffs, m_v));
     unsigned adjusted_term_index = m_terms.size() - 1;
     var_index ret = m_terms_start_index + adjusted_term_index;
     if (use_tableau() && !coeffs.empty()) {
-        add_row_for_term(m_orig_terms.back(), ret);
+        add_row_for_term(m_terms.back(), ret);
         if (m_settings.bound_propagation())
             m_rows_with_changed_bounds.insert(A_r().row_count() - 1);
     } 
@@ -114,13 +116,13 @@ var_index add_term(const vector<std::pair<mpq, var_index>> & coeffs,
     return ret;
 }
 
-void add_row_for_term(const lar_term * term, unsigned term_ext_index) {
+void lar_solver::add_row_for_term(const lar_term * term, unsigned term_ext_index) {
     lean_assert(sizes_are_correct());
     add_row_from_term_no_constraint(term, term_ext_index);
     lean_assert(sizes_are_correct());
 }
 
-void add_row_from_term_no_constraint(const lar_term * term, unsigned term_ext_index) {
+void lar_solver::add_row_from_term_no_constraint(const lar_term * term, unsigned term_ext_index) {
     register_new_ext_var_index(term_ext_index);
     // j will be a new variable
 	unsigned j = A_r().column_count();
@@ -140,7 +142,7 @@ void add_row_from_term_no_constraint(const lar_term * term, unsigned term_ext_in
         fill_last_row_of_A_d(A_d(), term);
 }
 
-void add_basic_var_to_core_fields() {
+void lar_solver::add_basic_var_to_core_fields() {
     bool use_lu = m_mpq_lar_core_solver.need_to_presolve_with_double_solver();
     lean_assert(!use_lu || A_r().column_count() == A_d().column_count());
     m_mpq_lar_core_solver.m_column_types.push_back(column_type::free_column);
@@ -151,7 +153,7 @@ void add_basic_var_to_core_fields() {
         add_new_var_to_core_fields_for_doubles(true);
 }
 
-constraint_index add_var_bound(var_index j, lconstraint_kind kind, const mpq & right_side)  {
+constraint_index lar_solver::add_var_bound(var_index j, lconstraint_kind kind, const mpq & right_side)  {
 	constraint_index ci = m_constraints.size();
     if (!is_term(j)) { // j is a var
         auto vc = new lar_var_constraint(j, kind, right_side);
@@ -164,7 +166,7 @@ constraint_index add_var_bound(var_index j, lconstraint_kind kind, const mpq & r
     return ci;
 }
 
-void update_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index) {
+void lar_solver::update_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index) {
     switch(m_mpq_lar_core_solver.m_column_types[j]) {
     case column_type::free_column:
         update_free_column_type_and_bound(j, kind, right_side, constr_index);
@@ -186,22 +188,32 @@ void update_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq
     }
 }
 
-void add_var_bound_on_constraint_for_term(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci) {
+void lar_solver::add_var_bound_on_constraint_for_term(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci) {
     lean_assert(is_term(j));
     unsigned adjusted_term_index = adjust_term_index(j);
-    unsigned term_j;
+    auto it = m_ext_vars_to_columns.find(j);
-    if (try_get_val(m_ext_vars_to_columns, j, term_j)) {
+    if (it != m_ext_vars_to_columns.end()) {
-        mpq rs = right_side - m_orig_terms[adjusted_term_index]->m_v;
+        unsigned term_j = it->second.ext_j();
-        m_constraints.push_back(new lar_term_constraint(m_orig_terms[adjusted_term_index], kind, right_side));
+        mpq rs = right_side - m_terms[adjusted_term_index]->m_v;
+        m_constraints.push_back(new lar_term_constraint(m_terms[adjusted_term_index], kind, right_side));
         update_column_type_and_bound(term_j, kind, rs, ci);
     }
     else {
-        add_constraint_from_term_and_create_new_column_row(j, m_orig_terms[adjusted_term_index], kind, right_side);
+        add_constraint_from_term_and_create_new_column_row(j, m_terms[adjusted_term_index], kind, right_side);
     }
 }
 
+constraint_index lar_solver::add_constraint(const vector<std::pair<mpq, var_index>>& left_side_with_terms, lconstraint_kind kind_par, const mpq& right_side_parm) {
+    vector<std::pair<mpq, var_index>> left_side;
+    mpq rs = - right_side_parm;
+    substitute_terms_in_linear_expression(left_side_with_terms, left_side, rs);
+    unsigned term_index = add_term(left_side, zero_of_type<mpq>());
+    constraint_index ci = m_constraints.size();
+    add_var_bound_on_constraint_for_term(term_index, kind_par, -rs, ci);
+    return ci;
+}
 
-void add_constraint_from_term_and_create_new_column_row(unsigned term_j, const lar_term* term,
+void lar_solver::add_constraint_from_term_and_create_new_column_row(unsigned term_j, const lar_term* term,
                                                         lconstraint_kind kind, const mpq & right_side) {
 
     add_row_from_term_no_constraint(term, term_j);
@@ -211,7 +223,7 @@ void add_constraint_from_term_and_create_new_column_row(unsigned term_j, const l
     lean_assert(A_r().column_count() == m_mpq_lar_core_solver.m_r_solver.m_costs.size());
 }
 
-void decide_on_strategy_and_adjust_initial_state() {
+void lar_solver::decide_on_strategy_and_adjust_initial_state() {
 	lean_assert(strategy_is_undecided());
 	if (m_vars_to_ul_pairs.size() > m_settings.column_number_threshold_for_using_lu_in_lar_solver) {
         m_settings.simplex_strategy() = simplex_strategy_enum::lu;
@@ -221,7 +233,7 @@ void decide_on_strategy_and_adjust_initial_state() {
     adjust_initial_state();
 }
 
-void adjust_initial_state() {
+void lar_solver::adjust_initial_state() {
     switch (m_settings.simplex_strategy()) {
     case simplex_strategy_enum::lu:
         adjust_initial_state_for_lu();
@@ -237,7 +249,7 @@ void adjust_initial_state() {
     }
 }
 
-void adjust_initial_state_for_lu() {
+void lar_solver::adjust_initial_state_for_lu() {
     copy_from_mpq_matrix(A_d());
 	unsigned n = A_d().column_count();
 	m_mpq_lar_core_solver.m_d_x.resize(n);
@@ -265,7 +277,7 @@ void adjust_initial_state_for_lu() {
         }*/
 }
 
-void adjust_initial_state_for_tableau_rows() {
+void lar_solver::adjust_initial_state_for_tableau_rows() {
     for (unsigned j = 0; j < m_terms.size(); j++) {
         if (contains(m_ext_vars_to_columns, j + m_terms_start_index))
             continue;
@@ -274,7 +286,7 @@ void adjust_initial_state_for_tableau_rows() {
 }
 
 // this fills the last row of A_d and sets the basis column: -1 in the last column of the row
-void fill_last_row_of_A_d(static_matrix<double, double> & A, const lar_term* ls) {
+void lar_solver::fill_last_row_of_A_d(static_matrix<double, double> & A, const lar_term* ls) {
     lean_assert(A.row_count() > 0);
     lean_assert(A.column_count() > 0);
     unsigned last_row = A.row_count() - 1;
@@ -290,7 +302,7 @@ void fill_last_row_of_A_d(static_matrix<double, double> & A, const lar_term* ls)
     A.set(last_row, basis_j, - 1 );
 }
 
-void update_free_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_ind) {
+void lar_solver::update_free_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_ind) {
     mpq y_of_bound(0);
     switch (kind) {
     case LT:
@@ -330,7 +342,7 @@ void update_free_column_type_and_bound(var_index j, lconstraint_kind kind, const
     m_columns_with_changed_bound.insert(j);
 }
 
-void update_upper_bound_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci) {
+void lar_solver::update_upper_bound_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci) {
     lean_assert(m_mpq_lar_core_solver.m_column_types()[j] == column_type::upper_bound);
     mpq y_of_bound(0);
     switch (kind) {
@@ -387,7 +399,7 @@ void update_upper_bound_column_type_and_bound(var_index j, lconstraint_kind kind
     }
 }
     
-void update_boxed_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci) {
+void lar_solver::update_boxed_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci) {
     lean_assert(m_status == INFEASIBLE || (m_mpq_lar_core_solver.m_column_types()[j] == column_type::boxed && m_mpq_lar_core_solver.m_r_low_bounds()[j] < m_mpq_lar_core_solver.m_r_upper_bounds()[j]));
     mpq y_of_bound(0);
     switch (kind) {
@@ -457,7 +469,7 @@ void update_boxed_column_type_and_bound(var_index j, lconstraint_kind kind, cons
                 
     }
 }
-void update_low_bound_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci) {
+void lar_solver::update_low_bound_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci) {
     lean_assert(m_mpq_lar_core_solver.m_column_types()[j] == column_type::low_bound);
     mpq y_of_bound(0);
     switch (kind) {
@@ -513,7 +525,7 @@ void update_low_bound_column_type_and_bound(var_index j, lconstraint_kind kind,
     }
 }
 
-void update_fixed_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci) {
+void lar_solver::update_fixed_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci) {
     lean_assert(m_status == INFEASIBLE || (m_mpq_lar_core_solver.m_column_types()[j] == column_type::fixed && m_mpq_lar_core_solver.m_r_low_bounds()[j] == m_mpq_lar_core_solver.m_r_upper_bounds()[j]));
     lean_assert(m_status == INFEASIBLE || (m_mpq_lar_core_solver.m_r_low_bounds()[j].y.is_zero() && m_mpq_lar_core_solver.m_r_upper_bounds()[j].y.is_zero()));
     auto v = numeric_pair<mpq>(right_side, mpq(0));
@@ -574,3 +586,4 @@ void update_fixed_column_type_and_bound(var_index j, lconstraint_kind kind, cons
     }
 }
     
+}

src/util/lp/int_solver.cpp

@@ -0,0 +1,6 @@
+/*
+  Copyright (c) 2017 Microsoft Corporation
+  Author: Lev Nachmanson
+*/
+
+#include "util/lp/int_solver.h"

src/util/lp/int_solver.h

@@ -0,0 +1,44 @@
+/*
+  Copyright (c) 2017 Microsoft Corporation
+  Author: Lev Nachmanson
+*/
+#pragma once
+#include "util/lp/lp_settings.h"
+class lemma; // forward definition
+namespace lean {
+class lar_solver;
+template <typename T, typename X>
+struct lp_constraint;
+
+class int_solver {
+public:
+    lar_solver *m_solver;
+    
+    int_solver(lar_solver* lp);
+    bool check();// main function to check that solution provided by lar_solver is valid for integral values or can be adjusted.
+private:
+
+    // how to tighten bounds for integer variables.
+    
+    
+    // gcd test
+    // 5*x + 3*y + 6*z = 5
+    // suppose x is fixed at 2.
+    // so we have 10 + 3(y + 2z) = 5
+    //             5 = -3(y + 2z)
+    // this is unsolvable because 5/3 is not an integer.
+    // so we create a lemma that rules out this condition.
+    // 
+    bool gcd_test(lemma& lemma); // returns false in case of failure. Creates a theory lemma in case of failure.
+
+    // create goromy cuts
+    // either creates a conflict or a bound.
+
+    // branch and bound: 
+    // decide what to branch and bound on
+    // creates a fresh inequality.
+
+    bool branch(const lp_constraint<mpq, mpq> & new_inequality);
+    
+};
+}

src/util/lp/lar_solver_instances.cpp

@@ -0,0 +1,17 @@
+/*
+  Copyright (c) 2017 Microsoft Corporation
+  Author: Lev Nachmanson
+*/
+
+#include "util/lp/lar_solver.cpp"
+#include "util/lp/init_lar_solver.cpp"
+
+
+
+
+template void  lean::lar_solver::copy_from_mpq_matrix<double,double>(class lean::static_matrix<double,double> &);
+
+
+
+
+

src/util/lp/lp_settings.h

@@ -16,6 +16,17 @@ namespace lean {
 typedef unsigned var_index;
 typedef unsigned constraint_index;
 typedef unsigned row_index;
+
+enum class final_check_status {
+    DONE,
+    CONTINUE,
+    UNSAT,
+    GIVEUP
+};
+
+typedef vector<std::pair<mpq, constraint_index>> explanation_t;
+
+
 enum class column_type  {
     free_column = 0,
         low_bound = 1,

src/util/lp/mps_reader.h

@@ -810,7 +810,7 @@ public:
             auto kind = get_lar_relation_from_row(row->m_type);
             vector<std::pair<mpq, var_index>> ls;
             for (auto s : row->m_row_columns) {
-                var_index i = solver->add_var(get_var_index(s.first));
+                var_index i = solver->add_var(get_var_index(s.first), false);
                 ls.push_back(std::make_pair(s.second, i));
             }
             solver->add_constraint(ls, kind, row->m_right_side);
@@ -828,20 +828,20 @@ public:
 
     void create_low_constraint_for_var(column* col, bound * b, lar_solver *solver) {
         vector<std::pair<mpq, var_index>> ls;
-        var_index i = solver->add_var(col->m_index);
+        var_index i = solver->add_var(col->m_index, false);
         ls.push_back(std::make_pair(numeric_traits<T>::one(), i));
         solver->add_constraint(ls, GE, b->m_low);
     }
 
     void create_upper_constraint_for_var(column* col, bound * b, lar_solver *solver) {
-        var_index i = solver->add_var(col->m_index);
+        var_index i = solver->add_var(col->m_index, false);
         vector<std::pair<mpq, var_index>> ls;
         ls.push_back(std::make_pair(numeric_traits<T>::one(), i));
         solver->add_constraint(ls, LE, b->m_upper);
     }
 
     void create_equality_contraint_for_var(column* col, bound * b, lar_solver *solver) {
-        var_index i = solver->add_var(col->m_index);
+        var_index i = solver->add_var(col->m_index, false);
         vector<std::pair<mpq, var_index>> ls;
         ls.push_back(std::make_pair(numeric_traits<T>::one(), i));
         solver->add_constraint(ls, EQ, b->m_fixed_value);
@@ -850,7 +850,7 @@ public:
     void fill_lar_solver_on_columns(lar_solver * solver) {
         for (auto s : m_columns) {
             mps_reader::column * col = s.second;
-            solver->add_var(col->m_index);
+            solver->add_var(col->m_index, false);
             auto b = col->m_bound;
             if (b == nullptr) return;
 

src/util/lp/nra_solver.cpp

@@ -0,0 +1,262 @@
+/*
+  Copyright (c) 2017 Microsoft Corporation
+  Author: Lev Nachmanson
+*/
+
+#pragma once
+#include "util/lp/lar_solver.h"
+#include "util/lp/nra_solver.h"
+#include "nlsat/nlsat_solver.h"
+#include "math/polynomial/polynomial.h"
+#include "math/polynomial/algebraic_numbers.h"
+#include "util/map.h"
+
+
+namespace nra {
+
+    struct solver::imp {
+        lean::lar_solver& s;
+        reslimit&      m_limit;  // TBD: extract from lar_solver
+        params_ref     m_params; // TBD: pass from outside
+        u_map<polynomial::var> m_lp2nl;  // map from lar_solver variables to nlsat::solver variables
+        nlsat::solver m_nlsat;
+
+        struct mon_eq {
+            mon_eq(lean::var_index v, unsigned sz, lean::var_index const* vs):
+                m_v(v), m_vs(sz, vs) {}
+            lean::var_index          m_v;
+            svector<lean::var_index> m_vs;
+        };
+
+        vector<mon_eq>                   m_monomials;
+        unsigned_vector                  m_lim;
+        mutable std::unordered_map<lean::var_index, rational> m_variable_values; // current model
+
+        imp(lean::lar_solver& s, reslimit& lim, params_ref const& p): 
+            s(s), 
+            m_limit(lim),
+            m_params(p),
+            m_nlsat(m_limit, m_params) {
+        }
+
+        bool need_check() {
+            return !m_monomials.empty() && !check_assignments();
+        }
+
+        void add(lean::var_index v, unsigned sz, lean::var_index const* vs) {
+            m_monomials.push_back(mon_eq(v, sz, vs));
+        }
+
+        void push() {
+            m_lim.push_back(m_monomials.size());
+        }
+
+        void pop(unsigned n) {
+            if (n == 0) return;
+            m_monomials.shrink(m_lim[m_lim.size() - n]);
+            m_lim.shrink(m_lim.size() - n);       
+        }
+
+        /*
+          \brief Check if polynomials are well defined.
+          multiply values for vs and check if they are equal to value for v.
+          epsilon has been computed.
+        */
+        bool check_assignment(mon_eq const& m) const {
+            rational r1 = m_variable_values[m.m_v];
+            rational r2(1);
+            for (auto w : m.m_vs) {
+                r2 *= m_variable_values[w];
+            }
+            return r1 == r2;
+        }
+
+        bool check_assignments() const {
+            s.get_model(m_variable_values);
+            for (auto const& m : m_monomials) {
+                if (!check_assignment(m)) return false;
+            }
+            return true;
+        }
+
+
+        /**
+           \brief one-shot nlsat check.
+           A one shot checker is the least functionality that can 
+           enable non-linear reasoning. 
+           In addition to checking satisfiability we would also need
+           to identify equalities in the model that should be assumed
+           with the remaining solver.
+           
+           TBD: use partial model from lra_solver to prime the state of nlsat_solver.
+        */
+        lbool check(lean::explanation_t& ex) {
+            SASSERT(need_check());
+            m_nlsat.reset();
+            m_lp2nl.reset();
+            vector<nlsat::assumption, false> core;
+
+            // add linear inequalities from lra_solver
+            for (unsigned i = 0; i < s.constraint_count(); ++i) {
+                add_constraint(i);
+            }
+
+            // add polynomial definitions.
+            for (auto const& m : m_monomials) {
+                add_monomial_eq(m);
+            }
+            // TBD: add variable bounds?
+
+            lbool r = m_nlsat.check(); 
+            TRACE("arith", m_nlsat.display(tout << r << "\n"););
+            switch (r) {
+            case l_true: 
+                break;
+            case l_false: 
+                ex.reset();
+                m_nlsat.get_core(core);
+                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;
+
+            case l_undef:
+                break;
+            }            
+            return r;
+        }                
+
+        void add_monomial_eq(mon_eq const& m) {
+            polynomial::manager& pm = m_nlsat.pm();
+            svector<polynomial::var> vars;
+            for (auto v : m.m_vs) {
+                vars.push_back(lp2nl(v));
+            }
+            polynomial::monomial_ref m1(pm.mk_monomial(vars.size(), vars.c_ptr()), pm);
+            polynomial::monomial_ref m2(pm.mk_monomial(lp2nl(m.m_v), 1), pm);
+            polynomial::monomial* mls[2] = { m1, m2 };
+            polynomial::scoped_numeral_vector coeffs(pm.m());
+            coeffs.push_back(mpz(1));
+            coeffs.push_back(mpz(-1));
+            polynomial::polynomial_ref p(pm.mk_polynomial(2, coeffs.c_ptr(), mls),  pm);
+            polynomial::polynomial* ps[1] = { p };
+            bool even[1] = { false };
+            nlsat::literal lit = m_nlsat.mk_ineq_literal(nlsat::atom::kind::EQ, 1, ps, even);
+            m_nlsat.mk_clause(1, &lit, 0);
+        }
+
+        void add_constraint(unsigned idx) {
+            auto& c = s.get_constraint(idx);
+            auto& pm = m_nlsat.pm();
+            auto k = c.m_kind;
+            auto rhs = c.m_right_side;
+            auto lhs = c.get_left_side_coefficients();
+            auto sz = lhs.size();
+            svector<polynomial::var> vars;
+            rational den = denominator(rhs);
+            for (auto kv : lhs) {
+                vars.push_back(lp2nl(kv.second));
+                den = lcm(den, denominator(kv.first));
+            }
+            vector<rational> coeffs;
+            for (auto kv : lhs) {
+                coeffs.push_back(den * kv.first);
+            }
+            rhs *= den;
+            polynomial::polynomial_ref p(pm.mk_linear(sz, coeffs.c_ptr(), vars.c_ptr(), -rhs), pm);
+            polynomial::polynomial* ps[1] = { p };
+            bool is_even[1] = { false };
+            nlsat::literal lit;
+            switch (k) {
+            case lean::lconstraint_kind::LE:
+                lit = ~m_nlsat.mk_ineq_literal(nlsat::atom::kind::GT, 1, ps, is_even);
+                break;
+            case lean::lconstraint_kind::GE:
+                lit = ~m_nlsat.mk_ineq_literal(nlsat::atom::kind::LT, 1, ps, is_even);
+                break;
+            case lean::lconstraint_kind::LT:
+                lit = m_nlsat.mk_ineq_literal(nlsat::atom::kind::LT, 1, ps, is_even);
+                break;
+            case lean::lconstraint_kind::GT:
+                lit = m_nlsat.mk_ineq_literal(nlsat::atom::kind::GT, 1, ps, is_even);
+                break;
+            case lean::lconstraint_kind::EQ:
+                lit = m_nlsat.mk_ineq_literal(nlsat::atom::kind::EQ, 1, ps, is_even);
+                break;
+            }
+
+            nlsat::assumption a = this + idx;
+            m_nlsat.mk_clause(1, &lit, a);
+        }               
+
+        bool is_int(lean::var_index v) {
+            // TBD: is it s.column_is_integer(v), if then the function should take a var_index and not unsigned; s.is_int(v);
+            return false;
+        }
+
+
+        polynomial::var lp2nl(lean::var_index v) {
+            polynomial::var r;
+            if (!m_lp2nl.find(v, r)) {
+                r = m_nlsat.mk_var(is_int(v));
+                m_lp2nl.insert(v, r);
+            }
+            return r;
+        }
+
+        nlsat::anum const& value(lean::var_index v) const {
+           return m_nlsat.value(m_lp2nl.find(v));
+        }
+
+        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, reslimit& lim, params_ref const& p) {
+        m_imp = alloc(imp, s, lim, p);
+    }
+
+    solver::~solver() {
+        dealloc(m_imp);
+    }
+
+    void solver::add_monomial(lean::var_index v, unsigned sz, lean::var_index const* vs) {
+        m_imp->add(v, sz, vs);
+    }
+
+    lbool solver::check(lean::explanation_t& ex) {
+        return m_imp->check(ex);
+    }
+
+    bool solver::need_check() {
+        return m_imp->need_check();
+    }
+
+    void solver::push() {
+        m_imp->push();
+    }
+
+    void solver::pop(unsigned n) {
+        m_imp->pop(n);
+    }
+
+    std::ostream& solver::display(std::ostream& out) const {
+        return m_imp->display(out);
+    }
+
+    nlsat::anum const& solver::value(lean::var_index v) const {
+        return m_imp->value(v);
+    }
+
+}

src/util/lp/nra_solver.h

@@ -0,0 +1,68 @@
+/*
+  Copyright (c) 2017 Microsoft Corporation
+  Author: Lev Nachmanson
+*/
+
+#pragma once
+#include "util/vector.h"
+#include "util/lp/lp_settings.h"
+#include "util/rlimit.h"
+#include "util/params.h"
+#include "nlsat/nlsat_solver.h"
+
+namespace lean {
+    class lar_solver;
+}
+
+
+namespace nra {
+
+
+
+    class solver {
+        struct imp;
+        imp* m_imp;
+
+    public:
+
+        solver(lean::lar_solver& s, reslimit& lim, params_ref const& p = params_ref());
+        
+        ~solver();
+
+        /*
+          \brief Add a definition v = vs[0]*vs[1]*...*vs[sz-1]
+          The variable v is equal to the product of variables vs.
+        */
+        void add_monomial(lean::var_index v, unsigned sz, lean::var_index const* vs);
+
+        /*
+          \brief Check feasiblity of linear constraints augmented by polynomial definitions
+          that are added.
+         */
+        lbool check(lean::explanation_t& ex);
+
+        /*
+          \brief determine whether nra check is needed.
+        */
+        bool need_check();
+
+        /*
+          \brief Access model.
+        */
+        nlsat::anum const& value(lean::var_index v) const;
+
+        /*
+          \brief push and pop scope. 
+          Monomial definitions are retraced when popping scope.
+        */
+        void push();
+        
+        void pop(unsigned n);
+
+        /*
+          \brief display state
+         */
+        std::ostream& display(std::ostream& out) const;
+
+    };
+}

src/util/lp/quick_xplain.cpp

@@ -20,7 +20,7 @@ void quick_xplain::copy_constraint_and_add_constraint_vars(const lar_constraint&
     vector < std::pair<mpq, unsigned>> ls;
     for (auto & p : lar_c.get_left_side_coefficients()) {
         unsigned j = p.second;
-        unsigned lj = m_qsol.add_var(j);
+        unsigned lj = m_qsol.add_var(j, false);
         ls.push_back(std::make_pair(p.first, lj));
     }
     m_constraints_in_local_vars.push_back(lar_constraint(ls, lar_c.m_kind, lar_c.m_right_side));
@@ -94,7 +94,7 @@ bool quick_xplain::is_feasible(const vector<unsigned> & x, unsigned k) const {
         vector < std::pair<mpq, unsigned>> ls;
         const lar_constraint & c = m_constraints_in_local_vars[i];
         for (auto & p : c.get_left_side_coefficients()) {
-            unsigned lj = l.add_var(p.second);
+            unsigned lj = l.add_var(p.second, false);
             ls.push_back(std::make_pair(p.first, lj));
         }
         l.add_constraint(ls, c.m_kind, c.m_right_side);