1 (* Title: HOL/SMT/SMT_Base.thy |
|
2 Author: Sascha Boehme, TU Muenchen |
|
3 *) |
|
4 |
|
5 header {* SMT-specific definitions and basic tools *} |
|
6 |
|
7 theory SMT_Base |
|
8 imports Real "~~/src/HOL/Word/Word" |
|
9 uses |
|
10 "~~/src/Tools/cache_io.ML" |
|
11 ("Tools/smt_additional_facts.ML") |
|
12 ("Tools/smt_monomorph.ML") |
|
13 ("Tools/smt_normalize.ML") |
|
14 ("Tools/smt_translate.ML") |
|
15 ("Tools/smt_solver.ML") |
|
16 ("Tools/smtlib_interface.ML") |
|
17 begin |
|
18 |
|
19 section {* Triggers for quantifier instantiation *} |
|
20 |
|
21 text {* |
|
22 Some SMT solvers support triggers for quantifier instantiation. Each trigger |
|
23 consists of one ore more patterns. A pattern may either be a list of positive |
|
24 subterms (the first being tagged by "pat" and the consecutive subterms tagged |
|
25 by "andpat"), or a list of negative subterms (the first being tagged by "nopat" |
|
26 and the consecutive subterms tagged by "andpat"). |
|
27 *} |
|
28 |
|
29 datatype pattern = Pattern |
|
30 |
|
31 definition pat :: "'a \<Rightarrow> pattern" |
|
32 where "pat _ = Pattern" |
|
33 |
|
34 definition nopat :: "'a \<Rightarrow> pattern" |
|
35 where "nopat _ = Pattern" |
|
36 |
|
37 definition andpat :: "pattern \<Rightarrow> 'a \<Rightarrow> pattern" (infixl "andpat" 60) |
|
38 where "_ andpat _ = Pattern" |
|
39 |
|
40 definition trigger :: "pattern list \<Rightarrow> bool \<Rightarrow> bool" |
|
41 where "trigger _ P = P" |
|
42 |
|
43 |
|
44 |
|
45 section {* Arithmetic *} |
|
46 |
|
47 text {* |
|
48 The sign of @{term "op mod :: int \<Rightarrow> int \<Rightarrow> int"} follows the sign of the |
|
49 divisor. In contrast to that, the sign of the following operation is that of |
|
50 the dividend. |
|
51 *} |
|
52 |
|
53 definition rem :: "int \<Rightarrow> int \<Rightarrow> int" (infixl "rem" 70) |
|
54 where "a rem b = |
|
55 (if (a \<ge> 0 \<and> b < 0) \<or> (a < 0 \<and> b \<ge> 0) then - (a mod b) else a mod b)" |
|
56 |
|
57 |
|
58 |
|
59 section {* Bitvectors *} |
|
60 |
|
61 text {* |
|
62 The following definitions provide additional functions not found in HOL-Word. |
|
63 *} |
|
64 |
|
65 definition sdiv :: "'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a word" (infix "sdiv" 70) |
|
66 where "w1 sdiv w2 = word_of_int (sint w1 div sint w2)" |
|
67 |
|
68 definition smod :: "'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a word" (infix "smod" 70) |
|
69 (* sign follows divisor *) |
|
70 where "w1 smod w2 = word_of_int (sint w1 mod sint w2)" |
|
71 |
|
72 definition srem :: "'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a word" (infix "srem" 70) |
|
73 (* sign follows dividend *) |
|
74 where "w1 srem w2 = word_of_int (sint w1 rem sint w2)" |
|
75 |
|
76 definition bv_shl :: "'a::len0 word \<Rightarrow> 'a word \<Rightarrow> 'a word" |
|
77 where "bv_shl w1 w2 = (w1 << unat w2)" |
|
78 |
|
79 definition bv_lshr :: "'a::len0 word \<Rightarrow> 'a word \<Rightarrow> 'a word" |
|
80 where "bv_lshr w1 w2 = (w1 >> unat w2)" |
|
81 |
|
82 definition bv_ashr :: "'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a word" |
|
83 where "bv_ashr w1 w2 = (w1 >>> unat w2)" |
|
84 |
|
85 |
|
86 |
|
87 section {* Higher-Order Encoding *} |
|
88 |
|
89 definition "apply" where "apply f x = f x" |
|
90 |
|
91 definition array_ext where "array_ext a b = (SOME x. a = b \<or> a x \<noteq> b x)" |
|
92 |
|
93 lemma fun_upd_eq: "(f = f (x := y)) = (f x = y)" |
|
94 proof |
|
95 assume "f = f(x:=y)" |
|
96 hence "f x = (f(x:=y)) x" by simp |
|
97 thus "f x = y" by simp |
|
98 qed (auto simp add: ext) |
|
99 |
|
100 lemmas array_rules = |
|
101 ext fun_upd_apply fun_upd_same fun_upd_other fun_upd_upd fun_upd_eq apply_def |
|
102 |
|
103 |
|
104 |
|
105 section {* First-order logic *} |
|
106 |
|
107 text {* |
|
108 Some SMT solver formats require a strict separation between formulas and terms. |
|
109 During normalization, all uninterpreted constants are treated as function |
|
110 symbols, and atoms (with uninterpreted head symbol) are turned into terms by |
|
111 equating them with true using the following term-level equation symbol: |
|
112 *} |
|
113 |
|
114 definition term_eq :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infix "term'_eq" 50) |
|
115 where "(x term_eq y) = (x = y)" |
|
116 |
|
117 |
|
118 |
|
119 section {* Setup *} |
|
120 |
|
121 use "Tools/smt_additional_facts.ML" |
|
122 use "Tools/smt_monomorph.ML" |
|
123 use "Tools/smt_normalize.ML" |
|
124 use "Tools/smt_translate.ML" |
|
125 use "Tools/smt_solver.ML" |
|
126 use "Tools/smtlib_interface.ML" |
|
127 |
|
128 setup {* SMT_Solver.setup *} |
|
129 |
|
130 end |
|