diff --git a/src/storm-dft/builder/DftExplorationHeuristic.h b/src/storm-dft/builder/DftExplorationHeuristic.h
index f4cc3c1ce..2de704e29 100644
--- a/src/storm-dft/builder/DftExplorationHeuristic.h
+++ b/src/storm-dft/builder/DftExplorationHeuristic.h
@@ -22,6 +22,8 @@ namespace storm {
DFTExplorationHeuristic(size_t id, DFTExplorationHeuristic const& predecessor, ValueType rate, ValueType exitRate);
+ virtual ~DFTExplorationHeuristic() = default;
+
void setBounds(ValueType lowerBound, ValueType upperBound);
virtual bool updateHeuristicValues(DFTExplorationHeuristic const& predecessor, ValueType rate, ValueType exitRate) = 0;
diff --git a/src/storm-pgcl/storage/pgcl/AbstractStatementVisitor.h b/src/storm-pgcl/storage/pgcl/AbstractStatementVisitor.h
index 75cb54186..0c0809e94 100755
--- a/src/storm-pgcl/storage/pgcl/AbstractStatementVisitor.h
+++ b/src/storm-pgcl/storage/pgcl/AbstractStatementVisitor.h
@@ -13,6 +13,8 @@ namespace storm {
*/
class AbstractStatementVisitor {
public:
+ virtual ~AbstractStatementVisitor() = default;
+
// Those functions need to be implemented for every possible
// statement instantiation.
virtual void visit(class AssignmentStatement const&) = 0;
diff --git a/src/storm-pgcl/storage/ppg/ProgramAction.h b/src/storm-pgcl/storage/ppg/ProgramAction.h
index adeb1c858..839a097c7 100644
--- a/src/storm-pgcl/storage/ppg/ProgramAction.h
+++ b/src/storm-pgcl/storage/ppg/ProgramAction.h
@@ -13,7 +13,9 @@ namespace storm {
ProgramAction(ProgramGraph* graph, ProgramActionIdentifier id) : graph(graph), actId(id) {
}
-
+
+ virtual ~ProgramAction() = default;
+
ProgramActionIdentifier id() const {
return actId;
}
diff --git a/src/storm/abstraction/MenuGameAbstractor.h b/src/storm/abstraction/MenuGameAbstractor.h
index 283559470..946fb0a97 100644
--- a/src/storm/abstraction/MenuGameAbstractor.h
+++ b/src/storm/abstraction/MenuGameAbstractor.h
@@ -24,6 +24,8 @@ namespace storm {
template <storm::dd::DdType DdType, typename ValueType>
class MenuGameAbstractor {
public:
+ virtual ~MenuGameAbstractor() = default;
+
/// Retrieves the abstraction.
virtual MenuGame<DdType, ValueType> abstract() = 0;
diff --git a/src/storm/abstraction/QualitativeResult.h b/src/storm/abstraction/QualitativeResult.h
index 8d2873541..0d027b3a7 100644
--- a/src/storm/abstraction/QualitativeResult.h
+++ b/src/storm/abstraction/QualitativeResult.h
@@ -13,6 +13,8 @@ namespace storm {
template <storm::dd::DdType Type>
class QualitativeResult {
public:
+ virtual ~QualitativeResult() = default;
+
virtual storm::dd::Bdd<Type> const& getStates() const = 0;
};
diff --git a/src/storm/abstraction/QualitativeResultMinMax.h b/src/storm/abstraction/QualitativeResultMinMax.h
index e748d4023..b6aa96382 100644
--- a/src/storm/abstraction/QualitativeResultMinMax.h
+++ b/src/storm/abstraction/QualitativeResultMinMax.h
@@ -10,6 +10,8 @@ namespace storm {
class QualitativeResultMinMax {
public:
+ virtual ~QualitativeResultMinMax() = default;
+
virtual bool isSymbolic() const;
template<storm::dd::DdType Type>
diff --git a/src/storm/abstraction/StateSet.h b/src/storm/abstraction/StateSet.h
index 2a4e0642d..badeaf534 100644
--- a/src/storm/abstraction/StateSet.h
+++ b/src/storm/abstraction/StateSet.h
@@ -10,6 +10,8 @@ namespace storm {
class StateSet {
public:
+ virtual ~StateSet() = default;
+
virtual bool isSymbolic() const;
template<storm::dd::DdType Type>
diff --git a/src/storm/counterexamples/Counterexample.h b/src/storm/counterexamples/Counterexample.h
index 8cd93178d..060f1f718 100644
--- a/src/storm/counterexamples/Counterexample.h
+++ b/src/storm/counterexamples/Counterexample.h
@@ -7,6 +7,8 @@ namespace storm {
class Counterexample {
public:
+ virtual ~Counterexample() = default;
+
virtual void writeToStream(std::ostream& out) const = 0;
};
diff --git a/src/storm/logic/FormulaVisitor.h b/src/storm/logic/FormulaVisitor.h
index 9548096f7..f0abd0436 100644
--- a/src/storm/logic/FormulaVisitor.h
+++ b/src/storm/logic/FormulaVisitor.h
@@ -10,6 +10,8 @@ namespace storm {
class FormulaVisitor {
public:
+ virtual ~FormulaVisitor() = default;
+
virtual boost::any visit(AtomicExpressionFormula const& f, boost::any const& data) const = 0;
virtual boost::any visit(AtomicLabelFormula const& f, boost::any const& data) const = 0;
virtual boost::any visit(BinaryBooleanStateFormula const& f, boost::any const& data) const = 0;
diff --git a/src/storm/modelchecker/hints/ModelCheckerHint.h b/src/storm/modelchecker/hints/ModelCheckerHint.h
index 14dd4dcbb..5ee82aea5 100644
--- a/src/storm/modelchecker/hints/ModelCheckerHint.h
+++ b/src/storm/modelchecker/hints/ModelCheckerHint.h
@@ -15,7 +15,8 @@ namespace storm {
class ModelCheckerHint {
public:
ModelCheckerHint() = default;
-
+ virtual ~ModelCheckerHint() = default;
+
// Returns true iff this hint does not contain any information.
virtual bool isEmpty() const;
diff --git a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorTask.h b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorTask.h
index f84b935b6..474eb10f8 100644
--- a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorTask.h
+++ b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorTask.h
@@ -24,7 +24,9 @@ namespace storm {
SparseMultiObjectivePreprocessorTask(std::shared_ptr<Objective<typename SparseModelType::ValueType>> const& objective) : objective(objective) {
// intentionally left empty
}
-
+
+ virtual ~SparseMultiObjectivePreprocessorTask() = default;
+
virtual void perform(SparseModelType& preprocessedModel) const = 0;
virtual bool requiresEndComponentAnalysis() const {
diff --git a/src/storm/modelchecker/prctl/helper/DsMpiUpperRewardBoundsComputer.h b/src/storm/modelchecker/prctl/helper/DsMpiUpperRewardBoundsComputer.h
index 7f2bb4278..f49470dcf 100644
--- a/src/storm/modelchecker/prctl/helper/DsMpiUpperRewardBoundsComputer.h
+++ b/src/storm/modelchecker/prctl/helper/DsMpiUpperRewardBoundsComputer.h
@@ -27,7 +27,9 @@ namespace storm {
* @param oneStepTargetProbabilities For each state the probability to go to a goal state in one step.
*/
DsMpiDtmcUpperRewardBoundsComputer(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType> const& rewards, std::vector<ValueType> const& oneStepTargetProbabilities);
-
+
+ virtual ~DsMpiDtmcUpperRewardBoundsComputer() = default;
+
/*!
* Computes upper bounds on the expected rewards.
*/
diff --git a/src/storm/models/sparse/ItemLabeling.h b/src/storm/models/sparse/ItemLabeling.h
index 746320afd..04d9950d2 100644
--- a/src/storm/models/sparse/ItemLabeling.h
+++ b/src/storm/models/sparse/ItemLabeling.h
@@ -33,6 +33,7 @@ namespace storm {
ItemLabeling(ItemLabeling const& other) = default;
ItemLabeling& operator=(ItemLabeling const& other) = default;
+ virtual ~ItemLabeling() = default;
virtual bool isStateLabeling() const;
virtual bool isChoiceLabeling() const;
diff --git a/src/storm/models/sparse/StateAnnotation.h b/src/storm/models/sparse/StateAnnotation.h
index b42e2c9be..edaf0feda 100644
--- a/src/storm/models/sparse/StateAnnotation.h
+++ b/src/storm/models/sparse/StateAnnotation.h
@@ -9,6 +9,8 @@ namespace storm {
class StateAnnotation {
public:
+ virtual ~StateAnnotation() = default;
+
virtual std::string getStateInfo(storm::storage::sparse::state_type const& state) const = 0;
};
diff --git a/src/storm/permissivesched/PermissiveSchedulerComputation.h b/src/storm/permissivesched/PermissiveSchedulerComputation.h
index 372b4a15d..5aa2f400e 100644
--- a/src/storm/permissivesched/PermissiveSchedulerComputation.h
+++ b/src/storm/permissivesched/PermissiveSchedulerComputation.h
@@ -26,8 +26,9 @@ namespace storm {
{
}
-
-
+
+ virtual ~PermissiveSchedulerComputation() = default;
+
virtual void calculatePermissiveScheduler(bool lowerBound, double boundary) = 0;
void setPenalties(PermissiveSchedulerPenalties penalties) {
diff --git a/src/storm/settings/ArgumentBase.h b/src/storm/settings/ArgumentBase.h
index b48a46183..4a5b4f133 100644
--- a/src/storm/settings/ArgumentBase.h
+++ b/src/storm/settings/ArgumentBase.h
@@ -26,7 +26,9 @@ namespace storm {
ArgumentBase(std::string const& name, std::string const& description) : hasBeenSet(false), name(name), description(description) {
// Intentionally left empty.
}
-
+
+ virtual ~ArgumentBase() = default;
+
/*!
* Retrieves the type of the argument.
*
diff --git a/src/storm/settings/ArgumentValidators.h b/src/storm/settings/ArgumentValidators.h
index 4b3b0b3d8..93ced6f26 100644
--- a/src/storm/settings/ArgumentValidators.h
+++ b/src/storm/settings/ArgumentValidators.h
@@ -12,6 +12,8 @@ namespace storm {
template <typename ValueType>
class ArgumentValidator {
public:
+ virtual ~ArgumentValidator() = default;
+
/*!
* Checks whether the argument passes the validation.
*/
diff --git a/src/storm/solver/GameSolver.h b/src/storm/solver/GameSolver.h
index a2f6888d4..bf2b2fdc9 100644
--- a/src/storm/solver/GameSolver.h
+++ b/src/storm/solver/GameSolver.h
@@ -167,6 +167,7 @@ namespace storm {
class GameSolverFactory {
public:
GameSolverFactory();
+ virtual ~GameSolverFactory() = default;
virtual std::unique_ptr<GameSolver<ValueType>> create(storm::storage::SparseMatrix<storm::storage::sparse::state_type> const& player1Matrix, storm::storage::SparseMatrix<ValueType> const& player2Matrix) const;
virtual std::unique_ptr<GameSolver<ValueType>> create(storm::storage::SparseMatrix<storm::storage::sparse::state_type>&& player1Matrix, storm::storage::SparseMatrix<ValueType>&& player2Matrix) const;
diff --git a/src/storm/solver/LinearEquationSolver.h b/src/storm/solver/LinearEquationSolver.h
index e2e5fdb11..fea208b57 100644
--- a/src/storm/solver/LinearEquationSolver.h
+++ b/src/storm/solver/LinearEquationSolver.h
@@ -179,6 +179,8 @@ namespace storm {
template<typename ValueType>
class LinearEquationSolverFactory {
public:
+ virtual ~LinearEquationSolverFactory() = default;
+
/*!
* Creates a new linear equation solver instance with the given matrix.
*
diff --git a/src/storm/solver/LpSolver.h b/src/storm/solver/LpSolver.h
index 7ec7cb906..08d91c463 100644
--- a/src/storm/solver/LpSolver.h
+++ b/src/storm/solver/LpSolver.h
@@ -36,6 +36,8 @@ namespace storm {
*/
LpSolver(OptimizationDirection const& optDir);
+ virtual ~LpSolver() = default;
+
/*!
* Registers an upper- and lower-bounded continuous variable, i.e. a variable that may take all real values
* within its bounds.
diff --git a/src/storm/solver/MinMaxLinearEquationSolver.h b/src/storm/solver/MinMaxLinearEquationSolver.h
index 5f095f5c8..d414eb9f7 100644
--- a/src/storm/solver/MinMaxLinearEquationSolver.h
+++ b/src/storm/solver/MinMaxLinearEquationSolver.h
@@ -207,6 +207,7 @@ namespace storm {
class MinMaxLinearEquationSolverFactory {
public:
MinMaxLinearEquationSolverFactory(MinMaxMethodSelection const& method = MinMaxMethodSelection::FROMSETTINGS, bool trackScheduler = false);
+ virtual ~MinMaxLinearEquationSolverFactory() = default;
std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType> const& matrix) const;
std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType>&& matrix) const;
diff --git a/src/storm/solver/SmtSolver.h b/src/storm/solver/SmtSolver.h
index 3e3a4eeb5..6d842500c 100644
--- a/src/storm/solver/SmtSolver.h
+++ b/src/storm/solver/SmtSolver.h
@@ -36,7 +36,8 @@ namespace storm {
* @param manager The manager responsible for the variables whose value can be requested.
*/
ModelReference(storm::expressions::ExpressionManager const& manager);
-
+ virtual ~ModelReference() = default;
+
virtual bool getBooleanValue(storm::expressions::Variable const& variable) const = 0;
virtual int_fast64_t getIntegerValue(storm::expressions::Variable const& variable) const = 0;
virtual double getRationalValue(storm::expressions::Variable const& variable) const = 0;
diff --git a/src/storm/solver/SymbolicEquationSolver.h b/src/storm/solver/SymbolicEquationSolver.h
index 73681d762..b4aa62933 100644
--- a/src/storm/solver/SymbolicEquationSolver.h
+++ b/src/storm/solver/SymbolicEquationSolver.h
@@ -13,6 +13,7 @@ namespace storm {
public:
SymbolicEquationSolver() = default;
SymbolicEquationSolver(storm::dd::Bdd<DdType> const& allRows);
+ virtual ~SymbolicEquationSolver() = default;
virtual void setLowerBounds(storm::dd::Add<DdType, ValueType> const& lowerBounds);
virtual void setLowerBound(ValueType const& lowerBound);
diff --git a/src/storm/solver/SymbolicGameSolver.h b/src/storm/solver/SymbolicGameSolver.h
index adcec325d..e6594d3de 100644
--- a/src/storm/solver/SymbolicGameSolver.h
+++ b/src/storm/solver/SymbolicGameSolver.h
@@ -54,7 +54,9 @@ namespace storm {
* @param relative Sets whether or not to use a relativ stopping criterion rather than an absolute one.
*/
SymbolicGameSolver(storm::dd::Add<Type, ValueType> const& A, storm::dd::Bdd<Type> const& allRows, storm::dd::Bdd<Type> const& illegalPlayer1Mask, storm::dd::Bdd<Type> const& illegalPlayer2Mask, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs, std::set<storm::expressions::Variable> const& player1Variables, std::set<storm::expressions::Variable> const& player2Variables, ValueType precision, uint_fast64_t maximalNumberOfIterations, bool relative);
-
+
+ virtual ~SymbolicGameSolver() = default;
+
/*!
* Solves the equation system defined by the game matrix. Note that the game matrix has to be given upon
* construction time of the solver object.
@@ -133,6 +135,8 @@ namespace storm {
template<storm::dd::DdType Type, typename ValueType>
class SymbolicGameSolverFactory {
public:
+ virtual ~SymbolicGameSolverFactory() = default;
+
virtual std::unique_ptr<storm::solver::SymbolicGameSolver<Type, ValueType>> create(storm::dd::Add<Type, ValueType> const& A, storm::dd::Bdd<Type> const& allRows, storm::dd::Bdd<Type> const& illegalPlayer1Mask, storm::dd::Bdd<Type> const& illegalPlayer2Mask, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs, std::set<storm::expressions::Variable> const& player1Variables, std::set<storm::expressions::Variable> const& player2Variables) const;
};
diff --git a/src/storm/solver/SymbolicLinearEquationSolver.h b/src/storm/solver/SymbolicLinearEquationSolver.h
index d8d2e00ca..96b4cab83 100644
--- a/src/storm/solver/SymbolicLinearEquationSolver.h
+++ b/src/storm/solver/SymbolicLinearEquationSolver.h
@@ -33,7 +33,8 @@ namespace storm {
class SymbolicLinearEquationSolver : public SymbolicEquationSolver<DdType, ValueType> {
public:
SymbolicLinearEquationSolver();
-
+ virtual ~SymbolicLinearEquationSolver() = default;
+
/*!
* Constructs a symbolic linear equation solver with the given meta variable sets and pairs.
*
@@ -116,6 +117,8 @@ namespace storm {
template<storm::dd::DdType DdType, typename ValueType>
class SymbolicLinearEquationSolverFactory {
public:
+ virtual ~SymbolicLinearEquationSolverFactory() = default;
+
std::unique_ptr<storm::solver::SymbolicLinearEquationSolver<DdType, ValueType>> create(storm::dd::Bdd<DdType> const& allRows, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs) const;
std::unique_ptr<storm::solver::SymbolicLinearEquationSolver<DdType, ValueType>> create(storm::dd::Add<DdType, ValueType> const& A, storm::dd::Bdd<DdType> const& allRows, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs) const;
diff --git a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.h b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.h
index 973caf59f..f8aabedc2 100644
--- a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.h
+++ b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.h
@@ -62,7 +62,8 @@ namespace storm {
class SymbolicMinMaxLinearEquationSolver : public SymbolicEquationSolver<DdType, ValueType> {
public:
SymbolicMinMaxLinearEquationSolver(SymbolicMinMaxLinearEquationSolverSettings<ValueType> const& settings = SymbolicMinMaxLinearEquationSolverSettings<ValueType>());
-
+ virtual ~SymbolicMinMaxLinearEquationSolver() = default;
+
/*!
* Constructs a symbolic min/max linear equation solver with the given meta variable sets and pairs.
*
@@ -237,6 +238,8 @@ namespace storm {
template<storm::dd::DdType DdType, typename ValueType>
class SymbolicMinMaxLinearEquationSolverFactory {
public:
+ virtual ~SymbolicMinMaxLinearEquationSolverFactory() = default;
+
virtual std::unique_ptr<storm::solver::SymbolicMinMaxLinearEquationSolver<DdType, ValueType>> create(storm::dd::Add<DdType, ValueType> const& A, storm::dd::Bdd<DdType> const& allRows, storm::dd::Bdd<DdType> const& illegalMask, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::set<storm::expressions::Variable> const& choiceVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs) const = 0;
/*!
diff --git a/src/storm/solver/TerminationCondition.h b/src/storm/solver/TerminationCondition.h
index 7c364989c..90f472c91 100644
--- a/src/storm/solver/TerminationCondition.h
+++ b/src/storm/solver/TerminationCondition.h
@@ -10,6 +10,8 @@ namespace storm {
template<typename ValueType>
class TerminationCondition {
public:
+ virtual ~TerminationCondition() = default;
+
/*!
* Retrieves whether the guarantee provided by the solver for the current result is sufficient to terminate.
*/
diff --git a/src/storm/solver/stateelimination/EliminatorBase.h b/src/storm/solver/stateelimination/EliminatorBase.h
index 1d918d562..996da58e6 100644
--- a/src/storm/solver/stateelimination/EliminatorBase.h
+++ b/src/storm/solver/stateelimination/EliminatorBase.h
@@ -19,7 +19,8 @@ namespace storm {
typedef typename FlexibleRowType::iterator FlexibleRowIterator;
EliminatorBase(storm::storage::FlexibleSparseMatrix<ValueType>& matrix, storm::storage::FlexibleSparseMatrix<ValueType>& transposedMatrix);
-
+ virtual ~EliminatorBase() = default;
+
void eliminate(uint64_t row, uint64_t column, bool clearRow);
// Provide virtual methods that can be customized by subclasses to govern side-effect of the elimination.
diff --git a/src/storm/solver/stateelimination/StatePriorityQueue.h b/src/storm/solver/stateelimination/StatePriorityQueue.h
index f5cf6c445..cc133fced 100644
--- a/src/storm/solver/stateelimination/StatePriorityQueue.h
+++ b/src/storm/solver/stateelimination/StatePriorityQueue.h
@@ -10,6 +10,8 @@ namespace storm {
class StatePriorityQueue {
public:
+ virtual ~StatePriorityQueue() = default;
+
virtual bool hasNext() const = 0;
virtual storm::storage::sparse::state_type pop() = 0;
virtual void update(storm::storage::sparse::state_type state);
diff --git a/src/storm/storage/bisimulation/BisimulationDecomposition.h b/src/storm/storage/bisimulation/BisimulationDecomposition.h
index 6aa56345c..51383da56 100644
--- a/src/storm/storage/bisimulation/BisimulationDecomposition.h
+++ b/src/storm/storage/bisimulation/BisimulationDecomposition.h
@@ -180,7 +180,9 @@ namespace storm {
* @param options The options to use during for the decomposition.
*/
BisimulationDecomposition(ModelType const& model, Options const& options);
-
+
+ virtual ~BisimulationDecomposition() = default;
+
/*!
* Retrieves the quotient of the model under the computed bisimulation.
*
diff --git a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp
index 218b11ad7..12b5e39f5 100644
--- a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp
+++ b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp
@@ -255,6 +255,8 @@ namespace storm {
STORM_LOG_TRACE("Partition has " << partitionBdd.existsAbstract(model.getRowVariables()).getNonZeroCount() << " states in " << this->numberOfBlocks << " blocks.");
}
+ virtual ~InternalSparseQuotientExtractorBase() = default;
+
storm::storage::SparseMatrix<ValueType> extractTransitionMatrix(storm::dd::Add<DdType, ValueType> const& transitionMatrix) {
return extractMatrixInternal(transitionMatrix);
}
diff --git a/src/storm/storage/dd/cudd/InternalCuddAdd.h b/src/storm/storage/dd/cudd/InternalCuddAdd.h
index 64e1176e7..5871e20dc 100644
--- a/src/storm/storage/dd/cudd/InternalCuddAdd.h
+++ b/src/storm/storage/dd/cudd/InternalCuddAdd.h
@@ -67,7 +67,8 @@ namespace storm {
InternalAdd& operator=(InternalAdd<DdType::CUDD, ValueType> const& other) = default;
InternalAdd(InternalAdd<DdType::CUDD, ValueType>&& other) = default;
InternalAdd& operator=(InternalAdd<DdType::CUDD, ValueType>&& other) = default;
-
+ virtual ~InternalAdd() = default;
+
/*!
* Retrieves whether the two DDs represent the same function.
*
diff --git a/src/storm/storage/dd/sylvan/InternalSylvanAdd.h b/src/storm/storage/dd/sylvan/InternalSylvanAdd.h
index c4374c2b1..79a29f187 100644
--- a/src/storm/storage/dd/sylvan/InternalSylvanAdd.h
+++ b/src/storm/storage/dd/sylvan/InternalSylvanAdd.h
@@ -60,7 +60,8 @@ namespace storm {
InternalAdd& operator=(InternalAdd<DdType::Sylvan, ValueType> const& other) = default;
InternalAdd(InternalAdd<DdType::Sylvan, ValueType>&& other) = default;
InternalAdd& operator=(InternalAdd<DdType::Sylvan, ValueType>&& other) = default;
-
+ virtual ~InternalAdd() = default;
+
/*!
* Retrieves whether the two DDs represent the same function.
*
@@ -732,7 +733,7 @@ namespace storm {
static MTBDD getLeaf(uint_fast64_t value);
/*!
- * Retrieves the sylvan representation of the given storm::Rat�onalNumber.
+ * Retrieves the sylvan representation of the given storm::Rat�onalNumber.
*
* @return The sylvan node for the given value.
*/
diff --git a/src/storm/storage/expressions/CompiledExpression.h b/src/storm/storage/expressions/CompiledExpression.h
index 786408c94..dfa0ea02b 100644
--- a/src/storm/storage/expressions/CompiledExpression.h
+++ b/src/storm/storage/expressions/CompiledExpression.h
@@ -7,6 +7,7 @@ namespace storm {
class CompiledExpression {
public:
+ virtual ~CompiledExpression() = default;
virtual bool isExprtkCompiledExpression() const;
ExprtkCompiledExpression& asExprtkCompiledExpression();
diff --git a/src/storm/storage/expressions/ExpressionEvaluatorBase.h b/src/storm/storage/expressions/ExpressionEvaluatorBase.h
index 80ae61af6..8fd552d28 100644
--- a/src/storm/storage/expressions/ExpressionEvaluatorBase.h
+++ b/src/storm/storage/expressions/ExpressionEvaluatorBase.h
@@ -9,7 +9,8 @@ namespace storm {
class ExpressionEvaluatorBase {
public:
ExpressionEvaluatorBase(storm::expressions::ExpressionManager const& manager);
-
+ virtual ~ExpressionEvaluatorBase() = default;
+
virtual bool asBool(Expression const& expression) const = 0;
virtual int_fast64_t asInt(Expression const& expression) const = 0;
virtual RationalReturnType asRational(Expression const& expression) const = 0;
diff --git a/src/storm/storage/expressions/ExpressionVisitor.h b/src/storm/storage/expressions/ExpressionVisitor.h
index edbdc5d5a..8ef1ea90d 100644
--- a/src/storm/storage/expressions/ExpressionVisitor.h
+++ b/src/storm/storage/expressions/ExpressionVisitor.h
@@ -20,6 +20,8 @@ namespace storm {
class ExpressionVisitor {
public:
+ virtual ~ExpressionVisitor() = default;
+
virtual boost::any visit(IfThenElseExpression const& expression, boost::any const& data) = 0;
virtual boost::any visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) = 0;
virtual boost::any visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) = 0;
diff --git a/src/storm/storage/expressions/Type.h b/src/storm/storage/expressions/Type.h
index 44295b76f..b173d5d53 100644
--- a/src/storm/storage/expressions/Type.h
+++ b/src/storm/storage/expressions/Type.h
@@ -15,6 +15,7 @@ namespace storm {
class BaseType {
public:
BaseType();
+ virtual ~BaseType() = default;
/*!
* Retrieves the mask that is associated with this type.
diff --git a/src/storm/storage/jani/Composition.h b/src/storm/storage/jani/Composition.h
index 773dd93cd..b1375cdce 100644
--- a/src/storm/storage/jani/Composition.h
+++ b/src/storm/storage/jani/Composition.h
@@ -9,6 +9,8 @@ namespace storm {
class Composition {
public:
+ virtual ~Composition() = default;
+
virtual boost::any accept(CompositionVisitor& visitor, boost::any const& data) const = 0;
virtual void write(std::ostream& stream) const = 0;
diff --git a/src/storm/storage/jani/CompositionVisitor.h b/src/storm/storage/jani/CompositionVisitor.h
index c346826e2..c9086c722 100644
--- a/src/storm/storage/jani/CompositionVisitor.h
+++ b/src/storm/storage/jani/CompositionVisitor.h
@@ -11,6 +11,8 @@ namespace storm {
class CompositionVisitor {
public:
+ virtual ~CompositionVisitor() = default;
+
virtual boost::any visit(AutomatonComposition const& composition, boost::any const& data) = 0;
virtual boost::any visit(ParallelComposition const& composition, boost::any const& data) = 0;
};
diff --git a/src/storm/storage/prism/Composition.h b/src/storm/storage/prism/Composition.h
index ac9602af6..06c61b362 100644
--- a/src/storm/storage/prism/Composition.h
+++ b/src/storm/storage/prism/Composition.h
@@ -10,6 +10,7 @@ namespace storm {
class Composition {
public:
Composition() = default;
+ virtual ~Composition() = default;
friend std::ostream& operator<<(std::ostream& stream, Composition const& composition);
diff --git a/src/storm/storage/prism/CompositionVisitor.h b/src/storm/storage/prism/CompositionVisitor.h
index 81f7ee40c..41fcd7f72 100644
--- a/src/storm/storage/prism/CompositionVisitor.h
+++ b/src/storm/storage/prism/CompositionVisitor.h
@@ -15,6 +15,8 @@ namespace storm {
class CompositionVisitor {
public:
+ virtual ~CompositionVisitor() = default;
+
virtual boost::any visit(ModuleComposition const& composition, boost::any const& data) = 0;
virtual boost::any visit(RenamingComposition const& composition, boost::any const& data) = 0;
virtual boost::any visit(HidingComposition const& composition, boost::any const& data) = 0;
diff --git a/src/storm/storage/prism/Variable.h b/src/storm/storage/prism/Variable.h
index 42ba9aec0..ae6c12935 100644
--- a/src/storm/storage/prism/Variable.h
+++ b/src/storm/storage/prism/Variable.h
@@ -17,7 +17,8 @@ namespace storm {
Variable& operator=(Variable const& otherVariable)= default;
Variable(Variable&& otherVariable) = default;
Variable& operator=(Variable&& otherVariable) = default;
-
+ virtual ~Variable() = default;
+
/*!
* Retrieves the name of the variable.
*
diff --git a/src/storm/utility/solver.h b/src/storm/utility/solver.h
index 2dd77f1d6..e75397535 100644
--- a/src/storm/utility/solver.h
+++ b/src/storm/utility/solver.h
@@ -59,6 +59,8 @@ namespace storm {
template<typename ValueType>
class LpSolverFactory {
public:
+ virtual ~LpSolverFactory() = default;
+
/*!
* Creates a new linear equation solver instance with the given name.
*
@@ -98,6 +100,8 @@ namespace storm {
class SmtSolverFactory {
public:
+ virtual ~SmtSolverFactory() = default;
+
/*!
* Creates a new SMT solver instance.
*