Lines Matching defs:fm
135 fun sat_clause m n fm =
136 if small_space (M.size m) n (length (FV fm)) 1 then M.count m fm
137 else (M.checkn m fm n, n);
139 fun sat_mod_fm m fm n =
140 let val (i,k) = sat_clause m n fm
147 let val sum = foldl (fn (fm,x) => sat_mod_fm m fm n + x) 0.0 fms
151 fun sat_wmod_fm (w,m) fm n = w * (sat_mod_fm m fm n) + (1.0 - w);
156 val fm = clause_to_formula cl
157 val sum = foldl (fn (wmod,x) => sat_wmod_fm wmod fm n + x) 0.0 wmods
224 fun is_prob_taut n fm = List.all (fn m => M.checkn m fm n = n) test_models;