| /seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
| H A D | Problem.sml | 23 fun lits (cl,n) = n + LiteralSet.size cl function
|
| H A D | Subsume.sml | 35 val lits = LiteralSet.toList cl value
42 val lits = clauseSym [lit] value
323 and lits = clauseSym (LiteralSet.toList cl) value
[all...] |
| H A D | Clause.sml | 260 val lits = largestLiterals cl value
|
| H A D | Proof.sml | 208 val lits = LiteralSet.intersectList [cl1,cl1',cl2,cl2'] value
|
| H A D | Waiting.sml | 78 val lits = Clause.literals cl value
161 val lits = Clause.literals cl value
|
| H A D | Active.sml | 289 val lits = Clause.literals cl value
572 val lits = Clause.largestLiterals cl value
|
| /seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
| H A D | Problem.sml | 23 fun lits (cl,n) = n + LiteralSet.size cl function
|
| H A D | Subsume.sml | 35 val lits = LiteralSet.toList cl value
42 val lits = clauseSym [lit] value
323 and lits = clauseSym (LiteralSet.toList cl) value
[all...] |
| H A D | Clause.sml | 260 val lits = largestLiterals cl value
|
| H A D | Proof.sml | 208 val lits = LiteralSet.intersectList [cl1,cl1',cl2,cl2'] value
|
| H A D | Waiting.sml | 78 val lits = Clause.literals cl value
161 val lits = Clause.literals cl value
|
| H A D | Active.sml | 289 val lits = Clause.literals cl value
572 val lits = Clause.largestLiterals cl value
|
| /seL4-l4v-master/HOL4/src/HolQbf/ |
| H A D | QbfLibrary.sml | 265 val (lits, p, p', p_is_pos) = find_pivot [] lits1 lits2 value
|
| H A D | QbfCertificate.sml | 384 val lits = QbfLibrary.literals_in_clause index_fn clause value
[all...] |
| /seL4-l4v-master/HOL4/src/HolSat/ |
| H A D | def_cnf.sml | 167 let val lits = List.rev (strip_disj tm) value
|
| /seL4-l4v-master/HOL4/src/HolSat/sat_solvers/minisat/ |
| H A D | Main.C | 32 void addLit(int parsed_lit,Solver& S, vec<Lit>& lits) { argument
38 void addClause(Solver& S, vec<Lit>& lits) { argument
51 vec<Lit> lits; local
57 addLit(atoi(stok.c_str()),S,lits); // firs local
[all...] |
| /seL4-l4v-master/HOL4/src/metis/ |
| H A D | mlibMeson.sml | 261 val lits = clause th value
|
| H A D | mlibRewrite.sml | 259 val lits = clause th value
|
| H A D | mlibClause.sml | 272 val lits = mlibThm.clause th value
290 val lits = mlibThm.clause th value
322 val lits = mlibThm.clause th value
445 val lits value
580 val lits = map (formula_subst sub) (literals cl) value
[all...] |
| H A D | mlibClauseset.sml | 286 val lits = map (fn lit => (FV lit, lit)) (literals cl) value
|
| /seL4-l4v-master/HOL4/src/HolSat/sat_solvers/zc2hs/ |
| H A D | zc2hs.cpp | 34 void addLit(int parsed_lit,vector<int>& lits, int& numvars) { argument
40 void addClause(vector<int>& lits, vec<vec<Lit> >& roots, parsed_clauses* pclauses, argument
69 vector<int> lits; local
75 addLit(atoi(stok.c_str()),lits,numvars); // first lit of first clause local
333 vec<Lit>& lits = clauses[c2c[ante]]; local
355 vec<Lit>& lits = clauses[c2c[conf_id]]; local
[all...] |
| /seL4-l4v-master/HOL4/src/pattern_matches/ |
| H A D | constrFamiliesLib.sml | 841 val lits = List.rev lits_rev value
935 val lits = HOLset.listItems ts value
[all...] |
| /seL4-l4v-master/HOL4/src/tfl/src/ |
| H A D | Induction.sml | 216 then let val lits = distinct col0 value
|