1/*======================================================================== 2 Copyright (C) 1996-2001 by Jorn Lind-Nielsen 3 All rights reserved 4 5 Permission is hereby granted, without written agreement and without 6 license or royalty fees, to use, reproduce, prepare derivative 7 works, distribute, and display this software and its documentation 8 for any purpose, provided that (1) the above copyright notice and 9 the following two paragraphs appear in all copies of the source code 10 and (2) redistributions, including without limitation binaries, 11 reproduce these notices in the supporting documentation. Substantial 12 modifications to this software may be copyrighted by their authors 13 and need not follow the licensing terms described here, provided 14 that the new terms are clearly indicated in all files where they apply. 15 16 IN NO EVENT SHALL JORN LIND-NIELSEN, OR DISTRIBUTORS OF THIS 17 SOFTWARE BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL, 18 INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS 19 SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE AUTHORS OR ANY OF THE 20 ABOVE PARTIES HAVE BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. 21 22 JORN LIND-NIELSEN SPECIFICALLY DISCLAIM ANY WARRANTIES, INCLUDING, 23 BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND 24 FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS 25 ON AN "AS IS" BASIS, AND THE AUTHORS AND DISTRIBUTORS HAVE NO 26 OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR 27 MODIFICATIONS. 28========================================================================*/ 29 30/************************************************************************* 31 $Header$ 32 FILE: bvec.h 33 DESCR: Boolean (BDD) vector handling 34 AUTH: Jorn Lind 35 DATE: (C) may 1999 36*************************************************************************/ 37 38#ifndef _BVEC_H 39#define _BVEC_H 40 41#include "fdd.h" 42 43 /* Boolean (BDD) vector */ 44/* 45NAME {* bvec *} 46SECTION {* bvec *} 47SHORT {* A boolean vector *} 48PROTO {* typedef struct s_bvec 49{ 50 int bitnum; 51 BDD *bitvec; 52} BVEC; 53 54typedef BVEC bvec; *} 55DESCR {* This data structure is used to store boolean vectors. The field 56 {\tt bitnum} is the number of elements in the vector and the 57 field {\tt bitvec} contains the actual BDDs in the vector. 58 The C++ version of {\tt bvec} is documented at the beginning of 59 this document *} 60*/ 61typedef struct s_bvec 62{ 63 int bitnum; 64 BDD *bitvec; 65} BVEC; 66 67#ifndef CPLUSPLUS 68typedef BVEC bvec; 69#endif 70 71 72#ifdef CPLUSPLUS 73extern "C" { 74#endif 75 76 /* Prototypes for bvec.c */ 77extern BVEC bvec_copy(BVEC v); 78extern BVEC bvec_true(int bitnum); 79extern BVEC bvec_false(int bitnum); 80extern BVEC bvec_con(int bitnum, int val); 81extern BVEC bvec_var(int bitnum, int offset, int step); 82extern BVEC bvec_varfdd(int var); 83extern BVEC bvec_varvec(int bitnum, int *var); 84extern BVEC bvec_coerce(int bitnum, BVEC v); 85extern int bvec_isconst(BVEC e); 86extern int bvec_val(BVEC e); 87extern void bvec_free(BVEC v); 88extern BVEC bvec_addref(BVEC v); 89extern BVEC bvec_delref(BVEC v); 90extern BVEC bvec_map1(BVEC a, BDD (*fun)(BDD)); 91extern BVEC bvec_map2(BVEC a, BVEC b, BDD (*fun)(BDD,BDD)); 92extern BVEC bvec_map3(BVEC a, BVEC b, BVEC c, BDD (*fun)(BDD,BDD,BDD)); 93extern BVEC bvec_add(BVEC left, BVEC right); 94extern BVEC bvec_sub(BVEC left, BVEC right); 95extern BVEC bvec_mulfixed(BVEC e, int c); 96extern BVEC bvec_mul(BVEC left, BVEC right); 97extern int bvec_divfixed(BVEC e, int c, BVEC *res, BVEC *rem); 98extern int bvec_div(BVEC left, BVEC right, BVEC *res, BVEC *rem); 99extern BVEC bvec_shlfixed(BVEC e, int pos, BDD c); 100extern BVEC bvec_shl(BVEC l, BVEC r, BDD c); 101extern BVEC bvec_shrfixed(BVEC e, int pos, BDD c); 102extern BVEC bvec_shr(BVEC l, BVEC r, BDD c); 103extern BDD bvec_lth(BVEC left, BVEC right); 104extern BDD bvec_lte(BVEC left, BVEC right); 105extern BDD bvec_gth(BVEC left, BVEC right); 106extern BDD bvec_gte(BVEC left, BVEC right); 107extern BDD bvec_equ(BVEC left, BVEC right); 108extern BDD bvec_neq(BVEC left, BVEC right); 109 110#ifdef CPLUSPLUS 111} 112#endif 113 114 115/************************************************************************* 116 If this file is included from a C++ compiler then the following 117 classes, wrappers and hacks are supplied. 118*************************************************************************/ 119#ifdef CPLUSPLUS 120 121/*=== User BVEC class ==================================================*/ 122 123class bvec 124{ 125 public: 126 127 bvec(void) { roots.bitvec=NULL; roots.bitnum=0; } 128 bvec(int bitnum) { roots=bvec_false(bitnum); } 129 bvec(int bitnum, int val) { roots=bvec_con(bitnum,val); } 130 bvec(const bvec &v) { roots=bvec_copy(v.roots); } 131 ~bvec(void) { bvec_free(roots); } 132 133 void set(int i, const bdd &b); 134 bdd operator[](int i) const { return roots.bitvec[i]; } 135 int bitnum(void) const { return roots.bitnum; } 136 int empty(void) const { return roots.bitnum==0; } 137 bvec operator=(const bvec &src); 138 139private: 140 BVEC roots; 141 142 bvec(const BVEC &v) { roots=v; } /* NOTE: Must be a shallow copy! */ 143 144 friend bvec bvec_truepp(int bitnum); 145 friend bvec bvec_falsepp(int bitnum); 146 friend bvec bvec_conpp(int bitnum, int val); 147 friend bvec bvec_varpp(int bitnum, int offset, int step); 148 friend bvec bvec_varfddpp(int var); 149 friend bvec bvec_varvecpp(int bitnum, int *var); 150 friend bvec bvec_coerce(int bitnum, const bvec &v); 151 friend int bvec_isconst(const bvec &e); 152 friend int bvec_val(const bvec &e); 153 friend bvec bvec_copy(const bvec &v); 154 friend bvec bvec_map1(const bvec &a, 155 bdd (*fun)(const bdd &)); 156 friend bvec bvec_map2(const bvec &a, const bvec &b, 157 bdd (*fun)(const bdd &, const bdd &)); 158 friend bvec bvec_map3(const bvec &a, const bvec &b, const bvec &c, 159 bdd (*fun)(const bdd &, const bdd &, const bdd &)); 160 friend bvec bvec_add(const bvec &left, const bvec &right); 161 friend bvec bvec_sub(const bvec &left, const bvec &right); 162 friend bvec bvec_mulfixed(const bvec &e, int c); 163 friend bvec bvec_mul(const bvec &left, const bvec &right); 164 friend int bvec_divfixed(const bvec &e, int c, bvec &res, bvec &rem); 165 friend int bvec_div(const bvec &l, const bvec &r, bvec &res, bvec &rem); 166 friend bvec bvec_shlfixed(const bvec &e, int pos, const bdd &c); 167 friend bvec bvec_shl(const bvec &left, const bvec &right, const bdd &c); 168 friend bvec bvec_shrfixed(const bvec &e, int pos, const bdd &c); 169 friend bvec bvec_shr(const bvec &left, const bvec &right, const bdd &c); 170 friend bdd bvec_lth(const bvec &left, const bvec &right); 171 friend bdd bvec_lte(const bvec &left, const bvec &right); 172 friend bdd bvec_gth(const bvec &left, const bvec &right); 173 friend bdd bvec_gte(const bvec &left, const bvec &right); 174 friend bdd bvec_equ(const bvec &left, const bvec &right); 175 friend bdd bvec_neq(const bvec &left, const bvec &right); 176 177public: 178 bvec operator&(const bvec &a) const { return bvec_map2(*this, a, bdd_and); } 179 bvec operator^(const bvec &a) const { return bvec_map2(*this, a, bdd_xor); } 180 bvec operator|(const bvec &a) const { return bvec_map2(*this, a, bdd_or); } 181 bvec operator!(void) const { return bvec_map1(*this, bdd_not); } 182 bvec operator<<(int a) const { return bvec_shlfixed(*this,a,bddfalse); } 183 bvec operator<<(const bvec &a) const { return bvec_shl(*this,a,bddfalse); } 184 bvec operator>>(int a) const { return bvec_shrfixed(*this,a,bddfalse); } 185 bvec operator>>(const bvec &a) const { return bvec_shr(*this,a,bddfalse); } 186 bvec operator+(const bvec &a) const { return bvec_add(*this, a); } 187 bvec operator-(const bvec &a) const { return bvec_sub(*this, a); } 188 bvec operator*(int a) const { return bvec_mulfixed(*this, a); } 189 bvec operator*(const bvec a) const { return bvec_mul(*this, a); } 190 bdd operator<(const bvec &a) const { return bvec_lth(*this, a); } 191 bdd operator<=(const bvec &a) const { return bvec_lte(*this, a); } 192 bdd operator>(const bvec &a) const { return bvec_gth(*this, a); } 193 bdd operator>=(const bvec &a) const { return bvec_gte(*this, a); } 194 bdd operator==(const bvec &a) const { return bvec_equ(*this, a); } 195 bdd operator!=(const bvec &a) const { return bvec_neq(*this, a); } 196}; 197 198 199inline bvec bvec_truepp(int bitnum) 200{ return bvec_true(bitnum); } 201 202inline bvec bvec_falsepp(int bitnum) 203{ return bvec_false(bitnum); } 204 205inline bvec bvec_conpp(int bitnum, int val) 206{ return bvec_con(bitnum, val); } 207 208inline bvec bvec_varpp(int bitnum, int offset, int step) 209{ return bvec_var(bitnum, offset, step); } 210 211inline bvec bvec_varfddpp(int var) 212{ return bvec_varfdd(var); } 213 214inline bvec bvec_varvecpp(int bitnum, int *var) 215{ return bvec_varvec(bitnum, var); } 216 217inline bvec bvec_coerce(int bitnum, const bvec &v) 218{ return bvec_coerce(bitnum, v.roots); } 219 220inline int bvec_isconst(const bvec &e) 221{ return bvec_isconst(e.roots); } 222 223inline int bvec_val(const bvec &e) 224{ return bvec_val(e.roots); } 225 226inline bvec bvec_copy(const bvec &v) 227{ return bvec_copy(v.roots); } 228 229inline bvec bvec_add(const bvec &left, const bvec &right) 230{ return bvec_add(left.roots, right.roots); } 231 232inline bvec bvec_sub(const bvec &left, const bvec &right) 233{ return bvec_sub(left.roots, right.roots); } 234 235inline bvec bvec_mulfixed(const bvec &e, int c) 236{ return bvec_mulfixed(e.roots, c); } 237 238inline bvec bvec_mul(const bvec &left, const bvec &right) 239{ return bvec_mul(left.roots, right.roots); } 240 241inline int bvec_divfixed(const bvec &e, int c, bvec &res, bvec &rem) 242{ return bvec_divfixed(e.roots, c, &res.roots, &rem.roots); } 243 244inline int bvec_div(const bvec &l, const bvec &r, bvec &res, bvec &rem) 245{ return bvec_div(l.roots, r.roots, &res.roots, &rem.roots); } 246 247inline bvec bvec_shlfixed(const bvec &e, int pos, const bdd &c) 248{ return bvec_shlfixed(e.roots, pos, c.root); } 249 250inline bvec bvec_shl(const bvec &left, const bvec &right, const bdd &c) 251{ return bvec_shl(left.roots, right.roots, c.root); } 252 253inline bvec bvec_shrfixed(const bvec &e, int pos, const bdd &c) 254{ return bvec_shrfixed(e.roots, pos, c.root); } 255 256inline bvec bvec_shr(const bvec &left, const bvec &right, const bdd &c) 257{ return bvec_shr(left.roots, right.roots, c.root); } 258 259inline bdd bvec_lth(const bvec &left, const bvec &right) 260{ return bvec_lth(left.roots, right.roots); } 261 262inline bdd bvec_lte(const bvec &left, const bvec &right) 263{ return bvec_lte(left.roots, right.roots); } 264 265inline bdd bvec_gth(const bvec &left, const bvec &right) 266{ return bvec_gth(left.roots, right.roots); } 267 268inline bdd bvec_gte(const bvec &left, const bvec &right) 269{ return bvec_gte(left.roots, right.roots); } 270 271inline bdd bvec_equ(const bvec &left, const bvec &right) 272{ return bvec_equ(left.roots, right.roots); } 273 274inline bdd bvec_neq(const bvec &left, const bvec &right) 275{ return bvec_neq(left.roots, right.roots); } 276 277 278 /* Hack to allow for overloading */ 279#define bvec_var(a,b,c) bvec_varpp(a,b,c) 280#define bvec_varfdd(a) bvec_varfddpp(a) 281#define bvec_varvec(a,b) bvec_varvecpp(a,b) 282#define bvec_true(a) bvec_truepp(a) 283#define bvec_false(a) bvec_falsepp(a) 284#define bvec_con(a,b) bvec_conpp((a),(b)) 285 286 287#endif /* CPLUSPLUS */ 288 289#endif /* _BVEC_H */ 290 291/* EOF */ 292