some minor updates

bdd/CuddMintermIterator.hh

@@ -92,13 +92,6 @@ class CuddMintermIterator {
       nminterm=bdd.CountMinterm(nvars);
       progress=1;
 
-
-      //std::cout << "Fresh cube ";
-      //for(size_t i=0; i<nvars_; i++)
-      //  std::cout << cube[ivars_[i]];
-      //std::cout<< std::endl;
-     
-
       /* check cube for don't cares */
       idontcares.reserve(nvars);
       ndontcares=0;
@@ -151,13 +144,6 @@ class CuddMintermIterator {
       /* determine the number of minterms */
       nminterm=bdd.CountMinterm(nvars_);
       progress=1.0;
-
-      //std::cout << "Fresh cube ";
-      //for(size_t i=0; i<nvars_; i++)
-      //  std::cout << cube[ivars_[i]];
-      //std::cout<< std::endl;
-     
-
       /* check cube for don't cares */
       idontcares.reserve(nvars_);
       ndontcares=0;

bdd/SymbolicSet.hh

@@ -418,12 +418,34 @@ public:
 
     return cube; 
   }  
-   /* function: setSymbolicSet 
+  /* function: setSymbolicSet 
    *
    * set the symbolic set to symset
    */
   inline void setSymbolicSet(const BDD symset) {
-    symbolicSet_=symset;
+    /*get variable ids not used in this set*/
+    std::vector<size_t> coIndBddVars;
+    for(size_t i=0; i< (size_t)ddmgr_->ReadSize(); i++) {
+      bool isinside=0;
+      for (size_t d=0; d<dim_; d++) 
+        for (size_t j=0; j<nofBddVars_[d]; j++) 
+          if(i==indBddVars_[d][j])
+            isinside=true;
+          
+      if(!isinside)
+        coIndBddVars.push_back(i);
+    } 
+    /* create cube to existentially abstract all bdd ids that are 
+     * not one of the indBddVar of this SymbolicSet
+     */
+    size_t t = coIndBddVars.size();
+    BDD* vars = new BDD[t];
+    for (size_t k=0;k<t; k++) 
+      vars[k]=ddmgr_->bddVar(coIndBddVars[k]);
+    BDD cube = ddmgr_->bddComputeCube(vars,NULL,t);
+    delete[] vars;
+
+    symbolicSet_ = symset.ExistAbstract(cube);
   }
   /* function:  getnofbddvars 
    *

readme.txt

@@ -47,8 +47,7 @@ Directory structure
 - ./mfiles/mexfiles/
   mex-file to read the C++ output from file 
 
-- ./sparse 
-  Contains the source C++ source code for the SCOTS classes 
-  which use sparse matrices as underlying data structure
- 
+- ./sparse
+  See https://gitlab.lrz.de/matthias/SCOTSv0.2 for the sparse matrix
+  implementation