Lines Matching refs:f2
379 fun get_abthms mf f1 f2 cch =
380 let (*FIXME: don't do the extra work if f1 and f2 are the same *)
387 val cab2 = #8(get_cache_entry mf2 f2)
405 | muCheck_aux (args as (msp,_,_,_,_),(seth,sel,state,ie)) mf vm dp (muAnd(cch,(f1,f2))) =
407 val (abthm,abthnm,mf1,mf2,cab1,cab1nm,cab2,cab2nm) = get_abthms mf f1 f2 cch
408 val tb = cache_get cch ie (BinExp (args,(seth,sel,state,ie)) bdd.And (snd(strip_comb(mf))) vm (f1,f2) dp abthm)
411 (List.nth(msp,3)))) dp [f1,f2] mf seth sel state
413 | muCheck_aux (args as (msp,_,_,_,_),(seth,sel,state,ie)) mf vm dp (muOr(cch,(f1,f2))) =
415 val (abthm,abthnm,mf1,mf2,cab1,cab1nm,cab2,cab2nm) = get_abthms mf f1 f2 cch
416 val tb = cache_get cch ie (BinExp (args,(seth,sel,state,ie)) bdd.Or (snd(strip_comb(mf))) vm (f1,f2) dp abthm)
419 (List.nth(msp,4)))) dp [f1,f2] mf seth sel state
476 and BinExp (args,(seth,sel,state,ie)) opr [t1,t2] vm (f1,f2) dp abthm mf opthm =
482 val b2 = muCheck_aux (args,(seth,sel,state,ie)) t2 vm dp f2