AI-PBDD

 view release on metacpan or  search on metacpan

Changes  view on Meta::CPAN

Revision history for Perl extension PBDD.

0.01  Wed Oct  5 17:14:59 2011
	- original version; created by h2xs 1.23 with options
		-AX PBDD

META.json  view on Meta::CPAN

{
   "abstract" : "unknown",
   "author" : [
      "Gianluca Torta <torta@di.unito.it>"
   ],
   "dynamic_config" : 1,
   "generated_by" : "ExtUtils::MakeMaker version 6.59, CPAN::Meta::Converter version 2.112150",
   "license" : [
      "unknown"
   ],
   "meta-spec" : {
      "url" : "http://search.cpan.org/perldoc?CPAN::Meta::Spec",
      "version" : "2"
   },
   "name" : "AI-PBDD",
   "no_index" : {
      "directory" : [
         "t",
         "inc"
      ]
   },
   "prereqs" : {
      "build" : {
         "requires" : {
            "ExtUtils::MakeMaker" : 0
         }
      },
      "configure" : {
         "requires" : {
            "ExtUtils::MakeMaker" : 0
         }
      },
      "runtime" : {
         "requires" : {}
      }
   },
   "release_status" : "stable",
   "version" : "0.01"
}

META.yml  view on Meta::CPAN

---
abstract: unknown
author:
  - 'Gianluca Torta <torta@di.unito.it>'
build_requires:
  ExtUtils::MakeMaker: 0
configure_requires:
  ExtUtils::MakeMaker: 0
dynamic_config: 1
generated_by: 'ExtUtils::MakeMaker version 6.59, CPAN::Meta::Converter version 2.112150'
license: unknown
meta-spec:
  url: http://module-build.sourceforge.net/META-spec-v1.4.html
  version: 1.4
name: AI-PBDD
no_index:
  directory:
    - t
    - inc
requires: {}
version: 0.01

Makefile.PL  view on Meta::CPAN

use ExtUtils::MakeMaker;

WriteMakefile(
    NAME => 'AI::PBDD',
    VERSION_FROM => 'lib/AI/PBDD.pm',
    C => ['XS.c'],
    OBJECT => 'XS.o',
    INC => "-I$ENV{BUDDYPATH}/include/ -I$ENV{BUDDYPATH}/src/",
    LIBS => "-L$ENV{BUDDYPATH}/lib -lbdd -lm",
    LDDLFLAGS => "-fPIC -shared",
    LD => 'g++',
    ($] >= 5.005 ?
      (ABSTRACT_FROM  => 'lib/AI/PBDD.pm',
       AUTHOR         => 'Gianluca Torta <torta@di.unito.it>') : ()),
);

README  view on Meta::CPAN

PBDD version 0.01
=================

This module provides a Perl interface to the BuDDy 2.4 library for Binary Decision Diagrams. The interface is as close as possible to JBDD, a Java interface to the BuDDy and CUDD packages written by Arash Vahidi.

DEPENDENCIES

Before building the PBDD module, you must:
1) download the buddy-2.4 library from:
      http://sourceforge.net/projects/buddy/
2) build and install buddy-2.4 as follows:
      export CFLAGS='-fPIC -O2'
      export CXXFLAGS='-fPIC -O2'
      ./configure --prefix=/my/buddy/home --disable-shared
      make
      make install
   NOTE: /my/buddy/home stands for the directory where you unzipped buddy-2.4

INSTALLATION

First of all set the environment variable BUDDYPATH to the directory where you unzipped buddy-2.4, e.g.:
   export BUDDYPATH=/my/buddy/home

Then type the following:

   perl Makefile.PL
   make
   make test
   make install


COPYRIGHT AND LICENCE

Copyright (C) 2011 by Gianluca Torta

This library is free software; you can redistribute it and/or modify
it under the same terms as Perl itself, either Perl version 5.12.3 or,
at your option, any later version of Perl 5 you may have available.

XS.xs  view on Meta::CPAN

#include "EXTERN.h"
#include "perl.h"
#include "XSUB.h"


#include "common.h"

void dumpBDD_info(int bdd)
{
  BddNode *node;

  node = &bddnodes[bdd];
  fprintf (stderr,
	   "BDD %d:	RefCount %d, Level %-3d, IF %-3d, ELSE %-3d, HASH %d\n",
	   bdd, node->refcou, node->level, node->high, node->low, node->hash);
	fflush(stderr);
}

long createPair(int *old, int *new_, int size) {
  bddPair *pair = bdd_newpair ();

  int i;
  int len = size;
  int *old_vars = (int *)old;
  int *new_vars = (int *)new_;

  for (i = 0; i < len; i++)
    {
      /*
       * XXX - not bdd_var() call for new_vars[i] ??
       */

      bdd_setbddpair (pair, bdd_var(old_vars[i]), new_vars[i]);
    }
    
  return (long)pair;
}

int makeSet(int *vars, int size, int offset)
{
  BDD tmp, ret = 1;
  int i;
  int *body = (int *)vars;

  // DONT USE ´ret = bdd_makeset(body + offset, size);´ (it uses index
  // not variables)

  bdd_addref (ret);
  for (i = size - 1; i >= 0; i--)
    {

      CHECK_BDD (body[offset + i]);

      tmp = bdd_apply (ret, body[offset + i], bddop_and);
      bdd_addref (tmp);
      bdd_delref (ret);
      ret = tmp;
    }

  return ret;
}

int checkBuddy() {
  int i;

  if (!checkBDD (0))
    {
      fprintf (stderr, "bdd FALSE failed sanity check\n");
      dumpBDD_info (0);
      return 0;
    }

  if (!checkBDD (1))
    {
      fprintf (stderr, "bdd TRUE failed sanity check\n");
      dumpBDD_info (1);
      return 0;
    }

  for (i = bddvarnum; i < bddvarnum; i++)
    {
      if (!checkBDD (2 * i + 2))
	{
	  dumpBDD_info (2 * i + 2);
	  printf ("bdd variable #%d failed sanity check\n", i);
	  return 0;
	}

      if (!checkBDD (2 * i + 3))
	{
	  printf ("shadow of bdd variable #%d failed sanity check\n", i);
	  dumpBDD_info (2 * i + 3);
	  return 0;
	}
    }

    return 1;
}

int checkBDD(int bdd)
{
  if (!bddrunning)
    {
      bdd_error (BDD_RUNNING);
      return 0;
    }
  if (bdd < 0 || (bdd) >= bddnodesize)
    {
      bdd_error (BDD_ILLBDD);
      return 0;
    }
  if (bdd >= 2 && LOW (bdd) == -1)
    {
      bdd_error (BDD_ILLBDD);
      return 0;
    }

  if (bddnodes[bdd].refcou == 0)
    {
      fprintf (stderr, "ERROR: refcount is zero\n");
      return 0;
    }
  // refcount for TRUE and FALSE is saturated by default, ignore them!
  if (bdd > 2 && bddnodes[bdd].refcou == MAXREF)
    {
      fprintf (stderr, "ERROR: refcount is saturated\n");
      return 0;
    }

  return 1;
}

void printSet_rec(char *txt, int level, int bdd)
 {

  if (bdd == 0)
    {
      /*
       * do nothing
       */
      return;
    }
  else if (bdd == 1)
    {
      printf ("%s	1\n", txt);
      return;
    }
  else
    {
      BDD low = LOW (bdd);
      BDD high = HIGH (bdd);
      int l;
      char save;


      // printf("BDD=%d/%d, LOW=%d, HIGH=%d\n", bdd,
      // bddlevel2var[LEVEL(bdd)], low, high);
      l = bdd < varcount * 2 ? bdd / 2 - 1 : bddlevel2var[LEVEL (bdd)];

      save = txt[l];
      txt[l] = '0';
      // printf("*L_low=%d\n", l);
      printSet_rec (txt, level + 1, low);
      txt[l] = save;


      save = txt[l];
      txt[l] = '1';
      // printf("*L_high=%d (%d)\n", l, varcount);
      printSet_rec (txt, level + 1, high);
      txt[l] = save;
    }
}

// XXX: we havent considred reordered variables yet!
// stuff like var2level() may be needed in some places when dynamic
// reordering is active!


// --- [ dynamic reordering ]
// --------------------------------------------------
#define MAX_REORDERING_METHODS		5
int reordering_method_table[MAX_REORDERING_METHODS] = {
  BDD_REORDER_NONE,		// JBDD_REORDER_NONE
  BDD_REORDER_WIN2,		// JBDD_REORDER_WIN2
  BDD_REORDER_WIN3,		// JBDD_REORDER_WIN3
  BDD_REORDER_SIFT,		// JBDD_REORDER_SIFT
  BDD_REORDER_RANDOM		// JBDD_REORDER_RANDOM
};


// -----------------------------------------------------------------------------------

static int current_reordering_method = BDD_REORDER_NONE;

MODULE = AI::PBDD		PACKAGE = AI::PBDD

PROTOTYPES: DISABLE

void 
reorder_setMethod(method)
   int method
PPCODE:
{
  if (method >= 0 && method < MAX_REORDERING_METHODS)
    current_reordering_method = reordering_method_table[method];
}

void reorder_now()
PPCODE:
{
  bdd_reorder (current_reordering_method);
}

void reorder_createVariableGroup(first, last, fix)
   int first
   int last
   int fix
PPCODE:
{
  bdd_intaddvarblock (first, last,
		      fix ? BDD_REORDER_FIXED : BDD_REORDER_FREE);
}

int internal_index(bdd) 
   int bdd
CODE:
{
  CHECK_BDD (bdd);

  RETVAL = (bdd < varcount * 2) ? (bdd / 2 - 1) : bddlevel2var[LEVEL (bdd)];
}
OUTPUT:
RETVAL

void printSet(bdd)
   int bdd;
PPCODE:
{

  char *txt;
  int i;


  CHECK_BDD (bdd);


  if (bdd < 2)
    {
      printf ("\n%s\n", bdd == 0 ? "False" : "True");
      return;
    }

  txt = (char *) malloc (bddvarnum + 2);
  if (!txt)
    {
      bdd_error (BDD_MEMORY);
      return;
    }

  for (i = 0; i < varcount; i++)
    txt[i] = '-';
  txt[i] = '\0';

  printf ("\n");
  printSet_rec (txt, 0, bdd);

  free (txt);
  fflush(stdout);
}

void init(varnum_, node_count)
   int varnum_
   int node_count
PPCODE:
{
  int ok;
  long nodenum, cachesize;

  if (node_count < MIN_NODES)
    node_count = MIN_NODES;
  else if (node_count > MAX_NODES)
    {
      fprintf (stderr,
	       "[JBDD:init()] Number of nodes should be between %d and %d	nodes\n",
	       MIN_NODES, MAX_NODES);
      exit (20);
    }

  nodenum = node_count;
  cachesize = nodenum / 8;	// WAS: 10


  if (has_bdd)
    {
      fprintf (stderr,
	       "A BDD package exist while you are trying to create another one\n"
	       "The BDD package is SINGLETON!\n");

      exit (20);
    }

  ok = bdd_init (nodenum, cachesize);
  if (ok == 0)
    {
      varnum = varnum_;
      varcount = 0;

      bdd_setmaxincrease (MAX_NODE_INCREASE);
      bdd_setvarnum (2 + 2 * varnum);
      has_bdd = 1;


       if (bdd_false () != 0 || bdd_true () != 1)
	{
	  fprintf (stderr, " INTERNAL ERROR : false = %d, true = %d\n",
		   bdd_false (), bdd_true ());
	  exit (20);
	}

    }
  else
    {
      fprintf (stderr, "bdd_init(%ld,%ld) Failed\n (error code %d)\n",
	       nodenum, cachesize, ok);
      exit (20);
    }
}

void kill ()
PPCODE:
{
  if (has_bdd)
    {
      bdd_done ();
      has_bdd = 0;
    }
  else
    fprintf (stderr, "Killing already dead BDD class :(\n");
}


int getOne()
CODE:
{
  BDD ret = bdd_true ();

  CHECK_BDD (ret);

  RETVAL = ret;
}
OUTPUT:
RETVAL

int getZero()
CODE:
{
  BDD ret = bdd_false ();

  CHECK_BDD (ret);

  RETVAL=ret;
}
OUTPUT:
RETVAL


