From eff57118fb2b34649050f7e7c9a38850f3bbec0e Mon Sep 17 00:00:00 2001
From: Christoph Schwering <c.schwering@unsw.edu.au>
Date: Fri, 3 Mar 2017 10:53:43 +1100
Subject: [PATCH] Cleaned up includes and ifdefs.

---
 README.md                           |   2 +-
 examples/minesweeper/kb.h           |  16 +--
 examples/minesweeper/minesweeper.cc |   2 +-
 examples/minesweeper/test.sh        |   2 +-
 examples/sudoku/kb.h                |   6 +-
 examples/tui/sudoku.h               |   2 +-
 examples/tui/tui-js.cc              |   2 +-
 examples/tui/tui.cc                 |   6 +-
 src/lela/clause.h                   |  39 +++----
 src/lela/format/output.h            | 160 +++++++++++++++-------------
 src/lela/format/pdl/context.h       |  11 +-
 src/lela/format/pdl/parser.h        |   6 +-
 src/lela/formula.h                  |   1 +
 src/lela/grounder.h                 |   1 +
 src/lela/kb.h                       |   6 ++
 src/lela/literal.h                  |   2 +
 src/lela/setup.h                    |   9 +-
 src/lela/solver.h                   |   5 +
 tests/clause.cc                     |   2 +-
 tests/formula.cc                    |   2 +-
 tests/grounder.cc                   |   2 +-
 tests/hashset.cc                    |   2 +-
 tests/kb.cc                         |   2 +-
 tests/literal.cc                    |   2 +-
 tests/setup.cc                      |   2 +-
 tests/solver.cc                     |   2 +-
 tests/syntax.cc                     |   2 +-
 tests/term.cc                       |   2 +-
 28 files changed, 168 insertions(+), 130 deletions(-)

diff --git a/README.md b/README.md
index 7e1d036..bde5a14 100644
--- a/README.md
+++ b/README.md
@@ -61,7 +61,7 @@ For more theoretical background see the papers linked below.
   [format/cpp/syntax.h](src/lela/format/cpp/syntax.h) overloads some C++
   operators.
 
-## Plan for the future
+## Future work
 
 * Add sitcalc-style actions: regression, progression, or simulate ESL [3] with
   preprocessing, or all of them?
