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

src/HOL/SMT.thy

changeset 41125 | 4a9eec045f2a |

parent 41124 | 1de17a2de5ad |

child 41126 | e0bd443c0fdd |

1.1 --- a/src/HOL/SMT.thy Wed Dec 15 08:39:24 2010 +0100 1.2 +++ b/src/HOL/SMT.thy Wed Dec 15 08:39:24 2010 +0100 1.3 @@ -32,16 +32,18 @@ 1.4 subsection {* Triggers for quantifier instantiation *} 1.5 1.6 text {* 1.7 -Some SMT solvers support triggers for quantifier instantiation. 1.8 -Each trigger consists of one ore more patterns. A pattern may either 1.9 -be a list of positive subterms (each being tagged by "pat"), or a 1.10 -list of negative subterms (each being tagged by "nopat"). 1.11 - 1.12 -When an SMT solver finds a term matching a positive pattern (a 1.13 -pattern with positive subterms only), it instantiates the 1.14 -corresponding quantifier accordingly. Negative patterns inhibit 1.15 -quantifier instantiations. Each pattern should mention all preceding 1.16 -bound variables. 1.17 +Some SMT solvers support patterns as a quantifier instantiation 1.18 +heuristics. Patterns may either be positive terms (tagged by "pat") 1.19 +triggering quantifier instantiations -- when the solver finds a 1.20 +term matching a positive pattern, it instantiates the corresponding 1.21 +quantifier accordingly -- or negative terms (tagged by "nopat") 1.22 +inhibiting quantifier instantiations. A list of patterns 1.23 +of the same kind is called a multipattern, and all patterns in a 1.24 +multipattern are considered conjunctively for quantifier instantiation. 1.25 +A list of multipatterns is called a trigger, and their multipatterns 1.26 +act disjunctively during quantifier instantiation. Each multipattern 1.27 +should mention at least all quantified variables of the preceding 1.28 +quantifier block. 1.29 *} 1.30 1.31 datatype pattern = Pattern 1.32 @@ -236,6 +238,24 @@ 1.33 1.34 declare [[ smt_datatypes = false ]] 1.35 1.36 +text {* 1.37 +The SMT method provides an inference mechanism to detect simple triggers 1.38 +in quantified formulas, which might increase the number of problems 1.39 +solvable by SMT solvers (note: triggers guide quantifier instantiations 1.40 +in the SMT solver). To turn it on, set the following option. 1.41 +*} 1.42 + 1.43 +declare [[ smt_infer_triggers = false ]] 1.44 + 1.45 +text {* 1.46 +The SMT method monomorphizes the given facts, that is, it tries to 1.47 +instantiate all schematic type variables with fixed types occurring 1.48 +in the problem. This is a (possibly nonterminating) fixed-point 1.49 +construction whose cycles are limited by the following option. 1.50 +*} 1.51 + 1.52 +declare [[ smt_monomorph_limit = 10 ]] 1.53 + 1.54 1.55 1.56 subsection {* Certificates *}