equal
deleted
inserted
replaced
113 {clause = clause_params, |
113 {clause = clause_params, |
114 prefactor = #prefactor Metis_Active.default, |
114 prefactor = #prefactor Metis_Active.default, |
115 postfactor = #postfactor Metis_Active.default} |
115 postfactor = #postfactor Metis_Active.default} |
116 val waiting_params = |
116 val waiting_params = |
117 {symbolsWeight = 1.0, |
117 {symbolsWeight = 1.0, |
118 variablesWeight = 0.0, |
118 variablesWeight = 0.5, |
119 literalsWeight = 0.0, |
119 literalsWeight = 0.1, |
120 models = []} |
120 models = []} |
121 val resolution_params = {active = active_params, waiting = waiting_params} |
121 val resolution_params = {active = active_params, waiting = waiting_params} |
122 |
122 |
123 (* Main function to start Metis proof and reconstruction *) |
123 (* Main function to start Metis proof and reconstruction *) |
124 fun FOL_SOLVE (type_enc :: fallback_type_encs) lam_trans ctxt cls ths0 = |
124 fun FOL_SOLVE (type_enc :: fallback_type_encs) lam_trans ctxt cls ths0 = |