diff --git a/examples/minesweeper/kb.h b/examples/minesweeper/kb.h
index aeaaa12..e6ad780 100644
--- a/examples/minesweeper/kb.h
+++ b/examples/minesweeper/kb.h
@@ -61,27 +61,27 @@ class KnowledgeBase {
         F(ctx_.CreateName(Bool)),
 #endif
         MineF(ctx_.CreateFunction(Bool, 2)) {
-    lela::format::output::RegisterSort(Bool, "");
-    lela::format::output::RegisterSort(XPos, "");
-    lela::format::output::RegisterSort(YPos, "");
-    lela::format::output::RegisterSymbol(T.symbol(), "T");
+    lela::format::RegisterSort(Bool, "");
+    lela::format::RegisterSort(XPos, "");
+    lela::format::RegisterSort(YPos, "");
+    lela::format::RegisterSymbol(T.symbol(), "T");
 #ifdef USE_DETERMINES
-    lela::format::output::RegisterSymbol(F.symbol(), "F");
+    lela::format::RegisterSymbol(F.symbol(), "F");
 #endif
-    lela::format::output::RegisterSymbol(MineF, "Mine");
+    lela::format::RegisterSymbol(MineF, "Mine");
     X.resize(g_->width());
     for (size_t i = 0; i < g_->width(); ++i) {
       X[i] = ctx_.CreateName(XPos);
       std::stringstream ss;
       ss << "#X" << i;
-      lela::format::output::RegisterSymbol(X[i].symbol(), ss.str());
+      lela::format::RegisterSymbol(X[i].symbol(), ss.str());
     }
     Y.resize(g_->height());
     for (size_t i = 0; i < g_->height(); ++i) {
       Y[i] = ctx_.CreateName(YPos);
       std::stringstream ss;
       ss << "#Y" << i;
-      lela::format::output::RegisterSymbol(Y[i].symbol(), ss.str());
+      lela::format::RegisterSymbol(Y[i].symbol(), ss.str());
     }
     processed_.resize(g_->n_fields(), false);
   }
diff --git a/examples/minesweeper/minesweeper.cc b/examples/minesweeper/minesweeper.cc
index 18def03..74c4748 100644
--- a/examples/minesweeper/minesweeper.cc
+++ b/examples/minesweeper/minesweeper.cc
@@ -31,7 +31,7 @@ struct Logger {
     if (first_ && k == -1) {
       std::cout << ", chosen at random.";
     } else if (k == -1) {
-      using lela::format::output::operator<<;
+      using lela::format::operator<<;
       std::cout << ", which is just a guess.";
     } else {
       std::cout << ", found at split level " << k << ".";
diff --git a/examples/minesweeper/test.sh b/examples/minesweeper/test.sh
index 64d5014..121da8a 100755
--- a/examples/minesweeper/test.sh
+++ b/examples/minesweeper/test.sh
@@ -7,6 +7,6 @@ F=test-${W}x${H}-${M}-${K}-${max}.log
 
 inxi -Fx -c 0 >$F
 
-for seed in $(seq 1 $max); do ./minesweeper $W $H $M $seed $K; done | grep You >>$F
+for seed in $(seq 1 $max); do ./minesweeper $W $H $M $seed $K | grep You >>$F; done
 echo $F
 
diff --git a/examples/sudoku/kb.h b/examples/sudoku/kb.h
index 4829ab7..7aabbf4 100644
--- a/examples/sudoku/kb.h
+++ b/examples/sudoku/kb.h
@@ -22,14 +22,14 @@ class KnowledgeBase {
       : max_k_(max_k),
         VAL_(ctx_.CreateSort()),
         val_(ctx_.CreateFunction(VAL_, 2)) {
-    lela::format::output::RegisterSort(VAL_, "");
-    lela::format::output::RegisterSymbol(val_, "val");
+    lela::format::RegisterSort(VAL_, "");
+    lela::format::RegisterSymbol(val_, "val");
     using namespace lela::format::cpp;
     for (std::size_t i = 1; i <= 9; ++i) {
       vals_.push_back(ctx_.CreateName(VAL_));
       std::stringstream ss;
       ss << i;
-      lela::format::output::RegisterSymbol(vals_.back().symbol(), ss.str());
+      lela::format::RegisterSymbol(vals_.back().symbol(), ss.str());
     }
     for (std::size_t x = 1; x <= 9; ++x) {
       for (std::size_t y = 1; y <= 9; ++y) {
diff --git a/examples/tui/sudoku.h b/examples/tui/sudoku.h
index 6e7c9ac..33a66c3 100644
--- a/examples/tui/sudoku.h
+++ b/examples/tui/sudoku.h
@@ -35,7 +35,7 @@ struct SudokuCallbacks {
             const lela::Clause c{lela::Literal::Eq(Val, ns_[n])};
             bool b = ctx->kb()->Entails(*lela::Formula::Factory::Know(0, lela::Formula::Factory::Atomic(c)));
             if (b) {
-              using lela::format::output::operator<<;
+              using lela::format::operator<<;
               std::stringstream ss;
               ss << ns_[n];
               std::cout << ss.str().substr(1);
diff --git a/examples/tui/tui-js.cc b/examples/tui/tui-js.cc
index 5815614..bfacb2b 100644
--- a/examples/tui/tui-js.cc
+++ b/examples/tui/tui-js.cc
@@ -20,7 +20,7 @@
 #include "battleship.h"
 #include "sudoku.h"
 
-using lela::format::output::operator<<;
+using lela::format::operator<<;
 
 template<typename T>
 inline std::string to_string(const T& x) {
diff --git a/examples/tui/tui.cc b/examples/tui/tui.cc
index 877ed00..1d25f00 100644
--- a/examples/tui/tui.cc
+++ b/examples/tui/tui.cc
@@ -20,7 +20,7 @@
 #include "battleship.h"
 #include "sudoku.h"
 
-using lela::format::output::operator<<;
+using lela::format::operator<<;
 
 template<typename ForwardIt, typename Context>
 static bool parse(ForwardIt begin, ForwardIt end, Context* ctx) {
@@ -128,7 +128,7 @@ struct Callback : public lela::format::pdl::DefaultCallback {
         std::cerr << "Setup[" << p << "] = " << std::endl << ctx->kb()->sphere(p)->setup() << std::endl;
       }
     } else if (proc == "print") {
-      lela::format::output::print_range(std::cout, args, "", "", " ");
+      lela::format::print_range(std::cout, args, "", "", " ");
       std::cout << std::endl;
     } else if (proc == "enable_query_logging") {
       ctx->logger()->print_queries = true;
@@ -140,7 +140,7 @@ struct Callback : public lela::format::pdl::DefaultCallback {
       // it's a call for Sudoku
     } else {
       std::cerr << "Calling " << proc;
-      lela::format::output::print_range(std::cerr, args, "(", ")", ",");
+      lela::format::print_range(std::cerr, args, "(", ")", ",");
       std::cerr << " failed" << std::endl;
     }
   }
diff --git a/src/lela/clause.h b/src/lela/clause.h
index a15700f..80b84c6 100644
--- a/src/lela/clause.h
+++ b/src/lela/clause.h
@@ -32,6 +32,7 @@
 #include <vector>
 
 #include <lela/literal.h>
+
 #include <lela/internal/bloom.h>
 #include <lela/internal/ints.h>
 #include <lela/internal/iter.h>
@@ -49,7 +50,7 @@ class Clause {
 
   explicit Clause(const Literal a) : size_(!a.invalid() ? 1 : 0) {
     lits1_[0] = a;
-#if defined(BLOOM)
+#ifdef BLOOM
     InitBloom();
 #endif
   }
@@ -69,7 +70,7 @@ class Clause {
       lits2_[i++] = *it++;
     }
     Minimize();
-#if defined(BLOOM)
+#ifdef BLOOM
     InitBloom();
 #endif
   }
@@ -79,7 +80,7 @@ class Clause {
     if (size2() > 0) {
       std::memcpy(lits2_.get(), c.lits2_.get(), size2() * sizeof(Literal));
     }
-#if defined(BLOOM)
+#ifdef BLOOM
     lhs_bloom_ = c.lhs_bloom_;
 #endif
     assert(!any([](Literal a) { return a.invalid(); }));
@@ -96,7 +97,7 @@ class Clause {
       }
       std::memcpy(lits2_.get(), c.lits2_.get(), size2() * sizeof(Literal));
     }
-#if defined(BLOOM)
+#ifdef BLOOM
     lhs_bloom_ = c.lhs_bloom_;
 #endif
     assert(!any([](Literal a) { return a.invalid(); }));
@@ -108,7 +109,7 @@ class Clause {
 
   bool operator==(const Clause& c) const {
     return size() == c.size() &&
-#if defined(BLOOM)
+#ifdef BLOOM
            lhs_bloom_ == c.lhs_bloom_ &&
 #endif
            std::memcmp(lits1_, c.lits1_, size1() * sizeof(Literal)) == 0 &&
@@ -159,14 +160,14 @@ class Clause {
   }
   bool invalid() const { return empty(); }
 
-#if defined(BLOOM)
+#ifdef BLOOM
   internal::BloomSet<Term> lhs_bloom() const { return lhs_bloom_; }
 #endif
 
   static bool Subsumes(const Literal a, const Clause c) {
     assert(a.primitive());
     assert(c.primitive());
-#if defined(BLOOM)
+#ifdef BLOOM
     if (!c.lhs_bloom_.PossiblyContains(a.lhs())) {
       return false;
     }
@@ -185,7 +186,7 @@ class Clause {
   static bool Subsumes(const Literal a, const Literal b, const Clause c) {
     assert(a < b);
     assert(c.primitive());
-#if defined(BLOOM)
+#ifdef BLOOM
     if (!c.lhs_bloom_.PossiblyContains(a.lhs()) || !c.lhs_bloom_.PossiblyContains(b.lhs())) {
       return false;
     }
@@ -213,7 +214,7 @@ next:
   static bool Subsumes(const Clause& c, const Clause& d) {
     assert(c.primitive());
     assert(d.primitive());
-#if defined(BLOOM)
+#ifdef BLOOM
     if (!c.lhs_bloom_.PossiblySubsetOf(d.lhs_bloom_)) {
       return false;
     }
@@ -244,7 +245,7 @@ next:
     assert(b.primitive());
     assert(!valid());
     assert(!b.valid() && !b.invalid());
-#if defined(BLOOM)
+#ifdef BLOOM
     if (!lhs_bloom_.PossiblyContains(b.lhs())) {
       return;
     }
@@ -256,7 +257,7 @@ next:
       }
     }
     RemoveNulls();
-#if defined(BLOOM)
+#ifdef BLOOM
     InitBloom();
 #endif
   }
@@ -279,7 +280,7 @@ next:
       }
     }
     RemoveNulls();
-#if defined(BLOOM)
+#ifdef BLOOM
     InitBloom();
 #endif
   }
@@ -302,7 +303,7 @@ next:
       }
     }
     RemoveNulls();
-#if defined(BLOOM)
+#ifdef BLOOM
     InitBloom();
 #endif
   }
@@ -313,7 +314,7 @@ next:
     assert(std::all_of(units.begin(), units.end(), [](Literal a) { return a.primitive(); }));
     assert(std::all_of(units.begin(), units.end(), [](Literal a) { return !a.valid() && !a.invalid(); }));
     for (Literal b : units) {
-#if defined(BLOOM)
+#ifdef BLOOM
       if (!lhs_bloom_.PossiblyContains(b.lhs())) {
         continue;
       }
@@ -326,7 +327,7 @@ next:
       }
     }
     RemoveNulls();
-#if defined(BLOOM)
+#ifdef BLOOM
     InitBloom();
 #endif
   }
@@ -337,7 +338,7 @@ next:
 
   bool Mentions(Literal a) const {
     return
-#if defined(BLOOM)
+#ifdef BLOOM
         lhs_bloom_.PossiblyContains(a.lhs()) &&
 #endif
         any([a](Literal b) { return a == b; });
@@ -345,7 +346,7 @@ next:
 
   bool MentionsLhs(Term t) const {
     return
-#if defined(BLOOM)
+#ifdef BLOOM
         lhs_bloom_.PossiblyContains(t) &&
 #endif
         any([t](Literal a) { return a.lhs() == t; });
@@ -431,7 +432,7 @@ next:
     assert(!any([](Literal a) { return a.invalid(); }));
   }
 
-#if defined(BLOOM)
+#ifdef BLOOM
   void InitBloom() {
     lhs_bloom_.Clear();
     for (size_t i = 0; i < size(); ++i) {
@@ -441,7 +442,7 @@ next:
 #endif
 
   size_t size_ = 0;
-#if defined(BLOOM)
+#ifdef BLOOM
   internal::BloomSet<Term> lhs_bloom_;
 #endif
   Literal lits1_[kArraySize];
diff --git a/src/lela/format/output.h b/src/lela/format/output.h
index db5c9a5..5d803b9 100644
--- a/src/lela/format/output.h
+++ b/src/lela/format/output.h
@@ -2,11 +2,9 @@
 // Copyright 2014-2017 Christoph Schwering
 // Licensed under the MIT license. See LICENSE file in the project root.
 //
-// Overloads the stream operator (<<) for Literal, Clause, and so on. For
-// Sort and Symbol objects, a human-readable name can be registered.
-
-#ifndef LELA_FORMAT_OUTPUT_H_
-#define LELA_FORMAT_OUTPUT_H_
+// Overloads the stream operator (<<) for Literal, Clause, and so on. These
+// operators are only activated when the corresponding header is included.
+// For Sort and Symbol objects, a human-readable name can be registered.
 
 #include <algorithm>
 #include <list>
@@ -19,27 +17,20 @@
 #include <utility>
 #include <vector>
 
-#include <lela/formula.h>
-#include <lela/literal.h>
-#if 0
-#include <lela/modal.h>
-#endif
-#include <lela/setup.h>
-#if 0
-#include <lela/solver.h>
-#endif
 #include <lela/term.h>
+
 #include <lela/internal/compar.h>
-#include <lela/internal/hashset.h>
 #include <lela/internal/iter.h>
 #include <lela/internal/maybe.h>
 
+#ifndef MARK
 #define MARK (std::cout << __FILE__ << ":" << __LINE__ << std::endl)
+#endif
 
 namespace lela {
 namespace format {
-namespace output {
 
+#ifndef LELA_FORMAT_OUTPUT_H_
 typedef std::unordered_map<Symbol::Sort, std::string> SortMap;
 typedef std::unordered_map<Symbol, std::string> SymbolMap;
 
@@ -124,13 +115,21 @@ std::ostream& operator<<(std::ostream& os, const std::unordered_map<K, T, H, E>&
 
 template<typename K, typename T, typename H, typename E>
 std::ostream& operator<<(std::ostream& os, const std::unordered_multimap<K, T, H, E>& map);
+#endif  // LELA_FORMAT_OUTPUT_H_
 
+#ifdef LELA_INTERNAL_HASHSET_H_
 template<typename T, typename H, typename E>
 std::ostream& operator<<(std::ostream& os, const internal::HashSet<T, H, E>& set);
+#endif  // LELA_INTERNAL_HASHSET_H_
 
+#ifdef LELA_INTERNAL_MAYBE_H_
 template<typename K, typename T>
 std::ostream& operator<<(std::ostream& os, const internal::Maybe<T>& m);
+#endif  // LELA_INTERNAL_MAYBE_H_
 
+#ifdef LELA_TERM_H_
+#ifndef LELA_TERM_OUTPUT
+#define LELA_TERM_OUTPUT
 std::ostream& operator<<(std::ostream& os, const Symbol s) {
   internal::Maybe<std::string> sort_name = LookupSort(s.sort());
   internal::Maybe<std::string> symbol_name = LookupSymbol(s);
@@ -166,79 +165,81 @@ std::ostream& operator<<(std::ostream& os, const Term t) {
   }
   return os;
 }
+#endif  // LELA_TERM_OUTPUT
+#endif  // LELA_TERM_H_
 
-struct PrintSymbolComparator {
-  typedef Symbol value_type;
-
-  bool operator()(Symbol s1, Symbol s2) const {
-    internal::Maybe<std::string> n1 = LookupSymbol(s1);
-    internal::Maybe<std::string> n2 = LookupSymbol(s2);
-    return n1 && n2  ? n1.val < n2.val :
-           n1 && !n2 ? true :
-           !n1 && n2 ? false :
-                       s1.hash() < s2.hash();
-  }
-};
-
-struct PrintTermComparator {
-  typedef Term value_type;
-
-  inline bool operator()(Term t1, Term t2) const;
-};
-
-inline bool PrintTermComparator::operator()(Term t1, Term t2) const {
-  internal::LexicographicComparator<
-      PrintSymbolComparator,
-      internal::LessComparator<Symbol::Arity>,
-      internal::LexicographicContainerComparator<Term::Vector, PrintTermComparator>> comp;
-  return comp(t1.symbol(), t1.arity(), t1.args(),
-              t2.symbol(), t2.arity(), t2.args());
-}
-
-struct PrintLiteralComparator {
-  typedef Literal value_type;
-
-  bool operator()(Literal l1, Literal l2) const {
-    return comp(l1.lhs(), l1.rhs(), l1.pos(),
-                l2.lhs(), l2.rhs(), l2.pos());
-  }
-
-  internal::LexicographicComparator<
-      PrintTermComparator,
-      PrintTermComparator,
-      internal::LessComparator<bool>> comp;
-};
-
+#ifdef LELA_LITERAL_H_
+#ifndef LELA_LITERAL_OUTPUT
+#define LELA_LITERAL_OUTPUT
 std::ostream& operator<<(std::ostream& os, const Literal a) {
   os << a.lhs() << ' ' << (a.pos() ? "\u003D" : "\u2260") << ' ' << a.rhs();
   return os;
 }
+#endif  // LELA_LITERAL_OUTPUT_
+#endif  // LELA_LITERAL_H_
 
+#ifdef LELA_CLAUSE_H_
+#ifndef LELA_CLAUSE_OUTPUT
+#define LELA_CLAUSE_OUTPUT
 std::ostream& operator<<(std::ostream& os, const Clause& c) {
+  struct PrintLiteralComparator {
+    struct PrintTermComparator {
+      struct PrintSymbolComparator {
+        typedef Symbol value_type;
+
+        bool operator()(Symbol s1, Symbol s2) const {
+          internal::Maybe<std::string> n1 = LookupSymbol(s1);
+          internal::Maybe<std::string> n2 = LookupSymbol(s2);
+          return n1 && n2  ? n1.val < n2.val :
+                 n1 && !n2 ? true :
+                 !n1 && n2 ? false :
+                             s1.hash() < s2.hash();
+        }
+      };
+
+      typedef Term value_type;
+
+      inline bool operator()(Term t1, Term t2) const {
+        internal::LexicographicComparator<
+            PrintSymbolComparator,
+            internal::LessComparator<Symbol::Arity>,
+            internal::LexicographicContainerComparator<Term::Vector, PrintTermComparator>> comp;
+        return comp(t1.symbol(), t1.arity(), t1.args(),
+                    t2.symbol(), t2.arity(), t2.args());
+      }
+    };
+
+    bool operator()(Literal l1, Literal l2) const {
+      return comp(l1.lhs(), l1.rhs(), l1.pos(),
+                  l2.lhs(), l2.rhs(), l2.pos());
+    }
+
+    internal::LexicographicComparator<
+        PrintTermComparator,
+        PrintTermComparator,
+        internal::LessComparator<bool>> comp;
+  };
   std::vector<Literal> vec(c.begin(), c.end());
   std::sort(vec.begin(), vec.end(), PrintLiteralComparator());
   return print_range(os, vec, "[", "]", " \u2228 ");
 }
+#endif  // LELA_OUTPUT_CLAUSE
+#endif  // LELA_CLAUSE_H_
 
+#ifdef LELA_SETUP_H_
+#ifndef LELA_SETUP_OUTPUT
+#define LELA_SETUP_OUTPUT
 std::ostream& operator<<(std::ostream& os, const Setup& s) {
   auto is = s.clauses();
   auto cs = internal::transform_range(is.begin(), is.end(), [&s](size_t i) { return s.clause(i); });
   return print_range(os, cs, "{ ", "\n}", "\n, ");
 }
+#endif  // LELA_SETUP_OUTPUT
+#endif  // LELA_SETUP_H_
 
-#if 0
-std::ostream& operator<<(std::ostream& os, const Solver& s) {
-  return os << s.setup();
-}
-
-std::ostream& operator<<(std::ostream& os, const KnowledgeBase& kb) {
-  for (const Solver& s : kb.spheres()) {
-    os << s << std::endl;
-  }
-  return os;
-}
-#endif
-
+#ifdef LELA_FORMULA_H_
+#ifndef LELA_FORMULA_OUTPUT
+#define LELA_FORMULA_OUTPUT
 std::ostream& operator<<(std::ostream& os, const Formula& alpha) {
   switch (alpha.type()) {
     case Formula::kAtomic:
@@ -293,7 +294,10 @@ std::ostream& operator<<(std::ostream& os, const Formula& alpha) {
 std::ostream& operator<<(std::ostream& os, const Formula::Ref& alpha) {
   return os << *alpha;
 }
+#endif  // LELA_FORMULA_OUTPUT
+#endif  // LELA_FORMULA_H_
 
+#ifndef LELA_FORMAT_OUTPUT_H_
 template<typename InputIt>
 std::ostream& print_sequence(std::ostream& os,
                              InputIt begin,
@@ -389,13 +393,22 @@ std::ostream& operator<<(std::ostream& os, const std::unordered_multimap<K, T, H
   print_sequence(os, map.begin(), map.end(), "m{", "}m", ", ");
   return os;
 }
+#endif  // LELA_FORMAT_OUTPUT_H_
 
+#ifdef LELA_INTERNAL_HASHSET_H_
+#ifndef LELA_INTERNAL_HASHSET_OUTPUT
+#define LELA_INTERNAL_HASHSET_OUTPUT
 template<typename T, typename H, typename E>
 std::ostream& operator<<(std::ostream& os, const internal::HashSet<T, H, E>& set) {
   print_sequence(os, set.begin(), set.end(), "{", "}", ", ");
   return os;
 }
+#endif  // LELA_INTERNAL_HASHSET_OUTPUT
+#endif  // LELA_INTERNAL_HASHSET_H_
 
+#ifdef LELA_INTERNAL_MAYBE_H_
+#ifndef LELA_INTERNAL_MAYBE_OUTPUT
+#define LELA_INTERNAL_MAYBE_OUTPUT
 template<typename T>
 std::ostream& operator<<(std::ostream& os, const internal::Maybe<T>& m) {
   if (m) {
@@ -405,10 +418,13 @@ std::ostream& operator<<(std::ostream& os, const internal::Maybe<T>& m) {
   }
   return os;
 }
+#endif  // LELA_INTERNAL_MAYBE_OUTPUT
+#endif  // LELA_INTERNAL_MAYBE_H_
 
-}  // namespace output
 }  // namespace format
 }  // namespace lela
 
+#ifndef LELA_FORMAT_OUTPUT_H_
+#define LELA_FORMAT_OUTPUT_H_
 #endif  // LELA_FORMAT_OUTPUT_H_
 
diff --git a/src/lela/format/pdl/context.h b/src/lela/format/pdl/context.h
index 4605c02..e7ca79b 100644
--- a/src/lela/format/pdl/context.h
+++ b/src/lela/format/pdl/context.h
@@ -12,8 +12,8 @@
 #ifndef LELA_FORMAT_PDL_CONTEXT_H_
 #define LELA_FORMAT_PDL_CONTEXT_H_
 
-#include <map>
 #include <iostream>
+#include <map>
 #include <string>
 #include <stdexcept>
 #include <utility>
@@ -22,6 +22,7 @@
 #include <lela/term.h>
 #include <lela/formula.h>
 #include <lela/kb.h>
+
 #include <lela/format/output.h>
 
 namespace lela {
@@ -132,7 +133,7 @@ class Context {
 
   void RegisterSort(const std::string& id) {
     const Symbol::Sort sort = CreateSort();
-    lela::format::output::RegisterSort(sort, "");
+    lela::format::RegisterSort(sort, "");
     sorts_.Register(id, sort);
     logger_(DefaultLogger::RegisterSortData(id));
   }
@@ -143,7 +144,7 @@ class Context {
     const Symbol::Sort sort = LookupSort(sort_id);
     const Term var = CreateVariable(sort);
     vars_.Register(id, var);
-    lela::format::output::RegisterSymbol(var.symbol(), id);
+    lela::format::RegisterSymbol(var.symbol(), id);
     logger_(DefaultLogger::RegisterVariableData(id, sort_id));
   }
 
@@ -153,7 +154,7 @@ class Context {
     const Symbol::Sort sort = LookupSort(sort_id);
     const Term name = CreateName(sort);
     names_.Register(id, name);
-    lela::format::output::RegisterSymbol(name.symbol(), id);
+    lela::format::RegisterSymbol(name.symbol(), id);
     logger_(DefaultLogger::RegisterNameData(id, sort_id));
   }
 
@@ -163,7 +164,7 @@ class Context {
     const Symbol::Sort sort = LookupSort(sort_id);
     const Symbol fun = CreateFunction(sort, arity);
     funs_.Register(id, fun);
-    lela::format::output::RegisterSymbol(fun, id);
+    lela::format::RegisterSymbol(fun, id);
     logger_(DefaultLogger::RegisterFunctionData(id, arity, sort_id));
   }
 
diff --git a/src/lela/format/pdl/parser.h b/src/lela/format/pdl/parser.h
index 32e372f..0f7777a 100644
--- a/src/lela/format/pdl/parser.h
+++ b/src/lela/format/pdl/parser.h
@@ -24,7 +24,9 @@
 #include <lela/formula.h>
 #include <lela/grounder.h>
 #include <lela/setup.h>
+
 #include <lela/format/output.h>
+
 #include <lela/format/pdl/lexer.h>
 
 namespace lela {
@@ -771,7 +773,7 @@ class Parser {
         return Success<>();
       } else {
         std::stringstream ss;
-        using lela::format::output::operator<<;
+        using lela::format::operator<<;
         ss << (is_assert ? "Assertion" : "Refutation") << " of " << *alpha.val << " failed";
         return Error<>(LELA_MSG(ss.str()));
       }
@@ -1173,7 +1175,7 @@ class Parser {
       const Result<Action<>> r = branch();
       if (!r) {
         std::stringstream ss;
-        using lela::format::output::operator<<;
+        using lela::format::operator<<;
         ss << Tok(0) << " " << Tok(1) << " " << Tok(2) << "...";
         return Error<Action<>>(LELA_MSG("Error in start with unparsed input "+ ss.str()), r);
       }
diff --git a/src/lela/formula.h b/src/lela/formula.h
index 1fff3c9..5af5e82 100644
--- a/src/lela/formula.h
+++ b/src/lela/formula.h
@@ -22,6 +22,7 @@
 #include <vector>
 
 #include <lela/clause.h>
+
 #include <lela/internal/iter.h>
 #include <lela/internal/ints.h>
 #include <lela/internal/maybe.h>
diff --git a/src/lela/grounder.h b/src/lela/grounder.h
index 5cae131..457651d 100644
--- a/src/lela/grounder.h
+++ b/src/lela/grounder.h
@@ -38,6 +38,7 @@
 #include <lela/clause.h>
 #include <lela/formula.h>
 #include <lela/setup.h>
+
 #include <lela/internal/hash.h>
 #include <lela/internal/ints.h>
 #include <lela/internal/iter.h>
diff --git a/src/lela/kb.h b/src/lela/kb.h
index 14e69b0..188ed43 100644
--- a/src/lela/kb.h
+++ b/src/lela/kb.h
@@ -31,9 +31,15 @@
 #include <utility>
 #include <vector>
 
+#include <lela/clause.h>
 #include <lela/formula.h>
+#include <lela/grounder.h>
+#include <lela/literal.h>
 #include <lela/solver.h>
+#include <lela/term.h>
+
 #include <lela/internal/ints.h>
+#include <lela/internal/iter.h>
 #include <lela/internal/maybe.h>
 
 namespace lela {
diff --git a/src/lela/literal.h b/src/lela/literal.h
index 4989187..7616235 100644
--- a/src/lela/literal.h
+++ b/src/lela/literal.h
@@ -25,7 +25,9 @@
 #include <utility>
 
 #include <lela/term.h>
+
 #include <lela/internal/ints.h>
+#include <lela/internal/maybe.h>
 
 namespace lela {
 
diff --git a/src/lela/setup.h b/src/lela/setup.h
index 7f28942..f269aa9 100644
--- a/src/lela/setup.h
+++ b/src/lela/setup.h
@@ -66,9 +66,12 @@
 #include <vector>
 
 #include <lela/clause.h>
-#include <lela/internal/intmap.h>
+#include <lela/literal.h>
+#include <lela/term.h>
+
 #include <lela/internal/ints.h>
 #include <lela/internal/iter.h>
+#include <lela/internal/maybe.h>
 
 namespace lela {
 
@@ -243,7 +246,7 @@ class Setup {
 
   bool LocallyConsistent(const std::unordered_set<Term>& ts) const {
     assert(std::all_of(ts.begin(), ts.end(), [](Term t) { return t.primitive(); }));
-#if defined(BLOOM)
+#ifdef BLOOM
     internal::BloomSet<Term> bs;
     for (Term t : ts) {
       bs.Add(t);
@@ -253,7 +256,7 @@ class Setup {
     for (size_t i : clauses()) {
       const Clause c = clause(i);
       if (
-#if defined(BLOOM)
+#ifdef BLOOM
           bs.PossiblyOverlaps(c.lhs_bloom()) &&
 #endif
           std::any_of(c.begin(), c.end(), [&ts](Literal a) { return ts.find(a.lhs()) != ts.end(); })) {
diff --git a/src/lela/solver.h b/src/lela/solver.h
index 3a9a97c..e5f287b 100644
--- a/src/lela/solver.h
+++ b/src/lela/solver.h
@@ -51,10 +51,15 @@
 #include <iterator>
 #include <list>
 
+#include <lela/formula.h>
 #include <lela/grounder.h>
+#include <lela/literal.h>
 #include <lela/setup.h>
 #include <lela/term.h>
 
+#include <lela/internal/ints.h>
+#include <lela/internal/maybe.h>
+
 namespace lela {
 
 class Solver {
diff --git a/tests/clause.cc b/tests/clause.cc
index ffc3ab7..c15ac65 100644
--- a/tests/clause.cc
+++ b/tests/clause.cc
@@ -9,7 +9,7 @@
 
 namespace lela {
 
-using namespace lela::format::output;
+using namespace lela::format;
 
 struct EqSubstitute {
   EqSubstitute(Term pre, Term post) : pre_(pre), post_(post) {}
diff --git a/tests/formula.cc b/tests/formula.cc
index 4a8db21..ca35c35 100644
--- a/tests/formula.cc
+++ b/tests/formula.cc
@@ -9,8 +9,8 @@
 
 namespace lela {
 
+using namespace lela::format;
 using namespace lela::format::cpp;
-using namespace lela::format::output;
 
 #define REGISTER_SYMBOL(x)    RegisterSymbol(x, #x)
 
diff --git a/tests/grounder.cc b/tests/grounder.cc
index 28f9723..e0e5d00 100644
--- a/tests/grounder.cc
+++ b/tests/grounder.cc
@@ -11,7 +11,7 @@
 
 namespace lela {
 
-using namespace lela::format::output;
+using namespace lela::format;
 
 std::unordered_set<Clause> unique(const Setup& s) {
   std::unordered_set<Clause> set;
diff --git a/tests/hashset.cc b/tests/hashset.cc
index d747998..6f2adee 100644
--- a/tests/hashset.cc
+++ b/tests/hashset.cc
@@ -19,7 +19,7 @@ struct Value {
 
 std::ostream& operator<<(std::ostream& os, Value i) { return std::cout << i.x; }
 
-using namespace lela::format::output;
+using namespace lela::format;
 
 namespace lela {
 namespace internal {
diff --git a/tests/kb.cc b/tests/kb.cc
index 31005b9..bd27e65 100644
--- a/tests/kb.cc
+++ b/tests/kb.cc
@@ -9,8 +9,8 @@
 
 namespace lela {
 
+using namespace lela::format;
 using namespace lela::format::cpp;
-using namespace lela::format::output;
 
 #define REGISTER_SYMBOL(x)    RegisterSymbol(x, #x)
 
diff --git a/tests/literal.cc b/tests/literal.cc
index e506224..503b8b5 100644
--- a/tests/literal.cc
+++ b/tests/literal.cc
@@ -8,7 +8,7 @@
 
 namespace lela {
 
-using namespace lela::format::output;
+using namespace lela::format;
 
 TEST(LiteralTest, general) {
   Symbol::Factory& sf = *Symbol::Factory::Instance();
diff --git a/tests/setup.cc b/tests/setup.cc
index 6146cc0..93a0e0d 100644
--- a/tests/setup.cc
+++ b/tests/setup.cc
@@ -11,7 +11,7 @@
 
 namespace lela {
 
-using namespace lela::format::output;
+using namespace lela::format;
 
 template<typename T>
 size_t dist(T r) { return std::distance(r.begin(), r.end()); }
diff --git a/tests/solver.cc b/tests/solver.cc
index eedd3cd..7465db6 100644
--- a/tests/solver.cc
+++ b/tests/solver.cc
@@ -9,8 +9,8 @@
 
 namespace lela {
 
+using namespace lela::format;
 using namespace lela::format::cpp;
-using namespace lela::format::output;
 
 #define REGISTER_SYMBOL(x)    RegisterSymbol(x, #x)
 
diff --git a/tests/syntax.cc b/tests/syntax.cc
index ceb8310..d4c3de5 100644
--- a/tests/syntax.cc
+++ b/tests/syntax.cc
@@ -9,8 +9,8 @@
 
 namespace lela {
 
+using namespace lela::format;
 using namespace lela::format::cpp;
-using namespace lela::format::output;
 
 #define REGISTER_SYMBOL(x)    RegisterSymbol(x, #x)
 
diff --git a/tests/term.cc b/tests/term.cc
index b84856c..ebd24a7 100644
--- a/tests/term.cc
+++ b/tests/term.cc
@@ -8,7 +8,7 @@
 
 namespace lela {
 
-using namespace lela::format::output;
+using namespace lela::format;
 
 struct EqSubstitute {
   EqSubstitute(Term pre, Term post) : pre_(pre), post_(post) {}
-- 
GitLab