diff --git a/resources/3rdparty/sylvan/src/storm_function_wrapper.cpp b/resources/3rdparty/sylvan/src/storm_function_wrapper.cpp index 9f1bebc2a..e480a6137 100644 --- a/resources/3rdparty/sylvan/src/storm_function_wrapper.cpp +++ b/resources/3rdparty/sylvan/src/storm_function_wrapper.cpp @@ -215,32 +215,25 @@ void print_storm_rational_function_to_file(storm_rational_function_ptr a, FILE* MTBDD testiTest(storm::RationalFunction const& currentFunction, std::map>> const& replacements) { if (currentFunction.isConstant()) { - std::cout << "Is constant, returning f = " << currentFunction << std::endl; return mtbdd_storm_rational_function((storm_rational_function_ptr)¤tFunction); } - - std::set variablesInFunction = currentFunction.gatherVariables(); - std::cout << "Entered testiTest with f = " << currentFunction << " and " << variablesInFunction.size() << " Variables left." << std::endl; + std::set variablesInFunction = currentFunction.gatherVariables(); std::map>>::const_iterator it = replacements.cbegin(); std::map>>::const_iterator end = replacements.cend(); - + // Walking the (ordered) map enforces an ordering on the MTBDD for (; it != end; ++it) { if (variablesInFunction.find(it->first) != variablesInFunction.cend()) { - std::cout << "Replacing variable!" << std::endl; std::map highReplacement = {{it->first, it->second.second.first}}; std::map lowReplacement = {{it->first, it->second.second.second}}; - std::cout << "High Function = " << currentFunction.substitute(highReplacement) << " w. replc = " << it->second.second.first << std::endl; MTBDD high = testiTest(currentFunction.substitute(highReplacement), replacements); - std::cout << "Low Function = " << currentFunction.substitute(lowReplacement) << " w. replc = " << it->second.second.second << std::endl; MTBDD low = testiTest(currentFunction.substitute(lowReplacement), replacements); LACE_ME return mtbdd_ite(mtbdd_ithvar(it->second.first), high, low); } } - - std::cout << "Found no variable, returning..." << std::endl; + return mtbdd_storm_rational_function((storm_rational_function_ptr)¤tFunction); } diff --git a/src/adapters/CarlAdapter.h b/src/adapters/CarlAdapter.h index b5a91248d..132e553a1 100644 --- a/src/adapters/CarlAdapter.h +++ b/src/adapters/CarlAdapter.h @@ -15,6 +15,7 @@ #include #include #include +#include namespace carl { // Define hash values for all polynomials and rational function. @@ -60,6 +61,7 @@ namespace storm { typedef carl::Variable RationalFunctionVariable; typedef carl::MultivariatePolynomial RawPolynomial; typedef carl::FactorizedPolynomial Polynomial; + typedef carl::Cache> RawPolynomialCache; typedef carl::Relation CompareRelation; typedef carl::RationalFunction RationalFunction; diff --git a/test/functional/storage/SylvanDdTest.cpp b/test/functional/storage/SylvanDdTest.cpp index 83e7e3d80..7ad91a531 100644 --- a/test/functional/storage/SylvanDdTest.cpp +++ b/test/functional/storage/SylvanDdTest.cpp @@ -163,7 +163,7 @@ TEST(SylvanDd, BddExistAbstractRepresentative) { EXPECT_TRUE(bddX0Y0Z0 == representative_xyz); } -TEST(SylvanDd, AddMinExistAbstractRepresentative) { +TEST(SylvanDd, AddMinAbstractRepresentative) { std::shared_ptr> manager(new storm::dd::DdManager()); storm::dd::Bdd bddZero; @@ -268,7 +268,7 @@ TEST(SylvanDd, AddMinExistAbstractRepresentative) { EXPECT_TRUE(representative_complex_xyz == comparison_complex_xyz); } -TEST(SylvanDd, AddMaxExistAbstractRepresentative) { +TEST(SylvanDd, AddMaxAbstractRepresentative) { std::shared_ptr> manager(new storm::dd::DdManager()); storm::dd::Bdd bddZero; @@ -431,12 +431,16 @@ TEST(SylvanDd, RationalFunctionLeaveReplacementNonVariable) { TEST(SylvanDd, RationalFunctionLeaveReplacementSimpleVariable) { std::shared_ptr> manager(new storm::dd::DdManager()); - // The cache that is used in case the underlying type needs a cache. - std::shared_ptr>> cache = std::make_shared>>(); - storm::dd::Add function; - carl::Variable x = carl::freshRealVariable("x"); - storm::RationalFunction variableX = storm::RationalFunction(typename storm::RationalFunction::PolyType(typename storm::RationalFunction::PolyType::PolyType(x), cache)); + + std::shared_ptr cache = std::make_shared(); + + carl::StringParser parser; + parser.setVariables({"x"}); + + storm::RawPolynomial polyX = parser.parseMultivariatePolynomial("x"); + storm::RationalFunction variableX = storm::RationalFunction(storm::Polynomial(polyX, cache)); + ASSERT_NO_THROW(function = manager->template getConstant(variableX)); std::pair xExpr; @@ -445,7 +449,7 @@ TEST(SylvanDd, RationalFunctionLeaveReplacementSimpleVariable) { std::map>> replacementMap; storm::RationalNumber rnOneThird = storm::RationalNumber(1) / storm::RationalNumber(3); storm::RationalNumber rnTwoThird = storm::RationalNumber(2) / storm::RationalNumber(3); - replacementMap.insert(std::make_pair(x, std::make_pair(xExpr.first, std::make_pair(rnOneThird, rnTwoThird)))); + replacementMap.insert(std::make_pair(parser.variables().find("x")->second, std::make_pair(xExpr.first, std::make_pair(rnOneThird, rnTwoThird)))); storm::dd::Add replacedAddSimpleX = function.replaceLeaves(replacementMap); @@ -465,14 +469,13 @@ TEST(SylvanDd, RationalFunctionLeaveReplacementSimpleVariable) { TEST(SylvanDd, RationalFunctionLeaveReplacementTwoVariables) { std::shared_ptr> manager(new storm::dd::DdManager()); - // The cache that is used in case the underlying type needs a cache. - std::shared_ptr>> cache = std::make_shared>>(); - storm::dd::Add function; - carl::Variable x = carl::freshRealVariable("x"); - carl::Variable y = carl::freshRealVariable("y"); - storm::RationalFunction variableX = storm::RationalFunction(typename storm::RationalFunction::PolyType(typename storm::RationalFunction::PolyType::PolyType(x), cache)); - storm::RationalFunction variableY = storm::RationalFunction(typename storm::RationalFunction::PolyType(typename storm::RationalFunction::PolyType::PolyType(y), cache)); + std::shared_ptr cache = std::make_shared(); + carl::StringParser parser; + parser.setVariables({"x", "y"}); + + storm::RationalFunction variableX(storm::Polynomial(parser.template parseMultivariatePolynomial("x"), cache)); + storm::RationalFunction variableY(storm::Polynomial(parser.template parseMultivariatePolynomial("y"), cache)); ASSERT_NO_THROW(function = manager->template getConstant(variableX * variableY)); std::pair xExpr; @@ -485,8 +488,8 @@ TEST(SylvanDd, RationalFunctionLeaveReplacementTwoVariables) { storm::RationalNumber rnTwoThird = storm::RationalNumber(2) / storm::RationalNumber(3); storm::RationalNumber rnOne = storm::RationalNumber(1); storm::RationalNumber rnTen = storm::RationalNumber(10); - replacementMap.insert(std::make_pair(x, std::make_pair(xExpr.first, std::make_pair(rnOneThird, rnTwoThird)))); - replacementMap.insert(std::make_pair(y, std::make_pair(yExpr.first, std::make_pair(rnOne, rnTen)))); + replacementMap.insert(std::make_pair(parser.variables().find("x")->second, std::make_pair(xExpr.first, std::make_pair(rnOneThird, rnTwoThird)))); + replacementMap.insert(std::make_pair(parser.variables().find("y")->second, std::make_pair(yExpr.first, std::make_pair(rnOne, rnTen)))); storm::dd::Add replacedAdd = function.replaceLeaves(replacementMap); @@ -507,67 +510,35 @@ TEST(SylvanDd, RationalFunctionLeaveReplacementTwoVariables) { EXPECT_TRUE(replacedAdd == complexAdd); } -TEST(SylvanDd, RationalFunctionBullshitTest) { - // The cache that is used in case the underlying type needs a cache. - std::shared_ptr>> cache = std::make_shared>>(); - - carl::Variable x = carl::freshRealVariable("x"); - carl::Variable y = carl::freshRealVariable("y"); - carl::Variable z = carl::freshRealVariable("z"); - storm::RationalFunction variableX = storm::RationalFunction(typename storm::RationalFunction::PolyType(typename storm::RationalFunction::PolyType::PolyType(x), cache)); - storm::RationalFunction variableY = storm::RationalFunction(typename storm::RationalFunction::PolyType(typename storm::RationalFunction::PolyType::PolyType(y), cache)); - storm::RationalFunction variableZ = storm::RationalFunction(typename storm::RationalFunction::PolyType(typename storm::RationalFunction::PolyType::PolyType(z), cache)); - - storm::RationalFunction constantOne(1); - storm::RationalFunction constantTwo(2); - storm::RationalFunction constantOneDivTwo(constantOne / constantTwo); - storm::RationalFunction tmpFunctionA(constantOneDivTwo); - tmpFunctionA *= variableZ; - tmpFunctionA /= variableY; - storm::RationalFunction tmpFunctionB(variableX); - tmpFunctionB *= variableY; - - //storm::RationalFunction rationalFunction(two * x + x*y + constantOneDivTwo * z / y); - storm::RationalFunction rationalFunction(constantTwo); - rationalFunction *= variableX; - rationalFunction += tmpFunctionB; - rationalFunction += tmpFunctionA; +TEST(SylvanDd, RationalFunctionCarlSubstituteTest) { + std::shared_ptr cache = std::make_shared(); + carl::StringParser parser; + parser.setVariables({"x", "y", "z"}); + storm::RationalFunction zHalfed = storm::RationalFunction(storm::Polynomial(parser.template parseMultivariatePolynomial("z"), cache), storm::Polynomial(parser.template parseMultivariatePolynomial("2"), cache)); + storm::RationalFunction rationalFunction = storm::RationalFunction(storm::Polynomial(parser.parseMultivariatePolynomial("2*x+x*y"), cache), storm::Polynomial(parser.parseMultivariatePolynomial("1"), cache)) + zHalfed; - std::map replacement = {{x, storm::RationalNumber(2)}}; + std::map replacement = {{parser.variables().find("x")->second, storm::RationalNumber(2)}}; storm::RationalFunction subX = rationalFunction.substitute(replacement); - ASSERT_EQ(subX, storm::RationalFunction(4) + storm::RationalFunction(2) * variableY + tmpFunctionA); + storm::RationalFunction cmp = storm::RationalFunction(storm::Polynomial(parser.template parseMultivariatePolynomial("4+2*y"), cache), storm::Polynomial(parser.template parseMultivariatePolynomial("1"), cache)) + zHalfed; + EXPECT_EQ(subX, cmp); + + storm::RawPolynomial poly(parser.template parseMultivariatePolynomial("2*x+x*y") + parser.template parseMultivariatePolynomial("z") / storm::RationalNumber(2)); + storm::RawPolynomial polySub = poly.substitute(replacement); + EXPECT_EQ(polySub, parser.template parseMultivariatePolynomial("4+2*y") + parser.template parseMultivariatePolynomial("z") / storm::RationalNumber(2)); } TEST(SylvanDd, RationalFunctionLeaveReplacementComplexFunction) { std::shared_ptr> manager(new storm::dd::DdManager()); - // The cache that is used in case the underlying type needs a cache. - std::shared_ptr>> cache = std::make_shared>>(); - storm::dd::Add function; - carl::Variable x = carl::freshRealVariable("x"); - carl::Variable y = carl::freshRealVariable("y"); - carl::Variable z = carl::freshRealVariable("z"); - storm::RationalFunction variableX = storm::RationalFunction(typename storm::RationalFunction::PolyType(typename storm::RationalFunction::PolyType::PolyType(x), cache)); - storm::RationalFunction variableY = storm::RationalFunction(typename storm::RationalFunction::PolyType(typename storm::RationalFunction::PolyType::PolyType(y), cache)); - storm::RationalFunction variableZ = storm::RationalFunction(typename storm::RationalFunction::PolyType(typename storm::RationalFunction::PolyType::PolyType(z), cache)); - - storm::RationalFunction constantOne(1); - storm::RationalFunction constantTwo(2); - storm::RationalFunction constantOneDivTwo(constantOne / constantTwo); - storm::RationalFunction tmpFunctionA(constantOneDivTwo); - tmpFunctionA *= variableZ; - tmpFunctionA /= variableY; - storm::RationalFunction tmpFunctionB(variableX); - tmpFunctionB *= variableY; - + std::shared_ptr cache = std::make_shared(); + carl::StringParser parser; + parser.setVariables({"x", "y", "z"}); + storm::RationalFunction zDivTwoY = storm::RationalFunction(storm::Polynomial(parser.template parseMultivariatePolynomial("z"), cache), storm::Polynomial(parser.template parseMultivariatePolynomial("2*y"), cache)); + //storm::RationalFunction rationalFunction(two * x + x*y + constantOneDivTwo * z / y); - storm::RationalFunction rationalFunction(constantTwo); - rationalFunction *= variableX; - rationalFunction += tmpFunctionB; - rationalFunction += tmpFunctionA; - + storm::RationalFunction rationalFunction = storm::RationalFunction(storm::Polynomial(parser.parseMultivariatePolynomial("2*x+x*y"), cache), storm::Polynomial(parser.parseMultivariatePolynomial("1"), cache)) + zDivTwoY; ASSERT_NO_THROW(function = manager->template getConstant(rationalFunction)); std::pair xExpr; @@ -584,9 +555,9 @@ TEST(SylvanDd, RationalFunctionLeaveReplacementComplexFunction) { storm::RationalNumber rnSeven(7); storm::RationalNumber rnEleven(11); storm::RationalNumber rnThirteen(13); - replacementMap.insert(std::make_pair(x, std::make_pair(xExpr.first, std::make_pair(rnTwo, rnSeven)))); - replacementMap.insert(std::make_pair(y, std::make_pair(yExpr.first, std::make_pair(rnThree, rnEleven)))); - replacementMap.insert(std::make_pair(z, std::make_pair(zExpr.first, std::make_pair(rnFive, rnThirteen)))); + replacementMap.insert(std::make_pair(parser.variables().find("x")->second, std::make_pair(xExpr.first, std::make_pair(rnTwo, rnSeven)))); + replacementMap.insert(std::make_pair(parser.variables().find("y")->second, std::make_pair(yExpr.first, std::make_pair(rnThree, rnEleven)))); + replacementMap.insert(std::make_pair(parser.variables().find("z")->second, std::make_pair(zExpr.first, std::make_pair(rnFive, rnThirteen)))); storm::dd::Add replacedAdd = function.replaceLeaves(replacementMap); @@ -599,31 +570,31 @@ TEST(SylvanDd, RationalFunctionLeaveReplacementComplexFunction) { auto f = [&](bool x, bool y, bool z) { storm::RationalNumber result(2); - if (x) { + if (!x) { result *= rnSeven; } else { result *= rnTwo; } storm::RationalNumber partTwo(1); - if (x) { + if (!x) { partTwo *= rnSeven; } else { partTwo *= rnTwo; } - if (y) { + if (!y) { partTwo *= rnEleven; } else { partTwo *= rnThree; } storm::RationalNumber partThree(1); - if (z) { + if (!z) { partThree *= rnThirteen; } else { partThree *= rnFive; } - if (y) { + if (!y) { partThree /= storm::RationalNumber(2) * rnEleven; } else { partThree /= storm::RationalNumber(2) * rnThree; @@ -642,94 +613,15 @@ TEST(SylvanDd, RationalFunctionLeaveReplacementComplexFunction) { + ((bddX1 && (bddY1 && bddZ0)).template toAdd() * manager->template getConstant(storm::RationalFunction(f(true, true, false)))) + ((bddX1 && (bddY1 && bddZ1)).template toAdd() * manager->template getConstant(storm::RationalFunction(f(true, true, true)))); - EXPECT_EQ(4ul, replacedAdd.getNonZeroCount()); - EXPECT_EQ(4ul, replacedAdd.getLeafCount()); - EXPECT_EQ(7ul, replacedAdd.getNodeCount()); + EXPECT_EQ(8ul, replacedAdd.getNonZeroCount()); + EXPECT_EQ(8ul, replacedAdd.getLeafCount()); + EXPECT_EQ(15ul, replacedAdd.getNodeCount()); EXPECT_TRUE(replacedAdd == complexAdd); replacedAdd.exportToDot("sylvan_replacedAddC.dot"); complexAdd.exportToDot("sylvan_complexAddC.dot"); } -TEST(SylvanDd, RationalFunctionLeaveReplacementComplexFunction2) { - std::shared_ptr> manager(new storm::dd::DdManager()); - - // The cache that is used in case the underlying type needs a cache. - std::shared_ptr>> cache = std::make_shared>>(); - - storm::dd::Add function; - carl::Variable x = carl::freshRealVariable("x"); - carl::Variable y = carl::freshRealVariable("y"); - carl::Variable z = carl::freshRealVariable("z"); - - storm::RationalFunction constantOne(1); - storm::RationalFunction constantTwo(2); - - storm::RationalFunction variableX = storm::RationalFunction(typename storm::RationalFunction::PolyType(typename storm::RationalFunction::PolyType::PolyType(x), cache)); - storm::RationalFunction variableY = storm::RationalFunction(typename storm::RationalFunction::PolyType(typename storm::RationalFunction::PolyType::PolyType(y), cache)); - storm::RationalFunction variableZ = storm::RationalFunction(typename storm::RationalFunction::PolyType(typename storm::RationalFunction::PolyType::PolyType(z), cache)); - - storm::RationalFunction constantOneDivTwo(constantOne / constantTwo); - storm::RationalFunction tmpFunctionA(constantOneDivTwo); - tmpFunctionA *= variableZ; - tmpFunctionA /= variableY; - storm::RationalFunction tmpFunctionB(variableX); - tmpFunctionB *= variableY; - - //storm::RationalFunction rationalFunction(two * x + x*y + constantOneDivTwo * z / y); - storm::RationalFunction rationalFunction(constantTwo); - rationalFunction *= variableX; - rationalFunction += tmpFunctionB; - rationalFunction += tmpFunctionA; - - ASSERT_NO_THROW(function = manager->template getConstant(rationalFunction)); - - EXPECT_EQ(0ul, function.getNonZeroCount()); - EXPECT_EQ(1ul, function.getLeafCount()); - EXPECT_EQ(1ul, function.getNodeCount()); - - std::pair xExpr; - std::pair yExpr; - std::pair zExpr; - ASSERT_NO_THROW(xExpr = manager->addMetaVariable("x", 0, 1)); - ASSERT_NO_THROW(yExpr = manager->addMetaVariable("y", 0, 1)); - ASSERT_NO_THROW(zExpr = manager->addMetaVariable("z", 0, 1)); - - storm::dd::Bdd bddX0 = manager->getEncoding(xExpr.first, 0); - storm::dd::Bdd bddX1 = manager->getEncoding(xExpr.first, 1); - storm::dd::Bdd bddY0 = manager->getEncoding(yExpr.first, 0); - storm::dd::Bdd bddY1 = manager->getEncoding(yExpr.first, 1); - storm::dd::Bdd bddZ0 = manager->getEncoding(zExpr.first, 0); - storm::dd::Bdd bddZ1 = manager->getEncoding(zExpr.first, 1); - - storm::dd::Add functionSimpleX; - ASSERT_NO_THROW(functionSimpleX = manager->template getConstant(storm::RationalFunction(variableX))); - - std::map>> replacementMapSimpleX; - - storm::RationalNumber rnOneThird = storm::RationalNumber(1) / storm::RationalNumber(3); - storm::RationalNumber rnTwoThird = storm::RationalNumber(2) / storm::RationalNumber(3); - replacementMapSimpleX.insert(std::make_pair(x, std::make_pair(xExpr.first, std::make_pair(rnOneThird, rnTwoThird)))); - - storm::dd::Add replacedAddSimpleX = functionSimpleX.replaceLeaves(replacementMapSimpleX); - replacedAddSimpleX.exportToDot("sylvan_replacementMapSimpleX.dot"); - - std::map>> replacementMap; - - storm::RationalNumber rnMinusOne(-1); - storm::RationalNumber rnOne(1); - storm::RationalNumber rnPointOne = storm::RationalNumber(1) / storm::RationalNumber(10); - storm::RationalNumber rnPointSixSix = storm::RationalNumber(2) / storm::RationalNumber(3); - storm::RationalNumber rnPointFive = storm::RationalNumber(1) / storm::RationalNumber(2); - - replacementMap.insert(std::make_pair(x, std::make_pair(xExpr.first, std::make_pair(rnMinusOne, rnOne)))); - replacementMap.insert(std::make_pair(y, std::make_pair(yExpr.first, std::make_pair(rnPointOne, rnPointSixSix)))); - replacementMap.insert(std::make_pair(z, std::make_pair(zExpr.first, std::make_pair(rnPointFive, rnOne)))); - - storm::dd::Add replacedAdd = function.replaceLeaves(replacementMap); - replacedAdd.exportToDot("sylvan_replaceLeave.dot"); -} - TEST(SylvanDd, RationalFunctionConstants) { std::shared_ptr> manager(new storm::dd::DdManager()); storm::dd::Add zero; @@ -755,33 +647,15 @@ TEST(SylvanDd, RationalFunctionConstants) { EXPECT_EQ(1ul, two.getLeafCount()); EXPECT_EQ(1ul, two.getNodeCount()); - // The cache that is used in case the underlying type needs a cache. - std::shared_ptr>> cache = std::make_shared>>(); - storm::dd::Add function; - carl::Variable x = carl::freshRealVariable("x"); - carl::Variable y = carl::freshRealVariable("y"); - carl::Variable z = carl::freshRealVariable("z"); + std::shared_ptr cache = std::make_shared(); + carl::StringParser parser; + parser.setVariables({"x", "y", "z"}); - storm::RationalFunction constantOne(1); + storm::RationalFunction partA = storm::RationalFunction(storm::Polynomial(parser.template parseMultivariatePolynomial("2*x+x*y"), cache)); + storm::RationalFunction partB = storm::RationalFunction(storm::Polynomial(parser.template parseMultivariatePolynomial("z"), cache), storm::Polynomial(parser.template parseMultivariatePolynomial("2*y"), cache)); - storm::RationalFunction variableX = storm::RationalFunction(typename storm::RationalFunction::PolyType(typename storm::RationalFunction::PolyType::PolyType(x), cache)); - storm::RationalFunction variableY = storm::RationalFunction(typename storm::RationalFunction::PolyType(typename storm::RationalFunction::PolyType::PolyType(y), cache)); - storm::RationalFunction variableZ = storm::RationalFunction(typename storm::RationalFunction::PolyType(typename storm::RationalFunction::PolyType::PolyType(z), cache)); - - storm::RationalFunction constantOneDivTwo(constantOne / constantTwo); - storm::RationalFunction tmpFunctionA(constantOneDivTwo); - tmpFunctionA *= variableZ; - tmpFunctionA /= variableY; - storm::RationalFunction tmpFunctionB(variableX); - tmpFunctionB *= variableY; - - - //storm::RationalFunction rationalFunction(two * x + x*y + constantOneDivTwo * z / y); - storm::RationalFunction rationalFunction(constantTwo); - rationalFunction *= variableX; - rationalFunction += tmpFunctionB; - rationalFunction += tmpFunctionA; + storm::RationalFunction rationalFunction = storm::RationalFunction(partA + partB); ASSERT_NO_THROW(function = manager->template getConstant(rationalFunction));