Clean header includes

include/datatype.h

@@ -16,8 +16,9 @@
 
 #pragma once
 
-#include "smt_defs.h"
+#include <string>
 
+#include "smt_defs.h"
 
 namespace smt {
 
@@ -26,7 +27,6 @@ class AbsDatatypeDecl {
  public:
   AbsDatatypeDecl(){};
   virtual ~AbsDatatypeDecl(){};
-
 };
 
 
@@ -38,19 +38,17 @@ class AbsDatatypeConstructorDecl {
   virtual bool compare(const DatatypeConstructorDecl & d) const = 0;
 };
 
-
 class AbsDatatype {
-
  public:
   AbsDatatype(){};
   virtual ~AbsDatatype(){};
-  virtual std::string get_name() const=0;
-  virtual int get_num_selectors(std::string cons) const=0;
-  virtual int get_num_constructors() const=0;
+  virtual std::string get_name() const = 0;
+  virtual int get_num_selectors(std::string cons) const = 0;
+  virtual int get_num_constructors() const = 0;
 };
 // Overloaded equivalence operators for two datatype constructor declarations
 bool operator==(const DatatypeConstructorDecl & d1,
                 const DatatypeConstructorDecl & d2);
 bool operator!=(const DatatypeConstructorDecl & d1,
                 const DatatypeConstructorDecl & d2);
-}
+}  // namespace smt

include/exceptions.h

@@ -80,4 +80,3 @@ class InternalSolverException : public SmtException
   explicit InternalSolverException(const char * msg) : SmtException(msg){};
   explicit InternalSolverException(const std::string& msg) : SmtException(msg){};
 };
-

include/generic_datatype.h

@@ -1,9 +1,10 @@
 #pragma once
-#include <unordered_map>
+
+#include <functional>
+#include <string>
 #include <vector>
 
 #include "datatype.h"
-#include "exceptions.h"
 #include "generic_sort.h"
 #include "smt_defs.h"
 

include/generic_solver.h

@@ -23,13 +23,18 @@
 
 #pragma once
 
+#include <cstdint>
+#include <memory>
 #include <string>
 #include <unordered_map>
-#include <unordered_set>
+#include <vector>
 
-#include "generic_sort.h"
-#include "generic_term.h"
+#include "generic_datatype.h"
+#include "result.h"
+#include "smt_defs.h"
 #include "solver.h"
