1 // -*- coding: utf-8 -*- 2 // Copyright (C) 2010, 2011, 2012, 2014, 2016, 2021 Laboratoire de 3 // 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 // et Marie Curie. 7 // 8 // This file is part of Spot, a model checking library. 9 // 10 // Spot is free software; you can redistribute it and/or modify it 11 // under the terms of the GNU General Public License as published by 12 // the Free Software Foundation; either version 3 of the License, or 13 // (at your option) any later version. 14 // 15 // Spot is distributed in the hope that it will be useful, but WITHOUT 16 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY 17 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public 18 // License for more details. 19 // 20 // You should have received a copy of the GNU General Public License 21 // along with this program. If not, see <http://www.gnu.org/licenses/>. 22 23 // This is derived from Buddy's headers, distributed with the 24 // following license: 25 26 /*======================================================================== 27 Copyright (C) 1996-2003 by Jorn Lind-Nielsen 28 All rights reserved 29 30 Permission is hereby granted, without written agreement and without 31 license or royalty fees, to use, reproduce, prepare derivative 32 works, distribute, and display this software and its documentation 33 for any purpose, provided that (1) the above copyright notice and 34 the following two paragraphs appear in all copies of the source code 35 and (2) redistributions, including without limitation binaries, 36 reproduce these notices in the supporting documentation. Substantial 37 modifications to this software may be copyrighted by their authors 38 and need not follow the licensing terms described here, provided 39 that the new terms are clearly indicated in all files where they apply. 40 41 IN NO EVENT SHALL JORN LIND-NIELSEN, OR DISTRIBUTORS OF THIS 42 SOFTWARE BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL, 43 INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS 44 SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE AUTHORS OR ANY OF THE 45 ABOVE PARTIES HAVE BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. 46 47 JORN LIND-NIELSEN SPECIFICALLY DISCLAIM ANY WARRANTIES, INCLUDING, 48 BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND 49 FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS 50 ON AN "AS IS" BASIS, AND THE AUTHORS AND DISTRIBUTORS HAVE NO 51 OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR 52 MODIFICATIONS. 53 ========================================================================*/ 54 55 %{ 56 // Workaround for SWIG 2.0.2 using ptrdiff_t but not including cstddef. 57 // It matters with g++ 4.6. 58 #include <cstddef> 59 %} 60 61 %module buddy 62 63 %include "std_string.i" 64 65 %{ 66 #include <sstream> 67 #include "bddx.h" 68 #include "fddx.h" 69 #include "bvecx.h" 70 %} 71 72 %typemap(in) (int* input_buf, int input_buf_size) { 73 if (!PySequence_Check($input)) 74 { 75 PyErr_SetString(PyExc_ValueError, "Expected a sequence"); 76 return 0; 77 } 78 $2 = PySequence_Length($input); 79 $1 = (int*) malloc($2 * sizeof(int)); 80 for (int i = 0; i < $2; ++i) 81 { 82 PyObject* o = PySequence_GetItem($input, i); 83 if (PyInt_Check(o)) 84 { 85 $1[i] = PyInt_AsLong(o); 86 } 87 else 88 { 89 PyErr_SetString(PyExc_ValueError, 90 "Sequence elements must be integers"); 91 return 0; 92 } 93 } 94 } 95 %typemap(freearg) (int* input_buf, int input_buf_size) { 96 if ($1) 97 free($1); 98 } 99 100 101 %inline { 102 struct const_int_ptr 103 { const_int_ptrconst_int_ptr104 const_int_ptr(const int* ptr) 105 : ptr(ptr) 106 { 107 } 108 const int* ptr; 109 }; 110 } 111 112 %extend const_int_ptr { 113 int __getitem__(int i)114 __getitem__(int i) 115 { 116 return self->ptr[i]; 117 } 118 } 119 120 struct bdd 121 { 122 int id(void) const; 123 }; 124 125 int bdd_init(int, int); 126 void bdd_done(void); 127 int bdd_setvarnum(int); 128 int bdd_extvarnum(int); 129 int bdd_isrunning(void); 130 int bdd_setmaxnodenum(int); 131 int bdd_setmaxincrease(int); 132 int bdd_setminfreenodes(int); 133 int bdd_getnodenum(void); 134 int bdd_getallocnum(void); 135 char* bdd_versionstr(void); 136 int bdd_versionnum(void); 137 void bdd_fprintstat(FILE *); 138 void bdd_printstat(void); 139 const char *bdd_errstring(int); 140 void bdd_clear_error(void); 141 142 bdd bdd_ithvar(int v); 143 bdd bdd_nithvar(int v); 144 int bdd_var(const bdd &r); 145 bdd bdd_low(const bdd &r); 146 bdd bdd_high(const bdd &r); 147 int bdd_scanset(const bdd &r, int *&v, int &n); 148 bdd bdd_makeset(int *v, int n); 149 int bdd_setbddpair(bddPair *p, int ov, const bdd &nv); 150 bdd bdd_replace(const bdd &r, bddPair *p); 151 bdd bdd_compose(const bdd &f, const bdd &g, int v); 152 bdd bdd_veccompose(const bdd &f, bddPair *p); 153 bdd bdd_restrict(const bdd &r, const bdd &var); 154 bdd bdd_constrain(const bdd &f, const bdd &c); 155 bdd bdd_simplify(const bdd &d, const bdd &b); 156 bdd bdd_ibuildcube(int v, int w, int *a); 157 bdd bdd_not(const bdd &r); 158 bdd bdd_apply(const bdd &l, const bdd &r, int op); 159 bdd bdd_and(const bdd &l, const bdd &r); 160 bdd bdd_or(const bdd &l, const bdd &r); 161 bdd bdd_xor(const bdd &l, const bdd &r); 162 bdd bdd_imp(const bdd &l, const bdd &r); 163 bdd bdd_biimp(const bdd &l, const bdd &r); 164 bdd bdd_setxor(const bdd &l, const bdd &r); 165 int bdd_implies(const bdd &l, const bdd &r); 166 bdd bdd_ite(const bdd &f, const bdd &g, const bdd &h); 167 bdd bdd_exist(const bdd &r, const bdd &var); 168 bdd bdd_existcomp(const bdd &r, const bdd &var); 169 bdd bdd_forall(const bdd &r, const bdd &var); 170 bdd bdd_forallcomp(const bdd &r, const bdd &var); 171 bdd bdd_unique(const bdd &r, const bdd &var); 172 bdd bdd_uniquecomp(const bdd &r, const bdd &var); 173 bdd bdd_appex(const bdd &l, const bdd &r, int op, const bdd &var); 174 bdd bdd_appexcomp(const bdd &l, const bdd &r, int op, const bdd &var); 175 bdd bdd_appall(const bdd &l, const bdd &r, int op, const bdd &var); 176 bdd bdd_appallcomp(const bdd &l, const bdd &r, int op, const bdd &var); 177 bdd bdd_appuni(const bdd &l, const bdd &r, int op, const bdd &var); 178 bdd bdd_appunicomp(const bdd &l, const bdd &r, int op, const bdd &var); 179 bdd bdd_support(const bdd &r); 180 bdd bdd_satone(const bdd &r); 181 bdd bdd_satoneset(const bdd &r, const bdd &var, const bdd &pol); 182 bdd bdd_fullsatone(const bdd &r); 183 void bdd_allsat(const bdd &r, bddallsathandler handler); 184 double bdd_satcount(const bdd &r); 185 double bdd_satcountset(const bdd &r, const bdd &varset); 186 double bdd_satcountln(const bdd &r); 187 double bdd_satcountlnset(const bdd &r, const bdd &varset); 188 int bdd_nodecount(const bdd &r); 189 int* bdd_varprofile(const bdd &r); 190 double bdd_pathcount(const bdd &r); 191 int bdd_have_common_assignment(const bdd &l, const bdd &r); 192 int bdd_is_cube(const bdd &b); 193 void bdd_fprinttable(FILE *file, const bdd &r); 194 void bdd_printtable(const bdd &r); 195 void bdd_fprintset(FILE *file, const bdd &r); 196 void bdd_printset(const bdd &r); 197 void bdd_printdot(const bdd &r); 198 void bdd_fprintdot(FILE* ofile, const bdd &r); 199 int bdd_fnprintdot(char* fname, const bdd &r); 200 int bdd_fnsave(char *fname, const bdd &r); 201 int bdd_save(FILE *ofile, const bdd &r); 202 int bdd_fnload(char *fname, bdd &r); 203 int bdd_load(FILE *ifile, bdd &r); 204 int bdd_addvarblock(const bdd &v, int f); 205 206 extern const bdd bddfalse; 207 extern const bdd bddtrue; 208 209 #define bddop_and 0 210 #define bddop_xor 1 211 #define bddop_or 2 212 #define bddop_nand 3 213 #define bddop_nor 4 214 #define bddop_imp 5 215 #define bddop_biimp 6 216 #define bddop_diff 7 217 #define bddop_less 8 218 #define bddop_invimp 9 219 220 #define BDD_REORDER_NONE 0 221 #define BDD_REORDER_WIN2 1 222 #define BDD_REORDER_WIN2ITE 2 223 #define BDD_REORDER_SIFT 3 224 #define BDD_REORDER_SIFTITE 4 225 #define BDD_REORDER_WIN3 5 226 #define BDD_REORDER_WIN3ITE 6 227 #define BDD_REORDER_RANDOM 7 228 229 %extend bdd { 230 // For Python 2.0 __cmp__(bdd * b)231 int __cmp__(bdd* b) { return b->id() - self->id(); } 232 233 // For Python 2.1+ and Python 3 __le__(bdd * b)234 bool __le__(bdd* b) { return self->id() <= b->id(); } __lt__(bdd * b)235 bool __lt__(bdd* b) { return self->id() < b->id(); } __eq__(bdd * b)236 bool __eq__(bdd* b) { return self->id() == b->id(); } __ne__(bdd * b)237 bool __ne__(bdd* b) { return self->id() != b->id(); } __ge__(bdd * b)238 bool __ge__(bdd* b) { return self->id() >= b->id(); } __gt__(bdd * b)239 bool __gt__(bdd* b) { return self->id() > b->id(); } 240 __hash__()241 size_t __hash__() { return self->id(); } 242 243 std::string __str__(void)244 __str__(void) 245 { 246 std::ostringstream res; 247 res << "bdd(id=" << self->id() << ")"; 248 return res.str(); 249 } 250 __and__(bdd & other)251 bdd __and__(bdd& other) { return *self & other; } __xor__(bdd & other)252 bdd __xor__(bdd& other) { return *self ^ other; } __or__(bdd & other)253 bdd __or__(bdd& other) { return *self | other; } __rshift__(bdd & other)254 bdd __rshift__(bdd& other) { return *self >> other; } __lshift__(bdd & other)255 bdd __lshift__(bdd& other) { return *self << other; } __sub__(bdd & other)256 bdd __sub__(bdd& other) { return *self - other; } __neg__(void)257 bdd __neg__(void) { return !*self; } 258 259 } 260 261 /************************************************************************/ 262 263 int fdd_extdomain(int* input_buf, int input_buf_size); 264 int fdd_overlapdomain(int, int); 265 void fdd_clearall(void); 266 int fdd_domainnum(void); 267 int fdd_domainsize(int); 268 int fdd_varnum(int); 269 const_int_ptr fdd_vars(int); 270 bdd fdd_ithvar(int, int); 271 int fdd_scanvar(bdd, int); 272 int* fdd_scanallvar(bdd); 273 bdd fdd_ithset(int); 274 bdd fdd_domain(int); 275 bdd fdd_equals(int, int); 276 void fdd_printset(bdd); 277 void fdd_fprintset(FILE*, bdd); 278 int fdd_scanset(const bdd &, int *&, int &); 279 bdd fdd_makeset(int*, int); 280 int fdd_intaddvarblock(int, int, int); 281 int fdd_setpair(bddPair*, int, int); 282 int fdd_setpairs(bddPair*, int*, int*, int); 283 284 /************************************************************************/ 285 286 bvec bvec_copy(bvec v); 287 bvec bvec_true(int bitnum); 288 bvec bvec_false(int bitnum); 289 bvec bvec_con(int bitnum, int val); 290 bvec bvec_var(int bitnum, int offset, int step); 291 bvec bvec_varfdd(int var); 292 bvec bvec_varvec(int bitnum, int *var); 293 bvec bvec_coerce(int bitnum, bvec v); 294 int bvec_isconst(bvec e); 295 int bvec_val(bvec e); 296 bvec bvec_map1(const bvec&, bdd (*fun)(const bdd &)); 297 bvec bvec_map2(const bvec&, const bvec&, bdd (*fun)(const bdd &, const bdd &)); 298 bvec bvec_map3(const bvec&, const bvec&, const bvec &, 299 bdd (*fun)(const bdd &, const bdd &, const bdd &)); 300 301 bvec bvec_add(bvec left, bvec right); 302 bvec bvec_sub(bvec left, bvec right); 303 bvec bvec_mulfixed(bvec e, int c); 304 bvec bvec_mul(bvec left, bvec right); 305 int bvec_divfixed(const bvec &, int c, bvec &, bvec &); 306 int bvec_div(const bvec &, const bvec &, bvec &, bvec &); 307 bvec bvec_ite(bdd a, bvec b, bvec c); 308 bvec bvec_shlfixed(bvec e, int pos, bdd c); 309 bvec bvec_shl(bvec l, bvec r, bdd c); 310 bvec bvec_shrfixed(bvec e, int pos, bdd c); 311 bvec bvec_shr(bvec l, bvec r, bdd c); 312 bdd bvec_lth(bvec left, bvec right); 313 bdd bvec_lte(bvec left, bvec right); 314 bdd bvec_gth(bvec left, bvec right); 315 bdd bvec_gte(bvec left, bvec right); 316 bdd bvec_equ(bvec left, bvec right); 317 bdd bvec_neq(bvec left, bvec right); 318 319 class bvec 320 { 321 public: 322 bvec(void); 323 bvec(int bitnum); 324 bvec(int bitnum, int val); 325 bvec(const bvec &v); 326 ~bvec(void); 327 328 void set(int i, const bdd &b); 329 int bitnum(void) const; 330 int empty(void) const; 331 bvec operator=(const bvec &src); 332 333 bvec operator&(const bvec &a) const; 334 bvec operator^(const bvec &a) const; 335 bvec operator|(const bvec &a) const; 336 bvec operator!(void) const; 337 bvec operator<<(int a) const; 338 bvec operator<<(const bvec &a) const; 339 bvec operator>>(int a) const; 340 bvec operator>>(const bvec &a) const; 341 bvec operator+(const bvec &a) const; 342 bvec operator-(const bvec &a) const; 343 bvec operator*(int a) const; 344 bvec operator*(const bvec a) const; 345 bdd operator<(const bvec &a) const; 346 bdd operator<=(const bvec &a) const; 347 bdd operator>(const bvec &a) const; 348 bdd operator>=(const bvec &a) const; 349 bdd operator==(const bvec &a) const; 350 bdd operator!=(const bvec &a) const; 351 }; 352 353 354 %extend bvec { 355 std::string __str__(void)356 __str__(void) 357 { 358 std::ostringstream res; 359 res << "bvec(bitnum=" << self->bitnum() << ")"; 360 return res.str(); 361 } 362 363 bdd __getitem__(int i)364 __getitem__(int i) 365 { 366 return (*self)[i]; 367 } 368 } 369