/seL4-l4v-master/HOL4/src/HolSat/sat_solvers/zc2hs/ |
H A D | zc2hs.cpp | 128 printf("PROOF ERROR! Resolved on variable with SAME polarity in both clauses: %d\n", x+1); 141 vec<vec<Lit> > clauses; member in struct:Checker 146 /*printf("%d: ROOT", clauses.size()); 149 clauses.push(); 150 c.copyTo(clauses.last()); } 153 /*printf("%d: CHAIN %d", clauses.size(), cs[0]-1); 156 clauses.push(); 157 vec<Lit>& c = clauses.last(); 158 clauses[cs[0]-1].copyTo(c); 161 resolve(c, clauses[c 266 vec<vec<Lit> >& clauses; member in class:Z2M 487 vec<vec<Lit> > clauses; // proof clause database local [all...] |
/seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
H A D | Waiting.sml | 12 (* A type of waiting sets of clauses. *) 35 clauses : (weight * (distance * Clause.clause)) Heap.heap, 55 fun size (Waiting {clauses,...}) = Heap.size clauses; 65 (fn Waiting {clauses,...} => 66 List.map (fn (w,(_,cl)) => (w, Clause.id cl, cl)) (Heap.toList clauses)) 190 (* Adding new clauses. *) 195 val Waiting {parameters,clauses,models} = waiting 215 val clauses = List.foldl addCl clauses (zi value 246 val clauses = Heap.new cmp value [all...] |
H A D | Waiting.sig | 10 (* The parameters control the order that clauses are removed from the *) 11 (* waiting set: clauses are assigned a weight and removed in strict weight *) 43 (* A type of waiting sets of clauses. *) 66 (* Adding new clauses. *)
|
H A D | Subsume.sml | 84 clauses : (Literal.literal list * Thm.clause * 'a) IntMap.map, 94 clauses = IntMap.new (), 98 fun size (Subsume {empty, unit, nonunit = {clauses,...}}) = 99 length empty + LiteralNet.size unit + IntMap.size clauses; 117 val {nextId,clauses,fstLits,sndLits} = nonunit 126 val clauses = IntMap.insert clauses (nextId,(lits',cl',a)) value 128 val nonunit = {nextId = nextId, clauses = clauses, 142 val {nextId,clauses,fstLit [all...] |
H A D | Active.sml | 195 "Active.isSaturated: clauses" cls 221 clauses : Clause.clause IntMap.map, 239 {parameters,clauses,units,subsume,literals,equations, 243 {parameters = parameters, clauses = clauses, units = units, 266 clauses = IntMap.new (), 276 fun size (Active {clauses,...}) = IntMap.size clauses; 278 fun clauses (Active {clauses function 501 val clauses = IntMap.insert clauses (Clause.id cl, cl) value 744 val clauses = IntMap.filter (idPred o fst) clauses value [all...] |
H A D | Active.sig | 36 (* Create a new active clause set and initialize clauses. *)
|
H A D | Problem.sig | 17 val size : problem -> {clauses : int,
|
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Waiting.sml | 12 (* A type of waiting sets of clauses. *) 35 clauses : (weight * (distance * Clause.clause)) Heap.heap, 55 fun size (Waiting {clauses,...}) = Heap.size clauses; 65 (fn Waiting {clauses,...} => 66 List.map (fn (w,(_,cl)) => (w, Clause.id cl, cl)) (Heap.toList clauses)) 190 (* Adding new clauses. *) 195 val Waiting {parameters,clauses,models} = waiting 215 val clauses = List.foldl addCl clauses (zi value 246 val clauses = Heap.new cmp value [all...] |
H A D | Waiting.sig | 10 (* The parameters control the order that clauses are removed from the *) 11 (* waiting set: clauses are assigned a weight and removed in strict weight *) 43 (* A type of waiting sets of clauses. *) 66 (* Adding new clauses. *)
|
H A D | Subsume.sml | 84 clauses : (Literal.literal list * Thm.clause * 'a) IntMap.map, 94 clauses = IntMap.new (), 98 fun size (Subsume {empty, unit, nonunit = {clauses,...}}) = 99 length empty + LiteralNet.size unit + IntMap.size clauses; 117 val {nextId,clauses,fstLits,sndLits} = nonunit 126 val clauses = IntMap.insert clauses (nextId,(lits',cl',a)) value 128 val nonunit = {nextId = nextId, clauses = clauses, 142 val {nextId,clauses,fstLit [all...] |
H A D | Active.sml | 195 "Active.isSaturated: clauses" cls 221 clauses : Clause.clause IntMap.map, 239 {parameters,clauses,units,subsume,literals,equations, 243 {parameters = parameters, clauses = clauses, units = units, 266 clauses = IntMap.new (), 276 fun size (Active {clauses,...}) = IntMap.size clauses; 278 fun clauses (Active {clauses function 501 val clauses = IntMap.insert clauses (Clause.id cl, cl) value 744 val clauses = IntMap.filter (idPred o fst) clauses value [all...] |
H A D | Active.sig | 36 (* Create a new active clause set and initialize clauses. *)
|
H A D | Problem.sig | 17 val size : problem -> {clauses : int,
|
/seL4-l4v-master/HOL4/src/metis/ |
H A D | mlibSubsume.sig | 23 (* All subsuming clauses *) 26 (* Subsuming clauses that don't contain more literals than the query *)
|
H A D | mlibSupport.sml | 193 clauses : (real * (real * clause)) heap, 198 let val SOS {parm = p, clauses = _, distance = d, models = m} = sos 199 in SOS {parm = p, clauses = c, distance = d, models = m} 203 let val SOS {parm = p, clauses = c, distance = _, models = m} = sos 204 in SOS {parm = p, clauses = c, distance = d, models = m} 208 let val SOS {parm = p, clauses = c, distance = d, models = _} = sos 209 in SOS {parm = p, clauses = c, distance = d, models = m} 254 SOS {parm = parm, clauses = empty_heap, distance = I.empty (), 258 fun ssize (SOS {clauses,...}) = H.size clauses; [all...] |
H A D | mlibCanon.sig | 26 (* A tautology filter for clauses *) 36 (* Categorizing sets of clauses *)
|
H A D | mlibClauseset.sml | 118 clauses : clause list, 126 val SET {parm = z, size = _, units = u, rewrites = r, clauses = c, 129 SET {parm = z, size = n, units = u, rewrites = r, clauses = c, 135 val SET {parm = z, size = n, units = _, rewrites = r, clauses = c, 138 SET {parm = z, size = n, units = u, rewrites = r, clauses = c, 144 val SET {parm = z, size = n, units = u, rewrites = _, clauses = c, 147 SET {parm = z, size = n, units = u, rewrites = r, clauses = c, 153 val SET {parm = z, size = n, units = u, rewrites = r, clauses = _, 156 SET {parm = z, size = n, units = u, rewrites = r, clauses = c, 162 val SET {parm = z, size = n, units = u, rewrites = r, clauses 214 fun clauses (SET {clauses, ...}) = clauses; function [all...] |
H A D | mlibClauseset.sig | 29 val clauses : clauseset -> clause list value 32 (* Simplify and strengthen clauses *) 45 (* Factor clauses *)
|
H A D | mlibSupport.sig | 40 (* Adding new clauses *)
|
/seL4-l4v-master/HOL4/src/HolSat/sat_solvers/minisat/ |
H A D | Main.C | 126 printf("PROOF ERROR! Resolved on variable with SAME polarity in both clauses: %d\n", x+1); 139 vec<vec<Lit> > clauses; member in struct:Checker 142 //**/printf("%d: ROOT", clauses.size()); 146 clauses.push(); 147 c.copyTo(clauses.last()); } 150 //**/printf("%d: CHAIN %d", clauses.size(), cs[0]-1); 152 clauses.push(); 153 vec<Lit>& c = clauses.last(); 157 clauses[cs[0]-1].copyTo(c); 159 resolve(c, clauses[c [all...] |
H A D | Solver.h | 54 vec<Clause*> clauses; // List of problem clauses. member in class:Solver 55 vec<Clause*> learnts; // List of learnt clauses. 116 // Operations on clauses: 153 for (int i = 0; i < clauses.size(); i++) if (clauses[i] != NULL) remove(clauses[i], true); 164 int nClauses() { return clauses.size(); }
|
/seL4-l4v-master/HOL4/src/HolSat/ |
H A D | dpll.sml | 94 (* clauses is (ci,[~t] |- ci') pairs, where ci' is expanded ci *) 96 val clauses = Array.foldr (fn ((c,th),l) => (c,th)::l) [] clauseth value 99 (ASSUME (fst (hd clauses))) (tl clauses) 100 in (cnfv,cnf_thm,lfn,clauses) end 102 fun undoCNF lfn clauses th = (* th is [ci] |- F *) 106 inst_th clauses (* ~t |- F *) 124 val (cnfv,cnf_thm,lfn,clauses) = doCNF (mk_neg t) 129 undoCNF lfn clauses cnf_entails_F (* [~t] |- F *)
|
/seL4-l4v-master/HOL4/src/HolQbf/ |
H A D | QbfConv.sig | 24 (* simplifies clauses (specialisation of SIMP_CONV). In particular, does the following rewrites: 30 removes the quantifier and all occurrences of x. also simplifies clauses (as above). *)
|
/seL4-l4v-master/HOL4/src/IndDef/ |
H A D | InductiveDefinition.sml | 247 (* Canonicalizes the set of clauses, disjoining compatible antecedants. *) 253 fun canonicalize_clauses clauses = 254 let val concls = map getconcl clauses 258 val closed = list_mk_conj clauses 263 val cthms = map2 canonicalize_clause clauses cargs 362 let val clauses = strip_conj tm value 363 val canonthm = canonicalize_clauses clauses 625 (* "Unschematize" a set of clauses. *) 678 fun unschematize_clauses clauses = let 679 val schem = map schem_head clauses 741 val clauses = strip_conj tm value 866 let val clauses = strip_conj tm value 879 let val clauses = strip_conj tm value [all...] |
H A D | CoIndDefLib.sml | 128 let val clauses = strip_conj tm value 129 val canonthm = canonicalize_clauses clauses 145 let val clauses = strip_conj tm value 146 val (clauses',fvs) = unschematize_clauses clauses 147 val _ = check_definition fvs clocs (list_mk_conj clauses') 149 (check_definition fvs clocs (list_mk_conj clauses'))
|