Searched refs:varset (Results 1 - 8 of 8) sorted by relevance

/seL4-l4v-master/HOL4/examples/muddy/
H A Dbdd.sig213 [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 Dbdd.sml146 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 Dfdd.c818 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 Dkernel.c1429 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 Dbdd.h666 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 Dbddop.c2351 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 Dmuddy.c471 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 Dmain.sml53 | SOME varset => if not (Binaryset.isEmpty varset) then SOME s
75 | SOME varset =>
77 (separate " " (map printmv (Binaryset.listItems varset)))))

Completed in 153 milliseconds