Searched refs:active (Results 1 - 25 of 63) sorted by relevance

123

/seL4-l4v-master/isabelle/src/Tools/Metis/src/
H A DActive.sig10 (* A type of active clause sets. *)
23 type active type
31 val size : active -> int
33 val saturation : active -> Clause.clause list
36 (* Create a new active clause set and initialize clauses. *)
41 active * {axioms : Clause.clause list, conjecture : Clause.clause list}
44 (* Add a clause into the active set and deduce all consequences. *)
47 val add : active -> Clause.clause -> active * Clause.clause list
53 val pp : active Prin
[all...]
H A DResolution.sml16 {active : Active.parameters,
22 active : Active.active,
30 {active = Active.default,
35 val {active = activeParm, waiting = waitingParm} = parameters value
37 val (active,cls) = Active.new activeParm ths (* cls = factored ths *) value
41 Resolution {parameters = parameters, active = active, waiting = waiting}
52 fun active (Resolution {active function
99 val (active,cls) = Active.add active cl value
[all...]
H A DResolution.sig14 {active : Active.parameters,
29 val active : resolution -> Active.active value
H A DActive.sml208 (* A type of active clause sets. *)
218 datatype active = type
236 fun setRewrite active rewrite =
240 subterms,allSubterms,...} = active
285 fun saturation active =
295 val cls = clauses active
300 val Active {parameters,...} = active
315 fun toStr active = "Active{" ^ Int.toString (size active) ^ "}"
432 fun simplifyActive simp active
771 val active = setRewrite active rewrite value
824 val active = addFactorClause active cl value
846 val (active,_,acc) = List.foldl factor1 (active,subsume,acc) cls value
847 val (active,cls) = extract_rewritables active value
878 val active = empty parameters value
879 val (active,axioms) = factor active (List.map mk_clause axioms) value
880 val (active,conjecture) = factor active (List.map mk_clause conjecture) value
900 val active = addClause active cl value
903 val (active,cls) = factor active cls value
[all...]
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/
H A DActive.sig10 (* A type of active clause sets. *)
23 type active type
31 val size : active -> int
33 val saturation : active -> Clause.clause list
36 (* Create a new active clause set and initialize clauses. *)
41 active * {axioms : Clause.clause list, conjecture : Clause.clause list}
44 (* Add a clause into the active set and deduce all consequences. *)
47 val add : active -> Clause.clause -> active * Clause.clause list
53 val pp : active Prin
[all...]
H A DResolution.sml16 {active : Active.parameters,
22 active : Active.active,
30 {active = Active.default,
35 val {active = activeParm, waiting = waitingParm} = parameters value
37 val (active,cls) = Active.new activeParm ths (* cls = factored ths *) value
41 Resolution {parameters = parameters, active = active, waiting = waiting}
52 fun active (Resolution {active function
99 val (active,cls) = Active.add active cl value
[all...]
H A DResolution.sig14 {active : Active.parameters,
29 val active : resolution -> Active.active value
H A DActive.sml208 (* A type of active clause sets. *)
218 datatype active = type
236 fun setRewrite active rewrite =
240 subterms,allSubterms,...} = active
285 fun saturation active =
295 val cls = clauses active
300 val Active {parameters,...} = active
315 fun toStr active = "Active{" ^ Int.toString (size active) ^ "}"
432 fun simplifyActive simp active
771 val active = setRewrite active rewrite value
824 val active = addFactorClause active cl value
846 val (active,_,acc) = List.foldl factor1 (active,subsume,acc) cls value
847 val (active,cls) = extract_rewritables active value
878 val active = empty parameters value
879 val (active,axioms) = factor active (List.map mk_clause axioms) value
880 val (active,conjecture) = factor active (List.map mk_clause conjecture) value
900 val active = addClause active cl value
903 val (active,cls) = factor active cls value
[all...]
/seL4-l4v-master/HOL4/examples/RL_Environment/
H A DRL_Socket.sig2 val sendStr : ('a, Socket.active Socket.stream) Socket.sock * string -> int
3 val receive : ('a, Socket.active Socket.stream) Socket.sock -> string
/seL4-l4v-master/isabelle/src/Pure/Concurrent/
H A Dconsumer_thread.scala47 private var active = true
51 def is_active: Boolean = active && thread.isAlive
81 else error("Consumer thread not active: " + quote(thread.getName))
121 synchronized { if (is_active) { active = false; mailbox.send(None) } }
/seL4-l4v-master/l4v/isabelle/src/Pure/Concurrent/
H A Dconsumer_thread.scala47 private var active = true
51 def is_active: Boolean = active && thread.isAlive
81 else error("Consumer thread not active: " + quote(thread.getName))
121 synchronized { if (is_active) { active = false; mailbox.send(None) } }
/seL4-l4v-master/l4v/spec/haskell/include/
H A Dgic.h21 uint32_t active[32]; /* [0x300, 0x380) */ member in struct:gic_dist_map_t
/seL4-l4v-master/HOL4/polyml/libpolyml/
H A Dgc_mark_phase.cpp148 bool active; member in class:MTGCProcessMarkPointers
181 MTGCProcessMarkPointers::MTGCProcessMarkPointers(): msp(0), active(false), locPtr(0)
237 if (! markStacks[i].active)
244 marker->active = true;
293 marker->active = false; // It's finished
600 marker->active = true;
618 marker->active = false;
678 marker->active = true;
696 marker->active = false;
/seL4-l4v-master/isabelle/src/Pure/Tools/
H A Ddebugger.scala54 active: Int = 0, // active views
63 def is_active: Boolean = active > 0
64 def inc_active: State = copy(active = active + 1)
65 def dec_active: State = copy(active = active - 1)
H A Dserver.scala351 def active(): Boolean =
396 list(db).find(server_info => server_info.name == name && server_info.active)
409 list(db).filterNot(_.active).foreach(server_info =>
445 while(server_info.active) { Thread.sleep(50) }
495 if server_info.active
/seL4-l4v-master/l4v/isabelle/src/Pure/Tools/
H A Ddebugger.scala54 active: Int = 0, // active views
63 def is_active: Boolean = active > 0
64 def inc_active: State = copy(active = active + 1)
65 def dec_active: State = copy(active = active - 1)
H A Dserver.scala351 def active(): Boolean =
396 list(db).find(server_info => server_info.name == name && server_info.active)
409 list(db).filterNot(_.active).foreach(server_info =>
445 while(server_info.active) { Thread.sleep(50) }
495 if server_info.active
/seL4-l4v-master/isabelle/src/Tools/jEdit/src/
H A Dpretty_tooltip.scala74 /* pending event and active state */ // owned by GUI thread
77 private var active = true
89 if (active) {
103 active = true
109 active = false
/seL4-l4v-master/l4v/isabelle/src/Tools/jEdit/src/
H A Dpretty_tooltip.scala74 /* pending event and active state */ // owned by GUI thread
77 private var active = true
89 if (active) {
103 active = true
109 active = false
/seL4-l4v-master/HOL4/polyml/basis/
H A DSocket.sml27 type active type
72 val getATMARK : ('af, active stream) sock -> bool
81 -> ('af, active stream) sock * 'af sock_addr
83 -> (('af, active stream) sock * 'af sock_addr) option
109 val sendVec : ('af, active stream) sock * Word8VectorSlice.slice -> int
110 val sendArr : ('af, active stream) sock * Word8ArraySlice.slice -> int
111 val sendVec' : ('af, active stream) sock * Word8VectorSlice.slice
113 val sendArr' : ('af, active stream) sock * Word8ArraySlice.slice
115 val sendVecNB : ('af, active stream) sock * Word8VectorSlice.slice -> int option
116 val sendArrNB : ('af, active strea
179 and active = ACTIVE type
[all...]
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/ParseTree/
H A DMATCH_COMPILER.sml619 fun pattDepth (Aot {patts=TupleField pl, ...}, active) =
620 List.foldl (fn (t, d) => Int.max(pattDepth(t, active), d)) 0 pl
622 | pattDepth (Aot {patts, defaults,...}, active) =
624 val activeDefaults = defaults intersect active
641 fun bestColumn(colsToDo, noOfCols, asTuples, active) =
649 val thisDepth = pattDepth (List.nth(asTuples, column), active)
697 fun pattCode(Aot {patts, defaults, vars, ...}, active: patSet, nextMatch: patSet * int -> pattCode, tupleNo) =
699 (* Get the set of defaults which are active. *)
700 val activeDefaults = defaults intersect active
746 (* If the active se
[all...]
/seL4-l4v-master/isabelle/src/Doc/Eisbach/document/
H A Droot.tex49 % This sort of command for each active author can be convenient
/seL4-l4v-master/l4v/isabelle/src/Doc/Eisbach/document/
H A Droot.tex49 % This sort of command for each active author can be convenient
/seL4-l4v-master/l4v/camkes/adl-spec/document/
H A Dintro.tex23 \item \emph{Distinction between active and passive components.} Components
/seL4-l4v-master/seL4/src/arch/arm/object/
H A Dvcpu.c32 static void vcpu_save(vcpu_t *vcpu, bool_t active) argument
39 /* If we aren't active then this state already got stored when
41 if (active) {
54 armv_vcpu_save(vcpu, active);
130 /* Current VCPU being active should indicate that the current thread
145 /* We shouldn't get a VGICMaintenance interrupt while a VCPU isn't active,
152 printf("Received VGIC maintenance without active VCPU!\n");
204 /* Current VCPU being active should indicate that the current thread

Completed in 115 milliseconds

123