From 1e2669d6407534b8067d18548233ac3ed27067d7 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 14 May 2004 16:11:46 +0000 Subject: [PATCH] * wrap/python/buddy.i: Preliminary bindings for FDD and BVEC. --- ChangeLog | 2 + wrap/python/buddy.i | 164 ++++++++++++++++++++++++++++++++++++++------ 2 files changed, 145 insertions(+), 21 deletions(-) diff --git a/ChangeLog b/ChangeLog index bfd13f923..546f81e35 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,7 @@ 2004-05-14 Alexandre Duret-Lutz + * wrap/python/buddy.i: Preliminary bindings for FDD and BVEC. + * ltltest/inf.cc, ltltest/reduc.cc, ltlvisit/reducform.cc: Fix style. * sanity/style.test: More tests. diff --git a/wrap/python/buddy.i b/wrap/python/buddy.i index 626842e0a..da495788d 100644 --- a/wrap/python/buddy.i +++ b/wrap/python/buddy.i @@ -1,23 +1,34 @@ -// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre -// et Marie Curie. -// -// This file is part of Spot, a model checking library. -// -// Spot is free software; you can redistribute it and/or modify it -// under the terms of the GNU General Public License as published by -// the Free Software Foundation; either version 2 of the License, or -// (at your option) any later version. -// -// Spot is distributed in the hope that it will be useful, but WITHOUT -// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -// License for more details. -// -// You should have received a copy of the GNU General Public License -// along with Spot; see the file COPYING. If not, write to the Free -// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA -// 02111-1307, USA. +/*======================================================================== + Copyright (C) 1996-2003 by Jorn Lind-Nielsen + All rights reserved + + Permission is hereby granted, without written agreement and without + license or royalty fees, to use, reproduce, prepare derivative + works, distribute, and display this software and its documentation + for any purpose, provided that (1) the above copyright notice and + the following two paragraphs appear in all copies of the source code + and (2) redistributions, including without limitation binaries, + reproduce these notices in the supporting documentation. Substantial + modifications to this software may be copyrighted by their authors + and need not follow the licensing terms described here, provided + that the new terms are clearly indicated in all files where they apply. + + IN NO EVENT SHALL JORN LIND-NIELSEN, OR DISTRIBUTORS OF THIS + SOFTWARE BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL, + INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS + SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE AUTHORS OR ANY OF THE + ABOVE PARTIES HAVE BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + + JORN LIND-NIELSEN SPECIFICALLY DISCLAIM ANY WARRANTIES, INCLUDING, + BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND + FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS + ON AN "AS IS" BASIS, AND THE AUTHORS AND DISTRIBUTORS HAVE NO + OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR + MODIFICATIONS. +========================================================================*/ + +/* Derived from Buddy's header by Alexandre.Duret-Lutz@lip6.fr */ + %module buddy @@ -26,6 +37,8 @@ %{ #include #include "bdd.h" +#include "fdd.h" +#include "bvec.h" %} struct bdd @@ -156,4 +169,113 @@ extern const bdd bddtrue; bdd __sub__(bdd& other) { return *self - other; } bdd __neg__(void) { return !*self; } -} \ No newline at end of file +} + +/************************************************************************/ + +int fdd_extdomain(int*, int); +int fdd_overlapdomain(int, int); +void fdd_clearall(void); +int fdd_domainnum(void); +int fdd_domainsize(int); +int fdd_varnum(int); +int* fdd_vars(int); +bdd fdd_ithvar(int, int); +int fdd_scanvar(bdd, int); +int* fdd_scanallvar(bdd); +bdd fdd_ithset(int); +bdd fdd_domain(int); +bdd fdd_equals(int, int); +void fdd_printset(bdd); +void fdd_fprintset(FILE*, bdd); +int fdd_scanset(const bdd &, int *&, int &); +bdd fdd_makeset(int*, int); +int fdd_intaddvarblock(int, int, int); +int fdd_setpair(bddPair*, int, int); +int fdd_setpairs(bddPair*, int*, int*, int); + +/************************************************************************/ + +bvec bvec_copy(bvec v); +bvec bvec_true(int bitnum); +bvec bvec_false(int bitnum); +bvec bvec_con(int bitnum, int val); +bvec bvec_var(int bitnum, int offset, int step); +bvec bvec_varfdd(int var); +bvec bvec_varvec(int bitnum, int *var); +bvec bvec_coerce(int bitnum, bvec v); +int bvec_isconst(bvec e); +int bvec_val(bvec e); +bvec bvec_map1(const bvec&, bdd (*fun)(const bdd &)); +bvec bvec_map2(const bvec&, const bvec&, bdd (*fun)(const bdd &, const bdd &)); +bvec bvec_map3(const bvec&, const bvec&, const bvec &, + bdd (*fun)(const bdd &, const bdd &, const bdd &)); + +bvec bvec_add(bvec left, bvec right); +bvec bvec_sub(bvec left, bvec right); +bvec bvec_mulfixed(bvec e, int c); +bvec bvec_mul(bvec left, bvec right); +int bvec_divfixed(const bvec &, int c, bvec &, bvec &); +int bvec_div(const bvec &, const bvec &, bvec &, bvec &); +bvec bvec_ite(bdd a, bvec b, bvec c); +bvec bvec_shlfixed(bvec e, int pos, bdd c); +bvec bvec_shl(bvec l, bvec r, bdd c); +bvec bvec_shrfixed(bvec e, int pos, bdd c); +bvec bvec_shr(bvec l, bvec r, bdd c); +bdd bvec_lth(bvec left, bvec right); +bdd bvec_lte(bvec left, bvec right); +bdd bvec_gth(bvec left, bvec right); +bdd bvec_gte(bvec left, bvec right); +bdd bvec_equ(bvec left, bvec right); +bdd bvec_neq(bvec left, bvec right); + +class bvec +{ + public: + bvec(void); + bvec(int bitnum); + bvec(int bitnum, int val); + bvec(const bvec &v); + ~bvec(void); + + void set(int i, const bdd &b); + int bitnum(void) const; + int empty(void) const; + bvec operator=(const bvec &src); + + bvec operator&(const bvec &a) const; + bvec operator^(const bvec &a) const; + bvec operator|(const bvec &a) const; + bvec operator!(void) const; + bvec operator<<(int a) const; + bvec operator<<(const bvec &a) const; + bvec operator>>(int a) const; + bvec operator>>(const bvec &a) const; + bvec operator+(const bvec &a) const; + bvec operator-(const bvec &a) const; + bvec operator*(int a) const; + bvec operator*(const bvec a) const; + bdd operator<(const bvec &a) const; + bdd operator<=(const bvec &a) const; + bdd operator>(const bvec &a) const; + bdd operator>=(const bvec &a) const; + bdd operator==(const bvec &a) const; + bdd operator!=(const bvec &a) const; +}; + + +%extend bvec { + std::string + __str__(void) + { + std::ostringstream res; + res << "bvec(bitnum=" << self->bitnum() << ")"; + return res.str(); + } + + bdd + __getitem__(int i) + { + return (*self)[i]; + } +}