int createBDD()
CODE:
{
  BDD ret;

  if (varcount >= varnum)
    {
      fprintf (stderr, "Maximum var count (%d) reached!!\n", varnum);
      exit (20);
    }

  ret = bdd_ithvar (varcount++);
  // bddnodes[ret].refcou = 1;	// why does BuDDy sets the initial
  // refcount to MAXREF (0x3FF) ?

  RETVAL=ret;
}
OUTPUT:
RETVAL

int getVarCount()
CODE:
{
  RETVAL = varcount;
}
OUTPUT:
RETVAL

int getBDD(index)
   int index
CODE:
{
  if (index < 0 || index >= varcount)
    {
      fprintf (stderr, "[JBUDDY.getBDD] requested bad BDD: %d\n", index);
      RETVAL=bdd_false();
    }
  RETVAL=bdd_ithvar (index);
}
OUTPUT:
RETVAL

int ref(bdd)
   int bdd
CODE:
{
  bdd_addref (bdd);
  RETVAL=bdd;
}
OUTPUT:
RETVAL

void localDeref(bdd)
   int bdd
CODE:
{
  CHECK_BDD (bdd);

  bdd_delref (bdd);
}

void deref(bdd)
   int bdd
CODE:
{

  CHECK_BDD (bdd);

  // ok, there is no recursive deref in BuDDy, as it is in CUDD.
  // I don't know how to fix this. I don't even know if this is needed
  // at all :)
  bdd_delref (bdd);
}

int and(l, r)
   int l
   int r
CODE:
{
  int bdd;

  CHECK_BDD (l);
  CHECK_BDD (r);

  bdd = bdd_apply (l, r, bddop_and);
  bdd_addref (bdd);
  RETVAL=bdd;
}
OUTPUT:
RETVAL

int or(l, r)
   int l
   int r
CODE:
{
  int bdd;

  CHECK_BDD (l);
  CHECK_BDD (r);

  bdd = bdd_apply (l, r, bddop_or);
  bdd_addref (bdd);
  RETVAL=bdd;
}
OUTPUT:
RETVAL

int andTo(l, r)
   int l
   int r
CODE:
{
  BDD ret;

  CHECK_BDD (l);
  CHECK_BDD (r);

  ret = bdd_apply (l, r, bddop_and);
  bdd_addref (ret);
  bdd_delref (l);
  RETVAL=ret;
}
OUTPUT:
RETVAL

int orTo(l, r)
   int l
   int r
CODE:
{
  BDD ret;

  CHECK_BDD (r);
  CHECK_BDD (l);

  ret = bdd_apply (l, r, bddop_or);
  bdd_addref (ret);
  bdd_delref (l);
  RETVAL=ret;
}
OUTPUT:
RETVAL

int nand(l, r)
   int l
   int r
CODE:
{
  BDD bdd;

  CHECK_BDD (l);
  CHECK_BDD (r);

  bdd = bdd_apply (l, r, bddop_nand);
  bdd_addref (bdd);
  RETVAL=bdd;
}
OUTPUT:
RETVAL

int nor(l, r)
   int l
   int r
CODE:
{
  BDD bdd;

  CHECK_BDD (l);
  CHECK_BDD (r);


  bdd = bdd_apply (l, r, bddop_nor);
  bdd_addref (bdd);
  RETVAL=bdd;
}
OUTPUT:
RETVAL

int xor(l, r)
   int l
   int r
CODE:
{
  BDD bdd;

  CHECK_BDD (l);
  CHECK_BDD (r);

  bdd = bdd_apply (l, r, bddop_xor);
  bdd_addref (bdd);
  RETVAL=bdd;
}
OUTPUT:
RETVAL

int ite(if_, then_, else_)
   int if_
   int then_
   int else_
CODE:
{

  BDD bdd;

  CHECK_BDD (if_);
  CHECK_BDD (then_);
  CHECK_BDD (else_);

  bdd = bdd_ite (if_, then_, else_);
  bdd_addref (bdd);
  RETVAL=bdd;
}
OUTPUT:
RETVAL

int imp(l, r)
   int l
   int r
CODE:
{
  BDD bdd;

  CHECK_BDD (l);
  CHECK_BDD (r);

  bdd = bdd_apply (l, r, bddop_imp);
  bdd_addref (bdd);
  RETVAL=bdd;
}
OUTPUT:
RETVAL

int biimp(l, r)
   int l
   int r
CODE:
{
  BDD bdd;

  CHECK_BDD (l);
  CHECK_BDD (r);

  bdd = bdd_apply (l, r, bddop_biimp);
  bdd_addref (bdd);
  RETVAL=bdd;
}
OUTPUT:
RETVAL

int not(bdd)
   int bdd
CODE:
{
  BDD tmp;

  CHECK_BDD (bdd);

  tmp = bdd_not (bdd);
  bdd_addref (tmp);
  RETVAL = tmp;
}
OUTPUT:
RETVAL

int exists(bdd, cube)
   int bdd
   int cube
CODE:
{
  BDD tmp;

  CHECK_BDD (bdd);
  CHECK_BDD (cube);

  tmp = bdd_exist (bdd, cube);
  bdd_addref (tmp);
  RETVAL=tmp;
}
OUTPUT:
RETVAL

int forall(bdd, cube)
   int bdd
   int cube
CODE:
{
  BDD tmp;

  CHECK_BDD (bdd);
  CHECK_BDD (cube);

  tmp = bdd_forall (bdd, cube);
  bdd_addref (tmp);
  RETVAL=tmp;
}
OUTPUT:
RETVAL

int relProd(l, r, cube)
   int l
   int r
   int cube
CODE:
{

  BDD bdd;

  CHECK_BDD (l);
  CHECK_BDD (r);

  bdd = bdd_appex (l, r, bddop_and, cube);
  bdd_addref (bdd);
  RETVAL=bdd;
}
OUTPUT:
RETVAL

int restrict(r, var)
   int r
   int var
CODE:
{
  BDD bdd;

  CHECK_BDD (r);
  CHECK_BDD (var);

  bdd = bdd_restrict (r, var);
  bdd_addref (bdd);
  RETVAL=bdd;
}
OUTPUT:
RETVAL

int constrain(f, c)
   int f
   int c
CODE:
{
  BDD bdd;

  CHECK_BDD (f);
  CHECK_BDD (c);

  bdd = bdd_constrain (f, c);
  bdd_addref (bdd);
  RETVAL=bdd;
}
OUTPUT:
RETVAL

long createPairI(old, new_,size)
   AV *old
   AV *new_
   int size
