src/HOL/SMT.thy
changeset 40162 7f58a9a843c2
parent 39483 9f0e5684f04b
child 40274 6486c610a549
     1.1 --- a/src/HOL/SMT.thy	Tue Oct 26 11:39:26 2010 +0200
     1.2 +++ b/src/HOL/SMT.thy	Tue Oct 26 11:45:12 2010 +0200
     1.3 @@ -19,9 +19,7 @@
     1.4    ("Tools/SMT/z3_proof_reconstruction.ML")
     1.5    ("Tools/SMT/z3_model.ML")
     1.6    ("Tools/SMT/z3_interface.ML")
     1.7 -  ("Tools/SMT/z3_solver.ML")
     1.8 -  ("Tools/SMT/cvc3_solver.ML")
     1.9 -  ("Tools/SMT/yices_solver.ML")
    1.10 +  ("Tools/SMT/smt_setup_solvers.ML")
    1.11  begin
    1.12  
    1.13  
    1.14 @@ -124,16 +122,12 @@
    1.15  use "Tools/SMT/z3_proof_literals.ML"
    1.16  use "Tools/SMT/z3_proof_reconstruction.ML"
    1.17  use "Tools/SMT/z3_model.ML"
    1.18 -use "Tools/SMT/z3_solver.ML"
    1.19 -use "Tools/SMT/cvc3_solver.ML"
    1.20 -use "Tools/SMT/yices_solver.ML"
    1.21 +use "Tools/SMT/smt_setup_solvers.ML"
    1.22  
    1.23  setup {*
    1.24    SMT_Solver.setup #>
    1.25    Z3_Proof_Reconstruction.setup #>
    1.26 -  Z3_Solver.setup #>
    1.27 -  CVC3_Solver.setup #>
    1.28 -  Yices_Solver.setup
    1.29 +  SMT_Setup_Solvers.setup
    1.30  *}
    1.31  
    1.32  
    1.33 @@ -171,6 +165,31 @@
    1.34  
    1.35  declare [[ smt_timeout = 20 ]]
    1.36  
    1.37 +text {*
    1.38 +In general, the binding to SMT solvers runs as an oracle, i.e, the SMT
    1.39 +solvers are fully trusted without additional checks.  The following
    1.40 +option can cause the SMT solver to run in proof-producing mode, giving
    1.41 +a checkable certificate.  This is currently only implemented for Z3.
    1.42 +*}
    1.43 +
    1.44 +declare [[ smt_oracle = false ]]
    1.45 +
    1.46 +text {*
    1.47 +Each SMT solver provides several commandline options to tweak its
    1.48 +behaviour.  They can be passed to the solver by setting the following
    1.49 +options.
    1.50 +*}
    1.51 +
    1.52 +declare [[ cvc3_options = "", yices_options = "", z3_options = "" ]]
    1.53 +
    1.54 +text {*
    1.55 +Enable the following option to use built-in support for datatypes and
    1.56 +records.  Currently, this is only implemented for Z3 running in oracle
    1.57 +mode.
    1.58 +*}
    1.59 +
    1.60 +declare [[ smt_datatypes = false ]]
    1.61 +
    1.62  
    1.63  
    1.64  subsection {* Certificates *}
    1.65 @@ -213,41 +232,14 @@
    1.66  
    1.67  declare [[ smt_trace = false ]]
    1.68  
    1.69 -
    1.70 -
    1.71 -subsection {* Z3-specific options *}
    1.72 -
    1.73  text {*
    1.74 -Z3 is the only SMT solver whose proofs are checked (or reconstructed)
    1.75 -in Isabelle (all other solvers are implemented as oracles).  Enabling
    1.76 -or disabling proof reconstruction for Z3 is controlled by the option
    1.77 -@{text z3_proofs}. 
    1.78 +From the set of assumptions given to the SMT solver, those assumptions
    1.79 +used in the proof are traced when the following option is set to
    1.80 +@{term true}.  This only works for Z3 when it runs in non-oracle mode
    1.81 +(see options @{text smt_solver} and @{text smt_oracle} above).
    1.82  *}
    1.83  
    1.84 -declare [[ z3_proofs = true ]]
    1.85 -
    1.86 -text {*
    1.87 -From the set of assumptions given to Z3, those assumptions used in
    1.88 -the proof are traced when the option @{text z3_trace_assms} is set to
    1.89 -@{term true}.
    1.90 -*}
    1.91 -
    1.92 -declare [[ z3_trace_assms = false ]]
    1.93 -
    1.94 -text {*
    1.95 -Z3 provides several commandline options to tweak its behaviour.  They
    1.96 -can be configured by writing them literally as value for the option
    1.97 -@{text z3_options}.
    1.98 -*}
    1.99 -
   1.100 -declare [[ z3_options = "" ]]
   1.101 -
   1.102 -text {*
   1.103 -The following configuration option may be used to enable mapping of
   1.104 -HOL datatypes and records to native datatypes provided by Z3.
   1.105 -*}
   1.106 -
   1.107 -declare [[ z3_datatypes = false ]]
   1.108 +declare [[ smt_trace_used_facts = false ]]
   1.109  
   1.110  
   1.111