From 4804ed636d974215df466a1ebe3ac387b5d4befd Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 13 Oct 2014 17:24:09 +0200 Subject: [PATCH] Adapted some code to work with carl. Former-commit-id: 722669f4bf7856f8479176c3feec2bd869eb70b4 --- src/adapters/ExplicitModelAdapter.h | 1 - src/adapters/extendedCarl.h | 35 +++++++++------- src/storage/SparseMatrix.cpp | 8 ++-- ...tronglyConnectedComponentDecomposition.cpp | 2 +- .../expressions/ExpressionEvaluation.h | 40 +++++++++++++------ src/storage/parameters.h | 6 ++- src/stormParametric.cpp | 6 +-- 7 files changed, 61 insertions(+), 37 deletions(-) diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index 35a7d1249..9699f1745 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -646,7 +646,6 @@ namespace storm { ModelComponents modelComponents; expressions::ExpressionEvaluation eval; - VariableInformation variableInformation; for (auto const& integerVariable : program.getGlobalIntegerVariables()) { variableInformation.variableToBoundsMap[integerVariable.getName()] = std::make_pair(integerVariable.getLowerBoundExpression().evaluateAsInt(), integerVariable.getUpperBoundExpression().evaluateAsInt()); diff --git a/src/adapters/extendedCarl.h b/src/adapters/extendedCarl.h index 90c1cef4d..fddb4950f 100644 --- a/src/adapters/extendedCarl.h +++ b/src/adapters/extendedCarl.h @@ -1,4 +1,4 @@ -/** +/** * @file: extendedCarl.h * @author: Sebastian Junges * @@ -13,22 +13,29 @@ #include #include #include +#include namespace carl { -template -inline size_t hash_value(carl::MultivariatePolynomial const& p) -{ - std::hash> h; - return h(p); -} -template -inline size_t hash_value(carl::RationalFunction const& f) -{ - std::hash h; - return h(f.nominator()) ^ h(f.denominator()); -} - + template + inline size_t hash_value(carl::MultivariatePolynomial const& p) + { + std::hash> h; + return h(p); + } + template + inline size_t hash_value(carl::RationalFunction const& f) + { + std::hash h; + return h(f.nominator()) ^ h(f.denominator()); + } + + template + inline size_t hash_value(carl::FactorizedPolynomial const& p) + { + std::hash> h; + return h(p); + } } diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index 6d9531428..0b84e9936 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -239,7 +239,7 @@ namespace storm { template SparseMatrix::SparseMatrix(index_type columnCount, std::vector const& rowIndications, std::vector> const& columnsAndValues, std::vector const& rowGroupIndices) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(columnsAndValues.size()), nonzeroEntryCount(0), columnsAndValues(columnsAndValues), rowIndications(rowIndications), rowGroupIndices(rowGroupIndices) { for (auto const& element : *this) { - if (element.getValue() != storm::utility::constantZero()) { + if (!storm::utility::isZero(element.getValue())) { ++this->nonzeroEntryCount; } } @@ -248,7 +248,7 @@ namespace storm { template SparseMatrix::SparseMatrix(index_type columnCount, std::vector&& rowIndications, std::vector>&& columnsAndValues, std::vector&& rowGroupIndices) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(columnsAndValues.size()), nonzeroEntryCount(0), columnsAndValues(std::move(columnsAndValues)), rowIndications(std::move(rowIndications)), rowGroupIndices(std::move(rowGroupIndices)) { for (auto const& element : *this) { - if (element.getValue() != storm::utility::constantZero()) { + if (!storm::utility::isZero(element.getValue())) { ++this->nonzeroEntryCount; } } @@ -604,7 +604,7 @@ namespace storm { // First, we need to count how many entries each column has. for (index_type group = 0; group < columnCount; ++group) { for (auto const& transition : joinGroups ? this->getRowGroup(group) : this->getRow(group)) { - if (transition.getValue() != storm::utility::constantZero()) { + if (!storm::utility::isZero(transition.getValue())) { ++rowIndications[transition.getColumn() + 1]; } } @@ -623,7 +623,7 @@ namespace storm { // Now we are ready to actually fill in the values of the transposed matrix. for (index_type group = 0; group < columnCount; ++group) { for (auto const& transition : joinGroups ? this->getRowGroup(group) : this->getRow(group)) { - if (transition.getValue() != storm::utility::constantZero()) { + if (!storm::utility::isZero(transition.getValue())) { columnsAndValues[nextIndices[transition.getColumn()]] = std::make_pair(group, transition.getValue()); nextIndices[transition.getColumn()]++; } diff --git a/src/storage/StronglyConnectedComponentDecomposition.cpp b/src/storage/StronglyConnectedComponentDecomposition.cpp index 7c6988303..63b6d1de5 100644 --- a/src/storage/StronglyConnectedComponentDecomposition.cpp +++ b/src/storage/StronglyConnectedComponentDecomposition.cpp @@ -171,7 +171,7 @@ namespace storm { p.push_back(currentState); for (auto const& successor : transitionMatrix.getRowGroup(currentState)) { - if (subsystem.get(successor.getColumn()) && successor.getValue() != storm::utility::constantZero()) { + if (subsystem.get(successor.getColumn()) && !storm::utility::isZero(successor.getValue())) { if (currentState == successor.getColumn()) { statesWithSelfLoop.set(currentState); } diff --git a/src/storage/expressions/ExpressionEvaluation.h b/src/storage/expressions/ExpressionEvaluation.h index 7b35109f7..95a076088 100644 --- a/src/storage/expressions/ExpressionEvaluation.h +++ b/src/storage/expressions/ExpressionEvaluation.h @@ -40,19 +40,29 @@ namespace expressions { { typedef std::map type; }; + + struct ExpressionEvaluationSettings { + static const bool useFactorizedPolynomials = false; + }; + + struct FactorizedPolynomialsEvaluationSettings : ExpressionEvaluationSettings { + static const bool useFactorizedPolynomials = true; + }; #endif - template + template class ExpressionEvaluationVisitor : public ExpressionVisitor { public: ExpressionEvaluationVisitor(S* sharedState) - : mSharedState(sharedState) + : mSharedState(sharedState), cache(new carl::Cache>()) { } - virtual ~ExpressionEvaluationVisitor() {} + virtual ~ExpressionEvaluationVisitor() { + + } virtual void visit(IfThenElseExpression const* expression) { @@ -101,13 +111,13 @@ namespace expressions { auto it = mSharedState->find(varName); if(it != mSharedState->end()) { - mValue = T(it->second); + mValue = T(typename T::PolyType(typename T::PolyType::PolyType(it->second), cache)); } else { carl::Variable nVar = carl::VariablePool::getInstance().getFreshVariable(varName); mSharedState->emplace(varName,nVar); - mValue = T(nVar); + mValue = convertVariableToPolynomial(nVar); } } virtual void visit(UnaryBooleanFunctionExpression const* expression) @@ -124,17 +134,25 @@ namespace expressions { } virtual void visit(IntegerLiteralExpression const* expression) { - // mValue = T(typename T::CoeffType(std::to_string(expression->getValue()), 10)); - mValue = T(expression->getValue()); + mValue = T(typename T::PolyType(typename T::CoeffType(expression->getValue()))); } virtual void visit(DoubleLiteralExpression const* expression) { std::stringstream str; str << std::fixed << std::setprecision( 3 ) << expression->getValue(); - mValue = T(carl::rationalize(str.str())); - + mValue = T(carl::rationalize(str.str())); } + template> = carl::dummy> + T convertVariableToPolynomial(carl::Variable const& nVar) { + return T(typename T::PolyType(typename T::PolyType::PolyType(nVar), cache)); + } + + template> = carl::dummy> + T convertVariableToPolynomial(carl::Variable const& nVar) { + return T(nVar); + } + const T& value() const { return mValue; @@ -143,6 +161,7 @@ namespace expressions { private: S* mSharedState; T mValue; + carl::Cache>* cache; }; template @@ -182,9 +201,6 @@ namespace expressions { return expr.evaluateAsDouble(val); } }; - - - } } diff --git a/src/storage/parameters.h b/src/storage/parameters.h index 923ef5fc9..8a017638e 100644 --- a/src/storage/parameters.h +++ b/src/storage/parameters.h @@ -10,9 +10,11 @@ namespace storm { - typedef carl::MultivariatePolynomial Polynomial; +// typedef carl::MultivariatePolynomial Polynomial; typedef carl::Variable Variable; - + typedef carl::MultivariatePolynomial RawPolynomial; + typedef carl::FactorizedPolynomial Polynomial; +// typedef RawPolynomial Polynomial; typedef carl::CompareRelation CompareRelation; typedef carl::RationalFunction RationalFunction; diff --git a/src/stormParametric.cpp b/src/stormParametric.cpp index f5f0271a0..d22c210bb 100644 --- a/src/stormParametric.cpp +++ b/src/stormParametric.cpp @@ -9,7 +9,7 @@ #include "src/utility/export.h" #include "src/modelchecker/reachability/CollectConstraints.h" -#include "src/modelchecker/reachability/DirectEncoding.h" +//#include "src/modelchecker/reachability/DirectEncoding.h" #include "src/modelchecker/reachability/SparseSccModelChecker.h" #include "src/storage/parameters.h" /*! @@ -75,8 +75,8 @@ int main(const int argc, const char** argv) { } if(storm::settings::parametricSettings().exportToSmt2File()) { - storm::modelchecker::reachability::DirectEncoding dec; - //storm::utility::exportStreamToFile(dec.encodeAsSmt2(modelChecker.getMatrix(), parameters,)); +// storm::modelchecker::reachability::DirectEncoding dec; +// storm::utility::exportStreamToFile(dec.encodeAsSmt2(modelChecker.getMatrix(), parameters,)); }