equal
deleted
inserted
replaced
531 val need_us = need_us |> map (rename_vars_in_nut pool rel_table) |
531 val need_us = need_us |> map (rename_vars_in_nut pool rel_table) |
532 val nondef_fs = map (kodkod_formula_from_nut ofs kk) nondef_us |
532 val nondef_fs = map (kodkod_formula_from_nut ofs kk) nondef_us |
533 val def_fs = map (kodkod_formula_from_nut ofs kk) def_us |
533 val def_fs = map (kodkod_formula_from_nut ofs kk) def_us |
534 val formula = fold (fold s_and) [def_fs, nondef_fs] KK.True |
534 val formula = fold (fold s_and) [def_fs, nondef_fs] KK.True |
535 val comment = (if unsound then "unsound" else "sound") ^ "\n" ^ |
535 val comment = (if unsound then "unsound" else "sound") ^ "\n" ^ |
536 Print_Mode.setmp [] multiline_string_for_scope scope |
536 multiline_string_for_scope scope |
537 val kodkod_sat_solver = |
537 val kodkod_sat_solver = |
538 Kodkod_SAT.sat_solver_spec actual_sat_solver |> snd |
538 Kodkod_SAT.sat_solver_spec actual_sat_solver |> snd |
539 val bit_width = if bits = 0 then 16 else bits + 1 |
539 val bit_width = if bits = 0 then 16 else bits + 1 |
540 val delay = |
540 val delay = |
541 if unsound then |
541 if unsound then |