merge and update

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

src/math/polynomial/polynomial.h

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

src/sat/sat_types.h

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

src/util/lp/lar_solver.h

@@ -31,6 +31,7 @@
 #include "util/lp/quick_xplain.h"
 #include "util/lp/conversion_helper.h"
 #include "util/lp/int_solver.h"
+#include "util/lp/nra_solver.h"
 
 namespace lean {
 
@@ -200,9 +201,7 @@ public:
 
     void set_status(lp_status s);
 
-    lp_status find_feasible_solution();
-   
-    void add_monomial(var_index v, svector<var_index> const& vars);
+    lp_status find_feasible_solution();   
     
     lp_status solve();
 
@@ -414,6 +413,7 @@ public:
         const impq & v = m_mpq_lar_core_solver.m_r_x[j];
         return impq_is_int(v);
     }
+
     inline bool column_is_real(unsigned j) const { return !column_is_integer(j); }	
 	final_check_status check_int_feasibility();
 };

src/util/lp/nra_solver.cpp

@@ -121,6 +121,7 @@ namespace nra {
                     TRACE("arith", tout << "ex: " << idx << "\n";);
                 }
                 break;
+
             case l_undef:
                 break;
             }            

src/util/lp/nra_solver.h

@@ -17,7 +17,7 @@ namespace lean {
 
 namespace nra {
 
-    typedef std::unordered_map<lean::var_index, rational> nra_model_t;
+
 
     class solver {
         struct imp;