Update readme and add macOS x86_64 CI.

.github/workflows/ci.yml

@@ -9,10 +9,12 @@ jobs:
     strategy:
       matrix:
         include:
-        - name: Linux
+        - name: Linux-x86_64
           os: ubuntu-latest
-        - name: macOS
+        - name: macOS-aarch64
           os: macos-latest
+        - name: macOS-x86_64
+          os: macos-13
     steps:
     - name: Install Elan
       run: |
@@ -25,4 +27,4 @@ jobs:
         lake update
         lake build Smt Smt.Rat Smt.Real
     - name: Test lean-smt
-      run: lake run test
+      run: lake test

README.md

@@ -13,13 +13,22 @@ are working on adding support for other theories as well.
 
 ## Requirements
 `lean-smt` depends on [`lean-cvc5`](https://github.com/abdoo8080/lean-cvc5) FFI,
-which currently only supports Linux (x86_64) and macOS (AArch64).
+which currently only supports Linux (x86_64) and macOS (AArch64 and x86_64).
 
 ## Usage
 To use `lean-smt` in your project, add the following line to your list of
 dependencies in `lakefile.lean`:
 ```lean
-require smt from git "https://github.com/ufmg-smite/lean-smt.git"@"main"
+require smt from git "https://github.com/ufmg-smite/lean-smt.git" @ "main"
+
+def libcpp : String :=
+  if System.Platform.isWindows then "libstdc++-6.dll"
+  else if System.Platform.isOSX then "libc++.dylib"
+  else "libstdc++.so.6"
+
+package foo where
+  moreLeanArgs := #[s!"--load-dynlib={libcpp}"]
+  moreGlobalServerArgs := #[s!"--load-dynlib={libcpp}"]
 ```
 `lean-smt` comes with one main tactic, `smt`, that translates the current goal
 into an SMT query, sends the query to cvc5, and (if the solver returns `unsat`)

lake-manifest.json

@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "aff591ae23965f28f15d8a1437a06d9febb704b0",
+   "rev": "b7a6933c50aea5bb294eeff9ed2555640bc9c435",
    "name": "cvc5",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "aff591ae23965f28f15d8a1437a06d9febb704b0",
+   "inputRev": "b7a6933c50aea5bb294eeff9ed2555640bc9c435",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/batteries",

lakefile.lean

@@ -3,7 +3,7 @@ import Lake
 open Lake DSL
 
 require cvc5 from
-  git "https://github.com/abdoo8080/lean-cvc5.git" @ "aff591ae23965f28f15d8a1437a06d9febb704b0"
+  git "https://github.com/abdoo8080/lean-cvc5.git" @ "b7a6933c50aea5bb294eeff9ed2555640bc9c435"
 
 require mathlib from
   git "https://github.com/leanprover-community/mathlib4.git" @ "v4.13.0"
@@ -40,7 +40,7 @@ USAGE:
 
 Run tests.
 -/
-script test do
+@[test_driver] script test do
   let files ← readAllFiles (FilePath.mk "Test")
   let mut tests : Array FilePath := #[]
   let mut expected : Array FilePath := #[]