CODE:
{
  int *oldarr = malloc(size*sizeof(int));
  int *newarr = malloc(size*sizeof(int));
  int i;
  long pair;

  for (i=0; i<size; i++) {
    SV** elem = av_fetch(old, i, 0);
    oldarr[i] = SvNV(*elem);
  }

  for (i=0; i<size; i++) {
    SV** elem = av_fetch(new_, i, 0);
    newarr[i] = SvNV(*elem);
  }

  pair = createPair(oldarr, newarr, size);

  free(newarr);
  free(oldarr);

  RETVAL=pair;
}
OUTPUT:
RETVAL

void deletePair(pair)
    long pair
PPCODE:
{

  bdd_freepair ((bddPair *) pair);
}

int replace(bdd, pair)
   int bdd
   long pair
CODE:
{
  BDD tmp;

  CHECK_BDD (bdd);

  tmp = bdd_replace (bdd, (bddPair *) pair);
  bdd_addref (tmp);
  RETVAL=tmp;
}
OUTPUT:
RETVAL

void showPair(pair)
   int pair
PPCODE:
{
  printf ("(function not supported, yet)\n");
}

int support(bdd)
   int bdd
CODE:
{
  BDD tmp;

  CHECK_BDD (bdd);

  tmp = bdd_support (bdd);
  bdd_addref (tmp);
  RETVAL=tmp;
}
OUTPUT:
RETVAL

int nodeCount(bdd)
   int bdd
CODE:
{
  CHECK_BDD (bdd);

  RETVAL=bdd_nodecount (bdd);
}
OUTPUT:
RETVAL

int satOne(bdd)
   int bdd
CODE:
{
  BDD tmp;
  CHECK_BDD (bdd);

  tmp = bdd_satone (bdd);
  bdd_addref (tmp);
  RETVAL=tmp;
}
OUTPUT:
RETVAL

double satCount__I(bdd)
   int bdd
CODE:
 {
  double div, sat;

  CHECK_BDD (bdd);

  // See init for a explaination about 2 + varnum...
  div = pow (2, 2 + varnum);

  sat = bdd_satcount (bdd);
  // fprintf(stderr, "sat = %lf, div = %lf or 2^%ld\n", sat, div, ( 2 +
  // varnum));

  sat /= div;

  RETVAL=sat;
}
OUTPUT:
RETVAL

double satCount__II(bdd, vars_ignored)
   int bdd
   int vars_ignored
CODE:    
{

  CHECK_BDD (bdd);

  // see init ...
//
//  RETVAL=(double) bdd_satcount (bdd) / pow (2,
//				     2 + varnum + 2 * vars_ignored);
//

  RETVAL=(double) bdd_satcount (bdd) / pow(2, 2 + varnum + vars_ignored);
}
OUTPUT:
RETVAL

void gc()
PPCODE:
{
  bdd_gbc ();
}

void printDot__I(bdd)
   int bdd
PPCODE:
{

  CHECK_BDD (bdd);

  bdd_printdot (bdd);
  printf ("\n");
}

void printDot__II(bdd, filename)
   int bdd
   char *filename
PPCODE:
{
  CHECK_BDD (bdd);
  bdd_fnprintdot (filename, bdd);
}

void print(bdd)
   int bdd
PPCODE:
{

  CHECK_BDD (bdd);

  bdd_printtable (bdd);
  printf ("\n");
  fflush (stdout);
}

void printStats()
PPCODE:
{
  bdd_printstat ();
}

int checkPackage()
CODE:
{
  RETVAL=(checkBuddy () ? 1 : 0);
}
OUTPUT:
RETVAL

void debugPackage()
PPCODE:
{
  IGNORE_CALL;
}

int internal_refcount(bdd)
   int bdd
CODE:
{

  CHECK_BDD (bdd);

  RETVAL=(bddnodes[bdd].refcou);
}
OUTPUT:	
RETVAL

int internal_isconst(bdd)
   int bdd
CODE:
{

  CHECK_BDD (bdd);

  RETVAL=(bdd == bddfalse) || (bdd == bddtrue);
}
OUTPUT:
RETVAL

int internal_constvalue(bdd)
   int bdd
CODE:
{

  CHECK_BDD (bdd);

  if (bdd == bddfalse)
    RETVAL=0;
  else
    RETVAL=1;
}
OUTPUT:
RETVAL

int internal_iscomplemented(bdd)
   int bdd
CODE:
{
  CHECK_BDD (bdd);

  RETVAL=0;	// no CE in BuDDy
}
OUTPUT:
RETVAL

int internal_then(bdd)
   int bdd
CODE:
{
  CHECK_BDD (bdd);

  RETVAL=bdd_high (bdd);
}
OUTPUT:
RETVAL

int internal_else(bdd)
   int bdd
CODE:
{
  CHECK_BDD (bdd);

  RETVAL=bdd_low (bdd);
}
OUTPUT:
RETVAL

void verbose(verb_)
   int verb_
PPCODE:
{
	// NOT IMPLEMENTED!
}

int makeSetI(vars, size)
   AV *vars
   int size
CODE:
{
  int *varsarr = malloc((av_len(vars)+1)*sizeof(int));
  int i;

  for (i=0; i<=av_len(vars); i++) {
    SV** elem = av_fetch(vars, i, 0);
    varsarr[i] = SvNV(*elem);
  }

  RETVAL = makeSet(varsarr, size, 0);
}
OUTPUT:
RETVAL

int makeSetII(vars, size, offset)
   AV *vars
   int size
   int offset
CODE:
{
  int *varsarr = malloc(av_len(vars)*sizeof(int));
  int i;

  for (i=0; i<=av_len(vars); i++) {
    SV** elem = av_fetch(vars, i, 0);
    varsarr[i] = SvNV(*elem);
  }

  RETVAL = makeSet(varsarr, size, offset);
}
OUTPUT:
RETVAL

int debugBDD(bdd)
   int bdd
CODE:
{

  CHECK_BDD (bdd);

  dumpBDD_info (bdd);
  RETVAL=(checkBDD (bdd) ? 1 : 0);
}
OUTPUT:
RETVAL

void reorder_enableDynamic(enable)
   int enable
PPCODE:
{
  if (enable)
    bdd_enable_reorder ();
  else
    bdd_disable_reorder ();
}

common.h  view on Meta::CPAN


