[HolSmt] HOL4_Z3_EXECUTABLE, etc. can be set to "" (empty) to disable the related solvers

Author: binghe

src/HolSmt/CVC.sml

@@ -19,15 +19,18 @@ structure CVC = struct
     end
 
   fun is_configured () =
-    Option.isSome (OS.Process.getEnv "HOL4_CVC_EXECUTABLE")
+      let val v = OS.Process.getEnv "HOL4_CVC_EXECUTABLE" in
+          (Option.isSome v) andalso (Option.valOf v <> "")
+      end;
+
+  val error_msg = "CVC not configured: set the HOL4_CVC_EXECUTABLE environment variable to point to the cvc5 executable file.";
 
   fun mk_CVC_fun name pre cmd_stem post goal =
     case OS.Process.getEnv "HOL4_CVC_EXECUTABLE" of
       SOME file =>
         SolverSpec.make_solver pre (file ^ cmd_stem) post goal
     | NONE =>
-        raise Feedback.mk_HOL_ERR "CVC" name
-          "CVC not configured: set the HOL4_CVC_EXECUTABLE environment variable to point to the cvc5 executable file."
+        raise Feedback.mk_HOL_ERR "CVC" name error_msg
 
   (* cvc5, SMT-LIB file format, no proofs *)
   val CVC_SMT_Oracle =

src/HolSmt/Yices.sml

@@ -777,19 +777,25 @@ structure Yices = struct
     end
 
   fun is_configured () =
-    Option.isSome (OS.Process.getEnv "HOL4_YICES_EXECUTABLE")
+      let val v = OS.Process.getEnv "HOL4_YICES_EXECUTABLE" in
+          (Option.isSome v) andalso (Option.valOf v <> "")
+      end;
+
+  val error_msg = "Yices not configured: set the HOL4_YICES_EXECUTABLE environment variable to point to the Yices executable file.";
 
   (* Yices 1.0.29, native file format *)
   fun Yices_Oracle goal =
     case OS.Process.getEnv "HOL4_YICES_EXECUTABLE" of
       SOME file =>
+        if file = "" then
+           raise Feedback.mk_HOL_ERR "Yices" "Yices_Oracle" error_msg
+        else
         SolverSpec.make_solver
           (Lib.pair () o goal_to_Yices)
           (file ^ " -tc ")
           (Lib.K result_fn)
           goal
     | NONE =>
-        raise Feedback.mk_HOL_ERR "Yices" "Yices_Oracle"
-          "Yices not configured: set the HOL4_YICES_EXECUTABLE environment variable to point to the Yices executable file."
+        raise Feedback.mk_HOL_ERR "Yices" "Yices_Oracle" error_msg
 
 end

src/HolSmt/Z3.sml

@@ -21,15 +21,21 @@ structure Z3 = struct
     end
 
   fun is_configured () =
-    Option.isSome (OS.Process.getEnv "HOL4_Z3_EXECUTABLE")
+      let val v = OS.Process.getEnv "HOL4_Z3_EXECUTABLE" in
+          (Option.isSome v) andalso (Option.valOf v <> "")
+      end;
+
+  val error_msg = "Z3 not configured: set the HOL4_Z3_EXECUTABLE environment variable to point to the Z3 executable file.";
 
   fun mk_Z3_fun name pre cmd_stem post goal =
     case OS.Process.getEnv "HOL4_Z3_EXECUTABLE" of
       SOME file =>
+        if file = "" then
+           raise Feedback.mk_HOL_ERR "Z3" name error_msg
+        else
         SolverSpec.make_solver pre (file ^ cmd_stem) post goal
     | NONE =>
-        raise Feedback.mk_HOL_ERR "Z3" name
-          "Z3 not configured: set the HOL4_Z3_EXECUTABLE environment variable to point to the Z3 executable file."
+        raise Feedback.mk_HOL_ERR "Z3" name error_msg
 
   (* Z3 (Linux/Unix), SMT-LIB file format, no proofs *)
   val Z3_SMT_Oracle =
@@ -58,6 +64,7 @@ structure Z3 = struct
       case OS.Process.getEnv "HOL4_Z3_EXECUTABLE" of
           NONE => "0"
         | SOME p =>
+          if p = "" then "0" else
           let
             val outfile = OS.FileSys.tmpName()
             fun work () = let

src/HolSmt/selftest.sml

@@ -1,6 +1,9 @@
 (* Copyright (c) 2009-2012 Tjark Weber. All rights reserved. *)
 
 (* Unit tests for HolSmtLib *)
+open HolKernel Parse boolLib bossLib;
+
+val _ = loose_equality ();
 
 val _ = print "Testing HolSmtLib\n"