87 |> HOLogic.mk_Trueprop |> cterm_of thy |> Thm.trivial |
87 |> HOLogic.mk_Trueprop |> cterm_of thy |> Thm.trivial |
88 | _ => raise Fail "unexpected tags sym clause" |
88 | _ => raise Fail "unexpected tags sym clause" |
89 end |
89 end |
90 |> Meson.make_meta_clause |
90 |> Meson.make_meta_clause |
91 |
91 |
92 fun clause_params type_enc = |
92 val clause_params = |
93 {ordering = Metis_KnuthBendixOrder.default, |
93 {ordering = Metis_KnuthBendixOrder.default, |
94 orderLiterals = Metis_Clause.UnsignedLiteralOrder, |
94 orderLiterals = Metis_Clause.UnsignedLiteralOrder, |
95 orderTerms = true} |
95 orderTerms = true} |
96 fun active_params type_enc = |
96 val active_params = |
97 {clause = clause_params type_enc, |
97 {clause = clause_params, |
98 prefactor = #prefactor Metis_Active.default, |
98 prefactor = #prefactor Metis_Active.default, |
99 postfactor = #postfactor Metis_Active.default} |
99 postfactor = #postfactor Metis_Active.default} |
100 val waiting_params = |
100 val waiting_params = |
101 {symbolsWeight = 1.0, |
101 {symbolsWeight = 1.0, |
102 variablesWeight = 0.0, |
102 variablesWeight = 0.0, |
103 literalsWeight = 0.0, |
103 literalsWeight = 0.0, |
104 models = []} |
104 models = []} |
105 fun resolution_params type_enc = |
105 val resolution_params = {active = active_params, waiting = waiting_params} |
106 {active = active_params type_enc, waiting = waiting_params} |
|
107 |
106 |
108 (* Main function to start Metis proof and reconstruction *) |
107 (* Main function to start Metis proof and reconstruction *) |
109 fun FOL_SOLVE (type_enc :: fallback_type_syss) ctxt cls ths0 = |
108 fun FOL_SOLVE (type_enc :: fallback_type_syss) ctxt cls ths0 = |
110 let val thy = Proof_Context.theory_of ctxt |
109 let val thy = Proof_Context.theory_of ctxt |
111 val new_skolemizer = |
110 val new_skolemizer = |
135 val _ = trace_msg ctxt (fn () => "START METIS PROVE PROCESS") |
134 val _ = trace_msg ctxt (fn () => "START METIS PROVE PROCESS") |
136 in |
135 in |
137 case filter (fn t => prop_of t aconv @{prop False}) cls of |
136 case filter (fn t => prop_of t aconv @{prop False}) cls of |
138 false_th :: _ => [false_th RS @{thm FalseE}] |
137 false_th :: _ => [false_th RS @{thm FalseE}] |
139 | [] => |
138 | [] => |
140 case Metis_Resolution.new (resolution_params type_enc) |
139 case Metis_Resolution.new resolution_params |
141 {axioms = thms, conjecture = []} |
140 {axioms = thms, conjecture = []} |
142 |> Metis_Resolution.loop of |
141 |> Metis_Resolution.loop of |
143 Metis_Resolution.Contradiction mth => |
142 Metis_Resolution.Contradiction mth => |
144 let val _ = trace_msg ctxt (fn () => "METIS RECONSTRUCTION START: " ^ |
143 let val _ = trace_msg ctxt (fn () => "METIS RECONSTRUCTION START: " ^ |
145 Metis_Thm.toString mth) |
144 Metis_Thm.toString mth) |