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