/**
 * this file contains the code common for SBL and buddy
 */

// XXX: we havent considred reordered variables yet!
// stuff like var2level() may be needed in some places when dynamic
// reordering is active!

//#include <jni.h>

#include <stdio.h>
#include <stdlib.h>
#include <math.h>

common.h  view on Meta::CPAN

//#include "jbdd.h"

// best to use C++ keywords (?)
enum e_bool { false = 0, true = 1 };
//#define bool int


// see if the __func__ macro is available??
static void dummy_function() {
#ifndef __func__
 #define __func__ "?"
#endif
}

#define IGNORE_CALL fprintf(stderr,"(this function (%s, %s/%d) is not implemented)\n",  __func__, __FILE__, __LINE__)


// ----------------------------------------------------------------------
static int has_bdd = 0;

static int varnum = 0;		// max vars

lib/AI/PBDD.pm  view on Meta::CPAN

use constant BDD_REORDER_NONE => 0;
use constant BDD_REORDER_WIN2 => 1;
use constant BDD_REORDER_WIN3 => 2;
use constant BDD_REORDER_SIFT => 3;
use constant BDD_REORDER_RANDOM => 4;


@ISA = qw(Exporter DynaLoader);

@EXPORT = qw(
	      BDD_REORDER_NONE
	      BDD_REORDER_WIN2
	      BDD_REORDER_WIN3
	      BDD_REORDER_SIFT
	      BDD_REORDER_RANDOM
);

@EXPORT_OK = qw(
// setup and cleanup
		 init
		 gc
		 verbose
		 kill
// simple BDD operations
		 getOne
		 getZero
		 createBDD
		 getVarCount
		 getBDD
// ref counting
		 ref
		 deref
		 localDeref
// BDD operations
		 and
		 or
		 andTo
		 orTo
		 nand
		 nor
		 xor
		 ite
		 imp
		 biimp
		 not
                 makeSet
		 exists
		 forall
		 relProd
		 restrict
		 constrain
// variables replacement
		 createPair
		 deletePair
		 replace
		 showPair
// BDD analysis
		 support
		 nodeCount
		 satOne
		 satCount
// printing
		 printDot
		 printSet
		 print
// debugging
		 printStats                 
		 checkPackage
		 debugPackage
		 debugBDD
// low-level access
		 internal_index
		 internal_refcount
		 internal_isconst
		 internal_constvalue
		 internal_iscomplemented
		 internal_then
		 internal_else
// dynamic variable ordering
		 reorder_setMethod
		 reorder_now
		 reorder_enableDynamic
		 reorder_createVariableGroup
);

$VERSION = '0.01';

bootstrap AI::PBDD $VERSION;

sub satCount {
  my ($bdd, $vars_ignored) = @_;

  if (!defined($vars_ignored)) {
    return satCount__I($bdd);
  } else {
    return satCount__II($bdd, $vars_ignored);
  }
}

sub printDot {
  my ($bdd, $filename) = @_;

  if (!defined($filename)) {
      printDot__I($bdd);
  } else {
      printDot__II($bdd, $filename);
  }
}

sub makeSet {
  my ($vars, $size, $offset) = @_;

  if (!defined($offset)) {
      return makeSetI($vars, $size);
  } else {
      return makeSetII($vars, $size, $offset);
  }
}

sub createPair {
  my ($old, $new) = @_;
  my $size = @$old;

  return createPairI($old, $new, $size);
}

1;

__END__

=head1 AI::PBDD

Perl wrapper for the BuDDy C library

=head1 SYNOPSIS

  use AI::PBDD qw(init createBDD and printDot kill);

  init(100, 100000);

  my $var1 = createBDD();
  my $var2 = createBDD();

  my $bdd = and($var1, $var2);

  printDot($bdd);

  kill();

=head1 DESCRIPTION

Binary Decision Diagrams (BDDs) are used for efficient computation of many common problems. This is done by giving a compact representation and a set of efficient operations on boolean functions f: {0,1}^n --> {0,1}.

It turns out that this representation is good enough to solve a huge amount of problems in Artificial Intelligence and other areas of computing such as hardware verification.

This is a Perl interface to the popular BDD package BuDDy. The interface is largely inspired by JBDD, a Java common interface for the two BDD packages BuDDy and CUDD written by Arash Vahidi, which can be found at L<http://javaddlib.sourceforge.net/jb...

PBDD allows you to combine the power of Perl with an efficient BDD package written in highly optimized C.

lib/AI/PBDD.pm  view on Meta::CPAN


=back

=head1 SEE ALSO

BDDs and their operations are described in many academic papers that can be found on the Internet. A good place to get started with BDDs is the wikipedia article L<http://en.wikipedia.org/wiki/Binary_decision_diagram>.

It can also be useful to look at the test code for this package in the C<t> directory, as well as at the JBDD documentation and exaples at L<http://javaddlib.sourceforge.net/jbdd/>.

=head1 VERSION
    
This man page documents "PBDD" version 0.01.

=head1 AUTHOR

  Gianluca Torta
  mailto:torta@di.unito.it

=head1 COPYRIGHT

Copyright (c) 2011 by Gianluca Torta. All rights reserved.

=head1 LICENSE

This package is free software; you can use, modify and redistribute
it under the same terms as Perl itself, i.e., at your option, under
the terms either of the "Artistic License" or the "GNU General Public

licences/license.JBDD  view on Meta::CPAN



JBDD copyright message


JBDD uses a public domain license based on zlib:

/*
  JBDD -- a Java interface to CUDD and BuDDY


  Copyright (C) 2003-2004 Arash Vahidi

  This software is provided 'as-is', without any express or implied
  warranty.  In no event will the authors be held liable for any damages
  arising from the use of this software.

  Permission is granted to anyone to use this software for any purpose,
  including commercial applications, and to alter it and redistribute it
  freely, subject to the following restrictions:

  1. The origin of this software must not be misrepresented; you must not
     claim that you wrote the original software. If you use this software
     in a product, an acknowledgment in the product documentation would be
     appreciated but is not required.
  2. Altered source versions must be plainly marked as such, and must not be
     misrepresented as being the original software.
  3. This notice may not be removed or altered from any source distribution.

  Arash Vahidi (vahidi [at] users.sourceforge.net)

*/



t/PBDD.t  view on Meta::CPAN


use Test::More tests => 39;
BEGIN { use_ok('AI::PBDD') };

