Leave Replacement finally working.

Former-commit-id: 239ea6d897

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<storm::RationalFunctionVariable, std::pair<uint32_t, std::pair<storm::RationalNumber, storm::RationalNumber>>> const& replacements) {
 	if (currentFunction.isConstant()) {
-		std::cout << "Is constant, returning f = " << currentFunction << std::endl;
 		return mtbdd_storm_rational_function((storm_rational_function_ptr)&currentFunction);
 	}
-	
-	std::set<storm::RationalFunctionVariable> variablesInFunction = currentFunction.gatherVariables();
-	std::cout << "Entered testiTest with f = " << currentFunction << " and " << variablesInFunction.size() << " Variables left." << std::endl;
 
+	std::set<storm::RationalFunctionVariable> variablesInFunction = currentFunction.gatherVariables();
 	std::map<storm::RationalFunctionVariable, std::pair<uint32_t, std::pair<storm::RationalNumber, storm::RationalNumber>>>::const_iterator it = replacements.cbegin();
 	std::map<storm::RationalFunctionVariable, std::pair<uint32_t, std::pair<storm::RationalNumber, storm::RationalNumber>>>::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<storm::RationalFunctionVariable, storm::RationalNumber> highReplacement = {{it->first, it->second.second.first}};
 			std::map<storm::RationalFunctionVariable, storm::RationalNumber> 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)&currentFunction);
 }
 

src/adapters/CarlAdapter.h

@@ -15,6 +15,7 @@
 #include <carl/core/FactorizedPolynomial.h>
 #include <carl/core/Relation.h>
 #include <carl/core/SimpleConstraint.h>
+#include <carl/util/stringparser.h>
 
 namespace carl {
     // Define hash values for all polynomials and rational function.
@@ -60,6 +61,7 @@ namespace storm {
     typedef carl::Variable RationalFunctionVariable;
     typedef carl::MultivariatePolynomial<RationalNumber> RawPolynomial;
     typedef carl::FactorizedPolynomial<RawPolynomial> Polynomial;
+	typedef carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>> RawPolynomialCache;
     typedef carl::Relation CompareRelation;
     
     typedef carl::RationalFunction<Polynomial, true> RationalFunction;

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<storm::dd::DdManager<storm::dd::DdType::Sylvan>> manager(new storm::dd::DdManager<storm::dd::DdType::Sylvan>());
 
 	storm::dd::Bdd<storm::dd::DdType::Sylvan> 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<storm::dd::DdManager<storm::dd::DdType::Sylvan>> manager(new storm::dd::DdManager<storm::dd::DdType::Sylvan>());
 
 	storm::dd::Bdd<storm::dd::DdType::Sylvan> bddZero;
@@ -431,12 +431,16 @@ TEST(SylvanDd, RationalFunctionLeaveReplacementNonVariable) {
 TEST(SylvanDd, RationalFunctionLeaveReplacementSimpleVariable) {
 	std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::Sylvan>> manager(new storm::dd::DdManager<storm::dd::DdType::Sylvan>());
 	
-	// The cache that is used in case the underlying type needs a cache.
-	std::shared_ptr<carl::Cache<carl::PolynomialFactorizationPair<storm::RawPolynomial>>> cache = std::make_shared<carl::Cache<carl::PolynomialFactorizationPair<storm::RawPolynomial>>>();
-	
 	storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalFunction> 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<storm::RawPolynomialCache> cache = std::make_shared<storm::RawPolynomialCache>();
+	
+	carl::StringParser parser;
+	parser.setVariables({"x"});
+	
+	storm::RawPolynomial polyX = parser.parseMultivariatePolynomial<storm::RationalNumber>("x");	
+	storm::RationalFunction variableX = storm::RationalFunction(storm::Polynomial(polyX, cache));
+	
 	ASSERT_NO_THROW(function = manager->template getConstant<storm::RationalFunction>(variableX));
 	
 	std::pair<storm::expressions::Variable, storm::expressions::Variable> xExpr;
@@ -445,7 +449,7 @@ TEST(SylvanDd, RationalFunctionLeaveReplacementSimpleVariable) {
 	std::map<storm::RationalFunctionVariable, std::pair<storm::expressions::Variable, std::pair<storm::RationalNumber, storm::RationalNumber>>> 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<storm::dd::DdType::Sylvan, storm::RationalFunction> replacedAddSimpleX = function.replaceLeaves(replacementMap);
 	
@@ -465,14 +469,13 @@ TEST(SylvanDd, RationalFunctionLeaveReplacementSimpleVariable) {
 TEST(SylvanDd, RationalFunctionLeaveReplacementTwoVariables) {
 	std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::Sylvan>> manager(new storm::dd::DdManager<storm::dd::DdType::Sylvan>());
 	
-	// The cache that is used in case the underlying type needs a cache.
-	std::shared_ptr<carl::Cache<carl::PolynomialFactorizationPair<storm::RawPolynomial>>> cache = std::make_shared<carl::Cache<carl::PolynomialFactorizationPair<storm::RawPolynomial>>>();
-	
 	storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalFunction> 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));