added option to enable trigger inference;
authorboehmes
Wed Dec 15 08:39:24 2010 +0100 (2010-12-15)
changeset 411254a9eec045f2a
parent 41124 1de17a2de5ad
child 41126 e0bd443c0fdd
added option to enable trigger inference;
better documentation of triggers and SMT available options
src/HOL/SMT.thy
src/HOL/Tools/SMT/smt_config.ML
     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 *}
     2.1 --- a/src/HOL/Tools/SMT/smt_config.ML	Wed Dec 15 08:39:24 2010 +0100
     2.2 +++ b/src/HOL/Tools/SMT/smt_config.ML	Wed Dec 15 08:39:24 2010 +0100
     2.3 @@ -26,6 +26,7 @@
     2.4    val trace: bool Config.T
     2.5    val trace_used_facts: bool Config.T
     2.6    val monomorph_limit: int Config.T
     2.7 +  val infer_triggers: bool Config.T
     2.8    val drop_bad_facts: bool Config.T
     2.9    val filter_only_facts: bool Config.T
    2.10    val debug_files: string Config.T
    2.11 @@ -135,6 +136,10 @@
    2.12  val (monomorph_limit, setup_monomorph_limit) =
    2.13    Attrib.config_int monomorph_limitN (K 10)
    2.14  
    2.15 +val infer_triggersN = "smt_infer_triggers"
    2.16 +val (infer_triggers, setup_infer_triggers) =
    2.17 +  Attrib.config_bool infer_triggersN (K false)
    2.18 +
    2.19  val drop_bad_factsN = "smt_drop_bad_facts"
    2.20  val (drop_bad_facts, setup_drop_bad_facts) =
    2.21    Attrib.config_bool drop_bad_factsN (K false)
    2.22 @@ -156,6 +161,7 @@
    2.23    setup_trace #>
    2.24    setup_verbose #>
    2.25    setup_monomorph_limit #>
    2.26 +  setup_infer_triggers #>
    2.27    setup_drop_bad_facts #>
    2.28    setup_filter_only_facts #>
    2.29    setup_trace_used_facts #>