From 7aace663fc3f2c4dc56e98a787f5e608f5e14770 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=C3=81ron=20Ricardo=20Perez-Lopez?= <arpl@cs.stanford.edu>
Date: Mon, 4 Nov 2024 16:22:35 -0800
Subject: [PATCH] Mark internal headers private (#362)

Also removed some unused headers and fixed some formatting errors.
---
 include/exceptions.h      | 2 ++
 include/ops.h             | 4 +++-
 include/smt_defs.h        | 3 ++-
 include/solver.h          | 2 ++
 include/solver_enums.h    | 2 ++
 include/sort.h            | 7 +++----
 include/term.h            | 3 ++-
 include/term_translator.h | 3 ++-
 8 files changed, 18 insertions(+), 8 deletions(-)

diff --git a/include/exceptions.h b/include/exceptions.h
index b6aaec3b8..a973fe85c 100644
--- a/include/exceptions.h
+++ b/include/exceptions.h
@@ -14,6 +14,8 @@
 **
 **/
 
+// IWYU pragma: private, include "smt.h"
+
 #pragma once
 
 #include <exception>
diff --git a/include/ops.h b/include/ops.h
index 9b45e539c..e9acc5538 100644
--- a/include/ops.h
+++ b/include/ops.h
@@ -14,6 +14,8 @@
 **
 **/
 
+// IWYU pragma: private, include "smt.h"
+
 #pragma once
 
 #include <cstdint>
@@ -191,7 +193,7 @@ namespace std
         return str_hash(o.to_string());
       }
     };
-}
+}  // namespace std
 
 namespace smt {
 // ops that can be applied to n arguments
diff --git a/include/smt_defs.h b/include/smt_defs.h
index f2c356236..8ecd90774 100644
--- a/include/smt_defs.h
+++ b/include/smt_defs.h
@@ -14,6 +14,8 @@
 **
 **/
 
+// IWYU pragma: private, include "smt.h"
+
 #pragma once
 
 #include <memory>
@@ -42,4 +44,3 @@ class AbsDatatype;
 using Datatype = std::shared_ptr<AbsDatatype>;
 
 }  // namespace smt
-
diff --git a/include/solver.h b/include/solver.h
index 98317fd3b..1ab46ff76 100644
--- a/include/solver.h
+++ b/include/solver.h
@@ -14,6 +14,8 @@
 **
 **/
 
+// IWYU pragma: private, include "smt.h"
+
 #pragma once
 
 #include <string>
diff --git a/include/solver_enums.h b/include/solver_enums.h
index ec4c39404..331ba43a4 100644
--- a/include/solver_enums.h
+++ b/include/solver_enums.h
@@ -14,6 +14,8 @@
 **
 **/
 
+// IWYU pragma: private, include "smt.h"
+
 #pragma once
 
 #include <unordered_set>
diff --git a/include/sort.h b/include/sort.h
index a3391dcbe..eb06466ee 100644
--- a/include/sort.h
+++ b/include/sort.h
@@ -14,14 +14,14 @@
 **
 **/
 
+// IWYU pragma: private, include "smt.h"
+
 #pragma once
 
 #include <string>
 #include <unordered_set>
 #include <vector>
 
-#include "ops.h"
-#include "datatype.h"
 #include "smt_defs.h"
 
 // Sort needs to have arguments
@@ -113,5 +113,4 @@ struct hash<smt::Sort>
 {
   size_t operator()(const smt::Sort & s) const { return s->hash(); }
 };
-}
-
+}  // namespace std
diff --git a/include/term.h b/include/term.h
index 4674bc6f0..2485b9e83 100644
--- a/include/term.h
+++ b/include/term.h
@@ -14,6 +14,8 @@
 **
 **/
 
+// IWYU pragma: private, include "smt.h"
+
 #pragma once
 
 #include <iostream>
@@ -193,4 +195,3 @@ namespace std
     }
   };
 }
-
diff --git a/include/term_translator.h b/include/term_translator.h
index a39dae3cd..d57e0e1a6 100644
--- a/include/term_translator.h
+++ b/include/term_translator.h
@@ -14,6 +14,8 @@
 **        symbols, which would throw an exception).
 **/
 
+// IWYU pragma: private, include "smt.h"
+
 #pragma once
 
 #include <unordered_map>
@@ -156,4 +158,3 @@ class TermTranslator
   std::unordered_map<std::string, Sort> uninterpreted_sorts;
 };
 }  // namespace smt
-