Fixed min/max Abstract w. repr.

Finally.


Former-commit-id: 1ccc06d924

resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c

@@ -213,7 +213,7 @@ TASK_IMPL_2(MTBDD, mtbdd_op_less, MTBDD*, pa, MTBDD*, pb)
 }
 
 /**
- * Binary operation Equals (for MTBDDs of same type)
+ * Binary operation Less or Equals (for MTBDDs of same type)
  * Only for MTBDDs where either all leaves are Boolean, or Integer, or Double.
  * For Integer/Double MTBDD, if either operand is mtbdd_false (not defined),
  * then the result is mtbdd_false (i.e. not defined).
@@ -261,6 +261,55 @@ TASK_IMPL_2(MTBDD, mtbdd_op_less_or_equal, MTBDD*, pa, MTBDD*, pb)
     return mtbdd_invalid;
 }
 
+/**
+ * Binary operation Greater or Equals (for MTBDDs of same type)
+ * Only for MTBDDs where either all leaves are Boolean, or Integer, or Double.
+ * For Integer/Double MTBDD, if either operand is mtbdd_false (not defined),
+ * then the result is mtbdd_false (i.e. not defined).
+ */
+TASK_IMPL_2(MTBDD, mtbdd_op_greater_or_equal, MTBDD*, pa, MTBDD*, pb)
+{
+    MTBDD a = *pa, b = *pb;
+    if (a == mtbdd_false && b == mtbdd_false) return mtbdd_true;
+    if (a == mtbdd_true && b == mtbdd_true) return mtbdd_true;
+    
+    mtbddnode_t na = MTBDD_GETNODE(a);
+    mtbddnode_t nb = MTBDD_GETNODE(b);
+    
+    if (mtbddnode_isleaf(na) && mtbddnode_isleaf(nb)) {
+        uint64_t val_a = mtbddnode_getvalue(na);
+        uint64_t val_b = mtbddnode_getvalue(nb);
+        if (mtbddnode_gettype(na) == 0 && mtbddnode_gettype(nb) == 0) {
+            int64_t va = *(int64_t*)(&val_a);
+            int64_t vb = *(int64_t*)(&val_b);
+            return va >= vb ? mtbdd_true : mtbdd_false;
+        } else if (mtbddnode_gettype(na) == 1 && mtbddnode_gettype(nb) == 1) {
+            // both double
+            double vval_a = *(double*)&val_a;
+            double vval_b = *(double*)&val_b;
+            if (vval_a >= vval_b) return mtbdd_true;
+            return mtbdd_false;
+        } else if (mtbddnode_gettype(na) == 2 && mtbddnode_gettype(nb) == 2) {
+            // both fraction
+            uint64_t nom_a = val_a>>32;
+            uint64_t nom_b = val_b>>32;
+            uint64_t denom_a = val_a&0xffffffff;
+            uint64_t denom_b = val_b&0xffffffff;
+            nom_a *= denom_b;
+            nom_b *= denom_a;
+            return nom_a >= nom_b ? mtbdd_true : mtbdd_false;
+        }
+#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL)
+		else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID && mtbddnode_gettype(nb) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) {
+			printf("ERROR mtbdd_op_greater_or_equal type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID");
+			assert(0);
+		}
+#endif
+    }
+    
+    return mtbdd_invalid;
+}
+
 /**
  * Binary operation Pow (for MTBDDs of same type)
  * Only for MTBDDs where either all leaves are Double.
@@ -629,54 +678,81 @@ TASK_IMPL_2(MTBDD, mtbdd_op_complement, MTBDD, a, size_t, k)
 }
 
 TASK_IMPL_3(BDD, mtbdd_minExistsRepresentative, MTBDD, a, BDD, variables, BDDVAR, prev_level) {
-	BDD zero = sylvan_false;
-    
 	/* Maybe perform garbage collection */
     sylvan_gc_test();
-	
-    /* Cube is guaranteed to be a cube at this point. */
-	printf("Entered method.\n");
+
+	if (sylvan_set_isempty(variables)) {
+		return sylvan_true;
+	}
+
+	/* Cube is guaranteed to be a cube at this point. */
     if (mtbdd_isleaf(a)) {
-		printf("is leaf\n");
-        if (sylvan_set_isempty(variables)) {
-			printf("set is empty\n");
-            return sylvan_true; // FIXME?
-        } else {
-			printf("have variables.\n");
-			BDD _v = sylvan_set_next(variables);
-			BDD res = CALL(mtbdd_minExistsRepresentative, a, _v, prev_level);
-			if (res == sylvan_invalid) {
-				return sylvan_invalid;
-			}
-			sylvan_ref(res);
-
-			BDD res1 = sylvan_ite(sylvan_ithvar(bddnode_getvariable(BDD_GETNODE(variables))), sylvan_false, res);
-			if (res1 == sylvan_invalid) {
-				sylvan_deref(res);
-				return sylvan_invalid;
-			}
+		BDD _v = sylvan_set_next(variables);
+		BDD res = CALL(mtbdd_minExistsRepresentative, a, _v, prev_level);
+		if (res == sylvan_invalid) {
+			return sylvan_invalid;
+		}
+		sylvan_ref(res);
+
+		BDD res1 = sylvan_not(sylvan_ite(sylvan_ithvar(bddnode_getvariable(BDD_GETNODE(variables))), sylvan_true, sylvan_not(res)));
+		if (res1 == sylvan_invalid) {
 			sylvan_deref(res);
-			return res1;
+			return sylvan_invalid;
+		}
+		sylvan_deref(res);
+		return res1;
+    }
+	
+	mtbddnode_t na = MTBDD_GETNODE(a);
+	uint32_t va = mtbddnode_getvariable(na);
+	bddnode_t nv = BDD_GETNODE(variables);
+	BDDVAR vv = bddnode_getvariable(nv);
+
+    /* Abstract a variable that does not appear in a. */
+    if (va > vv) {
+		BDD _v = sylvan_set_next(variables);
+        BDD res = CALL(mtbdd_minExistsRepresentative, a, _v, va);
+        if (res == sylvan_invalid) {
+            return sylvan_invalid;
         }
-    } else if (sylvan_set_isempty(variables)) {
-		mtbddnode_t na = MTBDD_GETNODE(a);
-		uint32_t va = mtbddnode_getvariable(na);
-		MTBDD E = mtbdd_getlow(a);
-		MTBDD T = mtbdd_gethigh(a);
-		BDD res1 = CALL(mtbdd_minExistsRepresentative, E, variables, va);
+        
+        // Fill in the missing variables to make representative unique.
+        sylvan_ref(res);
+        BDD res1 = sylvan_ite(sylvan_ithvar(vv), sylvan_false, res);
+        if (res1 == sylvan_invalid) {
+            sylvan_deref(res);
+            return sylvan_invalid;
+        }
+        sylvan_deref(res);
+       	return res1;
+    }
+    
+	/* TODO: Caching here. */
+    /*if ((res = cuddCacheLookup2(manager, Cudd_addMinAbstractRepresentative, f, cube)) != NULL) {
+        return(res);
+    }*/
+    
+    
+    MTBDD E = mtbdd_getlow(a);
+    MTBDD T = mtbdd_gethigh(a);
+    
+    /* If the two indices are the same, so are their levels. */
+    if (va == vv) {
+		BDD _v = sylvan_set_next(variables);
+        BDD res1 = CALL(mtbdd_minExistsRepresentative, E, _v, va);
         if (res1 == sylvan_invalid) {
             return