Searched refs:ci (Results 1 - 25 of 36) sorted by relevance

12

/seL4-l4v-master/seL4/src/arch/x86/machine/
H A Dcpu_identification.c37 BOOT_CODE static void x86_cpuid_fill_vendor_string(cpu_identity_t *ci) argument
39 MAY_ALIAS uint32_t *vendor_string32 = (uint32_t *)ci->vendor_string;
41 if (ci == NULL) {
49 ci->vendor_string[X86_CPUID_VENDOR_STRING_MAXLENGTH] = '\0';
56 BOOT_CODE static void x86_cpuid_intel_identity_initialize(cpu_identity_t *ci, argument
66 ci->display.family = original.family;
68 ci->display.family = ci->display.extended_family + original.family;
77 * if (ci->display.family == 0x06 || ci
97 x86_cpuid_amd_identity_initialize(cpu_identity_t *ci, struct family_model original) argument
118 cpu_identity_t *ci = x86_cpuid_get_identity(); local
[all...]
/seL4-l4v-master/HOL4/src/HolSat/sat_solvers/zc2hs/
H A Dzc2hs.cpp309 int addChain(vector<int>& resolvents, int ci) { argument
321 units.insert(make_pair(res[0],ci));
332 int addVChain(int vid, bool sgn, int ante, int ci) { argument
345 units.insert(make_pair(p,ci));
366 void addRoot(int ci) { argument
368 roots[ci].copyTo(clauses.last());
369 c2c[ci] = P.addRoot(clauses.last(),ci+1)-1;
370 pclauses[ci].first=DONE;
373 void build_clause(int ci) { argument
383 build_var(int ci) argument
397 int ci = vars[var(cc[ii])]; local
408 build(int ci) argument
440 int ci = vars[var(cc[ii])]; local
[all...]
/seL4-l4v-master/HOL4/src/HolSat/
H A DminisatResolve.sml40 fun dualise lfn orc clauseth ci =
59 handle Subscript => failwith("dualise"^(int_to_string (ci))^"\n")
77 fun prepareRootClause lfn orc clauseth cl ci =
79 val th = dualise lfn orc clauseth ci
80 val _ = Dynarray.update(cl,ci,th)
83 (* will return clause thm at index ci *)
84 fun getClause cl ci = Dynarray.sub(cl,ci)
85 handle Subscript => failwith("getClause"^(int_to_string (ci))^"\n")
115 val res = List.foldl (fn ((vi,ci),t
[all...]
H A Ddpll.sml66 fun CoreDPLL initial_th = let (* [ci] |- cnf *)
67 fun recurse th = let (* [assigns, ci] |- curr *)
77 (*[assigns,v=T,ci]|- curr[T/v],[assigns,v=F,ci]|- curr[F/v]*)
84 (* [assignsr\v,assignsl\v,ci] |- F *)
90 recurse initial_th (* [ci] |- F *)
94 (* clauses is (ci,[~t] |- ci') pairs, where ci' is expanded ci *)
[all...]
H A DminisatParse.sml88 else let val ci = id-(sat_getint fin) value
89 in loop ((v,ci)::acc) (len+1) end
H A DdimacsTools.sml161 fun foldthis (ci,c,svm) = let
169 Array.update(numclauses,ci,l);
/seL4-l4v-master/HOL4/Manual/Translations/IT/Tutorial/
H A Dcombin.tex190 nasconderemo dalla vista prima di iniziare. Evitiamo cos� messaggi che ci dicono
260 In altre parole, un sistema ha un $R$-forma normale in $x$ se non ci sono
408 propriet� diamante per $R$ ci garantir� l'esistenza di $r$,
469 Eseguiamo uno strip del goal il pi� possibile con l'obiettivo di rendere ci� che
543 un singolo passo-$R$ tra $z$ e $v$ abbiamo anche quello allo stesso modo. Tutto ci�
767 $x\;u$ pu� essere trasformata in $y\;v$ se ci sono trasformazioni
949 Qui ci sono quattro congiunti, e dovrebbe essere chiaro che nessuno tranne
956 i rami. Se la nostra tattica fallisce sul ramo \#2, come ci aspettiamo,
957 \texttt{TRY} ci protegger� da questo fallimento e ci permette
[all...]
H A Dmore-examples.tex35 in azione. In primo piano ci sono una semantica operazionale per un piccolo linguaggio
H A Deuclid.tex87 che ci sono infiniti numeri primi. Se fossimo arrivati ad affrontare questo
120 Spesso comunque, ci rimane un goal che richiede un p� di studio prima di
191 Il manager di dimostrazione ci dice che c'� soltanto una dimostrazione da gestire, e
245 che teoricamente � un albero!} ma ci� non importa, dal momento che il goalstack � stato
583 tutto ci� che rimane da fare � impacchettare la dimostrazione in una singola
649 ci� di cui abbiamo bisogno. Questa strategia per il caso induttivo � un p� vaga,
653 ci� che ci aspettavamo, dovremo ripensare il nostro approccio.
825 di simile a ci� che segue:
891 \ml{RW\_TAC}, e la semantica di \ml{THEN} ci permett
[all...]
H A Dproof-tools.tex183 La formula $\varphi'$ � ci� che passeremo poi a \ml{DPLL}. (Possiamo
216 Poich� non ci sono variabili libere in $\forall\vec{v}.\;\varphi$, la
226 Mettendo tutto ci� che sta di sopra insieme, possiamo scrivere la nostra funzione wrapper,
228 che ci ricorda che l'input deve essere quantificato universalmente.
277 convertire formule della forma che ci attendiamo in CNF semplicemente
294 Un approccio migliore � di convertire in ci� che � conosciuta come una ``CNF
570 Tutto ci� che rimane da fare � capire su quale variabile effettuare
679 (Se si desidera la velocit� reale, la funzione incorporata \ml{tautLib.TAUT\_PROVE} esegue ci� che sta sopra in meno di un centesimo di secondo, usando uno strumento esterno per generare la dimostrazione di insoddisfacibilit�, e per poi tradurre quella dimostrazione indietro in HOL.)
H A Dml.tex21 della workstation in modo tale che ci siano due finestre:
52 stampa un messaggio di sign-on e ci colloca all'interno di \ML. Il prompt \ML{} �
H A Dparity.tex88 caso \ml{Define} ha fatto una delle scelte per noi, ma ci sono
298 tempo {\small\verb|t|}. Cos� ci deve essere un percorso combinatorio
742 l'output al tempo {\small\verb|0|} nel caso non ci sia alcun azzeramento.
/seL4-l4v-master/HOL4/src/tactictoe/src/
H A DtttSearch.sml195 fun expo_polv_aux ci (c:real) l = case l of
197 | a :: m => (a,c) :: expo_polv_aux ci (ci * c) m
198 fun expo_polv ci l = expo_polv_aux ci ci l
/seL4-l4v-master/HOL4/src/integer/
H A DOmegaSimple.sig48 may be the sum of multiple ci * vi pairs.
H A DOmegaSymbolic.sml264 where each ci is either of the form d * x <= U or L <= e * x.
266 leaf_normalise all of the ci's and the equality term and then rename
269 Otherwise, multiply the ci's through so as to make them include
408 Every ci is a valid Omega leaf. This function converts the body
H A DOmegaSimple.sml179 and ~c is not <= d. X may be the sum of multiple ci * vi pairs.
H A DCooperMath.sml425 val ci = int_of_term c value
428 zero <= ci andalso ci < l_i
/seL4-l4v-master/HOL4/src/pred_set/src/more_theories/
H A DcardinalScript.sml859 case some ci. ci IN c /\ (cdf ci = di) of
861 | SOME ci => OPTION_MAP abf (caf ci)
869 Cases_on ���?ci. ci IN c /\ (cdf ci = di)��� >> fs[]
870 >- (���(some ci. ci I
[all...]
/seL4-l4v-master/HOL4/src/metis/
H A DmlibClauseset.sml361 fun resolv ci (dj,acc) =
362 case total (RESOLVE ci) dj of NONE => acc | SOME l => l :: acc
364 fun resolvants r (ci |-> l, acc) =
365 foldl (resolv ci) acc (N.unify r (negate l))
/seL4-l4v-master/HOL4/src/simp/src/
H A DsimpLib.sml214 type net_conv_info = {thypart : string option, ci : conv_info}
246 fun name_match ({thypart,ci}:net_conv_info) (* thing in simpset's net *) pats =
248 val ssnm = #name ci
326 {thypart = thypart, ci = {name = name, conval = USER_CONV data}})
671 tryfind (fn {ci = {conval,...},...} => conval solver stack tm)
967 fun foldthis {thypart, ci = {name,...}} nms = opttheory thypart name::nms
/seL4-l4v-master/HOL4/examples/HolBdd/
H A DDerivedBddRules.sml665 (* ((assi vm vi |--> bi),(assi' vm ci |--> bi')] *)
673 (* ((assi vm vi |--> bi),(assi' vm ci |--> bi'))] *)
678 (* (subst[v1|->ci,...,vi|->ci]tm) *)
783 (* where ci is T or F and the second element specifies a state satisfying *)
H A DPrimitiveBddRules.sml429 (* ((assi vm vi |--> bi),(assi' vm ci |--> bi'))] *)
431 (* (where c1,...,ci are T or F) *)
437 (* assi vm vi |--> bi ... assi' vm ci |-> bi' *)
442 (* (subst[v1 |-> c1, ... , vi |-> ci]tm) *)
444 (* restrict b (assignment[(var b1,mlval c1),...,(var i, mlval ci)]) *)
/seL4-l4v-master/HOL4/Manual/Translations/IT/Logic/
H A Dsemantics.tex12 chiamato una {\it teoria\/}. Questo oggetto � strettamente collegato con ci� che un
13 logico chiamerebbe una teoria\index{theories, nella logica HOL@teorie, nella logica \HOL{}!forma astratta di}, ma ci sono alcune differenze che sorgono
147 non ci siano ipotesi\index{ipotesi!di sequenti} (cio� $n=0$),
270 In aggiunta a queste otto regole, ci sono anche quattro {\it
670 modello. Il famoso teorema di incompletezza di G\"odel assicura che ci
836 ci� che costituisce una definizione di costante corretta � una restrizione
850 dal momento che non contiene $\alpha$. Di fatto, se ci fosse permesso di
1030 non sono necessariamente determinate in modo univoco. In modo corrispondente, ci possono
1068 Sezione~\ref{defs}. In un senso, ci� che causava il problema
1128 ci son
[all...]
H A Dpreface.tex56 L'\LCF\ originario fu implementato ad Edimburgo nei primi anni 1970, ed ora ci si
/seL4-l4v-master/HOL4/Manual/Translations/IT/Description/
H A Dpreface.tex56 L'\LCF\ originario fu implementato ad Edimburgo nei primi anni 1970, ed ora ci si

Completed in 174 milliseconds

12