#########################

# Insert your test code below, the Test::More module is use()ed here so read
# its man page ( perldoc Test::More ) for help writing this test script.

sub DumpBDD {
    my ($bdd,$names) = @_;
    my ($idx, $then, $else);

    if (AI::PBDD::internal_isconst($bdd) && AI::PBDD::internal_constvalue($bdd)) {
      return 'T';
    }
    if (AI::PBDD::internal_isconst($bdd) && !AI::PBDD::internal_constvalue($bdd)) {
      return 'F';
    }
    $idx = AI::PBDD::internal_index($bdd);
    $then = DumpBDD(AI::PBDD::internal_then($bdd), $names);
    $else = DumpBDD(AI::PBDD::internal_else($bdd), $names);

    return $$names{$idx} . " ($then) ($else)";
}

{
  #
  # getOne
  #
  AI::PBDD::init(100,1000000);
  my $v = AI::PBDD::getOne();
  is($v, 1, "getOne()");  
  AI::PBDD::kill();
}

{
  #
  # getZero
  #
  AI::PBDD::init(100,1000000);
  my $v = AI::PBDD::getZero();
  is($v, 0, "getZero()"); 
  AI::PBDD::kill();
}

{
  #
  # createBDD
  #

  # created BDDs (variables) are even integers
  AI::PBDD::init(100,1000000);
  my $v = AI::PBDD::createBDD();

  ok(!($v % 2), "first createBDD()");  

  ok(!($v % 2), "second createBDD()");  
  AI::PBDD::kill();
}

{
  #
  # getVarCount
  # getBDD
  #
  AI::PBDD::init(100,1000000);
  my $v1 = AI::PBDD::createBDD();
  my $v2 = AI::PBDD::createBDD();
  my $v3 = AI::PBDD::createBDD();
  my $v4 = AI::PBDD::createBDD();

  my $n = AI::PBDD::getVarCount();

  is($n, 4, "getVarCount()");  
  
  my $i = AI::PBDD::getBDD(2);
  is($i, $v3, "getBDD()");  

  AI::PBDD::kill();
}

{
  #
  # ref
  # deref
  # localDeref
  #
  AI::PBDD::init(100,1000000);
  my $bdd1 = AI::PBDD::createBDD();
  my $bdd2 = AI::PBDD::createBDD();
  # need a composite BDD: variables refcount is always 1023	
  my $bdd = AI::PBDD::and($bdd1,$bdd2); 

  AI::PBDD::ref($bdd);
  AI::PBDD::ref($bdd);

  my $rc = AI::PBDD::internal_refcount($bdd);
  is($rc, 3, "ref()");  

  AI::PBDD::deref($bdd);

  $rc = AI::PBDD::internal_refcount($bdd);
  is($rc, 2, "deref()");  

  AI::PBDD::localDeref($bdd);

  $rc = AI::PBDD::internal_refcount($bdd);
  is($rc, 1, "localDeref()");  
  
  AI::PBDD::kill();
}

{
  #
  # and
  # andTo
  #
  AI::PBDD::init(100,1000000);
  my %names = ();
  my $bdd1 = AI::PBDD::createBDD();
  $names{AI::PBDD::internal_index($bdd1)} = 'A';
  my $bdd2 = AI::PBDD::createBDD();
  $names{AI::PBDD::internal_index($bdd2)} = 'B';
  my $bdd3 = AI::PBDD::createBDD();
  $names{AI::PBDD::internal_index($bdd3)} = 'C';

  my $bdd = AI::PBDD::and($bdd1,$bdd2);
  my $dmp = DumpBDD($bdd, \%names);
  is($dmp, "A (B (T) (F)) (F)", "and()");  
  
  my $bddTo = AI::PBDD::andTo($bdd,$bdd3);
  $dmp = DumpBDD($bddTo, \%names);
  my $rc = AI::PBDD::internal_refcount($bdd);
  ok($dmp eq "A (B (C (T) (F)) (F)) (F)" && $rc == 0, "andTo()");  

  AI::PBDD::kill();
}

{
  #
  # or
  # orTo
  #
  AI::PBDD::init(100,1000000);
  my %names = ();
  my $bdd1 = AI::PBDD::createBDD();
  $names{AI::PBDD::internal_index($bdd1)} = 'A';
  my $bdd2 = AI::PBDD::createBDD();
  $names{AI::PBDD::internal_index($bdd2)} = 'B';
  my $bdd3 = AI::PBDD::createBDD();
  $names{AI::PBDD::internal_index($bdd3)} = 'C';

  my $bdd = AI::PBDD::or($bdd1,$bdd2);
  my $dmp = DumpBDD($bdd, \%names);
  is($dmp, "A (T) (B (T) (F))", "or()");  

  my $bddTo = AI::PBDD::orTo($bdd,$bdd3);
  $dmp = DumpBDD($bddTo, \%names);
  my $rc = AI::PBDD::internal_refcount($bdd);
  ok($dmp eq "A (T) (B (T) (C (T) (F)))" && $rc == 0, "orTo()");  
  
  AI::PBDD::kill();
}

{
  #
  # nand
  #
  AI::PBDD::init(100,1000000);
  my %names = ();
  my $bdd1 = AI::PBDD::createBDD();
  $names{AI::PBDD::internal_index($bdd1)} = 'A';
  my $bdd2 = AI::PBDD::createBDD();
  $names{AI::PBDD::internal_index($bdd2)} = 'B';

  my $bdd = AI::PBDD::nand($bdd1,$bdd2);
  my $dmp = DumpBDD($bdd, \%names);
  is($dmp, "A (B (F) (T)) (T)", "nand()");  

  AI::PBDD::kill();
}

{
  #
  # nor
  #
  AI::PBDD::init(100,1000000);
  my %names = ();
  my $bdd1 = AI::PBDD::createBDD();
  $names{AI::PBDD::internal_index($bdd1)} = 'A';
  my $bdd2 = AI::PBDD::createBDD();
  $names{AI::PBDD::internal_index($bdd2)} = 'B';

  my $bdd = AI::PBDD::nor($bdd1,$bdd2);
  my $dmp = DumpBDD($bdd, \%names);
  is($dmp, "A (F) (B (F) (T))", "nor()");  

  AI::PBDD::kill();
}

