/seL4-l4v-10.1.1/HOL4/src/metis/ |
H A D | mlibSolver.sml | 89 | 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 D | mlibThm.sig | 26 val clause : thm -> formula list value
|
H A D | mlibRewrite.sml | 182 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 D | mlibMeson.sml | 206 case clause th of [lit] => lit = goal | [] => true | _ => false; 261 val lits = clause th 301 map clause; 376 (* Unit clause shortcut. *)
|
H A D | mlibSubsume.sml | 209 (* Single clause versions *)
|
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
H A D | Subsume.sml | 75 (* 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 D | Rule.sml | 106 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 D | Waiting.sml | 35 clauses : (weight * (distance * Clause.clause)) Heap.heap, 74 type modelClause = NameSet.set * Thm.clause; 273 (* Removing the lightest clause. *)
|
H A D | metis.sml | 190 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 D | Subsume.sml | 75 (* 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 D | Rule.sml | 106 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 D | Waiting.sml | 35 clauses : (weight * (distance * Clause.clause)) Heap.heap, 74 type modelClause = NameSet.set * Thm.clause; 273 (* Removing the lightest clause. *)
|
H A D | metis.sml | 190 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 D | SolverTypes.h | 30 // 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 D | Solver.h | 56 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 D | IndDefLib.sml | 14 fun head clause = 15 let val appl = last (strip_imp (snd(strip_forall clause)))
|
H A D | InductiveDefinition.sml | 171 (* 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 D | EXPORT_PARSETREE.sml | 262 (* 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 D | QbfLibrary.sml | 92 (* 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 D | grammarLib.sml | 47 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 D | dimacsTools.sml | 26 ** 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 D | ClockedSemanticsScript.sml | 62 * (see clause for ``S_SEM v (S_REPEAT r)``). 120 * (see clause for ``S_SEM v (S_REPEAT r)``).
|
H A D | UnclockedSemanticsScript.sml | 83 * (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 D | Recftn.sml | 38 (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 D | selftest.sml | 80 "Testing arith on nested COND clause"
|