Merge pull request #8 from elsoroka/dev

Architecture improvements and support for fixed-size BitVectors

.github/workflows/ci.yml

@@ -1,4 +1,4 @@
-name: Workflow for Codecov example-julia
+name: CI
 on:
   push:
     branches:

.github/workflows/docs.yml

@@ -1,4 +1,4 @@
-name: Build and Deploy Documentation
+name: docs
 # https://github.com/julia-actions/julia-docdeploy
 on:
   push:

.gitignore

@@ -5,6 +5,13 @@
 # Files generated by invoking Julia with --track-allocation
 *.jl.mem
 
+# smt files generated by code
+*.smt
+
+# checkpoints
+*/.ipynb_checkpoints/*
+*.vscode/*
+
 # System-specific files and directories generated by the BinaryProvider and BinDeps packages
 # They contain absolute paths specific to the host computer, and so should not be committed
 deps/deps.jl
@@ -22,3 +29,38 @@ docs/site/
 # committed for packages, but should be committed for applications that require a static
 # environment.
 Manifest.toml
+
+## Core latex/pdflatex auxiliary files:
+*.aux
+*.lof
+*.log
+*.lot
+*.fls
+*.out
+*.toc
+*.fmt
+*.fot
+*.cb
+*.cb2
+.*.lb
+*.synctex.gz
+
+## Intermediate documents:
+*.dvi
+*.xdv
+*-converted-to.*
+# these rules might exclude image files for figures etc.
+# *.ps
+# *.eps
+# *.pdf
+
+## Generated if empty string is given at "Please type another file name for output:"
+# .pdf
+
+## Bibliography auxiliary files (bibtex/biblatex/biber):
+*.bbl
+*.bcf
+*.blg
+*-blx.aux
+*-blx.bib
+*.run.xml

README.md

@@ -1,34 +1,37 @@
 # [BooleanSatisfiability](https://elsoroka.github.io/BooleanSatisfiability.jl)
 
-![example workflow](https://github.com/github/docs/actions/workflows/ci.yml/badge.svg) [![codecov](https://codecov.io/gh/elsoroka/BooleanSatisfiability.jl/branch/main/graph/badge.svg?token=84BIREQL46)](https://codecov.io/gh/elsoroka/BooleanSatisfiability.jl)
+[![build status](https://github.com/elsoroka/BooleanSatisfiability.jl/actions/workflows/ci.yml/badge.svg?branch=main)](https://github.com/elsoroka/BooleanSatisfiability.jl/actions/workflows/CI.yml?query=branch%3Amain) [![docs](https://github.com/elsoroka/BooleanSatisfiability.jl/actions/workflows/docs.yml/badge.svg)](https://elsoroka.github.io/BooleanSatisfiability.jl/) [![codecov](https://codecov.io/gh/elsoroka/BooleanSatisfiability.jl/branch/main/graph/badge.svg?token=84BIREQL46)](https://codecov.io/gh/elsoroka/BooleanSatisfiability.jl)
 
-[![Build Status](https://github.com/elsoroka/BooleanSatisfiability.jl/actions/workflows/CI.yml/badge.svg?branch=main)](https://github.com/elsoroka/BooleanSatisfiability.jl/actions/workflows/CI.yml?query=branch%3Amain)
+BooleanSatisfiability.jl is a package for representing satisfiability modulo theories (SMT) problems in Julia. This package provides a simple front-end interface to common SMT solvers, including full support for vector-valued and matrix-valued expressions. Currently, the theories of propositional logic, Integers, Reals and fixed-size BitVectors are supported. We will eventually add support for all [SMT-LIB standard theories](http://smtlib.cs.uiowa.edu/theories.shtml).
 
-BooleanSatisfiability.jl is a package for representing Boolean satisfiability (SAT) and selected other satisfiability modulo theories (SMT) problems in Julia. This package provides a simple front-end interface to common SMT solvers, including full support for vector-valued and matrix-valued expressions.
+What you can do with this package:
+* Easily specify single-valued or vector-valued SMT expressions using Julia's built-in broadcasting capabilities.
+* Generate files in the [SMT-LIB](http://www.smtlib.org/) specification language.
+* Interact with any solver that follows the SMT-LIB standard.
 
-* Easily specify single-valued or vector-valued Boolean SAT, integer or real-valued SMT problems using Julia's built-in broadcasting capabilities.
-* Generate files in [SMT2](http://www.smtlib.org/) format.
-* BooleanSatisfiability.jl calls [Z3](https://www.microsoft.com/en-us/research/publication/z3-an-efficient-smt-solver/) as the back-end solver and interprets the result.
+## Examples
 
-## Example
-
-Solving the single-valued problem **(x ∧ y) ∨ (¬x ∧ y)**
-```
-x = Bool("x")
-y = Bool("y")
-expr = (x ∧ y) ∨ (¬x ∧ y)
-status = sat!(expr)
-println("x = $(value(x)), y = $(value(y))”)
-```
-
-Solving the vector-valued problem **(x1 ∧ y1) ∨ (¬x1 ∧ y1) ∧ ... ∧ (xn ∧ yn) ∨ (¬xn ∧ yn)**
+### Solving the vector-valued problem
+(x1 ∧ y1) ∨ (¬x1 ∧ y1) ∧ ... ∧ (xn ∧ yn) ∨ (¬xn ∧ yn)
 ```
 x = Bool(n, "x")
 y = Bool(n, "y")
 expr = (x .∧ y) .∨ (¬x .∧ y)
-status = sat!(expr)
+status = sat!(expr, solver=Z3())
 println("x = $(value(x)), y = $(value(y))”)
 ```
 
+### 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.
+```
+@satvariable(x, BitVector, 64)
+@satvariable(y, BitVector, 64)
+
+expr = not((~x & ~y) == ~(x | y))
+
+status = sat!(expr, solver=Z3())
+println(status) # if status is UNSAT we proved it.
+```
+
 ## Development status
 Working on a first release! Follow for updates.

TODOS.txt

@@ -69,10 +69,22 @@ Add a check at this stage so invoking the solver throws a WARNING or ERROR if th
 Add documentation about specifying a solver. Specifically, update advanced.md and the examples + tutorial - done 7/5/23
 Discuss Kochenderfer's API change for variables to match JuMP - done 7/7/23
 Update documentation to use value.(x)
-Print the error-causing solver output when a parsing error occurs - already happens
+Print the error-causing solver output when a parsing error occurs - done, already happens
 Update call_solver.jl to expose a function send_command(cmd::String; is_valid=nested_parens_match) which issues a command to an open solver process and returns the input when is_done is true. - done 7/5/23
 
 # TODO 7/8/23
 Make final API change of @satvariable to mirror JuMP @variable - done 7/8/23
-Update documentation and examples for variable macro.
+Update documentation and examples for variable macro. - done 7/12/23
 Use repo2docker to publish examples https://repo2docker.readthedocs.io/en/latest/usage.html
+
+# TODO 7/25/23
+Change @satvariable to use Bool instead of :Bool, etc. - done 7/25/23
+Use system newline in smt() - done 7/25/23
+
+# TODO 7/29/23
+and() and or() accept IntExpr type which is not permitted and doesn't match the SMT-LIB behavior. The operators \wedge and \vee correctly reject them. - fixed 8/1/23
+add an option assert=false to smt() which controls whether assert is generated - done 8/1/23
+Add README link to documentation and fix badges - fixed 8/1/23
+Fix to use z3.exe and cvc5.exe in Windows - done 7/31/23
+Fix the custom solver interactions test to use z3.exe and run on Windows - done 7/31/23
+clean up: all() should call and() and any() should call or() - done 8/1/23

docs/make.jl

@@ -20,7 +20,8 @@ pages = [
         "faq.md",
         "Examples" => [
             "example_scheduling.md",
-            "example_job_shop.md"
+            "example_job_shop.md",
+            "example_bv_lcg.md",
         ],
         "Library" => [
         "functions.md"

docs/src/advanced.md

@@ -26,7 +26,7 @@ In the SMT2 specification, after entering a problem and issuing the command `(ch
 
 Here's an example.
 ```julia
-@satvariable(x[1:2], :Bool)
+@satvariable(x[1:2], Bool)
 expr = (x[1] ∧ ¬x[1]) ∧ any(x) # unsat
 
 solver = Z3()

docs/src/example_bv_lcg.md

@@ -0,0 +1,48 @@
+# Predicting the output of a tiny LCG
+This example is "3.10.1 Cracking LCG with Z3" from *[SAT/SMT by Example](https://sat-smt.codes/SAT_SMT_by_example.pdf)* by Dennis Yurichev.
+
+A linear congruential generator (LCG) is an algorithm for generating pseudo-random numbers in which a series of transformations is used to move from one number to the next. LCGs are easy to implement using low-level bit operations, making them popular for resource-constrained embedded applications. However, they are unsuitable for many applications because their output is predictable.
+
+*SAT/SMT by Example*, example 3.10.1 shows how to predict the future output of an LCG by encoding its transformations. The original example starts with a small C program that prints the output of `rand() % 100` 10 times, producing 10 2 digit random numbers. It turns out C's rand() has this LCG implementation:
+
+1. `state = state * 214013 + 2531011`
+2. `state = (state >> 16) & 0x7FFF`
+3. `return state`
+
+Suppose we observe 10 states `n1,...,n10 = [37, 29, 74, 95, 98, 40, 23, 58, 61, 17]` from the LCG. We want to predict `n0`, the number before `n1`, and `n11`, the number after `n10`. (These are the numbers from *SAT/SMT by Example*.)
+
+```@example
+using BooleanSatisfiability
+
+@satvariable(states[1:10], BitVector, 32)
+@satvariable(output_prev, BitVector, 32)
+@satvariable(output_next, BitVector, 32)
+```
+```@example
+transitions = BoolExpr[states[i+1] == states[i] * 214013+2531011 for i=1:9]
+remainders = BoolExpr[
+    output_prev == urem(( states[1] >> 16 ) & 0x7FFF, 100),
+    urem(( states[2] >> 16) & 0x7FFF, 100) == 29,
+    urem(( states[3] >> 16) & 0x7FFF, 100) == 74,
+    urem(( states[4] >> 16) & 0x7FFF, 100) == 95,
+    urem(( states[5] >> 16) & 0x7FFF, 100) == 98,
+    urem(( states[6] >> 16) & 0x7FFF, 100) == 40,
+    urem(( states[7] >> 16) & 0x7FFF, 100) == 23,
+    urem(( states[8] >> 16) & 0x7FFF, 100) == 58,
+    urem(( states[9] >> 16) & 0x7FFF, 100) == 61,
+    output_next == urem(( states[10] >> 16) & 0x7FFF, 100),
+]
+```
+```@example
+expr = and(all(transitions), all(remainders))
+status = sat!(expr, solver=CVC5())
+println("status = $status")
+
+for (i,state) in enumerate(states)
+    println("state $i = $(value(state))")
+end
+
+# According to SAT/SMT By Example the previous output is 37 and the next output is 17.
+println("prev = $(value(output_prev))")
+println("next = $(value(output_next))")
+```

docs/src/example_job_shop.md

@@ -19,8 +19,8 @@ We'd like to find a solution such that all three jobs can be completed in an 8-h
 using BooleanSatisfiability
 n = 3 # number of jobs
 m = 2 # number of tasks per job
-@satvariable(t1[1:n], :Int)
-@satvariable(t2[1:n], :Int)
+@satvariable(t1[1:n], Int)
+@satvariable(t2[1:n], Int)
 d1 = [2; 3; 2]
 d2 = [1; 1; 3]
 ```

docs/src/example_scheduling.md

@@ -27,7 +27,7 @@ A_bar = Bool[
 ]
 
 # A is a matrix-valued variable such that ``A_{it} = 1`` if attendee ``i`` is in a meeting at time ``t`` and 0 otherwise.
-@satvariable(A[1:n, 1:T], :Bool)
+@satvariable(A[1:n, 1:T], Bool)
 
 ```
 The `index_sets` represent which meeting attendees are required at each meeting ``\mathcal{I_j}``.

docs/src/faq.md

@@ -49,16 +49,14 @@ To prevent names from being duplicated, BooleanSatisfiability.jl names new expre
 
 For example, suppose you have
 ```@example
-@satvariable(a, :Int)
-@satvariable(b, :Int)
+@satvariable(a, Int)
+@satvariable(b, Int)
 expr = a <= b
 print(smt(expr))
 ```
 The (long, ugly) name of the combined expression `a <= b` is generated by hashing the names `a` and `b`.
 
 **Q:** Why don't you just concatenate `a` and `b` and call it `LEQ_a_b`?
 
-**A:** Because what if we have `a = Int(10,"a"); expr = sum(a)`? Are we going to say `expr.name = ADD_a_1_a_2_a_3_a_4_a_5_a_6_a_7_a_8_a_9_a_10`? If not, where do we draw the line? What if we called it `ADD_a_1__a_10`, but then we defined `expr2 = a[1] + a[3:8] + a[10]`? Then both `expr` and `expr1` would share the name `ADD_a_1__a_10` and all heck would break loose.
-
-If you think of a nicer way to name expressions, please open an issue!
+**A:** Because what if we have `a = Int(10,"a"); expr = sum(a)`? Then `expr.name = ADD_a_1_a_2_a_3_a_4_a_5_a_6_a_7_a_8_a_9_a_10`. Or we could call it `ADD_a_1__a_10`, but what if then we defined `expr2 = a[1] + a[3:8] + a[10]`? It's easier to hash the names.
 

docs/src/functions.md

@@ -6,20 +6,14 @@ Depth = 3
 Test link [link](#Logical-Operations)
 
 ## Defining variables
-The preferred way to define a variable is
+Use the `@satvariable` macro to define a variable.
 ```@docs
 @satvariable
 ```
 
-This alternate syntax is also available.
-```@docs
-Bool(name::String)
-Int(name::String)
-Real(name::String)
-```
 
 ## Logical operations
-These are operations in the theory of propositional logic. For a formal definition of this theory, see Figure 3.2 in *The SMT-LIB Standard, Version 2.6*.
+These are operations in the theory of propositional logic. For a formal definition of this theory, see Figure 3.2 in *The SMT-LIB Standard, Version 2.6* or the SMT-LIB [Core theory declaration](http://smtlib.cs.uiowa.edu/theories.shtml).
 ```@docs
 not(z::BoolExpr)
 and(z1::BoolExpr, z2::BoolExpr)
@@ -49,26 +43,78 @@ Base.:/(a::RealExpr, b::RealExpr)
 ```
 
 ### Comparison operators
-`Base.==` - Method
-```julia
-    a  == b
-    a == 1.0
+These operators are available for `IntExpr`, `RealExpr`, and `BitVector` SMT variables.
+```@docs
+Base.:(==)(a::IntExpr, b::IntExpr)
+```
+For BitVector variables, the comparison operators implement unsigned comparison as defined in the SMT-LIB standard [theory of BitVectors](http://smtlib.cs.uiowa.edu/theories.shtml).
+
+```@docs
+Base.:<(a::IntExpr, b::IntExpr)
+Base.:<=(a::IntExpr, b::IntExpr)
+Base.:>(a::IntExpr, b::IntExpr)
+Base.:>=(a::IntExpr, b::IntExpr)
 ```
-Returns the Boolean expression a == b (arithmetic equivalence). Use dot broadcasting for vector-valued and matrix-valued expressions.
 
+## BitVector
 ```julia
-@satvariable(a[1:n], :Int)
-@satvariable(b[1:n, 1:m], :Int)
-a .== b
+    @satvariable(a, BitVector, 16)
+    @satvariable(b, BitVector, 12)
+
+    a + concat(bvconst(0x0, 4), b)
+```
+The SMT-LIB standard BitVector is often used to represent operations on fixed-size integers. Thus, BitVectorExprs can interoperate with Julia's native Integer, Unsigned and BigInt types.
+
+### Bitwise operators
+In addition to supporting the comparison operators above and arithmetic operators `+`, `-`, and `*`, the following BitVector-specific operators are available.
+Note that unsigned integer division is available using `div`.
+```@docs
+Base.div(a::BitVectorExpr{UInt8}, b::BitVectorExpr{UInt8})
 ```
 
-**Note:** To test whether two `AbstractExpr`s are eqivalent (in the sense that all properties are equal, not in the shared-memory-location sense of `===`), use `isequal`.
+The bitwise logical operator symbols `&`, `~` and `|` are provided for BitVector types instead of the Boolean logic symbols. This matches Julia's use of bitwise logical operators for Unsigned integer types.
+
+```@docs
+Base.:~(a::BitVectorExpr{UInt8})
+Base.:|(a::BitVectorExpr{UInt8}, b::BitVectorExpr{UInt8})
+Base.:&(a::BitVectorExpr{UInt8}, b::BitVectorExpr{UInt8})
+Base.:<<(a::BitVectorExpr{UInt8}, b::BitVectorExpr{UInt8})
+Base.:>>>(a::BitVectorExpr{UInt8}, b::BitVectorExpr{UInt8})
+urem(a::BitVectorExpr{UInt8}, b::BitVectorExpr{UInt8})
+```
+
+The following word-level operations are also available in the SMT-LIB standard.
+```@docs
+concat(a::BitVectorExpr{UInt8}, b::BitVectorExpr{UInt8})
+Base.getindex(a::BitVectorExpr{UInt8}, ind::UnitRange{Int64})
+bv2int(a::BitVectorExpr{UInt8})
+int2bv(a::IntExpr, s::Int)
+```
+
+### Utility functions for BitVectors
+```@docs
+bitcount(a::Integer)
+nextsize(n::Integer)
+bvconst(c::Integer, size::Int)
+```
+
+### Additional Z3 BitVector operators.
+Z3 implements the following signed comparisons for BitVectors. Note that these are not part of the SMT-LIB standard and other solvers may not support them.
+```@docs
+Base.:>>(a::BitVectorExpr{UInt8}, b::BitVectorExpr{UInt8})
+srem(a::BitVectorExpr{UInt8}, b::BitVectorExpr{UInt8})
+smod(a::BitVectorExpr{UInt8}, b::BitVectorExpr{UInt8})
+nor(a::BitVectorExpr{UInt8}, b::BitVectorExpr{UInt8})
+nand(a::BitVectorExpr{UInt8}, b::BitVectorExpr{UInt8})
+xnor(a::BitVectorExpr{UInt8}, b::BitVectorExpr{UInt8})
+```
 
+Signed comparisons are also Z3-specific.
 ```@docs
-Base.:<(a::AbstractExpr, b::AbstractExpr)
-Base.:<=(a::AbstractExpr, b::AbstractExpr)
-Base.:>(a::AbstractExpr, b::AbstractExpr)
-Base.:>=(a::AbstractExpr, b::AbstractExpr)
+slt(a::BitVectorExpr{UInt8}, b::BitVectorExpr{UInt8})
+sle(a::BitVectorExpr{UInt8}, b::BitVectorExpr{UInt8})
+sgt(a::BitVectorExpr{UInt8}, b::BitVectorExpr{UInt8})
+sge(a::BitVectorExpr{UInt8}, b::BitVectorExpr{UInt8})
 ```
 
 ## Generating the SMT representation of a problem

docs/src/installation.md

@@ -12,7 +12,7 @@ You can install the latest version of BooleanSatisfiability with the command
 (TODO) Add official way when package is published.
 
 ## Installing a Solver
-BooleanSatisfiability uses Julia's Base.Process library to interact with solvers. Thus to successfully install a solver for this package, all you need to do is make sure the appropriate command (listed below) works in your machine's terminal.
+BooleanSatisfiability uses Julia's Base.Process library to interact with solvers. Thus to successfully install a solver for this package, all you need to do is make sure the appropriate command works in your machine's terminal.
 
 ### Debian Linux
 **To install Z3**, use `sudo apt-get install z3`.
@@ -28,4 +28,15 @@ If you can launch cvc5 from the command line by typing `cvc5 --interactive --pro
 (TODO)
 
 ### Windows
-(TODO)
+**To install Z3**
+* Download the appropriate zip file for the [latest Z3 release](https://github.com/Z3Prover/z3/releases).
+* Unzip the file and put it in your applications folder.
+* Find z3.exe. Typically this will be in a bin file in your unzipped folder. Don't move it, but make a note of this file path.
+* Add the z3.exe file path to your PATH environment variable ([here's how to do this](https://helpdeskgeek.com/windows-10/add-windows-path-environment-variable/)).
+If you can open the WIndows command line and launch z3 by typing `z3.exe -smt2 -in`, your installation is correct.
+
+**To install cvc5**
+* Download the [latest release](https://github.com/cvc5/cvc5/releases/) of cvc5. Make sure you save the exe file as `cvc5.exe`, not `cvc5-Win64.exe` or anything else.
+* Make a note of the file path where you put cvc5.exe.
+* Add the cvc5.exe file path to your PATH environment variable ([here's how to do this](https://helpdeskgeek.com/windows-10/add-windows-path-environment-variable/)).
+If you can open the Windows command line and launch cvc5 by typing `cvc5 --interactive --produce-models`, your installation is correct.