summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/SMT.thy

changeset 36902 | c6bae4456741 |

parent 36899 | bcd6fce5bf06 |

child 37124 | fe22fc54b876 |

equal
deleted
inserted
replaced

36901:a20c5484dc9c | 36902:c6bae4456741 |
---|---|

24 ("Tools/SMT/yices_solver.ML") |
24 ("Tools/SMT/yices_solver.ML") |

25 begin |
25 begin |

26 |
26 |

27 |
27 |

28 |
28 |

29 section {* Triggers for quantifier instantiation *} |
29 subsection {* Triggers for quantifier instantiation *} |

30 |
30 |

31 text {* |
31 text {* |

32 Some SMT solvers support triggers for quantifier instantiation. |
32 Some SMT solvers support triggers for quantifier instantiation. |

33 Each trigger consists of one ore more patterns. A pattern may either |
33 Each trigger consists of one ore more patterns. A pattern may either |

34 be a list of positive subterms (the first being tagged by "pat" and |
34 be a list of positive subterms (the first being tagged by "pat" and |

51 definition trigger :: "pattern list \<Rightarrow> bool \<Rightarrow> bool" |
51 definition trigger :: "pattern list \<Rightarrow> bool \<Rightarrow> bool" |

52 where "trigger _ P = P" |
52 where "trigger _ P = P" |

53 |
53 |

54 |
54 |

55 |
55 |

56 section {* Higher-order encoding *} |
56 subsection {* Higher-order encoding *} |

57 |
57 |

58 text {* |
58 text {* |

59 Application is made explicit for constants occurring with varying |
59 Application is made explicit for constants occurring with varying |

60 numbers of arguments. This is achieved by the introduction of the |
60 numbers of arguments. This is achieved by the introduction of the |

61 following constant. |
61 following constant. |

72 lemmas array_rules = ext fun_upd_apply fun_upd_same fun_upd_other |
72 lemmas array_rules = ext fun_upd_apply fun_upd_same fun_upd_other |

73 fun_upd_upd |
73 fun_upd_upd |

74 |
74 |

75 |
75 |

76 |
76 |

77 section {* First-order logic *} |
77 subsection {* First-order logic *} |

78 |
78 |

79 text {* |
79 text {* |

80 Some SMT solvers require a strict separation between formulas and |
80 Some SMT solvers require a strict separation between formulas and |

81 terms. When translating higher-order into first-order problems, |
81 terms. When translating higher-order into first-order problems, |

82 all uninterpreted constants (those not builtin in the target solver) |
82 all uninterpreted constants (those not builtin in the target solver) |

89 definition term_eq :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infix "term'_eq" 50) |
89 definition term_eq :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infix "term'_eq" 50) |

90 where "(x term_eq y) = (x = y)" |
90 where "(x term_eq y) = (x = y)" |

91 |
91 |

92 |
92 |

93 |
93 |

94 section {* Setup *} |
94 subsection {* Setup *} |

95 |
95 |

96 use "Tools/SMT/smt_monomorph.ML" |
96 use "Tools/SMT/smt_monomorph.ML" |

97 use "Tools/SMT/smt_normalize.ML" |
97 use "Tools/SMT/smt_normalize.ML" |

98 use "Tools/SMT/smt_translate.ML" |
98 use "Tools/SMT/smt_translate.ML" |

99 use "Tools/SMT/smt_solver.ML" |
99 use "Tools/SMT/smt_solver.ML" |

116 Yices_Solver.setup |
116 Yices_Solver.setup |

117 *} |
117 *} |

118 |
118 |

119 |
119 |

120 |
120 |

121 section {* Configuration *} |
121 subsection {* Configuration *} |

122 |
122 |

123 text {* |
123 text {* |

124 The current configuration can be printed by the command |
124 The current configuration can be printed by the command |

125 @{text smt_status}, which shows the values of most options. |
125 @{text smt_status}, which shows the values of most options. |

126 *} |
126 *} |

222 |
222 |

223 declare [[ z3_options = "" ]] |
223 declare [[ z3_options = "" ]] |

224 |
224 |

225 |
225 |

226 |
226 |

227 section {* Schematic rules for Z3 proof reconstruction *} |
227 subsection {* Schematic rules for Z3 proof reconstruction *} |

228 |
228 |

229 text {* |
229 text {* |

230 Several prof rules of Z3 are not very well documented. There are two |
230 Several prof rules of Z3 are not very well documented. There are two |

231 lemma groups which can turn failing Z3 proof reconstruction attempts |
231 lemma groups which can turn failing Z3 proof reconstruction attempts |

232 into succeeding ones: the facts in @{text z3_rule} are tried prior to |
232 into succeeding ones: the facts in @{text z3_rule} are tried prior to |