Merge pull request #1732 from levnach/upbranch

fix in theory_lra.cpp get_value

src/smt/theory_lra.cpp

@@ -1168,7 +1168,9 @@ public:
         if (m_variable_values.count(vi) > 0)
             return m_variable_values[vi];
         
-        SASSERT (m_solver->is_term(vi));
+        if(!m_solver->is_term(vi))
+            return rational::zero();
+        
         m_todo_terms.push_back(std::make_pair(vi, rational::one()));
         rational result(0);
         while (!m_todo_terms.empty()) {

src/util/lp/lar_solver.cpp

@@ -1507,11 +1507,6 @@ bool lar_solver::column_is_fixed(unsigned j) const {
     return m_mpq_lar_core_solver.column_is_fixed(j);
 }
 
-    
-bool lar_solver::ext_var_is_int(var_index ext_var) const {
-    return m_var_register.external_is_int(ext_var);
-}
-
 // below is the initialization functionality of lar_solver
 
 bool lar_solver::strategy_is_undecided() const {

src/util/lp/lar_solver.h

@@ -155,8 +155,6 @@ public:
 
     bool var_is_int(var_index v) const;
 
-    bool ext_var_is_int(var_index ext_var) const;
-    
     void add_non_basic_var_to_core_fields(unsigned ext_j, bool is_int);
 
     void add_new_var_to_core_fields_for_doubles(bool register_in_basis);

src/util/lp/var_register.h

@@ -19,19 +19,19 @@ Revision History:
 #pragma once
 namespace lp  {
 class ext_var_info {
-    unsigned m_internal_j; // the internal index
+    unsigned m_external_j; // the internal index
     bool m_is_integer;
 public:
     ext_var_info() {}
     ext_var_info(unsigned j): ext_var_info(j, true) {}
-    ext_var_info(unsigned j , bool is_int) : m_internal_j(j), m_is_integer(is_int) {}
+    ext_var_info(unsigned j , bool is_int) : m_external_j(j), m_is_integer(is_int) {}
-    unsigned internal_j() const { return m_internal_j;}
+    unsigned external_j() const { return m_external_j;}
     bool is_integer() const {return m_is_integer;}
 };
 
 class var_register {
-    svector<unsigned> m_local_to_external;
+    svector<ext_var_info> m_local_to_external;
-    std::unordered_map<unsigned, ext_var_info> m_external_to_local;
+    std::unordered_map<unsigned, unsigned> m_external_to_local;
 public:
     unsigned add_var(unsigned user_var) {
         return add_var(user_var, true);
@@ -39,19 +39,23 @@ public:
     unsigned add_var(unsigned user_var, bool is_int) {
         auto t = m_external_to_local.find(user_var);
         if (t != m_external_to_local.end()) {
-            return t->second.internal_j();
+            return t->second;
         }
 
-        unsigned j = size();
+        m_local_to_external.push_back(ext_var_info(user_var, is_int));
-        m_external_to_local[user_var] = ext_var_info(j, is_int);
+        return m_external_to_local[user_var] = size() - 1;
-        m_local_to_external.push_back(user_var);
-        return j;
     }
 
-    const svector<unsigned> & vars() const { return m_local_to_external; }
+    svector<unsigned> vars() const {
+        svector<unsigned> ret;
+        for (const auto& p : m_local_to_external) {
+            ret.push_back(p.external_j());
+        }
+        return ret;
+    }
     
     unsigned local_to_external(unsigned local_var) const {
-        return m_local_to_external[local_var];
+        return m_local_to_external[local_var].external_j();
     }
     unsigned size() const {
         return m_local_to_external.size();
@@ -64,13 +68,7 @@ public:
     unsigned external_to_local(unsigned j) const {
         auto it = m_external_to_local.find(j);
         lp_assert(it != m_external_to_local.end());
-        return it->second.internal_j();
+        return it->second;
-    }
-
-    bool external_is_int(unsigned j) const {
-        auto it = m_external_to_local.find(j);
-        lp_assert(it != m_external_to_local.end());
-        return it->second.is_integer();
     }
 
     bool external_is_used(unsigned ext_j) const {
@@ -82,7 +80,7 @@ public:
         auto it = m_external_to_local.find(ext_j);
         if ( it == m_external_to_local.end())
             return false;
-        local_j = it->second.internal_j();
+        local_j = it->second;
         return true;
     }
 
@@ -90,19 +88,19 @@ public:
         auto it = m_external_to_local.find(ext_j);
         if ( it == m_external_to_local.end())
             return false;
-        local_j = it->second.internal_j();
+        local_j = it->second;
-        is_int = it->second.is_integer();
+        is_int = m_local_to_external[local_j].is_integer();
         return true;
     }
 
     
     bool local_is_int(unsigned j) const {
-        return external_is_int(m_local_to_external[j]);
+        return m_local_to_external[j].is_integer();
     }
 
     void shrink(unsigned shrunk_size) {
         for (unsigned j = size(); j-- > shrunk_size;) {
-            m_external_to_local.erase(m_local_to_external[j]);
+            m_external_to_local.erase(m_local_to_external[j].external_j());
         }
         m_local_to_external.resize(shrunk_size);
     }