Searched refs:addLit (Results 1 - 4 of 4) sorted by relevance
| /seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
| H A D | Clause.sml | 124 fun addLit ((_,atm),acc) = atomToTerms atm @ acc function
126 val tms = LiteralSet.foldl addLit [] lits
135 fun addLit ((p,atm),acc) = function
138 val tms = LiteralSet.foldl addLit [] lits
150 fun addLit (lit,s) = if isLarger lit then LiteralSet.add s lit else s function
152 LiteralSet.foldr addLit LiteralSet.empty litSet
172 fun addLit (lit,acc) = function
183 LiteralSet.foldr addLit [] (largestLiterals cl)
187 fun addLit (lit,acc) = function
194 fun largestSubterms cl = LiteralSet.foldl addLit [] (largestLiteral
[all...] |
| /seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
| H A D | Clause.sml | 124 fun addLit ((_,atm),acc) = atomToTerms atm @ acc function
126 val tms = LiteralSet.foldl addLit [] lits
135 fun addLit ((p,atm),acc) = function
138 val tms = LiteralSet.foldl addLit [] lits
150 fun addLit (lit,s) = if isLarger lit then LiteralSet.add s lit else s function
152 LiteralSet.foldr addLit LiteralSet.empty litSet
172 fun addLit (lit,acc) = function
183 LiteralSet.foldr addLit [] (largestLiterals cl)
187 fun addLit (lit,acc) = function
194 fun largestSubterms cl = LiteralSet.foldl addLit [] (largestLiteral
[all...] |
| /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) { function
57 addLit(atoi(stok.c_str()),S,lits); // first lit of first clause
65 else addLit(itok,S,lits);
|
| /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) { function
75 addLit(atoi(stok.c_str()),lits,numvars); // first lit of first clause
83 else addLit(itok,lits,numvars);
|
Completed in 41 milliseconds