diff options
| author | Hoang M. Le <hle@informatik.uni-bremen.de> | 2016-05-24 17:14:35 +0200 |
|---|---|---|
| committer | Hoang M. Le <hle@informatik.uni-bremen.de> | 2016-06-10 10:24:00 +0200 |
| commit | b097c8d29ccefee7aa799b0ca870cc4e8ec39812 (patch) | |
| tree | be9bb97f2adaf0ebab349aa87809b39f19f66031 | |
| parent | 96ed13583a464538cab900c851bcc7338150772a (diff) | |
| download | klee-b097c8d29ccefee7aa799b0ca870cc4e8ec39812.tar.gz | |
clean up metaSMT includes
| -rw-r--r-- | lib/Solver/CoreSolver.cpp | 7 | ||||
| -rw-r--r-- | lib/Solver/MetaSMTBuilder.h | 11 | ||||
| -rw-r--r-- | lib/Solver/MetaSMTSolver.cpp | 12 |
3 files changed, 9 insertions, 21 deletions
diff --git a/lib/Solver/CoreSolver.cpp b/lib/Solver/CoreSolver.cpp index 94bb3a5e..66328f30 100644 --- a/lib/Solver/CoreSolver.cpp +++ b/lib/Solver/CoreSolver.cpp @@ -15,14 +15,9 @@ #ifdef ENABLE_METASMT -#include <metaSMT/frontend/Array.hpp> +#include <metaSMT/DirectSolver_Context.hpp> #include <metaSMT/backend/Z3_Backend.hpp> #include <metaSMT/backend/Boolector.hpp> -#include <metaSMT/backend/MiniSAT.hpp> -#include <metaSMT/DirectSolver_Context.hpp> -#include <metaSMT/support/run_algorithm.hpp> -#include <metaSMT/API/Stack.hpp> -#include <metaSMT/API/Group.hpp> #define Expr VCExpr #define Type VCType diff --git a/lib/Solver/MetaSMTBuilder.h b/lib/Solver/MetaSMTBuilder.h index 9e1f9a62..9aca9f83 100644 --- a/lib/Solver/MetaSMTBuilder.h +++ b/lib/Solver/MetaSMTBuilder.h @@ -32,17 +32,6 @@ #include <metaSMT/frontend/Logic.hpp> #include <metaSMT/frontend/QF_BV.hpp> #include <metaSMT/frontend/Array.hpp> -#include <metaSMT/support/default_visitation_unrolling_limit.hpp> -#include <metaSMT/support/run_algorithm.hpp> - -#define Expr VCExpr -#define STP STP_Backend -#include <metaSMT/backend/STP.hpp> -#undef Expr -#undef STP - -#include <boost/mpl/vector.hpp> -#include <boost/format.hpp> using namespace metaSMT; using namespace metaSMT::logic::QF_BV; diff --git a/lib/Solver/MetaSMTSolver.cpp b/lib/Solver/MetaSMTSolver.cpp index c4f6a5d0..56964b5d 100644 --- a/lib/Solver/MetaSMTSolver.cpp +++ b/lib/Solver/MetaSMTSolver.cpp @@ -19,11 +19,15 @@ #include <metaSMT/DirectSolver_Context.hpp> #include <metaSMT/backend/Z3_Backend.hpp> #include <metaSMT/backend/Boolector.hpp> -#include <metaSMT/backend/MiniSAT.hpp> -#include <metaSMT/support/run_algorithm.hpp> -#include <metaSMT/API/Stack.hpp> -#include <metaSMT/API/Group.hpp> +#define Expr VCExpr +#define Type VCType +#define STP STP_Backend +#include <metaSMT/backend/STP.hpp> +#undef Expr +#undef Type +#undef STP + #include <errno.h> #include <unistd.h> #include <signal.h> |