variety of visibility fixes (should clean up some of the many warnings on MacOS-production-dynamic builds)

14 files changed, 35 insertions, 4 deletions

diff --git a/src/theory/arith/ordered_set.h b/src/theory/arith/ordered_set.h
index c126ab568..e3eebae5c 100644
--- a/src/theory/arith/ordered_set.h
+++ b/src/theory/arith/ordered_set.h
@@ -17,6 +17,11 @@
  ** \todo document this file
  **/
 
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__ARITH__ORDERED_SET_H
+#define __CVC4__THEORY__ARITH__ORDERED_SET_H
+
 #include <map>
 #include <set>
 #include "expr/kind.h"
@@ -114,3 +119,5 @@ typedef std::set<TNode, RightHandRationalLT> EqualValueSet;
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__ARITH__ORDERED_SET_H */
diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h
index aa333046b..9c5e343ef 100644
--- a/src/theory/arith/partial_model.h
+++ b/src/theory/arith/partial_model.h
@@ -17,6 +17,7 @@
  ** \todo document this file
  **/
 
+#include "cvc4_private.h"
 
 #include "context/context.h"
 #include "context/cdvector.h"
diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h
index f143b36c4..321f66c5f 100644
--- a/src/theory/arith/tableau.h
+++ b/src/theory/arith/tableau.h
@@ -17,6 +17,7 @@
  ** \todo document this file
  **/
 
+#include "cvc4_private.h"
 
 #include "expr/node.h"
 #include "expr/attribute.h"
@@ -399,10 +400,10 @@ private:
   uint32_t debugCountColLength(ArithVar var);
   uint32_t debugCountRowLength(ArithVar var);
 
-};
+};/* class Tableau */
 
-}; /* namespace arith  */
-}; /* namespace theory */
-}; /* namespace CVC4   */
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
 
 #endif /* __CVC4__THEORY__ARITH__TABLEAU_H */
diff --git a/src/theory/bv/cd_set_collection.h b/src/theory/bv/cd_set_collection.h
index ba9d104a1..e43479381 100644
--- a/src/theory/bv/cd_set_collection.h
+++ b/src/theory/bv/cd_set_collection.h
@@ -26,6 +26,8 @@
 
 #pragma once
 
+#include "cvc4_private.h"
+
 #include <iostream>
 #include "context/cdo.h"
 #include "theory/bv/theory_bv_utils.h"
diff --git a/src/theory/bv/slice_manager.h b/src/theory/bv/slice_manager.h
index 9e0b09f2f..80ac98001 100644
--- a/src/theory/bv/slice_manager.h
+++ b/src/theory/bv/slice_manager.h
@@ -24,6 +24,8 @@
  *      Author: dejan
  */
 
+#include "cvc4_private.h"
+
 #pragma once
 
 #include "context/cdo.h"
diff --git a/src/theory/bv/theory_bv_rewrite_rules_core.h b/src/theory/bv/theory_bv_rewrite_rules_core.h
index b1541fa4a..941b9d0b4 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_core.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_core.h
@@ -17,6 +17,8 @@
  ** \todo document this file
  **/
 
+#include "cvc4_private.h"
+
 #pragma once
 
 #include "theory/bv/theory_bv_rewrite_rules.h"
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index fc4fbf834..80c5ca7f7 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -17,6 +17,8 @@
  ** \todo document this file
  **/
 
+#include "cvc4_private.h"
+
 #pragma once 
 
 #include <set>
diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h
index f1a0e2b30..30267ce48 100644
--- a/src/theory/rewriter.h
+++ b/src/theory/rewriter.h
@@ -16,6 +16,8 @@
  ** The Rewriter class.
  **/
 
+#include "cvc4_private.h"
+
 #pragma once
 
 #include "expr/node.h"
diff --git a/src/theory/rewriter_attributes.h b/src/theory/rewriter_attributes.h
index c958abb68..3a39afd20 100644
--- a/src/theory/rewriter_attributes.h
+++ b/src/theory/rewriter_attributes.h
@@ -16,6 +16,8 @@
  ** Rewriter attributes.
  **/
 
+#include "cvc4_private.h"
+
 #pragma once
 
 namespace CVC4 {
diff --git a/src/theory/rewriter_tables_template.h b/src/theory/rewriter_tables_template.h
index 34204ec2d..9ab98168e 100644
--- a/src/theory/rewriter_tables_template.h
+++ b/src/theory/rewriter_tables_template.h
@@ -17,6 +17,8 @@
  ** from the Theory kinds files.
  **/
 
+#include "cvc4_private.h"
+
 #pragma once
 
 #include "theory/rewriter.h"
diff --git a/src/theory/term_registration_visitor.h b/src/theory/term_registration_visitor.h
index 29269bb52..edb759157 100644
--- a/src/theory/term_registration_visitor.h
+++ b/src/theory/term_registration_visitor.h
@@ -12,6 +12,8 @@
  ** information.\endverbatim
  **/
 
+#include "cvc4_private.h"
+
 #pragma once
 
 #include "context/context.h"
diff --git a/src/util/gmp_util.h b/src/util/gmp_util.h
index 7d2badbfe..e8054fe6b 100644
--- a/src/util/gmp_util.h
+++ b/src/util/gmp_util.h
@@ -17,6 +17,8 @@
  ** \todo document this file
  **/
 
+#include "cvc4_private.h"
+
 #ifndef __CVC4__GMP_UTIL_H
 #define __CVC4__GMP_UTIL_H
 
diff --git a/src/util/ite_removal.h b/src/util/ite_removal.h
index d68c6d933..8861d612c 100644
--- a/src/util/ite_removal.h
+++ b/src/util/ite_removal.h
@@ -16,6 +16,8 @@
  ** Removal of term ITEs.
  **/
 
+#include "cvc4_private.h"
+
 #pragma once
 
 #include <vector>
diff --git a/src/util/trans_closure.h b/src/util/trans_closure.h
index ef04d7af5..a551d4a31 100644
--- a/src/util/trans_closure.h
+++ b/src/util/trans_closure.h
@@ -16,6 +16,8 @@
  ** The transitive closure module.
  **/
 
+#include "cvc4_private.h"
+
 #ifndef __CVC4__UTIL__TRANSITIVE_CLOSURE_H
 #define __CVC4__UTIL__TRANSITIVE_CLOSURE_H