sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

getting rid of outdated carl simple constraint usage

tempestpy_adaptions
sjunges 7 years ago
parent
b4a8833e3f
commit
a994b80931
4 changed files with 13 additions and 62 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 30
      src/storm/adapters/Smt2ExpressionAdapter.h
  2. 6
      src/storm/analysis/GraphConditions.h
  3. 27
      src/storm/solver/SmtlibSmtSolver.cpp
  4. 12
      src/storm/solver/SmtlibSmtSolver.h

30
src/storm/adapters/Smt2ExpressionAdapter.h
View File

@ -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.

6
src/storm/analysis/GraphConditions.h
View File

@ -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;

27
src/storm/solver/SmtlibSmtSolver.cpp
View File

@ -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;

12
src/storm/solver/SmtlibSmtSolver.h
View File

@ -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

Write Preview
Loading…
Cancel
Save