Searched refs:clause (Results 1 - 25 of 130) sorted by relevance

123456

/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/
H A DClause.sig10 (* 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 DSubsume.sig10 (* 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 DActive.sig10 (* 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 DWaiting.sig14 (* 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 DProblem.sig14 {axioms : Thm.clause list,
15 conjecture : Thm.clause list}
24 val toClauses : problem -> Thm.clause list
H A DNormalize.sig49 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 DThm.sig19 type clause = LiteralSet.set type
32 val clause : thm -> clause value
100 val axiom : clause -> thm
H A DThm.sml15 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 DClause.sig10 (* 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 DSubsume.sig10 (* 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 DActive.sig10 (* 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 DWaiting.sig14 (* 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 DProblem.sig14 {axioms : Thm.clause list,
15 conjecture : Thm.clause list}
24 val toClauses : problem -> Thm.clause list
H A DNormalize.sig49 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 DThm.sig19 type clause = LiteralSet.set type
32 val clause : thm -> clause value
100 val axiom : clause -> thm
H A DThm.sml15 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 DmlibClause.sig30 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 DmlibClauseset.sig10 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 DmlibResolution.sig12 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 DmlibSupport.sig11 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 DmlibKernel.sml28 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 DmlibClause.sml209 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 DgrammarLib.sig7 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 DProof.h33 // (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 DProof.C68 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...]

Completed in 195 milliseconds

123456