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

12

/seL4-l4v-10.1.1/seL4/src/arch/x86/machine/
H A Dcpu_identification.c41 x86_cpuid_fill_vendor_string(cpu_identity_t *ci) argument
43 MAY_ALIAS uint32_t *vendor_string32 = (uint32_t *)ci->vendor_string;
45 if (ci == NULL) {
53 ci->vendor_string[X86_CPUID_VENDOR_STRING_MAXLENGTH] = '\0';
61 x86_cpuid_intel_identity_initialize(cpu_identity_t *ci, argument
71 ci->display.family = original.family;
73 ci->display.family = ci->display.extended_family + original.family;
82 * if (ci->display.family == 0x06 || ci
103 x86_cpuid_amd_identity_initialize(cpu_identity_t *ci, struct family_model original) argument
125 cpu_identity_t *ci = x86_cpuid_get_identity(); local
[all...]
/seL4-l4v-10.1.1/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-10.1.1/HOL4/src/HolSat/
H A DminisatResolve.sml36 fun dualise lfn orc clauseth ci =
55 handle Subscript => failwith("dualise"^(int_to_string (ci))^"\n")
67 fun prepareRootClause lfn orc clauseth cl ci =
69 val th = dualise lfn orc clauseth ci
70 val _ = Dynarray.update(cl,ci,th)
73 (* will return clause thm at index ci *)
74 fun getClause cl ci = Dynarray.sub(cl,ci)
75 handle Subscript => failwith("getClause"^(int_to_string (ci))^"\n")
103 val res = List.foldl (fn ((vi,ci),t
[all...]
H A Ddpll.sml65 fun CoreDPLL initial_th = let (* [ci] |- cnf *)
66 fun recurse th = let (* [assigns, ci] |- curr *)
75 val (l,r) = casesplit v th (*[assigns,v=T,ci]|- curr[T/v],[assigns,v=F,ci]|- curr[F/v]*)
82 (* [assignsr\v,assignsl\v,ci] |- F *)
88 recurse initial_th (* [ci] |- F *)
91 fun doCNF neg_tm = (* clauses is (ci,[~t] |- ci') pairs, where ci' is expanded ci *)
[all...]
H A DminisatParse.sml83 else let val ci = id-(sat_getint fin) value
84 in loop ((v,ci)::acc) (len+1) end
H A DdimacsTools.sml153 fun foldthis (ci,c,svm) = let
161 Array.update(numclauses,ci,l);
/seL4-l4v-10.1.1/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.
H A Dintro.tex102 Quando il proprio sistema ML � installato, e ci si trova nella directory radice della distribuzione, il passo successivo � eseguire \texttt{smart-configure}.
/seL4-l4v-10.1.1/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-10.1.1/HOL4/src/pred_set/src/more_theories/
H A DcardinalScript.sml869 case some ci. ci IN c /\ (cdf ci = di) of
871 | SOME ci => OPTION_MAP abf (caf ci)
879 Cases_on ���?ci. ci IN c /\ (cdf ci = di)��� >> fs[]
880 >- (���(some ci. ci I
[all...]
/seL4-l4v-10.1.1/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-10.1.1/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-10.1.1/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-10.1.1/HOL4/Manual/Translations/IT/Description/
H A Dpreface.tex56 L'\LCF\ originario fu implementato ad Edimburgo nei primi anni 1970, ed ora ci si
H A Dlibraries.tex247 fase successiva, il fatto che ci sia una costante chiamata \holtxt{+}
300 slegare da ci� che l'utente digita. Nel caso dell'addizione, il
417 caratteri. A meno che ci sia gi� nella grammatica uno specifico token ``misto'',
618 tipo pi� generale non � ci� che si desidera e l'utente deve aggiungere dei vincoli
640 sistema ci informer� che � stata eseguita la risoluzione dell'overloading.
754 Di fatto tuttavia, in un termine come $f(x)$, dove $f$ e $x$ non hanno fixity, la sintassi � trattata come se ci fosse una invisibile applicazione di funzione infissa tra i due token: $f\cdot{}x$.
777 I suffissi appaiono dopo il loro argomenti. Non ci sono suffissi
782 suffisso, allora ci sono sei ordinamenti possibili per i tre differenti
864 Dal momento che ci deve essere un termine ``a penzoloni'' sulla destra, la
882 Qui ci� ch
[all...]

Completed in 291 milliseconds

12