{
  #
  # xor
  #
  AI::PBDD::init(100,1000000);
  my %names = ();
  my $bdd1 = AI::PBDD::createBDD();
  $names{AI::PBDD::internal_index($bdd1)} = 'A';
  my $bdd2 = AI::PBDD::createBDD();
  $names{AI::PBDD::internal_index($bdd2)} = 'B';

  my $bdd = AI::PBDD::xor($bdd1,$bdd2);
  my $dmp = DumpBDD($bdd, \%names);
  is($dmp, "A (B (F) (T)) (B (T) (F))", "xor()");  

  AI::PBDD::kill();
}

{
  #
  # ite
  #
  AI::PBDD::init(100,1000000);
  my %names = ();
  my $bdd1 = AI::PBDD::createBDD();
  $names{AI::PBDD::internal_index($bdd1)} = 'A';
  my $bdd2 = AI::PBDD::createBDD();
  $names{AI::PBDD::internal_index($bdd2)} = 'B';
  my $bdd3 = AI::PBDD::createBDD();
  $names{AI::PBDD::internal_index($bdd3)} = 'C';

  my $bdd = AI::PBDD::ite($bdd1,$bdd2, $bdd3);
  my $dmp = DumpBDD($bdd, \%names);
  is($dmp, "A (B (T) (F)) (C (T) (F))", "ite()");  

  AI::PBDD::kill();
}

{
  #
  # imp
  #
  AI::PBDD::init(100,1000000);
  my %names = ();
  my $bdd1 = AI::PBDD::createBDD();
  $names{AI::PBDD::internal_index($bdd1)} = 'A';
  my $bdd2 = AI::PBDD::createBDD();
  $names{AI::PBDD::internal_index($bdd2)} = 'B';

  my $bdd = AI::PBDD::imp($bdd1,$bdd2);
  my $dmp = DumpBDD($bdd, \%names);
  is($dmp, "A (B (T) (F)) (T)", "imp()");  

  AI::PBDD::kill();
}

{
  #
  # biimp
  #
  AI::PBDD::init(100,1000000);
  my %names = ();
  my $bdd1 = AI::PBDD::createBDD();
  $names{AI::PBDD::internal_index($bdd1)} = 'A';
  my $bdd2 = AI::PBDD::createBDD();
  $names{AI::PBDD::internal_index($bdd2)} = 'B';

  my $bdd = AI::PBDD::biimp($bdd1,$bdd2);
  my $dmp = DumpBDD($bdd, \%names);
  is($dmp, "A (B (T) (F)) (B (F) (T))", "biimp()");  

  AI::PBDD::kill();
}

{
  #
  # not
  #
  AI::PBDD::init(100,1000000);
  my %names = ();
  my $bdd1 = AI::PBDD::createBDD();
  $names{AI::PBDD::internal_index($bdd1)} = 'A';

  my $bdd = AI::PBDD::not($bdd1);
  my $dmp = DumpBDD($bdd, \%names);
  is($dmp, "A (F) (T)", "not()");  

  AI::PBDD::kill();
}

{
  #
  # makeSet
  #
  my @vars;
  my %names = ();
  AI::PBDD::init(100,1000000);
  my $bdd1 = AI::PBDD::createBDD();
  $names{AI::PBDD::internal_index($bdd1)} = 'A';
  push @vars, $bdd1;
  my $bdd2 = AI::PBDD::createBDD();
  $names{AI::PBDD::internal_index($bdd2)} = 'B';
  push @vars, $bdd2;
  
  my $set = AI::PBDD::makeSet(\@vars, 2);
  my $dmp = DumpBDD($set, \%names);

  is($dmp, "A (B (T) (F)) (F)", "first makeSet()");  

  $set = AI::PBDD::makeSet(\@vars, 1, 1);
  $dmp = DumpBDD($set, \%names);

  is($dmp, "B (T) (F)", "second makeSet()");  

  AI::PBDD::kill();
}

{
  #
  # exists
  #
  AI::PBDD::init(100,1000000);
  my %names = ();
  my $bdd1 = AI::PBDD::createBDD();
  $names{AI::PBDD::internal_index($bdd1)} = 'A';
  my $bdd2 = AI::PBDD::createBDD();
  $names{AI::PBDD::internal_index($bdd2)} = 'B';
  my $bdd3 = AI::PBDD::and($bdd1,$bdd2);

  my $bdd = AI::PBDD::exists($bdd3, $bdd1);
  my $dmp = DumpBDD($bdd, \%names);
  is($dmp, "B (T) (F)", "first exists()");  

  $bdd = AI::PBDD::exists($bdd3, $bdd2);
  $dmp = DumpBDD($bdd, \%names);
  is($dmp, "A (T) (F)", "second exists()");  

  AI::PBDD::kill();
}

{
  #
  # forall
  #
  AI::PBDD::init(100,1000000);
  my %names = ();
  my $bdd1 = AI::PBDD::createBDD();
  $names{AI::PBDD::internal_index($bdd1)} = 'A';
  my $bdd2 = AI::PBDD::createBDD();
  $names{AI::PBDD::internal_index($bdd2)} = 'B';
  my $bdd3 = AI::PBDD::or($bdd1,$bdd2);

  my $bdd = AI::PBDD::forall($bdd3, $bdd1);
  my $dmp = DumpBDD($bdd, \%names);
  is($dmp, "B (T) (F)", "first forall()");  

  $bdd = AI::PBDD::forall($bdd3, $bdd2);
  $dmp = DumpBDD($bdd, \%names);
  is($dmp, "A (T) (F)", "second forall()");  

  AI::PBDD::kill();
}

{
  #
  # relProd
  #
  AI::PBDD::init(100,1000000);
  my %names = ();
  my $bdd1 = AI::PBDD::createBDD();
  $names{AI::PBDD::internal_index($bdd1)} = 'A';
  my $bdd2 = AI::PBDD::createBDD();
  $names{AI::PBDD::internal_index($bdd2)} = 'B';
  my $bdd3 = AI::PBDD::createBDD();
  $names{AI::PBDD::internal_index($bdd3)} = 'C';
  my $bdd4 = AI::PBDD::and($bdd1,$bdd2);
  my $bdd5 = AI::PBDD::and($bdd2,$bdd3);

  my $bdd = AI::PBDD::relProd($bdd4, $bdd5, $bdd2);
  my $dmp = DumpBDD($bdd, \%names);
  is($dmp, "A (C (T) (F)) (F)", "relProd()");  

  AI::PBDD::kill();
}

