CubeGenerator.hh

Go to the documentation of this file.

#ifndef CUBEGENERATOR_H_
#define CUBEGENERATOR_H_

#include <diades/utils/Assertion.hh>
#include <diades/sdmdl/Formula.hh>
using namespace std;


namespace Diades
{
  namespace Sdmdl
  {


        class CubeGenerator 
        {
        private:
          DdGen * gen;
          int * cube;
          CUDD_VALUE_TYPE value;
          const Formula & f;
        
        public:
          CubeGenerator(const Formula & f1):f(f1){
                require(Diades::Utils::Exception<Formula>,!f1.isNull(),"CubeGenerator: the formula is invalid");
                gen = Cudd_FirstCube(f.bddManager().getManager(),f.bdd().getNode(),&cube,&value);
          }
        
          ~CubeGenerator() { Cudd_GenFree(gen); }
        
          bool isEmpty() const { return Cudd_IsGenEmpty(gen); }
          int  cubeSize() const { return f.bddManager().ReadSize(); }
          int * currentCube() const {   return cube; }
        
          void nextCube() { Cudd_NextCube(gen, &cube, &value); }
        };

  };
};

//DdNode * 
//Cudd_CubeArrayToBdd(
//  DdManager * dd, 
//  int * array 
//)
//int 
//Cudd_BddToCubeArray(
//  DdManager * dd, 
//  DdNode * cube, 
//  int * array 
//)
//int 
//cuddCheckCube(
//  DdManager * dd, 
//  DdNode * g 
//)
#endif /*CUBEGENERATOR_H_*/