diff options
author | Cristian Cadar <c.cadar@imperial.ac.uk> | 2019-08-15 22:57:36 +0100 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2019-09-03 13:38:23 +0100 |
commit | a8abaa43873b8ee49320035817fcdd70a9879bda (patch) | |
tree | fc7251d414a9669e70d55b19b9a39ff00da48ede /lib/Solver | |
parent | e1f055b1785fd7f23fc4d30eeb0276278892ed20 (diff) | |
download | klee-a8abaa43873b8ee49320035817fcdd70a9879bda.tar.gz |
Moved solver-related header files into a separate klee/Solver/ directory.
Diffstat (limited to 'lib/Solver')
-rw-r--r-- | lib/Solver/AssignmentValidatingSolver.cpp | 4 | ||||
-rw-r--r-- | lib/Solver/CachingSolver.cpp | 9 | ||||
-rw-r--r-- | lib/Solver/CexCachingSolver.cpp | 6 | ||||
-rw-r--r-- | lib/Solver/ConstructSolverChain.cpp | 4 | ||||
-rw-r--r-- | lib/Solver/CoreSolver.cpp | 7 | ||||
-rw-r--r-- | lib/Solver/DummySolver.cpp | 6 | ||||
-rw-r--r-- | lib/Solver/FastCexSolver.cpp | 4 | ||||
-rw-r--r-- | lib/Solver/IncompleteSolver.cpp | 2 | ||||
-rw-r--r-- | lib/Solver/IndependentSolver.cpp | 4 | ||||
-rw-r--r-- | lib/Solver/MetaSMTSolver.cpp | 4 | ||||
-rw-r--r-- | lib/Solver/MetaSMTSolver.h | 2 | ||||
-rw-r--r-- | lib/Solver/QueryLoggingSolver.h | 4 | ||||
-rw-r--r-- | lib/Solver/STPBuilder.cpp | 4 | ||||
-rw-r--r-- | lib/Solver/STPSolver.cpp | 2 | ||||
-rw-r--r-- | lib/Solver/STPSolver.h | 2 | ||||
-rw-r--r-- | lib/Solver/Solver.cpp | 4 | ||||
-rw-r--r-- | lib/Solver/SolverCmdLine.cpp | 3 | ||||
-rw-r--r-- | lib/Solver/SolverImpl.cpp | 4 | ||||
-rw-r--r-- | lib/Solver/SolverStats.cpp | 2 | ||||
-rw-r--r-- | lib/Solver/ValidatingSolver.cpp | 4 | ||||
-rw-r--r-- | lib/Solver/Z3Builder.cpp | 4 | ||||
-rw-r--r-- | lib/Solver/Z3Solver.cpp | 4 | ||||
-rw-r--r-- | lib/Solver/Z3Solver.h | 2 |
23 files changed, 48 insertions, 43 deletions
diff --git a/lib/Solver/AssignmentValidatingSolver.cpp b/lib/Solver/AssignmentValidatingSolver.cpp index b75f982a..7e1ccd38 100644 --- a/lib/Solver/AssignmentValidatingSolver.cpp +++ b/lib/Solver/AssignmentValidatingSolver.cpp @@ -9,8 +9,8 @@ #include "klee/Expr/Constraints.h" #include "klee/Expr/Assignment.h" -#include "klee/Solver.h" -#include "klee/SolverImpl.h" +#include "klee/Solver/Solver.h" +#include "klee/Solver/SolverImpl.h" #include <vector> diff --git a/lib/Solver/CachingSolver.cpp b/lib/Solver/CachingSolver.cpp index 2eedc616..2c7371d0 100644 --- a/lib/Solver/CachingSolver.cpp +++ b/lib/Solver/CachingSolver.cpp @@ -8,14 +8,13 @@ //===----------------------------------------------------------------------===// -#include "klee/Solver.h" +#include "klee/Solver/Solver.h" #include "klee/Expr/Constraints.h" #include "klee/Expr/Expr.h" -#include "klee/IncompleteSolver.h" -#include "klee/SolverImpl.h" - -#include "klee/SolverStats.h" +#include "klee/Solver/IncompleteSolver.h" +#include "klee/Solver/SolverImpl.h" +#include "klee/Solver/SolverStats.h" #include <ciso646> #ifdef _LIBCPP_VERSION diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp index 5c181dc3..27a165e1 100644 --- a/lib/Solver/CexCachingSolver.cpp +++ b/lib/Solver/CexCachingSolver.cpp @@ -7,7 +7,7 @@ // //===----------------------------------------------------------------------===// -#include "klee/Solver.h" +#include "klee/Solver/Solver.h" #include "klee/Expr/Assignment.h" #include "klee/Expr/Constraints.h" @@ -17,8 +17,8 @@ #include "klee/Internal/ADT/MapOfSets.h" #include "klee/Internal/Support/ErrorHandling.h" #include "klee/OptionCategories.h" -#include "klee/SolverImpl.h" -#include "klee/SolverStats.h" +#include "klee/Solver/SolverImpl.h" +#include "klee/Solver/SolverStats.h" #include "klee/TimerStatIncrementer.h" #include "llvm/Support/CommandLine.h" diff --git a/lib/Solver/ConstructSolverChain.cpp b/lib/Solver/ConstructSolverChain.cpp index 39e0e824..ed6a77dd 100644 --- a/lib/Solver/ConstructSolverChain.cpp +++ b/lib/Solver/ConstructSolverChain.cpp @@ -10,10 +10,12 @@ /* * This file groups declarations that are common to both KLEE and Kleaver. */ + #include "klee/Common.h" -#include "klee/SolverCmdLine.h" #include "klee/Internal/Support/ErrorHandling.h" #include "klee/Internal/System/Time.h" +#include "klee/Solver/SolverCmdLine.h" + #include "llvm/Support/raw_ostream.h" diff --git a/lib/Solver/CoreSolver.cpp b/lib/Solver/CoreSolver.cpp index 774f52a7..e22f0471 100644 --- a/lib/Solver/CoreSolver.cpp +++ b/lib/Solver/CoreSolver.cpp @@ -10,11 +10,14 @@ #include "STPSolver.h" #include "Z3Solver.h" #include "MetaSMTSolver.h" -#include "klee/SolverCmdLine.h" + +#include "klee/Solver/SolverCmdLine.h" #include "klee/Internal/Support/ErrorHandling.h" -#include "klee/Solver.h" +#include "klee/Solver/Solver.h" + #include "llvm/Support/ErrorHandling.h" #include "llvm/Support/raw_ostream.h" + #include <string> namespace klee { diff --git a/lib/Solver/DummySolver.cpp b/lib/Solver/DummySolver.cpp index 39328653..60a4fb51 100644 --- a/lib/Solver/DummySolver.cpp +++ b/lib/Solver/DummySolver.cpp @@ -7,9 +7,9 @@ // //===----------------------------------------------------------------------===// -#include "klee/Solver.h" -#include "klee/SolverImpl.h" -#include "klee/SolverStats.h" +#include "klee/Solver/Solver.h" +#include "klee/Solver/SolverImpl.h" +#include "klee/Solver/SolverStats.h" namespace klee { diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp index 9f493cd1..3e1162fd 100644 --- a/lib/Solver/FastCexSolver.cpp +++ b/lib/Solver/FastCexSolver.cpp @@ -8,14 +8,14 @@ //===----------------------------------------------------------------------===// #define DEBUG_TYPE "cex-solver" -#include "klee/Solver.h" +#include "klee/Solver/Solver.h" #include "klee/Expr/Constraints.h" #include "klee/Expr/Expr.h" #include "klee/Expr/ExprEvaluator.h" #include "klee/Expr/ExprRangeEvaluator.h" #include "klee/Expr/ExprVisitor.h" -#include "klee/IncompleteSolver.h" +#include "klee/Solver/IncompleteSolver.h" #include "klee/Internal/Support/Debug.h" #include "klee/Internal/Support/IntEvaluation.h" // FIXME: Use APInt diff --git a/lib/Solver/IncompleteSolver.cpp b/lib/Solver/IncompleteSolver.cpp index e19a71e1..9b57bc6c 100644 --- a/lib/Solver/IncompleteSolver.cpp +++ b/lib/Solver/IncompleteSolver.cpp @@ -7,7 +7,7 @@ // //===----------------------------------------------------------------------===// -#include "klee/IncompleteSolver.h" +#include "klee/Solver/IncompleteSolver.h" #include "klee/Expr/Constraints.h" diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp index 12017e5c..7beb1a7c 100644 --- a/lib/Solver/IndependentSolver.cpp +++ b/lib/Solver/IndependentSolver.cpp @@ -8,14 +8,14 @@ //===----------------------------------------------------------------------===// #define DEBUG_TYPE "independent-solver" -#include "klee/Solver.h" +#include "klee/Solver/Solver.h" #include "klee/Expr/Assignment.h" #include "klee/Expr/Constraints.h" #include "klee/Expr/Expr.h" #include "klee/Expr/ExprUtil.h" #include "klee/Internal/Support/Debug.h" -#include "klee/SolverImpl.h" +#include "klee/Solver/SolverImpl.h" #include "llvm/Support/raw_ostream.h" diff --git a/lib/Solver/MetaSMTSolver.cpp b/lib/Solver/MetaSMTSolver.cpp index c4ff1f13..6817c47a 100644 --- a/lib/Solver/MetaSMTSolver.cpp +++ b/lib/Solver/MetaSMTSolver.cpp @@ -16,8 +16,8 @@ #include "klee/Expr/Constraints.h" #include "klee/Expr/ExprUtil.h" #include "klee/Internal/Support/ErrorHandling.h" -#include "klee/Solver.h" -#include "klee/SolverImpl.h" +#include "klee/Solver/Solver.h" +#include "klee/Solver/SolverImpl.h" #include "llvm/Support/ErrorHandling.h" diff --git a/lib/Solver/MetaSMTSolver.h b/lib/Solver/MetaSMTSolver.h index 9fa93719..89cb7143 100644 --- a/lib/Solver/MetaSMTSolver.h +++ b/lib/Solver/MetaSMTSolver.h @@ -11,7 +11,7 @@ #ifndef KLEE_METASMTSOLVER_H #define KLEE_METASMTSOLVER_H -#include "klee/Solver.h" +#include "klee/Solver/Solver.h" namespace klee { diff --git a/lib/Solver/QueryLoggingSolver.h b/lib/Solver/QueryLoggingSolver.h index 75faf3a3..3c012cc2 100644 --- a/lib/Solver/QueryLoggingSolver.h +++ b/lib/Solver/QueryLoggingSolver.h @@ -11,8 +11,8 @@ #ifndef KLEE_QUERYLOGGINGSOLVER_H #define KLEE_QUERYLOGGINGSOLVER_H -#include "klee/Solver.h" -#include "klee/SolverImpl.h" +#include "klee/Solver/Solver.h" +#include "klee/Solver/SolverImpl.h" #include "klee/Internal/System/Time.h" #include "llvm/Support/raw_ostream.h" diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp index 645c8989..ef6697ef 100644 --- a/lib/Solver/STPBuilder.cpp +++ b/lib/Solver/STPBuilder.cpp @@ -11,8 +11,8 @@ #include "STPBuilder.h" #include "klee/Expr/Expr.h" -#include "klee/Solver.h" -#include "klee/SolverStats.h" +#include "klee/Solver/Solver.h" +#include "klee/Solver/SolverStats.h" #include "klee/util/Bits.h" #include "ConstantDivision.h" diff --git a/lib/Solver/STPSolver.cpp b/lib/Solver/STPSolver.cpp index eb46b6db..ebb67254 100644 --- a/lib/Solver/STPSolver.cpp +++ b/lib/Solver/STPSolver.cpp @@ -18,7 +18,7 @@ #include "klee/Expr/ExprUtil.h" #include "klee/Internal/Support/ErrorHandling.h" #include "klee/OptionCategories.h" -#include "klee/SolverImpl.h" +#include "klee/Solver/SolverImpl.h" #include "llvm/Support/CommandLine.h" #include "llvm/Support/Errno.h" diff --git a/lib/Solver/STPSolver.h b/lib/Solver/STPSolver.h index 70b9aa12..494a30db 100644 --- a/lib/Solver/STPSolver.h +++ b/lib/Solver/STPSolver.h @@ -11,7 +11,7 @@ #ifndef KLEE_STPSOLVER_H #define KLEE_STPSOLVER_H -#include "klee/Solver.h" +#include "klee/Solver/Solver.h" namespace klee { /// STPSolver - A complete solver based on STP. diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp index 6c7361dc..855f7102 100644 --- a/lib/Solver/Solver.cpp +++ b/lib/Solver/Solver.cpp @@ -7,10 +7,10 @@ // //===----------------------------------------------------------------------===// -#include "klee/Solver.h" +#include "klee/Solver/Solver.h" #include "klee/Expr/Constraints.h" -#include "klee/SolverImpl.h" +#include "klee/Solver/SolverImpl.h" using namespace klee; diff --git a/lib/Solver/SolverCmdLine.cpp b/lib/Solver/SolverCmdLine.cpp index 9e190840..87b66317 100644 --- a/lib/Solver/SolverCmdLine.cpp +++ b/lib/Solver/SolverCmdLine.cpp @@ -12,8 +12,9 @@ * data that are common to both KLEE and Kleaver. */ +#include "klee/Solver/SolverCmdLine.h" + #include "klee/Config/Version.h" -#include "klee/SolverCmdLine.h" #include "klee/OptionCategories.h" #include "llvm/ADT/ArrayRef.h" diff --git a/lib/Solver/SolverImpl.cpp b/lib/Solver/SolverImpl.cpp index e8f30c9e..ad5388e5 100644 --- a/lib/Solver/SolverImpl.cpp +++ b/lib/Solver/SolverImpl.cpp @@ -7,8 +7,8 @@ // //===----------------------------------------------------------------------===// -#include "klee/Solver.h" -#include "klee/SolverImpl.h" +#include "klee/Solver/Solver.h" +#include "klee/Solver/SolverImpl.h" using namespace klee; diff --git a/lib/Solver/SolverStats.cpp b/lib/Solver/SolverStats.cpp index efdfe6ed..841bfc60 100644 --- a/lib/Solver/SolverStats.cpp +++ b/lib/Solver/SolverStats.cpp @@ -7,7 +7,7 @@ // //===----------------------------------------------------------------------===// -#include "klee/SolverStats.h" +#include "klee/Solver/SolverStats.h" using namespace klee; diff --git a/lib/Solver/ValidatingSolver.cpp b/lib/Solver/ValidatingSolver.cpp index 71e6834e..93d743db 100644 --- a/lib/Solver/ValidatingSolver.cpp +++ b/lib/Solver/ValidatingSolver.cpp @@ -8,8 +8,8 @@ //===----------------------------------------------------------------------===// #include "klee/Expr/Constraints.h" -#include "klee/Solver.h" -#include "klee/SolverImpl.h" +#include "klee/Solver/Solver.h" +#include "klee/Solver/SolverImpl.h" #include <vector> diff --git a/lib/Solver/Z3Builder.cpp b/lib/Solver/Z3Builder.cpp index 07a7b681..43440fa7 100644 --- a/lib/Solver/Z3Builder.cpp +++ b/lib/Solver/Z3Builder.cpp @@ -12,8 +12,8 @@ #include "klee/Expr/Expr.h" #include "klee/Internal/Support/ErrorHandling.h" -#include "klee/Solver.h" -#include "klee/SolverStats.h" +#include "klee/Solver/Solver.h" +#include "klee/Solver/SolverStats.h" #include "klee/util/Bits.h" #include "llvm/ADT/StringExtras.h" diff --git a/lib/Solver/Z3Solver.cpp b/lib/Solver/Z3Solver.cpp index cfcb77e7..00777a78 100644 --- a/lib/Solver/Z3Solver.cpp +++ b/lib/Solver/Z3Solver.cpp @@ -20,8 +20,8 @@ #include "klee/Expr/Constraints.h" #include "klee/Expr/Assignment.h" #include "klee/Expr/ExprUtil.h" -#include "klee/Solver.h" -#include "klee/SolverImpl.h" +#include "klee/Solver/Solver.h" +#include "klee/Solver/SolverImpl.h" #include "llvm/Support/CommandLine.h" #include "llvm/Support/raw_ostream.h" diff --git a/lib/Solver/Z3Solver.h b/lib/Solver/Z3Solver.h index bed74b88..9688ccff 100644 --- a/lib/Solver/Z3Solver.h +++ b/lib/Solver/Z3Solver.h @@ -11,7 +11,7 @@ #ifndef KLEE_Z3SOLVER_H #define KLEE_Z3SOLVER_H -#include "klee/Solver.h" +#include "klee/Solver/Solver.h" namespace klee { /// Z3Solver - A complete solver based on Z3 |