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: 738ad49d62

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);

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)<e instead of (f-g)<e ]
+ 
+ SideEffects [None]
+ 
+ SeeAlso     []
+ 
+ ******************************************************************************/
+int
+Cudd_EqualSupNormRel(
+                     DdManager * dd /* manager */,
+                     DdNode * f /* first ADD */,
+                     DdNode * g /* second ADD */,
+                     CUDD_VALUE_TYPE  tolerance /* maximum allowed difference */,
+                     int  pr /* verbosity level */)
+{
+    DdNode *fv, *fvn, *gv, *gvn, *r;
+    unsigned int topf, topg;
+    
+    statLine(dd);
+    /* Check terminal cases. */
+    if (f == g) return(1);
+    if (Cudd_IsConstant(f) && Cudd_IsConstant(g)) {
+        if (ddAbs((cuddV(f) - cuddV(g))/cuddV(f)) < tolerance) {
+            return(1);
+        } else {
+            if (pr>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********************************************************************
 

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(

resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.hh

@@ -426,8 +426,8 @@ public:
     ADD TimesPlus(const ADD& B, std::vector<ADD> z) const;
     ADD Triangle(const ADD& g, std::vector<ADD> 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
 
 

src/storage/dd/CuddDd.cpp

@@ -83,13 +83,21 @@ namespace storm {
             return *this;
         }
         
-        Dd<DdType::CUDD> Dd<DdType::CUDD>::operator~() const {
+        Dd<DdType::CUDD> Dd<DdType::CUDD>::operator!() const {
             Dd<DdType::CUDD> result(*this);
             result.complement();
             return result;
         }
+
+        Dd<DdType::CUDD> Dd<DdType::CUDD>::operator&&(Dd<DdType::CUDD> const& other) const {
+            std::set<std::string> metaVariableNames(this->getContainedMetaVariableNames());
+            metaVariableNames.insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end());
+            
+            // Rewrite a and b to not((not a) or (not b)). 
+            return Dd<DdType::CUDD>(this->getDdManager(), ~(~this->getCuddAdd()).Or(~other.getCuddAdd()), metaVariableNames);
+        }
         
-        Dd<DdType::CUDD> Dd<DdType::CUDD>::logicalOr(Dd<DdType::CUDD> const& other) const {
+        Dd<DdType::CUDD> Dd<DdType::CUDD>::operator||(Dd<DdType::CUDD> const& other) const {
             std::set<std::string> metaVariableNames(this->getContainedMetaVariableNames());
             metaVariableNames.insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end());
             return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().Or(other.getCuddAdd()), metaVariableNames);
@@ -204,6 +212,14 @@ namespace storm {
             this->cuddAdd = this->cuddAdd.MaxAbstract(cubeDd.getCuddAdd());
         }
         
+        bool Dd<DdType::CUDD>::equalModuloPrecision(Dd<DdType::CUDD> 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<DdType::CUDD>::swapVariables(std::vector<std::pair<std::string, std::string>> const& metaVariablePairs) {
             std::vector<ADD> from;
             std::vector<ADD> to;

src/storage/dd/CuddDd.h

@@ -48,6 +48,20 @@ namespace storm {
              */
             bool operator!=(Dd<DdType::CUDD> const& other) const;
             
+            /*!
+             * Performs a logical or of the current and the given DD.
+             *
+             * @return The logical or of the operands.
+             */
+            Dd<DdType::CUDD> operator||(Dd<DdType::CUDD> const& other) const;
+            
+            /*!
+             * Performs a logical and of the current and the given DD.
+             *
+             * @return The logical and of the operands.
+             */
+            Dd<DdType::CUDD> operator&&(Dd<DdType::CUDD> const& other) const;
+            
             /*!
              * Adds the two DDs.
              *
@@ -125,14 +139,7 @@ namespace storm {
              *
              * @return The logical complement of the current DD.
              */
-            Dd<DdType::CUDD> operator~() const;
-
-            /*!
-             * Performs a logical or of the current and the given DD.
-             *
-             * @return The logical or of the operands.
-             */
-            Dd<DdType::CUDD> logicalOr(Dd<DdType::CUDD> const& other) const;
+            Dd<DdType::CUDD> 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<std::string> 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<DdType::CUDD> 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.

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];
                 }
             }
                         

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<storm::dd::DdType::CUDD> 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) {