Searched refs:clauses (Results 1 - 25 of 120) sorted by relevance

12345

/seL4-l4v-master/HOL4/src/HolSat/sat_solvers/zc2hs/
H A Dzc2hs.cpp128 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 DWaiting.sml12 (* 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 DWaiting.sig10 (* 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 DSubsume.sml84 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 DActive.sml195 "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 DActive.sig36 (* Create a new active clause set and initialize clauses. *)
H A DProblem.sig17 val size : problem -> {clauses : int,
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/
H A DWaiting.sml12 (* 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 DWaiting.sig10 (* 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 DSubsume.sml84 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 DActive.sml195 "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 DActive.sig36 (* Create a new active clause set and initialize clauses. *)
H A DProblem.sig17 val size : problem -> {clauses : int,
/seL4-l4v-master/HOL4/src/metis/
H A DmlibSubsume.sig23 (* All subsuming clauses *)
26 (* Subsuming clauses that don't contain more literals than the query *)
H A DmlibSupport.sml193 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 DmlibCanon.sig26 (* A tautology filter for clauses *)
36 (* Categorizing sets of clauses *)
H A DmlibClauseset.sml118 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 DmlibClauseset.sig29 val clauses : clauseset -> clause list value
32 (* Simplify and strengthen clauses *)
45 (* Factor clauses *)
H A DmlibSupport.sig40 (* Adding new clauses *)
/seL4-l4v-master/HOL4/src/HolSat/sat_solvers/minisat/
H A DMain.C126 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 DSolver.h54 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 Ddpll.sml94 (* 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 DQbfConv.sig24 (* 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 DInductiveDefinition.sml247 (* 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 DCoIndDefLib.sml128 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'))

Completed in 181 milliseconds

12345