/seL4-l4v-10.1.1/seL4/src/arch/x86/machine/ |
H A D | cpu_identification.c | 41 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 D | zc2hs.cpp | 309 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 D | minisatResolve.sml | 36 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 D | dpll.sml | 65 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 D | minisatParse.sml | 83 else let val ci = id-(sat_getint fin) value 84 in loop ((v,ci)::acc) (len+1) end
|
H A D | dimacsTools.sml | 153 fun foldthis (ci,c,svm) = let 161 Array.update(numclauses,ci,l);
|
/seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Tutorial/ |
H A D | combin.tex | 190 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 D | more-examples.tex | 35 in azione. In primo piano ci sono una semantica operazionale per un piccolo linguaggio
|
H A D | euclid.tex | 87 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 D | proof-tools.tex | 183 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 D | ml.tex | 21 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 D | parity.tex | 88 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 D | intro.tex | 102 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 D | OmegaSimple.sig | 48 may be the sum of multiple ci * vi pairs.
|
H A D | OmegaSymbolic.sml | 264 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 D | OmegaSimple.sml | 179 and ~c is not <= d. X may be the sum of multiple ci * vi pairs.
|
H A D | CooperMath.sml | 425 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 D | cardinalScript.sml | 869 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 D | mlibClauseset.sml | 361 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 D | DerivedBddRules.sml | 665 (* ((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 D | PrimitiveBddRules.sml | 429 (* ((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 D | semantics.tex | 12 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 D | preface.tex | 56 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 D | preface.tex | 56 L'\LCF\ originario fu implementato ad Edimburgo nei primi anni 1970, ed ora ci si
|
H A D | libraries.tex | 247 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...] |