From 76b11f2d122ae1070bd982a9380d6b09aae424c7 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 21 Mar 2014 15:06:31 -0700
Subject: [PATCH] improved SLS

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/simplex/simplex_def.h | 3 +++
 src/smt/theory_diff_logic.cpp  | 2 ++
 src/smt/theory_pb.cpp          | 3 +++
 src/smt/theory_pb.h            | 2 +-
 4 files changed, 9 insertions(+), 1 deletion(-)

diff --git a/src/math/simplex/simplex_def.h b/src/math/simplex/simplex_def.h
index 0e00e368b..c3a2bef95 100644
--- a/src/math/simplex/simplex_def.h
+++ b/src/math/simplex/simplex_def.h
@@ -25,6 +25,9 @@ Notes:
 
 namespace simplex {
 
+    template<typename Ext>
+    const typename simplex<Ext>::var_t simplex<Ext>::null_var = UINT_MAX; 
+
     template<typename Ext>
     typename simplex<Ext>::row 
     simplex<Ext>::add_row(var_t base_var, unsigned num_vars, var_t const* vars, numeral const* coeffs) {
diff --git a/src/smt/theory_diff_logic.cpp b/src/smt/theory_diff_logic.cpp
index a68b7782b..cb1812f9f 100644
--- a/src/smt/theory_diff_logic.cpp
+++ b/src/smt/theory_diff_logic.cpp
@@ -28,5 +28,7 @@ template class theory_diff_logic<idl_ext>;
 template class theory_diff_logic<sidl_ext>;
 template class theory_diff_logic<rdl_ext>;
 template class theory_diff_logic<srdl_ext>;
+template class simplex::simplex<simplex::mpq_ext>;
+
 
 };
diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
index 7976e27b3..ef7d6aff8 100644
--- a/src/smt/theory_pb.cpp
+++ b/src/smt/theory_pb.cpp
@@ -61,6 +61,9 @@ namespace smt {
         };
     };
 
+    const unsigned theory_pb::null_index = UINT_MAX;
+
+
     unsigned theory_pb::arg_t::get_hash() const {
         return get_composite_hash<arg_t, arg_t::kind_hash, arg_t::child_hash>(*this, size());
     }
diff --git a/src/smt/theory_pb.h b/src/smt/theory_pb.h
index 46c68900a..595cf5e6e 100644
--- a/src/smt/theory_pb.h
+++ b/src/smt/theory_pb.h
@@ -272,7 +272,7 @@ namespace smt {
 
         // bool_var |-> index into m_lemma
         unsigned_vector   m_conseq_index;
-        static const unsigned null_index = UINT_MAX;
+        static const unsigned null_index;
         bool is_marked(bool_var v) const;
         void set_mark(bool_var v, unsigned idx);
         void unset_mark(bool_var v);