Lines Matching refs:cl
104 fun clause_to_formula cl = list_mk_disj (C.literals cl);
108 fun clause_to_string cl = PP.pp_to_string (!LINE_LENGTH) mlibClause.pp_clause cl;
154 | clause_sat wmods cl n =
156 val fm = clause_to_formula cl
169 fun clause_weight (parm : parameters) clsat dist cl =
172 val {id, ...} = C.dest_clause cl
173 val siz = Math.pow (clause_size cl, size_power)
174 val lit = Math.pow (clause_lits cl, literal_power)
178 chat ("clause_weight: " ^ clause_to_string cl ^ " -> " ^
266 fun add1 dist (cl,sos) =
270 val {id,...} = C.dest_clause cl
274 val sat = clause_sat models cl model_checks
275 val weight = clause_weight parm sat dist cl
276 val sos = update_clauses (H.add (weight,(dist,cl)) clauses) sos
311 | SOME ((_,cl),sos) => f (cl :: acc) sos;