44 val ord = fn ((s, _ : string list), (s', _)) => fast_string_ord (s, s') |
44 val ord = fn ((s, _ : string list), (s', _)) => fast_string_ord (s, s') |
45 val string_of = fst) |
45 val string_of = fst) |
46 |
46 |
47 open String_Redirect |
47 open String_Redirect |
48 |
48 |
49 val e_skolemize_rule = "skolemize" |
49 val e_skolemize_rules = ["skolemize", "shift_quantors"] |
50 val vampire_skolemisation_rule = "skolemisation" |
50 val vampire_skolemisation_rule = "skolemisation" |
51 (* TODO: Use "Z3_Proof.string_of_rule" once it is moved to Isabelle *) |
51 (* TODO: Use "Z3_Proof.string_of_rule" once it is moved to Isabelle *) |
52 val z3_apply_def_rule = "apply-def" |
52 val z3_apply_def_rule = "apply-def" |
53 val z3_hypothesis_rule = "hypothesis" |
53 val z3_hypothesis_rule = "hypothesis" |
54 val z3_intro_def_rule = "intro-def" |
54 val z3_intro_def_rule = "intro-def" |
55 val z3_lemma_rule = "lemma" |
55 val z3_lemma_rule = "lemma" |
56 val z3_skolemize_rule = "sk" |
56 val z3_skolemize_rule = "sk" |
57 val z3_th_lemma_rule = "th-lemma" |
57 val z3_th_lemma_rule = "th-lemma" |
58 |
58 |
59 val is_skolemize_rule = |
59 val skolemize_rules = e_skolemize_rules @ [vampire_skolemisation_rule, z3_skolemize_rule] |
60 member (op =) [e_skolemize_rule, vampire_skolemisation_rule, z3_skolemize_rule] |
60 |
61 |
61 val is_skolemize_rule = member (op =) skolemize_rules |
62 val is_arith_rule = String.isPrefix z3_th_lemma_rule |
62 val is_arith_rule = String.isPrefix z3_th_lemma_rule |
63 |
63 |
64 fun raw_label_of_num num = (num, 0) |
64 fun raw_label_of_num num = (num, 0) |
65 |
65 |
66 fun label_of_clause [(num, _)] = raw_label_of_num num |
66 fun label_of_clause [(num, _)] = raw_label_of_num num |