49 val e_skolemize_rule = "skolemize" |
49 val e_skolemize_rule = "skolemize" |
50 val leo2_extcnf_forall_neg_rule = "extcnf_forall_neg" |
50 val leo2_extcnf_forall_neg_rule = "extcnf_forall_neg" |
51 val satallax_skolemize_rule = "tab_ex" |
51 val satallax_skolemize_rule = "tab_ex" |
52 val spass_pirate_datatype_rule = "DT" |
52 val spass_pirate_datatype_rule = "DT" |
53 val vampire_skolemisation_rule = "skolemisation" |
53 val vampire_skolemisation_rule = "skolemisation" |
|
54 val veriT_la_generic_rule = "la_generic" |
|
55 val veriT_simp_arith_rule = "simp_arith" |
|
56 val veriT_tmp_ite_elim_rule = "tmp_ite_elim" |
54 val veriT_tmp_skolemize_rule = "tmp_skolemize" |
57 val veriT_tmp_skolemize_rule = "tmp_skolemize" |
55 val veriT_tmp_ite_elim_rule = "tmp_ite_elim" |
58 val z3_skolemize_rule = Z3_New_Proof.string_of_rule Z3_New_Proof.Skolemize |
56 val veriT_simp_arith_rule = "simp_arith" |
|
57 val veriT_la_generic_rule = "la_generic" |
|
58 val veriT_arith_rules = [veriT_simp_arith_rule, veriT_la_generic_rule] |
|
59 (* TODO: Use "Z3_Proof.string_of_rule" once it is moved to Isabelle *) |
|
60 val z3_skolemize_rule = "sk" |
|
61 val z3_th_lemma_rule = "th-lemma" |
59 val z3_th_lemma_rule = "th-lemma" |
62 val zipperposition_cnf_rule = "cnf" |
60 val zipperposition_cnf_rule = "cnf" |
63 |
61 |
64 val skolemize_rules = |
62 val skolemize_rules = |
65 [e_skolemize_rule, leo2_extcnf_forall_neg_rule, satallax_skolemize_rule, spass_skolemize_rule, |
63 [e_skolemize_rule, leo2_extcnf_forall_neg_rule, satallax_skolemize_rule, spass_skolemize_rule, |
66 vampire_skolemisation_rule, veriT_tmp_ite_elim_rule, veriT_tmp_skolemize_rule, z3_skolemize_rule, |
64 vampire_skolemisation_rule, veriT_tmp_ite_elim_rule, veriT_tmp_skolemize_rule, z3_skolemize_rule, |
67 zipperposition_cnf_rule] |
65 zipperposition_cnf_rule] |
68 |
66 |
69 val is_skolemize_rule = member (op =) skolemize_rules |
67 val is_skolemize_rule = member (op =) skolemize_rules |
70 val is_arith_rule = String.isPrefix z3_th_lemma_rule orf member (op =) veriT_arith_rules |
68 fun is_arith_rule rule = |
|
69 String.isPrefix z3_th_lemma_rule rule orelse rule = veriT_simp_arith_rule orelse |
|
70 rule = veriT_la_generic_rule |
71 val is_datatype_rule = String.isPrefix spass_pirate_datatype_rule |
71 val is_datatype_rule = String.isPrefix spass_pirate_datatype_rule |
72 |
72 |
73 fun raw_label_of_num num = (num, 0) |
73 fun raw_label_of_num num = (num, 0) |
74 |
74 |
75 fun label_of_clause [(num, _)] = raw_label_of_num num |
75 fun label_of_clause [(num, _)] = raw_label_of_num num |