Searched refs:clause (Results 51 - 75 of 130) sorted by relevance

123456

/seL4-l4v-10.1.1/HOL4/src/metis/
H A DmlibSolver.sml89 | final (SOME ths) = solves (map (concl o clause) ths)
308 filter = (fn x => null x orelse List.exists negative x) o clause};
312 filter = (fn x => null x orelse List.exists positive x) o clause};
315 {name = "all negative", filter = List.all negative o clause};
318 {name = "all positive", filter = List.all positive o clause};
H A DmlibThm.sig26 val clause : thm -> formula list value
H A DmlibRewrite.sml182 List.exists lit_match (clause th)
242 if not (mem neq (clause th)) then rewr_neqs dealt neqs th else
259 val lits = clause th
H A DmlibMeson.sml206 case clause th of [lit] => lit = goal | [] => true | _ => false;
261 val lits = clause th
301 map clause;
376 (* Unit clause shortcut. *)
H A DmlibSubsume.sml209 (* Single clause versions *)
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/
H A DSubsume.sml75 (* A type of clause sets that supports efficient subsumption checking. *)
80 {empty : (Thm.clause * Subst.subst * 'a) list,
81 unit : (Literal.literal * Thm.clause * 'a) LiteralNet.literalNet,
84 clauses : (Literal.literal list * Thm.clause * 'a) IntMap.map,
317 (* Single clause versions. *)
H A DRule.sml106 if LiteralSet.member lit (Thm.clause th) then SOME lit else NONE
390 if not (LiteralSet.equal (Thm.clause th) (Thm.clause th')) then th'
433 fun allLiteralsRule literule th = literalsRule literule (Thm.clause th) th;
532 fun removeIrrefl th = LiteralSet.foldl irrefl th (Thm.clause th);
554 snd (LiteralSet.foldl rem (LiteralSet.empty,th) (Thm.clause th));
578 case LiteralSet.firstl (total expand) (Thm.clause th) of
783 List.map fact (factor' (Thm.clause th))
H A DWaiting.sml35 clauses : (weight * (distance * Clause.clause)) Heap.heap,
74 type modelClause = NameSet.set * Thm.clause;
273 (* Removing the lightest clause. *)
H A Dmetis.sml190 plural clauses "clause" ^ ", " ^
261 {comments = ["Saturation clause set for " ^ filename],
266 conjecture = List.map Thm.clause ths}}
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/
H A DSubsume.sml75 (* A type of clause sets that supports efficient subsumption checking. *)
80 {empty : (Thm.clause * Subst.subst * 'a) list,
81 unit : (Literal.literal * Thm.clause * 'a) LiteralNet.literalNet,
84 clauses : (Literal.literal list * Thm.clause * 'a) IntMap.map,
317 (* Single clause versions. *)
H A DRule.sml106 if LiteralSet.member lit (Thm.clause th) then SOME lit else NONE
390 if not (LiteralSet.equal (Thm.clause th) (Thm.clause th')) then th'
433 fun allLiteralsRule literule th = literalsRule literule (Thm.clause th) th;
532 fun removeIrrefl th = LiteralSet.foldl irrefl th (Thm.clause th);
554 snd (LiteralSet.foldl rem (LiteralSet.empty,th) (Thm.clause th));
578 case LiteralSet.firstl (total expand) (Thm.clause th) of
783 List.map fact (factor' (Thm.clause th))
H A DWaiting.sml35 clauses : (weight * (distance * Clause.clause)) Heap.heap,
74 type modelClause = NameSet.set * Thm.clause;
273 (* Removing the lightest clause. *)
H A Dmetis.sml190 plural clauses "clause" ^ ", " ^
261 {comments = ["Saturation clause set for " ^ filename],
266 conjecture = List.map Thm.clause ths}}
/seL4-l4v-10.1.1/HOL4/src/HolSat/sat_solvers/minisat/
H A DSolverTypes.h30 // Variables, literals, clause IDs:
76 // Clause -- a simple class for representing a clause:
115 // GClause -- Generalize clause:
118 // Either a pointer to a clause or a literal.
128 Clause* clause () const { return (Clause*)data; } function in class:GClause
H A DSolver.h56 vec<ClauseId> unit_id; // 'unit_id[var]' is the clause ID for the unit literal 'var' or '~var' (if set at toplevel).
57 double cla_inc; // Amount to bump next clause with.
58 double cla_decay; // INVERSE decay factor for clause activity: stores 1/decay.
69 vec<Clause*> reason; // 'reason[var]' is the clause that implied the variables current value, or 'NULL' if none.
93 void record (const vec<Lit>& clause);
174 bool expensive_ccmin; // Controls conflict clause minimization. TRUE by default.
196 vec<Lit> conflict; // If problem is unsatisfiable under assumptions, this vector represent the conflict clause expressed in the assumptions.
197 ClauseId conflict_id; // (In proof logging mode only.) ID for the clause 'conflict' (for proof traverseral). NOTE! The empty clause is always the last clause derive
[all...]
/seL4-l4v-10.1.1/HOL4/src/IndDef/
H A DIndDefLib.sml14 fun head clause =
15 let val appl = last (strip_imp (snd(strip_forall clause)))
H A DInductiveDefinition.sml171 (* Translates a single clause to have variable arguments, simplifying. *)
189 fun canonicalize_clause clause carg =
190 let val (avs,bimp) = strip_forall clause
201 val th0 = MP (SPECL avs (ASSUME clause)) tth
217 "Vacuous clause trivialises whole definition"
221 val th0 = SPECL avs (ASSUME clause)
827 " in clause #"^Int.toString n ^
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/ParseTree/
H A DEXPORT_PARSETREE.sml262 (* The effect of this is to have all the elements of the clause as
284 fb as FValBind{clauses=[clause], location, functVar = ref idVal, ...}) =
285 (* If there's just one clause go straight to it. Otherwise we have an
289 val asChild = exportAClause(clause, idVal, fn () => exportFB(navigation, fb))
297 (* Each child gives a clause. *)
302 fun exportClause(navigation, clause as FValClause{ line, ...}) =
305 val asChild = exportAClause(clause, idVal, fn () => exportClause(navigation, clause))
/seL4-l4v-10.1.1/HOL4/src/HolQbf/
H A DQbfLibrary.sml92 (* clause theorem 'thm' in sequent form, as produced by *)
176 (* Implements forall-reduction. Takes a clause in sequent form, a list of *)
178 (* be a hypothesis of the clause) that is missing these variables, and *)
179 (* the list of literals present in the clause. Both lists must be *)
/seL4-l4v-10.1.1/HOL4/examples/formal-languages/context-free/
H A DgrammarLib.sml47 datatype clause = Syms of sym list | TmAQ of term type
48 type t = (string * clause list) list
246 (* clause = a sequence of tokens and non-terminals
250 val clause = value
261 sepby clause (token "|") <- token ";"
/seL4-l4v-10.1.1/HOL4/src/HolSat/
H A DdimacsTools.sml26 ** is the clause separator)
110 print " is not a clause or literal\n"; raise literalToIntError)
136 ** N.B. Definition of termToDimacs processes last clause first,
202 local (* dimacsToTerm_aux splits off one clause, dimacsToTerm iterates it *)
/seL4-l4v-10.1.1/HOL4/examples/PSL/1.1/official-semantics/
H A DClockedSemanticsScript.sml62 * (see clause for ``S_SEM v (S_REPEAT r)``).
120 * (see clause for ``S_SEM v (S_REPEAT r)``).
H A DUnclockedSemanticsScript.sml83 * (see clause for ``US_SEM v (S_REPEAT r)``).
137 * (see clause for ``US_SEM v (S_REPEAT r)``).
/seL4-l4v-10.1.1/HOL4/src/datatype/mutrec/
H A DRecftn.sml38 (again, (SCONatpat sc)). There may be at most one "allelse" clause per
41 type of the variable). As noted above, the "allelse" clause must
239 clause if it found that, as well as the rest of the def_info
242 matching with an "allelse" clause after already matching
250 (* check if there's an "allelse" clause for this type;
633 to an allelse clause, returns the list of conjs found as well
653 that they return so that when we come across an "allelse" clause
/seL4-l4v-10.1.1/HOL4/src/num/arith/src/
H A Dselftest.sml80 "Testing arith on nested COND clause"

Completed in 142 milliseconds

123456