Searched refs:lits (Results 1 - 25 of 41) sorted by relevance

12

/seL4-l4v-master/HOL4/src/HolSat/sat_solvers/zc2hs/
H A Dzc2hs.cpp34 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 DMain.C32 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 DSubsume.sml30 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 DLiteral.sml241 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 DRewrite.sml165 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 DWaiting.sml78 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 DProof.sml181 | 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 DClause.sml119 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 DProblem.sml23 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 DSubsume.sml30 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 DLiteral.sml241 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 DRewrite.sml165 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 DWaiting.sml78 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 DProof.sml181 | 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 DClause.sml119 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 DProblem.sml23 fun lits (cl,n) = n + LiteralSet.size cl function
32 literals = List.foldl lits 0 cls,
/seL4-l4v-master/HOL4/src/metis/
H A DmlibSubsume.sml58 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 DmlibUnits.sml102 fun prove (INL th) lits = SOME (map (fn lit => CONTR lit th) lits)
103 | prove (INR uns) lits = uprove uns lits;
H A DmlibClause.sml272 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 DfolMapping.sml321 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 DmlibClauseset.sml250 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 DQbfCertificate.sml64 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 DQbfLibrary.sml192 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 Dho_proverTools.sml99 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 DconstrFamiliesLib.sml840 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...]

Completed in 156 milliseconds

12