/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
H A D | Clause.sig | 10 (* A type of clause. *) 27 type clause type 37 val mk : clauseInfo -> clause 39 val dest : clause -> clauseInfo 41 val id : clause -> clauseId 43 val thm : clause -> Thm.thm 45 val equalThms : clause -> clause -> bool 47 val literals : clause -> Thm.clause [all...] |
H A D | Subsume.sig | 10 (* A type of clause sets that supports efficient subsumption checking. *) 19 val insert : 'a subsume -> Thm.clause * 'a -> 'a subsume 32 (Thm.clause * Subst.subst * 'a -> bool) -> 'a subsume -> Thm.clause -> 33 (Thm.clause * Subst.subst * 'a) option 35 val isSubsumed : 'a subsume -> Thm.clause -> bool 38 (Thm.clause * Subst.subst * 'a -> bool) -> 'a subsume -> Thm.clause -> 39 (Thm.clause * Subst.subst * 'a) option 41 val isStrictlySubsumed : 'a subsume -> Thm.clause [all...] |
H A D | Active.sig | 10 (* A type of active clause sets. *) 19 {clause : Clause.parameters, 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
|
H A D | Waiting.sig | 14 (* The weight of a clause is defined to be *) 20 (* d = the derivation distance of the clause from the axioms *) 21 (* s = the number of symbols in the clause *) 22 (* v = the number of distinct variables in the clause *) 23 (* l = the number of literals in the clause *) 24 (* m = the truth of the clause wrt the models *) 58 {axioms : Clause.clause list, 59 conjecture : Clause.clause list} -> waiting 69 val add : waiting -> distance * Clause.clause list -> waiting 72 (* Removing the lightest clause [all...] |
H A D | Problem.sig | 14 {axioms : Thm.clause list, 15 conjecture : Thm.clause list} 24 val toClauses : problem -> Thm.clause list
|
H A D | Normalize.sig | 49 val addCnf : thm -> cnf -> (Thm.clause * thm) list * cnf 51 val proveCnf : thm list -> (Thm.clause * thm) list 53 val cnf : Formula.formula -> Thm.clause list
|
H A D | Thm.sig | 19 type clause = LiteralSet.set type 32 val clause : thm -> clause value 100 val axiom : clause -> thm
|
H A D | Thm.sml | 15 type clause = LiteralSet.set; type 26 datatype thm = Thm of clause * (inferenceType * thm list); 34 fun clause (Thm (cl,_)) = cl; function 47 case LiteralSet.foldl chk (SOME AtomSet.empty) (clause th) of 54 fun isContradiction th = LiteralSet.null (clause th); 80 fun compare (th1,th2) = LiteralSet.compare (clause th1, clause th2); 82 fun equal th1 th2 = LiteralSet.equal (clause th1) (clause th2); 110 (List.map Literal.toFormula (LiteralSet.toList (clause t [all...] |
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Clause.sig | 10 (* A type of clause. *) 27 type clause type 37 val mk : clauseInfo -> clause 39 val dest : clause -> clauseInfo 41 val id : clause -> clauseId 43 val thm : clause -> Thm.thm 45 val equalThms : clause -> clause -> bool 47 val literals : clause -> Thm.clause [all...] |
H A D | Subsume.sig | 10 (* A type of clause sets that supports efficient subsumption checking. *) 19 val insert : 'a subsume -> Thm.clause * 'a -> 'a subsume 32 (Thm.clause * Subst.subst * 'a -> bool) -> 'a subsume -> Thm.clause -> 33 (Thm.clause * Subst.subst * 'a) option 35 val isSubsumed : 'a subsume -> Thm.clause -> bool 38 (Thm.clause * Subst.subst * 'a -> bool) -> 'a subsume -> Thm.clause -> 39 (Thm.clause * Subst.subst * 'a) option 41 val isStrictlySubsumed : 'a subsume -> Thm.clause [all...] |
H A D | Active.sig | 10 (* A type of active clause sets. *) 19 {clause : Clause.parameters, 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
|
H A D | Waiting.sig | 14 (* The weight of a clause is defined to be *) 20 (* d = the derivation distance of the clause from the axioms *) 21 (* s = the number of symbols in the clause *) 22 (* v = the number of distinct variables in the clause *) 23 (* l = the number of literals in the clause *) 24 (* m = the truth of the clause wrt the models *) 58 {axioms : Clause.clause list, 59 conjecture : Clause.clause list} -> waiting 69 val add : waiting -> distance * Clause.clause list -> waiting 72 (* Removing the lightest clause [all...] |
H A D | Problem.sig | 14 {axioms : Thm.clause list, 15 conjecture : Thm.clause list} 24 val toClauses : problem -> Thm.clause list
|
H A D | Normalize.sig | 49 val addCnf : thm -> cnf -> (Thm.clause * thm) list * cnf 51 val proveCnf : thm list -> (Thm.clause * thm) list 53 val cnf : Formula.formula -> Thm.clause list
|
H A D | Thm.sig | 19 type clause = LiteralSet.set type 32 val clause : thm -> clause value 100 val axiom : clause -> thm
|
H A D | Thm.sml | 15 type clause = LiteralSet.set; type 26 datatype thm = Thm of clause * (inferenceType * thm list); 34 fun clause (Thm (cl,_)) = cl; function 47 case LiteralSet.foldl chk (SOME AtomSet.empty) (clause th) of 54 fun isContradiction th = LiteralSet.null (clause th); 80 fun compare (th1,th2) = LiteralSet.compare (clause th1, clause th2); 82 fun equal th1 th2 = LiteralSet.equal (clause th1) (clause th2); 110 (List.map Literal.toFormula (LiteralSet.toList (clause t [all...] |
/seL4-l4v-10.1.1/HOL4/src/metis/ |
H A D | mlibClause.sig | 30 type clause type 34 val mk_clause : parameters -> thm -> clause 35 val dest_clause : clause -> bits 36 val literals : clause -> formula list 37 val is_empty : clause -> bool 38 val dest_rewr : clause -> int * thm 39 val is_rewr : clause -> bool 40 val rebrand : parameters -> clause -> clause 43 val largest_lits : clause [all...] |
H A D | mlibClauseset.sig | 10 type clause = mlibClause.clause type 29 val clauses : clauseset -> clause list 33 val simplify : clauseset -> clause -> clause 34 val strengthen : clauseset -> clause -> clause option 37 val subsumed : clauseset -> clause -> bool 39 (* Add a clause into the set *) 40 val add : clause [all...] |
H A D | mlibResolution.sig | 12 type clause = mlibClause.clause type 33 val select : resolution -> ((distance * clause) * resolution) option 34 val deduce : clause -> resolution -> clause list 35 val factor : clause list -> resolution -> clause list * resolution 36 val add : distance * clause list -> resolution -> resolution
|
H A D | mlibSupport.sig | 11 type clause = mlibClause.clause type 35 val new : parameters -> formula list -> clause list -> sos 37 val to_list : sos -> clause list 41 val add : distance * clause list -> sos -> sos 43 (* Removing the lightest clause *) 44 val remove : sos -> ((distance * clause) * sos) option
|
H A D | mlibKernel.sml | 28 val clause = fst o dest_thm; value 50 => if cl' = clause th' then th' else mlibThm (cl', (Inst, [th'])) 55 let val cl = rev (setify (clause th)) 56 in if cl = clause th then th else mlibThm (cl, (Factor, [th])) 61 val cl1 = clause th1 63 val cl2 = clause th2 76 val th_lits = clause th
|
H A D | mlibClause.sml | 209 datatype clause = CL of parameters * int * thm * termorder * derivation type 212 | mlibResolution of clause * clause 213 | Paramodulation of clause * clause 214 | Factor of clause; 222 val literals = mlibThm.clause o #thm o dest_clause; 272 val lits = mlibThm.clause th 290 val lits = mlibThm.clause th 322 val lits = mlibThm.clause t [all...] |
/seL4-l4v-10.1.1/HOL4/examples/formal-languages/context-free/ |
H A D | grammarLib.sig | 7 datatype clause = Syms of sym list | TmAQ of term type 8 type t = (string * clause list) list
|
/seL4-l4v-10.1.1/HOL4/src/HolSat/sat_solvers/minisat/ |
H A D | Proof.h | 33 // (offline mode) this class. Each call to 'root()' or 'chain()' produces a new clause. The first 34 // clause has ID 0, the next 1 and so on. These are the IDs passed to 'chain()'s 'cs' parameter. 52 vec<Lit> clause; member in class:Proof 55 vec<int64> c2fp; // c2fp[id] gives position in proof trace of clause with id 'id' 63 ClauseId addRoot (vec<Lit>& clause, ClauseId orig_root_id = -1); 72 ClauseId parseRoot (vec<Lit>& clause, File& fp, uint64 tmp, std::ofstream* fout = NULL); 75 ClauseId parseRoot (vec<Lit>& clause, File& fp, uint64 tmp);
|
H A D | Proof.C | 68 id_counter = 1; //HA: to save sign info on-the-fly, unit_id uses -ve clause id's to indicate 69 // that the clause literal is negated, so can't use 0 72 c2fp.push(0); // dummy argument (placeholder for clause ID 0 which does not exist) 85 cl.copyTo(clause); 87 sortUnique(clause); 90 trav->root(clause); 100 putUInt(fp, index(clause[0])); 101 for (int i = 1; i < clause.size(); i++) 102 putUInt(fp, index(clause[i]) - index(clause[ 178 parseRoot(vec<Lit>& clause, File& fp, uint64 tmp, std::ofstream* fout) argument [all...] |