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 *}