Moving the enum ArithType to partial_model. Adding a new type Unset in the enum. Always initializing VarInfo::d_type. (#1333)

3 files changed, 37 insertions, 43 deletions

diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index 4a9539d49..cfaf6ac03 100644
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -66,21 +66,6 @@ inline Node skolemFunction(const std::string& name, TypeNode dom, TypeNode range
   return currNM->mkSkolem(name, functionType);
 }
 
-/**
- * (For the moment) the type hierarchy goes as:
- * Integer <: Real
- * The type number of a variable is an integer representing the most specific
- * type of the variable. The possible values of type number are:
- */
-enum ArithType {
-  ATReal = 0,
-  ATInteger = 1
-};
-
-inline ArithType nodeToArithType(TNode x) {
-  return (x.getType().isInteger() ? ATInteger : ATReal);
-}
-
 /** \f$ k \in {LT, LEQ, EQ, GEQ, GT} \f$ */
 inline bool isRelationOperator(Kind k){
   using namespace kind;
diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp
index 2c50a1b1d..8d4e8c5f9 100644
--- a/src/theory/arith/partial_model.cpp
+++ b/src/theory/arith/partial_model.cpp
@@ -108,7 +108,7 @@ ArithVariables::var_iterator ArithVariables::var_end() const {
   return var_iterator(&d_vars, d_vars.end());
 }
 bool ArithVariables::isInteger(ArithVar x) const {
-  return d_vars[x].d_type >= ATInteger;
+  return d_vars[x].d_type >= ArithType::Integer;
 }
 
 /** Is the assignment to x integral? */
@@ -124,16 +124,16 @@ bool ArithVariables::isIntegerInput(ArithVar x) const {
 }
 
 ArithVariables::VarInfo::VarInfo()
-  : d_var(ARITHVAR_SENTINEL),
-    d_assignment(0),
-    d_lb(NullConstraint),
-    d_ub(NullConstraint),
-    d_cmpAssignmentLB(1),
-    d_cmpAssignmentUB(-1),
-    d_pushCount(0),
-    d_node(Node::null()),
-    d_auxiliary(false)
-{ }
+    : d_var(ARITHVAR_SENTINEL),
+      d_assignment(0),
+      d_lb(NullConstraint),
+      d_ub(NullConstraint),
+      d_cmpAssignmentLB(1),
+      d_cmpAssignmentUB(-1),
+      d_pushCount(0),
+      d_type(ArithType::Unset),
+      d_node(Node::null()),
+      d_auxiliary(false) {}
 
 bool ArithVariables::VarInfo::initialized() const {
   return d_var != ARITHVAR_SENTINEL;
@@ -154,13 +154,14 @@ void ArithVariables::VarInfo::initialize(ArithVar v, Node n, bool aux){
     //integral.
     //We'll use the isIntegral check from the polynomial package instead.
     Polynomial p = Polynomial::parsePolynomial(n);
-    d_type = p.isIntegral() ? ATInteger : ATReal;
+    d_type = p.isIntegral() ? ArithType::Integer : ArithType::Real;
   }else{
-    d_type = nodeToArithType(n);
+    d_type = n.getType().isInteger() ? ArithType::Integer : ArithType::Real;
   }
 
   Assert(initialized());
 }
+
 void ArithVariables::VarInfo::uninitialize(){
   d_var = ARITHVAR_SENTINEL;
   d_node = Node::null();
diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h
index 50fb2cb48..47a1c2d42 100644
--- a/src/theory/arith/partial_model.h
+++ b/src/theory/arith/partial_model.h
@@ -18,30 +18,37 @@
 
 #include "cvc4_private.h"
 
-#include "expr/node.h"
-
-#include "context/context.h"
-#include "context/cdlist.h"
+#ifndef __CVC4__THEORY__ARITH__PARTIAL_MODEL_H
+#define __CVC4__THEORY__ARITH__PARTIAL_MODEL_H
 
+#include <list>
+#include <vector>
 
-#include "theory/arith/arithvar.h"
+#include "context/cdlist.h"
+#include "context/context.h"
+#include "expr/node.h"
 #include "theory/arith/arith_utilities.h"
-#include "theory/arith/delta_rational.h"
-#include "theory/arith/constraint_forward.h"
-#include "theory/arith/callbacks.h"
+#include "theory/arith/arithvar.h"
 #include "theory/arith/bound_counts.h"
-
-
-#include <vector>
-#include <list>
-
-#pragma once
+#include "theory/arith/callbacks.h"
+#include "theory/arith/constraint_forward.h"
+#include "theory/arith/delta_rational.h"
 
 namespace CVC4 {
 namespace theory {
 namespace arith {
 
-
+/**
+ * (For the moment) the type hierarchy goes as:
+ * Integer <: Real
+ * The type number of a variable is an integer representing the most specific
+ * type of the variable. The possible values of type number are:
+ */
+enum class ArithType {
+  Unset,
+  Real,
+  Integer,
+};
 
 class ArithVariables {
 private:
@@ -409,3 +416,4 @@ private:
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
 
+#endif /* __CVC4__THEORY__ARITH__PARTIAL_MODEL_H */