362 |
362 |
363 fun string_for_comp (aa1, aa2, cmp, xs) = |
363 fun string_for_comp (aa1, aa2, cmp, xs) = |
364 string_for_annotation_atom aa1 ^ " " ^ string_for_comp_op cmp ^ |
364 string_for_annotation_atom aa1 ^ " " ^ string_for_comp_op cmp ^ |
365 subscript_string_for_vars " \<and> " xs ^ " " ^ string_for_annotation_atom aa2 |
365 subscript_string_for_vars " \<and> " xs ^ " " ^ string_for_annotation_atom aa2 |
366 |
366 |
367 fun string_for_assign_clause [] = "\<bot>" |
367 fun string_for_assign_clause NONE = "\<top>" |
368 | string_for_assign_clause asgs = |
368 | string_for_assign_clause (SOME []) = "\<bot>" |
|
369 | string_for_assign_clause (SOME asgs) = |
369 space_implode " \<or> " (map string_for_assign_literal asgs) |
370 space_implode " \<or> " (map string_for_assign_literal asgs) |
370 |
371 |
371 fun add_assign_literal (x, (sn, a)) clauses = |
372 fun add_assign_literal (x, (sn, a)) clauses = |
372 if exists (fn [(x', (sn', a'))] => |
373 if exists (fn [(x', (sn', a'))] => |
373 x = x' andalso ((sn = sn' andalso a <> a') orelse |
374 x = x' andalso ((sn = sn' andalso a <> a') orelse |
504 val bools_from_annotation = AList.lookup (op =) bool_table #> the |
506 val bools_from_annotation = AList.lookup (op =) bool_table #> the |
505 val annotation_from_bools = AList.find (op =) bool_table #> the_single |
507 val annotation_from_bools = AList.find (op =) bool_table #> the_single |
506 |
508 |
507 fun prop_for_bool b = if b then PL.True else PL.False |
509 fun prop_for_bool b = if b then PL.True else PL.False |
508 fun prop_for_bool_var_equality (v1, v2) = |
510 fun prop_for_bool_var_equality (v1, v2) = |
509 PL.And (PL.Or (PL.BoolVar v1, PL.Not (PL.BoolVar v2)), |
511 PL.SAnd (PL.SOr (PL.BoolVar v1, PL.SNot (PL.BoolVar v2)), |
510 PL.Or (PL.Not (PL.BoolVar v1), PL.BoolVar v2)) |
512 PL.SOr (PL.SNot (PL.BoolVar v1), PL.BoolVar v2)) |
511 fun prop_for_assign (x, a) = |
513 fun prop_for_assign (x, a) = |
512 let val (b1, b2) = bools_from_annotation a in |
514 let val (b1, b2) = bools_from_annotation a in |
513 PL.And (PL.BoolVar (fst_var x) |> not b1 ? PL.Not, |
515 PL.SAnd (PL.BoolVar (fst_var x) |> not b1 ? PL.SNot, |
514 PL.BoolVar (snd_var x) |> not b2 ? PL.Not) |
516 PL.BoolVar (snd_var x) |> not b2 ? PL.SNot) |
515 end |
517 end |
516 fun prop_for_assign_literal (x, (Plus, a)) = prop_for_assign (x, a) |
518 fun prop_for_assign_literal (x, (Plus, a)) = prop_for_assign (x, a) |
517 | prop_for_assign_literal (x, (Minus, a)) = PL.Not (prop_for_assign (x, a)) |
519 | prop_for_assign_literal (x, (Minus, a)) = PL.SNot (prop_for_assign (x, a)) |
518 fun prop_for_atom_assign (A a', a) = prop_for_bool (a = a') |
520 fun prop_for_atom_assign (A a', a) = prop_for_bool (a = a') |
519 | prop_for_atom_assign (V x, a) = prop_for_assign_literal (x, (Plus, a)) |
521 | prop_for_atom_assign (V x, a) = prop_for_assign_literal (x, (Plus, a)) |
520 fun prop_for_atom_equality (aa1, A a2) = prop_for_atom_assign (aa1, a2) |
522 fun prop_for_atom_equality (aa1, A a2) = prop_for_atom_assign (aa1, a2) |
521 | prop_for_atom_equality (A a1, aa2) = prop_for_atom_assign (aa2, a1) |
523 | prop_for_atom_equality (A a1, aa2) = prop_for_atom_assign (aa2, a1) |
522 | prop_for_atom_equality (V x1, V x2) = |
524 | prop_for_atom_equality (V x1, V x2) = |
523 PL.And (prop_for_bool_var_equality (pairself fst_var (x1, x2)), |
525 PL.SAnd (prop_for_bool_var_equality (pairself fst_var (x1, x2)), |
524 prop_for_bool_var_equality (pairself snd_var (x1, x2))) |
526 prop_for_bool_var_equality (pairself snd_var (x1, x2))) |
525 val prop_for_assign_clause = PL.exists o map prop_for_assign_literal |
527 val prop_for_assign_clause = PL.exists o map prop_for_assign_literal |
526 fun prop_for_exists_var_assign_literal xs a = |
528 fun prop_for_exists_var_assign_literal xs a = |
527 PL.exists (map (fn x => prop_for_assign_literal (x, (Plus, a))) xs) |
529 PL.exists (map (fn x => prop_for_assign_literal (x, (Plus, a))) xs) |
528 fun prop_for_comp (aa1, aa2, Eq, []) = |
530 fun prop_for_comp (aa1, aa2, Eq, []) = |
529 PL.SAnd (prop_for_comp (aa1, aa2, Leq, []), |
531 PL.SAnd (prop_for_comp (aa1, aa2, Leq, []), |
530 prop_for_comp (aa2, aa1, Leq, [])) |
532 prop_for_comp (aa2, aa1, Leq, [])) |
531 | prop_for_comp (aa1, aa2, Neq, []) = |
533 | prop_for_comp (aa1, aa2, Neq, []) = |
532 PL.Not (prop_for_comp (aa1, aa2, Eq, [])) |
534 PL.SNot (prop_for_comp (aa1, aa2, Eq, [])) |
533 | prop_for_comp (aa1, aa2, Leq, []) = |
535 | prop_for_comp (aa1, aa2, Leq, []) = |
534 PL.SOr (prop_for_atom_equality (aa1, aa2), prop_for_atom_assign (aa2, Gen)) |
536 PL.SOr (prop_for_atom_equality (aa1, aa2), prop_for_atom_assign (aa2, Gen)) |
535 | prop_for_comp (aa1, aa2, cmp, xs) = |
537 | prop_for_comp (aa1, aa2, cmp, xs) = |
536 PL.SOr (prop_for_exists_var_assign_literal xs Gen, |
538 PL.SOr (prop_for_exists_var_assign_literal xs Gen, |
537 prop_for_comp (aa1, aa2, cmp, [])) |
539 prop_for_comp (aa1, aa2, cmp, [])) |
682 [(aa1, (Neq, Gen)), (aa2, (Eq, Tru)), (res_aa, (Eq, Gen))], |
684 [(aa1, (Neq, Gen)), (aa2, (Eq, Tru)), (res_aa, (Eq, Gen))], |
683 [(aa1, (Neq, New)), (aa2, (Eq, Tru)), (res_aa, (Eq, Gen))], |
685 [(aa1, (Neq, New)), (aa2, (Eq, Tru)), (res_aa, (Eq, Gen))], |
684 [(aa1, (Eq, Fls)), (aa2, (Neq, Gen)), (res_aa, (Eq, Gen))], |
686 [(aa1, (Eq, Fls)), (aa2, (Neq, Gen)), (res_aa, (Eq, Gen))], |
685 [(aa1, (Eq, Fls)), (aa2, (Neq, New)), (res_aa, (Eq, Gen))]] |
687 [(aa1, (Eq, Fls)), (aa2, (Neq, New)), (res_aa, (Eq, Gen))]] |
686 |
688 |
687 fun annotation_literal_from_quasi_literal (aa, (cmp, a)) = |
689 fun add_annotation_clause_from_quasi_clause _ NONE = NONE |
688 case aa of |
690 | add_annotation_clause_from_quasi_clause [] accum = accum |
689 A a' => if annotation_comp cmp a' a then NONE |
691 | add_annotation_clause_from_quasi_clause ((aa, (cmp, a)) :: rest) accum = |
690 else (trace_msg (K "**** Unsolvable"); raise UNSOLVABLE ()) |
692 case aa of |
691 | V x => SOME (x, (sign_for_comp_op cmp, a)) |
693 A a' => if annotation_comp cmp a' a then NONE |
692 |
694 else add_annotation_clause_from_quasi_clause rest accum |
693 val assign_clause_from_quasi_clause = |
695 | V x => add_annotation_clause_from_quasi_clause rest accum |
694 map_filter annotation_literal_from_quasi_literal |
696 |> Option.map (cons (x, (sign_for_comp_op cmp, a))) |
695 val add_quasi_clause = assign_clause_from_quasi_clause #> add_assign_clause |
697 |
|
698 fun assign_clause_from_quasi_clause clause = |
|
699 add_annotation_clause_from_quasi_clause clause (SOME []) |
696 |
700 |
697 fun add_connective_var conn mk_quasi_clauses res_aa aa1 aa2 = |
701 fun add_connective_var conn mk_quasi_clauses res_aa aa1 aa2 = |
698 (trace_msg (fn () => "*** Add " ^ string_for_annotation_atom res_aa ^ " = " ^ |
702 (trace_msg (fn () => "*** Add " ^ string_for_annotation_atom res_aa ^ " = " ^ |
699 string_for_annotation_atom aa1 ^ " " ^ conn ^ " " ^ |
703 string_for_annotation_atom aa1 ^ " " ^ conn ^ " " ^ |
700 string_for_annotation_atom aa2); |
704 string_for_annotation_atom aa2); |
701 fold add_quasi_clause (mk_quasi_clauses res_aa aa1 aa2)) |
705 fold (add_assign_clause o assign_clause_from_quasi_clause) |
702 |
706 (mk_quasi_clauses res_aa aa1 aa2)) |
703 fun add_connective_frames conn mk_quasi_clauses res_frame frame1 frame2 = |
707 fun add_connective_frames conn mk_quasi_clauses res_frame frame1 frame2 = |
704 fold I (map3 (fn (_, res_aa) => fn (_, aa1) => fn (_, aa2) => |
708 fold I (map3 (fn (_, res_aa) => fn (_, aa1) => fn (_, aa2) => |
705 add_connective_var conn mk_quasi_clauses res_aa aa1 aa2) |
709 add_connective_var conn mk_quasi_clauses res_aa aa1 aa2) |
706 res_frame frame1 frame2) |
710 res_frame frame1 frame2) |
707 |
711 |
727 | add_annotation_atom_comp_alt _ (A _) _ _ = |
731 | add_annotation_atom_comp_alt _ (A _) _ _ = |
728 (trace_msg (K "*** Expected G"); raise UNSOLVABLE ()) |
732 (trace_msg (K "*** Expected G"); raise UNSOLVABLE ()) |
729 | add_annotation_atom_comp_alt cmp (V x) aa1 aa2 = |
733 | add_annotation_atom_comp_alt cmp (V x) aa1 aa2 = |
730 add_annotation_atom_comp cmp [x] aa1 aa2 |
734 add_annotation_atom_comp cmp [x] aa1 aa2 |
731 |
735 |
732 fun add_arg_order1 ((_, aa), (_, prev_aa)) = |
736 fun add_arg_order1 ((_, aa), (_, prev_aa)) = I |
733 add_annotation_atom_comp_alt Neq prev_aa (A Gen) aa |
737 add_annotation_atom_comp_alt Neq prev_aa (A Gen) aa |
734 fun add_app1 fun_aa ((_, res_aa), (_, arg_aa)) = |
738 fun add_app1 fun_aa ((_, res_aa), (_, arg_aa)) = I |
735 add_annotation_atom_comp_alt Leq arg_aa fun_aa res_aa |
739 let |
736 ##> add_quasi_clause [(arg_aa, (Neq, Gen)), (res_aa, (Eq, Gen))] |
740 val clause = [(arg_aa, (Eq, New)), (res_aa, (Eq, Gen))] |
|
741 |> assign_clause_from_quasi_clause |
|
742 in |
|
743 trace_msg (fn () => "*** Add " ^ string_for_assign_clause clause); |
|
744 apsnd (add_assign_clause clause) |
|
745 #> add_annotation_atom_comp_alt Leq arg_aa fun_aa res_aa |
|
746 end |
737 fun add_app _ [] [] = I |
747 fun add_app _ [] [] = I |
738 | add_app fun_aa res_frame arg_frame = |
748 | add_app fun_aa res_frame arg_frame = |
739 add_comp_frame (A New) Leq arg_frame |
749 add_comp_frame (A New) Leq arg_frame |
740 #> fold add_arg_order1 (tl arg_frame ~~ (fst (split_last arg_frame))) |
750 #> fold add_arg_order1 (tl arg_frame ~~ (fst (split_last arg_frame))) |
741 #> fold (add_app1 fun_aa) (res_frame ~~ arg_frame) |
751 #> fold (add_app1 fun_aa) (res_frame ~~ arg_frame) |