/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 37 lits.push_back( (parsed_lit > 0) ? var+var : var+var+1 ); 40 void addClause(vector<int>& lits, vec<vec<Lit> >& roots, parsed_clauses* pclauses, argument 43 sort(lits.begin(),lits.end()); 44 lits.erase(unique(lits.begin(),lits.end()),lits.end()); //sortUnique(lits); 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/HolSat/sat_solvers/minisat/ |
H A D | Main.C | 32 void addLit(int parsed_lit,Solver& S, vec<Lit>& lits) { argument 35 lits.push( (parsed_lit > 0) ? Lit(var) : ~Lit(var) ); 38 void addClause(Solver& S, vec<Lit>& lits) { argument 39 /*for (int i=0;i<lits.size();i++) 40 cout << (sign(lits[i]) ? "-" : "") << (var(lits[i])+1) << " "; 42 S.addClause(lits); 43 lits.clear(); 51 vec<Lit> lits; local 57 addLit(atoi(stok.c_str()),S,lits); // firs local [all...] |
/seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
H A D | Subsume.sml | 30 fun clauseSym lits = List.foldl addSym lits lits; 35 val lits = LiteralSet.toList cl value 37 sortMap Literal.typedSymbols (revCompare Int.compare) lits 42 val lits = clauseSym [lit] value 44 fn lit' => not (List.exists (can (Literal.unify Subst.empty lit')) lits) 125 val lits' = otherLits @ [fstLit,sndLit] 126 val clauses = IntMap.insert clauses (nextId,(lits',cl',a)) 174 fun genClauseSubsumes pred cl' lits' c 323 and lits = clauseSym (LiteralSet.toList cl) value [all...] |
H A D | Literal.sml | 241 fun f (lits,set) = NameSet.union set (freeVars lits) 260 fun subst sub lits = 262 fun substLit (lit,(eq,lits')) = 267 (eq, add lits' lit') 270 val (eq,lits') = foldl substLit (true,empty) lits 272 if eq then lits else lits'
|
H A D | Rewrite.sml | 165 fun literalsReducible order known id lits = 166 LiteralSet.exists (literalReducible order known id) lits; 305 fun add (lit,(neq,lits)) = 307 SOME neq => (neq,lits) 308 | NONE => (neq, LiteralSet.add lits lit) 354 fun rewriteIdLiteralsRule' order known redexes id lits th = 358 fun rewr_neq_lit (lit, acc as (changed,neq,lits,th)) = 369 SOME neq => (true,neq,lits,th) 370 | NONE => (changed, neq, LiteralSet.add lits lit', th) 374 fun rewr_neq_lits neq lits t [all...] |
H A D | Waiting.sml | 78 val lits = Clause.literals cl value 79 val fvs = LiteralSet.freeVars lits 81 (fvs,lits) 161 val lits = Clause.literals cl value 162 val symbolsW = Math.pow (clauseSymbols lits, symbolsWeight) 163 val variablesW = Math.pow (clauseVariables lits, variablesWeight) 164 val literalsW = Math.pow (clauseLiterals lits, literalsWeight)
|
H A D | Proof.sml | 181 | recon ((lit :: lits, sub) :: others) = 186 | SOME sub => (lits,sub) :: acc 208 val lits = LiteralSet.intersectList [cl1,cl1',cl2,cl2'] value 210 if not (LiteralSet.null lits) then LiteralSet.pick lits 424 (_, Axiom lits) => LiteralSet.freeIn v lits 440 (_, Axiom lits) => LiteralSet.freeVars lits
|
H A D | Clause.sml | 119 fun isLargerLiteral ({ordering,orderLiterals,...} : parameters) lits = 126 val tms = LiteralSet.foldl addLit [] lits 131 case LiteralSet.findl (K true) lits of 138 val tms = LiteralSet.foldl addLit [] lits 260 val lits = largestLiterals cl value 264 List.map apply (Rule.factor' lits)
|
H A D | Problem.sml | 23 fun lits (cl,n) = n + LiteralSet.size cl function 32 literals = List.foldl lits 0 cls,
|
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Subsume.sml | 30 fun clauseSym lits = List.foldl addSym lits lits; 35 val lits = LiteralSet.toList cl value 37 sortMap Literal.typedSymbols (revCompare Int.compare) lits 42 val lits = clauseSym [lit] value 44 fn lit' => not (List.exists (can (Literal.unify Subst.empty lit')) lits) 125 val lits' = otherLits @ [fstLit,sndLit] 126 val clauses = IntMap.insert clauses (nextId,(lits',cl',a)) 174 fun genClauseSubsumes pred cl' lits' c 323 and lits = clauseSym (LiteralSet.toList cl) value [all...] |
H A D | Literal.sml | 241 fun f (lits,set) = NameSet.union set (freeVars lits) 260 fun subst sub lits = 262 fun substLit (lit,(eq,lits')) = 267 (eq, add lits' lit') 270 val (eq,lits') = foldl substLit (true,empty) lits 272 if eq then lits else lits'
|
H A D | Rewrite.sml | 165 fun literalsReducible order known id lits = 166 LiteralSet.exists (literalReducible order known id) lits; 305 fun add (lit,(neq,lits)) = 307 SOME neq => (neq,lits) 308 | NONE => (neq, LiteralSet.add lits lit) 354 fun rewriteIdLiteralsRule' order known redexes id lits th = 358 fun rewr_neq_lit (lit, acc as (changed,neq,lits,th)) = 369 SOME neq => (true,neq,lits,th) 370 | NONE => (changed, neq, LiteralSet.add lits lit', th) 374 fun rewr_neq_lits neq lits t [all...] |
H A D | Waiting.sml | 78 val lits = Clause.literals cl value 79 val fvs = LiteralSet.freeVars lits 81 (fvs,lits) 161 val lits = Clause.literals cl value 162 val symbolsW = Math.pow (clauseSymbols lits, symbolsWeight) 163 val variablesW = Math.pow (clauseVariables lits, variablesWeight) 164 val literalsW = Math.pow (clauseLiterals lits, literalsWeight)
|
H A D | Proof.sml | 181 | recon ((lit :: lits, sub) :: others) = 186 | SOME sub => (lits,sub) :: acc 208 val lits = LiteralSet.intersectList [cl1,cl1',cl2,cl2'] value 210 if not (LiteralSet.null lits) then LiteralSet.pick lits 424 (_, Axiom lits) => LiteralSet.freeIn v lits 440 (_, Axiom lits) => LiteralSet.freeVars lits
|
H A D | Clause.sml | 119 fun isLargerLiteral ({ordering,orderLiterals,...} : parameters) lits = 126 val tms = LiteralSet.foldl addLit [] lits 131 case LiteralSet.findl (K true) lits of 138 val tms = LiteralSet.foldl addLit [] lits 260 val lits = largestLiterals cl value 264 List.map apply (Rule.factor' lits)
|
H A D | Problem.sml | 23 fun lits (cl,n) = n + LiteralSet.size cl function 32 literals = List.foldl lits 0 cls,
|
/seL4-l4v-master/HOL4/src/metis/ |
H A D | mlibSubsume.sml | 58 fun psymize lits = List.mapPartial (total psym) lits @ lits; 81 (* Assumes flits has already been extended with symmetries of equality lits. *) 120 fun add (lits |-> a) (SUBSUME {zero,one,many}) = 122 (case sort_literals lits of 128 val k = (i, length lits)
|
H A D | mlibUnits.sml | 102 fun prove (INL th) lits = SOME (map (fn lit => CONTR lit th) lits) 103 | prove (INR uns) lits = uprove uns lits;
|
H A D | mlibClause.sml | 272 val lits = mlibThm.clause th value 273 val objs = objects lits 279 List.mapPartial (total collect) (enumerate 0 lits) 290 val lits = mlibThm.clause th value 291 val objs = objects lits 303 foldl f [] (enumerate 0 lits) 322 val lits = mlibThm.clause th value 323 val objs = objects lits 347 foldl collect [] (enumerate 0 lits) 445 val lits value 580 val lits = map (formula_subst sub) (literals cl) value [all...] |
H A D | folMapping.sml | 321 fun finalize_lits (lits, th) = 322 case rev lits of [] => th 532 fun hol_literals_to_fol parm (vars, lits) = 533 map (hol_literal_to_fol parm vars) lits; 634 val lits = try hol_literals_to_fol parm 637 val [lit1, lit2] = lits; 703 fun freshen (lits, th) = 704 if #with_types parm then (lits, th) 706 let val sub = fresh_tyvars lits 707 in (map (inst sub) lits, INST_T [all...] |
H A D | mlibClauseset.sml | 250 fun AX cl lits = mk_clause (#parm (dest_clause cl)) (mlibThm.AXIOM lits); 256 fun add_lits lits shar = foldl (fn ((_,x),l) => x :: l) lits shar; 259 fun dfs acc lits vars vlits = 261 (_,[]) => components (rev lits :: acc) vlits 262 | (disj,shar) => dfs acc (add_lits lits shar) (add_vars vars shar) disj 286 val lits = map (fn lit => (FV lit, lit)) (literals cl) value 287 val (glits,vlits) = List.partition (null o fst) lits
|
/seL4-l4v-master/HOL4/src/HolQbf/ |
H A D | QbfCertificate.sml | 64 fun extension_lits lits ["0"] = 65 List.rev lits 72 | extension_lits lits (literal :: xs) = 73 extension_lits (int_from_string literal :: lits) xs 78 | extension ext (vindex :: "A" :: lits) = 80 AND (extension_lits [] lits)) 100 | resolution_args lits ("0" :: xs) = 101 (List.rev lits, resolution_clauses [] xs) 102 | resolution_args lits (lit :: xs) = 103 resolution_args (int_from_string lit :: lits) x 384 val lits = QbfLibrary.literals_in_clause index_fn clause value [all...] |
H A D | QbfLibrary.sml | 192 lits as (j, lit, l_is_forall) :: littail) = 198 val (thm, lits') = if i < Int.abs j then 199 (thm, lits) 204 forall_reduce (thm, vartail, hyp, lits') 212 forall_reduce (thm, vartail, hyp, lits) 215 (thm, vars, hyp, lits) 265 val (lits, p, p', p_is_pos) = find_pivot [] lits1 lits2 value 290 forall_reduce (th, vars, hyp, lits)
|
/seL4-l4v-master/HOL4/examples/miller/ho_prover/ |
H A D | ho_proverTools.sml | 99 fun literals_term lits = 100 (case map literal_term (rev lits) of [] => F 103 fun clause_term (CLAUSE ((v, _), lits)) = mk_foralls (v, literals_term lits); 151 fun clause_canon_vars (CLAUSE (vars, lits)) = 152 CLAUSE (canon_tm vars (map snd lits), lits); 227 fun reassem previous next (sub, vars, lits, vf) = 232 (sub, CLAUSE (vars, previous' @ lits @ next'), vf) 242 fn CLAUSE (vars, lits) [all...] |
/seL4-l4v-master/HOL4/src/pattern_matches/ |
H A D | constrFamiliesLib.sml | 840 val _ = if (List.null lits_rev) then (failwith "" "no lits") else () 841 val lits = List.rev lits_rev value 842 val cases_no = List.length lits + 1 850 fun mk_expand_thm lits = case lits of 852 | (l :: lits') => let 856 val thm2a = mk_expand_thm lits' 862 val thm0 = mk_expand_thm lits 875 fun mk_lits_preconds (sua, sub, c_tms) pre lits = 876 case lits o 935 val lits = HOLset.listItems ts value [all...] |