added new method "smt": an oracle-based connection to external SMT solvers
authorboehmes
Fri Sep 18 18:13:19 2009 +0200 (2009-09-18)
changeset 3261842865636d006
parent 32608 c0056c2c1d17
child 32619 02f45a09a9f2
added new method "smt": an oracle-based connection to external SMT solvers
CONTRIBUTORS
NEWS
etc/components
src/HOL/IsaMakefile
src/HOL/SMT/Examples/SMT_Examples.thy
src/HOL/SMT/IsaMakefile
src/HOL/SMT/ROOT.ML
src/HOL/SMT/SMT.thy
src/HOL/SMT/SMT_Definitions.thy
src/HOL/SMT/Tools/cvc3_solver.ML
src/HOL/SMT/Tools/smt_builtin.ML
src/HOL/SMT/Tools/smt_monomorph.ML
src/HOL/SMT/Tools/smt_normalize.ML
src/HOL/SMT/Tools/smt_solver.ML
src/HOL/SMT/Tools/smt_translate.ML
src/HOL/SMT/Tools/smtlib_interface.ML
src/HOL/SMT/Tools/yices_solver.ML
src/HOL/SMT/Tools/z3_interface.ML
src/HOL/SMT/Tools/z3_model.ML
src/HOL/SMT/Tools/z3_solver.ML
src/HOL/SMT/etc/settings
src/HOL/SMT/lib/scripts/remote_smt.pl
     1.1 --- a/CONTRIBUTORS	Fri Sep 18 14:40:24 2009 +0200
     1.2 +++ b/CONTRIBUTORS	Fri Sep 18 18:13:19 2009 +0200
     1.3 @@ -7,6 +7,9 @@
     1.4  Contributions to this Isabelle version
     1.5  --------------------------------------
     1.6  
     1.7 +* September 2009: Sascha Boehme, TUM
     1.8 +  SMT method using external SMT solvers
     1.9 +
    1.10  * September 2009: Florian Haftmann, TUM
    1.11    Refinement of Sets and Lattices
    1.12  
     2.1 --- a/NEWS	Fri Sep 18 14:40:24 2009 +0200
     2.2 +++ b/NEWS	Fri Sep 18 18:13:19 2009 +0200
     2.3 @@ -18,6 +18,13 @@
     2.4  
     2.5  *** HOL ***
     2.6  
     2.7 +* New proof method "smt" for a combination of first-order logic
     2.8 +with equality, linear and nonlinear (natural/integer/real)
     2.9 +arithmetic, and fixed-size bitvectors; there is also basic
    2.10 +support for higher-order features (esp. lambda abstractions).
    2.11 +It is an incomplete decision procedure based on external SMT
    2.12 +solvers using the oracle mechanism.
    2.13 +
    2.14  * Reorganization of number theory:
    2.15    * former session NumberTheory now named Old_Number_Theory
    2.16    * new session Number_Theory by Jeremy Avigad; if possible, prefer this.
     3.1 --- a/etc/components	Fri Sep 18 14:40:24 2009 +0200
     3.2 +++ b/etc/components	Fri Sep 18 18:13:19 2009 +0200
     3.3 @@ -15,3 +15,4 @@
     3.4  src/HOL/Tools/ATP_Manager
     3.5  src/HOL/Mirabelle
     3.6  src/HOL/Library/Sum_Of_Squares
     3.7 +src/HOL/SMT
     4.1 --- a/src/HOL/IsaMakefile	Fri Sep 18 14:40:24 2009 +0200
     4.2 +++ b/src/HOL/IsaMakefile	Fri Sep 18 18:13:19 2009 +0200
     4.3 @@ -40,6 +40,7 @@
     4.4    HOL-Prolog \
     4.5    HOL-SET-Protocol \
     4.6    HOL-SizeChange \
     4.7 +  HOL-SMT \
     4.8    HOL-Statespace \
     4.9    HOL-Subst \
    4.10        TLA-Buffer \
    4.11 @@ -1134,6 +1135,19 @@
    4.12  	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Mirabelle
    4.13  
    4.14  
    4.15 +## HOL-SMT
    4.16 +
    4.17 +HOL-SMT: HOL-Word $(LOG)/HOL-SMT.gz
    4.18 +
    4.19 +$(LOG)/HOL-SMT.gz: $(OUT)/HOL-Word SMT/SMT_Definitions.thy SMT/SMT.thy \
    4.20 +  SMT/Tools/smt_normalize.ML SMT/Tools/smt_monomorph.ML \
    4.21 +  SMT/Tools/smt_translate.ML SMT/Tools/smt_builtin.ML \
    4.22 +  SMT/Tools/smtlib_interface.ML SMT/Tools/smt_solver.ML \
    4.23 +  SMT/Tools/cvc3_solver.ML SMT/Tools/yices_solver.ML \
    4.24 +  SMT/Tools/z3_interface.ML SMT/Tools/z3_solver.ML SMT/Tools/z3_model.ML
    4.25 +	@cd SMT; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-Word HOL-SMT
    4.26 +
    4.27 +
    4.28  ## clean
    4.29  
    4.30  clean:
    4.31 @@ -1156,4 +1170,4 @@
    4.32  		$(LOG)/HOL-Unix.gz $(OUT)/HOL-Word $(LOG)/HOL-Word.gz	\
    4.33  		$(LOG)/HOL-Word-Examples.gz $(OUT)/HOL-NSA		\
    4.34  		$(LOG)/HOL-NSA.gz $(LOG)/HOL-NSA-Examples.gz            \
    4.35 -                $(LOG)/HOL-Mirabelle.gz
    4.36 +                $(LOG)/HOL-Mirabelle.gz $(LOG)/HOL-SMT.gz
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/SMT/Examples/SMT_Examples.thy	Fri Sep 18 18:13:19 2009 +0200
     5.3 @@ -0,0 +1,182 @@
     5.4 +(*  Title:       SMT_Examples.thy
     5.5 +    Author:      Sascha Böhme, TU Muenchen
     5.6 +*)
     5.7 +
     5.8 +header {* Examples for the 'smt' tactic. *}
     5.9 +
    5.10 +theory SMT_Examples
    5.11 +imports "../SMT"
    5.12 +begin
    5.13 +
    5.14 +declare [[smt_solver=z3, z3_proofs=false]]
    5.15 +declare [[smt_trace=true]] (*FIXME*)
    5.16 +
    5.17 +
    5.18 +section {* Propositional and first-order logic *}
    5.19 +
    5.20 +lemma "True" by smt
    5.21 +lemma "p \<or> \<not>p" by smt
    5.22 +lemma "(p \<and> True) = p" by smt
    5.23 +lemma "(p \<or> q) \<and> \<not>p \<Longrightarrow> q" by smt
    5.24 +lemma "(a \<and> b) \<or> (c \<and> d) \<Longrightarrow> (a \<and> b) \<or> (c \<and> d)" by smt
    5.25 +lemma "P=P=P=P=P=P=P=P=P=P" by smt
    5.26 +
    5.27 +axiomatization symm_f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
    5.28 +  symm_f: "symm_f x y = symm_f y x"
    5.29 +lemma "a = a \<and> symm_f a b = symm_f b a" by (smt add: symm_f)
    5.30 +
    5.31 +
    5.32 +section {* Linear arithmetic *}
    5.33 +
    5.34 +lemma "(3::int) = 3" by smt
    5.35 +lemma "(3::real) = 3" by smt
    5.36 +lemma "(3 :: int) + 1 = 4" by smt
    5.37 +lemma "max (3::int) 8 > 5" by smt
    5.38 +lemma "abs (x :: real) + abs y \<ge> abs (x + y)" by smt
    5.39 +lemma "let x = (2 :: int) in x + x \<noteq> 5" by smt
    5.40 +
    5.41 +text{* 
    5.42 +The following example was taken from HOL/ex/PresburgerEx.thy, where it says:
    5.43 +
    5.44 +  This following theorem proves that all solutions to the
    5.45 +  recurrence relation $x_{i+2} = |x_{i+1}| - x_i$ are periodic with
    5.46 +  period 9.  The example was brought to our attention by John
    5.47 +  Harrison. It does does not require Presburger arithmetic but merely
    5.48 +  quantifier-free linear arithmetic and holds for the rationals as well.
    5.49 +
    5.50 +  Warning: it takes (in 2006) over 4.2 minutes! 
    5.51 +
    5.52 +There, it is proved by "arith". SMT is able to prove this within a fraction
    5.53 +of one second.
    5.54 +*}
    5.55 +
    5.56 +lemma "\<lbrakk> x3 = abs x2 - x1; x4 = abs x3 - x2; x5 = abs x4 - x3;
    5.57 +         x6 = abs x5 - x4; x7 = abs x6 - x5; x8 = abs x7 - x6;
    5.58 +         x9 = abs x8 - x7; x10 = abs x9 - x8; x11 = abs x10 - x9 \<rbrakk>
    5.59 + \<Longrightarrow> x1 = x10 & x2 = (x11::int)"
    5.60 +  by smt
    5.61 +
    5.62 +lemma "\<exists>x::int. 0 < x" by smt
    5.63 +lemma "\<exists>x::real. 0 < x" by smt
    5.64 +lemma "\<forall>x y::int. x < y \<longrightarrow> (2 * x + 1) < (2 * y)" by smt
    5.65 +lemma "\<forall>x y::int. (2 * x + 1) \<noteq> (2 * y)" by smt
    5.66 +lemma "~ (\<exists>x y z::int. 4 * x + -6 * y = (1::int))" by smt
    5.67 +lemma "~ (\<exists>x::int. False)" by smt
    5.68 +
    5.69 +
    5.70 +section {* Non-linear arithmetic *}
    5.71 +
    5.72 +lemma "((x::int) * (1 + y) - x * (1 - y)) = (2 * x * y)" by smt
    5.73 +lemma
    5.74 +  "(U::int) + (1 + p) * (b + e) + p * d =
    5.75 +   U + (2 * (1 + p) * (b + e) + (1 + p) * d + d * p) - (1 + p) * (b + d + e)"
    5.76 +  by smt
    5.77 +
    5.78 +
    5.79 +section {* Linear arithmetic for natural numbers *}
    5.80 +
    5.81 +lemma "a < 3 \<Longrightarrow> (7::nat) > 2 * a" by smt
    5.82 +lemma "let x = (1::nat) + y in x - y > 0 * x" by smt
    5.83 +lemma
    5.84 +  "let x = (1::nat) + y in
    5.85 +   let P = (if x > 0 then True else False) in
    5.86 +   False \<or> P = (x - 1 = y) \<or> (\<not>P \<longrightarrow> False)"
    5.87 +  by smt
    5.88 +
    5.89 +
    5.90 +section {* Bitvectors *}
    5.91 +
    5.92 +locale bv
    5.93 +begin
    5.94 +
    5.95 +declare [[smt_solver=z3]]
    5.96 +
    5.97 +lemma "(27 :: 4 word) = -5" by smt
    5.98 +lemma "(27 :: 4 word) = 11" by smt
    5.99 +lemma "23 < (27::8 word)" by smt
   5.100 +lemma "27 + 11 = (6::5 word)" by smt
   5.101 +lemma "7 * 3 = (21::8 word)" by smt
   5.102 +lemma "11 - 27 = (-16::8 word)" by smt
   5.103 +lemma "- -11 = (11::5 word)" by smt
   5.104 +lemma "-40 + 1 = (-39::7 word)" by smt
   5.105 +lemma "a + 2 * b + c - b = (b + c) + (a :: 32 word)" by smt
   5.106 +
   5.107 +lemma "0b110 AND 0b101 = (0b100 :: 32 word)" by smt
   5.108 +lemma "0b110 OR 0b011 = (0b111 :: 8 word)" by smt
   5.109 +lemma "0xF0 XOR 0xFF = (0x0F :: 8 word)" by smt
   5.110 +lemma "NOT (0xF0 :: 16 word) = 0xFF0F" by smt
   5.111 +
   5.112 +lemma "word_cat (27::4 word) (27::8 word) = (2843::12 word)" by smt
   5.113 +lemma "word_cat (0b0011::4 word) (0b1111::6word) = (0b0011001111 :: 10 word)" 
   5.114 +  by smt
   5.115 +
   5.116 +lemma "slice 1 (0b10110 :: 4 word) = (0b11 :: 2 word)" by smt
   5.117 +
   5.118 +lemma "ucast (0b1010 :: 4 word) = (0b1010 :: 10 word)" by smt
   5.119 +lemma "scast (0b1010 :: 4 word) = (0b111010 :: 6 word)" by smt
   5.120 +
   5.121 +lemma "bv_lshr 0b10011 2 = (0b100::8 word)" by smt
   5.122 +lemma "bv_ashr 0b10011 2 = (0b100::8 word)" by smt
   5.123 +
   5.124 +lemma "word_rotr 2 0b0110 = (0b1001::4 word)" by smt
   5.125 +lemma "word_rotl 1 0b1110 = (0b1101::4 word)" by smt
   5.126 +
   5.127 +lemma "(x AND 0xff00) OR (x AND 0x00ff) = (x::16 word)" by smt
   5.128 +
   5.129 +lemma "w < 256 \<Longrightarrow> (w :: 16 word) AND 0x00FF = w" by smt
   5.130 +
   5.131 +end
   5.132 +
   5.133 +
   5.134 +section {* Pairs *}
   5.135 +
   5.136 +lemma "fst (x, y) = a \<Longrightarrow> x = a" by smt
   5.137 +lemma "p1 = (x, y) \<and> p2 = (y, x) \<Longrightarrow> fst p1 = snd p2" by smt
   5.138 +
   5.139 +
   5.140 +section {* Higher-order problems and recursion *}
   5.141 +
   5.142 +lemma "(f g x = (g x \<and> True)) \<or> (f g x = True) \<or> (g x = True)" by smt
   5.143 +lemma "P ((2::int) < 3) = P True" by smt
   5.144 +lemma "P ((2::int) < 3) = (P True :: bool)" by smt
   5.145 +lemma "P (0 \<le> (a :: 4 word)) = P True" using [[smt_solver=z3]] by smt
   5.146 +lemma "id 3 = 3 \<and> id True = True" by (smt add: id_def)
   5.147 +lemma "i \<noteq> i1 \<and> i \<noteq> i2 \<Longrightarrow> ((f (i1 := v1)) (i2 := v2)) i = f i" by smt
   5.148 +lemma "map (\<lambda>i::nat. i + 1) [0, 1] = [1, 2]" by (smt add: map.simps)
   5.149 +lemma "(ALL x. P x) | ~ All P" by smt
   5.150 +
   5.151 +fun dec_10 :: "nat \<Rightarrow> nat" where
   5.152 +  "dec_10 n = (if n < 10 then n else dec_10 (n - 10))"
   5.153 +lemma "dec_10 (4 * dec_10 4) = 6" by (smt add: dec_10.simps)
   5.154 +
   5.155 +axiomatization
   5.156 +  eval_dioph :: "int list \<Rightarrow> nat list \<Rightarrow> int"
   5.157 +  where
   5.158 +  eval_dioph_mod:
   5.159 +  "eval_dioph ks xs mod int n = eval_dioph ks (map (\<lambda>x. x mod n) xs) mod int n"
   5.160 +  and
   5.161 +  eval_dioph_div_mult:
   5.162 +  "eval_dioph ks (map (\<lambda>x. x div n) xs) * int n +
   5.163 +   eval_dioph ks (map (\<lambda>x. x mod n) xs) = eval_dioph ks xs"
   5.164 +lemma
   5.165 +  "(eval_dioph ks xs = l) =
   5.166 +   (eval_dioph ks (map (\<lambda>x. x mod 2) xs) mod 2 = l mod 2 \<and>
   5.167 +    eval_dioph ks (map (\<lambda>x. x div 2) xs) =
   5.168 +      (l - eval_dioph ks (map (\<lambda>x. x mod 2) xs)) div 2)"
   5.169 +  by (smt add: eval_dioph_mod[where n=2] eval_dioph_div_mult[where n=2])
   5.170 +
   5.171 +
   5.172 +section {* Monomorphization examples *}
   5.173 +
   5.174 +definition P :: "'a \<Rightarrow> bool" where "P x = True"
   5.175 +lemma poly_P: "P x \<and> (P [x] \<or> \<not>P[x])" by (simp add: P_def)
   5.176 +lemma "P (1::int)" by (smt add: poly_P)
   5.177 +
   5.178 +consts g :: "'a \<Rightarrow> nat"
   5.179 +axioms
   5.180 +  g1: "g (Some x) = g [x]"
   5.181 +  g2: "g None = g []"
   5.182 +  g3: "g xs = length xs"
   5.183 +lemma "g (Some (3::int)) = g (Some True)" by (smt add: g1 g2 g3 list.size)
   5.184 +
   5.185 +end
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/SMT/IsaMakefile	Fri Sep 18 18:13:19 2009 +0200
     6.3 @@ -0,0 +1,39 @@
     6.4 +
     6.5 +## targets
     6.6 +
     6.7 +default: HOL-SMT
     6.8 +images: HOL-SMT
     6.9 +test: 
    6.10 +
    6.11 +all: images test
    6.12 +
    6.13 +
    6.14 +## global settings
    6.15 +
    6.16 +SRC = $(ISABELLE_HOME)/src
    6.17 +OUT = $(ISABELLE_OUTPUT)
    6.18 +LOG = $(OUT)/log
    6.19 +
    6.20 +USEDIR = $(ISATOOL) usedir -v true 
    6.21 +
    6.22 +
    6.23 +## HOL-SMT
    6.24 +
    6.25 +HOL-SMT: $(OUT)/HOL-SMT
    6.26 +
    6.27 +$(OUT)/HOL-SMT: $(OUT)/HOL-Word ROOT.ML SMT_Definitions.thy SMT.thy \
    6.28 +  Tools/cancel_conj_disj.ML Tools/smt_normalize.ML Tools/smt_monomorph.ML \
    6.29 +  Tools/smt_translate.ML Tools/smt_builtin.ML Tools/smtlib_interface.ML \
    6.30 +  Tools/smt_solver.ML Tools/cvc3_solver.ML Tools/yices_solver.ML \
    6.31 +  Tools/z3_interface.ML Tools/z3_solver.ML Tools/z3_model.ML \
    6.32 +  Tools/z3_proof.ML Tools/z3_proof_rules.ML Tools/z3_proof_terms.ML
    6.33 +	@$(USEDIR) -b HOL-Word HOL-SMT
    6.34 +
    6.35 +$(OUT)/HOL-Word:
    6.36 +	@$(ISATOOL) make HOL-Word -C $(SRC)/HOL
    6.37 +
    6.38 +
    6.39 +## clean
    6.40 +
    6.41 +clean:
    6.42 +	@rm -f $(OUT)/HOL-SMT
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/SMT/ROOT.ML	Fri Sep 18 18:13:19 2009 +0200
     7.3 @@ -0,0 +1,1 @@
     7.4 +use_thy "SMT";
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/SMT/SMT.thy	Fri Sep 18 18:13:19 2009 +0200
     8.3 @@ -0,0 +1,51 @@
     8.4 +(*  Title:      HOL/SMT/SMT.thy
     8.5 +    Author:     Sascha Boehme, TU Muenchen
     8.6 +*)
     8.7 +
     8.8 +header {* SMT method using external SMT solvers (CVC3, Yices, Z3) *}
     8.9 +
    8.10 +theory SMT
    8.11 +imports SMT_Definitions
    8.12 +uses
    8.13 +  "Tools/smt_normalize.ML"
    8.14 +  "Tools/smt_monomorph.ML"
    8.15 +  "Tools/smt_translate.ML"
    8.16 +  "Tools/smt_solver.ML"
    8.17 +  "Tools/smtlib_interface.ML"
    8.18 +  "Tools/cvc3_solver.ML"
    8.19 +  "Tools/yices_solver.ML"
    8.20 +  "Tools/z3_model.ML"
    8.21 +  "Tools/z3_interface.ML"
    8.22 +  "Tools/z3_solver.ML"
    8.23 +begin
    8.24 +
    8.25 +setup {*
    8.26 +  SMT_Normalize.setup #>
    8.27 +  SMT_Solver.setup #>
    8.28 +  CVC3_Solver.setup #>
    8.29 +  Yices_Solver.setup #>
    8.30 +  Z3_Solver.setup
    8.31 +*}
    8.32 +
    8.33 +ML {*
    8.34 +OuterSyntax.improper_command "smt_status"
    8.35 +  "Show the available SMT solvers and the currently selected solver."
    8.36 +  OuterKeyword.diag
    8.37 +    (Scan.succeed (Toplevel.no_timing o Toplevel.keep (fn state =>
    8.38 +      SMT_Solver.print_setup (Context.Proof (Toplevel.context_of state)))))
    8.39 +*}
    8.40 +
    8.41 +method_setup smt = {*
    8.42 +  let fun solver thms ctxt = SMT_Solver.smt_tac ctxt thms
    8.43 +  in
    8.44 +    Scan.optional (Scan.lift (Args.add -- Args.colon) |-- Attrib.thms) [] >>
    8.45 +    (Method.SIMPLE_METHOD' oo solver)
    8.46 +  end
    8.47 +*} "Applies an SMT solver to the current goal."
    8.48 +
    8.49 +declare [[ smt_solver = z3, smt_timeout = 20, smt_trace = false ]]
    8.50 +declare [[ smt_unfold_defs = true ]]
    8.51 +declare [[ z3_proofs = false ]]
    8.52 +
    8.53 +end
    8.54 +
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/SMT/SMT_Definitions.thy	Fri Sep 18 18:13:19 2009 +0200
     9.3 @@ -0,0 +1,113 @@
     9.4 +(*  Title:      HOL/SMT/SMT_Definitions.thy
     9.5 +    Author:     Sascha Boehme, TU Muenchen
     9.6 +*)
     9.7 +
     9.8 +header {* SMT-specific definitions *}
     9.9 +
    9.10 +theory SMT_Definitions
    9.11 +imports Real Word "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
    9.12 +begin
    9.13 +
    9.14 +section {* Triggers for quantifier instantiation *}
    9.15 +
    9.16 +text {*
    9.17 +Some SMT solvers support triggers for quantifier instantiation. Each trigger
    9.18 +consists of one ore more patterns. A pattern may either be a list of positive
    9.19 +subterms (the first being tagged by "pat" and the consecutive subterms tagged
    9.20 +by "andpat"), or a list of negative subterms (the first being tagged by "nopat"
    9.21 +and the consecutive subterms tagged by "andpat").
    9.22 +*}
    9.23 +
    9.24 +datatype pattern = Pattern
    9.25 +
    9.26 +definition pat :: "'a \<Rightarrow> pattern"
    9.27 +where "pat _ = Pattern"
    9.28 +
    9.29 +definition nopat :: "bool \<Rightarrow> pattern"
    9.30 +where "nopat _ = Pattern"
    9.31 +
    9.32 +definition andpat :: "pattern \<Rightarrow> 'a \<Rightarrow> pattern" (infixl "andpat" 60)
    9.33 +where "_ andpat _ = Pattern"
    9.34 +
    9.35 +definition trigger :: "pattern list \<Rightarrow> bool \<Rightarrow> bool"
    9.36 +where "trigger _ P = P"
    9.37 +
    9.38 +
    9.39 +section {* Arithmetic *}
    9.40 +
    9.41 +text {*
    9.42 +The sign of @{term "op mod :: int \<Rightarrow> int \<Rightarrow> int"} follows the sign of the
    9.43 +divisor. In contrast to that, the sign of the following operation is that of
    9.44 +the dividend.
    9.45 +*}
    9.46 +
    9.47 +definition rem :: "int \<Rightarrow> int \<Rightarrow> int" (infixl "rem" 70)
    9.48 +where "a rem b = 
    9.49 +  (if (a \<ge> 0 \<and> b < 0) \<or> (a < 0 \<and> b \<ge> 0) then - (a mod b) else a mod b)"
    9.50 +
    9.51 +text {* A decision procedure for linear real arithmetic: *}
    9.52 +
    9.53 +setup {*
    9.54 +  Arith_Data.add_tactic "Ferrante-Rackoff" (K FerranteRackoff.dlo_tac)
    9.55 +*}
    9.56 +
    9.57 +
    9.58 +section {* Bitvectors *}
    9.59 +
    9.60 +text {*
    9.61 +The following definitions provide additional functions not found in HOL-Word.
    9.62 +*}
    9.63 +
    9.64 +definition sdiv :: "'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a word" (infix "sdiv" 70)
    9.65 +where "w1 sdiv w2 = word_of_int (sint w1 div sint w2)"
    9.66 +
    9.67 +definition smod :: "'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a word" (infix "smod" 70)
    9.68 +  (* sign follows divisor *)
    9.69 +where "w1 smod w2 = word_of_int (sint w1 mod sint w2)"
    9.70 +
    9.71 +definition srem :: "'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a word" (infix "srem" 70)
    9.72 +  (* sign follows dividend *)
    9.73 +where "w1 srem w2 = word_of_int (sint w1 rem sint w2)"
    9.74 +
    9.75 +definition bv_shl :: "'a::len0 word \<Rightarrow> 'a word \<Rightarrow> 'a word"
    9.76 +where "bv_shl w1 w2 = (w1 << unat w2)"
    9.77 +
    9.78 +definition bv_lshr :: "'a::len0 word \<Rightarrow> 'a word \<Rightarrow> 'a word"
    9.79 +where "bv_lshr w1 w2 = (w1 >> unat w2)"
    9.80 +
    9.81 +definition bv_ashr :: "'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a word"
    9.82 +where "bv_ashr w1 w2 = (w1 >>> unat w2)"
    9.83 +
    9.84 +
    9.85 +section {* Higher-order encoding *}
    9.86 +
    9.87 +definition "apply" where "apply f x = f x"
    9.88 +
    9.89 +
    9.90 +section {* First-order logic *}
    9.91 +
    9.92 +text {*
    9.93 +Some SMT solver formats require a strict separation between formulas and terms.
    9.94 +The following marker symbols are used internally to separate those categories:
    9.95 +*}
    9.96 +
    9.97 +definition formula :: "bool \<Rightarrow> bool" where "formula x = x"
    9.98 +definition "term" where "term x = x"
    9.99 +
   9.100 +text {*
   9.101 +Predicate symbols also occurring as function symbols are turned into function
   9.102 +symbols by translating atomic formulas into terms:
   9.103 +*}
   9.104 +
   9.105 +abbreviation holds :: "bool \<Rightarrow> bool" where "holds \<equiv> (\<lambda>P. term P = term True)"
   9.106 +
   9.107 +text {*
   9.108 +The following constant represents equivalence, to be treated differently than
   9.109 +the (polymorphic) equality predicate:
   9.110 +*}
   9.111 +
   9.112 +definition iff :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infix "iff" 50) where
   9.113 +  "(x iff y) = (x = y)"
   9.114 +
   9.115 +end
   9.116 +
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/HOL/SMT/Tools/cvc3_solver.ML	Fri Sep 18 18:13:19 2009 +0200
    10.3 @@ -0,0 +1,59 @@
    10.4 +(*  Title:      HOL/SMT/Tools/cvc3_solver.ML
    10.5 +    Author:     Sascha Boehme, TU Muenchen
    10.6 +
    10.7 +Interface of the SMT solver CVC3.
    10.8 +*)
    10.9 +
   10.10 +signature CVC3_SOLVER =
   10.11 +sig
   10.12 +  val setup: theory -> theory
   10.13 +end
   10.14 +
   10.15 +structure CVC3_Solver: CVC3_SOLVER =
   10.16 +struct
   10.17 +
   10.18 +val solver_name = "cvc3"
   10.19 +val env_var = "CVC3_SOLVER"
   10.20 +
   10.21 +val options =
   10.22 +  ["+counterexample", "-lang", "smtlib", "-output-lang", "presentation"]
   10.23 +
   10.24 +val is_sat = String.isPrefix "Satisfiable."
   10.25 +val is_unsat = String.isPrefix "Unsatisfiable."
   10.26 +val is_unknown = String.isPrefix "Unknown."
   10.27 +
   10.28 +fun cex_kind true = "Counterexample"
   10.29 +  | cex_kind false = "Possible counterexample"
   10.30 +
   10.31 +fun raise_cex real ctxt recon ls =
   10.32 +  let
   10.33 +    val start = String.isPrefix "%Satisfiable  Variable Assignment: %"
   10.34 +    val index = find_index start ls
   10.35 +    val ls = if index > 0 then Library.drop (index + 1, ls) else []
   10.36 +    val p = Pretty.big_list (cex_kind real ^ " found:") (map Pretty.str ls)
   10.37 +  in error (Pretty.string_of p) end
   10.38 +
   10.39 +fun core_oracle (SMT_Solver.ProofData {context, output, recon, ...}) =
   10.40 +  let
   10.41 +    val empty_line = (fn "" => true | _ => false)
   10.42 +    val split_first = (fn [] => ("", []) | l :: ls => (l, ls))
   10.43 +    val (l, ls) = split_first (dropwhile empty_line output)
   10.44 +  in
   10.45 +    if is_unsat l then @{cprop False}
   10.46 +    else if is_sat l then raise_cex true context recon ls
   10.47 +    else if is_unknown l then raise_cex false context recon ls
   10.48 +    else error (solver_name ^ " failed")
   10.49 +  end
   10.50 +
   10.51 +fun smtlib_solver oracle _ =
   10.52 +  SMT_Solver.SolverConfig {
   10.53 +    name = {env_var=env_var, remote_name=solver_name},
   10.54 +    interface = SMTLIB_Interface.interface,
   10.55 +    arguments = options,
   10.56 +    reconstruct = oracle }
   10.57 +
   10.58 +val setup =
   10.59 +  Thm.add_oracle (Binding.name solver_name, core_oracle) #-> (fn (_, oracle) =>
   10.60 +  SMT_Solver.add_solver (solver_name, smtlib_solver oracle))
   10.61 +
   10.62 +end
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/HOL/SMT/Tools/smt_builtin.ML	Fri Sep 18 18:13:19 2009 +0200
    11.3 @@ -0,0 +1,78 @@
    11.4 +(*  Title:      HOL/SMT/Tools/smt_builtin.ML
    11.5 +    Author:     Sascha Boehme, TU Muenchen
    11.6 +
    11.7 +Tables for built-in symbols.
    11.8 +*)
    11.9 +
   11.10 +signature SMT_BUILTIN =
   11.11 +sig
   11.12 +  type sterm = (SMT_Translate.sym, typ) sterm
   11.13 +  type builtin_fun = typ -> sterm list -> (string * sterm list) option
   11.14 +  type table = (typ * builtin_fun) list Symtab.table
   11.15 +
   11.16 +  val make: (term * string) list -> table
   11.17 +  val add: term * builtin_fun -> table -> table
   11.18 +  val lookup: table -> theory -> string * typ -> sterm list ->
   11.19 +    (string * sterm list) option
   11.20 +
   11.21 +  val bv_rotate: (int -> string) -> builtin_fun
   11.22 +  val bv_extend: (int -> string) -> builtin_fun
   11.23 +  val bv_extract: (int -> int -> string) -> builtin_fun
   11.24 +end
   11.25 +
   11.26 +structure SMT_Builtin: SMT_BUILTIN =
   11.27 +struct
   11.28 +
   11.29 +structure T = SMT_Translate
   11.30 +
   11.31 +type sterm = (SMT_Translate.sym, typ) sterm
   11.32 +type builtin_fun = typ -> sterm list -> (string * sterm list) option
   11.33 +type table = (typ * builtin_fun) list Symtab.table
   11.34 +
   11.35 +fun make entries =
   11.36 +  let
   11.37 +    fun dest (t, bn) =
   11.38 +      let val (n, T) = Term.dest_Const t
   11.39 +      in (n, (Logic.varifyT T, K (pair bn))) end
   11.40 +  in Symtab.make (AList.group (op =) (map dest entries)) end
   11.41 +
   11.42 +fun add (t, f) tab =
   11.43 +  let val (n, T) = apsnd Logic.varifyT (Term.dest_Const t)
   11.44 +  in Symtab.map_default (n, []) (AList.update (op =) (T, f)) tab end
   11.45 +
   11.46 +fun lookup tab thy (n, T) =
   11.47 +  AList.lookup (Sign.typ_instance thy) (Symtab.lookup_list tab n) T T
   11.48 +
   11.49 +
   11.50 +fun dest_binT T =
   11.51 +  (case T of
   11.52 +    Type (@{type_name "Numeral_Type.num0"}, _) => 0
   11.53 +  | Type (@{type_name "Numeral_Type.num1"}, _) => 1
   11.54 +  | Type (@{type_name "Numeral_Type.bit0"}, [T]) => 2 * dest_binT T
   11.55 +  | Type (@{type_name "Numeral_Type.bit1"}, [T]) => 1 + 2 * dest_binT T
   11.56 +  | _ => raise TYPE ("dest_binT", [T], []))
   11.57 +
   11.58 +fun dest_wordT T =
   11.59 +  (case T of
   11.60 +    Type (@{type_name "word"}, [T]) => dest_binT T
   11.61 +  | _ => raise TYPE ("dest_wordT", [T], []))
   11.62 +
   11.63 +
   11.64 +val dest_nat = (fn
   11.65 +    SApp (SConst (@{const_name nat}, _), [SApp (SNum (i, _), _)]) => SOME i
   11.66 +  | _ => NONE)
   11.67 +
   11.68 +fun bv_rotate mk_name T ts =
   11.69 +  dest_nat (hd ts) |> Option.map (fn i => (mk_name i, tl ts))
   11.70 +
   11.71 +fun bv_extend mk_name T ts =
   11.72 +  (case (try dest_wordT (domain_type T), try dest_wordT (range_type T)) of
   11.73 +    (SOME i, SOME j) => if j - i >= 0 then SOME (mk_name (j - i), ts) else NONE
   11.74 +  | _ => NONE)
   11.75 +
   11.76 +fun bv_extract mk_name T ts =
   11.77 +  (case (try dest_wordT (body_type T), dest_nat (hd ts)) of
   11.78 +    (SOME i, SOME lb) => SOME (mk_name (i + lb - 1) lb, tl ts)
   11.79 +  | _ => NONE)
   11.80 +
   11.81 +end
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/HOL/SMT/Tools/smt_monomorph.ML	Fri Sep 18 18:13:19 2009 +0200
    12.3 @@ -0,0 +1,120 @@
    12.4 +(*  Title:      HOL/SMT/Tools/smt_monomorph.ML
    12.5 +    Author:     Sascha Boehme, TU Muenchen
    12.6 +
    12.7 +Monomorphization of terms, i.e., computation of all (necessary) instances.
    12.8 +*)
    12.9 +
   12.10 +signature SMT_MONOMORPH =
   12.11 +sig
   12.12 +  val monomorph: theory -> term list -> term list
   12.13 +end
   12.14 +
   12.15 +structure SMT_Monomorph: SMT_MONOMORPH =
   12.16 +struct
   12.17 +
   12.18 +fun selection [] = []
   12.19 +  | selection (x :: xs) = (x, xs) :: map (apsnd (cons x)) (selection xs)
   12.20 +
   12.21 +fun permute [] = []
   12.22 +  | permute [x] = [[x]]
   12.23 +  | permute xs = maps (fn (y, ys) => map (cons y) (permute ys)) (selection xs)
   12.24 +
   12.25 +fun fold_all f = fold (fn x => maps (f x))
   12.26 +
   12.27 +
   12.28 +val typ_has_tvars = Term.exists_subtype (fn TVar _ => true | _ => false)
   12.29 +val term_has_tvars = Term.exists_type typ_has_tvars
   12.30 +
   12.31 +val ignored = member (op =) [
   12.32 +  @{const_name All}, @{const_name Ex}, @{const_name Let}, @{const_name If},
   12.33 +  @{const_name "op ="}, @{const_name zero_class.zero},
   12.34 +  @{const_name one_class.one}, @{const_name number_of}]
   12.35 +fun consts_of ts = AList.group (op =) (fold Term.add_consts ts [])
   12.36 +  |> filter_out (ignored o fst)
   12.37 +
   12.38 +val join_consts = curry (AList.join (op =) (K (merge (op =))))
   12.39 +fun diff_consts cs ds = 
   12.40 +  let fun diff (n, Ts) =
   12.41 +    (case AList.lookup (op =) cs n of
   12.42 +      NONE => SOME (n, Ts)
   12.43 +    | SOME Us =>
   12.44 +        let val Ts' = fold (remove (op =)) Us Ts
   12.45 +        in if null Ts' then NONE else SOME (n, Ts') end)
   12.46 +  in map_filter diff ds end
   12.47 +
   12.48 +fun instances thy is (n, Ts) env =
   12.49 +  let
   12.50 +    val Us = these (AList.lookup (op =) is n)
   12.51 +    val Ts' = filter typ_has_tvars (map (Envir.subst_type env) Ts)
   12.52 +  in
   12.53 +    (case map_product pair Ts' Us of
   12.54 +      [] => [env]
   12.55 +    | TUs => map_filter (try (fn TU => Sign.typ_match thy TU env)) TUs)
   12.56 +  end
   12.57 +
   12.58 +fun proper_match ps env =
   12.59 +  forall (forall (not o typ_has_tvars o Envir.subst_type env) o snd) ps
   12.60 +
   12.61 +val eq_tab = gen_eq_set (op =) o pairself Vartab.dest
   12.62 +
   12.63 +fun specialize thy cs is ((r, ps), ces) (ts, ns) =
   12.64 +  let
   12.65 +    val ps' = filter (AList.defined (op =) is o fst) ps
   12.66 +
   12.67 +    val envs = permute ps'
   12.68 +      |> maps (fn ps => fold_all (instances thy is) ps [Vartab.empty])
   12.69 +      |> filter (proper_match ps')
   12.70 +      |> filter_out (member eq_tab ces)
   12.71 +      |> distinct eq_tab
   12.72 +
   12.73 +    val us = map (fn env => Envir.subst_term_types env r) envs
   12.74 +    val ns' = join_consts (diff_consts is (diff_consts cs (consts_of us))) ns
   12.75 +  in (envs @ ces, (fold (insert (op aconv)) us ts, ns')) end
   12.76 +
   12.77 +
   12.78 +fun incr_tvar_indices i t =
   12.79 +  let
   12.80 +    val incrT = Logic.incr_tvar i
   12.81 +
   12.82 +    fun incr t =
   12.83 +      (case t of
   12.84 +        Const (n, T) => Const (n, incrT T)
   12.85 +      | Free (n, T) => Free (n, incrT T)
   12.86 +      | Abs (n, T, t1) => Abs (n, incrT T, incr t1)
   12.87 +      | t1 $ t2 => incr t1 $ incr t2
   12.88 +      | _ => t)
   12.89 +  in incr t end
   12.90 +
   12.91 +
   12.92 +val monomorph_limit = 10
   12.93 +
   12.94 +(* Instantiate all polymorphic constants (i.e., constants occurring both with
   12.95 +   ground types and type variables) with all (necessary) ground types; thereby
   12.96 +   create copies of terms containing those constants.
   12.97 +   To prevent non-termination, there is an upper limit for the number of
   12.98 +   recursions involved in the fixpoint construction. *)
   12.99 +fun monomorph thy ts =
  12.100 +  let
  12.101 +    val (ps, ms) = List.partition term_has_tvars ts
  12.102 +
  12.103 +    fun with_tvar (n, Ts) =
  12.104 +      let val Ts' = filter typ_has_tvars Ts
  12.105 +      in if null Ts' then NONE else SOME (n, Ts') end
  12.106 +    fun incr t idx = (incr_tvar_indices idx t, idx + Term.maxidx_of_term t + 1)
  12.107 +    val rps = fst (fold_map incr ps 0)
  12.108 +      |> map (fn r => (r, map_filter with_tvar (consts_of [r])))
  12.109 +
  12.110 +    fun mono count is ces cs ts =
  12.111 +      let
  12.112 +        val spec = specialize thy cs is
  12.113 +        val (ces', (ts', is')) = fold_map spec (rps ~~ ces) (ts, [])
  12.114 +        val cs' = join_consts is cs
  12.115 +      in
  12.116 +        if null is' then ts'
  12.117 +        else if count > monomorph_limit then
  12.118 +          (Output.warning "monomorphization limit reached"; ts')
  12.119 +        else mono (count + 1) is' ces' cs' ts'
  12.120 +      end
  12.121 +  in mono 0 (consts_of ms) (map (K []) rps) [] ms end
  12.122 +
  12.123 +end
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/src/HOL/SMT/Tools/smt_normalize.ML	Fri Sep 18 18:13:19 2009 +0200
    13.3 @@ -0,0 +1,408 @@
    13.4 +(*  Title:      HOL/SMT/Tools/smt_normalize.ML
    13.5 +    Author:     Sascha Boehme, TU Muenchen
    13.6 +
    13.7 +Normalization steps on theorems required by SMT solvers:
    13.8 +  * unfold trivial let expressions,
    13.9 +  * replace negative numerals by negated positive numerals,
   13.10 +  * embed natural numbers into integers,
   13.11 +  * add extra rules specifying types and constants which occur frequently,
   13.12 +  * lift lambda terms,
   13.13 +  * make applications explicit for functions with varying number of arguments,
   13.14 +  * fully translate into object logic, add universal closure. 
   13.15 +*)
   13.16 +
   13.17 +signature SMT_NORMALIZE =
   13.18 +sig
   13.19 +  val normalize_rule: Proof.context -> thm -> thm
   13.20 +  val instantiate_free: Thm.cterm * Thm.cterm -> thm -> thm
   13.21 +  val discharge_definition: Thm.cterm -> thm -> thm
   13.22 +
   13.23 +  val trivial_let: Proof.context -> thm list -> thm list
   13.24 +  val positive_numerals: Proof.context -> thm list -> thm list
   13.25 +  val nat_as_int: Proof.context -> thm list -> thm list
   13.26 +  val unfold_defs: bool Config.T
   13.27 +  val add_pair_rules: Proof.context -> thm list -> thm list
   13.28 +  val add_fun_upd_rules: Proof.context -> thm list -> thm list
   13.29 +  val add_abs_min_max_rules: Proof.context -> thm list -> thm list
   13.30 +
   13.31 +  datatype config =
   13.32 +    RewriteTrivialLets |
   13.33 +    RewriteNegativeNumerals |
   13.34 +    RewriteNaturalNumbers |
   13.35 +    AddPairRules |
   13.36 +    AddFunUpdRules |
   13.37 +    AddAbsMinMaxRules
   13.38 +
   13.39 +  val normalize: config list -> Proof.context -> thm list ->
   13.40 +    Thm.cterm list * thm list
   13.41 +
   13.42 +  val setup: theory -> theory
   13.43 +end
   13.44 +
   13.45 +structure SMT_Normalize: SMT_NORMALIZE =
   13.46 +struct
   13.47 +
   13.48 +val norm_binder_conv = Conv.try_conv (More_Conv.rewrs_conv [
   13.49 +  @{lemma "All P == ALL x. P x" by (rule reflexive)},
   13.50 +  @{lemma "Ex P == EX x. P x" by (rule reflexive)},
   13.51 +  @{lemma "Let c P == let x = c in P x" by (rule reflexive)}])
   13.52 +
   13.53 +fun cert ctxt = Thm.cterm_of (ProofContext.theory_of ctxt)
   13.54 +
   13.55 +fun norm_meta_def cv thm = 
   13.56 +  let val thm' = Thm.combination thm (Thm.reflexive cv)
   13.57 +  in Thm.transitive thm' (Thm.beta_conversion false (Thm.rhs_of thm')) end
   13.58 +
   13.59 +fun norm_def ctxt thm =
   13.60 +  (case Thm.prop_of thm of
   13.61 +    Const (@{const_name "=="}, _) $ _ $ Abs (_, T, _) =>
   13.62 +      let val v = Var ((Name.uu, #maxidx (Thm.rep_thm thm) + 1), T)
   13.63 +      in norm_def ctxt (norm_meta_def (cert ctxt v) thm) end
   13.64 +  | @{term Trueprop} $ (Const (@{const_name "op ="}, _) $ _ $ Abs _) =>
   13.65 +      norm_def ctxt (thm RS @{thm fun_cong})
   13.66 +  | _ => thm)
   13.67 +
   13.68 +fun normalize_rule ctxt =
   13.69 +  Conv.fconv_rule (
   13.70 +    Thm.beta_conversion true then_conv
   13.71 +    Thm.eta_conversion then_conv
   13.72 +    More_Conv.bottom_conv (K norm_binder_conv) ctxt) #>
   13.73 +  norm_def ctxt #>
   13.74 +  Drule.forall_intr_vars #>
   13.75 +  Conv.fconv_rule ObjectLogic.atomize
   13.76 +
   13.77 +fun instantiate_free (cv, ct) thm =
   13.78 +  if Term.exists_subterm (equal (Thm.term_of cv)) (Thm.prop_of thm)
   13.79 +  then Thm.forall_elim ct (Thm.forall_intr cv thm)
   13.80 +  else thm
   13.81 +
   13.82 +fun discharge_definition ct thm =
   13.83 +  let val (cv, cu) = Thm.dest_equals ct
   13.84 +  in
   13.85 +    Thm.implies_intr ct thm
   13.86 +    |> instantiate_free (cv, cu)
   13.87 +    |> (fn thm => Thm.implies_elim thm (Thm.reflexive cu))
   13.88 +  end
   13.89 +
   13.90 +fun if_conv c cv1 cv2 ct = (if c (Thm.term_of ct) then cv1 else cv2) ct
   13.91 +fun if_true_conv c cv = if_conv c cv Conv.all_conv
   13.92 +
   13.93 +
   13.94 +(* simplification of trivial let expressions (whose bound variables occur at
   13.95 +   most once) *)
   13.96 +
   13.97 +local
   13.98 +  fun count i (Bound j) = if j = i then 1 else 0
   13.99 +    | count i (t $ u) = count i t + count i u
  13.100 +    | count i (Abs (_, _, t)) = count (i + 1) t
  13.101 +    | count _ _ = 0
  13.102 +
  13.103 +  fun is_trivial_let (Const (@{const_name Let}, _) $ _ $ Abs (_, _, t)) =
  13.104 +        (count 0 t <= 1)
  13.105 +    | is_trivial_let _ = false
  13.106 +
  13.107 +  fun let_conv _ = if_true_conv is_trivial_let (Conv.rewr_conv @{thm Let_def})
  13.108 +
  13.109 +  fun cond_let_conv ctxt = if_true_conv (Term.exists_subterm is_trivial_let)
  13.110 +    (More_Conv.top_conv let_conv ctxt)
  13.111 +in
  13.112 +fun trivial_let ctxt = map (Conv.fconv_rule (cond_let_conv ctxt))
  13.113 +end
  13.114 +
  13.115 +
  13.116 +(* rewriting of negative integer numerals into positive numerals *)
  13.117 +
  13.118 +local
  13.119 +  fun neg_numeral @{term Int.Min} = true
  13.120 +    | neg_numeral _ = false
  13.121 +  fun is_number_sort thy T = Sign.of_sort thy (T, @{sort number_ring})
  13.122 +  fun is_neg_number ctxt (Const (@{const_name number_of}, T) $ t) =
  13.123 +        Term.exists_subterm neg_numeral t andalso
  13.124 +        is_number_sort (ProofContext.theory_of ctxt) (Term.body_type T)
  13.125 +    | is_neg_number _ _ = false
  13.126 +  fun has_neg_number ctxt = Term.exists_subterm (is_neg_number ctxt)
  13.127 +
  13.128 +  val pos_numeral_ss = HOL_ss
  13.129 +    addsimps [@{thm Int.number_of_minus}, @{thm Int.number_of_Min}]
  13.130 +    addsimps [@{thm Int.numeral_1_eq_1}]
  13.131 +    addsimps @{thms Int.pred_bin_simps}
  13.132 +    addsimps @{thms Int.normalize_bin_simps}
  13.133 +    addsimps @{lemma
  13.134 +      "Int.Min = - Int.Bit1 Int.Pls"
  13.135 +      "Int.Bit0 (- Int.Pls) = - Int.Pls"
  13.136 +      "Int.Bit0 (- k) = - Int.Bit0 k"
  13.137 +      "Int.Bit1 (- k) = - Int.Bit1 (Int.pred k)"
  13.138 +      by simp_all (simp add: pred_def)}
  13.139 +
  13.140 +  fun pos_conv ctxt = if_conv (is_neg_number ctxt)
  13.141 +    (Simplifier.rewrite (Simplifier.context ctxt pos_numeral_ss))
  13.142 +    Conv.no_conv
  13.143 +
  13.144 +  fun cond_pos_conv ctxt = if_true_conv (has_neg_number ctxt)
  13.145 +    (More_Conv.top_sweep_conv pos_conv ctxt)
  13.146 +in
  13.147 +fun positive_numerals ctxt = map (Conv.fconv_rule (cond_pos_conv ctxt))
  13.148 +end
  13.149 +
  13.150 +
  13.151 +(* embedding of standard natural number operations into integer operations *)
  13.152 +
  13.153 +local
  13.154 +  val nat_embedding = @{lemma
  13.155 +    "nat (int n) = n"
  13.156 +    "i >= 0 --> int (nat i) = i"
  13.157 +    "i < 0 --> int (nat i) = 0"
  13.158 +    by simp_all}
  13.159 +
  13.160 +  val nat_rewriting = @{lemma
  13.161 +    "0 = nat 0"
  13.162 +    "1 = nat 1"
  13.163 +    "number_of i = nat (number_of i)"
  13.164 +    "int (nat 0) = 0"
  13.165 +    "int (nat 1) = 1"
  13.166 +    "a < b = (int a < int b)"
  13.167 +    "a <= b = (int a <= int b)"
  13.168 +    "Suc a = nat (int a + 1)"
  13.169 +    "a + b = nat (int a + int b)"
  13.170 +    "a - b = nat (int a - int b)"
  13.171 +    "a * b = nat (int a * int b)"
  13.172 +    "a div b = nat (int a div int b)"
  13.173 +    "a mod b = nat (int a mod int b)"
  13.174 +    "int (nat (int a + int b)) = int a + int b"
  13.175 +    "int (nat (int a * int b)) = int a * int b"
  13.176 +    "int (nat (int a div int b)) = int a div int b"
  13.177 +    "int (nat (int a mod int b)) = int a mod int b"
  13.178 +    by (simp add: nat_mult_distrib nat_div_distrib nat_mod_distrib
  13.179 +      int_mult[symmetric] zdiv_int[symmetric] zmod_int[symmetric])+}
  13.180 +
  13.181 +  fun on_positive num f x = 
  13.182 +    (case try HOLogic.dest_number (Thm.term_of num) of
  13.183 +      SOME (_, i) => if i >= 0 then SOME (f x) else NONE
  13.184 +    | NONE => NONE)
  13.185 +
  13.186 +  val cancel_int_nat_ss = HOL_ss
  13.187 +    addsimps [@{thm Nat_Numeral.nat_number_of}]
  13.188 +    addsimps [@{thm Nat_Numeral.int_nat_number_of}]
  13.189 +    addsimps @{thms neg_simps}
  13.190 +
  13.191 +  fun cancel_int_nat_simproc _ ss ct = 
  13.192 +    let
  13.193 +      val num = Thm.dest_arg (Thm.dest_arg ct)
  13.194 +      val goal = Thm.mk_binop @{cterm "op == :: int => _"} ct num
  13.195 +      val simpset = Simplifier.inherit_context ss cancel_int_nat_ss
  13.196 +      fun tac _ = Simplifier.simp_tac simpset 1
  13.197 +    in on_positive num (Goal.prove_internal [] goal) tac end
  13.198 +
  13.199 +  val nat_ss = HOL_ss
  13.200 +    addsimps nat_rewriting
  13.201 +    addsimprocs [Simplifier.make_simproc {
  13.202 +      name = "cancel_int_nat_num", lhss = [@{cpat "int (nat _)"}],
  13.203 +      proc = cancel_int_nat_simproc, identifier = [] }]
  13.204 +
  13.205 +  fun conv ctxt = Simplifier.rewrite (Simplifier.context ctxt nat_ss)
  13.206 +
  13.207 +  val uses_nat_type = Term.exists_type (Term.exists_subtype (equal @{typ nat}))
  13.208 +in
  13.209 +fun nat_as_int ctxt thms =
  13.210 +  let
  13.211 +    fun norm thm uses_nat =
  13.212 +      if not (uses_nat_type (Thm.prop_of thm)) then (thm, uses_nat)
  13.213 +      else (Conv.fconv_rule (conv ctxt) thm, true)
  13.214 +    val (thms', uses_nat) = fold_map norm thms false
  13.215 +  in if uses_nat then nat_embedding @ thms' else thms' end
  13.216 +end
  13.217 +
  13.218 +
  13.219 +(* include additional rules *)
  13.220 +
  13.221 +val (unfold_defs, unfold_defs_setup) =
  13.222 +  Attrib.config_bool "smt_unfold_defs" true
  13.223 +
  13.224 +local
  13.225 +  val pair_rules = [@{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}]
  13.226 +
  13.227 +  val pair_type = (fn Type (@{type_name "*"}, _) => true | _ => false)
  13.228 +  val exists_pair_type = Term.exists_type (Term.exists_subtype pair_type)
  13.229 +
  13.230 +  val fun_upd_rules = [@{thm fun_upd_same}, @{thm fun_upd_apply}]
  13.231 +  val is_fun_upd = (fn Const (@{const_name fun_upd}, _) => true | _ => false)
  13.232 +  val exists_fun_upd = Term.exists_subterm is_fun_upd
  13.233 +in
  13.234 +fun add_pair_rules _ thms =
  13.235 +  thms
  13.236 +  |> exists (exists_pair_type o Thm.prop_of) thms ? append pair_rules
  13.237 +
  13.238 +fun add_fun_upd_rules _ thms =
  13.239 +  thms
  13.240 +  |> exists (exists_fun_upd o Thm.prop_of) thms ? append fun_upd_rules
  13.241 +end
  13.242 +
  13.243 +
  13.244 +local
  13.245 +  fun mk_entry t thm = (Term.head_of t, (thm, thm RS @{thm eq_reflection}))
  13.246 +  fun prepare_def thm =
  13.247 +    (case HOLogic.dest_Trueprop (Thm.prop_of thm) of
  13.248 +      Const (@{const_name "op ="}, _) $ t $ _ => mk_entry t thm
  13.249 +    | t => raise TERM ("prepare_def", [t]))
  13.250 +
  13.251 +  val defs = map prepare_def [
  13.252 +    @{thm abs_if[where 'a = int]}, @{thm abs_if[where 'a = real]},
  13.253 +    @{thm min_def[where 'a = int]}, @{thm min_def[where 'a = real]},
  13.254 +    @{thm max_def[where 'a = int]}, @{thm max_def[where 'a = real]}]
  13.255 +
  13.256 +  fun add_sym t = if AList.defined (op =) defs t then insert (op =) t else I
  13.257 +  fun add_syms thms = fold (Term.fold_aterms add_sym o Thm.prop_of) thms []
  13.258 +
  13.259 +  fun unfold_conv ctxt ct =
  13.260 +    (case AList.lookup (op =) defs (Term.head_of (Thm.term_of ct)) of
  13.261 +      SOME (_, eq) => Conv.rewr_conv eq
  13.262 +    | NONE => Conv.all_conv) ct
  13.263 +in
  13.264 +fun add_abs_min_max_rules ctxt thms =
  13.265 +  if Config.get ctxt unfold_defs
  13.266 +  then map (Conv.fconv_rule (More_Conv.bottom_conv unfold_conv ctxt)) thms
  13.267 +  else map fst (map_filter (AList.lookup (op =) defs) (add_syms thms)) @ thms
  13.268 +end
  13.269 +
  13.270 +
  13.271 +(* lift lambda terms into additional rules *)
  13.272 +
  13.273 +local
  13.274 +  val meta_eq = @{cpat "op =="}
  13.275 +  val meta_eqT = hd (Thm.dest_ctyp (Thm.ctyp_of_term meta_eq))
  13.276 +  fun inst_meta cT = Thm.instantiate_cterm ([(meta_eqT, cT)], []) meta_eq
  13.277 +  fun mk_meta_eq ct cu = Thm.mk_binop (inst_meta (Thm.ctyp_of_term ct)) ct cu
  13.278 +
  13.279 +  fun lambda_conv conv =
  13.280 +    let
  13.281 +      fun sub_conv cvs ctxt ct =
  13.282 +        (case Thm.term_of ct of
  13.283 +          Const (@{const_name All}, _) $ Abs _ => quant_conv cvs ctxt
  13.284 +        | Const (@{const_name Ex}, _) $ Abs _ => quant_conv cvs ctxt
  13.285 +        | Const _ $ Abs _ => Conv.arg_conv (at_lambda_conv cvs ctxt)
  13.286 +        | Const (@{const_name Let}, _) $ _ $ Abs _ => Conv.combination_conv
  13.287 +            (Conv.arg_conv (sub_conv cvs ctxt)) (abs_conv cvs ctxt)
  13.288 +        | Abs _ => at_lambda_conv cvs ctxt
  13.289 +        | _ $ _ => Conv.comb_conv (sub_conv cvs ctxt)
  13.290 +        | _ => Conv.all_conv) ct
  13.291 +      and abs_conv cvs = Conv.abs_conv (fn (cv, cx) => sub_conv (cv::cvs) cx)
  13.292 +      and quant_conv cvs ctxt = Conv.arg_conv (abs_conv cvs ctxt)
  13.293 +      and at_lambda_conv cvs ctxt = abs_conv cvs ctxt then_conv conv cvs ctxt
  13.294 +    in sub_conv [] end
  13.295 +
  13.296 +  fun used_vars cvs ct =
  13.297 +    let
  13.298 +      val lookup = AList.lookup (op aconv) (map (` Thm.term_of) cvs)
  13.299 +      val add = (fn (SOME ct) => insert (op aconvc) ct | _ => I)
  13.300 +    in Term.fold_aterms (add o lookup) (Thm.term_of ct) [] end
  13.301 +
  13.302 +  val rev_int_fst_ord = rev_order o int_ord o pairself fst
  13.303 +  fun ordered_values tab =
  13.304 +    Termtab.fold (fn (_, x) => OrdList.insert rev_int_fst_ord x) tab []
  13.305 +    |> map snd
  13.306 +in
  13.307 +fun lift_lambdas ctxt thms =
  13.308 +  let
  13.309 +    val declare_frees = fold (Thm.fold_terms Term.declare_term_frees)
  13.310 +    val names = ref (declare_frees thms (Name.make_context []))
  13.311 +    val fresh_name = change_result names o yield_singleton Name.variants
  13.312 +
  13.313 +    val defs = ref (Termtab.empty : (int * thm) Termtab.table)
  13.314 +    fun add_def t thm = change defs (Termtab.update (t, (serial (), thm)))
  13.315 +    fun make_def cvs eq = Thm.symmetric (fold norm_meta_def cvs eq)
  13.316 +    fun def_conv cvs ctxt ct =
  13.317 +      let
  13.318 +        val cvs' = used_vars cvs ct
  13.319 +        val ct' = fold Thm.cabs cvs' ct
  13.320 +      in
  13.321 +        (case Termtab.lookup (!defs) (Thm.term_of ct') of
  13.322 +          SOME (_, eq) => make_def cvs' eq
  13.323 +        | NONE =>
  13.324 +            let
  13.325 +              val {t, T, ...} = Thm.rep_cterm ct'
  13.326 +              val eq = mk_meta_eq (cert ctxt (Free (fresh_name "", T))) ct'
  13.327 +              val thm = Thm.assume eq
  13.328 +            in (add_def t thm; make_def cvs' thm) end)
  13.329 +      end
  13.330 +    val thms' = map (Conv.fconv_rule (lambda_conv def_conv ctxt)) thms
  13.331 +    val eqs = ordered_values (!defs)
  13.332 +  in
  13.333 +    (maps (#hyps o Thm.crep_thm) eqs, map (normalize_rule ctxt) eqs @ thms')
  13.334 +  end
  13.335 +end
  13.336 +
  13.337 +
  13.338 +(* make application explicit for functions with varying number of arguments *)
  13.339 +
  13.340 +local
  13.341 +  val const = prefix "c" and free = prefix "f"
  13.342 +  fun min i (e as (_, j)) = if i <> j then (true, Int.min (i, j)) else e
  13.343 +  fun add t i = Symtab.map_default (t, (false, i)) (min i)
  13.344 +  fun traverse t =
  13.345 +    (case Term.strip_comb t of
  13.346 +      (Const (n, _), ts) => add (const n) (length ts) #> fold traverse ts 
  13.347 +    | (Free (n, _), ts) => add (free n) (length ts) #> fold traverse ts
  13.348 +    | (Abs (_, _, u), ts) => fold traverse (u :: ts)
  13.349 +    | (_, ts) => fold traverse ts)
  13.350 +  val prune = (fn (n, (true, i)) => Symtab.update (n, i) | _ => I)
  13.351 +  fun prune_tab tab = Symtab.fold prune tab Symtab.empty
  13.352 +
  13.353 +  fun binop_conv cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
  13.354 +  fun nary_conv conv1 conv2 ct =
  13.355 +    (Conv.combination_conv (nary_conv conv1 conv2) conv2 else_conv conv1) ct
  13.356 +  fun abs_conv conv tb = Conv.abs_conv (fn (cv, cx) =>
  13.357 +    let val n = fst (Term.dest_Free (Thm.term_of cv))
  13.358 +    in conv (Symtab.update (free n, 0) tb) cx end)
  13.359 +  val apply_rule = @{lemma "f x == apply f x" by (simp add: apply_def)}
  13.360 +in
  13.361 +fun explicit_application ctxt thms =
  13.362 +  let
  13.363 +    fun sub_conv tb ctxt ct =
  13.364 +      (case Term.strip_comb (Thm.term_of ct) of
  13.365 +        (Const (n, _), ts) => app_conv tb (const n) (length ts) ctxt
  13.366 +      | (Free (n, _), ts) => app_conv tb (free n) (length ts) ctxt
  13.367 +      | (Abs _, ts) => nary_conv (abs_conv sub_conv tb ctxt) (sub_conv tb ctxt)
  13.368 +      | (_, ts) => nary_conv Conv.all_conv (sub_conv tb ctxt)) ct
  13.369 +    and app_conv tb n i ctxt =
  13.370 +      (case Symtab.lookup tb n of
  13.371 +        NONE => nary_conv Conv.all_conv (sub_conv tb ctxt)
  13.372 +      | SOME j => apply_conv tb ctxt (i - j))
  13.373 +    and apply_conv tb ctxt i ct = (
  13.374 +      if i = 0 then nary_conv Conv.all_conv (sub_conv tb ctxt)
  13.375 +      else
  13.376 +        Conv.rewr_conv apply_rule then_conv
  13.377 +        binop_conv (apply_conv tb ctxt (i-1)) (sub_conv tb ctxt)) ct
  13.378 +
  13.379 +    val tab = prune_tab (fold (traverse o Thm.prop_of) thms Symtab.empty)
  13.380 +  in map (Conv.fconv_rule (sub_conv tab ctxt)) thms end
  13.381 +end
  13.382 +
  13.383 +
  13.384 +(* combined normalization *)
  13.385 +
  13.386 +datatype config =
  13.387 +  RewriteTrivialLets |
  13.388 +  RewriteNegativeNumerals |
  13.389 +  RewriteNaturalNumbers |
  13.390 +  AddPairRules |
  13.391 +  AddFunUpdRules |
  13.392 +  AddAbsMinMaxRules
  13.393 +
  13.394 +fun normalize config ctxt thms =
  13.395 +  let fun if_enabled c f = member (op =) config c ? f ctxt
  13.396 +  in
  13.397 +    thms
  13.398 +    |> if_enabled RewriteTrivialLets trivial_let
  13.399 +    |> if_enabled RewriteNegativeNumerals positive_numerals
  13.400 +    |> if_enabled RewriteNaturalNumbers nat_as_int
  13.401 +    |> if_enabled AddPairRules add_pair_rules
  13.402 +    |> if_enabled AddFunUpdRules add_fun_upd_rules
  13.403 +    |> if_enabled AddAbsMinMaxRules add_abs_min_max_rules
  13.404 +    |> map (normalize_rule ctxt)
  13.405 +    |> lift_lambdas ctxt
  13.406 +    |> apsnd (explicit_application ctxt)
  13.407 +  end
  13.408 +
  13.409 +val setup = unfold_defs_setup
  13.410 +
  13.411 +end
    14.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.2 +++ b/src/HOL/SMT/Tools/smt_solver.ML	Fri Sep 18 18:13:19 2009 +0200
    14.3 @@ -0,0 +1,248 @@
    14.4 +(*  Title:      HOL/SMT/Tools/smt_solver.ML
    14.5 +    Author:     Sascha Boehme, TU Muenchen
    14.6 +
    14.7 +SMT solvers registry and SMT tactic.
    14.8 +*)
    14.9 +
   14.10 +signature SMT_SOLVER =
   14.11 +sig
   14.12 +  exception SMT_COUNTEREXAMPLE of bool * term list
   14.13 +
   14.14 +  datatype interface = Interface of {
   14.15 +    normalize: SMT_Normalize.config list,
   14.16 +    translate: SMT_Translate.config }
   14.17 +
   14.18 +  datatype proof_data = ProofData of {
   14.19 +    context: Proof.context,
   14.20 +    output: string list,
   14.21 +    recon: SMT_Translate.recon,
   14.22 +    assms: thm list option }
   14.23 +
   14.24 +  datatype solver_config = SolverConfig of {
   14.25 +    name: {env_var: string, remote_name: string},
   14.26 +    interface: interface,
   14.27 +    arguments: string list,
   14.28 +    reconstruct: proof_data -> thm }
   14.29 +
   14.30 +  (*options*)
   14.31 +  val timeout: int Config.T
   14.32 +  val with_timeout: Proof.context -> ('a -> 'b) -> 'a -> 'b
   14.33 +  val trace: bool Config.T
   14.34 +  val trace_msg: Proof.context -> ('a -> string) -> 'a -> unit
   14.35 +
   14.36 +  (*solvers*)
   14.37 +  type solver = Proof.context -> thm list -> thm
   14.38 +  type solver_info = Context.generic -> Pretty.T list
   14.39 +  val add_solver: string * (Proof.context -> solver_config) -> theory ->
   14.40 +    theory
   14.41 +  val all_solver_names_of: theory -> string list
   14.42 +  val add_solver_info: string * solver_info -> theory -> theory
   14.43 +  val solver_name_of: Context.generic -> string
   14.44 +  val select_solver: string -> Context.generic -> Context.generic
   14.45 +  val solver_of: Context.generic -> solver
   14.46 +
   14.47 +  (*tactic*)
   14.48 +  val smt_tac': bool -> Proof.context -> thm list -> int -> Tactical.tactic
   14.49 +  val smt_tac: Proof.context -> thm list -> int -> Tactical.tactic
   14.50 +
   14.51 +  (*setup*)
   14.52 +  val setup: theory -> theory
   14.53 +  val print_setup: Context.generic -> unit
   14.54 +end
   14.55 +
   14.56 +structure SMT_Solver: SMT_SOLVER =
   14.57 +struct
   14.58 +
   14.59 +exception SMT_COUNTEREXAMPLE of bool * term list
   14.60 +
   14.61 +val theory_of = Context.cases I ProofContext.theory_of
   14.62 +
   14.63 +
   14.64 +datatype interface = Interface of {
   14.65 +  normalize: SMT_Normalize.config list,
   14.66 +  translate: SMT_Translate.config }
   14.67 +
   14.68 +datatype proof_data = ProofData of {
   14.69 +  context: Proof.context,
   14.70 +  output: string list,
   14.71 +  recon: SMT_Translate.recon,
   14.72 +  assms: thm list option }
   14.73 +
   14.74 +datatype solver_config = SolverConfig of {
   14.75 +  name: {env_var: string, remote_name: string},
   14.76 +  interface: interface,
   14.77 +  arguments: string list,
   14.78 +  reconstruct: proof_data -> thm }
   14.79 +
   14.80 +
   14.81 +(* SMT options *)
   14.82 +
   14.83 +val (timeout, setup_timeout) = Attrib.config_int "smt_timeout" 30
   14.84 +
   14.85 +fun with_timeout ctxt f x =
   14.86 +  TimeLimit.timeLimit (Time.fromSeconds (Config.get ctxt timeout)) f x
   14.87 +  handle TimeLimit.TimeOut => error ("SMT: timeout")
   14.88 +
   14.89 +val (trace, setup_trace) = Attrib.config_bool "smt_trace" false
   14.90 +
   14.91 +fun trace_msg ctxt f x =
   14.92 +  if Config.get ctxt trace then Output.tracing (f x) else ()
   14.93 +
   14.94 +
   14.95 +(* interface to external solvers *)
   14.96 +
   14.97 +local
   14.98 +
   14.99 +fun with_tmp_files f x =
  14.100 +  let
  14.101 +    fun tmp_path () = File.tmp_path (Path.explode ("smt-" ^ serial_string ()))
  14.102 +    val in_path = tmp_path () and out_path = tmp_path ()
  14.103 +    val y = Exn.capture (f in_path out_path) x
  14.104 +    val _ = try File.rm in_path and _ = try File.rm out_path
  14.105 +  in Exn.release y end
  14.106 +
  14.107 +fun run in_path out_path (ctxt, cmd, output) =
  14.108 +  let
  14.109 +    val x = File.open_output output in_path
  14.110 +    val _ = trace_msg ctxt File.read in_path
  14.111 +
  14.112 +    val _ = with_timeout ctxt system_out (cmd in_path out_path)
  14.113 +    fun lines_of path = the_default [] (try (File.fold_lines cons out_path) [])
  14.114 +    val ls = rev (dropwhile (equal "") (lines_of out_path))
  14.115 +    val _ = trace_msg ctxt cat_lines ls
  14.116 +  in (x, ls) end
  14.117 +
  14.118 +in
  14.119 +
  14.120 +fun run_solver ctxt {env_var, remote_name} args output =
  14.121 +  let
  14.122 +    val qf = File.shell_path and qq = enclose "'" "'"
  14.123 +    val path = getenv env_var and remote = getenv "REMOTE_SMT_SOLVER"
  14.124 +    fun cmd f1 f2 =
  14.125 +      if path <> ""
  14.126 +      then map qq (path :: args) @ [qf f1, ">", qf f2]
  14.127 +      else map qq (remote :: remote_name :: args) @ [qf f1, qf f2]
  14.128 +  in with_tmp_files run (ctxt, space_implode " " oo cmd, output) end
  14.129 +
  14.130 +end
  14.131 +
  14.132 +fun make_proof_data ctxt ((recon, thms), ls) =
  14.133 +  ProofData {context=ctxt, output=ls, recon=recon, assms=SOME thms}
  14.134 +
  14.135 +fun gen_solver solver ctxt prems =
  14.136 +  let
  14.137 +    val SolverConfig {name, interface, arguments, reconstruct} = solver ctxt
  14.138 +    val Interface {normalize=nc, translate=tc} = interface
  14.139 +    val thy = ProofContext.theory_of ctxt
  14.140 +  in
  14.141 +    SMT_Normalize.normalize nc ctxt prems
  14.142 +    ||> run_solver ctxt name arguments o SMT_Translate.translate tc thy
  14.143 +    ||> reconstruct o make_proof_data ctxt
  14.144 +    |-> fold SMT_Normalize.discharge_definition
  14.145 +  end
  14.146 +
  14.147 +
  14.148 +(* solver store *)
  14.149 +
  14.150 +type solver = Proof.context -> thm list -> thm
  14.151 +type solver_info = Context.generic -> Pretty.T list
  14.152 +
  14.153 +structure Solvers = TheoryDataFun
  14.154 +(
  14.155 +  type T = ((Proof.context -> solver_config) * solver_info) Symtab.table
  14.156 +  val empty = Symtab.empty
  14.157 +  val copy = I
  14.158 +  val extend = I
  14.159 +  fun merge _ = Symtab.merge (K true)
  14.160 +    handle Symtab.DUP name => error ("Duplicate SMT solver: " ^ quote name)
  14.161 +)
  14.162 +
  14.163 +val no_solver = "(none)"
  14.164 +val add_solver = Solvers.map o Symtab.update_new o apsnd (rpair (K []))
  14.165 +val all_solver_names_of = Symtab.keys o Solvers.get
  14.166 +val lookup_solver = Symtab.lookup o Solvers.get
  14.167 +fun add_solver_info (n, i) = Solvers.map (Symtab.map_entry n (apsnd (K i)))
  14.168 +
  14.169 +
  14.170 +(* selected solver *)
  14.171 +
  14.172 +structure SelectedSolver = GenericDataFun
  14.173 +(
  14.174 +  type T = serial * string
  14.175 +  val empty = (serial (), no_solver)
  14.176 +  val extend = I
  14.177 +  fun merge _ (sl1 as (s1, _), sl2 as (s2, _)) = if s1 > s2 then sl1 else sl2
  14.178 +)
  14.179 +
  14.180 +val solver_name_of = snd o SelectedSolver.get
  14.181 +
  14.182 +fun select_solver name gen =
  14.183 +  if is_none (lookup_solver (theory_of gen) name)
  14.184 +  then error ("SMT solver not registered: " ^ quote name)
  14.185 +  else SelectedSolver.map (K (serial (), name)) gen
  14.186 +
  14.187 +fun raw_solver_of gen =
  14.188 +  (case lookup_solver (theory_of gen) (solver_name_of gen) of
  14.189 +    NONE => error "No SMT solver selected"
  14.190 +  | SOME (s, _) => s)
  14.191 +
  14.192 +val solver_of = gen_solver o raw_solver_of
  14.193 +
  14.194 +
  14.195 +(* SMT tactic *)
  14.196 +
  14.197 +fun smt_unsat_tac solver ctxt rules =
  14.198 +  Tactic.rtac @{thm ccontr} THEN'
  14.199 +  SUBPROOF (fn {context, prems, ...} =>
  14.200 +    Tactic.rtac (solver context (rules @ prems)) 1) ctxt
  14.201 +
  14.202 +fun pretty_counterex ctxt (real, ex) =
  14.203 +  let
  14.204 +    val msg = if real then "Counterexample found:"
  14.205 +      else "Potential counterexample found:"
  14.206 +    val cex = if null ex then [Pretty.str "(no assignments)"]
  14.207 +      else map (Syntax.pretty_term ctxt) ex
  14.208 +  in Pretty.string_of (Pretty.big_list msg cex) end
  14.209 +
  14.210 +fun smt_tac' pass_smt_exns ctxt =
  14.211 +  let
  14.212 +    val solver = solver_of (Context.Proof ctxt)
  14.213 +    fun safe_solver ctxt thms = solver ctxt thms
  14.214 +      handle SMT_COUNTEREXAMPLE cex => error (pretty_counterex ctxt cex)
  14.215 +    val solver' = if pass_smt_exns then solver else safe_solver
  14.216 +  in smt_unsat_tac solver' ctxt end
  14.217 +
  14.218 +val smt_tac = smt_tac' false
  14.219 +
  14.220 +
  14.221 +(* setup *)
  14.222 +
  14.223 +val setup =
  14.224 +  Attrib.setup (Binding.name "smt_solver")
  14.225 +    (Scan.lift (OuterParse.$$$ "=" |-- Args.name) >>
  14.226 +      (Thm.declaration_attribute o K o select_solver))
  14.227 +    "SMT solver configuration" #>
  14.228 +  setup_timeout #>
  14.229 +  setup_trace
  14.230 +
  14.231 +fun print_setup gen =
  14.232 +  let
  14.233 +    val t = string_of_int (Config.get_generic gen timeout)
  14.234 +    val names = sort string_ord (all_solver_names_of (theory_of gen))
  14.235 +    val ns = if null names then [no_solver] else names
  14.236 +    val take_info = (fn (_, []) => NONE | info => SOME info)
  14.237 +    val infos =
  14.238 +      theory_of gen
  14.239 +      |> Symtab.dest o Solvers.get
  14.240 +      |> map_filter (fn (n, (_, info)) => take_info (n, info gen))
  14.241 +      |> sort (prod_ord string_ord (K EQUAL))
  14.242 +      |> map (fn (n, ps) => Pretty.big_list (n ^ ":") ps)
  14.243 +  in
  14.244 +    Pretty.writeln (Pretty.big_list "SMT setup:" [
  14.245 +      Pretty.str ("Current SMT solver: " ^ solver_name_of gen),
  14.246 +      Pretty.str_list "Available SMT solvers: "  "" ns,
  14.247 +      Pretty.str ("Current timeout: " ^ t ^ " seconds"),
  14.248 +      Pretty.big_list "Solver-specific settings:" infos])
  14.249 +  end
  14.250 +
  14.251 +end
    15.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.2 +++ b/src/HOL/SMT/Tools/smt_translate.ML	Fri Sep 18 18:13:19 2009 +0200
    15.3 @@ -0,0 +1,507 @@
    15.4 +(*  Title:      HOL/SMT/Tools/smt_translate.ML
    15.5 +    Author:     Sascha Boehme, TU Muenchen
    15.6 +
    15.7 +Translate theorems into an SMT intermediate format and serialize them,
    15.8 +depending on an SMT interface.
    15.9 +*)
   15.10 +
   15.11 +signature SMT_TRANSLATE =
   15.12 +sig
   15.13 +  (* intermediate term structure *)
   15.14 +  datatype sym =
   15.15 +    SConst of string * typ |
   15.16 +    SFree of string * typ |
   15.17 +    SNum of int * typ
   15.18 +  datatype squant = SForall | SExists
   15.19 +  datatype 'a spattern = SPat of 'a list | SNoPat of 'a list
   15.20 +  datatype ('a, 'b) sterm =
   15.21 +    SVar of int |
   15.22 +    SApp of 'a * ('a, 'b) sterm list |
   15.23 +    SLet of (string * 'b) * ('a, 'b) sterm * ('a, 'b) sterm |
   15.24 +    SQuant of squant * (string * 'b) list * ('a, 'b) sterm spattern list *
   15.25 +      ('a, 'b) sterm
   15.26 +
   15.27 +  (* table for built-in symbols *)
   15.28 +  type builtin_fun = typ -> (sym, typ) sterm list ->
   15.29 +    (string * (sym, typ) sterm list) option
   15.30 +  type builtin_table = (typ * builtin_fun) list Symtab.table
   15.31 +  val builtin_make: (term * string) list -> builtin_table
   15.32 +  val builtin_add: term * builtin_fun -> builtin_table -> builtin_table
   15.33 +  val builtin_lookup: builtin_table -> theory -> string * typ ->
   15.34 +    (sym, typ) sterm list -> (string * (sym, typ) sterm list) option
   15.35 +  val bv_rotate: (int -> string) -> builtin_fun
   15.36 +  val bv_extend: (int -> string) -> builtin_fun
   15.37 +  val bv_extract: (int -> int -> string) -> builtin_fun
   15.38 +
   15.39 +  (* configuration options *)
   15.40 +  datatype prefixes = Prefixes of {
   15.41 +    var_prefix: string,
   15.42 +    typ_prefix: string,
   15.43 +    fun_prefix: string,
   15.44 +    pred_prefix: string }
   15.45 +  datatype markers = Markers of {
   15.46 +    term_marker: string,
   15.47 +    formula_marker: string }
   15.48 +  datatype builtins = Builtins of {
   15.49 +    builtin_typ: typ -> string option,
   15.50 +    builtin_num: int * typ -> string option,
   15.51 +    builtin_fun: bool -> builtin_table }
   15.52 +  datatype sign = Sign of {
   15.53 +    typs: string list,
   15.54 +    funs: (string * (string list * string)) list,
   15.55 +    preds: (string * string list) list }
   15.56 +  datatype config = Config of {
   15.57 +    strict: bool,
   15.58 +    prefixes: prefixes,
   15.59 +    markers: markers,
   15.60 +    builtins: builtins,
   15.61 +    serialize: sign -> (string, string) sterm list -> TextIO.outstream -> unit}
   15.62 +  datatype recon = Recon of {typs: typ Symtab.table, terms: term Symtab.table}
   15.63 +
   15.64 +  val translate: config -> theory -> thm list -> TextIO.outstream ->
   15.65 +    recon * thm list
   15.66 +
   15.67 +  val dest_binT: typ -> int
   15.68 +  val dest_funT: int -> typ -> typ list * typ
   15.69 +end
   15.70 +
   15.71 +structure SMT_Translate: SMT_TRANSLATE =
   15.72 +struct
   15.73 +
   15.74 +(* Intermediate term structure *)
   15.75 +
   15.76 +datatype sym =
   15.77 +  SConst of string * typ |
   15.78 +  SFree of string * typ |
   15.79 +  SNum of int * typ
   15.80 +datatype squant = SForall | SExists
   15.81 +datatype 'a spattern = SPat of 'a list | SNoPat of 'a list
   15.82 +datatype ('a, 'b) sterm =
   15.83 +  SVar of int |
   15.84 +  SApp of 'a * ('a, 'b) sterm list |
   15.85 +  SLet of (string * 'b) * ('a, 'b) sterm * ('a, 'b) sterm |
   15.86 +  SQuant of squant * (string * 'b) list * ('a, 'b) sterm spattern list *
   15.87 +    ('a, 'b) sterm
   15.88 +
   15.89 +fun app c ts = SApp (c, ts)
   15.90 +
   15.91 +fun map_pat f (SPat ps) = SPat (map f ps)
   15.92 +  | map_pat f (SNoPat ps) = SNoPat (map f ps)
   15.93 +
   15.94 +fun fold_map_pat f (SPat ps) = fold_map f ps #>> SPat
   15.95 +  | fold_map_pat f (SNoPat ps) = fold_map f ps #>> SNoPat
   15.96 +
   15.97 +val make_sconst = SConst o Term.dest_Const
   15.98 +
   15.99 +
  15.100 +(* General type destructors. *)
  15.101 +
  15.102 +fun dest_binT T =
  15.103 +  (case T of
  15.104 +    Type (@{type_name "Numeral_Type.num0"}, _) => 0
  15.105 +  | Type (@{type_name "Numeral_Type.num1"}, _) => 1
  15.106 +  | Type (@{type_name "Numeral_Type.bit0"}, [T]) => 2 * dest_binT T
  15.107 +  | Type (@{type_name "Numeral_Type.bit1"}, [T]) => 1 + 2 * dest_binT T
  15.108 +  | _ => raise TYPE ("dest_binT", [T], []))
  15.109 +
  15.110 +val dest_wordT = (fn
  15.111 +    Type (@{type_name "word"}, [T]) => dest_binT T
  15.112 +  | T => raise TYPE ("dest_wordT", [T], []))
  15.113 +
  15.114 +val dest_funT =
  15.115 +  let
  15.116 +    fun dest Ts 0 T = (rev Ts, T)
  15.117 +      | dest Ts i (Type ("fun", [T, U])) = dest (T::Ts) (i-1) U
  15.118 +      | dest _ _ T = raise TYPE ("dest_funT", [T], [])
  15.119 +  in dest [] end
  15.120 +
  15.121 +
  15.122 +(* Table for built-in symbols *)
  15.123 +
  15.124 +type builtin_fun = typ -> (sym, typ) sterm list ->
  15.125 +  (string * (sym, typ) sterm list) option
  15.126 +type builtin_table = (typ * builtin_fun) list Symtab.table
  15.127 +
  15.128 +fun builtin_make entries =
  15.129 +  let
  15.130 +    fun dest (t, bn) =
  15.131 +      let val (n, T) = Term.dest_Const t
  15.132 +      in (n, (Logic.varifyT T, K (SOME o pair bn))) end
  15.133 +  in Symtab.make (AList.group (op =) (map dest entries)) end
  15.134 +
  15.135 +fun builtin_add (t, f) tab =
  15.136 +  let val (n, T) = apsnd Logic.varifyT (Term.dest_Const t)
  15.137 +  in Symtab.map_default (n, []) (AList.update (op =) (T, f)) tab end
  15.138 +
  15.139 +fun builtin_lookup tab thy (n, T) ts =
  15.140 +  AList.lookup (Sign.typ_instance thy) (Symtab.lookup_list tab n) T
  15.141 +  |> (fn SOME f => f T ts | NONE => NONE)
  15.142 +
  15.143 +local
  15.144 +  val dest_nat = (fn
  15.145 +      SApp (SConst (@{const_name nat}, _), [SApp (SNum (i, _), _)]) => SOME i
  15.146 +    | _ => NONE)
  15.147 +in
  15.148 +fun bv_rotate mk_name T ts =
  15.149 +  dest_nat (hd ts) |> Option.map (fn i => (mk_name i, tl ts))
  15.150 +
  15.151 +fun bv_extend mk_name T ts =
  15.152 +  (case (try dest_wordT (domain_type T), try dest_wordT (range_type T)) of
  15.153 +    (SOME i, SOME j) => if j - i >= 0 then SOME (mk_name (j - i), ts) else NONE
  15.154 +  | _ => NONE)
  15.155 +
  15.156 +fun bv_extract mk_name T ts =
  15.157 +  (case (try dest_wordT (body_type T), dest_nat (hd ts)) of
  15.158 +    (SOME i, SOME lb) => SOME (mk_name (i + lb - 1) lb, tl ts)
  15.159 +  | _ => NONE)
  15.160 +end
  15.161 +
  15.162 +
  15.163 +(* Configuration options *)
  15.164 +
  15.165 +datatype prefixes = Prefixes of {
  15.166 +  var_prefix: string,
  15.167 +  typ_prefix: string,
  15.168 +  fun_prefix: string,
  15.169 +  pred_prefix: string }
  15.170 +datatype markers = Markers of {
  15.171 +  term_marker: string,
  15.172 +  formula_marker: string }
  15.173 +datatype builtins = Builtins of {
  15.174 +  builtin_typ: typ -> string option,
  15.175 +  builtin_num: int * typ -> string option,
  15.176 +  builtin_fun: bool -> builtin_table }
  15.177 +datatype sign = Sign of {
  15.178 +  typs: string list,
  15.179 +  funs: (string * (string list * string)) list,
  15.180 +  preds: (string * string list) list }
  15.181 +datatype config = Config of {
  15.182 +  strict: bool,
  15.183 +  prefixes: prefixes,
  15.184 +  markers: markers,
  15.185 +  builtins: builtins,
  15.186 +  serialize: sign -> (string, string) sterm list -> TextIO.outstream -> unit}
  15.187 +datatype recon = Recon of {typs: typ Symtab.table, terms: term Symtab.table}
  15.188 +
  15.189 +
  15.190 +(* Translate Isabelle/HOL terms into SMT intermediate terms.
  15.191 +   We assume that lambda-lifting has been performed before, i.e., lambda
  15.192 +   abstractions occur only at quantifiers and let expressions.
  15.193 +*)
  15.194 +local
  15.195 +  val quantifier = (fn
  15.196 +      @{const_name All} => SOME SForall
  15.197 +    | @{const_name Ex} => SOME SExists
  15.198 +    | _ => NONE)
  15.199 +
  15.200 +  fun group_quant qname vs (t as Const (q, _) $ Abs (n, T, u)) =
  15.201 +        if q = qname then group_quant qname ((n, T) :: vs) u else (vs, t)
  15.202 +    | group_quant qname vs t = (vs, t)
  15.203 +
  15.204 +  fun dest_trigger (@{term trigger} $ tl $ t) = (HOLogic.dest_list tl, t)
  15.205 +    | dest_trigger t = ([], t)
  15.206 +
  15.207 +  fun pat f ps (Const (@{const_name pat}, _) $ p) = SPat (rev (f p :: ps))
  15.208 +    | pat f ps (Const (@{const_name nopat}, _) $ p) = SNoPat (rev (f p :: ps))
  15.209 +    | pat f ps (Const (@{const_name andpat}, _) $ p $ t) = pat f (f p :: ps) t
  15.210 +    | pat _ _ t = raise TERM ("pat", [t])
  15.211 +
  15.212 +  fun trans Ts t =
  15.213 +    (case Term.strip_comb t of
  15.214 +      (t1 as Const (qn, qT), [t2 as Abs (n, T, t3)]) =>
  15.215 +        (case quantifier qn of
  15.216 +          SOME q =>
  15.217 +            let
  15.218 +              val (vs, u) = group_quant qn [(n, T)] t3
  15.219 +              val Us = map snd vs @ Ts
  15.220 +              val (ps, b) = dest_trigger u
  15.221 +            in SQuant (q, rev vs, map (pat (trans Us) []) ps, trans Us b) end
  15.222 +        | NONE => raise TERM ("intermediate", [t]))
  15.223 +    | (Const (@{const_name Let}, _), [t1, Abs (n, T, t2)]) =>
  15.224 +        SLet ((n, T), trans Ts t1, trans (T :: Ts) t2)
  15.225 +    | (Const (c as (@{const_name distinct}, _)), [t1]) =>
  15.226 +        (* this is not type-correct, but will be corrected at a later stage *)
  15.227 +        SApp (SConst c, map (trans Ts) (HOLogic.dest_list t1))
  15.228 +    | (Const c, ts) =>
  15.229 +        (case try HOLogic.dest_number t of
  15.230 +          SOME (T, i) => SApp (SNum (i, T), [])
  15.231 +        | NONE => SApp (SConst c, map (trans Ts) ts))
  15.232 +    | (Free c, ts) => SApp (SFree c, map (trans Ts) ts)
  15.233 +    | (Bound i, []) => SVar i
  15.234 +    | _ => raise TERM ("intermediate", [t]))
  15.235 +in
  15.236 +fun intermediate ts = map (trans [] o HOLogic.dest_Trueprop) ts
  15.237 +end
  15.238 +
  15.239 +
  15.240 +(* Separate formulas from terms by adding special marker symbols ("term",
  15.241 +   "formula"). Atoms "P" whose head symbol also occurs as function symbol are
  15.242 +   rewritten to "term P = term True". Connectives and built-in predicates
  15.243 +   occurring at term level are replaced by new constants, and theorems
  15.244 +   specifying their meaning are added.
  15.245 +*)
  15.246 +local
  15.247 +  (** Add the marker symbols "term" and "formulas" to separate formulas and
  15.248 +      terms. **)
  15.249 +
  15.250 +  val connectives = map make_sconst [@{term True}, @{term False},
  15.251 +    @{term Not}, @{term "op &"}, @{term "op |"}, @{term "op -->"},
  15.252 +    @{term "op = :: bool => _"}]
  15.253 +
  15.254 +  fun note false c (ps, fs) = (insert (op =) c ps, fs)
  15.255 +    | note true c (ps, fs) = (ps, insert (op =) c fs)
  15.256 +
  15.257 +  val term_marker = SConst (@{const_name term}, Term.dummyT)
  15.258 +  val formula_marker = SConst (@{const_name formula}, Term.dummyT)
  15.259 +  fun mark f true t = f true t #>> app term_marker o single
  15.260 +    | mark f false t = f false t #>> app formula_marker o single
  15.261 +  fun mark' f false t = f true t #>> app term_marker o single
  15.262 +    | mark' f true t = f true t
  15.263 +  val mark_term = app term_marker o single
  15.264 +  fun lift_term_marker c ts =
  15.265 +    let val rem = (fn SApp (SConst (@{const_name term}, _), [t]) => t | t => t)
  15.266 +    in mark_term (SApp (c, map rem ts)) end
  15.267 +  fun is_term (SApp (SConst (@{const_name term}, _), _)) = true
  15.268 +    | is_term _ = false
  15.269 +
  15.270 +  fun either x = (fn y as SOME _ => y | _ => x)
  15.271 +  fun get_loc loc i t =
  15.272 +    (case t of
  15.273 +      SVar j => if i = j then SOME loc else NONE
  15.274 +    | SApp (SConst (@{const_name term}, _), us) => get_locs true i us
  15.275 +    | SApp (SConst (@{const_name formula}, _), us) => get_locs false i us
  15.276 +    | SApp (_, us) => get_locs loc i us
  15.277 +    | SLet (_, u1, u2) => either (get_loc true i u1) (get_loc loc (i+1) u2)
  15.278 +    | SQuant (_, vs, _, u) => get_loc loc (i + length vs) u)
  15.279 +  and get_locs loc i ts = fold (either o get_loc loc i) ts NONE
  15.280 +
  15.281 +  fun sep loc t =
  15.282 +    (case t of
  15.283 +      SVar i => pair t
  15.284 +    | SApp (c as SConst (@{const_name If}, _), u :: us) =>
  15.285 +        mark sep false u ##>> fold_map (sep loc) us #>> app c o (op ::)
  15.286 +    | SApp (c, us) =>
  15.287 +        if not loc andalso member (op =) connectives c
  15.288 +        then fold_map (sep loc) us #>> app c
  15.289 +        else note loc c #> fold_map (mark' sep loc) us #>> app c
  15.290 +    | SLet (v, u1, u2) =>
  15.291 +        sep loc u2 #-> (fn u2' =>
  15.292 +        mark sep (the (get_loc loc 0 u2')) u1 #>> (fn u1' =>
  15.293 +        SLet (v, u1', u2')))
  15.294 +    | SQuant (q, vs, ps, u) =>
  15.295 +        fold_map (fold_map_pat (mark sep true)) ps ##>>
  15.296 +        sep loc u #>> (fn (ps', u') =>
  15.297 +        SQuant (q, vs, ps', u')))
  15.298 +
  15.299 +  (** Rewrite atoms. **)
  15.300 +
  15.301 +  val unterm_rule = @{lemma "term x == x" by (simp add: term_def)}
  15.302 +  val unterm_conv = More_Conv.top_sweep_conv (K (Conv.rewr_conv unterm_rule))
  15.303 +
  15.304 +  val dest_word_type = (fn Type (@{type_name word}, [T]) => T | T => T)
  15.305 +  fun instantiate [] _ = I
  15.306 +    | instantiate (v :: _) T =
  15.307 +        Term.subst_TVars [(v, dest_word_type (Term.domain_type T))]
  15.308 +
  15.309 +  fun dest_alls (Const (@{const_name All}, _) $ Abs (_, _, t)) = dest_alls t
  15.310 +    | dest_alls t = t
  15.311 +  val dest_iff = (fn (Const (@{const_name iff}, _) $ t $ _ ) => t | t => t)
  15.312 +  val dest_eq = (fn (Const (@{const_name "op ="}, _) $ t $ _ ) => t | t => t)
  15.313 +  val dest_not = (fn (@{term Not} $ t) => t | t => t)
  15.314 +  val head_of = HOLogic.dest_Trueprop #> dest_alls #> dest_iff #> dest_not #>
  15.315 +    dest_eq #> Term.head_of
  15.316 +
  15.317 +  fun prepare ctxt thm =
  15.318 +    let
  15.319 +      val rule = Conv.fconv_rule (unterm_conv ctxt) thm
  15.320 +      val prop = Thm.prop_of thm
  15.321 +      val inst = instantiate (Term.add_tvar_names prop [])
  15.322 +      fun inst_for T = (singleton intermediate (inst T prop), rule)
  15.323 +    in (make_sconst (head_of (Thm.prop_of rule)), inst_for) end
  15.324 +
  15.325 +  val logicals = map (prepare @{context})
  15.326 +    @{lemma 
  15.327 +      "~ holds False"
  15.328 +      "ALL p. holds (~ p) iff (~ holds p)"
  15.329 +      "ALL p q. holds (p & q) iff (holds p & holds q)"
  15.330 +      "ALL p q. holds (p | q) iff (holds p | holds q)"
  15.331 +      "ALL p q. holds (p --> q) iff (holds p --> holds q)"
  15.332 +      "ALL p q. holds (p iff q) iff (holds p iff holds q)"
  15.333 +      "ALL p q. holds (p = q) iff (p = q)"
  15.334 +      "ALL (a::int) b. holds (a < b) iff (a < b)"
  15.335 +      "ALL (a::int) b. holds (a <= b) iff (a <= b)"
  15.336 +      "ALL (a::real) b. holds (a < b) iff (a < b)"
  15.337 +      "ALL (a::real) b. holds (a <= b) iff (a <= b)"
  15.338 +      "ALL (a::'a::len0 word) b. holds (a < b) iff (a < b)"
  15.339 +      "ALL (a::'a::len0 word) b. holds (a <= b) iff (a <= b)"
  15.340 +      "ALL a b. holds (a <s b) iff (a <s b)"
  15.341 +      "ALL a b. holds (a <=s b) iff (a <=s b)"
  15.342 +      by (simp_all add: term_def iff_def)}
  15.343 +
  15.344 +  fun is_instance thy (SConst (n, T), SConst (m, U)) =
  15.345 +        (n = m) andalso Sign.typ_instance thy (T, U)
  15.346 +    | is_instance _ _ = false
  15.347 +
  15.348 +  fun lookup_logical thy (c as SConst (_, T)) =
  15.349 +        AList.lookup (is_instance thy) logicals c
  15.350 +        |> Option.map (fn inst_for => inst_for T)
  15.351 +    | lookup_logical _ _ = NONE
  15.352 +
  15.353 +  val s_eq = make_sconst @{term "op = :: bool => _"}
  15.354 +  val s_True = mark_term (SApp (make_sconst @{term True}, []))
  15.355 +  fun holds (SApp (c, ts)) = SApp (s_eq, [lift_term_marker c ts, s_True])
  15.356 +    | holds t = SApp (s_eq, [mark_term t, s_True])
  15.357 +
  15.358 +  val rewr_iff = (fn
  15.359 +      SConst (@{const_name "op ="}, T as @{typ "bool => bool => bool"}) =>
  15.360 +        SConst (@{const_name iff}, T)
  15.361 +    | c => c)
  15.362 +
  15.363 +  fun rewrite ls =
  15.364 +    let
  15.365 +      fun rewr env loc t =
  15.366 +        (case t of
  15.367 +          SVar i => if not loc andalso nth env i then holds t else t
  15.368 +        | SApp (c as SConst (@{const_name term}, _), [u]) =>
  15.369 +            SApp (c, [rewr env true u])
  15.370 +        | SApp (c as SConst (@{const_name formula}, _), [u]) =>
  15.371 +            SApp (c, [rewr env false u])
  15.372 +        | SApp (c, us) =>
  15.373 +            let val f = if not loc andalso member (op =) ls c then holds else I
  15.374 +            in f (SApp (rewr_iff c, map (rewr env loc) us)) end
  15.375 +        | SLet (v, u1, u2) =>
  15.376 +            SLet (v, rewr env loc u1, rewr (is_term u1 :: env) loc u2)
  15.377 +        | SQuant (q, vs, ps, u) =>
  15.378 +            let val e = replicate (length vs) true @ env
  15.379 +            in SQuant (q, vs, map (map_pat (rewr e loc)) ps, rewr e loc u) end)
  15.380 +    in map (rewr [] false) end
  15.381 +in
  15.382 +fun separate thy ts =
  15.383 +  let
  15.384 +    val (ts', (ps, fs)) = fold_map (sep false) ts ([], [])
  15.385 +    val eq_name = (fn
  15.386 +        (SConst (n, _), SConst (m, _)) => n = m
  15.387 +      | (SFree (n, _), SFree (m, _)) => n = m
  15.388 +      | _ => false)
  15.389 +    val ls = filter (member eq_name fs) ps
  15.390 +    val (us, thms) = split_list (map_filter (lookup_logical thy) fs)
  15.391 +  in (thms, us @ rewrite ls ts') end
  15.392 +end
  15.393 +
  15.394 +
  15.395 +(* Collect the signature of intermediate terms, identify built-in symbols,
  15.396 +   rename uninterpreted symbols and types, make bound variables unique.
  15.397 +   We require @{term distinct} to be a built-in constant of the SMT solver.
  15.398 +*)
  15.399 +local
  15.400 +  fun empty_nctxt p = (p, 1)
  15.401 +  fun make_nctxt (pT, pf, pp) = (empty_nctxt pT, empty_nctxt (pf, pp))
  15.402 +  fun fresh_name (p, i) = (p ^ string_of_int i, (p, i+1))
  15.403 +  fun fresh_typ (nT, nfp) = fresh_name nT ||> (fn nT' => (nT', nfp))
  15.404 +  fun fresh_fun loc (nT, ((pf, pp), i)) =
  15.405 +    let val p = if loc then pf else pp
  15.406 +    in fresh_name (p, i) ||> (fn (_, i') => (nT, ((pf, pp), i'))) end
  15.407 +
  15.408 +  val empty_sign = (Typtab.empty, Termtab.empty, Termtab.empty)
  15.409 +  fun lookup_typ (typs, _, _) = Typtab.lookup typs
  15.410 +  fun lookup_fun true (_, funs, _) = Termtab.lookup funs
  15.411 +    | lookup_fun false (_, _, preds) = Termtab.lookup preds
  15.412 +  fun add_typ x (typs, funs, preds) = (Typtab.update x typs, funs, preds)
  15.413 +  fun add_fun true x (typs, funs, preds) = (typs, Termtab.update x funs, preds)
  15.414 +    | add_fun false x (typs, funs, preds) = (typs, funs, Termtab.update x preds)
  15.415 +  fun make_sign (typs, funs, preds) = Sign {
  15.416 +    typs = map snd (Typtab.dest typs),
  15.417 +    funs = map snd (Termtab.dest funs),
  15.418 +    preds = map (apsnd fst o snd) (Termtab.dest preds) }
  15.419 +  fun make_rtab (typs, funs, preds) =
  15.420 +    let
  15.421 +      val rTs = Typtab.dest typs |> map swap |> Symtab.make
  15.422 +      val rts = Termtab.dest funs @ Termtab.dest preds
  15.423 +        |> map (apfst fst o swap) |> Symtab.make
  15.424 +    in Recon {typs=rTs, terms=rts} end
  15.425 +
  15.426 +  fun either f g x = (case f x of NONE => g x | y => y)
  15.427 +
  15.428 +  fun rep_typ (Builtins {builtin_typ, ...}) T (st as (vars, ns, sgn)) =
  15.429 +    (case either builtin_typ (lookup_typ sgn) T of
  15.430 +      SOME n => (n, st)
  15.431 +    | NONE =>
  15.432 +        let val (n, ns') = fresh_typ ns
  15.433 +        in (n, (vars, ns', add_typ (T, n) sgn)) end)
  15.434 +
  15.435 +  fun rep_var bs (n, T) (vars, ns, sgn) =
  15.436 +    let val (n', vars') = fresh_name vars
  15.437 +    in (vars', ns, sgn) |> rep_typ bs T |>> pair n' end
  15.438 +
  15.439 +  fun rep_fun bs loc t T i (st as (_, _, sgn0)) =
  15.440 +    (case lookup_fun loc sgn0 t of
  15.441 +      SOME (n, _) => (n, st)
  15.442 +    | NONE =>
  15.443 +        let
  15.444 +          val (Us, U) = dest_funT i T
  15.445 +          val (uns, (vars, ns, sgn)) =
  15.446 +            st |> fold_map (rep_typ bs) Us ||>> rep_typ bs U
  15.447 +          val (n, ns') = fresh_fun loc ns
  15.448 +        in (n, (vars, ns', add_fun loc (t, (n, uns)) sgn)) end)
  15.449 +
  15.450 +  fun rep_num (bs as Builtins {builtin_num, ...}) (i, T) st =
  15.451 +    (case builtin_num (i, T) of
  15.452 +      SOME n => (n, st)
  15.453 +    | NONE => rep_fun bs true (HOLogic.mk_number T i) T 0 st)
  15.454 +in
  15.455 +fun signature_of prefixes markers builtins thy ts =
  15.456 +  let
  15.457 +    val Prefixes {var_prefix, typ_prefix, fun_prefix, pred_prefix} = prefixes
  15.458 +    val Markers {formula_marker, term_marker} = markers
  15.459 +    val Builtins {builtin_fun, ...} = builtins
  15.460 +
  15.461 +    fun sign loc t =
  15.462 +      (case t of
  15.463 +        SVar i => pair (SVar i)
  15.464 +      | SApp (c as SConst (@{const_name term}, _), [u]) =>
  15.465 +          sign true u #>> app term_marker o single
  15.466 +      | SApp (c as SConst (@{const_name formula}, _), [u]) =>
  15.467 +          sign false u #>> app formula_marker o single
  15.468 +      | SApp (SConst (c as (_, T)), ts) =>
  15.469 +          (case builtin_lookup (builtin_fun loc) thy c ts of
  15.470 +            SOME (n, ts') => fold_map (sign loc) ts' #>> app n
  15.471 +          | NONE =>
  15.472 +              rep_fun builtins loc (Const c) T (length ts) ##>>
  15.473 +              fold_map (sign loc) ts #>> SApp)
  15.474 +      | SApp (SFree (c as (_, T)), ts) =>
  15.475 +          rep_fun builtins loc (Free c) T (length ts) ##>>
  15.476 +          fold_map (sign loc) ts #>> SApp
  15.477 +      | SApp (SNum n, _) => rep_num builtins n #>> (fn n => SApp (n, []))
  15.478 +      | SLet (v, u1, u2) =>
  15.479 +          rep_var builtins v #-> (fn v' =>
  15.480 +          sign loc u1 ##>> sign loc u2 #>> (fn (u1', u2') =>
  15.481 +          SLet (v', u1', u2')))
  15.482 +      | SQuant (q, vs, ps, u) =>
  15.483 +          fold_map (rep_var builtins) vs ##>>
  15.484 +          fold_map (fold_map_pat (sign loc)) ps ##>>
  15.485 +          sign loc u #>> (fn ((vs', ps'), u') =>
  15.486 +          SQuant (q, vs', ps', u')))
  15.487 +  in
  15.488 +    (empty_nctxt var_prefix, make_nctxt (typ_prefix, fun_prefix, pred_prefix),
  15.489 +      empty_sign)
  15.490 +    |> fold_map (sign false) ts
  15.491 +    |> (fn (us, (_, _, sgn)) => (make_rtab sgn, (make_sign sgn, us)))
  15.492 +  end
  15.493 +end
  15.494 +
  15.495 +
  15.496 +(* Combination of all translation functions and invocation of serialization. *)
  15.497 +
  15.498 +fun translate config thy thms stream =
  15.499 +  let val Config {strict, prefixes, markers, builtins, serialize} = config
  15.500 +  in
  15.501 +    map Thm.prop_of thms
  15.502 +    |> SMT_Monomorph.monomorph thy
  15.503 +    |> intermediate
  15.504 +    |> (if strict then separate thy else pair [])
  15.505 +    ||>> signature_of prefixes markers builtins thy
  15.506 +    ||> (fn (sgn, ts) => serialize sgn ts stream)
  15.507 +    |> (fn ((thms', rtab), _) => (rtab, thms' @ thms))
  15.508 +  end
  15.509 +
  15.510 +end
    16.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.2 +++ b/src/HOL/SMT/Tools/smtlib_interface.ML	Fri Sep 18 18:13:19 2009 +0200
    16.3 @@ -0,0 +1,168 @@
    16.4 +(*  Title:      HOL/SMT/Tools/smtlib_interface.ML
    16.5 +    Author:     Sascha Boehme, TU Muenchen
    16.6 +
    16.7 +Interface to SMT solvers based on the SMT-LIB format.
    16.8 +*)
    16.9 +
   16.10 +signature SMTLIB_INTERFACE =
   16.11 +sig
   16.12 +  val basic_builtins: SMT_Translate.builtins
   16.13 +  val default_attributes: string list
   16.14 +  val gen_interface: SMT_Translate.builtins -> string list ->
   16.15 +    SMT_Solver.interface
   16.16 +  val interface: SMT_Solver.interface
   16.17 +end
   16.18 +
   16.19 +structure SMTLIB_Interface: SMTLIB_INTERFACE =
   16.20 +struct
   16.21 +
   16.22 +structure T = SMT_Translate
   16.23 +
   16.24 +
   16.25 +(* built-in types, functions and predicates *)
   16.26 +
   16.27 +val builtin_typ = (fn
   16.28 +    @{typ int} => SOME "Int"
   16.29 +  | @{typ real} => SOME "Real"
   16.30 +  | _ => NONE)
   16.31 +
   16.32 +val builtin_num = (fn
   16.33 +    (i, @{typ int}) => SOME (string_of_int i)
   16.34 +  | (i, @{typ real}) => SOME (string_of_int i ^ ".0")
   16.35 +  | _ => NONE)
   16.36 +
   16.37 +val builtin_funcs = T.builtin_make [
   16.38 +  (@{term If}, "ite"),
   16.39 +  (@{term "uminus :: int => _"}, "~"),
   16.40 +  (@{term "plus :: int => _"}, "+"),
   16.41 +  (@{term "minus :: int => _"}, "-"),
   16.42 +  (@{term "times :: int => _"}, "*"),
   16.43 +  (@{term "uminus :: real => _"}, "~"),
   16.44 +  (@{term "plus :: real => _"}, "+"),
   16.45 +  (@{term "minus :: real => _"}, "-"),
   16.46 +  (@{term "times :: real => _"}, "*") ]
   16.47 +
   16.48 +val builtin_preds = T.builtin_make [
   16.49 +  (@{term True}, "true"),
   16.50 +  (@{term False}, "false"),
   16.51 +  (@{term Not}, "not"),
   16.52 +  (@{term "op &"}, "and"),
   16.53 +  (@{term "op |"}, "or"),
   16.54 +  (@{term "op -->"}, "implies"),
   16.55 +  (@{term "op iff"}, "iff"),
   16.56 +  (@{term If}, "if_then_else"),
   16.57 +  (@{term distinct}, "distinct"),
   16.58 +  (@{term "op ="}, "="),
   16.59 +  (@{term "op < :: int => _"}, "<"),
   16.60 +  (@{term "op <= :: int => _"}, "<="),
   16.61 +  (@{term "op < :: real => _"}, "<"),
   16.62 +  (@{term "op <= :: real => _"}, "<=") ]
   16.63 +
   16.64 +
   16.65 +(* serialization *)
   16.66 +
   16.67 +fun wr s stream = (TextIO.output (stream, s); stream)
   16.68 +fun wr_line f = f #> wr "\n"
   16.69 +
   16.70 +fun sep f = wr " " #> f
   16.71 +fun par f = sep (wr "(" #> f #> wr ")")
   16.72 +
   16.73 +fun wr1 s = sep (wr s)
   16.74 +fun wrn f n = (fn [] => wr1 n | ts => par (wr n #> fold f ts))
   16.75 +fun ins s f = (fn [] => I | x::xs => f x #> fold (fn x => wr1 s #> f x) xs)
   16.76 +
   16.77 +val term_marker = "__term"
   16.78 +val formula_marker = "__form"
   16.79 +fun dest_marker (T.SApp ("__term", [t])) = SOME (true, t)
   16.80 +  | dest_marker (T.SApp ("__form", [t])) = SOME (false, t)
   16.81 +  | dest_marker _ = NONE
   16.82 +
   16.83 +val tvar = prefix "?"
   16.84 +val fvar = prefix "$"
   16.85 +
   16.86 +fun wr_expr loc env t =
   16.87 +  (case t of
   16.88 +    T.SVar i => wr1 (nth env i)
   16.89 +  | T.SApp (n, ts) =>
   16.90 +      (case dest_marker t of
   16.91 +        SOME (loc', t') => wr_expr loc' env t'
   16.92 +      | NONE => wrn (wr_expr loc env) n ts)
   16.93 +  | T.SLet ((v, _), t1, t2) =>
   16.94 +      if loc then raise TERM ("SMTLIB: let expression in term", [])
   16.95 +      else
   16.96 +        let
   16.97 +          val (loc', t1') = the (dest_marker t1)
   16.98 +          val (kind, v') = if loc' then ("let", tvar v)  else ("flet", fvar v)
   16.99 +        in
  16.100 +          par (wr kind #> par (wr v' #> wr_expr loc' env t1') #>
  16.101 +            wr_expr loc (v' :: env) t2)
  16.102 +        end
  16.103 +  | T.SQuant (q, vs, ps, b) =>
  16.104 +      let
  16.105 +        val wr_quant = wr o (fn T.SForall => "forall" | T.SExists => "exists")
  16.106 +        fun wr_var (n, s) = par (wr (tvar n) #> wr1 s)
  16.107 +
  16.108 +        val wre = wr_expr loc (map (tvar o fst) (rev vs) @ env)
  16.109 +
  16.110 +        fun wrp s ts = wr1 (":" ^ s ^ "{") #> ins "," wre ts #> wr1 "}"
  16.111 +        fun wr_pat (T.SPat ts) = wrp "pat" ts
  16.112 +          | wr_pat (T.SNoPat ts) = wrp "nopat" ts
  16.113 +      in par (wr_quant q #> fold wr_var vs #> wre b #> fold wr_pat ps) end)
  16.114 +
  16.115 +fun serialize attributes (T.Sign {typs, funs, preds}) ts stream =
  16.116 +  let
  16.117 +    fun wr_decl (n, Ts) = wr_line (sep (par (wr n #> fold wr1 Ts)))
  16.118 +  in
  16.119 +    stream
  16.120 +    |> wr_line (wr "(benchmark Isabelle")
  16.121 +    |> fold (wr_line o wr) attributes
  16.122 +    |> length typs > 0 ?
  16.123 +         wr_line (wr ":extrasorts" #> par (fold wr1 typs))
  16.124 +    |> length funs > 0 ? (
  16.125 +         wr_line (wr ":extrafuns (") #>
  16.126 +         fold (wr_decl o apsnd (fn (Ts, T) => Ts @ [T])) funs #>
  16.127 +         wr_line (wr " )"))
  16.128 +    |> length preds > 0 ? (
  16.129 +         wr_line (wr ":extrapreds (") #>
  16.130 +         fold wr_decl preds #>
  16.131 +         wr_line (wr " )"))
  16.132 +    |> fold (fn t => wr ":assumption" #> wr_line (wr_expr false [] t)) ts
  16.133 +    |> wr_line (wr ":formula true")
  16.134 +    |> wr_line (wr ")")
  16.135 +    |> K ()
  16.136 +  end
  16.137 +
  16.138 +
  16.139 +(* SMT solver interface using the SMT-LIB input format *)
  16.140 +
  16.141 +val basic_builtins = T.Builtins {
  16.142 +  builtin_typ = builtin_typ,
  16.143 +  builtin_num = builtin_num,
  16.144 +  builtin_fun = (fn true => builtin_funcs | false => builtin_preds) }
  16.145 +
  16.146 +val default_attributes = [":logic AUFLIRA", ":status unknown"]
  16.147 +
  16.148 +fun gen_interface builtins attributes = SMT_Solver.Interface {
  16.149 +  normalize = [
  16.150 +    SMT_Normalize.RewriteTrivialLets,
  16.151 +    SMT_Normalize.RewriteNegativeNumerals,
  16.152 +    SMT_Normalize.RewriteNaturalNumbers,
  16.153 +    SMT_Normalize.AddAbsMinMaxRules,
  16.154 +    SMT_Normalize.AddPairRules,
  16.155 +    SMT_Normalize.AddFunUpdRules ],
  16.156 +  translate = T.Config {
  16.157 +    strict = true,
  16.158 +    prefixes = T.Prefixes {
  16.159 +      var_prefix = "x",
  16.160 +      typ_prefix = "T",
  16.161 +      fun_prefix = "uf_",
  16.162 +      pred_prefix = "up_" },
  16.163 +    markers = T.Markers {
  16.164 +      term_marker = term_marker,
  16.165 +      formula_marker = formula_marker },
  16.166 +    builtins = builtins,
  16.167 +    serialize = serialize attributes }}
  16.168 +
  16.169 +val interface = gen_interface basic_builtins default_attributes
  16.170 +
  16.171 +end
    17.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.2 +++ b/src/HOL/SMT/Tools/yices_solver.ML	Fri Sep 18 18:13:19 2009 +0200
    17.3 @@ -0,0 +1,52 @@
    17.4 +(*  Title:      HOL/SMT/Tools/yices_solver.ML
    17.5 +    Author:     Sascha Boehme, TU Muenchen
    17.6 +
    17.7 +Interface of the SMT solver Yices.
    17.8 +*)
    17.9 +
   17.10 +signature YICES_SOLVER =
   17.11 +sig
   17.12 +  val setup: theory -> theory
   17.13 +end
   17.14 +
   17.15 +structure Yices_Solver: YICES_SOLVER =
   17.16 +struct
   17.17 +
   17.18 +val solver_name = "yices"
   17.19 +val env_var = "YICES_SOLVER"
   17.20 +
   17.21 +val options = ["--evidence", "--smtlib"]
   17.22 +
   17.23 +fun cex_kind true = "Counterexample"
   17.24 +  | cex_kind false = "Possible counterexample"
   17.25 +
   17.26 +fun raise_cex real ctxt rtab ls =
   17.27 +  let val p = Pretty.big_list (cex_kind real ^ " found:") (map Pretty.str ls)
   17.28 +  in error (Pretty.string_of p) end
   17.29 +
   17.30 +structure S = SMT_Solver
   17.31 +
   17.32 +fun core_oracle (SMT_Solver.ProofData {context, output, recon, ...}) =
   17.33 +  let
   17.34 +    val empty_line = (fn "" => true | _ => false)
   17.35 +    val split_first = (fn [] => ("", []) | l :: ls => (l, ls))
   17.36 +    val (l, ls) = split_first (dropwhile empty_line output)
   17.37 +  in
   17.38 +    if String.isPrefix "unsat" l then @{cprop False}
   17.39 +    else if String.isPrefix "sat" l then raise_cex true context recon ls
   17.40 +    else if String.isPrefix "unknown" l then raise_cex false context recon ls
   17.41 +    else error (solver_name ^ " failed")
   17.42 +  end
   17.43 +
   17.44 +fun smtlib_solver oracle _ =
   17.45 +  SMT_Solver.SolverConfig {
   17.46 +    name = {env_var=env_var, remote_name=solver_name},
   17.47 +    interface = SMTLIB_Interface.interface,
   17.48 +    arguments = options,
   17.49 +    reconstruct = oracle }
   17.50 +
   17.51 +val setup =
   17.52 +  Thm.add_oracle (Binding.name solver_name, core_oracle) #-> (fn (_, oracle) =>
   17.53 +  SMT_Solver.add_solver (solver_name, smtlib_solver oracle))
   17.54 +
   17.55 +end
    18.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    18.2 +++ b/src/HOL/SMT/Tools/z3_interface.ML	Fri Sep 18 18:13:19 2009 +0200
    18.3 @@ -0,0 +1,98 @@
    18.4 +(*  Title:      HOL/SMT/Tools/z3_interface.ML
    18.5 +    Author:     Sascha Boehme, TU Muenchen
    18.6 +
    18.7 +Interface to Z3 based on a relaxed version of SMT-LIB.
    18.8 +*)
    18.9 +
   18.10 +signature Z3_INTERFACE =
   18.11 +sig
   18.12 +  val interface: SMT_Solver.interface
   18.13 +end
   18.14 +
   18.15 +structure Z3_Interface: Z3_INTERFACE =
   18.16 +struct
   18.17 +
   18.18 +structure T = SMT_Translate
   18.19 +
   18.20 +fun mk_name1 n i = n ^ "[" ^ string_of_int i ^ "]"
   18.21 +fun mk_name2 n i j = n ^ "[" ^ string_of_int i ^ ":" ^ string_of_int j ^ "]"
   18.22 +
   18.23 +val builtin_typ = (fn
   18.24 +    @{typ int} => SOME "Int"
   18.25 +  | @{typ real} => SOME "Real"
   18.26 +  | Type (@{type_name word}, [T]) =>
   18.27 +      Option.map (mk_name1 "BitVec") (try T.dest_binT T)
   18.28 +  | _ => NONE)
   18.29 +
   18.30 +val builtin_num = (fn
   18.31 +    (i, @{typ int}) => SOME (string_of_int i)
   18.32 +  | (i, @{typ real}) => SOME (string_of_int i ^ ".0")
   18.33 +  | (i, Type (@{type_name word}, [T])) =>
   18.34 +      Option.map (mk_name1 ("bv" ^ string_of_int i)) (try T.dest_binT T)
   18.35 +  | _ => NONE)
   18.36 +
   18.37 +val builtin_funcs = T.builtin_make [
   18.38 +  (@{term If}, "ite"),
   18.39 +  (@{term "uminus :: int => _"}, "~"),
   18.40 +  (@{term "plus :: int => _"}, "+"),
   18.41 +  (@{term "minus :: int => _"}, "-"),
   18.42 +  (@{term "times :: int => _"}, "*"),
   18.43 +  (@{term "op div :: int => _"}, "div"),
   18.44 +  (@{term "op mod :: int => _"}, "mod"),
   18.45 +  (@{term "op rem"}, "rem"),
   18.46 +  (@{term "uminus :: real => _"}, "~"),
   18.47 +  (@{term "plus :: real => _"}, "+"),
   18.48 +  (@{term "minus :: real => _"}, "-"),
   18.49 +  (@{term "times :: real => _"}, "*"),
   18.50 +  (@{term "op / :: real => _"}, "/"),
   18.51 +  (@{term "bitNOT :: 'a::len0 word => _"}, "bvnot"),
   18.52 +  (@{term "op AND :: 'a::len0 word => _"}, "bvand"),
   18.53 +  (@{term "op OR :: 'a::len0 word => _"}, "bvor"),
   18.54 +  (@{term "op XOR :: 'a::len0 word => _"}, "bvxor"),
   18.55 +  (@{term "uminus :: 'a::len0 word => _"}, "bvneg"),
   18.56 +  (@{term "op + :: 'a::len0 word => _"}, "bvadd"),
   18.57 +  (@{term "op - :: 'a::len0 word => _"}, "bvsub"),
   18.58 +  (@{term "op * :: 'a::len0 word => _"}, "bvmul"),
   18.59 +  (@{term "op div :: 'a::len0 word => _"}, "bvudiv"),
   18.60 +  (@{term "op mod :: 'a::len0 word => _"}, "bvurem"),
   18.61 +  (@{term "op sdiv"}, "bvsdiv"),
   18.62 +  (@{term "op smod"}, "bvsmod"),
   18.63 +  (@{term "op srem"}, "bvsrem"),
   18.64 +  (@{term word_cat}, "concat"),
   18.65 +  (@{term bv_shl}, "bvshl"),
   18.66 +  (@{term bv_lshr}, "bvlshr"),
   18.67 +  (@{term bv_ashr}, "bvashr")]
   18.68 +  |> T.builtin_add (@{term slice}, T.bv_extract (mk_name2 "extract"))
   18.69 +  |> T.builtin_add (@{term ucast}, T.bv_extend (mk_name1 "zero_extend"))
   18.70 +  |> T.builtin_add (@{term scast}, T.bv_extend (mk_name1 "sign_extend"))
   18.71 +  |> T.builtin_add (@{term word_rotl}, T.bv_rotate (mk_name1 "rotate_left"))
   18.72 +  |> T.builtin_add (@{term word_rotr}, T.bv_rotate (mk_name1 "rotate_right"))
   18.73 +
   18.74 +val builtin_preds = T.builtin_make [
   18.75 +  (@{term True}, "true"),
   18.76 +  (@{term False}, "false"),
   18.77 +  (@{term Not}, "not"),
   18.78 +  (@{term "op &"}, "and"),
   18.79 +  (@{term "op |"}, "or"),
   18.80 +  (@{term "op -->"}, "implies"),
   18.81 +  (@{term "op iff"}, "iff"),
   18.82 +  (@{term If}, "if_then_else"),
   18.83 +  (@{term distinct}, "distinct"),
   18.84 +  (@{term "op ="}, "="),
   18.85 +  (@{term "op < :: int => _"}, "<"),
   18.86 +  (@{term "op <= :: int => _"}, "<="),
   18.87 +  (@{term "op < :: real => _"}, "<"),
   18.88 +  (@{term "op <= :: real => _"}, "<="),
   18.89 +  (@{term "op < :: 'a::len0 word => _"}, "bvult"),
   18.90 +  (@{term "op <= :: 'a::len0 word => _"}, "bvule"),
   18.91 +  (@{term word_sless}, "bvslt"),
   18.92 +  (@{term word_sle}, "bvsle")]
   18.93 +
   18.94 +val builtins = T.Builtins {
   18.95 +  builtin_typ = builtin_typ,
   18.96 +  builtin_num = builtin_num,
   18.97 +  builtin_fun = (fn true => builtin_funcs | false => builtin_preds) }
   18.98 +
   18.99 +val interface = SMTLIB_Interface.gen_interface builtins []
  18.100 +
  18.101 +end
    19.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    19.2 +++ b/src/HOL/SMT/Tools/z3_model.ML	Fri Sep 18 18:13:19 2009 +0200
    19.3 @@ -0,0 +1,159 @@
    19.4 +(*  Title:      HOL/SMT/Tools/z3_model.ML
    19.5 +    Author:     Sascha Boehme and Philipp Meyer, TU Muenchen
    19.6 +
    19.7 +Parser for counterexamples generated by Z3.
    19.8 +*)
    19.9 +
   19.10 +signature Z3_MODEL =
   19.11 +sig
   19.12 +  val parse_counterex: SMT_Translate.recon -> string list -> term list
   19.13 +end
   19.14 +
   19.15 +structure Z3_Model: Z3_MODEL =
   19.16 +struct
   19.17 +
   19.18 +(* parsing primitives *)
   19.19 +
   19.20 +fun lift f (x, y) = apsnd (pair x) (f y)
   19.21 +fun lift' f v (x, y) = apsnd (rpair y) (f v x)
   19.22 +
   19.23 +fun $$ s = lift (Scan.$$ s)
   19.24 +fun this s = lift (Scan.this_string s)
   19.25 +
   19.26 +fun par scan = $$ "(" |-- scan --| $$ ")"
   19.27 +
   19.28 +val digit = (fn
   19.29 +  "0" => SOME 0 | "1" => SOME 1 | "2" => SOME 2 | "3" => SOME 3 |
   19.30 +  "4" => SOME 4 | "5" => SOME 5 | "6" => SOME 6 | "7" => SOME 7 |
   19.31 +  "8" => SOME 8 | "9" => SOME 9 | _ => NONE)
   19.32 +
   19.33 +val nat_num = Scan.repeat1 (Scan.some digit) >>
   19.34 +  (fn ds => fold (fn d => fn i => i * 10 + d) ds 0)
   19.35 +val int_num = Scan.optional (Scan.$$ "-" >> K (fn i => ~i)) I :|--
   19.36 +  (fn sign => nat_num >> sign)
   19.37 +
   19.38 +val is_char = Symbol.is_ascii_letter orf Symbol.is_ascii_digit orf
   19.39 +  member (op =) (explode "_+*-/%~=<>$&|?!.@^#")
   19.40 +val name = Scan.many1 is_char >> implode
   19.41 +
   19.42 +
   19.43 +(* parsing counterexamples *)
   19.44 +
   19.45 +datatype context = Context of {
   19.46 +  ttab: term Symtab.table,
   19.47 +  nctxt: Name.context,
   19.48 +  vtab: term Inttab.table }
   19.49 +
   19.50 +fun make_context (ttab, nctxt, vtab) =
   19.51 +  Context {ttab=ttab, nctxt=nctxt, vtab=vtab}
   19.52 +
   19.53 +fun empty_context (SMT_Translate.Recon {terms, ...}) =
   19.54 +  let
   19.55 +    val ns = Symtab.fold (Term.add_free_names o snd) terms []
   19.56 +    val nctxt = Name.make_context ns
   19.57 +  in make_context (terms, nctxt, Inttab.empty) end
   19.58 +
   19.59 +fun map_context f (Context {ttab, nctxt, vtab}) =
   19.60 +  make_context (f (ttab, nctxt, vtab))
   19.61 +
   19.62 +fun fresh_name (cx as Context {nctxt, ...}) =
   19.63 +  let val (n, nctxt') = yield_singleton Name.variants "" nctxt
   19.64 +  in (n, map_context (fn (ttab, _, vtab) => (ttab, nctxt', vtab)) cx) end
   19.65 +
   19.66 +fun ident name (cx as Context {ttab, ...}) = 
   19.67 +  (case Symtab.lookup ttab name of
   19.68 +    SOME t => (t, cx)
   19.69 +  | NONE =>
   19.70 +      let val (n, cx') = fresh_name cx
   19.71 +      in (Free (n, Term.dummyT), cx) end)
   19.72 +
   19.73 +fun set_value t i = map_context (fn (ttab, nctxt, vtab) =>
   19.74 +  (ttab, nctxt, Inttab.update (i, t) vtab))
   19.75 +
   19.76 +fun get_value T i (cx as Context {vtab, ...}) =
   19.77 +  (case Inttab.lookup vtab i of
   19.78 +    SOME t => (t, cx)
   19.79 +  | _ => cx |> fresh_name |-> (fn n =>
   19.80 +      let val t = Free (n, T)
   19.81 +      in set_value t i #> pair t end))
   19.82 +
   19.83 +
   19.84 +fun space s = lift (Scan.many Symbol.is_ascii_blank) s
   19.85 +fun spaced p = p --| space
   19.86 +
   19.87 +val key = spaced (lift name) #-> lift' ident
   19.88 +val mapping = spaced (this "->")
   19.89 +fun in_braces p = spaced ($$ "{") |-- p --| spaced ($$ "}")
   19.90 +
   19.91 +val bool_expr =
   19.92 +  this "true" >> K @{term True} ||
   19.93 +  this "false" >> K @{term False}
   19.94 +
   19.95 +fun number_expr T =
   19.96 +  let
   19.97 +    val num = lift int_num >> HOLogic.mk_number T
   19.98 +    fun frac n d = Const (@{const_name divide}, T --> T --> T) $ n $ d
   19.99 +  in num :|-- (fn n => Scan.optional ($$ "/" |-- num >> frac n) n) end
  19.100 +
  19.101 +val value = this "val!" |-- lift nat_num
  19.102 +fun value_expr T = value #-> lift' (get_value T)
  19.103 +
  19.104 +val domT = Term.domain_type
  19.105 +val ranT = Term.range_type
  19.106 +fun const_array T t = Abs ("x", T, t)
  19.107 +fun upd_array T ((a, t), u) =
  19.108 +  Const (@{const_name fun_upd}, [T, domT T, ranT T] ---> T) $ a $ t $ u
  19.109 +fun array_expr T st = if not (can domT T) then Scan.fail st else st |> (
  19.110 +  par (spaced (this "const") |-- expr (ranT T)) >> const_array (domT T) ||
  19.111 +  par (spaced (this "store") |-- spaced (array_expr T) --
  19.112 +    expr (Term.domain_type T) -- expr (Term.range_type T)) >> upd_array T)
  19.113 +
  19.114 +and expr T st =
  19.115 +  spaced (bool_expr || number_expr T || value_expr T || array_expr T) st
  19.116 +
  19.117 +fun const_val t =
  19.118 +  let fun rep u = spaced value #-> apfst o set_value u #> pair []
  19.119 +  in
  19.120 +    if can HOLogic.dest_number t then rep t
  19.121 +    else if t = @{term TT} then rep @{term True}
  19.122 +    else expr (Term.fastype_of t) >> (fn u => [HOLogic.mk_eq (t, u)])
  19.123 +  end
  19.124 +
  19.125 +fun func_value T = mapping |-- expr T
  19.126 +
  19.127 +fun first_pat T =
  19.128 +  let
  19.129 +    fun args T = if not (can domT T) then Scan.succeed [] else
  19.130 +      expr (domT T) ::: args (ranT T)
  19.131 +    fun value ts = func_value (snd (SMT_Translate.dest_funT (length ts) T))
  19.132 +  in args T :-- value end
  19.133 +
  19.134 +fun func_pat (Ts, T) = fold_map expr Ts -- func_value T
  19.135 +fun else_pat (Ts, T) =
  19.136 +  let fun else_arg T cx = cx |> fresh_name |>> (fn n => Free (n, T))
  19.137 +  in
  19.138 +    fold_map (lift' else_arg) Ts ##>>
  19.139 +    spaced (this "else") |-- func_value T
  19.140 +  end
  19.141 +fun next_pats T (fts as (ts, _)) =
  19.142 +  let val Tps = SMT_Translate.dest_funT (length ts) T
  19.143 +  in Scan.repeat (func_pat Tps) @@@ (else_pat Tps >> single) >> cons fts end
  19.144 +
  19.145 +fun mk_def' f (ts, t) = HOLogic.mk_eq (Term.list_comb (f, ts), t)
  19.146 +fun mk_def (Const (@{const_name apply}, _)) (u :: us, t) = mk_def' u (us, t)
  19.147 +  | mk_def f (ts, t) = mk_def' f (ts, t)
  19.148 +fun func_pats t =
  19.149 +  let val T = Term.fastype_of t
  19.150 +  in first_pat T :|-- next_pats T >> map (mk_def t) end
  19.151 +
  19.152 +val assign =
  19.153 +  key --| mapping :|-- (fn t => in_braces (func_pats t) || const_val t)
  19.154 +
  19.155 +val cex = space |-- Scan.repeat assign
  19.156 +
  19.157 +fun parse_counterex recon ls =
  19.158 +  (empty_context recon, explode (cat_lines ls))
  19.159 +  |> Scan.catch (Scan.finite' Symbol.stopper (Scan.error cex))
  19.160 +  |> flat o fst
  19.161 +
  19.162 +end
    20.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    20.2 +++ b/src/HOL/SMT/Tools/z3_solver.ML	Fri Sep 18 18:13:19 2009 +0200
    20.3 @@ -0,0 +1,83 @@
    20.4 +(*  Title:      HOL/SMT/Tools/z3_solver.ML
    20.5 +    Author:     Sascha Boehme, TU Muenchen
    20.6 +
    20.7 +Interface of the SMT solver Z3.
    20.8 +*)
    20.9 +
   20.10 +signature Z3_SOLVER =
   20.11 +sig
   20.12 +  val proofs: bool Config.T
   20.13 +  val options: string Config.T
   20.14 +
   20.15 +  val setup: theory -> theory
   20.16 +end
   20.17 +
   20.18 +structure Z3_Solver: Z3_SOLVER =
   20.19 +struct
   20.20 +
   20.21 +val solver_name = "z3"
   20.22 +val env_var = "Z3_SOLVER"
   20.23 +
   20.24 +val (proofs, proofs_setup) = Attrib.config_bool "z3_proofs" false
   20.25 +val (options, options_setup) = Attrib.config_string "z3_options" ""
   20.26 +
   20.27 +fun add xs ys = ys @ xs
   20.28 +
   20.29 +fun get_options ctxt =
   20.30 +  ["MODEL=true", "PRE_SIMPLIFY_EXPR=false", "CONTEXT_SIMPLIFIER=false"]
   20.31 +  |> Config.get ctxt proofs ? add ["DISPLAY_PROOF=true", "PROOF_MODE=2"]
   20.32 +  |> add (space_explode " " (Config.get ctxt options))
   20.33 +
   20.34 +fun pretty_config context = [
   20.35 +  Pretty.str ("With proofs: " ^
   20.36 +    (if Config.get_generic context proofs then "true" else "false")),
   20.37 +  Pretty.str ("Options: " ^
   20.38 +    space_implode " " (get_options (Context.proof_of context))) ]
   20.39 +
   20.40 +fun cmdline_options ctxt =
   20.41 +  get_options ctxt
   20.42 +  |> add ["-smt"]
   20.43 +
   20.44 +fun raise_cex real recon ls =
   20.45 +  let val cex = Z3_Model.parse_counterex recon ls
   20.46 +  in raise SMT_Solver.SMT_COUNTEREXAMPLE (real, cex) end
   20.47 +
   20.48 +fun check_unsat recon output =
   20.49 +  let
   20.50 +    val raw = not o String.isPrefix "WARNING" orf String.isPrefix "ERROR"
   20.51 +    val (ls, l) = the_default ([], "") (try split_last (filter raw output))
   20.52 +  in
   20.53 +    if String.isPrefix "unsat" l then ls
   20.54 +    else if String.isPrefix "sat" l then raise_cex true recon ls
   20.55 +    else if String.isPrefix "unknown" l then raise_cex false recon ls
   20.56 +    else error (solver_name ^ " failed")
   20.57 +  end
   20.58 +
   20.59 +fun core_oracle (SMT_Solver.ProofData {output, recon, ...}) =
   20.60 +  check_unsat recon output
   20.61 +  |> K @{cprop False}
   20.62 +
   20.63 +(* FIXME
   20.64 +fun prover (SMT_Solver.ProofData {context, output, recon, assms}) =
   20.65 +  check_unsat recon output
   20.66 +  |> Z3_Proof.reconstruct context assms recon
   20.67 +*)
   20.68 +
   20.69 +fun solver oracle ctxt =
   20.70 +  let val with_proof = Config.get ctxt proofs
   20.71 +  in
   20.72 +    SMT_Solver.SolverConfig {
   20.73 +      name = {env_var=env_var, remote_name=solver_name},
   20.74 +      interface = Z3_Interface.interface,
   20.75 +      arguments = cmdline_options ctxt,
   20.76 +      reconstruct = (*FIXME:if with_proof then prover else*) oracle }
   20.77 +  end
   20.78 +
   20.79 +val setup =
   20.80 +  proofs_setup #>
   20.81 +  options_setup #>
   20.82 +  Thm.add_oracle (Binding.name solver_name, core_oracle) #-> (fn (_, oracle) =>
   20.83 +  SMT_Solver.add_solver (solver_name, solver oracle)) #>
   20.84 +  SMT_Solver.add_solver_info (solver_name, pretty_config)
   20.85 +
   20.86 +end
    21.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    21.2 +++ b/src/HOL/SMT/etc/settings	Fri Sep 18 18:13:19 2009 +0200
    21.3 @@ -0,0 +1,13 @@
    21.4 +ISABELLE_SMT="$COMPONENT"
    21.5 +
    21.6 +REMOTE_SMT_SOLVER="$ISABELLE_SMT/lib/scripts/remote_smt.pl"
    21.7 +
    21.8 +REMOTE_SMT_URL="http://www4.in.tum.de/smt/smt"
    21.9 +
   21.10 +#
   21.11 +# Paths to local SMT solvers:
   21.12 +#
   21.13 +# CVC_SOLVER=PATH
   21.14 +# YICES_SOLVER=PATH
   21.15 +# Z3_SOLVER=PATH
   21.16 +
    22.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    22.2 +++ b/src/HOL/SMT/lib/scripts/remote_smt.pl	Fri Sep 18 18:13:19 2009 +0200
    22.3 @@ -0,0 +1,43 @@
    22.4 +#!/usr/bin/env perl -w
    22.5 +#
    22.6 +# Script to invoke remote SMT solvers.
    22.7 +# Author: Sascha Böhme
    22.8 +#
    22.9 +
   22.10 +use strict;
   22.11 +use LWP;
   22.12 +
   22.13 +
   22.14 +# environment
   22.15 +
   22.16 +my $remote_smt_url = $ENV{"REMOTE_SMT_URL"};
   22.17 +
   22.18 +
   22.19 +# arguments
   22.20 +
   22.21 +my $solver = $ARGV[0];
   22.22 +my @options = @ARGV[1 .. ($#ARGV - 2)];
   22.23 +my $problem_file = $ARGV[-2];
   22.24 +my $output_file = $ARGV[-1];
   22.25 +
   22.26 +
   22.27 +# call solver
   22.28 +
   22.29 +my $agent = LWP::UserAgent->new;
   22.30 +$agent->agent("SMT-Request");
   22.31 +$agent->timeout(180);
   22.32 +my $response = $agent->post($remote_smt_url, [
   22.33 +  "Solver" => $solver,
   22.34 +  "Options" => join(" ", @options),
   22.35 +  "Problem" => [$problem_file] ],
   22.36 +  "Content_Type" => "form-data");
   22.37 +if (not $response->is_success) {
   22.38 +  print "HTTP-Error: " . $response->message . "\n";
   22.39 +  exit 1;
   22.40 +}
   22.41 +else {
   22.42 +  open(FILE, ">$output_file");
   22.43 +  print FILE $response->content;
   22.44 +  close(FILE);
   22.45 +}
   22.46 +