diff options
author | Daniel Schemmel <daniel@schemmel.net> | 2023-03-24 15:05:43 +0000 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2023-04-21 13:07:31 +0100 |
commit | ac0fa15ab0679fe1b5067b07647b0701ae3bc347 (patch) | |
tree | f2294eb5f0795ee9ce0f92d527242b7b7a507e79 /include | |
parent | e9d77be6c688836d68a2be5f3f0a02e63f392bb8 (diff) | |
download | klee-ac0fa15ab0679fe1b5067b07647b0701ae3bc347.tar.gz |
use unique_ptr all throughout the solver chain
Diffstat (limited to 'include')
-rw-r--r-- | include/klee/Solver/Common.h | 13 | ||||
-rw-r--r-- | include/klee/Solver/IncompleteSolver.h | 7 | ||||
-rw-r--r-- | include/klee/Solver/Solver.h | 38 | ||||
-rw-r--r-- | include/klee/Solver/SolverImpl.h | 10 |
4 files changed, 34 insertions, 34 deletions
diff --git a/include/klee/Solver/Common.h b/include/klee/Solver/Common.h index 7b244158..626ea55a 100644 --- a/include/klee/Solver/Common.h +++ b/include/klee/Solver/Common.h @@ -24,13 +24,10 @@ namespace klee { const char ALL_QUERIES_KQUERY_FILE_NAME[]="all-queries.kquery"; const char SOLVER_QUERIES_KQUERY_FILE_NAME[]="solver-queries.kquery"; - Solver *constructSolverChain(Solver *coreSolver, - std::string querySMT2LogPath, - std::string baseSolverQuerySMT2LogPath, - std::string queryKQueryLogPath, - std::string baseSolverQueryKQueryLogPath); -} - - +std::unique_ptr<Solver> constructSolverChain( + std::unique_ptr<Solver> coreSolver, std::string querySMT2LogPath, + std::string baseSolverQuerySMT2LogPath, std::string queryKQueryLogPath, + std::string baseSolverQueryKQueryLogPath); +} // namespace klee #endif /* KLEE_COMMON_H */ diff --git a/include/klee/Solver/IncompleteSolver.h b/include/klee/Solver/IncompleteSolver.h index b8ef1929..8bcf7f88 100644 --- a/include/klee/Solver/IncompleteSolver.h +++ b/include/klee/Solver/IncompleteSolver.h @@ -91,10 +91,11 @@ class StagedSolverImpl : public SolverImpl { private: std::unique_ptr<IncompleteSolver> primary; std::unique_ptr<Solver> secondary; - + public: - StagedSolverImpl(IncompleteSolver *_primary, Solver *_secondary); - + StagedSolverImpl(std::unique_ptr<IncompleteSolver> primary, + std::unique_ptr<Solver> secondary); + bool computeTruth(const Query&, bool &isValid); bool computeValidity(const Query&, Solver::Validity &result); bool computeValue(const Query&, ref<Expr> &result); diff --git a/include/klee/Solver/Solver.h b/include/klee/Solver/Solver.h index 2689d19c..c50b17d8 100644 --- a/include/klee/Solver/Solver.h +++ b/include/klee/Solver/Solver.h @@ -71,7 +71,7 @@ namespace klee { std::unique_ptr<SolverImpl> impl; - Solver(SolverImpl *impl); + Solver(std::unique_ptr<SolverImpl> impl); virtual ~Solver(); /// evaluate - Determine for a particular state if the query @@ -215,19 +215,22 @@ namespace klee { /// /// \param s - The primary underlying solver to use. /// \param oracle - The solver to check query results against. - Solver *createValidatingSolver(Solver *s, Solver *oracle, bool ownsOracle = false); + std::unique_ptr<Solver> createValidatingSolver(std::unique_ptr<Solver> s, + Solver *oracle, + bool ownsOracle); /// createAssignmentValidatingSolver - Create a solver that when requested /// for an assignment will check that the computed assignment satisfies /// the Query. /// \param s - The underlying solver to use. - Solver *createAssignmentValidatingSolver(Solver *s); + std::unique_ptr<Solver> + createAssignmentValidatingSolver(std::unique_ptr<Solver> s); /// createCachingSolver - Create a solver which will cache the queries in /// memory (without eviction). /// /// \param s - The underlying solver to use. - Solver *createCachingSolver(Solver *s); + std::unique_ptr<Solver> createCachingSolver(std::unique_ptr<Solver> s); /// createCexCachingSolver - Create a counterexample caching solver. This is a /// more sophisticated cache which records counterexamples for a constraint @@ -235,41 +238,40 @@ namespace klee { /// quickly find satisfying assignments. /// /// \param s - The underlying solver to use. - Solver *createCexCachingSolver(Solver *s); + std::unique_ptr<Solver> createCexCachingSolver(std::unique_ptr<Solver> s); /// createFastCexSolver - Create a "fast counterexample solver", which tries /// to quickly compute a satisfying assignment for a constraint set using /// value propogation and range analysis. /// /// \param s - The underlying solver to use. - Solver *createFastCexSolver(Solver *s); + std::unique_ptr<Solver> createFastCexSolver(std::unique_ptr<Solver> s); /// createIndependentSolver - Create a solver which will eliminate any /// unnecessary constraints before propogating the query to the underlying /// solver. /// /// \param s - The underlying solver to use. - Solver *createIndependentSolver(Solver *s); - + std::unique_ptr<Solver> createIndependentSolver(std::unique_ptr<Solver> s); + /// createKQueryLoggingSolver - Create a solver which will forward all queries /// after writing them to the given path in .kquery format. - Solver *createKQueryLoggingSolver(Solver *s, std::string path, - time::Span minQueryTimeToLog, - bool logTimedOut); + std::unique_ptr<Solver> + createKQueryLoggingSolver(std::unique_ptr<Solver> s, std::string path, + time::Span minQueryTimeToLog, bool logTimedOut); /// createSMTLIBLoggingSolver - Create a solver which will forward all queries /// after writing them to the given path in .smt2 format. - Solver *createSMTLIBLoggingSolver(Solver *s, std::string path, - time::Span minQueryTimeToLog, - bool logTimedOut); - + std::unique_ptr<Solver> + createSMTLIBLoggingSolver(std::unique_ptr<Solver> s, std::string path, + time::Span minQueryTimeToLog, bool logTimedOut); /// createDummySolver - Create a dummy solver implementation which always /// fails. - Solver *createDummySolver(); + std::unique_ptr<Solver> createDummySolver(); // Create a solver based on the supplied ``CoreSolverType``. - Solver *createCoreSolver(CoreSolverType cst); -} + std::unique_ptr<Solver> createCoreSolver(CoreSolverType cst); + } // namespace klee #endif /* KLEE_SOLVER_H */ diff --git a/include/klee/Solver/SolverImpl.h b/include/klee/Solver/SolverImpl.h index f03db964..b73370b9 100644 --- a/include/klee/Solver/SolverImpl.h +++ b/include/klee/Solver/SolverImpl.h @@ -23,12 +23,12 @@ namespace klee { /// SolverImpl - Abstract base clase for solver implementations. class SolverImpl { - // DO NOT IMPLEMENT. - SolverImpl(const SolverImpl&); - void operator=(const SolverImpl&); - public: - SolverImpl() {} + SolverImpl() = default; + + SolverImpl(const SolverImpl&) = delete; + SolverImpl& operator=(const SolverImpl&) = delete; + virtual ~SolverImpl(); enum SolverRunStatus { SOLVER_RUN_STATUS_SUCCESS_SOLVABLE, |