From 61d4bb956c01437662c1d11fbf72d5cb19dd0c77 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 17 Apr 2014 10:49:01 +0200 Subject: [PATCH] Added functionality to compare two ADDs up to a given precision. Added logical operator overloads to DD interface. Added tests for all new features. Former-commit-id: 738ad49d62089c5ebf6058abdb182f180d154be4 --- resources/3rdparty/cudd-2.5.0/src/cudd/cudd.h | 1 + .../3rdparty/cudd-2.5.0/src/cudd/cuddSat.c | 65 +++++++++++++++++++ .../3rdparty/cudd-2.5.0/src/obj/cuddObj.cc | 10 +++ .../3rdparty/cudd-2.5.0/src/obj/cuddObj.hh | 4 +- src/storage/dd/CuddDd.cpp | 20 +++++- src/storage/dd/CuddDd.h | 34 +++++++--- src/storage/dd/CuddDdManager.cpp | 4 +- test/functional/storage/CuddDdTest.cpp | 16 +++-- 8 files changed, 136 insertions(+), 18 deletions(-) diff --git a/resources/3rdparty/cudd-2.5.0/src/cudd/cudd.h b/resources/3rdparty/cudd-2.5.0/src/cudd/cudd.h index 5a2c2f952..51d509b35 100644 --- a/resources/3rdparty/cudd-2.5.0/src/cudd/cudd.h +++ b/resources/3rdparty/cudd-2.5.0/src/cudd/cudd.h @@ -964,6 +964,7 @@ extern DdNode * Cudd_Increasing (DdManager *dd, DdNode *f, int i); extern int Cudd_EquivDC (DdManager *dd, DdNode *F, DdNode *G, DdNode *D); extern int Cudd_bddLeqUnless (DdManager *dd, DdNode *f, DdNode *g, DdNode *D); extern int Cudd_EqualSupNorm (DdManager *dd, DdNode *f, DdNode *g, CUDD_VALUE_TYPE tolerance, int pr); +extern int Cudd_EqualSupNormRel (DdManager *dd, DdNode *f, DdNode *g, CUDD_VALUE_TYPE tolerance, int pr); extern DdNode * Cudd_bddMakePrime (DdManager *dd, DdNode *cube, DdNode *f); extern DdNode * Cudd_bddMaximallyExpand(DdManager *dd, DdNode *lb, DdNode *ub, DdNode *f); extern DdNode * Cudd_bddLargestPrimeUnate(DdManager *dd , DdNode *f, DdNode *phaseBdd); diff --git a/resources/3rdparty/cudd-2.5.0/src/cudd/cuddSat.c b/resources/3rdparty/cudd-2.5.0/src/cudd/cuddSat.c index 19dcafff0..869733f32 100644 --- a/resources/3rdparty/cudd-2.5.0/src/cudd/cuddSat.c +++ b/resources/3rdparty/cudd-2.5.0/src/cudd/cuddSat.c @@ -853,6 +853,71 @@ Cudd_EqualSupNorm( } /* end of Cudd_EqualSupNorm */ +/**Function******************************************************************** + + Synopsis [Compares two ADDs for equality within tolerance.] + + Description [Same as Cudd_EqualSupNorm but tests for max _relative_ difference + i.e. (f-g/f)0) { + (void) fprintf(dd->out,"Offending nodes:\n"); + (void) fprintf(dd->out, + "f: address = %p\t value = %40.30f\n", + (void *) f, cuddV(f)); + (void) fprintf(dd->out, + "g: address = %p\t value = %40.30f\n", + (void *) g, cuddV(g)); + } + return(0); + } + } + + /* We only insert the result in the cache if the comparison is + ** successful. Therefore, if we hit we return 1. */ + r = cuddCacheLookup2(dd,(DD_CTFP)Cudd_EqualSupNormRel,f,g); + if (r != NULL) { + return(1); + } + + /* Compute the cofactors and solve the recursive subproblems. */ + topf = cuddI(dd,f->index); + topg = cuddI(dd,g->index); + + if (topf <= topg) {fv = cuddT(f); fvn = cuddE(f);} else {fv = fvn = f;} + if (topg <= topf) {gv = cuddT(g); gvn = cuddE(g);} else {gv = gvn = g;} + + if (!Cudd_EqualSupNormRel(dd,fv,gv,tolerance,pr)) return(0); + if (!Cudd_EqualSupNormRel(dd,fvn,gvn,tolerance,pr)) return(0); + + cuddCacheInsert2(dd,(DD_CTFP)Cudd_EqualSupNormRel,f,g,DD_ONE(dd)); + + return(1); + +} /* end of Cudd_EqualSupNormRel */ /**Function******************************************************************** diff --git a/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.cc b/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.cc index c9fcf7b11..2753c0950 100644 --- a/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.cc +++ b/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.cc @@ -4747,6 +4747,16 @@ ADD::EqualSupNorm( } // ADD::EqualSupNorm +bool +ADD::EqualSupNormRel( + const ADD& g, + CUDD_VALUE_TYPE tolerance, + int pr) const +{ + DdManager *mgr = checkSameManager(g); + return Cudd_EqualSupNormRel(mgr, node, g.node, tolerance, pr) != 0; + +} // ADD::EqualSupNormRel BDD BDD::MakePrime( diff --git a/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.hh b/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.hh index a1a859490..795a7a2ee 100644 --- a/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.hh +++ b/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.hh @@ -426,8 +426,8 @@ public: ADD TimesPlus(const ADD& B, std::vector z) const; ADD Triangle(const ADD& g, std::vector z) const; ADD Eval(int * inputs) const; - bool EqualSupNorm(const ADD& g, CUDD_VALUE_TYPE tolerance, int pr) const; - + bool EqualSupNorm(const ADD& g, CUDD_VALUE_TYPE tolerance, int pr = 0) const; + bool EqualSupNormRel(const ADD& g, CUDD_VALUE_TYPE tolerance, int pr = 0) const; }; // ADD diff --git a/src/storage/dd/CuddDd.cpp b/src/storage/dd/CuddDd.cpp index ef204f790..c5fb92bbd 100644 --- a/src/storage/dd/CuddDd.cpp +++ b/src/storage/dd/CuddDd.cpp @@ -83,13 +83,21 @@ namespace storm { return *this; } - Dd Dd::operator~() const { + Dd Dd::operator!() const { Dd result(*this); result.complement(); return result; } + + Dd Dd::operator&&(Dd const& other) const { + std::set metaVariableNames(this->getContainedMetaVariableNames()); + metaVariableNames.insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end()); + + // Rewrite a and b to not((not a) or (not b)). + return Dd(this->getDdManager(), ~(~this->getCuddAdd()).Or(~other.getCuddAdd()), metaVariableNames); + } - Dd Dd::logicalOr(Dd const& other) const { + Dd Dd::operator||(Dd const& other) const { std::set metaVariableNames(this->getContainedMetaVariableNames()); metaVariableNames.insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end()); return Dd(this->getDdManager(), this->getCuddAdd().Or(other.getCuddAdd()), metaVariableNames); @@ -204,6 +212,14 @@ namespace storm { this->cuddAdd = this->cuddAdd.MaxAbstract(cubeDd.getCuddAdd()); } + bool Dd::equalModuloPrecision(Dd const& other, double precision, bool relative) const { + if (relative) { + return this->getCuddAdd().EqualSupNormRel(other.getCuddAdd(), precision); + } else { + return this->getCuddAdd().EqualSupNorm(other.getCuddAdd(), precision); + } + } + void Dd::swapVariables(std::vector> const& metaVariablePairs) { std::vector from; std::vector to; diff --git a/src/storage/dd/CuddDd.h b/src/storage/dd/CuddDd.h index 8ca99614a..1942f6504 100644 --- a/src/storage/dd/CuddDd.h +++ b/src/storage/dd/CuddDd.h @@ -48,6 +48,20 @@ namespace storm { */ bool operator!=(Dd const& other) const; + /*! + * Performs a logical or of the current and the given DD. + * + * @return The logical or of the operands. + */ + Dd operator||(Dd const& other) const; + + /*! + * Performs a logical and of the current and the given DD. + * + * @return The logical and of the operands. + */ + Dd operator&&(Dd const& other) const; + /*! * Adds the two DDs. * @@ -125,14 +139,7 @@ namespace storm { * * @return The logical complement of the current DD. */ - Dd operator~() const; - - /*! - * Performs a logical or of the current and the given DD. - * - * @return The logical or of the operands. - */ - Dd logicalOr(Dd const& other) const; + Dd operator!() const; /*! * Logically complements the current DD. The result will map all encodings with a value @@ -222,6 +229,17 @@ namespace storm { */ void maxAbstract(std::set const& metaVariableNames); + /*! + * Checks whether the current and the given DD represent the same function modulo some given precision. + * + * @param other The DD with which to compare. + * @param precision An upper bound on the maximal difference between any two function values that is to be + * tolerated. + * @param relative If set to true, not the absolute values have to be within the precision, but the relative + * values. + */ + bool equalModuloPrecision(Dd const& other, double precision, bool relative = true) const; + /*! * Swaps the given pairs of meta variables in the DD. The pairs of meta variables must be guaranteed to have * the same number of underlying DD variables. diff --git a/src/storage/dd/CuddDdManager.cpp b/src/storage/dd/CuddDdManager.cpp index cda474e7f..4352e52b7 100644 --- a/src/storage/dd/CuddDdManager.cpp +++ b/src/storage/dd/CuddDdManager.cpp @@ -45,14 +45,14 @@ namespace storm { if (value & (1ull << (ddVariables.size() - 1))) { result = ddVariables[0]; } else { - result = ~ddVariables[0]; + result = !ddVariables[0]; } for (std::size_t i = 1; i < ddVariables.size(); ++i) { if (value & (1ull << (ddVariables.size() - i - 1))) { result *= ddVariables[i]; } else { - result *= ~ddVariables[i]; + result *= !ddVariables[i]; } } diff --git a/test/functional/storage/CuddDdTest.cpp b/test/functional/storage/CuddDdTest.cpp index 01d40164a..c405006d8 100644 --- a/test/functional/storage/CuddDdTest.cpp +++ b/test/functional/storage/CuddDdTest.cpp @@ -130,9 +130,12 @@ TEST(CuddDd, OperatorTest) { dd3 += manager->getZero(); EXPECT_TRUE(dd3 == manager->getConstant(2)); + dd3 = dd1 && manager->getConstant(3); + EXPECT_TRUE(dd1 == manager->getOne()); + dd3 = dd1 * manager->getConstant(3); EXPECT_TRUE(dd3 == manager->getConstant(3)); - + dd3 *= manager->getConstant(2); EXPECT_TRUE(dd3 == manager->getConstant(6)); @@ -148,10 +151,10 @@ TEST(CuddDd, OperatorTest) { dd3.complement(); EXPECT_TRUE(dd3 == manager->getZero()); - dd1 = ~dd3; + dd1 = !dd3; EXPECT_TRUE(dd1 == manager->getOne()); - dd3 = dd1.logicalOr(dd2); + dd3 = dd1 || dd2; EXPECT_TRUE(dd3 == manager->getOne()); dd1 = manager->getIdentity("x"); @@ -161,7 +164,7 @@ TEST(CuddDd, OperatorTest) { EXPECT_EQ(1, dd3.getNonZeroCount()); storm::dd::Dd dd4 = dd1.notEquals(dd2); - EXPECT_TRUE(dd4 == ~dd3); + EXPECT_TRUE(dd4 == !dd3); dd3 = dd1.less(dd2); EXPECT_EQ(11, dd3.getNonZeroCount()); @@ -174,6 +177,11 @@ TEST(CuddDd, OperatorTest) { dd3 = dd1.greaterOrEqual(dd2); EXPECT_EQ(5, dd3.getNonZeroCount()); + + dd1 = manager->getConstant(0.01); + dd2 = manager->getConstant(0.01 + 1e-6); + EXPECT_TRUE(dd1.equalModuloPrecision(dd2, 1e-6, false)); + EXPECT_FALSE(dd1.equalModuloPrecision(dd2, 1e-6)); } TEST(CuddDd, AbstractionTest) {