equal
deleted
inserted
replaced
193 is_real_cex = (result = Sat), |
193 is_real_cex = (result = Sat), |
194 free_constraints = ts, |
194 free_constraints = ts, |
195 const_defs = us}) |
195 const_defs = us}) |
196 end) |
196 end) |
197 |
197 |
198 val cfalse = Thm.global_cterm_of @{theory} (@{const Trueprop} $ @{const False}) |
198 val cfalse = Thm.cterm_of @{context} (@{const Trueprop} $ @{const False}) |
199 in |
199 in |
200 |
200 |
201 fun add_solver cfg = |
201 fun add_solver cfg = |
202 let |
202 let |
203 val {name, class, avail, command, options, default_max_relevant, |
203 val {name, class, avail, command, options, default_max_relevant, |
266 fun check_topsorts ctxt iwthms = map (apsnd (apsnd (check_topsort ctxt))) iwthms |
266 fun check_topsorts ctxt iwthms = map (apsnd (apsnd (check_topsort ctxt))) iwthms |
267 |
267 |
268 |
268 |
269 (* filter *) |
269 (* filter *) |
270 |
270 |
271 val cnot = Thm.global_cterm_of @{theory} @{const Not} |
271 val cnot = Thm.cterm_of @{context} @{const Not} |
272 |
272 |
273 fun mk_result outcome xrules = { outcome = outcome, used_facts = xrules } |
273 fun mk_result outcome xrules = { outcome = outcome, used_facts = xrules } |
274 |
274 |
275 type 'a smt_filter_data = ('a * thm) list * ((int * thm) list * Proof.context) |
275 type 'a smt_filter_data = ('a * thm) list * ((int * thm) list * Proof.context) |
276 |
276 |