Searched refs:varset (Results 1 - 8 of 8) sorted by relevance
/seL4-l4v-master/HOL4/examples/muddy/ |
H A D | bdd.sig | 213 [scanset varset] gives the vector of the variables in varset. 215 [fromSet varset] gives the bdd representing the conjunction of 216 all the variables in varset. 237 [exist varset r] constructs the existential quantification over all 238 the variables in the varset of r. 240 [forall varset r] constructs the universal quantification over all 241 the variables in the varset of r. 243 [appex x y opr varset] equivalent to 'exist varset (appl [all...] |
H A D | bdd.sml | 146 fun appall r1 r2 opr varset = appall_ r1 r2 (opr2i opr) varset 147 fun appex r1 r2 opr varset = appex_ r1 r2 (opr2i opr) varset
|
/seL4-l4v-master/HOL4/examples/muddy/muddyC/buddy/src/ |
H A D | fdd.c | 818 PROTO {* int fdd_scanset(BDD r, int **varset, int *varnum) *} 820 and then stores these in {\tt varset}. {\tt varset} will be set 823 responsibility to free {\tt varset} after use. *} 827 int fdd_scanset(BDD r, int **varset, int *varnum) argument 853 if ((*varset=(int*)malloc(sizeof(int)*num)) == NULL) 865 (*varset)[num++] = n; 883 PROTO {* BDD fdd_makeset(int *varset, int varnum) *} 885 the variable blocks in the array {\tt varset}. The argument 886 {\tt varnum} defines the size of {\tt varset} 890 fdd_makeset(int *varset, int varnum) argument [all...] |
H A D | kernel.c | 1429 int bdd_scanset(BDD r, int **varset, int *varnum) argument 1437 *varset = NULL; 1444 if (((*varset) = (int *)malloc(sizeof(int)*num)) == NULL) 1448 (*varset)[num++] = bddlevel2var[LEVEL(n)]; 1472 BDD bdd_makeset(int *varset, int varnum) argument 1480 tmp = bdd_apply(res, bdd_ithvar(varset[v]), bddop_and);
|
H A D | bdd.h | 666 inline double bdd_satcountset(const bdd &r, const bdd &varset) argument 667 { return bdd_satcountset(r.root, varset.root); } 672 inline double bdd_satcountlnset(const bdd &r, const bdd &varset) argument 673 { return bdd_satcountlnset(r.root, varset.root); }
|
H A D | bddop.c | 2351 double bdd_satcountset(BDD r, BDD varset) *} 2356 set {\tt varset} are considered. This makes the function a 2374 double bdd_satcountset(BDD r, BDD varset) argument 2379 if (ISCONST(varset) || ISZERO(r)) /* empty set */ 2382 for (n=varset ; !ISCONST(n) ; n=HIGH(n)) 2429 double bdd_satcountlnset(BDD r, BDD varset)*} 2438 set {\tt varset} are considered. This makes the function 2458 double bdd_satcountlnset(BDD r, BDD varset) argument 2463 if (ISCONST(varset)) /* empty set */ 2466 for (n=varset ; !ISCONS [all...] |
/seL4-l4v-master/HOL4/examples/muddy/muddyC/ |
H A D | muddy.c | 471 EXTERNML value mlbdd_bdd_scanset(value varset) argument 476 if(bdd_scanset(Bdd_val(varset), &v, &n)) { 500 EXTERNML value mlbdd_bdd_exist(value b1, value varset) /* ML */ argument 502 return mlbdd_make(bdd_exist(Bdd_val(b1),Bdd_val(varset))); 506 EXTERNML value mlbdd_bdd_forall(value b1, value varset) /* ML */ argument 508 return mlbdd_make(bdd_forall(Bdd_val(b1),Bdd_val(varset))); 513 value opr, value varset) /* ML */ 516 Int_val(opr), Bdd_val(varset))); 521 value opr, value varset) /* ML */ 524 Int_val(opr), Bdd_val(varset))); 512 mlbdd_bdd_appall(value left, value right, value opr, value varset) argument 520 mlbdd_bdd_appex(value left, value right, value opr, value varset) argument [all...] |
/seL4-l4v-master/l4v/tools/c-parser/standalone-parser/ |
H A D | main.sml | 53 | SOME varset => if not (Binaryset.isEmpty varset) then SOME s 75 | SOME varset => 77 (separate " " (map printmv (Binaryset.listItems varset)))))
|
Completed in 153 milliseconds