Merge pull request #43 from elsoroka/download-z3

Automatically download Z3 if not already installed

Project.toml

@@ -5,6 +5,7 @@ version = "0.1.1"
 
 [compat]
 julia = "1"
+z3_jll = "4.13"
 
 [extras]
 Test = "8dfed614-e22c-5e08-85e1-65c5234f0b40"
@@ -14,3 +15,4 @@ test = ["Test"]
 
 [deps]
 Logging = "56ddb016-857b-54e1-b83d-db4d58db5568"
+z3_jll = "1bc4e1ec-7839-5212-8f2f-0d16b7bd09bc"

README.md

@@ -16,6 +16,7 @@ You can read the documentation [here](https://elsoroka.github.io/Satisfiability.
 ### Solving the vector-valued Boolean problem
 (x1 ∧ y1) ∨ (¬x1 ∧ y1) ∧ ... ∧ (xn ∧ yn) ∨ (¬xn ∧ yn)
 ```julia
+n = 10
 @satvariable(x[1:n], Bool)
 @satvariable(y[1:n], Bool)
 expr = (x .∧ y) .∨ (¬x .∧ y)

src/call_solver.jl

@@ -1,4 +1,5 @@
 import Base.open, Base.close
+using z3_jll
 
 ##### SOLVER OBJECT #####
 abstract type AbstractSolver end
@@ -25,12 +26,21 @@ end
 
 # some instantiation options, currently we are not using kwargs
 Solver(name::String, cmd::Cmd; kwargs...) = Solver(name, cmd, kwargs)
+Z3(; kwargs...) = Solver("Z3", `$(z3()) -smt2 -in`, kwargs)
 if Sys.iswindows()
-    Z3(; kwargs...) = Solver("Z3", `z3.exe -smt2 -in`, kwargs)
+    try success(`z3.exe --version`)
+        # use z3 if it is available on path
+        Z3(; kwargs...) = Solver("Z3", `z3.exe -smt2 -in`, kwargs)
+    catch
+    end
     CVC5(; kwargs...) = Solver("CVC5", `cvc5.exe --interactive --produce-models --incremental`, kwargs)
     Yices(; kwargs...) = Solver("Yices", `yices-smt2.exe --interactive --smt2-model-format`)
 else
-    Z3(; kwargs...) = Solver("Z3", `z3 -smt2 -in`, kwargs)
+    try success(`z3.exe --version`)
+        # use z3 if it is available on path
+        Z3(; kwargs...) = Solver("Z3", `z3 -smt2 -in`, kwargs)
+    catch
+    end
     CVC5(; kwargs...) = Solver("CVC5", `cvc5 --interactive --produce-models --incremental`, kwargs)
     Yices(; kwargs...) = Solver("Yices", `yices-smt2 --interactive --smt2-model-format`)
 end