Enable support for OpenSMT as a main solver

kind2-mc · Jan 18, 2025 · 681403a · 681403a
1 parent b1da905
commit 681403a
Show file tree

Hide file tree

Showing 3 changed files with 51 additions and 29 deletions.
diff --git a/README.rst b/README.rst
@@ -57,14 +57,16 @@ given enough time and resources).
 
 ``--timeout <int>`` (default ``0`` = none) -- Run for the given number of seconds of wall clock time
 
-``--smt_solver {Bitwuzla|cvc5|MathSAT|SMTInterpol|Yices|Yices2|Z3}`` (default ``Z3``\ ) -- Select SMT solver
+``--smt_solver {Bitwuzla|cvc5|MathSAT|OpenSMT|SMTInterpol|Yices|Yices2|Z3}`` (default ``Z3``\ ) -- Select SMT solver
 
 ``--bitwuzla_bin <file>`` -- Executable for Bitwuzla
 
 ``--cvc5_bin <file>`` -- Executable for cvc5
 
 ``--mathsat_bin <file>`` -- Executable for MathSAT 5
 
+``--opensmt_bin <file>`` -- Executable for OpenSMT
+
 ``--smtinterpol_jar <file>`` -- JAR of SMTInterpol
 
 ``--yices_bin <file>`` -- Executable for Yices 1 (native input)
@@ -103,6 +105,7 @@ To run Kind 2 the following software must be installed on your computer:
   * `Bitwuzla <https://bitwuzla.github.io/>`_ (for inputs with only machine integers),
   * `cvc5 <https://cvc5.github.io/>`_\ ,
   * `MathSAT 5 <http://mathsat.fbk.eu/index.html>`_\ ,
+  * `OpenSMT <https://verify.inf.usi.ch/opensmt>`_ (v2.8.0),
   * `SMTInterpol <https://ultimate.informatik.uni-freiburg.de/smtinterpol/>`_\ ,
   * `Yices 2 <http://yices.csl.sri.com/>`_\ ,
   * `Yices 1 <https://yices.csl.sri.com/old/download-yices1.html>`_\ , or

diff --git a/doc/usr/source/home.rst b/doc/usr/source/home.rst
@@ -37,14 +37,16 @@ given enough time and resources).
 
 ``--timeout <int>`` (default ``0`` = none) -- Run for the given number of seconds of wall clock time
 
-``--smt_solver {Bitwuzla|cvc5|MathSAT|SMTInterpol|Yices|Yices2|Z3}`` (default ``Z3``\ ) -- Select SMT solver
+``--smt_solver {Bitwuzla|cvc5|MathSAT|OpenSMT|SMTInterpol|Yices|Yices2|Z3}`` (default ``Z3``\ ) -- Select SMT solver
 
 ``--bitwuzla_bin <file>`` -- Executable for Bitwuzla
 
 ``--cvc5_bin <file>`` -- Executable for cvc5
 
 ``--mathsat_bin <file>`` -- Executable for MathSAT 5
 
+``--opensmt_bin <file>`` -- Executable for OpenSMT
+
 ``--smtinterpol_jar <file>`` -- JAR of SMTInterpol
 
 ``--yices_bin <file>`` -- Executable for Yices 1 (native input)
@@ -83,6 +85,7 @@ To run Kind 2 the following software must be installed on your computer:
   * `Bitwuzla <https://bitwuzla.github.io/>`_ (for inputs with only machine integers),
   * `cvc5 <https://cvc5.github.io/>`_\ ,
   * `MathSAT 5 <http://mathsat.fbk.eu/index.html>`_\ ,
+  * `OpenSMT <https://verify.inf.usi.ch/opensmt>`_ (v2.8.0),
   * `SMTInterpol <https://ultimate.informatik.uni-freiburg.de/smtinterpol/>`_\ ,
   * `Yices 2 <http://yices.csl.sri.com/>`_\ ,
   * `Yices 1 <https://yices.csl.sri.com/old/download-yices1.html>`_\ , or

diff --git a/src/flags.ml b/src/flags.ml
@@ -135,7 +135,7 @@ module Smt = struct
     | "bitwuzla" -> `Bitwuzla_SMTLIB
     | "cvc5" -> `cvc5_SMTLIB
     | "mathsat" ->  `MathSAT_SMTLIB
-    (* | "opensmt" -> `OpenSMT_SMTLIB *)
+    | "opensmt" -> `OpenSMT_SMTLIB
     | "smtinterpol" -> `SMTInterpol_SMTLIB
     | "yices2" -> `Yices2_SMTLIB
     | "yices" -> `Yices_native
