src/HOL/SMT.thy
changeset 41432 3214c39777ab
parent 41426 09615ed31f04
child 41459 f0db8f40d656
     1.1 --- a/src/HOL/SMT.thy	Tue Jan 04 15:46:38 2011 -0800
     1.2 +++ b/src/HOL/SMT.thy	Thu Jan 06 17:51:56 2011 +0100
     1.3 @@ -176,17 +176,11 @@
     1.4  
     1.5  text {*
     1.6  The option @{text smt_solver} can be used to change the target SMT
     1.7 -solver.  The possible values are @{text cvc3}, @{text yices}, and
     1.8 -@{text z3}.  It is advisable to locally install the selected solver,
     1.9 -although this is not necessary for @{text cvc3} and @{text z3}, which
    1.10 -can also be used over an Internet-based service.
    1.11 -
    1.12 -When using local SMT solvers, the path to their binaries should be
    1.13 -declared by setting the following environment variables:
    1.14 -@{text CVC3_SOLVER}, @{text YICES_SOLVER}, and @{text Z3_SOLVER}.
    1.15 +solver.  The possible values can be obtained from the @{text smt_status}
    1.16 +command.
    1.17  *}
    1.18  
    1.19 -declare [[ smt_solver = z3 ]]
    1.20 +declare [[ smt_solver = cvc3 ]]
    1.21  
    1.22  text {*
    1.23  Since SMT solvers are potentially non-terminating, there is a timeout
    1.24 @@ -218,7 +212,9 @@
    1.25  options.
    1.26  *}
    1.27  
    1.28 -declare [[ cvc3_options = "", yices_options = "", z3_options = "" ]]
    1.29 +declare [[ cvc3_options = "", remote_cvc3_options = "" ]]
    1.30 +declare [[ yices_options = "" ]]
    1.31 +declare [[ z3_options = "", remote_z3_options = "" ]]
    1.32  
    1.33  text {*
    1.34  Enable the following option to use built-in support for datatypes and