* wrap/python/buddy.i: Preliminary bindings for FDD and BVEC.
This commit is contained in:
Alexandre Duret-Lutz
parent
f2f10852c6
commit
1e2669d640
2 changed files with 145 additions and 21 deletions
|
|
@ -1,5 +1,7 @@
|
||||||
2004-05-14 Alexandre Duret-Lutz <adl@src.lip6.fr>
|
2004-05-14 Alexandre Duret-Lutz <adl@src.lip6.fr>
|
||||||
|
|
||||||
|
* wrap/python/buddy.i: Preliminary bindings for FDD and BVEC.
|
||||||
|
|
||||||
* ltltest/inf.cc, ltltest/reduc.cc, ltlvisit/reducform.cc: Fix style.
|
* ltltest/inf.cc, ltltest/reduc.cc, ltlvisit/reducform.cc: Fix style.
|
||||||
* sanity/style.test: More tests.
|
* sanity/style.test: More tests.
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -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
|
Copyright (C) 1996-2003 by Jorn Lind-Nielsen
|
||||||
// et Marie Curie.
|
All rights reserved
|
||||||
//
|
|
||||||
// This file is part of Spot, a model checking library.
|
Permission is hereby granted, without written agreement and without
|
||||||
//
|
license or royalty fees, to use, reproduce, prepare derivative
|
||||||
// Spot is free software; you can redistribute it and/or modify it
|
works, distribute, and display this software and its documentation
|
||||||
// under the terms of the GNU General Public License as published by
|
for any purpose, provided that (1) the above copyright notice and
|
||||||
// the Free Software Foundation; either version 2 of the License, or
|
the following two paragraphs appear in all copies of the source code
|
||||||
// (at your option) any later version.
|
and (2) redistributions, including without limitation binaries,
|
||||||
//
|
reproduce these notices in the supporting documentation. Substantial
|
||||||
// Spot is distributed in the hope that it will be useful, but WITHOUT
|
modifications to this software may be copyrighted by their authors
|
||||||
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
|
and need not follow the licensing terms described here, provided
|
||||||
// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
|
that the new terms are clearly indicated in all files where they apply.
|
||||||
// License for more details.
|
|
||||||
//
|
IN NO EVENT SHALL JORN LIND-NIELSEN, OR DISTRIBUTORS OF THIS
|
||||||
// You should have received a copy of the GNU General Public License
|
SOFTWARE BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL,
|
||||||
// along with Spot; see the file COPYING. If not, write to the Free
|
INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS
|
||||||
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
|
SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE AUTHORS OR ANY OF THE
|
||||||
// 02111-1307, USA.
|
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
|
%module buddy
|
||||||
|
|
||||||
|
|
@ -26,6 +37,8 @@
|
||||||
%{
|
%{
|
||||||
#include <sstream>
|
#include <sstream>
|
||||||
#include "bdd.h"
|
#include "bdd.h"
|
||||||
|
#include "fdd.h"
|
||||||
|
#include "bvec.h"
|
||||||
%}
|
%}
|
||||||
|
|
||||||
struct bdd
|
struct bdd
|
||||||
|
|
@ -157,3 +170,112 @@ extern const bdd bddtrue;
|
||||||
bdd __neg__(void) { return !*self; }
|
bdd __neg__(void) { return !*self; }
|
||||||
|
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/************************************************************************/
|
||||||
|
|
||||||
|
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];
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue