From 2ca0b80f6ae414d903618182fa22004caf8aebaf Mon Sep 17 00:00:00 2001
From: Emiko Soroka <emiko@me.com>
Date: Thu, 23 May 2024 09:04:11 -0700
Subject: [PATCH 1/2] @Mykel suggested this change to automatically download z3
 if it's not already installed.

---
 Project.toml       |  2 ++
 src/call_solver.jl | 14 ++++++++++++--
 2 files changed, 14 insertions(+), 2 deletions(-)

diff --git a/Project.toml b/Project.toml
index 449c87b..c403965 100644
--- a/Project.toml
+++ b/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"
\ No newline at end of file
diff --git a/src/call_solver.jl b/src/call_solver.jl
index 5127efb..789b1a2 100644
--- a/src/call_solver.jl
+++ b/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

From 51337b331c428f69f9e899e344e2a934399a200c Mon Sep 17 00:00:00 2001
From: Emiko Soroka <emiko@me.com>
Date: Thu, 23 May 2024 09:05:37 -0700
Subject: [PATCH 2/2] while we're at it, fix issue #42, undefined n variable in
 README example

---
 README.md | 1 +
 1 file changed, 1 insertion(+)

diff --git a/README.md b/README.md
index 1150aa3..04e5b5f 100644
--- a/README.md
+++ b/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)