AI-PBDD
view release on metacpan or search on metacpan
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
{
"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"
}
---
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>') : ()),
);
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.
#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 ();
}
/**
* 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>
//#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)
*/
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 )