{
  #
  # restrict
  #
  AI::PBDD::init(100,1000000);
  my %names = ();
  my $bdd1 = AI::PBDD::createBDD();
  $names{AI::PBDD::internal_index($bdd1)} = 'A';
  my $bdd2 = AI::PBDD::createBDD();
  $names{AI::PBDD::internal_index($bdd2)} = 'B';
  my $bdd3 = AI::PBDD::and($bdd1,$bdd2);

  my $bdd = AI::PBDD::restrict($bdd3, $bdd1);
  my $dmp = DumpBDD($bdd, \%names);
  is($dmp, "B (T) (F)", "first restrict()");  

  $bdd = AI::PBDD::restrict($bdd3, AI::PBDD::not($bdd1));
  $dmp = DumpBDD($bdd, \%names);
  is($dmp, "F", "second restrict()");  

  AI::PBDD::kill();
}

{
  #
  # constrain
  #
  AI::PBDD::init(100,1000000);
  my %names = ();
  my $bdd1 = AI::PBDD::createBDD();
  $names{AI::PBDD::internal_index($bdd1)} = 'A';
  my $bdd2 = AI::PBDD::createBDD();
  $names{AI::PBDD::internal_index($bdd2)} = 'B';
  my $bdd3 = AI::PBDD::createBDD();
  $names{AI::PBDD::internal_index($bdd3)} = 'C';
  my $bdd4 = AI::PBDD::createBDD();
  $names{AI::PBDD::internal_index($bdd4)} = 'D';
  my $bdd5 = AI::PBDD::or($bdd1,$bdd2);
  my $bdd6 = AI::PBDD::or($bdd3,$bdd4);
  my $bdd7 = AI::PBDD::and($bdd5,$bdd6);
  my $bdd8 = AI::PBDD::or($bdd1,$bdd3);

  my $bdd = AI::PBDD::constrain($bdd7, $bdd8);
  my $dmp = DumpBDD($bdd, \%names);
  is($dmp, "A (C (T) (D (T) (F))) (B (T) (F))", "constrain()");  

  AI::PBDD::kill();
}

{
  #
  # replace
  #
  AI::PBDD::init(100,1000000);
  my %names = ();
  my $bdd1 = AI::PBDD::createBDD();
  $names{AI::PBDD::internal_index($bdd1)} = 'A';
  my $bdd2 = AI::PBDD::createBDD();
  $names{AI::PBDD::internal_index($bdd2)} = 'B';
  my $bdd3 = AI::PBDD::createBDD();
  $names{AI::PBDD::internal_index($bdd3)} = 'C';
  my $bdd4 = AI::PBDD::createBDD();
  $names{AI::PBDD::internal_index($bdd4)} = 'D';
  my $bdd5 = AI::PBDD::or($bdd1, $bdd2);

  my @old = ($bdd1,$bdd2);
  my @new = ($bdd3,$bdd4);

  my $pair = AI::PBDD::createPair(\@old, \@new);

  my $bdd = AI::PBDD::replace($bdd5, $pair);
  my $dmp = DumpBDD($bdd, \%names);
  is($dmp, "C (T) (D (T) (F))", "replace()");  

  AI::PBDD::deletePair($pair);

  AI::PBDD::kill();
}

{
  #
  # support
  #
  AI::PBDD::init(100,1000000);
  my %names = ();
  my $bdd1 = AI::PBDD::createBDD();
  $names{AI::PBDD::internal_index($bdd1)} = 'A';
  my $bdd2 = AI::PBDD::createBDD();
  $names{AI::PBDD::internal_index($bdd2)} = 'B';
  my $bdd = AI::PBDD::and($bdd1, $bdd2);

  my $cube = AI::PBDD::support($bdd);
  my $dmp = DumpBDD($cube, \%names);
  is($dmp, "A (B (T) (F)) (F)", "support()");  

  AI::PBDD::kill();
}

{
  #
  # nodeCount
  #
  AI::PBDD::init(100,1000000);
  my %names = ();
  my $bdd1 = AI::PBDD::createBDD();
  $names{AI::PBDD::internal_index($bdd1)} = 'A';
  my $bdd2 = AI::PBDD::createBDD();
  $names{AI::PBDD::internal_index($bdd2)} = 'B';
  my $bdd3 = AI::PBDD::createBDD();
  $names{AI::PBDD::internal_index($bdd3)} = 'C';
  my $bdd4 = AI::PBDD::createBDD();
  $names{AI::PBDD::internal_index($bdd4)} = 'D';
  my $bdd5 = AI::PBDD::or($bdd1, $bdd2);
  my $bdd6 = AI::PBDD::or($bdd3, $bdd4);
  my $bdd7 = AI::PBDD::and($bdd5, $bdd6);

  my $cnt = AI::PBDD::nodeCount($bdd7);
  is($cnt, 4, "nodeCount()");  

  AI::PBDD::kill();
}

{
  #
  # satOne
  # satCount
  #
  AI::PBDD::init(100,1000000);
  my %names = ();
  my $bdd1 = AI::PBDD::createBDD();
  $names{AI::PBDD::internal_index($bdd1)} = 'A';
  my $bdd2 = AI::PBDD::createBDD();
  $names{AI::PBDD::internal_index($bdd2)} = 'B';

  my $bdd = AI::PBDD::xor($bdd1, $bdd2);
  my $minterm = AI::PBDD::satOne($bdd);
  my $dmp = DumpBDD($minterm, \%names);
  ok($dmp eq "A (B (F) (T)) (F)" ||
     $dmp eq "A (F) (B (T) (F))", "satOne()");  

  my $cnt = AI::PBDD::satCount($bdd);
  is($cnt, 2*2**98, "first satCount()");

  $cnt = AI::PBDD::satCount($bdd,98);
  is($cnt, 2, "second satCount()");

  $bdd = AI::PBDD::or($bdd1, $bdd2);
  $cnt = AI::PBDD::satCount($bdd);
  is($cnt, 3*2**98, "third satCount()");

  $cnt = AI::PBDD::satCount($bdd,98);
  is($cnt, 3, "fourth satCount()");

  AI::PBDD::kill();
}



( run in 0.314 second using v1.01-cache-2.11-cpan-4d50c553e7e )