Merge pull request #54 from rafaelbailo/main

Automatically test julia examples in README.md

.github/workflows/ci.yml

@@ -14,21 +14,24 @@ jobs:
     steps:
       - name: Checkout
         uses: actions/checkout@master
-      
+
       - name: Setup z3
         run: sudo apt-get -y install z3
-
+
+      - name: Setup Yices
+        run: sudo add-apt-repository ppa:sri-csl/formal-methods; sudo apt-get update; sudo apt-get install yices2
+
       - name: Set up Julia latest version
         uses: julia-actions/setup-julia@latest
       - uses: julia-actions/cache@v2
-      
+
       - name: Run tests
         uses: julia-actions/julia-buildpkg@v1
       - uses: julia-actions/julia-runtest@v1
       - uses: julia-actions/julia-processcoverage@v1
       - name: Upload coverage reports to Codecov
-        uses: codecov/codecov-action@v4 
+        uses: codecov/codecov-action@v4
         env:
           CODECOV_TOKEN: ${{ secrets.CODECOV_TOKEN }}
         with:
-          file: lcov.info  # https://github.com/julia-actions/julia-processcoverage
+          file: lcov.info # https://github.com/julia-actions/julia-processcoverage

README.md

@@ -66,15 +66,12 @@ Now let's suppose we want to use Yices, another SMT solver. Unlike Z3, Yices req
 
 status = sat!(distinct(x,y), f(x) == y, f(f(x)) == x, solver=Yices(), logic="QF_UFLIA")
 println("status = $status")
-```
-
-We see this yields the same result.
 
-```julia
 println(f(x.value))               # prints 0
 println(f(x.value) == y.value)    # true
 println(f(f(x.value)) == x.value) # true
 ```
+We see this yields the same result.
 
 ### Proving a bitwise version of de Morgan's law.
 In this example we want to show there is NO possible value of x and y such that de Morgan's bitwise law doesn't hold.

test/README_tests.jl

@@ -0,0 +1,26 @@
+using Satisfiability
+using Test
+
+function test_julia_examples_in_markdown(path)
+  file = read(path, String)
+  file_by_code_blocks = split(file, "```julia")[2:end]
+  possible_examples = map(s -> first(split(s, "```")), file_by_code_blocks)
+  for example ∈ possible_examples
+    quote_example = "begin\n" * example * "\nend"
+    parsed =
+      @test_nowarn Meta.parse(quote_example)
+    @test try
+      eval(parsed)
+      true
+    catch e
+      showerror(stdout, e, catch_backtrace())
+      println()
+      false
+    end
+  end
+end
+
+@testset "Test README.md examples" begin
+  using Satisfiability
+  test_julia_examples_in_markdown("../README.md")
+end

test/runtests.jl

@@ -29,13 +29,15 @@ include("ufunc_tests.jl")
     SET_DUPLICATE_NAME_WARNING!(true)
     @satvariable(z, Bool)
     @test_logs (:warn, "Duplicate variable name z of type Bool") @satvariable(z, Bool)
-    
+
     # now we should have no warnings
     SET_DUPLICATE_NAME_WARNING!(false)
-    @test_logs min_level=Logging.Warn @satvariable(z, Bool)
-    
+    @test_logs min_level = Logging.Warn @satvariable(z, Bool)
+
     # we can also clear the list
     SET_DUPLICATE_NAME_WARNING!(true)
     CLEAR_VARNAMES!()
-    @test_logs min_level=Logging.Warn @satvariable(z, Bool)
-end
+    @test_logs min_level = Logging.Warn @satvariable(z, Bool)
+end
+
+include("README_tests.jl")