Commit 992a9686 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

* wrap/python/buddy.i: New file.

* wrap/python/Makefile.am (EXTRA_DIST): Add it.
(python_PYTHON, MAINTAINERCLEANFILES): Add buddy.py.
(pyexec_LTLIBRARIES): Add _buddy.la.
(_buddy_la_SOURCES, _buddy_la_LDFLAGS, $(srcdir)/buddy_wrap.cxx)
($(srcdir)/buddy.py): New.
* wrap/python/tests/bddnqueen.py: New file.
* wrap/python/tests/Makefile.am (TESTS): Add it.
parent f1f81fbf
2003-08-01 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* wrap/python/buddy.i: New file.
* wrap/python/Makefile.am (EXTRA_DIST): Add it.
(python_PYTHON, MAINTAINERCLEANFILES): Add buddy.py.
(pyexec_LTLIBRARIES): Add _buddy.la.
(_buddy_la_SOURCES, _buddy_la_LDFLAGS, $(srcdir)/buddy_wrap.cxx)
($(srcdir)/buddy.py): New.
* wrap/python/tests/bddnqueen.py: New file.
* wrap/python/tests/Makefile.am (TESTS): Add it.
* src/ltlvisit/lunabbrev.cc, src/ltlvisit/lunabbrev.hh: Merge the
two unabbreviate_logic definitions (const and non-const) into a
function that takes a const formula* and return a non-const
......
......@@ -4,7 +4,8 @@ Makefile
Makefile.in
*.la
spot.py*
buddy.py*
*.lo
*.loT
spot_wrap.cxx
*_wrap.cxx
*.pyc
SUBDIRS = tests
AM_CPPFLAGS = -I$(PYTHONINC) -I$(top_srcdir)/src
AM_CPPFLAGS = -I$(PYTHONINC) -I$(top_srcdir)/src $(BUDDY_CPPFLAGS)
python_PYTHON = $(srcdir)/spot.py
pyexec_LTLIBRARIES = _spot.la
EXTRA_DIST = ltihooks.py spot.i buddy.i
python_PYTHON = $(srcdir)/spot.py $(srcdir)/buddy.py
pyexec_LTLIBRARIES = _spot.la _buddy.la
_spot_la_SOURCES = $(srcdir)/spot_wrap.cxx
_spot_la_LDFLAGS = -avoid-version -module
_spot_la_LIBADD = $(top_builddir)/src/libspot.la
EXTRA_DIST = ltihooks.py spot.i
$(srcdir)/spot_wrap.cxx: $(srcdir)/spot.i
swig -c++ -python -I$(top_srcdir)/src $(srcdir)/spot.i
$(srcdir)/spot.py: $(srcdir)/spot.i
$(MAKE) $(AM_MAKEFLAGS) spot_wrap.cxx
_buddy_la_SOURCES = $(srcdir)/buddy_wrap.cxx
_buddy_la_LDFLAGS = -avoid-version -module $(BUDDY_LDFLAGS)
$(srcdir)/buddy_wrap.cxx: $(srcdir)/buddy.i
swig -c++ -python $(BUDDY_CPPFLAGS) $(srcdir)/buddy.i
$(srcdir)/buddy.py: $(srcdir)/buddy.i
$(MAKE) $(AM_MAKEFLAGS) buddy_wrap.cxx
MAINTAINERCLEANFILES = $(srcdir)/spot_wrap.cxx $(srcdir)/spot.py
%module buddy
%include "std_string.i"
%{
#include <sstream>
#include "bdd.h"
%}
struct bdd
{
int id(void) const;
};
int bdd_init(int, int);
void bdd_done(void);
int bdd_setvarnum(int);
int bdd_extvarnum(int);
int bdd_isrunning(void);
int bdd_setmaxnodenum(int);
int bdd_setmaxincrease(int);
int bdd_setminfreenodes(int);
int bdd_getnodenum(void);
int bdd_getallocnum(void);
char* bdd_versionstr(void);
int bdd_versionnum(void);
void bdd_fprintstat(FILE *);
void bdd_printstat(void);
const char *bdd_errstring(int);
void bdd_clear_error(void);
bdd bdd_ithvar(int v);
bdd bdd_nithvar(int v);
int bdd_var(const bdd &r);
bdd bdd_low(const bdd &r);
bdd bdd_high(const bdd &r);
int bdd_scanset(const bdd &r, int *&v, int &n);
bdd bdd_makeset(int *v, int n);
int bdd_setbddpair(bddPair *p, int ov, const bdd &nv);
bdd bdd_replace(const bdd &r, bddPair *p);
bdd bdd_compose(const bdd &f, const bdd &g, int v);
bdd bdd_veccompose(const bdd &f, bddPair *p);
bdd bdd_restrict(const bdd &r, const bdd &var);
bdd bdd_constrain(const bdd &f, const bdd &c);
bdd bdd_simplify(const bdd &d, const bdd &b);
bdd bdd_ibuildcube(int v, int w, int *a);
bdd bdd_not(const bdd &r);
bdd bdd_apply(const bdd &l, const bdd &r, int op);
bdd bdd_and(const bdd &l, const bdd &r);
bdd bdd_or(const bdd &l, const bdd &r);
bdd bdd_xor(const bdd &l, const bdd &r);
bdd bdd_imp(const bdd &l, const bdd &r);
bdd bdd_biimp(const bdd &l, const bdd &r);
bdd bdd_ite(const bdd &f, const bdd &g, const bdd &h);
bdd bdd_exist(const bdd &r, const bdd &var);
bdd bdd_existcomp(const bdd &r, const bdd &var);
bdd bdd_forall(const bdd &r, const bdd &var);
bdd bdd_forallcomp(const bdd &r, const bdd &var);
bdd bdd_unique(const bdd &r, const bdd &var);
bdd bdd_uniquecomp(const bdd &r, const bdd &var);
bdd bdd_appex(const bdd &l, const bdd &r, int op, const bdd &var);
bdd bdd_appexcomp(const bdd &l, const bdd &r, int op, const bdd &var);
bdd bdd_appall(const bdd &l, const bdd &r, int op, const bdd &var);
bdd bdd_appallcomp(const bdd &l, const bdd &r, int op, const bdd &var);
bdd bdd_appuni(const bdd &l, const bdd &r, int op, const bdd &var);
bdd bdd_appunicomp(const bdd &l, const bdd &r, int op, const bdd &var);
bdd bdd_support(const bdd &r);
bdd bdd_satone(const bdd &r);
bdd bdd_satoneset(const bdd &r, const bdd &var, const bdd &pol);
bdd bdd_fullsatone(const bdd &r);
void bdd_allsat(const bdd &r, bddallsathandler handler);
double bdd_satcount(const bdd &r);
double bdd_satcountset(const bdd &r, const bdd &varset);
double bdd_satcountln(const bdd &r);
double bdd_satcountlnset(const bdd &r, const bdd &varset);
int bdd_nodecount(const bdd &r);
int* bdd_varprofile(const bdd &r);
double bdd_pathcount(const bdd &r);
void bdd_fprinttable(FILE *file, const bdd &r);
void bdd_printtable(const bdd &r);
void bdd_fprintset(FILE *file, const bdd &r);
void bdd_printset(const bdd &r);
void bdd_printdot(const bdd &r);
void bdd_fprintdot(FILE* ofile, const bdd &r);
int bdd_fnprintdot(char* fname, const bdd &r);
int bdd_fnsave(char *fname, const bdd &r);
int bdd_save(FILE *ofile, const bdd &r);
int bdd_fnload(char *fname, bdd &r);
int bdd_load(FILE *ifile, bdd &r);
int bdd_addvarblock(const bdd &v, int f);
extern const bdd bddfalse;
extern const bdd bddtrue;
#define bddop_and 0
#define bddop_xor 1
#define bddop_or 2
#define bddop_nand 3
#define bddop_nor 4
#define bddop_imp 5
#define bddop_biimp 6
#define bddop_diff 7
#define bddop_less 8
#define bddop_invimp 9
#define BDD_REORDER_NONE 0
#define BDD_REORDER_WIN2 1
#define BDD_REORDER_WIN2ITE 2
#define BDD_REORDER_SIFT 3
#define BDD_REORDER_SIFTITE 4
#define BDD_REORDER_WIN3 5
#define BDD_REORDER_WIN3ITE 6
#define BDD_REORDER_RANDOM 7
%extend bdd {
int
__cmp__(bdd* b)
{
return b->id() - self->id();
}
std::string
__str__(void)
{
std::ostringstream res;
res << "bdd(id=" << self->id() << ")";
return res.str();
}
bdd __and__(bdd& other) { return *self & other; }
bdd __xor__(bdd& other) { return *self ^ other; }
bdd __or__(bdd& other) { return *self | other; }
bdd __rshift__(bdd& other) { return *self >> other; }
bdd __lshift__(bdd& other) { return *self << other; }
bdd __sub__(bdd& other) { return *self - other; }
bdd __neg__(void) { return !*self; }
}
\ No newline at end of file
......@@ -5,4 +5,5 @@ TESTS_ENVIRONMENT = ./run
check_SCRIPTS = run
TESTS = \
ltlsimple.py
ltlsimple.py \
bddnqueen.py
\ No newline at end of file
# Python translation of the C++ example from the BuDDy distribution.
# (compare with buddy/examples/queen/queen.cxx)
import ltihooks
import sys
from buddy import *
# Build the requirements for all other fields than (i,j) assuming
# that (i,j) has a queen.
def build(i, j):
a = b = c = d = bddtrue
# No one in the same column.
for l in side:
if l != j:
a &= X[i][j] >> -X[i][l]
# No one in the same row.
for k in side:
if k != i:
b &= X[i][j] >> -X[k][j]
# No one in the same up-right diagonal.
for k in side:
ll = k - i + j
if ll >= 0 and ll < N:
if k != i:
c &= X[i][j] >> -X[k][ll]
# No one in the same down-right diagonal.
for k in side:
ll = i + j - k
if ll >= 0 and ll < N:
if k != i:
c &= X[i][j] >> -X[k][ll]
global queen
queen &= a & b & c & d
# Get the number of queens from the command-line, or default to 8.
if len(sys.argv) > 1:
N = int(argv[1])
else:
N = 8
side = range(N)
# Initialize with 100000 nodes, 10000 cache entries and NxN variables.
bdd_init(N * N * 256, 10000)
bdd_setvarnum(N * N)
queen = bddtrue
# Build variable array.
X = [[bdd_ithvar(i*N+j) for j in side] for i in side]
# Place a queen in each row.
for i in side:
e = bddfalse
for j in side:
e |= X[i][j]
queen &= e
# Build requirements for each variable(field).
for i in side:
for j in side:
print "Adding position %d, %d" % (i, j)
build(i, j)
# Print the results.
print "There are", bdd_satcount(queen), "solutions"
print "one is:"
solution = bdd_satone(queen)
bdd_printset(solution)
print
bdd_done()
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment