191 handle TERM _ => th; (*probably dest_Trueprop on a weird theorem*) |
191 handle TERM _ => th; (*probably dest_Trueprop on a weird theorem*) |
192 |
192 |
193 |
193 |
194 (*** The basic CNF transformation ***) |
194 (*** The basic CNF transformation ***) |
195 |
195 |
|
196 val max_clauses = ref 20; |
|
197 |
|
198 fun sum x y = if x < !max_clauses andalso y < !max_clauses then x+y else !max_clauses; |
|
199 fun prod x y = if x < !max_clauses andalso y < !max_clauses then x*y else !max_clauses; |
|
200 |
196 (*Estimate the number of clauses in order to detect infeasible theorems*) |
201 (*Estimate the number of clauses in order to detect infeasible theorems*) |
197 fun nclauses (Const("Trueprop",_) $ t) = nclauses t |
202 fun signed_nclauses b (Const("Trueprop",_) $ t) = signed_nclauses b t |
198 | nclauses (Const("op &",_) $ t $ u) = nclauses t + nclauses u |
203 | signed_nclauses b (Const("Not",_) $ t) = signed_nclauses (not b) t |
199 | nclauses (Const("Ex", _) $ Abs (_,_,t)) = nclauses t |
204 | signed_nclauses b (Const("op &",_) $ t $ u) = |
200 | nclauses (Const("All",_) $ Abs (_,_,t)) = nclauses t |
205 if b then sum (signed_nclauses b t) (signed_nclauses b u) |
201 | nclauses (Const("op |",_) $ t $ u) = nclauses t * nclauses u |
206 else prod (signed_nclauses b t) (signed_nclauses b u) |
202 | nclauses _ = 1; (* literal *) |
207 | signed_nclauses b (Const("op |",_) $ t $ u) = |
|
208 if b then prod (signed_nclauses b t) (signed_nclauses b u) |
|
209 else sum (signed_nclauses b t) (signed_nclauses b u) |
|
210 | signed_nclauses b (Const("op -->",_) $ t $ u) = |
|
211 if b then prod (signed_nclauses (not b) t) (signed_nclauses b u) |
|
212 else sum (signed_nclauses (not b) t) (signed_nclauses b u) |
|
213 | signed_nclauses b (Const("op =",_) $ t $ u) = |
|
214 if b then sum (prod (signed_nclauses (not b) t) (signed_nclauses b u)) |
|
215 (prod (signed_nclauses (not b) u) (signed_nclauses b t)) |
|
216 else sum (prod (signed_nclauses b t) (signed_nclauses b u)) |
|
217 (prod (signed_nclauses (not b) t) (signed_nclauses (not b) u)) |
|
218 | signed_nclauses b (Const("Ex", _) $ Abs (_,_,t)) = signed_nclauses b t |
|
219 | signed_nclauses b (Const("All",_) $ Abs (_,_,t)) = signed_nclauses b t |
|
220 | signed_nclauses _ _ = 1; (* literal *) |
|
221 |
|
222 val nclauses = signed_nclauses true; |
|
223 |
|
224 fun too_many_clauses t = nclauses t >= !max_clauses; |
203 |
225 |
204 (*Replaces universally quantified variables by FREE variables -- because |
226 (*Replaces universally quantified variables by FREE variables -- because |
205 assumptions may not contain scheme variables. Later, call "generalize". *) |
227 assumptions may not contain scheme variables. Later, call "generalize". *) |
206 fun freeze_spec th = |
228 fun freeze_spec th = |
207 let val newname = gensym "mes_" |
229 let val newname = gensym "mes_" |
245 (fn st' => st' |> METAHYPS (resop cnf_nil) 1) |
267 (fn st' => st' |> METAHYPS (resop cnf_nil) 1) |
246 in Seq.list_of (tac (th RS disj_forward)) @ ths end |
268 in Seq.list_of (tac (th RS disj_forward)) @ ths end |
247 | _ => (*no work to do*) th::ths |
269 | _ => (*no work to do*) th::ths |
248 and cnf_nil th = cnf_aux (th,[]) |
270 and cnf_nil th = cnf_aux (th,[]) |
249 in |
271 in |
250 if nclauses (concl_of th) > 20 |
272 if too_many_clauses (concl_of th) |
251 then (Output.debug ("cnf is ignoring: " ^ string_of_thm th); ths) |
273 then (Output.debug ("cnf is ignoring: " ^ string_of_thm th); ths) |
252 else cnf_aux (th,ths) |
274 else cnf_aux (th,ths) |
253 end; |
275 end; |
254 |
276 |
255 (*Convert all suitable free variables to schematic variables, |
277 (*Convert all suitable free variables to schematic variables, |