Searched refs:bitnum (Results 1 - 5 of 5) sorted by relevance
| /seL4-l4v-10.1.1/HOL4/examples/muddy/muddyC/buddy/src/ |
| H A D | fdd.h | 118 inline bdd* fdd_conpp(int bitnum, int var)
119 { return fdd_transfer( bitnum, fdd_con(bitnum, var) ); }
121 inline bdd* fdd_varpp(int bitnum, int var)
122 { return fdd_transfer( bitnum, fdd_var(bitnum, var) ); }
124 extern int fdd_isconst(int bitnum, bdd *e);
125 extern int fdd_val(int bitnum, bdd *e);
127 inline bdd* fdd_add(int bitnum, bdd *left, bdd *right)
128 { return fdd_termopr(bitnum, lef
[all...] |
| H A D | bvec.c | 41 #define DEFAULT(v) { v.bitnum=0; v.bitvec=NULL; }
46 static bvec bvec_build(int bitnum, int isTrue) argument
51 vec.bitvec = NEW(BDD,bitnum);
52 vec.bitnum = bitnum;
56 vec.bitnum = 0;
60 for (n=0 ; n<bitnum ; n++)
73 int bitnum=0;
78 bitnum++;
81 return bitnum;
124 bvec_true(int bitnum) argument
140 bvec_false(int bitnum) argument
157 bvec_con(int bitnum, int val) argument
188 bvec_var(int bitnum, int offset, int step) argument
245 bvec_varvec(int bitnum, int *var) argument
271 bvec_coerce(int bitnum, bvec v) argument
700 int bitnum = left.bitnum + right.bitnum; local
846 int bitnum = left.bitnum + right.bitnum; local
[all...] |
| H A D | bvec.h | 50 int bitnum;
56 {\tt bitnum} is the number of elements in the vector and the
63 int bitnum; member in struct:s_bvec
78 extern BVEC bvec_true(int bitnum);
79 extern BVEC bvec_false(int bitnum);
80 extern BVEC bvec_con(int bitnum, int val);
81 extern BVEC bvec_var(int bitnum, int offset, int step);
83 extern BVEC bvec_varvec(int bitnum, int *var);
84 extern BVEC bvec_coerce(int bitnum, BVEC v);
127 bvec(void) { roots.bitvec=NULL; roots.bitnum
128 bvec(int bitnum) argument
129 bvec(int bitnum, int val) argument
135 int bitnum(void) const { return roots.bitnum; } function in class:bvec
199 bvec_truepp(int bitnum) argument
202 bvec_falsepp(int bitnum) argument
205 bvec_conpp(int bitnum, int val) argument
208 bvec_varpp(int bitnum, int offset, int step) argument
214 bvec_varvecpp(int bitnum, int *var) argument
217 bvec_coerce(int bitnum, const bvec &v) argument
[all...] |
| H A D | cppext.cxx | 549 void bvec::set(int bitnum, const bdd &b) argument
551 bdd_delref(roots.bitvec[bitnum]);
552 roots.bitvec[bitnum] = b.root;
553 bdd_addref(roots.bitvec[bitnum]);
565 res = bvec_false(a.bitnum());
566 for (n=0 ; n < a.bitnum() ; n++)
579 if (a.bitnum() != b.bitnum())
585 res = bvec_false(a.bitnum());
586 for (n=0 ; n < a.bitnum() ;
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/muddy/muddyC/ |
| H A D | muddy.c | 850 t.bitnum=bvecbitnum_val(obj);
863 /* Creation of a bvec makes a finalized pair (mlbdd_finalize, bitnum, bitvec) */
868 bvecbitnum_val(res) = v.bitnum;
|
Completed in 89 milliseconds