# HG changeset patch # User boehmes # Date 1253515531 -7200 # Node ID 35094c8fd8bff6a595644f624fafdd8475621810 # Parent bfbdeddc03bc9cfd2f36dc783c95df793dcb3764# Parent 02f45a09a9f2d376e7427029fc516c9e910ae8f9 merged diff -r bfbdeddc03bc -r 35094c8fd8bf CONTRIBUTORS --- a/CONTRIBUTORS Sun Sep 20 19:17:33 2009 +0200 +++ b/CONTRIBUTORS Mon Sep 21 08:45:31 2009 +0200 @@ -7,6 +7,9 @@ Contributions to this Isabelle version -------------------------------------- +* September 2009: Sascha Boehme, TUM + SMT method using external SMT solvers + * September 2009: Florian Haftmann, TUM Refinement of Sets and Lattices diff -r bfbdeddc03bc -r 35094c8fd8bf NEWS --- a/NEWS Sun Sep 20 19:17:33 2009 +0200 +++ b/NEWS Mon Sep 21 08:45:31 2009 +0200 @@ -18,6 +18,13 @@ *** HOL *** +* New proof method "smt" for a combination of first-order logic +with equality, linear and nonlinear (natural/integer/real) +arithmetic, and fixed-size bitvectors; there is also basic +support for higher-order features (esp. lambda abstractions). +It is an incomplete decision procedure based on external SMT +solvers using the oracle mechanism. + * Reorganization of number theory: * former session NumberTheory now named Old_Number_Theory * new session Number_Theory by Jeremy Avigad; if possible, prefer this. diff -r bfbdeddc03bc -r 35094c8fd8bf etc/components --- a/etc/components Sun Sep 20 19:17:33 2009 +0200 +++ b/etc/components Mon Sep 21 08:45:31 2009 +0200 @@ -15,3 +15,4 @@ src/HOL/Tools/ATP_Manager src/HOL/Mirabelle src/HOL/Library/Sum_Of_Squares +src/HOL/SMT diff -r bfbdeddc03bc -r 35094c8fd8bf src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Sun Sep 20 19:17:33 2009 +0200 +++ b/src/HOL/IsaMakefile Mon Sep 21 08:45:31 2009 +0200 @@ -40,6 +40,7 @@ HOL-Prolog \ HOL-SET-Protocol \ HOL-SizeChange \ + HOL-SMT \ HOL-Statespace \ HOL-Subst \ TLA-Buffer \ @@ -1134,6 +1135,19 @@ @$(ISABELLE_TOOL) usedir $(OUT)/HOL Mirabelle +## HOL-SMT + +HOL-SMT: HOL-Word $(LOG)/HOL-SMT.gz + +$(LOG)/HOL-SMT.gz: $(OUT)/HOL-Word SMT/SMT_Definitions.thy SMT/SMT.thy \ + SMT/Tools/smt_normalize.ML SMT/Tools/smt_monomorph.ML \ + SMT/Tools/smt_translate.ML SMT/Tools/smt_builtin.ML \ + SMT/Tools/smtlib_interface.ML SMT/Tools/smt_solver.ML \ + SMT/Tools/cvc3_solver.ML SMT/Tools/yices_solver.ML \ + SMT/Tools/z3_interface.ML SMT/Tools/z3_solver.ML SMT/Tools/z3_model.ML + @cd SMT; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-Word HOL-SMT + + ## clean clean: @@ -1156,4 +1170,4 @@ $(LOG)/HOL-Unix.gz $(OUT)/HOL-Word $(LOG)/HOL-Word.gz \ $(LOG)/HOL-Word-Examples.gz $(OUT)/HOL-NSA \ $(LOG)/HOL-NSA.gz $(LOG)/HOL-NSA-Examples.gz \ - $(LOG)/HOL-Mirabelle.gz + $(LOG)/HOL-Mirabelle.gz $(LOG)/HOL-SMT.gz diff -r bfbdeddc03bc -r 35094c8fd8bf src/HOL/SMT/Examples/SMT_Examples.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/SMT/Examples/SMT_Examples.thy Mon Sep 21 08:45:31 2009 +0200 @@ -0,0 +1,182 @@ +(* Title: SMT_Examples.thy + Author: Sascha Boehme, TU Muenchen +*) + +header {* Examples for the 'smt' tactic. *} + +theory SMT_Examples +imports "../SMT" +begin + +declare [[smt_solver=z3, z3_proofs=false]] +declare [[smt_trace=true]] (*FIXME*) + + +section {* Propositional and first-order logic *} + +lemma "True" by smt +lemma "p \ \p" by smt +lemma "(p \ True) = p" by smt +lemma "(p \ q) \ \p \ q" by smt +lemma "(a \ b) \ (c \ d) \ (a \ b) \ (c \ d)" by smt +lemma "P=P=P=P=P=P=P=P=P=P" by smt + +axiomatization symm_f :: "'a \ 'a \ 'a" where + symm_f: "symm_f x y = symm_f y x" +lemma "a = a \ symm_f a b = symm_f b a" by (smt add: symm_f) + + +section {* Linear arithmetic *} + +lemma "(3::int) = 3" by smt +lemma "(3::real) = 3" by smt +lemma "(3 :: int) + 1 = 4" by smt +lemma "max (3::int) 8 > 5" by smt +lemma "abs (x :: real) + abs y \ abs (x + y)" by smt +lemma "let x = (2 :: int) in x + x \ 5" by smt + +text{* +The following example was taken from HOL/ex/PresburgerEx.thy, where it says: + + This following theorem proves that all solutions to the + recurrence relation $x_{i+2} = |x_{i+1}| - x_i$ are periodic with + period 9. The example was brought to our attention by John + Harrison. It does does not require Presburger arithmetic but merely + quantifier-free linear arithmetic and holds for the rationals as well. + + Warning: it takes (in 2006) over 4.2 minutes! + +There, it is proved by "arith". SMT is able to prove this within a fraction +of one second. +*} + +lemma "\ x3 = abs x2 - x1; x4 = abs x3 - x2; x5 = abs x4 - x3; + x6 = abs x5 - x4; x7 = abs x6 - x5; x8 = abs x7 - x6; + x9 = abs x8 - x7; x10 = abs x9 - x8; x11 = abs x10 - x9 \ + \ x1 = x10 & x2 = (x11::int)" + by smt + +lemma "\x::int. 0 < x" by smt +lemma "\x::real. 0 < x" by smt +lemma "\x y::int. x < y \ (2 * x + 1) < (2 * y)" by smt +lemma "\x y::int. (2 * x + 1) \ (2 * y)" by smt +lemma "~ (\x y z::int. 4 * x + -6 * y = (1::int))" by smt +lemma "~ (\x::int. False)" by smt + + +section {* Non-linear arithmetic *} + +lemma "((x::int) * (1 + y) - x * (1 - y)) = (2 * x * y)" by smt +lemma + "(U::int) + (1 + p) * (b + e) + p * d = + U + (2 * (1 + p) * (b + e) + (1 + p) * d + d * p) - (1 + p) * (b + d + e)" + by smt + + +section {* Linear arithmetic for natural numbers *} + +lemma "a < 3 \ (7::nat) > 2 * a" by smt +lemma "let x = (1::nat) + y in x - y > 0 * x" by smt +lemma + "let x = (1::nat) + y in + let P = (if x > 0 then True else False) in + False \ P = (x - 1 = y) \ (\P \ False)" + by smt + + +section {* Bitvectors *} + +locale bv +begin + +declare [[smt_solver=z3]] + +lemma "(27 :: 4 word) = -5" by smt +lemma "(27 :: 4 word) = 11" by smt +lemma "23 < (27::8 word)" by smt +lemma "27 + 11 = (6::5 word)" by smt +lemma "7 * 3 = (21::8 word)" by smt +lemma "11 - 27 = (-16::8 word)" by smt +lemma "- -11 = (11::5 word)" by smt +lemma "-40 + 1 = (-39::7 word)" by smt +lemma "a + 2 * b + c - b = (b + c) + (a :: 32 word)" by smt + +lemma "0b110 AND 0b101 = (0b100 :: 32 word)" by smt +lemma "0b110 OR 0b011 = (0b111 :: 8 word)" by smt +lemma "0xF0 XOR 0xFF = (0x0F :: 8 word)" by smt +lemma "NOT (0xF0 :: 16 word) = 0xFF0F" by smt + +lemma "word_cat (27::4 word) (27::8 word) = (2843::12 word)" by smt +lemma "word_cat (0b0011::4 word) (0b1111::6word) = (0b0011001111 :: 10 word)" + by smt + +lemma "slice 1 (0b10110 :: 4 word) = (0b11 :: 2 word)" by smt + +lemma "ucast (0b1010 :: 4 word) = (0b1010 :: 10 word)" by smt +lemma "scast (0b1010 :: 4 word) = (0b111010 :: 6 word)" by smt + +lemma "bv_lshr 0b10011 2 = (0b100::8 word)" by smt +lemma "bv_ashr 0b10011 2 = (0b100::8 word)" by smt + +lemma "word_rotr 2 0b0110 = (0b1001::4 word)" by smt +lemma "word_rotl 1 0b1110 = (0b1101::4 word)" by smt + +lemma "(x AND 0xff00) OR (x AND 0x00ff) = (x::16 word)" by smt + +lemma "w < 256 \ (w :: 16 word) AND 0x00FF = w" by smt + +end + + +section {* Pairs *} + +lemma "fst (x, y) = a \ x = a" by smt +lemma "p1 = (x, y) \ p2 = (y, x) \ fst p1 = snd p2" by smt + + +section {* Higher-order problems and recursion *} + +lemma "(f g x = (g x \ True)) \ (f g x = True) \ (g x = True)" by smt +lemma "P ((2::int) < 3) = P True" by smt +lemma "P ((2::int) < 3) = (P True :: bool)" by smt +lemma "P (0 \ (a :: 4 word)) = P True" using [[smt_solver=z3]] by smt +lemma "id 3 = 3 \ id True = True" by (smt add: id_def) +lemma "i \ i1 \ i \ i2 \ ((f (i1 := v1)) (i2 := v2)) i = f i" by smt +lemma "map (\i::nat. i + 1) [0, 1] = [1, 2]" by (smt add: map.simps) +lemma "(ALL x. P x) | ~ All P" by smt + +fun dec_10 :: "nat \ nat" where + "dec_10 n = (if n < 10 then n else dec_10 (n - 10))" +lemma "dec_10 (4 * dec_10 4) = 6" by (smt add: dec_10.simps) + +axiomatization + eval_dioph :: "int list \ nat list \ int" + where + eval_dioph_mod: + "eval_dioph ks xs mod int n = eval_dioph ks (map (\x. x mod n) xs) mod int n" + and + eval_dioph_div_mult: + "eval_dioph ks (map (\x. x div n) xs) * int n + + eval_dioph ks (map (\x. x mod n) xs) = eval_dioph ks xs" +lemma + "(eval_dioph ks xs = l) = + (eval_dioph ks (map (\x. x mod 2) xs) mod 2 = l mod 2 \ + eval_dioph ks (map (\x. x div 2) xs) = + (l - eval_dioph ks (map (\x. x mod 2) xs)) div 2)" + by (smt add: eval_dioph_mod[where n=2] eval_dioph_div_mult[where n=2]) + + +section {* Monomorphization examples *} + +definition P :: "'a \ bool" where "P x = True" +lemma poly_P: "P x \ (P [x] \ \P[x])" by (simp add: P_def) +lemma "P (1::int)" by (smt add: poly_P) + +consts g :: "'a \ nat" +axioms + g1: "g (Some x) = g [x]" + g2: "g None = g []" + g3: "g xs = length xs" +lemma "g (Some (3::int)) = g (Some True)" by (smt add: g1 g2 g3 list.size) + +end diff -r bfbdeddc03bc -r 35094c8fd8bf src/HOL/SMT/IsaMakefile --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/SMT/IsaMakefile Mon Sep 21 08:45:31 2009 +0200 @@ -0,0 +1,39 @@ + +## targets + +default: HOL-SMT +images: HOL-SMT +test: + +all: images test + + +## global settings + +SRC = $(ISABELLE_HOME)/src +OUT = $(ISABELLE_OUTPUT) +LOG = $(OUT)/log + +USEDIR = $(ISATOOL) usedir -v true + + +## HOL-SMT + +HOL-SMT: $(OUT)/HOL-SMT + +$(OUT)/HOL-SMT: $(OUT)/HOL-Word ROOT.ML SMT_Definitions.thy SMT.thy \ + Tools/cancel_conj_disj.ML Tools/smt_normalize.ML Tools/smt_monomorph.ML \ + Tools/smt_translate.ML Tools/smt_builtin.ML Tools/smtlib_interface.ML \ + Tools/smt_solver.ML Tools/cvc3_solver.ML Tools/yices_solver.ML \ + Tools/z3_interface.ML Tools/z3_solver.ML Tools/z3_model.ML \ + Tools/z3_proof.ML Tools/z3_proof_rules.ML Tools/z3_proof_terms.ML + @$(USEDIR) -b HOL-Word HOL-SMT + +$(OUT)/HOL-Word: + @$(ISATOOL) make HOL-Word -C $(SRC)/HOL + + +## clean + +clean: + @rm -f $(OUT)/HOL-SMT diff -r bfbdeddc03bc -r 35094c8fd8bf src/HOL/SMT/ROOT.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/SMT/ROOT.ML Mon Sep 21 08:45:31 2009 +0200 @@ -0,0 +1,1 @@ +use_thy "SMT"; diff -r bfbdeddc03bc -r 35094c8fd8bf src/HOL/SMT/SMT.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/SMT/SMT.thy Mon Sep 21 08:45:31 2009 +0200 @@ -0,0 +1,51 @@ +(* Title: HOL/SMT/SMT.thy + Author: Sascha Boehme, TU Muenchen +*) + +header {* SMT method using external SMT solvers (CVC3, Yices, Z3) *} + +theory SMT +imports SMT_Definitions +uses + "Tools/smt_normalize.ML" + "Tools/smt_monomorph.ML" + "Tools/smt_translate.ML" + "Tools/smt_solver.ML" + "Tools/smtlib_interface.ML" + "Tools/cvc3_solver.ML" + "Tools/yices_solver.ML" + "Tools/z3_model.ML" + "Tools/z3_interface.ML" + "Tools/z3_solver.ML" +begin + +setup {* + SMT_Normalize.setup #> + SMT_Solver.setup #> + CVC3_Solver.setup #> + Yices_Solver.setup #> + Z3_Solver.setup +*} + +ML {* +OuterSyntax.improper_command "smt_status" + "Show the available SMT solvers and the currently selected solver." + OuterKeyword.diag + (Scan.succeed (Toplevel.no_timing o Toplevel.keep (fn state => + SMT_Solver.print_setup (Context.Proof (Toplevel.context_of state))))) +*} + +method_setup smt = {* + let fun solver thms ctxt = SMT_Solver.smt_tac ctxt thms + in + Scan.optional (Scan.lift (Args.add -- Args.colon) |-- Attrib.thms) [] >> + (Method.SIMPLE_METHOD' oo solver) + end +*} "Applies an SMT solver to the current goal." + +declare [[ smt_solver = z3, smt_timeout = 20, smt_trace = false ]] +declare [[ smt_unfold_defs = true ]] +declare [[ z3_proofs = false ]] + +end + diff -r bfbdeddc03bc -r 35094c8fd8bf src/HOL/SMT/SMT_Definitions.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/SMT/SMT_Definitions.thy Mon Sep 21 08:45:31 2009 +0200 @@ -0,0 +1,113 @@ +(* Title: HOL/SMT/SMT_Definitions.thy + Author: Sascha Boehme, TU Muenchen +*) + +header {* SMT-specific definitions *} + +theory SMT_Definitions +imports Real Word "~~/src/HOL/Decision_Procs/Dense_Linear_Order" +begin + +section {* Triggers for quantifier instantiation *} + +text {* +Some SMT solvers support triggers for quantifier instantiation. Each trigger +consists of one ore more patterns. A pattern may either be a list of positive +subterms (the first being tagged by "pat" and the consecutive subterms tagged +by "andpat"), or a list of negative subterms (the first being tagged by "nopat" +and the consecutive subterms tagged by "andpat"). +*} + +datatype pattern = Pattern + +definition pat :: "'a \ pattern" +where "pat _ = Pattern" + +definition nopat :: "bool \ pattern" +where "nopat _ = Pattern" + +definition andpat :: "pattern \ 'a \ pattern" (infixl "andpat" 60) +where "_ andpat _ = Pattern" + +definition trigger :: "pattern list \ bool \ bool" +where "trigger _ P = P" + + +section {* Arithmetic *} + +text {* +The sign of @{term "op mod :: int \ int \ int"} follows the sign of the +divisor. In contrast to that, the sign of the following operation is that of +the dividend. +*} + +definition rem :: "int \ int \ int" (infixl "rem" 70) +where "a rem b = + (if (a \ 0 \ b < 0) \ (a < 0 \ b \ 0) then - (a mod b) else a mod b)" + +text {* A decision procedure for linear real arithmetic: *} + +setup {* + Arith_Data.add_tactic "Ferrante-Rackoff" (K FerranteRackoff.dlo_tac) +*} + + +section {* Bitvectors *} + +text {* +The following definitions provide additional functions not found in HOL-Word. +*} + +definition sdiv :: "'a::len word \ 'a word \ 'a word" (infix "sdiv" 70) +where "w1 sdiv w2 = word_of_int (sint w1 div sint w2)" + +definition smod :: "'a::len word \ 'a word \ 'a word" (infix "smod" 70) + (* sign follows divisor *) +where "w1 smod w2 = word_of_int (sint w1 mod sint w2)" + +definition srem :: "'a::len word \ 'a word \ 'a word" (infix "srem" 70) + (* sign follows dividend *) +where "w1 srem w2 = word_of_int (sint w1 rem sint w2)" + +definition bv_shl :: "'a::len0 word \ 'a word \ 'a word" +where "bv_shl w1 w2 = (w1 << unat w2)" + +definition bv_lshr :: "'a::len0 word \ 'a word \ 'a word" +where "bv_lshr w1 w2 = (w1 >> unat w2)" + +definition bv_ashr :: "'a::len word \ 'a word \ 'a word" +where "bv_ashr w1 w2 = (w1 >>> unat w2)" + + +section {* Higher-order encoding *} + +definition "apply" where "apply f x = f x" + + +section {* First-order logic *} + +text {* +Some SMT solver formats require a strict separation between formulas and terms. +The following marker symbols are used internally to separate those categories: +*} + +definition formula :: "bool \ bool" where "formula x = x" +definition "term" where "term x = x" + +text {* +Predicate symbols also occurring as function symbols are turned into function +symbols by translating atomic formulas into terms: +*} + +abbreviation holds :: "bool \ bool" where "holds \ (\P. term P = term True)" + +text {* +The following constant represents equivalence, to be treated differently than +the (polymorphic) equality predicate: +*} + +definition iff :: "bool \ bool \ bool" (infix "iff" 50) where + "(x iff y) = (x = y)" + +end + diff -r bfbdeddc03bc -r 35094c8fd8bf src/HOL/SMT/Tools/cvc3_solver.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/SMT/Tools/cvc3_solver.ML Mon Sep 21 08:45:31 2009 +0200 @@ -0,0 +1,59 @@ +(* Title: HOL/SMT/Tools/cvc3_solver.ML + Author: Sascha Boehme, TU Muenchen + +Interface of the SMT solver CVC3. +*) + +signature CVC3_SOLVER = +sig + val setup: theory -> theory +end + +structure CVC3_Solver: CVC3_SOLVER = +struct + +val solver_name = "cvc3" +val env_var = "CVC3_SOLVER" + +val options = + ["+counterexample", "-lang", "smtlib", "-output-lang", "presentation"] + +val is_sat = String.isPrefix "Satisfiable." +val is_unsat = String.isPrefix "Unsatisfiable." +val is_unknown = String.isPrefix "Unknown." + +fun cex_kind true = "Counterexample" + | cex_kind false = "Possible counterexample" + +fun raise_cex real ctxt recon ls = + let + val start = String.isPrefix "%Satisfiable Variable Assignment: %" + val index = find_index start ls + val ls = if index > 0 then Library.drop (index + 1, ls) else [] + val p = Pretty.big_list (cex_kind real ^ " found:") (map Pretty.str ls) + in error (Pretty.string_of p) end + +fun core_oracle (SMT_Solver.ProofData {context, output, recon, ...}) = + let + val empty_line = (fn "" => true | _ => false) + val split_first = (fn [] => ("", []) | l :: ls => (l, ls)) + val (l, ls) = split_first (dropwhile empty_line output) + in + if is_unsat l then @{cprop False} + else if is_sat l then raise_cex true context recon ls + else if is_unknown l then raise_cex false context recon ls + else error (solver_name ^ " failed") + end + +fun smtlib_solver oracle _ = + SMT_Solver.SolverConfig { + name = {env_var=env_var, remote_name=solver_name}, + interface = SMTLIB_Interface.interface, + arguments = options, + reconstruct = oracle } + +val setup = + Thm.add_oracle (Binding.name solver_name, core_oracle) #-> (fn (_, oracle) => + SMT_Solver.add_solver (solver_name, smtlib_solver oracle)) + +end diff -r bfbdeddc03bc -r 35094c8fd8bf src/HOL/SMT/Tools/smt_builtin.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/SMT/Tools/smt_builtin.ML Mon Sep 21 08:45:31 2009 +0200 @@ -0,0 +1,78 @@ +(* Title: HOL/SMT/Tools/smt_builtin.ML + Author: Sascha Boehme, TU Muenchen + +Tables for built-in symbols. +*) + +signature SMT_BUILTIN = +sig + type sterm = (SMT_Translate.sym, typ) sterm + type builtin_fun = typ -> sterm list -> (string * sterm list) option + type table = (typ * builtin_fun) list Symtab.table + + val make: (term * string) list -> table + val add: term * builtin_fun -> table -> table + val lookup: table -> theory -> string * typ -> sterm list -> + (string * sterm list) option + + val bv_rotate: (int -> string) -> builtin_fun + val bv_extend: (int -> string) -> builtin_fun + val bv_extract: (int -> int -> string) -> builtin_fun +end + +structure SMT_Builtin: SMT_BUILTIN = +struct + +structure T = SMT_Translate + +type sterm = (SMT_Translate.sym, typ) sterm +type builtin_fun = typ -> sterm list -> (string * sterm list) option +type table = (typ * builtin_fun) list Symtab.table + +fun make entries = + let + fun dest (t, bn) = + let val (n, T) = Term.dest_Const t + in (n, (Logic.varifyT T, K (pair bn))) end + in Symtab.make (AList.group (op =) (map dest entries)) end + +fun add (t, f) tab = + let val (n, T) = apsnd Logic.varifyT (Term.dest_Const t) + in Symtab.map_default (n, []) (AList.update (op =) (T, f)) tab end + +fun lookup tab thy (n, T) = + AList.lookup (Sign.typ_instance thy) (Symtab.lookup_list tab n) T T + + +fun dest_binT T = + (case T of + Type (@{type_name "Numeral_Type.num0"}, _) => 0 + | Type (@{type_name "Numeral_Type.num1"}, _) => 1 + | Type (@{type_name "Numeral_Type.bit0"}, [T]) => 2 * dest_binT T + | Type (@{type_name "Numeral_Type.bit1"}, [T]) => 1 + 2 * dest_binT T + | _ => raise TYPE ("dest_binT", [T], [])) + +fun dest_wordT T = + (case T of + Type (@{type_name "word"}, [T]) => dest_binT T + | _ => raise TYPE ("dest_wordT", [T], [])) + + +val dest_nat = (fn + SApp (SConst (@{const_name nat}, _), [SApp (SNum (i, _), _)]) => SOME i + | _ => NONE) + +fun bv_rotate mk_name T ts = + dest_nat (hd ts) |> Option.map (fn i => (mk_name i, tl ts)) + +fun bv_extend mk_name T ts = + (case (try dest_wordT (domain_type T), try dest_wordT (range_type T)) of + (SOME i, SOME j) => if j - i >= 0 then SOME (mk_name (j - i), ts) else NONE + | _ => NONE) + +fun bv_extract mk_name T ts = + (case (try dest_wordT (body_type T), dest_nat (hd ts)) of + (SOME i, SOME lb) => SOME (mk_name (i + lb - 1) lb, tl ts) + | _ => NONE) + +end diff -r bfbdeddc03bc -r 35094c8fd8bf src/HOL/SMT/Tools/smt_monomorph.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/SMT/Tools/smt_monomorph.ML Mon Sep 21 08:45:31 2009 +0200 @@ -0,0 +1,120 @@ +(* Title: HOL/SMT/Tools/smt_monomorph.ML + Author: Sascha Boehme, TU Muenchen + +Monomorphization of terms, i.e., computation of all (necessary) instances. +*) + +signature SMT_MONOMORPH = +sig + val monomorph: theory -> term list -> term list +end + +structure SMT_Monomorph: SMT_MONOMORPH = +struct + +fun selection [] = [] + | selection (x :: xs) = (x, xs) :: map (apsnd (cons x)) (selection xs) + +fun permute [] = [] + | permute [x] = [[x]] + | permute xs = maps (fn (y, ys) => map (cons y) (permute ys)) (selection xs) + +fun fold_all f = fold (fn x => maps (f x)) + + +val typ_has_tvars = Term.exists_subtype (fn TVar _ => true | _ => false) +val term_has_tvars = Term.exists_type typ_has_tvars + +val ignored = member (op =) [ + @{const_name All}, @{const_name Ex}, @{const_name Let}, @{const_name If}, + @{const_name "op ="}, @{const_name zero_class.zero}, + @{const_name one_class.one}, @{const_name number_of}] +fun consts_of ts = AList.group (op =) (fold Term.add_consts ts []) + |> filter_out (ignored o fst) + +val join_consts = curry (AList.join (op =) (K (merge (op =)))) +fun diff_consts cs ds = + let fun diff (n, Ts) = + (case AList.lookup (op =) cs n of + NONE => SOME (n, Ts) + | SOME Us => + let val Ts' = fold (remove (op =)) Us Ts + in if null Ts' then NONE else SOME (n, Ts') end) + in map_filter diff ds end + +fun instances thy is (n, Ts) env = + let + val Us = these (AList.lookup (op =) is n) + val Ts' = filter typ_has_tvars (map (Envir.subst_type env) Ts) + in + (case map_product pair Ts' Us of + [] => [env] + | TUs => map_filter (try (fn TU => Sign.typ_match thy TU env)) TUs) + end + +fun proper_match ps env = + forall (forall (not o typ_has_tvars o Envir.subst_type env) o snd) ps + +val eq_tab = gen_eq_set (op =) o pairself Vartab.dest + +fun specialize thy cs is ((r, ps), ces) (ts, ns) = + let + val ps' = filter (AList.defined (op =) is o fst) ps + + val envs = permute ps' + |> maps (fn ps => fold_all (instances thy is) ps [Vartab.empty]) + |> filter (proper_match ps') + |> filter_out (member eq_tab ces) + |> distinct eq_tab + + val us = map (fn env => Envir.subst_term_types env r) envs + val ns' = join_consts (diff_consts is (diff_consts cs (consts_of us))) ns + in (envs @ ces, (fold (insert (op aconv)) us ts, ns')) end + + +fun incr_tvar_indices i t = + let + val incrT = Logic.incr_tvar i + + fun incr t = + (case t of + Const (n, T) => Const (n, incrT T) + | Free (n, T) => Free (n, incrT T) + | Abs (n, T, t1) => Abs (n, incrT T, incr t1) + | t1 $ t2 => incr t1 $ incr t2 + | _ => t) + in incr t end + + +val monomorph_limit = 10 + +(* Instantiate all polymorphic constants (i.e., constants occurring both with + ground types and type variables) with all (necessary) ground types; thereby + create copies of terms containing those constants. + To prevent non-termination, there is an upper limit for the number of + recursions involved in the fixpoint construction. *) +fun monomorph thy ts = + let + val (ps, ms) = List.partition term_has_tvars ts + + fun with_tvar (n, Ts) = + let val Ts' = filter typ_has_tvars Ts + in if null Ts' then NONE else SOME (n, Ts') end + fun incr t idx = (incr_tvar_indices idx t, idx + Term.maxidx_of_term t + 1) + val rps = fst (fold_map incr ps 0) + |> map (fn r => (r, map_filter with_tvar (consts_of [r]))) + + fun mono count is ces cs ts = + let + val spec = specialize thy cs is + val (ces', (ts', is')) = fold_map spec (rps ~~ ces) (ts, []) + val cs' = join_consts is cs + in + if null is' then ts' + else if count > monomorph_limit then + (Output.warning "monomorphization limit reached"; ts') + else mono (count + 1) is' ces' cs' ts' + end + in mono 0 (consts_of ms) (map (K []) rps) [] ms end + +end diff -r bfbdeddc03bc -r 35094c8fd8bf src/HOL/SMT/Tools/smt_normalize.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/SMT/Tools/smt_normalize.ML Mon Sep 21 08:45:31 2009 +0200 @@ -0,0 +1,408 @@ +(* Title: HOL/SMT/Tools/smt_normalize.ML + Author: Sascha Boehme, TU Muenchen + +Normalization steps on theorems required by SMT solvers: + * unfold trivial let expressions, + * replace negative numerals by negated positive numerals, + * embed natural numbers into integers, + * add extra rules specifying types and constants which occur frequently, + * lift lambda terms, + * make applications explicit for functions with varying number of arguments, + * fully translate into object logic, add universal closure. +*) + +signature SMT_NORMALIZE = +sig + val normalize_rule: Proof.context -> thm -> thm + val instantiate_free: Thm.cterm * Thm.cterm -> thm -> thm + val discharge_definition: Thm.cterm -> thm -> thm + + val trivial_let: Proof.context -> thm list -> thm list + val positive_numerals: Proof.context -> thm list -> thm list + val nat_as_int: Proof.context -> thm list -> thm list + val unfold_defs: bool Config.T + val add_pair_rules: Proof.context -> thm list -> thm list + val add_fun_upd_rules: Proof.context -> thm list -> thm list + val add_abs_min_max_rules: Proof.context -> thm list -> thm list + + datatype config = + RewriteTrivialLets | + RewriteNegativeNumerals | + RewriteNaturalNumbers | + AddPairRules | + AddFunUpdRules | + AddAbsMinMaxRules + + val normalize: config list -> Proof.context -> thm list -> + Thm.cterm list * thm list + + val setup: theory -> theory +end + +structure SMT_Normalize: SMT_NORMALIZE = +struct + +val norm_binder_conv = Conv.try_conv (More_Conv.rewrs_conv [ + @{lemma "All P == ALL x. P x" by (rule reflexive)}, + @{lemma "Ex P == EX x. P x" by (rule reflexive)}, + @{lemma "Let c P == let x = c in P x" by (rule reflexive)}]) + +fun cert ctxt = Thm.cterm_of (ProofContext.theory_of ctxt) + +fun norm_meta_def cv thm = + let val thm' = Thm.combination thm (Thm.reflexive cv) + in Thm.transitive thm' (Thm.beta_conversion false (Thm.rhs_of thm')) end + +fun norm_def ctxt thm = + (case Thm.prop_of thm of + Const (@{const_name "=="}, _) $ _ $ Abs (_, T, _) => + let val v = Var ((Name.uu, #maxidx (Thm.rep_thm thm) + 1), T) + in norm_def ctxt (norm_meta_def (cert ctxt v) thm) end + | @{term Trueprop} $ (Const (@{const_name "op ="}, _) $ _ $ Abs _) => + norm_def ctxt (thm RS @{thm fun_cong}) + | _ => thm) + +fun normalize_rule ctxt = + Conv.fconv_rule ( + Thm.beta_conversion true then_conv + Thm.eta_conversion then_conv + More_Conv.bottom_conv (K norm_binder_conv) ctxt) #> + norm_def ctxt #> + Drule.forall_intr_vars #> + Conv.fconv_rule ObjectLogic.atomize + +fun instantiate_free (cv, ct) thm = + if Term.exists_subterm (equal (Thm.term_of cv)) (Thm.prop_of thm) + then Thm.forall_elim ct (Thm.forall_intr cv thm) + else thm + +fun discharge_definition ct thm = + let val (cv, cu) = Thm.dest_equals ct + in + Thm.implies_intr ct thm + |> instantiate_free (cv, cu) + |> (fn thm => Thm.implies_elim thm (Thm.reflexive cu)) + end + +fun if_conv c cv1 cv2 ct = (if c (Thm.term_of ct) then cv1 else cv2) ct +fun if_true_conv c cv = if_conv c cv Conv.all_conv + + +(* simplification of trivial let expressions (whose bound variables occur at + most once) *) + +local + fun count i (Bound j) = if j = i then 1 else 0 + | count i (t $ u) = count i t + count i u + | count i (Abs (_, _, t)) = count (i + 1) t + | count _ _ = 0 + + fun is_trivial_let (Const (@{const_name Let}, _) $ _ $ Abs (_, _, t)) = + (count 0 t <= 1) + | is_trivial_let _ = false + + fun let_conv _ = if_true_conv is_trivial_let (Conv.rewr_conv @{thm Let_def}) + + fun cond_let_conv ctxt = if_true_conv (Term.exists_subterm is_trivial_let) + (More_Conv.top_conv let_conv ctxt) +in +fun trivial_let ctxt = map (Conv.fconv_rule (cond_let_conv ctxt)) +end + + +(* rewriting of negative integer numerals into positive numerals *) + +local + fun neg_numeral @{term Int.Min} = true + | neg_numeral _ = false + fun is_number_sort thy T = Sign.of_sort thy (T, @{sort number_ring}) + fun is_neg_number ctxt (Const (@{const_name number_of}, T) $ t) = + Term.exists_subterm neg_numeral t andalso + is_number_sort (ProofContext.theory_of ctxt) (Term.body_type T) + | is_neg_number _ _ = false + fun has_neg_number ctxt = Term.exists_subterm (is_neg_number ctxt) + + val pos_numeral_ss = HOL_ss + addsimps [@{thm Int.number_of_minus}, @{thm Int.number_of_Min}] + addsimps [@{thm Int.numeral_1_eq_1}] + addsimps @{thms Int.pred_bin_simps} + addsimps @{thms Int.normalize_bin_simps} + addsimps @{lemma + "Int.Min = - Int.Bit1 Int.Pls" + "Int.Bit0 (- Int.Pls) = - Int.Pls" + "Int.Bit0 (- k) = - Int.Bit0 k" + "Int.Bit1 (- k) = - Int.Bit1 (Int.pred k)" + by simp_all (simp add: pred_def)} + + fun pos_conv ctxt = if_conv (is_neg_number ctxt) + (Simplifier.rewrite (Simplifier.context ctxt pos_numeral_ss)) + Conv.no_conv + + fun cond_pos_conv ctxt = if_true_conv (has_neg_number ctxt) + (More_Conv.top_sweep_conv pos_conv ctxt) +in +fun positive_numerals ctxt = map (Conv.fconv_rule (cond_pos_conv ctxt)) +end + + +(* embedding of standard natural number operations into integer operations *) + +local + val nat_embedding = @{lemma + "nat (int n) = n" + "i >= 0 --> int (nat i) = i" + "i < 0 --> int (nat i) = 0" + by simp_all} + + val nat_rewriting = @{lemma + "0 = nat 0" + "1 = nat 1" + "number_of i = nat (number_of i)" + "int (nat 0) = 0" + "int (nat 1) = 1" + "a < b = (int a < int b)" + "a <= b = (int a <= int b)" + "Suc a = nat (int a + 1)" + "a + b = nat (int a + int b)" + "a - b = nat (int a - int b)" + "a * b = nat (int a * int b)" + "a div b = nat (int a div int b)" + "a mod b = nat (int a mod int b)" + "int (nat (int a + int b)) = int a + int b" + "int (nat (int a * int b)) = int a * int b" + "int (nat (int a div int b)) = int a div int b" + "int (nat (int a mod int b)) = int a mod int b" + by (simp add: nat_mult_distrib nat_div_distrib nat_mod_distrib + int_mult[symmetric] zdiv_int[symmetric] zmod_int[symmetric])+} + + fun on_positive num f x = + (case try HOLogic.dest_number (Thm.term_of num) of + SOME (_, i) => if i >= 0 then SOME (f x) else NONE + | NONE => NONE) + + val cancel_int_nat_ss = HOL_ss + addsimps [@{thm Nat_Numeral.nat_number_of}] + addsimps [@{thm Nat_Numeral.int_nat_number_of}] + addsimps @{thms neg_simps} + + fun cancel_int_nat_simproc _ ss ct = + let + val num = Thm.dest_arg (Thm.dest_arg ct) + val goal = Thm.mk_binop @{cterm "op == :: int => _"} ct num + val simpset = Simplifier.inherit_context ss cancel_int_nat_ss + fun tac _ = Simplifier.simp_tac simpset 1 + in on_positive num (Goal.prove_internal [] goal) tac end + + val nat_ss = HOL_ss + addsimps nat_rewriting + addsimprocs [Simplifier.make_simproc { + name = "cancel_int_nat_num", lhss = [@{cpat "int (nat _)"}], + proc = cancel_int_nat_simproc, identifier = [] }] + + fun conv ctxt = Simplifier.rewrite (Simplifier.context ctxt nat_ss) + + val uses_nat_type = Term.exists_type (Term.exists_subtype (equal @{typ nat})) +in +fun nat_as_int ctxt thms = + let + fun norm thm uses_nat = + if not (uses_nat_type (Thm.prop_of thm)) then (thm, uses_nat) + else (Conv.fconv_rule (conv ctxt) thm, true) + val (thms', uses_nat) = fold_map norm thms false + in if uses_nat then nat_embedding @ thms' else thms' end +end + + +(* include additional rules *) + +val (unfold_defs, unfold_defs_setup) = + Attrib.config_bool "smt_unfold_defs" true + +local + val pair_rules = [@{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}] + + val pair_type = (fn Type (@{type_name "*"}, _) => true | _ => false) + val exists_pair_type = Term.exists_type (Term.exists_subtype pair_type) + + val fun_upd_rules = [@{thm fun_upd_same}, @{thm fun_upd_apply}] + val is_fun_upd = (fn Const (@{const_name fun_upd}, _) => true | _ => false) + val exists_fun_upd = Term.exists_subterm is_fun_upd +in +fun add_pair_rules _ thms = + thms + |> exists (exists_pair_type o Thm.prop_of) thms ? append pair_rules + +fun add_fun_upd_rules _ thms = + thms + |> exists (exists_fun_upd o Thm.prop_of) thms ? append fun_upd_rules +end + + +local + fun mk_entry t thm = (Term.head_of t, (thm, thm RS @{thm eq_reflection})) + fun prepare_def thm = + (case HOLogic.dest_Trueprop (Thm.prop_of thm) of + Const (@{const_name "op ="}, _) $ t $ _ => mk_entry t thm + | t => raise TERM ("prepare_def", [t])) + + val defs = map prepare_def [ + @{thm abs_if[where 'a = int]}, @{thm abs_if[where 'a = real]}, + @{thm min_def[where 'a = int]}, @{thm min_def[where 'a = real]}, + @{thm max_def[where 'a = int]}, @{thm max_def[where 'a = real]}] + + fun add_sym t = if AList.defined (op =) defs t then insert (op =) t else I + fun add_syms thms = fold (Term.fold_aterms add_sym o Thm.prop_of) thms [] + + fun unfold_conv ctxt ct = + (case AList.lookup (op =) defs (Term.head_of (Thm.term_of ct)) of + SOME (_, eq) => Conv.rewr_conv eq + | NONE => Conv.all_conv) ct +in +fun add_abs_min_max_rules ctxt thms = + if Config.get ctxt unfold_defs + then map (Conv.fconv_rule (More_Conv.bottom_conv unfold_conv ctxt)) thms + else map fst (map_filter (AList.lookup (op =) defs) (add_syms thms)) @ thms +end + + +(* lift lambda terms into additional rules *) + +local + val meta_eq = @{cpat "op =="} + val meta_eqT = hd (Thm.dest_ctyp (Thm.ctyp_of_term meta_eq)) + fun inst_meta cT = Thm.instantiate_cterm ([(meta_eqT, cT)], []) meta_eq + fun mk_meta_eq ct cu = Thm.mk_binop (inst_meta (Thm.ctyp_of_term ct)) ct cu + + fun lambda_conv conv = + let + fun sub_conv cvs ctxt ct = + (case Thm.term_of ct of + Const (@{const_name All}, _) $ Abs _ => quant_conv cvs ctxt + | Const (@{const_name Ex}, _) $ Abs _ => quant_conv cvs ctxt + | Const _ $ Abs _ => Conv.arg_conv (at_lambda_conv cvs ctxt) + | Const (@{const_name Let}, _) $ _ $ Abs _ => Conv.combination_conv + (Conv.arg_conv (sub_conv cvs ctxt)) (abs_conv cvs ctxt) + | Abs _ => at_lambda_conv cvs ctxt + | _ $ _ => Conv.comb_conv (sub_conv cvs ctxt) + | _ => Conv.all_conv) ct + and abs_conv cvs = Conv.abs_conv (fn (cv, cx) => sub_conv (cv::cvs) cx) + and quant_conv cvs ctxt = Conv.arg_conv (abs_conv cvs ctxt) + and at_lambda_conv cvs ctxt = abs_conv cvs ctxt then_conv conv cvs ctxt + in sub_conv [] end + + fun used_vars cvs ct = + let + val lookup = AList.lookup (op aconv) (map (` Thm.term_of) cvs) + val add = (fn (SOME ct) => insert (op aconvc) ct | _ => I) + in Term.fold_aterms (add o lookup) (Thm.term_of ct) [] end + + val rev_int_fst_ord = rev_order o int_ord o pairself fst + fun ordered_values tab = + Termtab.fold (fn (_, x) => OrdList.insert rev_int_fst_ord x) tab [] + |> map snd +in +fun lift_lambdas ctxt thms = + let + val declare_frees = fold (Thm.fold_terms Term.declare_term_frees) + val names = ref (declare_frees thms (Name.make_context [])) + val fresh_name = change_result names o yield_singleton Name.variants + + val defs = ref (Termtab.empty : (int * thm) Termtab.table) + fun add_def t thm = change defs (Termtab.update (t, (serial (), thm))) + fun make_def cvs eq = Thm.symmetric (fold norm_meta_def cvs eq) + fun def_conv cvs ctxt ct = + let + val cvs' = used_vars cvs ct + val ct' = fold Thm.cabs cvs' ct + in + (case Termtab.lookup (!defs) (Thm.term_of ct') of + SOME (_, eq) => make_def cvs' eq + | NONE => + let + val {t, T, ...} = Thm.rep_cterm ct' + val eq = mk_meta_eq (cert ctxt (Free (fresh_name "", T))) ct' + val thm = Thm.assume eq + in (add_def t thm; make_def cvs' thm) end) + end + val thms' = map (Conv.fconv_rule (lambda_conv def_conv ctxt)) thms + val eqs = ordered_values (!defs) + in + (maps (#hyps o Thm.crep_thm) eqs, map (normalize_rule ctxt) eqs @ thms') + end +end + + +(* make application explicit for functions with varying number of arguments *) + +local + val const = prefix "c" and free = prefix "f" + fun min i (e as (_, j)) = if i <> j then (true, Int.min (i, j)) else e + fun add t i = Symtab.map_default (t, (false, i)) (min i) + fun traverse t = + (case Term.strip_comb t of + (Const (n, _), ts) => add (const n) (length ts) #> fold traverse ts + | (Free (n, _), ts) => add (free n) (length ts) #> fold traverse ts + | (Abs (_, _, u), ts) => fold traverse (u :: ts) + | (_, ts) => fold traverse ts) + val prune = (fn (n, (true, i)) => Symtab.update (n, i) | _ => I) + fun prune_tab tab = Symtab.fold prune tab Symtab.empty + + fun binop_conv cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2 + fun nary_conv conv1 conv2 ct = + (Conv.combination_conv (nary_conv conv1 conv2) conv2 else_conv conv1) ct + fun abs_conv conv tb = Conv.abs_conv (fn (cv, cx) => + let val n = fst (Term.dest_Free (Thm.term_of cv)) + in conv (Symtab.update (free n, 0) tb) cx end) + val apply_rule = @{lemma "f x == apply f x" by (simp add: apply_def)} +in +fun explicit_application ctxt thms = + let + fun sub_conv tb ctxt ct = + (case Term.strip_comb (Thm.term_of ct) of + (Const (n, _), ts) => app_conv tb (const n) (length ts) ctxt + | (Free (n, _), ts) => app_conv tb (free n) (length ts) ctxt + | (Abs _, ts) => nary_conv (abs_conv sub_conv tb ctxt) (sub_conv tb ctxt) + | (_, ts) => nary_conv Conv.all_conv (sub_conv tb ctxt)) ct + and app_conv tb n i ctxt = + (case Symtab.lookup tb n of + NONE => nary_conv Conv.all_conv (sub_conv tb ctxt) + | SOME j => apply_conv tb ctxt (i - j)) + and apply_conv tb ctxt i ct = ( + if i = 0 then nary_conv Conv.all_conv (sub_conv tb ctxt) + else + Conv.rewr_conv apply_rule then_conv + binop_conv (apply_conv tb ctxt (i-1)) (sub_conv tb ctxt)) ct + + val tab = prune_tab (fold (traverse o Thm.prop_of) thms Symtab.empty) + in map (Conv.fconv_rule (sub_conv tab ctxt)) thms end +end + + +(* combined normalization *) + +datatype config = + RewriteTrivialLets | + RewriteNegativeNumerals | + RewriteNaturalNumbers | + AddPairRules | + AddFunUpdRules | + AddAbsMinMaxRules + +fun normalize config ctxt thms = + let fun if_enabled c f = member (op =) config c ? f ctxt + in + thms + |> if_enabled RewriteTrivialLets trivial_let + |> if_enabled RewriteNegativeNumerals positive_numerals + |> if_enabled RewriteNaturalNumbers nat_as_int + |> if_enabled AddPairRules add_pair_rules + |> if_enabled AddFunUpdRules add_fun_upd_rules + |> if_enabled AddAbsMinMaxRules add_abs_min_max_rules + |> map (normalize_rule ctxt) + |> lift_lambdas ctxt + |> apsnd (explicit_application ctxt) + end + +val setup = unfold_defs_setup + +end diff -r bfbdeddc03bc -r 35094c8fd8bf src/HOL/SMT/Tools/smt_solver.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/SMT/Tools/smt_solver.ML Mon Sep 21 08:45:31 2009 +0200 @@ -0,0 +1,248 @@ +(* Title: HOL/SMT/Tools/smt_solver.ML + Author: Sascha Boehme, TU Muenchen + +SMT solvers registry and SMT tactic. +*) + +signature SMT_SOLVER = +sig + exception SMT_COUNTEREXAMPLE of bool * term list + + datatype interface = Interface of { + normalize: SMT_Normalize.config list, + translate: SMT_Translate.config } + + datatype proof_data = ProofData of { + context: Proof.context, + output: string list, + recon: SMT_Translate.recon, + assms: thm list option } + + datatype solver_config = SolverConfig of { + name: {env_var: string, remote_name: string}, + interface: interface, + arguments: string list, + reconstruct: proof_data -> thm } + + (*options*) + val timeout: int Config.T + val with_timeout: Proof.context -> ('a -> 'b) -> 'a -> 'b + val trace: bool Config.T + val trace_msg: Proof.context -> ('a -> string) -> 'a -> unit + + (*solvers*) + type solver = Proof.context -> thm list -> thm + type solver_info = Context.generic -> Pretty.T list + val add_solver: string * (Proof.context -> solver_config) -> theory -> + theory + val all_solver_names_of: theory -> string list + val add_solver_info: string * solver_info -> theory -> theory + val solver_name_of: Context.generic -> string + val select_solver: string -> Context.generic -> Context.generic + val solver_of: Context.generic -> solver + + (*tactic*) + val smt_tac': bool -> Proof.context -> thm list -> int -> Tactical.tactic + val smt_tac: Proof.context -> thm list -> int -> Tactical.tactic + + (*setup*) + val setup: theory -> theory + val print_setup: Context.generic -> unit +end + +structure SMT_Solver: SMT_SOLVER = +struct + +exception SMT_COUNTEREXAMPLE of bool * term list + +val theory_of = Context.cases I ProofContext.theory_of + + +datatype interface = Interface of { + normalize: SMT_Normalize.config list, + translate: SMT_Translate.config } + +datatype proof_data = ProofData of { + context: Proof.context, + output: string list, + recon: SMT_Translate.recon, + assms: thm list option } + +datatype solver_config = SolverConfig of { + name: {env_var: string, remote_name: string}, + interface: interface, + arguments: string list, + reconstruct: proof_data -> thm } + + +(* SMT options *) + +val (timeout, setup_timeout) = Attrib.config_int "smt_timeout" 30 + +fun with_timeout ctxt f x = + TimeLimit.timeLimit (Time.fromSeconds (Config.get ctxt timeout)) f x + handle TimeLimit.TimeOut => error ("SMT: timeout") + +val (trace, setup_trace) = Attrib.config_bool "smt_trace" false + +fun trace_msg ctxt f x = + if Config.get ctxt trace then Output.tracing (f x) else () + + +(* interface to external solvers *) + +local + +fun with_tmp_files f x = + let + fun tmp_path () = File.tmp_path (Path.explode ("smt-" ^ serial_string ())) + val in_path = tmp_path () and out_path = tmp_path () + val y = Exn.capture (f in_path out_path) x + val _ = try File.rm in_path and _ = try File.rm out_path + in Exn.release y end + +fun run in_path out_path (ctxt, cmd, output) = + let + val x = File.open_output output in_path + val _ = trace_msg ctxt File.read in_path + + val _ = with_timeout ctxt system_out (cmd in_path out_path) + fun lines_of path = the_default [] (try (File.fold_lines cons out_path) []) + val ls = rev (dropwhile (equal "") (lines_of out_path)) + val _ = trace_msg ctxt cat_lines ls + in (x, ls) end + +in + +fun run_solver ctxt {env_var, remote_name} args output = + let + val qf = File.shell_path and qq = enclose "'" "'" + val path = getenv env_var and remote = getenv "REMOTE_SMT_SOLVER" + fun cmd f1 f2 = + if path <> "" + then map qq (path :: args) @ [qf f1, ">", qf f2] + else map qq (remote :: remote_name :: args) @ [qf f1, qf f2] + in with_tmp_files run (ctxt, space_implode " " oo cmd, output) end + +end + +fun make_proof_data ctxt ((recon, thms), ls) = + ProofData {context=ctxt, output=ls, recon=recon, assms=SOME thms} + +fun gen_solver solver ctxt prems = + let + val SolverConfig {name, interface, arguments, reconstruct} = solver ctxt + val Interface {normalize=nc, translate=tc} = interface + val thy = ProofContext.theory_of ctxt + in + SMT_Normalize.normalize nc ctxt prems + ||> run_solver ctxt name arguments o SMT_Translate.translate tc thy + ||> reconstruct o make_proof_data ctxt + |-> fold SMT_Normalize.discharge_definition + end + + +(* solver store *) + +type solver = Proof.context -> thm list -> thm +type solver_info = Context.generic -> Pretty.T list + +structure Solvers = TheoryDataFun +( + type T = ((Proof.context -> solver_config) * solver_info) Symtab.table + val empty = Symtab.empty + val copy = I + val extend = I + fun merge _ = Symtab.merge (K true) + handle Symtab.DUP name => error ("Duplicate SMT solver: " ^ quote name) +) + +val no_solver = "(none)" +val add_solver = Solvers.map o Symtab.update_new o apsnd (rpair (K [])) +val all_solver_names_of = Symtab.keys o Solvers.get +val lookup_solver = Symtab.lookup o Solvers.get +fun add_solver_info (n, i) = Solvers.map (Symtab.map_entry n (apsnd (K i))) + + +(* selected solver *) + +structure SelectedSolver = GenericDataFun +( + type T = serial * string + val empty = (serial (), no_solver) + val extend = I + fun merge _ (sl1 as (s1, _), sl2 as (s2, _)) = if s1 > s2 then sl1 else sl2 +) + +val solver_name_of = snd o SelectedSolver.get + +fun select_solver name gen = + if is_none (lookup_solver (theory_of gen) name) + then error ("SMT solver not registered: " ^ quote name) + else SelectedSolver.map (K (serial (), name)) gen + +fun raw_solver_of gen = + (case lookup_solver (theory_of gen) (solver_name_of gen) of + NONE => error "No SMT solver selected" + | SOME (s, _) => s) + +val solver_of = gen_solver o raw_solver_of + + +(* SMT tactic *) + +fun smt_unsat_tac solver ctxt rules = + Tactic.rtac @{thm ccontr} THEN' + SUBPROOF (fn {context, prems, ...} => + Tactic.rtac (solver context (rules @ prems)) 1) ctxt + +fun pretty_counterex ctxt (real, ex) = + let + val msg = if real then "Counterexample found:" + else "Potential counterexample found:" + val cex = if null ex then [Pretty.str "(no assignments)"] + else map (Syntax.pretty_term ctxt) ex + in Pretty.string_of (Pretty.big_list msg cex) end + +fun smt_tac' pass_smt_exns ctxt = + let + val solver = solver_of (Context.Proof ctxt) + fun safe_solver ctxt thms = solver ctxt thms + handle SMT_COUNTEREXAMPLE cex => error (pretty_counterex ctxt cex) + val solver' = if pass_smt_exns then solver else safe_solver + in smt_unsat_tac solver' ctxt end + +val smt_tac = smt_tac' false + + +(* setup *) + +val setup = + Attrib.setup (Binding.name "smt_solver") + (Scan.lift (OuterParse.$$$ "=" |-- Args.name) >> + (Thm.declaration_attribute o K o select_solver)) + "SMT solver configuration" #> + setup_timeout #> + setup_trace + +fun print_setup gen = + let + val t = string_of_int (Config.get_generic gen timeout) + val names = sort string_ord (all_solver_names_of (theory_of gen)) + val ns = if null names then [no_solver] else names + val take_info = (fn (_, []) => NONE | info => SOME info) + val infos = + theory_of gen + |> Symtab.dest o Solvers.get + |> map_filter (fn (n, (_, info)) => take_info (n, info gen)) + |> sort (prod_ord string_ord (K EQUAL)) + |> map (fn (n, ps) => Pretty.big_list (n ^ ":") ps) + in + Pretty.writeln (Pretty.big_list "SMT setup:" [ + Pretty.str ("Current SMT solver: " ^ solver_name_of gen), + Pretty.str_list "Available SMT solvers: " "" ns, + Pretty.str ("Current timeout: " ^ t ^ " seconds"), + Pretty.big_list "Solver-specific settings:" infos]) + end + +end diff -r bfbdeddc03bc -r 35094c8fd8bf src/HOL/SMT/Tools/smt_translate.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/SMT/Tools/smt_translate.ML Mon Sep 21 08:45:31 2009 +0200 @@ -0,0 +1,507 @@ +(* Title: HOL/SMT/Tools/smt_translate.ML + Author: Sascha Boehme, TU Muenchen + +Translate theorems into an SMT intermediate format and serialize them, +depending on an SMT interface. +*) + +signature SMT_TRANSLATE = +sig + (* intermediate term structure *) + datatype sym = + SConst of string * typ | + SFree of string * typ | + SNum of int * typ + datatype squant = SForall | SExists + datatype 'a spattern = SPat of 'a list | SNoPat of 'a list + datatype ('a, 'b) sterm = + SVar of int | + SApp of 'a * ('a, 'b) sterm list | + SLet of (string * 'b) * ('a, 'b) sterm * ('a, 'b) sterm | + SQuant of squant * (string * 'b) list * ('a, 'b) sterm spattern list * + ('a, 'b) sterm + + (* table for built-in symbols *) + type builtin_fun = typ -> (sym, typ) sterm list -> + (string * (sym, typ) sterm list) option + type builtin_table = (typ * builtin_fun) list Symtab.table + val builtin_make: (term * string) list -> builtin_table + val builtin_add: term * builtin_fun -> builtin_table -> builtin_table + val builtin_lookup: builtin_table -> theory -> string * typ -> + (sym, typ) sterm list -> (string * (sym, typ) sterm list) option + val bv_rotate: (int -> string) -> builtin_fun + val bv_extend: (int -> string) -> builtin_fun + val bv_extract: (int -> int -> string) -> builtin_fun + + (* configuration options *) + datatype prefixes = Prefixes of { + var_prefix: string, + typ_prefix: string, + fun_prefix: string, + pred_prefix: string } + datatype markers = Markers of { + term_marker: string, + formula_marker: string } + datatype builtins = Builtins of { + builtin_typ: typ -> string option, + builtin_num: int * typ -> string option, + builtin_fun: bool -> builtin_table } + datatype sign = Sign of { + typs: string list, + funs: (string * (string list * string)) list, + preds: (string * string list) list } + datatype config = Config of { + strict: bool, + prefixes: prefixes, + markers: markers, + builtins: builtins, + serialize: sign -> (string, string) sterm list -> TextIO.outstream -> unit} + datatype recon = Recon of {typs: typ Symtab.table, terms: term Symtab.table} + + val translate: config -> theory -> thm list -> TextIO.outstream -> + recon * thm list + + val dest_binT: typ -> int + val dest_funT: int -> typ -> typ list * typ +end + +structure SMT_Translate: SMT_TRANSLATE = +struct + +(* Intermediate term structure *) + +datatype sym = + SConst of string * typ | + SFree of string * typ | + SNum of int * typ +datatype squant = SForall | SExists +datatype 'a spattern = SPat of 'a list | SNoPat of 'a list +datatype ('a, 'b) sterm = + SVar of int | + SApp of 'a * ('a, 'b) sterm list | + SLet of (string * 'b) * ('a, 'b) sterm * ('a, 'b) sterm | + SQuant of squant * (string * 'b) list * ('a, 'b) sterm spattern list * + ('a, 'b) sterm + +fun app c ts = SApp (c, ts) + +fun map_pat f (SPat ps) = SPat (map f ps) + | map_pat f (SNoPat ps) = SNoPat (map f ps) + +fun fold_map_pat f (SPat ps) = fold_map f ps #>> SPat + | fold_map_pat f (SNoPat ps) = fold_map f ps #>> SNoPat + +val make_sconst = SConst o Term.dest_Const + + +(* General type destructors. *) + +fun dest_binT T = + (case T of + Type (@{type_name "Numeral_Type.num0"}, _) => 0 + | Type (@{type_name "Numeral_Type.num1"}, _) => 1 + | Type (@{type_name "Numeral_Type.bit0"}, [T]) => 2 * dest_binT T + | Type (@{type_name "Numeral_Type.bit1"}, [T]) => 1 + 2 * dest_binT T + | _ => raise TYPE ("dest_binT", [T], [])) + +val dest_wordT = (fn + Type (@{type_name "word"}, [T]) => dest_binT T + | T => raise TYPE ("dest_wordT", [T], [])) + +val dest_funT = + let + fun dest Ts 0 T = (rev Ts, T) + | dest Ts i (Type ("fun", [T, U])) = dest (T::Ts) (i-1) U + | dest _ _ T = raise TYPE ("dest_funT", [T], []) + in dest [] end + + +(* Table for built-in symbols *) + +type builtin_fun = typ -> (sym, typ) sterm list -> + (string * (sym, typ) sterm list) option +type builtin_table = (typ * builtin_fun) list Symtab.table + +fun builtin_make entries = + let + fun dest (t, bn) = + let val (n, T) = Term.dest_Const t + in (n, (Logic.varifyT T, K (SOME o pair bn))) end + in Symtab.make (AList.group (op =) (map dest entries)) end + +fun builtin_add (t, f) tab = + let val (n, T) = apsnd Logic.varifyT (Term.dest_Const t) + in Symtab.map_default (n, []) (AList.update (op =) (T, f)) tab end + +fun builtin_lookup tab thy (n, T) ts = + AList.lookup (Sign.typ_instance thy) (Symtab.lookup_list tab n) T + |> (fn SOME f => f T ts | NONE => NONE) + +local + val dest_nat = (fn + SApp (SConst (@{const_name nat}, _), [SApp (SNum (i, _), _)]) => SOME i + | _ => NONE) +in +fun bv_rotate mk_name T ts = + dest_nat (hd ts) |> Option.map (fn i => (mk_name i, tl ts)) + +fun bv_extend mk_name T ts = + (case (try dest_wordT (domain_type T), try dest_wordT (range_type T)) of + (SOME i, SOME j) => if j - i >= 0 then SOME (mk_name (j - i), ts) else NONE + | _ => NONE) + +fun bv_extract mk_name T ts = + (case (try dest_wordT (body_type T), dest_nat (hd ts)) of + (SOME i, SOME lb) => SOME (mk_name (i + lb - 1) lb, tl ts) + | _ => NONE) +end + + +(* Configuration options *) + +datatype prefixes = Prefixes of { + var_prefix: string, + typ_prefix: string, + fun_prefix: string, + pred_prefix: string } +datatype markers = Markers of { + term_marker: string, + formula_marker: string } +datatype builtins = Builtins of { + builtin_typ: typ -> string option, + builtin_num: int * typ -> string option, + builtin_fun: bool -> builtin_table } +datatype sign = Sign of { + typs: string list, + funs: (string * (string list * string)) list, + preds: (string * string list) list } +datatype config = Config of { + strict: bool, + prefixes: prefixes, + markers: markers, + builtins: builtins, + serialize: sign -> (string, string) sterm list -> TextIO.outstream -> unit} +datatype recon = Recon of {typs: typ Symtab.table, terms: term Symtab.table} + + +(* Translate Isabelle/HOL terms into SMT intermediate terms. + We assume that lambda-lifting has been performed before, i.e., lambda + abstractions occur only at quantifiers and let expressions. +*) +local + val quantifier = (fn + @{const_name All} => SOME SForall + | @{const_name Ex} => SOME SExists + | _ => NONE) + + fun group_quant qname vs (t as Const (q, _) $ Abs (n, T, u)) = + if q = qname then group_quant qname ((n, T) :: vs) u else (vs, t) + | group_quant qname vs t = (vs, t) + + fun dest_trigger (@{term trigger} $ tl $ t) = (HOLogic.dest_list tl, t) + | dest_trigger t = ([], t) + + fun pat f ps (Const (@{const_name pat}, _) $ p) = SPat (rev (f p :: ps)) + | pat f ps (Const (@{const_name nopat}, _) $ p) = SNoPat (rev (f p :: ps)) + | pat f ps (Const (@{const_name andpat}, _) $ p $ t) = pat f (f p :: ps) t + | pat _ _ t = raise TERM ("pat", [t]) + + fun trans Ts t = + (case Term.strip_comb t of + (t1 as Const (qn, qT), [t2 as Abs (n, T, t3)]) => + (case quantifier qn of + SOME q => + let + val (vs, u) = group_quant qn [(n, T)] t3 + val Us = map snd vs @ Ts + val (ps, b) = dest_trigger u + in SQuant (q, rev vs, map (pat (trans Us) []) ps, trans Us b) end + | NONE => raise TERM ("intermediate", [t])) + | (Const (@{const_name Let}, _), [t1, Abs (n, T, t2)]) => + SLet ((n, T), trans Ts t1, trans (T :: Ts) t2) + | (Const (c as (@{const_name distinct}, _)), [t1]) => + (* this is not type-correct, but will be corrected at a later stage *) + SApp (SConst c, map (trans Ts) (HOLogic.dest_list t1)) + | (Const c, ts) => + (case try HOLogic.dest_number t of + SOME (T, i) => SApp (SNum (i, T), []) + | NONE => SApp (SConst c, map (trans Ts) ts)) + | (Free c, ts) => SApp (SFree c, map (trans Ts) ts) + | (Bound i, []) => SVar i + | _ => raise TERM ("intermediate", [t])) +in +fun intermediate ts = map (trans [] o HOLogic.dest_Trueprop) ts +end + + +(* Separate formulas from terms by adding special marker symbols ("term", + "formula"). Atoms "P" whose head symbol also occurs as function symbol are + rewritten to "term P = term True". Connectives and built-in predicates + occurring at term level are replaced by new constants, and theorems + specifying their meaning are added. +*) +local + (** Add the marker symbols "term" and "formulas" to separate formulas and + terms. **) + + val connectives = map make_sconst [@{term True}, @{term False}, + @{term Not}, @{term "op &"}, @{term "op |"}, @{term "op -->"}, + @{term "op = :: bool => _"}] + + fun note false c (ps, fs) = (insert (op =) c ps, fs) + | note true c (ps, fs) = (ps, insert (op =) c fs) + + val term_marker = SConst (@{const_name term}, Term.dummyT) + val formula_marker = SConst (@{const_name formula}, Term.dummyT) + fun mark f true t = f true t #>> app term_marker o single + | mark f false t = f false t #>> app formula_marker o single + fun mark' f false t = f true t #>> app term_marker o single + | mark' f true t = f true t + val mark_term = app term_marker o single + fun lift_term_marker c ts = + let val rem = (fn SApp (SConst (@{const_name term}, _), [t]) => t | t => t) + in mark_term (SApp (c, map rem ts)) end + fun is_term (SApp (SConst (@{const_name term}, _), _)) = true + | is_term _ = false + + fun either x = (fn y as SOME _ => y | _ => x) + fun get_loc loc i t = + (case t of + SVar j => if i = j then SOME loc else NONE + | SApp (SConst (@{const_name term}, _), us) => get_locs true i us + | SApp (SConst (@{const_name formula}, _), us) => get_locs false i us + | SApp (_, us) => get_locs loc i us + | SLet (_, u1, u2) => either (get_loc true i u1) (get_loc loc (i+1) u2) + | SQuant (_, vs, _, u) => get_loc loc (i + length vs) u) + and get_locs loc i ts = fold (either o get_loc loc i) ts NONE + + fun sep loc t = + (case t of + SVar i => pair t + | SApp (c as SConst (@{const_name If}, _), u :: us) => + mark sep false u ##>> fold_map (sep loc) us #>> app c o (op ::) + | SApp (c, us) => + if not loc andalso member (op =) connectives c + then fold_map (sep loc) us #>> app c + else note loc c #> fold_map (mark' sep loc) us #>> app c + | SLet (v, u1, u2) => + sep loc u2 #-> (fn u2' => + mark sep (the (get_loc loc 0 u2')) u1 #>> (fn u1' => + SLet (v, u1', u2'))) + | SQuant (q, vs, ps, u) => + fold_map (fold_map_pat (mark sep true)) ps ##>> + sep loc u #>> (fn (ps', u') => + SQuant (q, vs, ps', u'))) + + (** Rewrite atoms. **) + + val unterm_rule = @{lemma "term x == x" by (simp add: term_def)} + val unterm_conv = More_Conv.top_sweep_conv (K (Conv.rewr_conv unterm_rule)) + + val dest_word_type = (fn Type (@{type_name word}, [T]) => T | T => T) + fun instantiate [] _ = I + | instantiate (v :: _) T = + Term.subst_TVars [(v, dest_word_type (Term.domain_type T))] + + fun dest_alls (Const (@{const_name All}, _) $ Abs (_, _, t)) = dest_alls t + | dest_alls t = t + val dest_iff = (fn (Const (@{const_name iff}, _) $ t $ _ ) => t | t => t) + val dest_eq = (fn (Const (@{const_name "op ="}, _) $ t $ _ ) => t | t => t) + val dest_not = (fn (@{term Not} $ t) => t | t => t) + val head_of = HOLogic.dest_Trueprop #> dest_alls #> dest_iff #> dest_not #> + dest_eq #> Term.head_of + + fun prepare ctxt thm = + let + val rule = Conv.fconv_rule (unterm_conv ctxt) thm + val prop = Thm.prop_of thm + val inst = instantiate (Term.add_tvar_names prop []) + fun inst_for T = (singleton intermediate (inst T prop), rule) + in (make_sconst (head_of (Thm.prop_of rule)), inst_for) end + + val logicals = map (prepare @{context}) + @{lemma + "~ holds False" + "ALL p. holds (~ p) iff (~ holds p)" + "ALL p q. holds (p & q) iff (holds p & holds q)" + "ALL p q. holds (p | q) iff (holds p | holds q)" + "ALL p q. holds (p --> q) iff (holds p --> holds q)" + "ALL p q. holds (p iff q) iff (holds p iff holds q)" + "ALL p q. holds (p = q) iff (p = q)" + "ALL (a::int) b. holds (a < b) iff (a < b)" + "ALL (a::int) b. holds (a <= b) iff (a <= b)" + "ALL (a::real) b. holds (a < b) iff (a < b)" + "ALL (a::real) b. holds (a <= b) iff (a <= b)" + "ALL (a::'a::len0 word) b. holds (a < b) iff (a < b)" + "ALL (a::'a::len0 word) b. holds (a <= b) iff (a <= b)" + "ALL a b. holds (a Option.map (fn inst_for => inst_for T) + | lookup_logical _ _ = NONE + + val s_eq = make_sconst @{term "op = :: bool => _"} + val s_True = mark_term (SApp (make_sconst @{term True}, [])) + fun holds (SApp (c, ts)) = SApp (s_eq, [lift_term_marker c ts, s_True]) + | holds t = SApp (s_eq, [mark_term t, s_True]) + + val rewr_iff = (fn + SConst (@{const_name "op ="}, T as @{typ "bool => bool => bool"}) => + SConst (@{const_name iff}, T) + | c => c) + + fun rewrite ls = + let + fun rewr env loc t = + (case t of + SVar i => if not loc andalso nth env i then holds t else t + | SApp (c as SConst (@{const_name term}, _), [u]) => + SApp (c, [rewr env true u]) + | SApp (c as SConst (@{const_name formula}, _), [u]) => + SApp (c, [rewr env false u]) + | SApp (c, us) => + let val f = if not loc andalso member (op =) ls c then holds else I + in f (SApp (rewr_iff c, map (rewr env loc) us)) end + | SLet (v, u1, u2) => + SLet (v, rewr env loc u1, rewr (is_term u1 :: env) loc u2) + | SQuant (q, vs, ps, u) => + let val e = replicate (length vs) true @ env + in SQuant (q, vs, map (map_pat (rewr e loc)) ps, rewr e loc u) end) + in map (rewr [] false) end +in +fun separate thy ts = + let + val (ts', (ps, fs)) = fold_map (sep false) ts ([], []) + val eq_name = (fn + (SConst (n, _), SConst (m, _)) => n = m + | (SFree (n, _), SFree (m, _)) => n = m + | _ => false) + val ls = filter (member eq_name fs) ps + val (us, thms) = split_list (map_filter (lookup_logical thy) fs) + in (thms, us @ rewrite ls ts') end +end + + +(* Collect the signature of intermediate terms, identify built-in symbols, + rename uninterpreted symbols and types, make bound variables unique. + We require @{term distinct} to be a built-in constant of the SMT solver. +*) +local + fun empty_nctxt p = (p, 1) + fun make_nctxt (pT, pf, pp) = (empty_nctxt pT, empty_nctxt (pf, pp)) + fun fresh_name (p, i) = (p ^ string_of_int i, (p, i+1)) + fun fresh_typ (nT, nfp) = fresh_name nT ||> (fn nT' => (nT', nfp)) + fun fresh_fun loc (nT, ((pf, pp), i)) = + let val p = if loc then pf else pp + in fresh_name (p, i) ||> (fn (_, i') => (nT, ((pf, pp), i'))) end + + val empty_sign = (Typtab.empty, Termtab.empty, Termtab.empty) + fun lookup_typ (typs, _, _) = Typtab.lookup typs + fun lookup_fun true (_, funs, _) = Termtab.lookup funs + | lookup_fun false (_, _, preds) = Termtab.lookup preds + fun add_typ x (typs, funs, preds) = (Typtab.update x typs, funs, preds) + fun add_fun true x (typs, funs, preds) = (typs, Termtab.update x funs, preds) + | add_fun false x (typs, funs, preds) = (typs, funs, Termtab.update x preds) + fun make_sign (typs, funs, preds) = Sign { + typs = map snd (Typtab.dest typs), + funs = map snd (Termtab.dest funs), + preds = map (apsnd fst o snd) (Termtab.dest preds) } + fun make_rtab (typs, funs, preds) = + let + val rTs = Typtab.dest typs |> map swap |> Symtab.make + val rts = Termtab.dest funs @ Termtab.dest preds + |> map (apfst fst o swap) |> Symtab.make + in Recon {typs=rTs, terms=rts} end + + fun either f g x = (case f x of NONE => g x | y => y) + + fun rep_typ (Builtins {builtin_typ, ...}) T (st as (vars, ns, sgn)) = + (case either builtin_typ (lookup_typ sgn) T of + SOME n => (n, st) + | NONE => + let val (n, ns') = fresh_typ ns + in (n, (vars, ns', add_typ (T, n) sgn)) end) + + fun rep_var bs (n, T) (vars, ns, sgn) = + let val (n', vars') = fresh_name vars + in (vars', ns, sgn) |> rep_typ bs T |>> pair n' end + + fun rep_fun bs loc t T i (st as (_, _, sgn0)) = + (case lookup_fun loc sgn0 t of + SOME (n, _) => (n, st) + | NONE => + let + val (Us, U) = dest_funT i T + val (uns, (vars, ns, sgn)) = + st |> fold_map (rep_typ bs) Us ||>> rep_typ bs U + val (n, ns') = fresh_fun loc ns + in (n, (vars, ns', add_fun loc (t, (n, uns)) sgn)) end) + + fun rep_num (bs as Builtins {builtin_num, ...}) (i, T) st = + (case builtin_num (i, T) of + SOME n => (n, st) + | NONE => rep_fun bs true (HOLogic.mk_number T i) T 0 st) +in +fun signature_of prefixes markers builtins thy ts = + let + val Prefixes {var_prefix, typ_prefix, fun_prefix, pred_prefix} = prefixes + val Markers {formula_marker, term_marker} = markers + val Builtins {builtin_fun, ...} = builtins + + fun sign loc t = + (case t of + SVar i => pair (SVar i) + | SApp (c as SConst (@{const_name term}, _), [u]) => + sign true u #>> app term_marker o single + | SApp (c as SConst (@{const_name formula}, _), [u]) => + sign false u #>> app formula_marker o single + | SApp (SConst (c as (_, T)), ts) => + (case builtin_lookup (builtin_fun loc) thy c ts of + SOME (n, ts') => fold_map (sign loc) ts' #>> app n + | NONE => + rep_fun builtins loc (Const c) T (length ts) ##>> + fold_map (sign loc) ts #>> SApp) + | SApp (SFree (c as (_, T)), ts) => + rep_fun builtins loc (Free c) T (length ts) ##>> + fold_map (sign loc) ts #>> SApp + | SApp (SNum n, _) => rep_num builtins n #>> (fn n => SApp (n, [])) + | SLet (v, u1, u2) => + rep_var builtins v #-> (fn v' => + sign loc u1 ##>> sign loc u2 #>> (fn (u1', u2') => + SLet (v', u1', u2'))) + | SQuant (q, vs, ps, u) => + fold_map (rep_var builtins) vs ##>> + fold_map (fold_map_pat (sign loc)) ps ##>> + sign loc u #>> (fn ((vs', ps'), u') => + SQuant (q, vs', ps', u'))) + in + (empty_nctxt var_prefix, make_nctxt (typ_prefix, fun_prefix, pred_prefix), + empty_sign) + |> fold_map (sign false) ts + |> (fn (us, (_, _, sgn)) => (make_rtab sgn, (make_sign sgn, us))) + end +end + + +(* Combination of all translation functions and invocation of serialization. *) + +fun translate config thy thms stream = + let val Config {strict, prefixes, markers, builtins, serialize} = config + in + map Thm.prop_of thms + |> SMT_Monomorph.monomorph thy + |> intermediate + |> (if strict then separate thy else pair []) + ||>> signature_of prefixes markers builtins thy + ||> (fn (sgn, ts) => serialize sgn ts stream) + |> (fn ((thms', rtab), _) => (rtab, thms' @ thms)) + end + +end diff -r bfbdeddc03bc -r 35094c8fd8bf src/HOL/SMT/Tools/smtlib_interface.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/SMT/Tools/smtlib_interface.ML Mon Sep 21 08:45:31 2009 +0200 @@ -0,0 +1,168 @@ +(* Title: HOL/SMT/Tools/smtlib_interface.ML + Author: Sascha Boehme, TU Muenchen + +Interface to SMT solvers based on the SMT-LIB format. +*) + +signature SMTLIB_INTERFACE = +sig + val basic_builtins: SMT_Translate.builtins + val default_attributes: string list + val gen_interface: SMT_Translate.builtins -> string list -> + SMT_Solver.interface + val interface: SMT_Solver.interface +end + +structure SMTLIB_Interface: SMTLIB_INTERFACE = +struct + +structure T = SMT_Translate + + +(* built-in types, functions and predicates *) + +val builtin_typ = (fn + @{typ int} => SOME "Int" + | @{typ real} => SOME "Real" + | _ => NONE) + +val builtin_num = (fn + (i, @{typ int}) => SOME (string_of_int i) + | (i, @{typ real}) => SOME (string_of_int i ^ ".0") + | _ => NONE) + +val builtin_funcs = T.builtin_make [ + (@{term If}, "ite"), + (@{term "uminus :: int => _"}, "~"), + (@{term "plus :: int => _"}, "+"), + (@{term "minus :: int => _"}, "-"), + (@{term "times :: int => _"}, "*"), + (@{term "uminus :: real => _"}, "~"), + (@{term "plus :: real => _"}, "+"), + (@{term "minus :: real => _"}, "-"), + (@{term "times :: real => _"}, "*") ] + +val builtin_preds = T.builtin_make [ + (@{term True}, "true"), + (@{term False}, "false"), + (@{term Not}, "not"), + (@{term "op &"}, "and"), + (@{term "op |"}, "or"), + (@{term "op -->"}, "implies"), + (@{term "op iff"}, "iff"), + (@{term If}, "if_then_else"), + (@{term distinct}, "distinct"), + (@{term "op ="}, "="), + (@{term "op < :: int => _"}, "<"), + (@{term "op <= :: int => _"}, "<="), + (@{term "op < :: real => _"}, "<"), + (@{term "op <= :: real => _"}, "<=") ] + + +(* serialization *) + +fun wr s stream = (TextIO.output (stream, s); stream) +fun wr_line f = f #> wr "\n" + +fun sep f = wr " " #> f +fun par f = sep (wr "(" #> f #> wr ")") + +fun wr1 s = sep (wr s) +fun wrn f n = (fn [] => wr1 n | ts => par (wr n #> fold f ts)) +fun ins s f = (fn [] => I | x::xs => f x #> fold (fn x => wr1 s #> f x) xs) + +val term_marker = "__term" +val formula_marker = "__form" +fun dest_marker (T.SApp ("__term", [t])) = SOME (true, t) + | dest_marker (T.SApp ("__form", [t])) = SOME (false, t) + | dest_marker _ = NONE + +val tvar = prefix "?" +val fvar = prefix "$" + +fun wr_expr loc env t = + (case t of + T.SVar i => wr1 (nth env i) + | T.SApp (n, ts) => + (case dest_marker t of + SOME (loc', t') => wr_expr loc' env t' + | NONE => wrn (wr_expr loc env) n ts) + | T.SLet ((v, _), t1, t2) => + if loc then raise TERM ("SMTLIB: let expression in term", []) + else + let + val (loc', t1') = the (dest_marker t1) + val (kind, v') = if loc' then ("let", tvar v) else ("flet", fvar v) + in + par (wr kind #> par (wr v' #> wr_expr loc' env t1') #> + wr_expr loc (v' :: env) t2) + end + | T.SQuant (q, vs, ps, b) => + let + val wr_quant = wr o (fn T.SForall => "forall" | T.SExists => "exists") + fun wr_var (n, s) = par (wr (tvar n) #> wr1 s) + + val wre = wr_expr loc (map (tvar o fst) (rev vs) @ env) + + fun wrp s ts = wr1 (":" ^ s ^ "{") #> ins "," wre ts #> wr1 "}" + fun wr_pat (T.SPat ts) = wrp "pat" ts + | wr_pat (T.SNoPat ts) = wrp "nopat" ts + in par (wr_quant q #> fold wr_var vs #> wre b #> fold wr_pat ps) end) + +fun serialize attributes (T.Sign {typs, funs, preds}) ts stream = + let + fun wr_decl (n, Ts) = wr_line (sep (par (wr n #> fold wr1 Ts))) + in + stream + |> wr_line (wr "(benchmark Isabelle") + |> fold (wr_line o wr) attributes + |> length typs > 0 ? + wr_line (wr ":extrasorts" #> par (fold wr1 typs)) + |> length funs > 0 ? ( + wr_line (wr ":extrafuns (") #> + fold (wr_decl o apsnd (fn (Ts, T) => Ts @ [T])) funs #> + wr_line (wr " )")) + |> length preds > 0 ? ( + wr_line (wr ":extrapreds (") #> + fold wr_decl preds #> + wr_line (wr " )")) + |> fold (fn t => wr ":assumption" #> wr_line (wr_expr false [] t)) ts + |> wr_line (wr ":formula true") + |> wr_line (wr ")") + |> K () + end + + +(* SMT solver interface using the SMT-LIB input format *) + +val basic_builtins = T.Builtins { + builtin_typ = builtin_typ, + builtin_num = builtin_num, + builtin_fun = (fn true => builtin_funcs | false => builtin_preds) } + +val default_attributes = [":logic AUFLIRA", ":status unknown"] + +fun gen_interface builtins attributes = SMT_Solver.Interface { + normalize = [ + SMT_Normalize.RewriteTrivialLets, + SMT_Normalize.RewriteNegativeNumerals, + SMT_Normalize.RewriteNaturalNumbers, + SMT_Normalize.AddAbsMinMaxRules, + SMT_Normalize.AddPairRules, + SMT_Normalize.AddFunUpdRules ], + translate = T.Config { + strict = true, + prefixes = T.Prefixes { + var_prefix = "x", + typ_prefix = "T", + fun_prefix = "uf_", + pred_prefix = "up_" }, + markers = T.Markers { + term_marker = term_marker, + formula_marker = formula_marker }, + builtins = builtins, + serialize = serialize attributes }} + +val interface = gen_interface basic_builtins default_attributes + +end diff -r bfbdeddc03bc -r 35094c8fd8bf src/HOL/SMT/Tools/yices_solver.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/SMT/Tools/yices_solver.ML Mon Sep 21 08:45:31 2009 +0200 @@ -0,0 +1,52 @@ +(* Title: HOL/SMT/Tools/yices_solver.ML + Author: Sascha Boehme, TU Muenchen + +Interface of the SMT solver Yices. +*) + +signature YICES_SOLVER = +sig + val setup: theory -> theory +end + +structure Yices_Solver: YICES_SOLVER = +struct + +val solver_name = "yices" +val env_var = "YICES_SOLVER" + +val options = ["--evidence", "--smtlib"] + +fun cex_kind true = "Counterexample" + | cex_kind false = "Possible counterexample" + +fun raise_cex real ctxt rtab ls = + let val p = Pretty.big_list (cex_kind real ^ " found:") (map Pretty.str ls) + in error (Pretty.string_of p) end + +structure S = SMT_Solver + +fun core_oracle (SMT_Solver.ProofData {context, output, recon, ...}) = + let + val empty_line = (fn "" => true | _ => false) + val split_first = (fn [] => ("", []) | l :: ls => (l, ls)) + val (l, ls) = split_first (dropwhile empty_line output) + in + if String.isPrefix "unsat" l then @{cprop False} + else if String.isPrefix "sat" l then raise_cex true context recon ls + else if String.isPrefix "unknown" l then raise_cex false context recon ls + else error (solver_name ^ " failed") + end + +fun smtlib_solver oracle _ = + SMT_Solver.SolverConfig { + name = {env_var=env_var, remote_name=solver_name}, + interface = SMTLIB_Interface.interface, + arguments = options, + reconstruct = oracle } + +val setup = + Thm.add_oracle (Binding.name solver_name, core_oracle) #-> (fn (_, oracle) => + SMT_Solver.add_solver (solver_name, smtlib_solver oracle)) + +end diff -r bfbdeddc03bc -r 35094c8fd8bf src/HOL/SMT/Tools/z3_interface.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/SMT/Tools/z3_interface.ML Mon Sep 21 08:45:31 2009 +0200 @@ -0,0 +1,98 @@ +(* Title: HOL/SMT/Tools/z3_interface.ML + Author: Sascha Boehme, TU Muenchen + +Interface to Z3 based on a relaxed version of SMT-LIB. +*) + +signature Z3_INTERFACE = +sig + val interface: SMT_Solver.interface +end + +structure Z3_Interface: Z3_INTERFACE = +struct + +structure T = SMT_Translate + +fun mk_name1 n i = n ^ "[" ^ string_of_int i ^ "]" +fun mk_name2 n i j = n ^ "[" ^ string_of_int i ^ ":" ^ string_of_int j ^ "]" + +val builtin_typ = (fn + @{typ int} => SOME "Int" + | @{typ real} => SOME "Real" + | Type (@{type_name word}, [T]) => + Option.map (mk_name1 "BitVec") (try T.dest_binT T) + | _ => NONE) + +val builtin_num = (fn + (i, @{typ int}) => SOME (string_of_int i) + | (i, @{typ real}) => SOME (string_of_int i ^ ".0") + | (i, Type (@{type_name word}, [T])) => + Option.map (mk_name1 ("bv" ^ string_of_int i)) (try T.dest_binT T) + | _ => NONE) + +val builtin_funcs = T.builtin_make [ + (@{term If}, "ite"), + (@{term "uminus :: int => _"}, "~"), + (@{term "plus :: int => _"}, "+"), + (@{term "minus :: int => _"}, "-"), + (@{term "times :: int => _"}, "*"), + (@{term "op div :: int => _"}, "div"), + (@{term "op mod :: int => _"}, "mod"), + (@{term "op rem"}, "rem"), + (@{term "uminus :: real => _"}, "~"), + (@{term "plus :: real => _"}, "+"), + (@{term "minus :: real => _"}, "-"), + (@{term "times :: real => _"}, "*"), + (@{term "op / :: real => _"}, "/"), + (@{term "bitNOT :: 'a::len0 word => _"}, "bvnot"), + (@{term "op AND :: 'a::len0 word => _"}, "bvand"), + (@{term "op OR :: 'a::len0 word => _"}, "bvor"), + (@{term "op XOR :: 'a::len0 word => _"}, "bvxor"), + (@{term "uminus :: 'a::len0 word => _"}, "bvneg"), + (@{term "op + :: 'a::len0 word => _"}, "bvadd"), + (@{term "op - :: 'a::len0 word => _"}, "bvsub"), + (@{term "op * :: 'a::len0 word => _"}, "bvmul"), + (@{term "op div :: 'a::len0 word => _"}, "bvudiv"), + (@{term "op mod :: 'a::len0 word => _"}, "bvurem"), + (@{term "op sdiv"}, "bvsdiv"), + (@{term "op smod"}, "bvsmod"), + (@{term "op srem"}, "bvsrem"), + (@{term word_cat}, "concat"), + (@{term bv_shl}, "bvshl"), + (@{term bv_lshr}, "bvlshr"), + (@{term bv_ashr}, "bvashr")] + |> T.builtin_add (@{term slice}, T.bv_extract (mk_name2 "extract")) + |> T.builtin_add (@{term ucast}, T.bv_extend (mk_name1 "zero_extend")) + |> T.builtin_add (@{term scast}, T.bv_extend (mk_name1 "sign_extend")) + |> T.builtin_add (@{term word_rotl}, T.bv_rotate (mk_name1 "rotate_left")) + |> T.builtin_add (@{term word_rotr}, T.bv_rotate (mk_name1 "rotate_right")) + +val builtin_preds = T.builtin_make [ + (@{term True}, "true"), + (@{term False}, "false"), + (@{term Not}, "not"), + (@{term "op &"}, "and"), + (@{term "op |"}, "or"), + (@{term "op -->"}, "implies"), + (@{term "op iff"}, "iff"), + (@{term If}, "if_then_else"), + (@{term distinct}, "distinct"), + (@{term "op ="}, "="), + (@{term "op < :: int => _"}, "<"), + (@{term "op <= :: int => _"}, "<="), + (@{term "op < :: real => _"}, "<"), + (@{term "op <= :: real => _"}, "<="), + (@{term "op < :: 'a::len0 word => _"}, "bvult"), + (@{term "op <= :: 'a::len0 word => _"}, "bvule"), + (@{term word_sless}, "bvslt"), + (@{term word_sle}, "bvsle")] + +val builtins = T.Builtins { + builtin_typ = builtin_typ, + builtin_num = builtin_num, + builtin_fun = (fn true => builtin_funcs | false => builtin_preds) } + +val interface = SMTLIB_Interface.gen_interface builtins [] + +end diff -r bfbdeddc03bc -r 35094c8fd8bf src/HOL/SMT/Tools/z3_model.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/SMT/Tools/z3_model.ML Mon Sep 21 08:45:31 2009 +0200 @@ -0,0 +1,159 @@ +(* Title: HOL/SMT/Tools/z3_model.ML + Author: Sascha Boehme and Philipp Meyer, TU Muenchen + +Parser for counterexamples generated by Z3. +*) + +signature Z3_MODEL = +sig + val parse_counterex: SMT_Translate.recon -> string list -> term list +end + +structure Z3_Model: Z3_MODEL = +struct + +(* parsing primitives *) + +fun lift f (x, y) = apsnd (pair x) (f y) +fun lift' f v (x, y) = apsnd (rpair y) (f v x) + +fun $$ s = lift (Scan.$$ s) +fun this s = lift (Scan.this_string s) + +fun par scan = $$ "(" |-- scan --| $$ ")" + +val digit = (fn + "0" => SOME 0 | "1" => SOME 1 | "2" => SOME 2 | "3" => SOME 3 | + "4" => SOME 4 | "5" => SOME 5 | "6" => SOME 6 | "7" => SOME 7 | + "8" => SOME 8 | "9" => SOME 9 | _ => NONE) + +val nat_num = Scan.repeat1 (Scan.some digit) >> + (fn ds => fold (fn d => fn i => i * 10 + d) ds 0) +val int_num = Scan.optional (Scan.$$ "-" >> K (fn i => ~i)) I :|-- + (fn sign => nat_num >> sign) + +val is_char = Symbol.is_ascii_letter orf Symbol.is_ascii_digit orf + member (op =) (explode "_+*-/%~=<>$&|?!.@^#") +val name = Scan.many1 is_char >> implode + + +(* parsing counterexamples *) + +datatype context = Context of { + ttab: term Symtab.table, + nctxt: Name.context, + vtab: term Inttab.table } + +fun make_context (ttab, nctxt, vtab) = + Context {ttab=ttab, nctxt=nctxt, vtab=vtab} + +fun empty_context (SMT_Translate.Recon {terms, ...}) = + let + val ns = Symtab.fold (Term.add_free_names o snd) terms [] + val nctxt = Name.make_context ns + in make_context (terms, nctxt, Inttab.empty) end + +fun map_context f (Context {ttab, nctxt, vtab}) = + make_context (f (ttab, nctxt, vtab)) + +fun fresh_name (cx as Context {nctxt, ...}) = + let val (n, nctxt') = yield_singleton Name.variants "" nctxt + in (n, map_context (fn (ttab, _, vtab) => (ttab, nctxt', vtab)) cx) end + +fun ident name (cx as Context {ttab, ...}) = + (case Symtab.lookup ttab name of + SOME t => (t, cx) + | NONE => + let val (n, cx') = fresh_name cx + in (Free (n, Term.dummyT), cx) end) + +fun set_value t i = map_context (fn (ttab, nctxt, vtab) => + (ttab, nctxt, Inttab.update (i, t) vtab)) + +fun get_value T i (cx as Context {vtab, ...}) = + (case Inttab.lookup vtab i of + SOME t => (t, cx) + | _ => cx |> fresh_name |-> (fn n => + let val t = Free (n, T) + in set_value t i #> pair t end)) + + +fun space s = lift (Scan.many Symbol.is_ascii_blank) s +fun spaced p = p --| space + +val key = spaced (lift name) #-> lift' ident +val mapping = spaced (this "->") +fun in_braces p = spaced ($$ "{") |-- p --| spaced ($$ "}") + +val bool_expr = + this "true" >> K @{term True} || + this "false" >> K @{term False} + +fun number_expr T = + let + val num = lift int_num >> HOLogic.mk_number T + fun frac n d = Const (@{const_name divide}, T --> T --> T) $ n $ d + in num :|-- (fn n => Scan.optional ($$ "/" |-- num >> frac n) n) end + +val value = this "val!" |-- lift nat_num +fun value_expr T = value #-> lift' (get_value T) + +val domT = Term.domain_type +val ranT = Term.range_type +fun const_array T t = Abs ("x", T, t) +fun upd_array T ((a, t), u) = + Const (@{const_name fun_upd}, [T, domT T, ranT T] ---> T) $ a $ t $ u +fun array_expr T st = if not (can domT T) then Scan.fail st else st |> ( + par (spaced (this "const") |-- expr (ranT T)) >> const_array (domT T) || + par (spaced (this "store") |-- spaced (array_expr T) -- + expr (Term.domain_type T) -- expr (Term.range_type T)) >> upd_array T) + +and expr T st = + spaced (bool_expr || number_expr T || value_expr T || array_expr T) st + +fun const_val t = + let fun rep u = spaced value #-> apfst o set_value u #> pair [] + in + if can HOLogic.dest_number t then rep t + else if t = @{term TT} then rep @{term True} + else expr (Term.fastype_of t) >> (fn u => [HOLogic.mk_eq (t, u)]) + end + +fun func_value T = mapping |-- expr T + +fun first_pat T = + let + fun args T = if not (can domT T) then Scan.succeed [] else + expr (domT T) ::: args (ranT T) + fun value ts = func_value (snd (SMT_Translate.dest_funT (length ts) T)) + in args T :-- value end + +fun func_pat (Ts, T) = fold_map expr Ts -- func_value T +fun else_pat (Ts, T) = + let fun else_arg T cx = cx |> fresh_name |>> (fn n => Free (n, T)) + in + fold_map (lift' else_arg) Ts ##>> + spaced (this "else") |-- func_value T + end +fun next_pats T (fts as (ts, _)) = + let val Tps = SMT_Translate.dest_funT (length ts) T + in Scan.repeat (func_pat Tps) @@@ (else_pat Tps >> single) >> cons fts end + +fun mk_def' f (ts, t) = HOLogic.mk_eq (Term.list_comb (f, ts), t) +fun mk_def (Const (@{const_name apply}, _)) (u :: us, t) = mk_def' u (us, t) + | mk_def f (ts, t) = mk_def' f (ts, t) +fun func_pats t = + let val T = Term.fastype_of t + in first_pat T :|-- next_pats T >> map (mk_def t) end + +val assign = + key --| mapping :|-- (fn t => in_braces (func_pats t) || const_val t) + +val cex = space |-- Scan.repeat assign + +fun parse_counterex recon ls = + (empty_context recon, explode (cat_lines ls)) + |> Scan.catch (Scan.finite' Symbol.stopper (Scan.error cex)) + |> flat o fst + +end diff -r bfbdeddc03bc -r 35094c8fd8bf src/HOL/SMT/Tools/z3_solver.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/SMT/Tools/z3_solver.ML Mon Sep 21 08:45:31 2009 +0200 @@ -0,0 +1,83 @@ +(* Title: HOL/SMT/Tools/z3_solver.ML + Author: Sascha Boehme, TU Muenchen + +Interface of the SMT solver Z3. +*) + +signature Z3_SOLVER = +sig + val proofs: bool Config.T + val options: string Config.T + + val setup: theory -> theory +end + +structure Z3_Solver: Z3_SOLVER = +struct + +val solver_name = "z3" +val env_var = "Z3_SOLVER" + +val (proofs, proofs_setup) = Attrib.config_bool "z3_proofs" false +val (options, options_setup) = Attrib.config_string "z3_options" "" + +fun add xs ys = ys @ xs + +fun get_options ctxt = + ["MODEL=true", "PRE_SIMPLIFY_EXPR=false", "CONTEXT_SIMPLIFIER=false"] + |> Config.get ctxt proofs ? add ["DISPLAY_PROOF=true", "PROOF_MODE=2"] + |> add (space_explode " " (Config.get ctxt options)) + +fun pretty_config context = [ + Pretty.str ("With proofs: " ^ + (if Config.get_generic context proofs then "true" else "false")), + Pretty.str ("Options: " ^ + space_implode " " (get_options (Context.proof_of context))) ] + +fun cmdline_options ctxt = + get_options ctxt + |> add ["-smt"] + +fun raise_cex real recon ls = + let val cex = Z3_Model.parse_counterex recon ls + in raise SMT_Solver.SMT_COUNTEREXAMPLE (real, cex) end + +fun check_unsat recon output = + let + val raw = not o String.isPrefix "WARNING" orf String.isPrefix "ERROR" + val (ls, l) = the_default ([], "") (try split_last (filter raw output)) + in + if String.isPrefix "unsat" l then ls + else if String.isPrefix "sat" l then raise_cex true recon ls + else if String.isPrefix "unknown" l then raise_cex false recon ls + else error (solver_name ^ " failed") + end + +fun core_oracle (SMT_Solver.ProofData {output, recon, ...}) = + check_unsat recon output + |> K @{cprop False} + +(* FIXME +fun prover (SMT_Solver.ProofData {context, output, recon, assms}) = + check_unsat recon output + |> Z3_Proof.reconstruct context assms recon +*) + +fun solver oracle ctxt = + let val with_proof = Config.get ctxt proofs + in + SMT_Solver.SolverConfig { + name = {env_var=env_var, remote_name=solver_name}, + interface = Z3_Interface.interface, + arguments = cmdline_options ctxt, + reconstruct = (*FIXME:if with_proof then prover else*) oracle } + end + +val setup = + proofs_setup #> + options_setup #> + Thm.add_oracle (Binding.name solver_name, core_oracle) #-> (fn (_, oracle) => + SMT_Solver.add_solver (solver_name, solver oracle)) #> + SMT_Solver.add_solver_info (solver_name, pretty_config) + +end diff -r bfbdeddc03bc -r 35094c8fd8bf src/HOL/SMT/etc/settings --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/SMT/etc/settings Mon Sep 21 08:45:31 2009 +0200 @@ -0,0 +1,13 @@ +ISABELLE_SMT="$COMPONENT" + +REMOTE_SMT_SOLVER="$ISABELLE_SMT/lib/scripts/remote_smt.pl" + +REMOTE_SMT_URL="http://www4.in.tum.de/smt/smt" + +# +# Paths to local SMT solvers: +# +# CVC_SOLVER=PATH +# YICES_SOLVER=PATH +# Z3_SOLVER=PATH + diff -r bfbdeddc03bc -r 35094c8fd8bf src/HOL/SMT/lib/scripts/remote_smt.pl --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/SMT/lib/scripts/remote_smt.pl Mon Sep 21 08:45:31 2009 +0200 @@ -0,0 +1,43 @@ +#!/usr/bin/env perl -w +# +# Script to invoke remote SMT solvers. +# Author: Sascha Boehme, TU Muenchen +# + +use strict; +use LWP; + + +# environment + +my $remote_smt_url = $ENV{"REMOTE_SMT_URL"}; + + +# arguments + +my $solver = $ARGV[0]; +my @options = @ARGV[1 .. ($#ARGV - 2)]; +my $problem_file = $ARGV[-2]; +my $output_file = $ARGV[-1]; + + +# call solver + +my $agent = LWP::UserAgent->new; +$agent->agent("SMT-Request"); +$agent->timeout(180); +my $response = $agent->post($remote_smt_url, [ + "Solver" => $solver, + "Options" => join(" ", @options), + "Problem" => [$problem_file] ], + "Content_Type" => "form-data"); +if (not $response->is_success) { + print "HTTP-Error: " . $response->message . "\n"; + exit 1; +} +else { + open(FILE, ">$output_file"); + print FILE $response->content; + close(FILE); +} +