summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/SMT.thy

changeset 41059 | d2b1fc1b8e19 |

parent 40806 | 59d96f777da3 |

child 41121 | 5c5d05963f93 |

1.1 --- a/src/HOL/SMT.thy Mon Dec 06 16:54:22 2010 +0100 1.2 +++ b/src/HOL/SMT.thy Tue Dec 07 14:53:12 2010 +0100 1.3 @@ -105,16 +105,18 @@ 1.4 subsection {* First-order logic *} 1.5 1.6 text {* 1.7 -Some SMT solvers require a strict separation between formulas and 1.8 -terms. When translating higher-order into first-order problems, 1.9 -all uninterpreted constants (those not builtin in the target solver) 1.10 +Some SMT solvers only accept problems in first-order logic, i.e., 1.11 +where formulas and terms are syntactically separated. When 1.12 +translating higher-order into first-order problems, all 1.13 +uninterpreted constants (those not built-in in the target solver) 1.14 are treated as function symbols in the first-order sense. Their 1.15 -occurrences as head symbols in atoms (i.e., as predicate symbols) is 1.16 -turned into terms by equating such atoms with @{term True} using the 1.17 -following term-level equation symbol. 1.18 +occurrences as head symbols in atoms (i.e., as predicate symbols) are 1.19 +turned into terms by equating such atoms with @{term True}. 1.20 +Whenever the boolean type occurs in first-order terms, it is replaced 1.21 +by the following type. 1.22 *} 1.23 1.24 -definition term_eq :: "bool \<Rightarrow> bool \<Rightarrow> bool" where "term_eq x y = (x = y)" 1.25 +typedecl term_bool 1.26 1.27 1.28 1.29 @@ -159,7 +161,10 @@ 1.30 1.31 setup {* 1.32 SMT_Config.setup #> 1.33 + SMT_Normalize.setup #> 1.34 SMT_Solver.setup #> 1.35 + SMTLIB_Interface.setup #> 1.36 + Z3_Interface.setup #> 1.37 Z3_Proof_Reconstruction.setup #> 1.38 SMT_Setup_Solvers.setup 1.39 *} 1.40 @@ -354,9 +359,10 @@ 1.41 1.42 1.43 1.44 +hide_type term_bool 1.45 hide_type (open) pattern 1.46 -hide_const Pattern term_eq 1.47 -hide_const (open) trigger pat nopat weight fun_app z3div z3mod 1.48 +hide_const Pattern fun_app 1.49 +hide_const (open) trigger pat nopat weight z3div z3mod 1.50 1.51 1.52