@@ -153,7 +153,7 @@ module Smt = struct
     | `detect -> "detect"
 
   (* Suggested order of use (more capabilities, more theories, better performance) *)
-  let solver_values = "Z3, cvc5, Yices2, MathSAT, SMTInterpol, Bitwuzla, Yices"
+  let solver_values = "Z3, cvc5, Yices2, MathSAT, SMTInterpol, OpenSMT, Bitwuzla, Yices"
   let solver_default = `detect
   let solver = ref solver_default
   let _ = add_spec
@@ -535,6 +535,11 @@ module Smt = struct
         set_solver `SMTInterpol_SMTLIB;
         set_smtinterpol_jar exec;
       with Not_found ->
+      try
+        let exec = find_solver ~fail:false "OpenSMT" (opensmt_bin ()) in
+        set_solver `OpenSMT_SMTLIB;
+        set_opensmt_bin exec;
+      with Not_found ->
       try
         let exec = find_solver ~fail:false "Bitwuzla" (bitwuzla_bin ()) in
         set_solver `Bitwuzla_SMTLIB;
@@ -612,32 +617,43 @@ module Smt = struct
       | `Z3_SMTLIB -> ()
       | _ -> find_solver ~fail:true "Z3" (z3_bin ()) |> ignore
     )
-    | `detect ->
-      try
-        let exec = find_solver ~fail:false "MathSAT" (mathsat_bin ()) in
-        set_itp_solver `MathSAT_SMTLIB;
-        set_mathsat_bin exec;
-      with Not_found ->
-      try
-        let exec = find_solver ~filetype:"JAR" ~fail:false "SMTInterpol" (smtinterpol_jar ()) in
-        set_itp_solver `SMTInterpol_SMTLIB;
-        set_smtinterpol_jar exec;
-      with Not_found ->
-      try
-        let exec = find_solver ~fail:false "Z3" (z3_bin ()) in
-        set_itp_solver `Z3_QE;
-        set_z3_bin exec;
-      with Not_found ->
-      try
-        let exec = find_solver ~fail:false "cvc5" (cvc5_bin ()) in
-        set_itp_solver `cvc5_QE;
-        set_cvc5_bin exec;
-      with Not_found -> 
-      try
-        let exec = find_solver ~fail:false "OpenSMT" (opensmt_bin ()) in
+    | `detect -> (
+      match solver () with
+      | `OpenSMT_SMTLIB ->
+        (* MathSAT interpolation requires a combination of LIA/LRA,
+           which is not currently supported by OpenSMT.
+           If the user selects OpenSMT as the main solver, we give
+           preference to OpenSMT as the interpolating solver over MathSAT.
+        *)
         set_itp_solver `OpenSMT_SMTLIB;
-        set_opensmt_bin exec;
-      with Not_found -> () (* Ẃe keep `detect to know no itp solver was found *)
+      | _ -> (
+        try
+          let exec = find_solver ~fail:false "MathSAT" (mathsat_bin ()) in
+          set_itp_solver `MathSAT_SMTLIB;
+          set_mathsat_bin exec;
+        with Not_found ->
+        try
+          let exec = find_solver ~filetype:"JAR" ~fail:false "SMTInterpol" (smtinterpol_jar ()) in
+          set_itp_solver `SMTInterpol_SMTLIB;
+          set_smtinterpol_jar exec;
+        with Not_found ->
+        try
+          let exec = find_solver ~fail:false "Z3" (z3_bin ()) in
+          set_itp_solver `Z3_QE;
+          set_z3_bin exec;
+        with Not_found ->
+        try
+          let exec = find_solver ~fail:false "cvc5" (cvc5_bin ()) in
+          set_itp_solver `cvc5_QE;
+          set_cvc5_bin exec;
+        with Not_found ->
+        try
+          let exec = find_solver ~fail:false "OpenSMT" (opensmt_bin ()) in
+          set_itp_solver `OpenSMT_SMTLIB;
+          set_opensmt_bin exec;
+        with Not_found -> () (* Ẃe keep `detect to know no itp solver was found *)
+      )
+    )
 end