buddy.i 11.6 KB
Newer Older
1 2 3
// -*- coding: utf-8 -*-
// Copyright (C) 2010, 2011, 2012  Laboratoire de Recherche et
// Développement de l'EPITA.
4
// Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
5
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27
// 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.

// This is derived from Buddy's headers, distributed with the
// following license:

28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56
/*========================================================================
	       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.
========================================================================*/

57 58 59 60 61
%{
  // Workaround for SWIG 2.0.2 using ptrdiff_t but not including cstddef.
  // It matters with g++ 4.6.
#include <cstddef>
%}
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
62

63 64 65 66 67 68 69
%module buddy

%include "std_string.i"

%{
#include <sstream>
#include "bdd.h"
70 71
#include "fdd.h"
#include "bvec.h"
72 73
%}

74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121
%typemap(in) (int* input_buf, int input_buf_size) {
  if (!PySequence_Check($input))
    {
      PyErr_SetString(PyExc_ValueError, "Expected a sequence");
      return 0;
    }
  $2 = PySequence_Length($input);
  $1 = (int*) malloc($2 * sizeof(int));
  for (int i = 0; i < $2; ++i)
    {
      PyObject* o = PySequence_GetItem($input, i);
      if (PyInt_Check(o))
        {
          $1[i] = PyInt_AsLong(o);
	}
      else
        {
          PyErr_SetString(PyExc_ValueError,
                          "Sequence elements must be integers");
          return 0;
        }
    }
}
%typemap(freearg) (int* input_buf, int input_buf_size) {
  if ($1)
    free($1);
}


%inline {
  struct const_int_ptr
  {
    const_int_ptr(const int* ptr)
      : ptr(ptr)
    {
    }
    const int* ptr;
  };
}

%extend const_int_ptr {
  int
  __getitem__(int i)
  {
    return self->ptr[i];
  }
}

122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165
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);
166
bdd bdd_setxor(const bdd &l, const bdd &r);
167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228
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 {
229 230 231 232 233 234 235 236 237 238 239
  // For Python 2.0
  int __cmp__(bdd* b) { return b->id() - self->id(); }

  // For Python 2.1+ and Python 3
  bool __le__(bdd* b) { return self->id() <= b->id(); }
  bool __lt__(bdd* b) { return self->id() < b->id(); }
  bool __eq__(bdd* b) { return self->id() == b->id(); }
  bool __ne__(bdd* b) { return self->id() != b->id(); }
  bool __ge__(bdd* b) { return self->id() >= b->id(); }
  bool __gt__(bdd* b) { return self->id() > b->id(); }

240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256

  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; }

257 258 259 260
}

/************************************************************************/

261
int  fdd_extdomain(int* input_buf, int input_buf_size);
262 263 264 265 266
int  fdd_overlapdomain(int, int);
void fdd_clearall(void);
int  fdd_domainnum(void);
int  fdd_domainsize(int);
int  fdd_varnum(int);
267
const_int_ptr fdd_vars(int);
268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366
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];
  }
}