Header cleanup

usi-verification-and-security · Feb 17, 2024 · ed30ea3 · ed30ea3
1 parent 1e969d4
commit ed30ea3
Show file tree

Hide file tree

Showing 6 changed files with 9 additions and 4 deletions.
diff --git a/src/ChcInterpreter.h b/src/ChcInterpreter.h
@@ -10,9 +10,11 @@
 #include "ChcSystem.h"
 #include "Normalizer.h"
 #include "Options.h"
+#include "osmt_parser.h"
 #include "proofs/Term.h"
 #include "transformers/Transformer.h"
 #include <engine/Engine.h> // TODO: remove this and create an engine factory
+
 #include <memory>
 
 class LetBinder {

diff --git a/src/Witnesses.h b/src/Witnesses.h
@@ -9,7 +9,6 @@
 
 #include "TransitionSystem.h"
 #include "graph/ChcGraph.h"
-#include "osmt_solver.h"
 #include "proofs/Term.h"
 #include "Normalizer.h"
 #include <memory>

diff --git a/src/engine/IMC.h b/src/engine/IMC.h
@@ -10,6 +10,7 @@
 
 #include "Engine.h"
 #include "TransitionSystem.h"
+#include "osmt_solver.h"
 
 class IMC : public Engine {
     Logic & logic;

diff --git a/src/engine/TPA.h b/src/engine/TPA.h
@@ -9,6 +9,8 @@
 
 #include "Engine.h"
 
+#include "osmt_solver.h"
+
 class TransitionSystem;
 
 enum class ReachabilityResult { REACHABLE, UNREACHABLE };

diff --git a/src/transformers/SingleLoopTransformation.cc b/src/transformers/SingleLoopTransformation.cc
@@ -271,8 +271,9 @@ SingleLoopTransformation::WitnessBackTranslator::translateInvariant(PTRef induct
     return ValidityWitness(std::move(vertexInvariants));
 }
 
-std::set<PTRef> SingleLoopTransformation::WitnessBackTranslator::getVarsForVertex(SymRef vertex) const {
-    std::set<PTRef> vars;
+std::unordered_set<PTRef, PTRefHash>
+SingleLoopTransformation::WitnessBackTranslator::getVarsForVertex(SymRef vertex) const {
+    std::unordered_set<PTRef, PTRefHash> vars;
     for (auto const & entry : positionVarMap) {
         if (entry.first.vertex == vertex) { vars.insert(entry.second); }
     }

diff --git a/src/transformers/SingleLoopTransformation.h b/src/transformers/SingleLoopTransformation.h
@@ -76,7 +76,7 @@ class SingleLoopTransformation {
 
         ErrorOr<ValidityWitness> translateInvariant(PTRef inductiveInvariant);
 
-        std::set<PTRef> getVarsForVertex(SymRef vertex) const;
+        std::unordered_set<PTRef, PTRefHash> getVarsForVertex(SymRef vertex) const;
     };
 
     // Main method