44 |
44 |
45 open String_Redirect |
45 open String_Redirect |
46 |
46 |
47 val trace = Attrib.setup_config_bool @{binding sledgehammer_isar_trace} (K false) |
47 val trace = Attrib.setup_config_bool @{binding sledgehammer_isar_trace} (K false) |
48 |
48 |
|
49 val e_definition_rule = "definition" |
49 val e_skolemize_rule = "skolemize" |
50 val e_skolemize_rule = "skolemize" |
50 val leo2_extcnf_forall_neg_rule = "extcnf_forall_neg" |
51 val leo2_extcnf_forall_neg_rule = "extcnf_forall_neg" |
51 val satallax_skolemize_rule = "tab_ex" |
52 val satallax_skolemize_rule = "tab_ex" |
52 val spass_pirate_datatype_rule = "DT" |
53 val spass_pirate_datatype_rule = "DT" |
53 val vampire_skolemisation_rule = "skolemisation" |
54 val vampire_skolemisation_rule = "skolemisation" |
58 val z3_skolemize_rule = Z3_New_Proof.string_of_rule Z3_New_Proof.Skolemize |
59 val z3_skolemize_rule = Z3_New_Proof.string_of_rule Z3_New_Proof.Skolemize |
59 val z3_th_lemma_rule_prefix = Z3_New_Proof.string_of_rule (Z3_New_Proof.Th_Lemma "") |
60 val z3_th_lemma_rule_prefix = Z3_New_Proof.string_of_rule (Z3_New_Proof.Th_Lemma "") |
60 val zipperposition_cnf_rule = "cnf" |
61 val zipperposition_cnf_rule = "cnf" |
61 |
62 |
62 val skolemize_rules = |
63 val skolemize_rules = |
63 [e_skolemize_rule, leo2_extcnf_forall_neg_rule, satallax_skolemize_rule, spass_skolemize_rule, |
64 [e_definition_rule, e_skolemize_rule, leo2_extcnf_forall_neg_rule, satallax_skolemize_rule, |
64 vampire_skolemisation_rule, veriT_tmp_ite_elim_rule, veriT_tmp_skolemize_rule, z3_skolemize_rule, |
65 spass_skolemize_rule, vampire_skolemisation_rule, veriT_tmp_ite_elim_rule, |
65 zipperposition_cnf_rule] |
66 veriT_tmp_skolemize_rule, z3_skolemize_rule, zipperposition_cnf_rule] |
66 |
67 |
67 val is_skolemize_rule = member (op =) skolemize_rules |
68 val is_skolemize_rule = member (op =) skolemize_rules |
68 fun is_arith_rule rule = |
69 fun is_arith_rule rule = |
69 String.isPrefix z3_th_lemma_rule_prefix rule orelse rule = veriT_simp_arith_rule orelse |
70 String.isPrefix z3_th_lemma_rule_prefix rule orelse rule = veriT_simp_arith_rule orelse |
70 rule = veriT_la_generic_rule |
71 rule = veriT_la_generic_rule |