diff --git a/src/storm/adapters/Smt2ExpressionAdapter.h b/src/storm/adapters/Smt2ExpressionAdapter.h
index c61566177..f1b96b71e 100644
--- a/src/storm/adapters/Smt2ExpressionAdapter.h
+++ b/src/storm/adapters/Smt2ExpressionAdapter.h
@@ -38,8 +38,7 @@ namespace storm {
std::string translateExpression(storm::expressions::Expression const& ) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented");
}
-
-#ifdef STORM_HAVE_CARL
+
/*!
* Translates the given constraint "leftHandSide relation rightHandSide" to an equivalent expression for Smt2.
@@ -60,6 +59,7 @@ namespace storm {
") " +
")";
}
+
/*!
* Translates the given constraint "leftHandSide relation 0" to an equivalent expression for Smt2.
@@ -67,31 +67,16 @@ namespace storm {
* @param constraint
* @return An equivalent expression for Smt2.
*/
- std::string translateExpression(storm::ArithConstraint<storm::RawPolynomial> const& constraint) {
- std::stringstream ss;
- ss << "(" << constraint.rel() << " " <<
- constraint.lhs().toString(false, useReadableVarNames) << " " <<
- "0 " <<
- ")";
- return ss.str();
- }
-
- /*!
- * Translates the given constraint "leftHandSide relation 0" to an equivalent expression for Smt2.
-
- * @param constraint
- * @return An equivalent expression for Smt2.
- */
- std::string translateExpression(storm::ArithConstraint<storm::Polynomial> const& constraint) {
+ std::string translateExpression(storm::RationalFunction const& leftHandSide, storm::CompareRelation const& relation) {
std::stringstream ss;
- ss << "(" << constraint.rel() << " " <<
- constraint.lhs().toString(false, useReadableVarNames) << " " <<
+ ss << "(" << relation << " " <<
+ leftHandSide.toString(false, useReadableVarNames) << " " <<
"0 " <<
")";
return ss.str();
}
-#endif
+
/*!
* Translates the given variable to an equivalent expression for Smt2.
*
@@ -126,7 +111,7 @@ namespace storm {
}
-#ifdef STORM_HAVE_CARL
+
/*! Checks whether the variables in the given set are already declared and creates them if necessary
* @param variables the set of variables to check
*/
@@ -167,7 +152,6 @@ namespace storm {
}
return result;
}
-#endif
private:
// The manager that can be used to build expressions.
diff --git a/src/storm/analysis/GraphConditions.h b/src/storm/analysis/GraphConditions.h
index 48b4aee64..394f11b31 100644
--- a/src/storm/analysis/GraphConditions.h
+++ b/src/storm/analysis/GraphConditions.h
@@ -8,12 +8,12 @@
namespace storm {
namespace analysis {
-
+
template <typename ValueType, typename Enable=void>
struct ConstraintType {
- typedef storm::ArithConstraint<ValueType> val;
+ typedef void* val;
};
-
+
template<typename ValueType>
struct ConstraintType<ValueType, typename std::enable_if<std::is_same<storm::RationalFunction, ValueType>::value>::type> {
typedef carl::Formula<typename ValueType::PolyType::PolyType> val;
diff --git a/src/storm/solver/SmtlibSmtSolver.cpp b/src/storm/solver/SmtlibSmtSolver.cpp
index 8dcd37ddc..69394ec8a 100644
--- a/src/storm/solver/SmtlibSmtSolver.cpp
+++ b/src/storm/solver/SmtlibSmtSolver.cpp
@@ -102,33 +102,6 @@ namespace storm {
writeCommand("( assert " + expressionAdapter->translateExpression(leftHandSide, relation, rightHandSide) + " )", true);
}
- void SmtlibSmtSolver::add(storm::ArithConstraint<storm::RationalFunction> const& constraint) {
- add(constraint.lhs(), constraint.rel());
- }
-
- void SmtlibSmtSolver::add(storm::ArithConstraint<storm::RawPolynomial> const& constraint) {
- //if some of the occurring variables are not declared yet, we will have to.
- std::set<storm::RationalFunctionVariable> variables = constraint.lhs().gatherVariables();
- std::vector<std::string> const varDeclarations = expressionAdapter->checkForUndeclaredVariables(variables);
- for (auto declaration : varDeclarations){
- writeCommand(declaration, true);
- }
- writeCommand("( assert " + expressionAdapter->translateExpression(constraint) + " )", true);
- }
-
- void SmtlibSmtSolver::add(storm::RationalFunctionVariable const& guard, typename storm::ArithConstraint<storm::Polynomial> const& constraint){
- STORM_LOG_THROW((guard.getType()==carl::VariableType::VT_BOOL), storm::exceptions::IllegalArgumentException, "Tried to add a guarded constraint, but the guard is not of type bool.");
- //if some of the occurring variables are not declared yet, we will have to (including the guard!).
- std::set<storm::RationalFunctionVariable> variables = constraint.lhs().gatherVariables();
- variables.insert(guard);
- std::vector<std::string> const varDeclarations = expressionAdapter->checkForUndeclaredVariables(variables);
- for (auto declaration : varDeclarations){
- writeCommand(declaration, true);
- }
- std::string guardName= carl::VariablePool::getInstance().getName(guard, this->useReadableVarNames);
- writeCommand("( assert (=> " + guardName + " " + expressionAdapter->translateExpression(constraint) + " ) )", true);
- }
-
void SmtlibSmtSolver::add(const storm::RationalFunctionVariable& variable, bool value){
STORM_LOG_THROW((variable.getType()==carl::VariableType::VT_BOOL), storm::exceptions::IllegalArgumentException, "Tried to add a constraint that consists of a non-boolean variable.");
std::set<storm::RationalFunctionVariable> variableSet;
diff --git a/src/storm/solver/SmtlibSmtSolver.h b/src/storm/solver/SmtlibSmtSolver.h
index 70e4c325f..6ae64eb92 100644
--- a/src/storm/solver/SmtlibSmtSolver.h
+++ b/src/storm/solver/SmtlibSmtSolver.h
@@ -51,12 +51,7 @@ namespace storm {
//adds the constraint "leftHandSide relation rightHandSide"
virtual void add(storm::RationalFunction const& leftHandSide, storm::CompareRelation const& relation, storm::RationalFunction const& rightHandSide=storm::RationalFunction(0));
- //adds the given carl constraint
- void add(typename storm::ArithConstraint<storm::RationalFunction> const& constraint);
- void add(typename storm::ArithConstraint<storm::RawPolynomial> const& constraint);
-
- // adds the given carl constraint that is guarded by the given guard. The guard should have type 'bool'
- void add(storm::RationalFunctionVariable const& guard, typename storm::ArithConstraint<storm::Polynomial> const& constraint);
+
// asserts that the given variable has the given value. The variable should have type 'bool'
void add(storm::RationalFunctionVariable const& variable, bool value);
@@ -65,10 +60,9 @@ namespace storm {
virtual CheckResult check() override;
virtual CheckResult checkWithAssumptions(std::set<storm::expressions::Expression> const& assumptions) override;
-#ifndef WINDOWS
+
virtual CheckResult checkWithAssumptions(std::initializer_list<storm::expressions::Expression> const& assumptions) override;
-#endif
-
+
bool isNeedsRestart() const;
//Todo: some of these might be added in the future