+#include "sort.h"
+#include "term.h"
 
 namespace smt {
 

include/generic_sort.h

@@ -16,16 +16,18 @@
 
 #pragma once
 
+#include <cstddef>
+#include <cstdint>
 #include <functional>
+#include <string>
+#include <vector>
 
 #include "exceptions.h"
-#include "generic_datatype.h"
 #include "smt_defs.h"
 #include "sort.h"
 
 namespace smt {
 
-class GenericDatatye;
 /* Helper functions for creating generic sorts */
 Sort make_uninterpreted_generic_sort(std::string name, uint64_t arity);
 Sort make_uninterpreted_generic_sort(Sort sort_cons, const SortVec& sorts);

include/generic_term.h

@@ -16,7 +16,10 @@
 
 #pragma once
 
+#include <cstddef>
+#include <cstdint>
 #include <functional>
+#include <string>
 
 #include "ops.h"
 #include "smt_defs.h"

include/identity_walker.h

@@ -16,10 +16,8 @@
 
 #pragma once
 
-#include <utility>
-
-#include "exceptions.h"
-#include "smt.h"
+#include "smt_defs.h"
+#include "term.h"
 
 
 namespace smt

include/logging_solver.h

@@ -16,11 +16,19 @@
 
 #pragma once
 
+#include <cstddef>
+#include <cstdint>
+#include <memory>
+#include <string>
+#include <unordered_map>
+
+#include "result.h"
+#include "smt_defs.h"
 #include "solver.h"
+#include "sort.h"
+#include "term.h"
 #include "term_hashtable.h"
 
-#include <string>
-
 namespace smt {
 
 class LoggingSolver : public AbsSmtSolver

include/logging_sort.h

@@ -16,6 +16,10 @@
 
 #pragma once
 
+#include <cstddef>
+#include <cstdint>
+#include <string>
+
 #include "exceptions.h"
 #include "smt_defs.h"
 #include "sort.h"

include/logging_term.h

@@ -16,6 +16,10 @@
 
 #pragma once
 
+#include <cstddef>
+#include <cstdint>
+#include <string>
+
 #include "ops.h"
 #include "smt_defs.h"
 #include "term.h"

include/ops.h

@@ -16,12 +16,13 @@
 
 #pragma once
 
+#include <cstddef>
 #include <cstdint>
+#include <functional>
 #include <iostream>
 #include <string>
-#include <utility>
 #include <unordered_set>
-#include <functional>
+#include <utility>
 
 namespace smt {
 

include/portfolio_solver.h

@@ -17,9 +17,10 @@
 
 #include <condition_variable>
 #include <mutex>
-#include <thread>
+#include <vector>
 
-#include "smt.h"
+#include "result.h"
+#include "smt_defs.h"
 
 namespace smt {
 

include/printing_solver.h

@@ -15,8 +15,13 @@
 
 #pragma once
 
+#include <cstdint>
+#include <iostream>
+#include <string>
+
+#include "smt_defs.h"
 #include "solver.h"
-#include "term_hashtable.h"
+#include "term.h"
 
 namespace smt {
 

include/result.h

@@ -16,6 +16,8 @@
 
 #pragma once
 
+#include <iostream>
+#include <string>
 namespace smt
 {
 enum ResultType

include/smtlib_reader.h

@@ -16,12 +16,21 @@
 
 #pragma once
 
-#include "assert.h"
+#include <cassert>
+#include <cstddef>
+#include <cstdint>
 #include <string>
 #include <unordered_map>
+#include <unordered_set>
+#include <vector>
 
-#include "smt.h"
+#include "exceptions.h"
+#include "ops.h"
+#include "result.h"
+#include "smt_defs.h"
 #include "smtlibparser.h"
+#include "sort.h"
+#include "term.h"
 
 #define YY_DECL smtlib::parser::symbol_type yylex(smt::SmtLibReader & drv)
 YY_DECL;

include/smtlib_utils.h

@@ -16,6 +16,8 @@
 
 #pragma once
 
+#include <string>
+
 /* string constants for the SMT-LIB commands */
 const std::string SET_OPTION_STR = "set-option";
 const std::string SET_LOGIC_STR = "set-logic";

include/smtlibparser_maps.h

@@ -1,4 +1,5 @@
 #include <string>
+#include <unordered_map>
 
 #include "ops.h"
 

include/solver.h

@@ -16,6 +16,7 @@
 
 #pragma once
 
+#include <cstdint>
 #include <string>
 #include <vector>
 

include/solver_enums.h

@@ -16,6 +16,10 @@
 
 #pragma once
 
+#include <cstddef>
+#include <functional>
+#include <iostream>
+#include <string>
 #include <unordered_set>
 
 namespace smt {

include/solver_utils.h

@@ -15,7 +15,8 @@
 **/
 #pragma once
 
-#include "smt.h"
+#include "smt_defs.h"
+#include "term.h"
 
 namespace smt {
 

include/sort.h

@@ -16,6 +16,8 @@
 
 #pragma once
 
+#include <cstddef>
+#include <cstdint>
 #include <string>
 #include <unordered_set>
 #include <vector>

include/sort_inference.h

@@ -18,10 +18,8 @@
 
 #include <unordered_set>
 
-#include "assert.h"
-#include "generic_sort.h"
-#include "ops.h"
-#include "solver.h"
+#include "smt_defs.h"
+#include "sort.h"
 #include "term.h"
 
 namespace smt {
@@ -240,4 +238,3 @@ Sort constructor_sort(Op op,
                       const SortVec & sorts);
 
 }  // namespace smt
-

include/sorting_network.h

@@ -15,7 +15,8 @@
 
 #pragma once
 
-#include "smt.h"
+#include "smt_defs.h"
+#include "term.h"
 
 namespace smt {
 

include/substitution_walker.h

@@ -16,6 +16,8 @@
 #pragma once
 
 #include "identity_walker.h"
+#include "smt_defs.h"
+#include "term.h"
 
 namespace smt {
 // class for doing substitutions

include/term.h

@@ -16,6 +16,8 @@
 
 #pragma once
 
+#include <cstddef>
+#include <cstdint>
 #include <iostream>
 #include <iterator>
 #include <list>

include/term_hashtable.h

@@ -17,6 +17,7 @@
 
 #pragma once
 
+#include <cstddef>
 #include <unordered_map>
 
 #include "smt_defs.h"

include/term_translator.h

@@ -16,6 +16,7 @@
 
 #pragma once
 
+#include <string>
 #include <unordered_map>
 
 #include "smt_defs.h"

include/tree_walker.h

@@ -18,10 +18,11 @@
 
 #pragma once
 
+#include <unordered_map>
 #include <utility>
+#include <vector>
 
-#include "exceptions.h"
-#include "smt.h"
+#include "smt_defs.h"
 
 namespace smt {
 /* vector of pairs holding terms and ints that gets used within visit in the

include/utils.h

@@ -16,12 +16,17 @@
 
 #pragma once
 
+#include <cassert>
+#include <cstddef>
 #include <iostream>
 #include <sstream>
 #include <string>
+#include <unordered_map>
 
-#include "assert.h"
-#include "smt.h"
+#include "ops.h"
+#include "smt_defs.h"
+#include "term.h"
+#include "term_translator.h"
 
 #ifndef NDEBUG
 #define _ASSERTIONS