AI-PBDD
view release on metacpan or search on metacpan
#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;
}
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)
{
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 ]
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
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:
}
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 (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);
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)
}
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
//#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
static int varcount = 0; // current var count!
#define MAX_NODES 8000000
lib/AI/PBDD.pm view on Meta::CPAN
// 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
lib/AI/PBDD.pm view on Meta::CPAN
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);
lib/AI/PBDD.pm view on Meta::CPAN
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...
lib/AI/PBDD.pm view on Meta::CPAN
=item B<$cnt = satCount($bdd,$nvars)>
Number of minterms that satisfy C<$bdd>. The number of minterms is computed by considering all of the variables in the package (defined with the call to the C<init> function), but it is possible to specify the number of variables C<$nvars> to be igno...
=back
=head2 PRINTING
=over 4
=item B<printDot($bdd)>
=item B<printDot($bdd,$filename)>
Print the BDD as a Graphviz DOT model to STDOUT (or the given C<$filename>).
=item B<printSet($bdd)>
Print the BDD minterms to STDOUT.
=item B<print($bdd)>
Print the BDD in the native BuDDy representation to STDOUT.
=back
=head2 DEBUGGING
=over 4
=item B<printStats>
Print package statistics to STDOUT.
=item B<$ok = checkPackage>
Return 0 if something is wrong.
=item B<debugPackage>
Debug the BDD package.
# Before `make install' is performed this script should be runnable with
# `make test'. After `make install' it should work as `perl PBDD.t'
#########################
# change 'tests => 1' to 'tests => last_test_to_print';
use strict;
use warnings;
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
( run in 0.654 second using v1.01-cache-2.11-cpan-de7293f3b23 )