--- 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
--- 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.
--- 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
--- 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
--- /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 \<or> \<not>p" by smt
+lemma "(p \<and> True) = p" by smt
+lemma "(p \<or> q) \<and> \<not>p \<Longrightarrow> q" by smt
+lemma "(a \<and> b) \<or> (c \<and> d) \<Longrightarrow> (a \<and> b) \<or> (c \<and> d)" by smt
+lemma "P=P=P=P=P=P=P=P=P=P" by smt
+
+axiomatization symm_f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
+ symm_f: "symm_f x y = symm_f y x"
+lemma "a = a \<and> 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 \<ge> abs (x + y)" by smt
+lemma "let x = (2 :: int) in x + x \<noteq> 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 "\<lbrakk> 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 \<rbrakk>
+ \<Longrightarrow> x1 = x10 & x2 = (x11::int)"
+ by smt
+
+lemma "\<exists>x::int. 0 < x" by smt
+lemma "\<exists>x::real. 0 < x" by smt
+lemma "\<forall>x y::int. x < y \<longrightarrow> (2 * x + 1) < (2 * y)" by smt
+lemma "\<forall>x y::int. (2 * x + 1) \<noteq> (2 * y)" by smt
+lemma "~ (\<exists>x y z::int. 4 * x + -6 * y = (1::int))" by smt
+lemma "~ (\<exists>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 \<Longrightarrow> (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 \<or> P = (x - 1 = y) \<or> (\<not>P \<longrightarrow> 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 \<Longrightarrow> (w :: 16 word) AND 0x00FF = w" by smt
+
+end
+
+
+section {* Pairs *}
+
+lemma "fst (x, y) = a \<Longrightarrow> x = a" by smt
+lemma "p1 = (x, y) \<and> p2 = (y, x) \<Longrightarrow> fst p1 = snd p2" by smt
+
+
+section {* Higher-order problems and recursion *}
+
+lemma "(f g x = (g x \<and> True)) \<or> (f g x = True) \<or> (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 \<le> (a :: 4 word)) = P True" using [[smt_solver=z3]] by smt
+lemma "id 3 = 3 \<and> id True = True" by (smt add: id_def)
+lemma "i \<noteq> i1 \<and> i \<noteq> i2 \<Longrightarrow> ((f (i1 := v1)) (i2 := v2)) i = f i" by smt
+lemma "map (\<lambda>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 \<Rightarrow> 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 \<Rightarrow> nat list \<Rightarrow> int"
+ where
+ eval_dioph_mod:
+ "eval_dioph ks xs mod int n = eval_dioph ks (map (\<lambda>x. x mod n) xs) mod int n"
+ and
+ eval_dioph_div_mult:
+ "eval_dioph ks (map (\<lambda>x. x div n) xs) * int n +
+ eval_dioph ks (map (\<lambda>x. x mod n) xs) = eval_dioph ks xs"
+lemma
+ "(eval_dioph ks xs = l) =
+ (eval_dioph ks (map (\<lambda>x. x mod 2) xs) mod 2 = l mod 2 \<and>
+ eval_dioph ks (map (\<lambda>x. x div 2) xs) =
+ (l - eval_dioph ks (map (\<lambda>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 \<Rightarrow> bool" where "P x = True"
+lemma poly_P: "P x \<and> (P [x] \<or> \<not>P[x])" by (simp add: P_def)
+lemma "P (1::int)" by (smt add: poly_P)
+
+consts g :: "'a \<Rightarrow> 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
--- /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
--- /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";
--- /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
+
--- /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 \<Rightarrow> pattern"
+where "pat _ = Pattern"
+
+definition nopat :: "bool \<Rightarrow> pattern"
+where "nopat _ = Pattern"
+
+definition andpat :: "pattern \<Rightarrow> 'a \<Rightarrow> pattern" (infixl "andpat" 60)
+where "_ andpat _ = Pattern"
+
+definition trigger :: "pattern list \<Rightarrow> bool \<Rightarrow> bool"
+where "trigger _ P = P"
+
+
+section {* Arithmetic *}
+
+text {*
+The sign of @{term "op mod :: int \<Rightarrow> int \<Rightarrow> 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 \<Rightarrow> int \<Rightarrow> int" (infixl "rem" 70)
+where "a rem b =
+ (if (a \<ge> 0 \<and> b < 0) \<or> (a < 0 \<and> b \<ge> 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 \<Rightarrow> 'a word \<Rightarrow> 'a word" (infix "sdiv" 70)
+where "w1 sdiv w2 = word_of_int (sint w1 div sint w2)"
+
+definition smod :: "'a::len word \<Rightarrow> 'a word \<Rightarrow> '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 \<Rightarrow> 'a word \<Rightarrow> '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 \<Rightarrow> 'a word \<Rightarrow> 'a word"
+where "bv_shl w1 w2 = (w1 << unat w2)"
+
+definition bv_lshr :: "'a::len0 word \<Rightarrow> 'a word \<Rightarrow> 'a word"
+where "bv_lshr w1 w2 = (w1 >> unat w2)"
+
+definition bv_ashr :: "'a::len word \<Rightarrow> 'a word \<Rightarrow> '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 \<Rightarrow> 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 \<Rightarrow> bool" where "holds \<equiv> (\<lambda>P. term P = term True)"
+
+text {*
+The following constant represents equivalence, to be treated differently than
+the (polymorphic) equality predicate:
+*}
+
+definition iff :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infix "iff" 50) where
+ "(x iff y) = (x = y)"
+
+end
+
--- /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
--- /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
--- /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
--- /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
--- /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
--- /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 <s b) iff (a <s b)"
+ "ALL a b. holds (a <=s b) iff (a <=s b)"
+ by (simp_all add: term_def iff_def)}
+
+ fun is_instance thy (SConst (n, T), SConst (m, U)) =
+ (n = m) andalso Sign.typ_instance thy (T, U)
+ | is_instance _ _ = false
+
+ fun lookup_logical thy (c as SConst (_, T)) =
+ AList.lookup (is_instance thy) logicals c
+ |> 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
--- /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
--- /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
--- /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
--- /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
--- /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
--- /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
+
--- /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);
+}
+