variety of visibility fixes (should clean up some of the many warnings on MacOS-produ...

diff --git a/src/theory/arith/ordered_set.h b/src/theory/arith/ordered_set.h
index c126ab568301edf480827aba94b572d9dd2f0d38..e3eebae5c60e8dfd08fb7e1244f8d5bff24c4675 100644 (file)
--- 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 aa333046bc9746f78866915ce009c188a6d081d1..9c5e343ef794a13d2a79eb3bc6e4fb6e1ff70c3f 100644 (file)
--- 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 f143b36c4f516db2789368990adba0224eaeceda..321f66c5fec9b08cc91e4c4d53950260b612d3f5 100644 (file)
--- 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 ba9d104a16c854392d3a787849df8dfc4043157f..e434793811836956400249992887212de77718bf 100644 (file)
--- 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 9e0b09f2f7b6b97e87206ff592e784fbe0657ace..80ac980014f6ffd6489dd22cf805bc4e1df7abb1 100644 (file)
--- 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 b1541fa4ab283307af5290707dd3d1ba7011d3c4..941b9d0b48db9d4e45ce9fbef5adf410105011af 100644 (file)
--- 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 fc4fbf83429c10732262aeb7a961971c4ba0118b..80c5ca7f78cde6c1c471ec4992c2c930cfa3b84f 100644 (file)
--- 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 f1a0e2b306a78ef576285ae00381075d17e87ed7..30267ce4884df7ee250831d548425796bb10cf64 100644 (file)
--- 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 c958abb681b71aa9cb5f704a5ab4a1d9d75a625e..3a39afd20521730fb42873f361841a2beb855540 100644 (file)
--- 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 34204ec2da2bdfd7195ba94988fa65b4c16233d0..9ab98168e8fe3d6cd0fd9c721495686bcd80287e 100644 (file)
--- 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 29269bb527ce1f99f1547db4e490cba4d9901be5..edb75915734c9aa62bd55b20e154db3a5a1569e6 100644 (file)
--- 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 7d2badbfe6c56fdf4cdcd62ca370c5bd7948236a..e8054fe6be3a258e71d7dcc9591b8e50dc7b85eb 100644 (file)
--- 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 d68c6d93333bb8b779d5929744c5e5fce1ff746a..8861d612c8fd0ed61acd41887518ab62d961163e 100644 (file)
--- 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 ef04d7af5ec8e78d4d5dc478a81b8e8bd3ea90cc..a551d4a31bd774ce3e6bb3434ec550014fe6cf23 100644 (file)
--- 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