fixplex

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

src/CMakeLists.txt

@@ -37,9 +37,9 @@ endforeach()
 add_subdirectory(util)
 add_subdirectory(math/polynomial)
 add_subdirectory(math/dd)
-add_subdirectory(math/polysat)
 add_subdirectory(math/hilbert)
 add_subdirectory(math/simplex)
+add_subdirectory(math/polysat)
 add_subdirectory(math/automata)
 add_subdirectory(math/interval)
 add_subdirectory(math/realclosure)

src/math/polysat/CMakeLists.txt

@@ -10,4 +10,5 @@ z3_add_component(polysat
   COMPONENT_DEPENDENCIES
     util
     dd
+    simplex
 )

src/math/polysat/solver.cpp

@@ -18,6 +18,7 @@ Author:
 
 #include "math/polysat/solver.h"
 #include "math/polysat/log.h"
+#include "math/polysat/fixplex_def.h"
 
 namespace polysat {
 
@@ -69,6 +70,8 @@ namespace polysat {
         m_bdd(1000),
         m_dm(m_value_manager, m_alloc),
         m_free_vars(m_activity) {
+
+        fixplex<uint64_ext> s(m_lim);
     }
 
     solver::~solver() {}

src/math/polysat/solver.h

@@ -25,6 +25,7 @@ Author:
 #include "math/polysat/ule_constraint.h"
 #include "math/polysat/justification.h"
 #include "math/polysat/trail.h"
+#include "math/polysat/fixplex.h"
 
 namespace polysat {
 

src/math/simplex/sparse_matrix.h

@@ -201,6 +201,16 @@ namespace simplex {
         row_iterator row_begin(row const& r) { return row_iterator(m_rows[r.id()], true); }
         row_iterator row_end(row const& r) { return row_iterator(m_rows[r.id()], false); }
 
+        struct row_entries_t {
+            sparse_matrix& m;
+            row const& r;
+            row_entries_t(sparse_matrix & m, row const& r): m(m), r(r) {}
+            row_iterator begin() { return m.row_begin(r); }
+            row_iterator end() { return m.row_end(r); }
+        };
+
+        row_entries_t row_entries(row const& r) { return row_entries_t(*this, r); }
+
         unsigned column_size(var_t v) const { return m_columns[v].size(); }
 
         class col_iterator {

src/util/mpz.cpp

@@ -84,6 +84,13 @@ inline uint32_t _trailing_zeros32(uint32_t x) {
 #endif
 #endif
 
+unsigned trailing_zeros(uint32_t x) {
+    return static_cast<unsigned>(_trailing_zeros32(x));
+}
+
+unsigned trailing_zeros(uint64_t x) {
+    return static_cast<unsigned>(_trailing_zeros64(x));
+}
 
 #define _bit_min(x, y) (y + ((x - y) & ((int)(x - y) >> 31)))
 #define _bit_max(x, y) (x - ((x - y) & ((int)(x - y) >> 31)))

src/util/mpz.h

@@ -29,6 +29,9 @@ Revision History:
 
 unsigned u_gcd(unsigned u, unsigned v);
 uint64_t u64_gcd(uint64_t u, uint64_t v);
+unsigned trailing_zeros(uint64_t);
+unsigned trailing_zeros(uint32_t);
+
 
 #ifdef _MP_GMP
 typedef unsigned digit_t;