From a994b80931f4f7af8c1a07ccd559b42db86748c1 Mon Sep 17 00:00:00 2001 From: sjunges Date: Sun, 13 Aug 2017 18:58:36 +0200 Subject: [PATCH] getting rid of outdated carl simple constraint usage --- src/storm/adapters/Smt2ExpressionAdapter.h | 30 +++++----------------- src/storm/analysis/GraphConditions.h | 6 ++--- src/storm/solver/SmtlibSmtSolver.cpp | 27 ------------------- src/storm/solver/SmtlibSmtSolver.h | 12 +++------ 4 files changed, 13 insertions(+), 62 deletions(-) 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 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 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 struct ConstraintType { - typedef storm::ArithConstraint val; + typedef void* val; }; - + template struct ConstraintType::value>::type> { typedef carl::Formula 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 const& constraint) { - add(constraint.lhs(), constraint.rel()); - } - - void SmtlibSmtSolver::add(storm::ArithConstraint const& constraint) { - //if some of the occurring variables are not declared yet, we will have to. - std::set variables = constraint.lhs().gatherVariables(); - std::vector 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 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 variables = constraint.lhs().gatherVariables(); - variables.insert(guard); - std::vector 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 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 const& constraint); - void add(typename storm::ArithConstraint 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 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 const& assumptions) override; -#ifndef WINDOWS + virtual CheckResult checkWithAssumptions(std::initializer_list const& assumptions) override; -#endif - + bool isNeedsRestart() const; //Todo: some of these might be added in the future