Searched refs:av (Results 1 - 25 of 29) sorted by relevance

12

/seL4-l4v-master/HOL4/examples/muddy/muddyC/buddy/examples/adder/
H A Dadder.cxx180 int test_vector(bdd av, bdd bv, int a, int b) argument
186 bdd resv = av & bv & xout[n];
206 bdd av = setval(a,0); local
209 if (test_vector(av,bv,a,b) == 0)
/seL4-l4v-master/HOL4/examples/muddy/muddyC/buddy/src/
H A Dbddtest.cxx75 int main(int ac, char** av) argument
/seL4-l4v-master/HOL4/examples/muddy/muddyC/buddy/examples/queen/
H A Dqueen.cxx75 int main(int ac, char **av) argument
85 N = atoi(av[1]);
/seL4-l4v-master/HOL4/src/metis/
H A DmlibTerm.sml587 fun fvt av =
590 if null av then mem else (fn v => fn vs => mem v av orelse mem v vs)
601 | fv vs ((av, Atom t ) :: fms) = fv (fvt av vs [t]) fms
602 | fv vs ((av, Not p ) :: fms) = fv vs ((av, p) :: fms)
603 | fv vs ((av, And (p, q) ) :: fms) = fv vs ((av, p) :: (av,
[all...]
H A DmlibOmega.sml51 fun factoid_key (ALT av) = KEY(av, V.length av - 1)
53 fun keyhash (KEY(av, len)) = khash av (SOME len)
82 fun toList (ALT av) = V.foldr op:: [] av
88 ALT av => V.sub(av, V.length av
[all...]
/seL4-l4v-master/HOL4/src/portableML/poly/
H A DIntmap.sml70 fun single_L (a,av,x,T{key=b,value=bv,left=y,right=z,...}) =
71 N(b,bv,N(a,av,x,y),z)
73 fun single_R (b,bv,T{key=a,value=av,left=x,right=y,...},z) =
74 N(a,av,x,N(b,bv,y,z))
76 fun double_L (a,av,w,T{key=c,value=cv,left=T{key=b,value=bv,left=x,right=y,...},right=z,...}) =
77 N(b,bv,N(a,av,w,x),N(c,cv,y,z))
79 fun double_R (c,cv,T{key=a,value=av,left=w,right=T{key=b,value=bv,left=x,right=y,...},...},z) =
80 N(b,bv,N(a,av,w,x),N(c,cv,y,z))
/seL4-l4v-master/HOL4/tools-poly/poly/
H A DBinarymap.sml73 fun single_L (a,av,x,T{key=b,value=bv,left=y,right=z,...}) =
74 N(b,bv,N(a,av,x,y),z)
76 fun single_R (b,bv,T{key=a,value=av,left=x,right=y,...},z) =
77 N(a,av,x,N(b,bv,y,z))
79 fun double_L (a,av,w,T{key=c,value=cv,
82 N(b,bv,N(a,av,w,x),N(c,cv,y,z))
84 fun double_R (c,cv,T{key=a,value=av,left=w,
86 N(b,bv,N(a,av,w,x),N(c,cv,y,z))
/seL4-l4v-master/HOL4/examples/dev/sw/
H A Dint-binary-map.sml86 fun single_L (a,av,x,T{key=b,value=bv,left=y,right=z,...}) =
87 N(b,bv,N(a,av,x,y),z)
89 fun single_R (b,bv,T{key=a,value=av,left=x,right=y,...},z) =
90 N(a,av,x,N(b,bv,y,z))
92 fun double_L (a,av,w,T{key=c,value=cv,left=T{key=b,value=bv,left=x,right=y,...},right=z,...}) =
93 N(b,bv,N(a,av,w,x),N(c,cv,y,z))
95 fun double_R (c,cv,T{key=a,value=av,left=w,right=T{key=b,value=bv,left=x,right=y,...},...},z) =
96 N(b,bv,N(a,av,w,x),N(c,cv,y,z))
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/
H A Dint-binary-map.sml86 fun single_L (a,av,x,T{key=b,value=bv,left=y,right=z,...}) =
87 N(b,bv,N(a,av,x,y),z)
89 fun single_R (b,bv,T{key=a,value=av,left=x,right=y,...},z) =
90 N(a,av,x,N(b,bv,y,z))
92 fun double_L (a,av,w,T{key=c,value=cv,left=T{key=b,value=bv,left=x,right=y,...},right=z,...}) =
93 N(b,bv,N(a,av,w,x),N(c,cv,y,z))
95 fun double_R (c,cv,T{key=a,value=av,left=w,right=T{key=b,value=bv,left=x,right=y,...},...},z) =
96 N(b,bv,N(a,av,w,x),N(c,cv,y,z))
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/util/
H A Dint-binary-map.sml86 fun single_L (a,av,x,T{key=b,value=bv,left=y,right=z,...}) =
87 N(b,bv,N(a,av,x,y),z)
89 fun single_R (b,bv,T{key=a,value=av,left=x,right=y,...},z) =
90 N(a,av,x,N(b,bv,y,z))
92 fun double_L (a,av,w,T{key=c,value=cv,left=T{key=b,value=bv,left=x,right=y,...},right=z,...}) =
93 N(b,bv,N(a,av,w,x),N(c,cv,y,z))
95 fun double_R (c,cv,T{key=a,value=av,left=w,right=T{key=b,value=bv,left=x,right=y,...},...},z) =
96 N(b,bv,N(a,av,w,x),N(c,cv,y,z))
/seL4-l4v-master/HOL4/developers/mlton-srcs/
H A DBinarymap.sml142 fun single_L (a,av,x,T{key=b,value=bv,left=y,right=z,...}) =
143 N(b,bv,N(a,av,x,y),z)
145 fun single_R (b,bv,T{key=a,value=av,left=x,right=y,...},z) =
146 N(a,av,x,N(b,bv,y,z))
148 fun double_L (a,av,w,T{key=c,value=cv,
151 N(b,bv,N(a,av,w,x),N(c,cv,y,z))
153 fun double_R (c,cv,T{key=a,value=av,left=w,
155 N(b,bv,N(a,av,w,x),N(c,cv,y,z))
/seL4-l4v-master/HOL4/src/integer/
H A DOmegaMLShadow.sml41 ALT av => extract(av, 0, SOME (Vector.length av - 1))
44 ALT av => Vector.sub(av, Vector.length av - 1)
47 case f of ALT av => Vector.length av
110 ALT av => Vector.foldri
114 av
[all...]
H A Dint_arithScript.sml826 mn | dx + bqn + vpm /\ d | av - ub )
867 (* m | ax + b /\ n | ux + v ==> d | av - ub *)
889 (* mn | dx + vmp + bnq /\ d | av - ub ==> m | ax + b *)
949 (* mn | dx + vmp + bnq /\ d | av - ub ==> n | ux + v *)
/seL4-l4v-master/HOL4/examples/muddy/muddyC/buddy/examples/calculator/
H A Dparser.y210 int main(int ac, char **av)
214 while ((c=getopt(ac, av, "hg")) != EOF)
230 yyin = fopen(av[optind],"r");
233 cerr << "Could not open file: " << av[optind] << endl;
/seL4-l4v-master/HOL4/src/datatype/
H A DDatatypeSimps.sml148 val (avoid, case_args') = Lib.foldl_map (fn (av, (args, v)) =>
149 let val v' = variant av v in
150 (v' :: av, (args, v')) end) (input_arg'::avoid, case_args)
445 val (_, args') = foldl_map (fn (av, v) => let val v' = variant av v in (v' :: av, v') end) (free_vars_full, args)
/seL4-l4v-master/HOL4/polyml/libpolyml/
H A Dpoly_specific.cpp395 PolyWord *av = (PolyWord*)a; local
397 if ((*av).IsTagged() || (*bv).IsTagged()) return 0; // Shouldn't happen
398 PolyObject *ao = (*av).AsObjPtr(), *bo = (*bv).AsObjPtr();
/seL4-l4v-master/HOL4/examples/HolCheck/
H A DdbgTools.sml21 fun set_pfx s k = foldr (fn (v,av) => if String.isPrefix v k then true else av) false s
H A DmuSyntax.sml468 in List.foldl (fn (_,av) => mk_subs2 av l) mv l end
477 | "RV" => (inst [``:'a``|->prop_type] ``RV ^(List.foldr (fn (sb,av) => if (Term.compare(snd sb,av)=EQUAL)
478 then fst sb else av) (List.hd args) subs)``,l)
H A DcearTools.sml78 val astate = pairSyntax.list_mk_pair(List.tabulate(nabsv,fn i => mk_bool_var("av"^(int_to_string i))))
156 val navn = "av"^(int_to_string(nabsv-1))
252 val vmabs = List.filter (fn (t,_) => (String.size t) >= 3 andalso String.compare("av",String.substring(t,0,2))=EQUAL )
/seL4-l4v-master/isabelle/src/Tools/Metis/src/
H A DTerm.sml241 fun avoid av n = NameSet.member n av;
243 fun variantPrime av = Name.variantPrime {avoid = avoid av};
245 fun variantNum av = Name.variantNum {avoid = avoid av};
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/
H A DTerm.sml241 fun avoid av n = NameSet.member n av;
243 fun variantPrime av = Name.variantPrime {avoid = avoid av};
245 fun variantNum av = Name.variantNum {avoid = avoid av};
/seL4-l4v-master/HOL4/src/IndDef/
H A DInductiveDefinition.sml43 fun variants av [] = []
44 | variants av (h::t) =
45 let val vh = vary av h
46 in vh::variants (vh::av) t
/seL4-l4v-master/graph-refine/
H A Drep_graph.py422 def av (nm, typ, mem_name = None): function in function:GraphSlice.get_loop_pc_env
435 env[(nm, typ)] = av (nm + '_after', typ,
445 pc = mk_smt_expr (av ('pc_of', boolT), boolT)
/seL4-l4v-master/HOL4/src/quotient/examples/
H A Dtactics.sml130 `<|vv`;`<|vsv`;`<|av`;`:==`;`//v`;`<<`]; ();
/seL4-l4v-master/HOL4/src/AI/
H A DaiLib.sml355 val av = Array.sub (arr,a) value
359 Array.update (arr,b,av)

Completed in 158 milliseconds

12