Lines Matching defs:tb
145 val tb = if (Option.isSome absf) then (* FIXME: can we remove the reference to absf? *)
151 (*val _ = dbgTools.DTM (dpfx^ (getTerm tb)) val _ = dbgTools.DST (dpfx^ "(tb)\n") (*DBG*)*)
152 val res = BddEqMp sth tb
171 val _ = dbgTools.DST (dpfx^ "rv tb sth\n") (*DBG*)
177 val _ = dbgTools.DST (dpfx^ "rv tb\n") (*DBG*)*)
183 fun mk_rv_spec_thm msr seth sel msreq ie ee state (tb,gth,sth,env,ix,rsc,ithm,abthm,_,_) dp mf =
295 let val (tb,gth,sth,env,ix,rsc,ithm,abthm,ado_subthm,ado_eqthm) = !cch
308 if (Option.isSome tb)
309 then Option.valOf tb
312 then let val tb = tb_func mf (Option.valOf sth)
313 val _ = upd_cch_tb cch tb
314 in tb end
322 val tb = tb_func mf sth
323 val _ = upd_cch_tb cch tb val _ = upd_cch_sth cch sth
324 in tb end
332 val tb = tb_func mf sth
333 val _ = upd_cch_tb cch tb val _ = upd_cch_sth cch sth val _ = upd_cch_gth cch gth
334 in tb end
336 if (Option.isSome tb andalso (check_rv rsc dp))
341 (*val _ = dbgTools.DTM (dpfx^ (getTerm (Option.valOf tb))) (*DBG*)
342 val _ = dbgTools.DST (dpfx^ " cached tb\n") (*DBG*)
343 val _ = if then let val _ = print _rsc rsc "cached tb" in () end else () (*DBG*)*)
355 val tb = BddEqMp sithm (Option.valOf tb)
356 val _ = dbgTools.DST (dpfx^"cg_ tb cache read done\n")
357 val _ = upd_cch_tb cch tb val _ = upd_cch_sth cch sth1 val _ = upd_cch_env cch ie
358 in tb end
360 else (* otherwise we have to recompute this tb (however note that no clean subformula will be recomputed) *)
364 val tb = tb_func mf sth
365 val _ = upd_cch_tb cch tb val _ = upd_cch_sth cch sth val _ = upd_cch_env cch ie
366 in tb end
372 val tb = tb_func mf sth
373 val _ = upd_cch_tb cch tb val _ = upd_cch_sth cch sth
375 in tb end
396 val tb = cache_get cch ie (mk_ap_tb vm absf) (mk_gen_ap_thm ksname state msa) dp [] mf seth sel state
398 in tb end
401 val tb = cache_get cch ie (mk_rv_tb ee (!cch)) (mk_rv_spec_thm msr seth sel msreq ie ee state (!cch) dp) dp []
404 in tb end
408 val tb = cache_get cch ie (BinExp (args,(seth,sel,state,ie)) bdd.And (snd(strip_comb(mf))) vm (f1,f2) dp abthm)
412 in tb end
416 val tb = cache_get cch ie (BinExp (args,(seth,sel,state,ie)) bdd.Or (snd(strip_comb(mf))) vm (f1,f2) dp abthm)
420 in tb end
424 val tb = cache_get cch ie (NotExp (args,(seth,sel,state,ie)) mf1 vm dp f1 abthm)
426 in tb end
434 val tb = cache_get cch ie (ModalExp (args,(seth,sel,state,ie)) act false (List.last(snd(strip_comb mf)))
437 in tb end
441 val tb = cache_get cch ie (ModalExp (args,(seth,sel,state,ie)) act true (List.last(snd(strip_comb mf)))
444 in tb end
449 val tb = cache_get cch ie (FixExp (args,(seth,sel,state,ie)) [rvnm,cabthmnm] (BddCon false vm) vm
452 in tb end
457 val tb = cache_get cch ie (FixExp (args,(seth,sel,state,ie)) [rvnm,cabthmnm] (BddCon true vm) vm
460 in tb end
465 val tb = BddNot (muCheck_aux (args,(seth,sel,state,ie)) mf1 vm dp f1)
467 (*val _ = dbgTools.DTM (dpfx^ (getTerm tb)) val _ = dbgTools.DST (dpfx^ " NotExp tb\n")
471 val tb2 = BddEqMp sth tb
490 val tb =BddEqMp opthm bb
493 in tb end
754 val rvl = Array.foldr (fn((rv,tb),l)=> (rv,getTerm tb)::l) [] ee
823 fun finish tb frv_thms =
826 val unfrv = BddApConv (ONCE_REWRITE_CONV [frv_find frv_thms (List.hd(snd(strip_comb(getTerm tb))))]) tb
908 fun checkResult tb mf ks_def (I1,Itb,ITdf) state ie vm =
912 val _ = dbgTools.DTB (dpfx^"cr_tb") tb (*DBG*)
913 val _ = dbgTools.DBD (dpfx^"cr_tb_bdd") (getBdd tb) (*DBG*)
914 (*val _ = dbgTools.DTM (dpfx^ (getTerm tb)) val _ = dbgTools.DST (dpfx^ " tb\n") (*DBG*)
915 val _ = List.app (fn t => let val _ = dbgTools.DTM (dpfx^ t) val _ = dbgTools.DST (dpfx^" tb assum\n") in () end)
916 (HOLset.listItems (getAssums tb))(*DBG*)*)
931 val Itb3 = (BddOp(bdd.Imp,Itb2,tb))
959 val tb = muCheck_aux (init_stuff,(seth,sel,state,ie)) mf vm ((Array.length ee)-1) mfml
960 val res_tb = finish tb frv_thms
1012 val actl = List.filter (fn (nm,tb) => bdd.equal bdd.TRUE (getBdd tb)) (ListPair.zip(acts,restbs))