Lines Matching refs:cl
79 fun clause_to_string cl =
80 PP.pp_to_string (!LINE_LENGTH) mlibClause.pp_clause cl;
152 and check set sos n (d,cl) =
153 case ofilt (not o mlibClauseset.subsumed set) (beef_up set cl) of
155 | SOME cl => (n, SOME ((d,cl),sos));
164 | SOME ((d,cl),sos) =>
167 val {order_stickiness, ...} = #parm (mlibClause.dest_clause cl)
168 val cl = if order_stickiness <= 2 then mlibClause.drop_order cl else cl
169 val set = mlibClauseset.add cl set
172 SOME ((d,cl),res)
177 fun deduce cl res =
180 chat ("\ngiven clause:\n" ^ clause_to_string cl ^ "\n")
182 val cl = mlibClause.FRESH_VARS cl
183 val cls = mlibClauseset.deduce set cl
210 | SOME ((d,cl),res) =>
212 val cls = deduce cl res
256 and g (dcl as (_,cl), res) =
257 if not (mlibClause.is_empty cl) then h dcl res
258 else (swipe res; S.CONS (SOME cl, stat (h dcl o shove) res))
259 and h (d,cl) res =
261 val cls = deduce cl res