diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 1a3bd99..bc78fb8 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -1,4 +1,4 @@ -name: Workflow for Codecov example-julia +name: CI on: push: branches: diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index b546215..6cb2175 100644 --- a/.github/workflows/docs.yml +++ b/.github/workflows/docs.yml @@ -1,4 +1,4 @@ -name: Build and Deploy Documentation +name: docs # https://github.com/julia-actions/julia-docdeploy on: push: diff --git a/.gitignore b/.gitignore index 29126e4..312b302 100644 --- a/.gitignore +++ b/.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 \ No newline at end of file diff --git a/README.md b/README.md index 05c67bf..e3b8876 100644 --- a/README.md +++ b/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. diff --git a/TODOS.txt b/TODOS.txt index 0e056ad..99444ce 100644 --- a/TODOS.txt +++ b/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 \ No newline at end of file diff --git a/docs/make.jl b/docs/make.jl index a721475..0efa0b9 100644 --- a/docs/make.jl +++ b/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" diff --git a/docs/src/advanced.md b/docs/src/advanced.md index c58fb8b..ba022b2 100644 --- a/docs/src/advanced.md +++ b/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() diff --git a/docs/src/example_bv_lcg.md b/docs/src/example_bv_lcg.md new file mode 100644 index 0000000..6de7616 --- /dev/null +++ b/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))") +``` diff --git a/docs/src/example_job_shop.md b/docs/src/example_job_shop.md index 9313d4e..c59e5a9 100644 --- a/docs/src/example_job_shop.md +++ b/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] ``` diff --git a/docs/src/example_scheduling.md b/docs/src/example_scheduling.md index e79f880..8768230 100644 --- a/docs/src/example_scheduling.md +++ b/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}``. diff --git a/docs/src/faq.md b/docs/src/faq.md index 52cfdd6..1bc3807 100644 --- a/docs/src/faq.md +++ b/docs/src/faq.md @@ -49,8 +49,8 @@ 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)) ``` @@ -58,7 +58,5 @@ The (long, ugly) name of the combined expression `a <= b` is generated by hashin **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. diff --git a/docs/src/functions.md b/docs/src/functions.md index 2e90f1a..ce4fdbd 100644 --- a/docs/src/functions.md +++ b/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 diff --git a/docs/src/installation.md b/docs/src/installation.md index 9a2430d..52bfbe4 100644 --- a/docs/src/installation.md +++ b/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) \ No newline at end of file +**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. diff --git a/docs/src/tutorial.md b/docs/src/tutorial.md index dba4fd3..ea943e9 100644 --- a/docs/src/tutorial.md +++ b/docs/src/tutorial.md @@ -8,19 +8,20 @@ We say a formula is **valid** if it is true for every assignment of values to it One famous transformation is De Morgan's law: `a ∧ b = ¬(¬a ∨ ¬b)`. To show validity of De Morgan's law, we can construct the bidirectional implication `a ∧ b ⟺ ¬(¬a ∨ ¬b)`. It suffices to show that the negation of this formula is unsatisfiable. ```@example -@satvariable(a, :Bool) -@satvariable(b, :Bool) +@satvariable(a, Bool) +@satvariable(b, Bool) conjecture = iff(a ∧ b, ¬(¬a ∨ ¬b)) status = sat!(¬conjecture, Z3()) # status will be either :SAT or :UNSAT ``` + ## A common logical mistake Suppose you have Boolean variables `p`, `q` and `r`. A common mistake made by students in discrete math classes is to think that if `p` implies `q` and `q` implies `r` (`(p ⟹ q) ∧ (q ⟹ r)`) then `p` must imply `r` (`p ⟹ r`). Are these statements equivalent? We can use a SAT solver to check. ```@example -@satvariable(p, :Bool) -@satvariable(q, :Bool) -@satvariable(r, :Bool) +@satvariable(p, Bool) +@satvariable(q, Bool) +@satvariable(r, Bool) conjecture = iff((p ⟹ q) ∧ (q ⟹ r), p ⟹ r) status = sat!(¬conjecture, Z3()) @@ -40,7 +41,7 @@ A simpler version, illustrated in this [classic XKCD strip](https://xkcd.com/287 In fact, the problem in the XKCD strip can be expressed as a linear equation over integers. ```@example -@satvariable(a[1:6], :Bool) +@satvariable(a[1:6], Bool) c = [215; 275; 335; 355; 420; 580] expr = and([all(a .>= 0), sum(a .* c) == 1505]) sat!(expr, Z3()) @@ -48,4 +49,19 @@ println("Result: $(value(a))") println("Check: $(sum(value(a) .* c))") ``` +## Proving properties of fixed-size integer arithmetic +This example is from Microsoft's [Z3 tutorial](https://microsoft.github.io/z3guide/docs/theories/Bitvectors/). +A bitvector `x` is a power of two (or zero) if and only if `x & (x - 1)` is zero, where & is bitwise and. We prove this property for an 8-bit vector. + +```@example +println("Example 1 (should be SAT)") +@satvariable(b, BitVector, 8) +is_power_of_two = b & (b - 0x01) == 0 +# iff is_power_of_two holds, b must be one of 1, 2, 4, ... 128 +expr = iff(is_power_of_two, + any([b == 2^i for i=0:7])) +status = sat!(expr) +#println(smt(expr)) +println(status) # if status is SAT we proved it. +``` diff --git a/examples/bv_lcg.jl b/examples/bv_lcg.jl new file mode 100644 index 0000000..fe3e0e3 --- /dev/null +++ b/examples/bv_lcg.jl @@ -0,0 +1,46 @@ +# This example is from "SAT/SMT by Example" by Dennis Yurichev. It is example 3.10.1 Cracking LCG with Z3. +# A linear congruential generator (LCG) is an algorithm for generating pseudo-random numbers. A series of transformations is used to move from one number to the next +# LCGs are simple to implement using low-level bit operations. In SAT/SMT by example, +# Mr. Yurichev dumps the assmbly code for a small loop that prints `rand() % 100` (in C) 10 times. +# He finds the following LCG code: + +# 1. `tmp := state * 214013 + 2531011` +# 2. `state = tmp` +# 3. `(state >> 16) & 0x7FFF` +# 4. `return state` + +# Now 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. +# The following code does exactly that. +using BooleanSatisfiability + +@satvariable(states[1:10], BitVector, 32) +@satvariable(output_prev, BitVector, 32) +@satvariable(output_next, BitVector, 32) + +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), +] + +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 +println("prev = $(value(output_prev))") +println("next = $(value(output_next))") + +# According to Mr. Yurichev's example, the previous output is 37 and the next output is 17! +# This matches on my machine using Z3 and CVC5. diff --git a/examples/bv_mini.jl b/examples/bv_mini.jl new file mode 100644 index 0000000..35d79a5 --- /dev/null +++ b/examples/bv_mini.jl @@ -0,0 +1,30 @@ +push!(LOAD_PATH, "../src") +push!(LOAD_PATH, "./") +using BooleanSatisfiability + +# https://microsoft.github.io/z3guide/docs/theories/Bitvectors/ +# There is a fast way to check that fixed size numbers are powers of two. +# A bitvector x is a power of two or zero if and only if x & (x - 1) is zero, +# where & represents the bitwise and. We check this for 8 bits. +println("Example 1 (should be SAT)") +@satvariable(b, BitVector, 8) +is_power_of_two = b & (b - 0x01) == 0 + +# iff is_power_of_two holds, b must be one of 1, 2, 4, ... 128 +expr = iff(is_power_of_two, + any([b == 2^i for i=0:7])) +status = sat!(expr) +#println(smt(expr)) +println(status) # if status is SAT we proved it. + + +# Here is another mini example: 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. +println("Example 2 (should be UNSAT)") +@satvariable(x, BitVector, 64) +@satvariable(y, BitVector, 64) + +expr = not((~x & ~y) == ~(x | y)) + +status = sat!(expr) +println(status) # if status is UNSAT we proved it. diff --git a/examples/job_shop_scheduling.jl b/examples/job_shop_scheduling.jl index 778f666..b270783 100644 --- a/examples/job_shop_scheduling.jl +++ b/examples/job_shop_scheduling.jl @@ -16,8 +16,8 @@ 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] diff --git a/examples/mini_example.jl b/examples/mini_example.jl index 7235391..a77cf24 100644 --- a/examples/mini_example.jl +++ b/examples/mini_example.jl @@ -4,9 +4,9 @@ using BooleanSatisfiability # let's define a matrix of Boolean statements n = 3 m = 2 -@satvariable(x[1:m, 1:n], :Bool) -@satvariable(y[1:m, 1:n], :Bool) -@satvariable(z[1:n], :Bool) +@satvariable(x[1:m, 1:n], Bool) +@satvariable(y[1:m, 1:n], Bool) +@satvariable(z[1:n], Bool) # At each step, either x or y has to be true expr1 = all(x .∨ y) .∨ and.(¬z, z) diff --git a/examples/schedule_example.jl b/examples/schedule_example.jl index 265b742..197c2bb 100644 --- a/examples/schedule_example.jl +++ b/examples/schedule_example.jl @@ -26,7 +26,7 @@ A_bar = Bool[ index_sets = [[1,2,3], [3,4,5], [1,3,5], [1,4]] J = length(index_sets) # number of meetings -@satvariable(A[1:n, 1:T], :Bool) +@satvariable(A[1:n, 1:T], Bool) unavailability = and(¬A_bar .⟹ ¬A) diff --git a/examples/scheduling_example.ipynb b/examples/scheduling_example.ipynb index 406ba36..6c17759 100644 --- a/examples/scheduling_example.ipynb +++ b/examples/scheduling_example.ipynb @@ -120,8 +120,7 @@ } ], "source": [ - "A = Bool(n,T,\"A\")\n", - "value(A)\n", + "@satvariable(A[1:n, 1:T], Bool)\n", "\n", "#past_availability = all(¬A_bar .⟹ ¬A)\n", "booked = BoolExpr[]\n", diff --git a/src/BitVectorExpr.jl b/src/BitVectorExpr.jl new file mode 100644 index 0000000..72a22d0 --- /dev/null +++ b/src/BitVectorExpr.jl @@ -0,0 +1,555 @@ +import Base.getindex, Base.setproperty! +import Base.+, Base.-, Base.*, Base.<<, Base.>>, Base.>>>, Base.div, Base.&, Base.|, Base.~, Base.nor, Base.nand +import Base.>, Base.>=, Base.<, Base.<=, Base.== +# >>> is arithmetic shift right, corresponding to bvashr in SMT-LIB +# >> is logical shift right, bvlshr in SMT-LIB +# << is logical shift left, bvshl in SMT-LIB +# where operators exist (or, and, not, xor) +# Base.rem and Base.% both implement the remainder in integer division. + +# This design decision supports subclasses of AbstractBitVectorExpr +# which is used to represent SMT-LIB extract (indexing) of BitVectors +abstract type AbstractBitVectorExpr <: AbstractExpr end + +mutable struct BitVectorExpr{T<:Integer} <: AbstractBitVectorExpr + op :: Symbol + children :: Array{AbstractExpr} + value :: Union{T, Nothing, Missing} + name :: String + length :: Int + __is_commutative :: Bool + + BitVectorExpr{T}(op::Symbol, + children::Array{C}, + value::Union{T, Nothing, Missing}, + name::String, + length::Int; + __is_commutative = false) where T <: Integer where C <: AbstractExpr = new(op, children, value, name, length, __is_commutative) +end + +mutable struct SlicedBitVectorExpr{T<:Integer} <: AbstractBitVectorExpr + op :: Symbol + children :: Array{AbstractExpr} + value :: Union{T, Nothing, Missing} + name :: String + length :: Int + __is_commutative :: Bool # this doesn't mean anything here and is always false + range :: Union{UnitRange{I}, I} where I <: Integer +end + +""" + BitVector("a", n) + + Construct a single BitVector variable with name "a" and length n. Note that unlike Bool, Int, and Real, one cannot construct an array of BitVectors. + The length n may be any positive integer. +""" +function BitVectorExpr(name::String, length::Int) + global GLOBAL_VARNAMES + global WARN_DUPLICATE_NAMES + if name ∈ GLOBAL_VARNAMES[BitVectorExpr] + if WARN_DUPLICATE_NAMES @warn("Duplicate variable name $name of type BitVector") end + else + push!(GLOBAL_VARNAMES[BitVectorExpr], name) + end + return BitVectorExpr{nextsize(length)}(:identity, AbstractExpr[], nothing, "$name", length) +end + + +# some utility functions +"""" + nextsize(n::Integer) + +Returns the smallest unsigned integer type that can store a number with n bits. +If n is larger than the largest available type (`UInt128`), returns type `BigInt`. +""" +function nextsize(n::Integer) # works on BigInt and UInt + if sign(n) == -1 + @error("Constants must be unsigned or positive BigInts!") + end + sz = 2^Integer((round(log2(n), RoundUp, digits=0))) + sz = max(sz, 8) # sizes smaller than 8 get 8 bits + if sz > 128 + return BigInt + else + return eval(Symbol("UInt$sz")) # returns the correct size of int + end +end + +"""" + bitcount(a::Integer) + +Returns the minimum number of bits required to store the number `a`. +""" +function bitcount(a::Integer) # works on BigInt and UInt + if a == 0 + return 1 + end + if sign(a) == -1 + @error("Constants must be unsigned or positive BigInts!") + end + result = findlast((x) -> x != 0, a .>> collect(0:8*sizeof(a))) + return result +end + +function hexstr(a::Integer, ReturnType::Type) + if sign(a) == -1 + @error("Constants must be unsigned or positive BigInts!") + end + return string(a, base=16, pad=sizeof(ReturnType)*2) +end + + +function __bvnop(op::Function, opname::Symbol, ReturnType::Type, es::Array{T}; __is_commutative=false, __try_flatten=false) where T <: AbstractBitVectorExpr + # This expression comes about because while SMT-LIB supports any length bit vector, + # we store the value in Julia as a standard size. So you have to mask any extra bits away. + value = nothing + values = getproperty.(es, :value) + if all(.!(isnothing.(values))) + # We are guaranteed es all have the same type by our type signature + value = op(values...) + end + + children, name = __combine(es, opname, __is_commutative, __try_flatten) + if ReturnType <: AbstractBitVectorExpr + return ReturnType{nextsize(es[1].length)}(opname, children, value, name, es[1].length, __is_commutative=__is_commutative) + else # it must be a BoolExpr or IntExpr + return ReturnType(opname, children, value, name) + end +end + +function __bv1op(e::AbstractBitVectorExpr, op::Function, opname::Symbol, l=nothing) + l = isnothing(l) ? e.length : l + value = nothing + if !isnothing(e.value) + valtype = typeof(e.value) + mask = typemax(valtype) >> (8*sizeof(valtype) - e.length) + value = valtype(op(e.value) & mask) + end + name = __get_hash_name(opname, [e,]) + return BitVectorExpr{nextsize(e.length)}(opname, [e,], value, name, l) +end + + +##### Integer arithmetic ##### + ++(e1::T, e2::T) where T <: AbstractBitVectorExpr = __bvnop(+, :bvadd, BitVectorExpr, [e1, e2], __is_commutative=true, __try_flatten=true) +-(e1::T, e2::T) where T <: AbstractBitVectorExpr = __bvnop(-, :bvsub, BitVectorExpr, [e1, e2]) +*(e1::T, e2::T) where T <: AbstractBitVectorExpr = __bvnop(*, :bvmul, BitVectorExpr, [e1, e2],__is_commutative=true, __try_flatten=true) + +""" + div(a::BitVectorExpr, b::BitVectorExpr) + +Unsigned integer division of two BitVectors. +""" +div(e1::AbstractBitVectorExpr, e2::AbstractBitVectorExpr) = __bvnop(div, :bvudiv, BitVectorExpr, [e1, e2]) + +# unary minus, this is an arithmetic minus not a bit flip. +-(e::BitVectorExpr) = __bv1op(e, -, :bvneg) + +# NOTE: Julia rem(a, b) and a%b return the unsigned remainder when a and b are unsigned +# the signed arithmetic is done when a and b are signed +# We do not implement % (modulus) because it could result in confusion +# The reason is Julia naturally prints unsigned integers in hex notation +# This matches how people usually think of BitVectors. So we store values as unsigned +# and cast to signed when necessary. +# But Julia decides whether to the unsigned or signed arithmetic based on the variable type +# while SMT-LIB defines only signed modulo, bvsmod. Thus it is confusing to implement Base.% or Base.rem +# We define urem and srem for the unsigned and signed things, respectively. + +# Yikes! A function that returns a function. +__signfix(f::Function) = (a, b) -> unsigned(f(signed(a), signed(b))) + +# these all have arity 2 +""" + urem(a::BitVectorExpr, b::BitVectorExpr) + +Unsigned remainder of BitVector a divided by BitVector b. +""" +urem(e1::T, e2::T) where T <: AbstractBitVectorExpr = __bvnop(rem, :bvurem, BitVectorExpr, [e1, e2]) + +""" + a << b + +Logical left shift a << b. +""" +<<(e1::T, e2::T) where T <: AbstractBitVectorExpr = __bvnop(<<, :bvshl, BitVectorExpr, [e1, e2]) # shift left + +""" + a >>> b + +Logical right shift a >>> b. +""" +>>>(e1::T, e2::T) where T <: AbstractBitVectorExpr = __bvnop(>>>, :bvlshr, BitVectorExpr, [e1, e2]) # logical shift right + +# Extra arithmetic operators supported by Z3 but not part of the SMT-LIB standard. + +""" + srem(a::BitVectorExpr, b::BitVectorExpr) + +Signed remainder of BitVector a divided by BitVector b. This operator is not part of the SMT-LIB standard BitVector theory: it is implemented by Z3. It may not be available when using other solvers. +""" +srem(e1::T, e2::T) where T <: AbstractBitVectorExpr = __bvnop(__signfix(rem), :bvsrem, BitVectorExpr, [e1, e2]) # unique to z3 + +""" + smod(a::BitVectorExpr, b::BitVectorExpr) + +Signed modulus of BitVector a divided by BitVector b. This operator is not part of the SMT-LIB standard BitVector theory: it is implemented by Z3. It may not be available when using other solvers. +""" +smod(e1::T, e2::T) where T <: AbstractBitVectorExpr = __bvnop(__signfix(mod), :bvsmod, BitVectorExpr, [e1, e2]) # unique to z3 + +""" + a >> b + +Arithmetic right shift a >> b. This operator is not part of the SMT-LIB standard BitVector theory: it is implemented by Z3. It may not be available when using other solvers. +""" +>>(e1::AbstractBitVectorExpr, e2::AbstractBitVectorExpr) = __bvnop(__signfix(>>), :bvashr, BitVectorExpr, [e1, e2]) # arithmetic shift right - unique to Z3 + + +##### Bitwise logical operations (arity n>=2) ##### +function or(es::Array{T}, consts=Integer[]) where T <: AbstractBitVectorExpr + if length(consts)>0 + push!(es, bvconst(reduce(|, consts), es[1].length)) + end + expr = __bvnop((a,b) -> a | b, :bvor, BitVectorExpr, es, __is_commutative=true, __try_flatten=true) + return expr +end + +or(zs::Vararg{Union{T, Integer}}) where T <: AbstractBitVectorExpr = or(collect(zs)) +# We need this declaration to enable the syntax and.([z1, z2,...,zn]) where z1, z2,...,zn are broadcast-compatible + +function and(es::Array{T}, consts=Integer[]) where T <: AbstractBitVectorExpr + if length(consts)>0 + push!(es, bvconst(reduce(&, consts), es[1].length)) + end + expr = __bvnop((a,b) -> a & b, :bvand, BitVectorExpr, es, __is_commutative=true, __try_flatten=true) + return expr +end + +and(zs::Vararg{Union{T, Integer}}) where T <: AbstractBitVectorExpr = and(collect(zs)) +# We need this declaration to enable the syntax and.([z1, z2,...,zn]) where z1, z2,...,zn are broadcast-compatible + +""" + a | b + or(a, b, c...) + +Bitwise or. For n>2 variables, use the or(...) notation. +""" +(|)(e1::AbstractBitVectorExpr, e2::AbstractBitVectorExpr) = or([e1, e2]) + +""" + a & b + and(a, b, c...) + +Bitwise and. For n>2 variables, use the and(...) notation. +""" +(&)(e1::AbstractBitVectorExpr, e2::AbstractBitVectorExpr) = and([e1, e2]) + +# Extra logical operators supported by Z3 but not part of the SMT-LIB standard. +""" + nor(a, b) + a ⊽ b + +Bitwise nor. This operator is not part of the SMT-LIB standard BitVector theory: it is implemented by Z3. It may not be available when using other solvers. When using other solvers, write ~(a | b) isntead of nor(a,b). +""" +nor(e1::AbstractBitVectorExpr, e2::AbstractBitVectorExpr) = __bvnop((a,b) -> ~(a | b), :bvnor, BitVectorExpr, [e1, e2], __is_commutative=true) +⊽(e1::AbstractBitVectorExpr, e2::AbstractBitVectorExpr) = nor(e1, e2) + +""" + nand(a, b) + a ⊼ b + +Bitwise nand. This operator is not part of the SMT-LIB standard BitVector theory: it is implemented by Z3. It may not be available when using other solvers. When using other solvers, write ~(a & b) isntead of nand(a,b). +""" +nand(e1::AbstractBitVectorExpr, e2::AbstractBitVectorExpr) = __bvnop((a,b) -> ~(a & b), :bvnand, BitVectorExpr, [e1, e2], __is_commutative=true) +⊼(e1::AbstractBitVectorExpr, e2::AbstractBitVectorExpr) = nand(e1, e2) + + +# note that bvxnor is left-accumulating, so bvxnor(a, b, c) = bvxnor(bvxnor(a, b), c) +# bvnor and bvnand have arity 2 +xnor(a::T,b::T) where T <: Integer = (a & b) | (~a & ~b) + +function xnor(es_mixed::Array{T}) where T + es_mixed = collect(es_mixed) + vars, consts = __check_inputs_nary_op(es_mixed, const_type=Integer, expr_type=BitVectorExpr) + if isnothing(vars) || length(vars)==0 + return reduce(xnor, consts) + end + + es = map((e) -> isa(e, Integer) ? bvconst(e, vars[1].length) : e, es_mixed) + expr = __bvnop(xnor, :bvxnor, BitVectorExpr, es) + return expr +end + +""" + xnor(a, b) + xnor(a, b, c...) + +Bitwise xnor. When n>2 operands are provided, xnor is left-associative (that is, `xnor(a, b, c) = reduce(xnor, [a,b,c])`. This operator is not part of the SMT-LIB standard BitVector theory: it is implemented by Z3. It may not be available when using other solvers. When using other solvers, write (a & b) | (~a & ~b). +""" +xnor(zs::Vararg{Union{T, Integer}}) where T <: AbstractBitVectorExpr = xnor(collect(zs)) +# We need this declaration to enable the syntax and.([z1, z2,...,zn]) where z1, z2,...,zn are broadcast-compatible + +""" + ~a + +Bitwise not. +""" +~(e::BitVectorExpr) = __bv1op(e, ~, :bvnot) + +##### Bitwise predicates ##### +<(e1::T, e2::T) where T <: AbstractBitVectorExpr = __bvnop(>, :bvult, BoolExpr, [e1, e2]) +<=(e1::T, e2::T) where T <: AbstractBitVectorExpr = __bvnop(>=, :bvule, BoolExpr, [e1, e2]) +>(e1::AbstractBitVectorExpr, e2::AbstractBitVectorExpr) = __bvnop(>, :bvugt, BoolExpr, [e1, e2]) +>=(e1::AbstractBitVectorExpr, e2::AbstractBitVectorExpr) = __bvnop(>=, :bvuge, BoolExpr, [e1, e2]) + +(==)(e1::AbstractBitVectorExpr, e2::AbstractBitVectorExpr) = __bvnop((==), :eq, BoolExpr, [e1, e2]) + +# Signed comparisons are supported by Z3 but not part of the SMT-LIB standard. +"""" + slt(a::BitVectorExpr, b::BitVectorExpr) + +Signed less-than. This is not the same as a < b (unsigned BitVectorExpr comparison). This operator is not part of the SMT-LIB standard BitVector theory: it is implemented by Z3. It may not be available when using other solvers. +""" +slt(e1::AbstractBitVectorExpr, e2::AbstractBitVectorExpr) = __bvnop(__signfix(>), :bvslt, BoolExpr, [e1, e2]) + +""" + sle(a::BitVectorExpr, b::BitVectorExpr) + +Signed less-than-or-equal. This is not the same as a <+ b (unsigned BitVectorExpr comparison). This operator is not part of the SMT-LIB standard BitVector theory: it is implemented by Z3. It may not be available when using other solvers. +""" +sle(e1::AbstractBitVectorExpr, e2::AbstractBitVectorExpr) = __bvnop(__signfix(>=), :bvsle, BoolExpr, [e1, e2]) + +""" + sgt(a::BitVectorExpr, b::BitVectorExpr) + +Signed greater-than. This is not the same as a > b (unsigned BitVectorExpr comparison). This operator is not part of the SMT-LIB standard BitVector theory: it is implemented by Z3. It may not be available when using other solvers. +""" +sgt(e1::AbstractBitVectorExpr, e2::AbstractBitVectorExpr) = __bvnop(__signfix(>), :bvsgt, BoolExpr, [e1, e2]) + +""" + sge(a::BitVectorExpr, b::BitVectorExpr) + +Signed greater-than-or-equal. This is not the same as a >= b (unsigned BitVectorExpr comparison). This operator is not part of the SMT-LIB standard BitVector theory: it is implemented by Z3. It may not be available when using other solvers. +""" +sge(e1::AbstractBitVectorExpr, e2::AbstractBitVectorExpr) = __bvnop(__signfix(>=), :bvsge, BoolExpr, [e1, e2]) + + +##### Word-level operations ##### +# concat and extract are the only SMT-LIB standard operations +# z3 adds some more, note that concat can accept constants and has arity n >= 2 +""" + concat(a, b) + concat(a, bvconst(0xffff, 16), b, bvconst(0x01, 8), ...) + concat(bvconst(0x01, 8), bvconst(0x02, 12)...) + +Concatenate BitVectorExprs and constants of varying sizes. To guarantee a constant is the correct bit size, it should be wrapped using bvconst - otherwise its size will be inferred using `bitcount`. + +concat(a,b) returns a BitVector with size a.length + b.length. + +Arguments are concatenated such that the first argument to concat corresponds to the most significant bits of the resulting value. Thus: +```julia + expr = concat(bvconst(0x01, 8), bvconst(0x02, 8), bvconst(0x03, 4)) + println(expr.length) # 20 + println(expr.value) # 0x01023 +``` +""" +function concat(es_mixed::Vararg{Any}) + es_mixed = collect(es_mixed) + vars, consts = __check_inputs_nary_op(es_mixed, const_type=Integer, expr_type=BitVectorExpr) + # only consts + if isnothing(vars) || length(vars)==0 + return concat(consts) + end + + # preserve order of inputs + es = map((e) -> isa(e, Integer) ? bvconst(e, bitcount(e)) : e, es_mixed) + + lengths = getproperty.(es, :length) + l = sum(lengths) + ReturnType = nextsize(l) + + values = getproperty.(es, :value) + value = any(isnothing.(values)) ? nothing : __concat(values, lengths, ReturnType) + + name = __get_hash_name(:concat, es) + + return BitVectorExpr{ReturnType}(:concat, collect(es), value, name, l) +end + +# for constant values +function concat(vals::Array{T}) where T <: Integer + lengths = map(bitcount, vals) + return __concat(vals, lengths, nextsize(sum(lengths))) +end +function __concat(vals::Array{T}, bitsizes::Array{R}, ReturnType::Type) where T <: Integer where R <: Integer + value = ReturnType(0) # this generates an unsigned int or BigInt of the appropriate size + acc = sum(bitsizes) + for (v, s) in zip(vals, bitsizes) + acc -= s + value |= ReturnType(v) << acc + end + return value +end + + +##### INDEXING ##### +# SMT-LIB indexing is called extract and works in a slightly weird manner +# Here we enable indexing using the Julia slice operator. + +Base.getindex(e::AbstractBitVectorExpr, ind_1::Int64, ind_2::Int64) = getindex(e, UnitRange(ind_1, ind_2)) +Base.getindex(e::AbstractBitVectorExpr, ind::Int64) = getindex(e, ind, ind) + +""" + @satvariable(a, BitVector, 8) + a[4:8] # has length 5 + a[3] + +Slice or index into a BitVector, returning a new BitVector with the appropriate length. This corresponds to the SMT-LIB operation `extract`. +""" +function Base.getindex(e::AbstractBitVectorExpr, ind::UnitRange{Int64}) + if first(ind) > last(ind) || first(ind) < 1 || last(ind) > e.length + error("Cannot extract sequence $ind from BitVector!") + end + + # typeof(e).parameters[1] returns the type of the first parameter to the parametric type of e + ReturnIntType = typeof(e).parameters[1] + v = isnothing(e.value) ? nothing : e.value & ReturnIntType(reduce(|, map((i) -> 2^(i-1), ind))) + + # the SMT-LIB operator is (_ extract $(last(ind)) $(first(ind))) + return SlicedBitVectorExpr{ReturnIntType}(:extract, [e], v, __get_hash_name(:extract, [e]), length(ind), false, ind) +end + + +##### Translation to/from integer ##### +# Be aware these have high overhead +""" + @satvariable(b, BitVector, 8) + a = bv2int(b) + +Wrap BitVectorExpr b, representing a conversion to IntExpr. The value of the integer expression will be limited by the size of the wrapped BitVector. This operation has high overhead and may impact solver performance. +""" +bv2int(e::AbstractBitVectorExpr) = IntExpr(:bv2int, [e,], isnothing(e.value) ? nothing : Int(e.value), __get_hash_name(:bv2int, [e])) + +""" + @satvariable(a, Int) + b = int2bv(a, 8) + +Wrap IntExpr a, representing a conversion to a BitVector of specified length. This operation has high overhead and may impact solver performance. + +""" +function int2bv(e::IntExpr, size::Int) + name = __get_hash_name(:int2bv, [e]) + expr = BitVectorExpr{nextsize(size)}(:int2bv, [e], isnothing(e.value) ? nothing : unsigned(e.value), name, size) + return expr +end + + +##### INTEROPERABILITY WITH CONSTANTS ##### +# RULE +# Given a variable with sort (_ BitVec n) and a const with sort (_ BitVec m) +# as long as m ≤ n any operation with the same size output is valid (except concat which adds them) +# Short constants will be padded with zeros because this matches Julia's behavior. + +# size must be the SMT-LIB bitvector length, for example if you have a bitvector of length 12 pass in 12 NOT 16 +# this function returns c of the correct Unsigned type to interoperate with the bitvector.value +# which is the smallest Unsigned type that fits the SMT-LIB bitvector length. +""" + bvconst(0x01, 32) + bvconst(2, 8) + +Wraps a nonnegative integer constant for interoperability with BitVectorExprs. While the correct size of a BitVector constant can usually be inferred (for example, if `a` is a BitVector of length 16, the constant in `a + 0x0f` can also be wrapped to length 16), in a few cases it cannot. + +Specifically, when concatenating BitVectorExprs and constants, one should wrap the constants in `bvconst` to ensure their size matches your expectations. + +`bvconst` will pad constants to the requested size, but will not truncate constants. For example, `bvconst(0xffff, 12)` yields an error because `0xffff`` requires 16 bits. + +""" +function bvconst(c::Integer, size::Int) + if c < 0 + error("Cannot combine negative integer constant $c with BitVector") + end + + minsize = bitcount(c) + # nextsize(size) returns the correct Unsigned type + ReturnType = nextsize(size) + if minsize > size + error("BitVector of size $size cannot be combined with constant of size $minsize") + elseif minsize == size + return BitVectorExpr{ReturnType}(:const, AbstractExpr[], ReturnType(c), "const_0x$(hexstr(c, ReturnType))", size) + else # it's smaller and we need to pad it + return BitVectorExpr{ReturnType}(:const, AbstractExpr[], ReturnType(c), "const_0x$(hexstr(c, ReturnType))", size) + end +end +# Constants, to match Julia conventions, may be specified in binary, hex, or octal. +# Constants may be specified in base 10 as long as they are explicitly constructed to be of type Unsigned or BigInt. +# Examples: 0xDEADBEEF (UInt32), 0b0101 (UInt8), 0o7700 (UInt16), big"123456789012345678901234567890" (BigInt) +# Consts can be padded, so for example you can add 0x01 (UInt8) to (_ BitVec 16) +# Variables cannot be padded! For example, 0x0101 (Uint16) cannot be added to (_ BitVec 8). + + +__2ops = [:+, :-, :*, :/, :<, :<=, :>, :>=, :sle, :slt, :sge, :sgt, :nand, :nor, :<<, :>>, :>>>, :&, :|, :~, :srem, :urem, :smod] + +for op in __2ops + @eval $op(a::Integer, b::AbstractBitVectorExpr) = $op(bvconst(a, b.length), b) + @eval $op(a::AbstractBitVectorExpr, b::Integer) = $op(a, bvconst(b, a.length)) +end + +(==)(e::AbstractBitVectorExpr, c::Integer) = e == bvconst(c, e.length) +(==)(c::Integer, e::AbstractBitVectorExpr) = bvconst(c, e.length) == e + +##### CONSTANT VERSIONS (for value propagation) ##### + +function __trim_bits!(e::AbstractBitVectorExpr) + mask = typemax(typeof(e.value)) >> (8*sizeof(typeof(e.value)) - e.length) + e.value = e.value & mask +end + +__bitvector_const_ops = Dict( + :bvudiv => div, + :bvshl => (<<), + :bvlshr => (>>>), + :bvashr => __signfix(>>), + :bvand => (&), + :bvor => (|), + :bvnot => ~, + :bvneg => -, + :bvadd => +, + :bvsub => -, + :bvmul => *, + :bvurem => rem, + :bvsrem => __signfix(rem), + :bvsmod => __signfix(mod), + :bvnor => (a,b) -> ~(a & b), + :bvnand => (a,b) -> ~(a & b), + :bvxnor => (vals) -> reduce(xnor, vals), + :bvult => <, + :bvule => <=, + :bvugt => >=, + :bvuge => >, + :bvslt => __signfix(<), + :bvsle => __signfix(<=), + :bvsgt => __signfix(>=), + :bvsge => __signfix(>), +) + +# We overload this function from sat.jl to specialize it +# This is for propagating the values back up in __assign! (called when a problem is sat and a satisfying assignment is found). + +function __propagate_value!(z::AbstractBitVectorExpr) + vs = getproperty.(z.children, :value) + + # special cases + if z.op == :concat + ls = getproperty.(z.children, :length) + z.value = __concat(vs, ls, nextsize(z.length)) + elseif z.op == :int2bv + z.value = nextsize(z.length)(z.children[1].value) + elseif z.op == :extract + ReturnIntType = typeof(z).parameters[1] + v = z.children[1].value + z.value = v & ReturnIntType(reduce(|, map((i) -> 2^(i-1), z.range))) + else + op = __bitvector_const_ops[z.op] + z.value = length(vs)>1 ? op(vs...) : op(vs[1]) + end +end \ No newline at end of file diff --git a/src/BoolExpr.jl b/src/BoolExpr.jl index c4051ee..c95b4be 100644 --- a/src/BoolExpr.jl +++ b/src/BoolExpr.jl @@ -5,37 +5,35 @@ import Base.length, Base.size, Base.show, Base.string, Base.isequal, Base.hash, # Define the Variable object abstract type AbstractExpr end -# op: :IDENTITY (variable only, no operation), :NOT, :AND, :OR, :XOR, :IFF, :IMPLIES, :ITE (if-then-else) +# op: :identity (variable only, no operation), :not, :and, :or, :xor, :iff, :implies, :ite (if-then-else) # children: BoolExpr children for an expression. And(z1, z2) has children [z1, z2] # value: Bool array or nothing if result not computed -# name: String name of variable / expression. Can get long, we're working on that. +# name: String name of variable / expression. +# __is_commutative: true if AbstractExpr is a commutative operator, false if not. mutable struct BoolExpr <: AbstractExpr op :: Symbol children :: Array{AbstractExpr} value :: Union{Bool, Nothing, Missing} name :: String + __is_commutative :: Bool + + # for convenience + BoolExpr(op::Symbol, + children::Array{T}, + value::Union{Bool, Nothing, Missing}, + name::String; + __is_commutative = false) where T <: AbstractExpr = new(op, children, value, name, __is_commutative) end -# define a type that accepts Array{T, Bool}, Array{Bool}, and Array{T} -# ExprArray{T} = Union{Array{Union{T, Bool}}, Array{T}, Array{Bool}} ##### CONSTRUCTORS ##### """ - Bool("z") +BoolExpr("z") Construct a single Boolean variable with name "z". - -```julia - Bool(n, "z") - Bool(m, n, "z") -``` - -Construct a vector-valued or matrix-valued Boolean variable with name "z". - -Vector and matrix-valued Booleans use Julia's built-in array functionality: calling `Bool(n,"z")` returns a `Vector{BoolExpr}`, while calling `Bool(m, n, "z")` returns a `Matrix{BoolExpr}`. """ -function Bool(name::String) :: BoolExpr +function BoolExpr(name::String) :: BoolExpr # This unsightly bit enables warning when users define two variables with the same string name. global GLOBAL_VARNAMES global WARN_DUPLICATE_NAMES @@ -44,53 +42,7 @@ function Bool(name::String) :: BoolExpr else push!(GLOBAL_VARNAMES[BoolExpr], name) end - return BoolExpr(:IDENTITY, Array{AbstractExpr}[], nothing, "$(name)") -end -# may eventually be removed in favor of macros -Bool(n::Int, name::String) :: Vector{BoolExpr} = BoolExpr[Bool("$(name)_$(i)") for i=1:n] -Bool(m::Int, n::Int, name::String) :: Matrix{BoolExpr} = BoolExpr[Bool("$(name)_$(i)_$(j)") for i=1:m, j=1:n] - - - -__valid_vartypes = [:Bool, :Int, :Real] -""" - @satvariable(z, :Bool) - @satvariable(a[1:n], :Int) - -Construct a SAT variable with name z, optional array dimensions, and specified type (`:Bool`, `:Int` or `:Real`). - -One and two-dimensional variables can be constructed with the following syntax. -```julia -@satvariable(a[1:n], :Int) # an Int vector of length n -@satvariable(x[1:m, 1:n], :Real) # an m x n Int matrix -``` -""" -macro satvariable(expr, exprtype) - # check exprtype - if !isa(exprtype, QuoteNode) || !(exprtype.value ∈ __valid_vartypes) # unknown - @error "Unknown expression type $exprtype" - end - - # inside here name and t are exprs - if isa(expr, Symbol) # one variable, eg @Bool(x) - name = string(expr) - # this line resolves to something like x = Bool("x") - return esc(:($expr = $(exprtype.value)($name))) - - elseif length(expr.args) == 2 && isa(expr.args[1], Symbol) - stem = expr.args[1] - name = string(stem) - iterable = expr.args[2] - - return esc(:($stem = [$(exprtype.value)("$(:($$name))_$(i)") for i in $iterable])) - elseif length(expr.args) == 3 - stem = expr.args[1] - name = string(stem) - iterable1, iterable2 = expr.args[2], expr.args[3] - return esc(:($stem = [$(exprtype.value)("$(:($$name))_$(i)_$(j)") for i in $iterable1, j in $iterable2])) - else - @error "Unable to create Bool from expression $expr. Recommended usage: \"@Bool(x)\", \"@Bool(x[1:n])\", or \"@Bool(x[1:m, 1:n])\"." - end + return BoolExpr(:identity, AbstractExpr[], nothing, "$(name)") end @@ -106,7 +58,7 @@ Base.show(io::IO, expr::AbstractExpr) = print(io, string(expr)) # This helps us print nested exprs function Base.string(expr::AbstractExpr, indent=0)::String - if expr.op == :IDENTITY + if expr.op == :identity return "$(repeat(" | ", indent))$(expr.name)$(isnothing(expr.value) ? "" : " = $(expr.value)")\n" else res = "$(repeat(" | ", indent))$(expr.name)$(isnothing(expr.value) ? "" : " = $(expr.value)")\n" @@ -117,20 +69,21 @@ function Base.string(expr::AbstractExpr, indent=0)::String end end -# Utility functions -include("ops.jl") - "Test equality of two AbstractExprs. To construct an equality constraint, use `==`." function Base.isequal(expr1::AbstractExpr, expr2::AbstractExpr) return (expr1.op == expr2.op) && all(expr1.value .== expr2.value) && (expr1.name == expr2.name) && - (expr1.op ∈ __commutative_ops ? __is_permutation(expr1.children, expr2.children) : ((length(expr1.children) == length(expr2.children)) && all(isequal.(expr1.children, expr2.children)))) + (expr1.__is_commutative ? __is_permutation(expr1.children, expr2.children) : ((length(expr1.children) == length(expr2.children)) && all(isequal.(expr1.children, expr2.children)))) end # Required for isequal apparently, since isequal(expr1, expr2) implies hash(expr1) == hash(expr2). -function Base.hash(expr::AbstractExpr) - return hash("$(show(expr))") +function Base.hash(expr::AbstractExpr, h::UInt) + if length(expr.children)>0 + return hash(expr.op, hash(expr.__is_commutative, hash(hash(expr.children, h), h))) + else + return hash(expr.op, hash(expr.__is_commutative, hash(expr.name, h))) + end end # Overload because Base.in uses == which se used to construct equality expressions diff --git a/src/BooleanOperations.jl b/src/BooleanOperations.jl index 753eac2..53b4000 100644 --- a/src/BooleanOperations.jl +++ b/src/BooleanOperations.jl @@ -5,35 +5,38 @@ include("utilities.jl") ##### NAMING COMBINED BOOLEXPRS ##### -"Given an array of named BoolExprs with indices, returns the name stem with no indices. -Example: array with names z_1_1,...,z_m_n returns string z" -function __get_name_stem(zs::Array{T}) where T <: AbstractExpr - if length(size(zs)) == 1 - return zs[1].name[1:end-2] # since the name here will be name_1 - elseif length(size(zs)) == 2 - return zs[1].name[1:end-4] - else - error("Array of size $(size(zs)) not supported.") - end -end - "Given an array of named BoolExprs, returns a combined name for use when naming exprs that have multiple children. Example: array with names z_1_1,...,z_m_n returns string z_1_1...z_m_n if m*n>max_items. If m*n <= max_items, all names are listed." -function __get_combined_name(zs::Array{T}; max_items=3) where T <: AbstractExpr - names = sort(vec(getproperty.(zs, :name))) - if length(names) > max_items - return "$(names[1])_to_$(names[end])" +function __get_combined_name(zs::Array{T}; is_commutative=false) where T <: AbstractExpr + if is_commutative + names = sort(vec(getproperty.(zs, :name))) else - return join(names, "__") + names = vec(getproperty.(zs, :name)) end + return join(names, "__") end -function __get_hash_name(op::Symbol, zs::Array{T}) where T <: AbstractExpr - combined_name = __get_combined_name(zs, max_items=Inf) +function __get_hash_name(op::Symbol, zs::Array{T}; is_commutative=false) where T <: AbstractExpr + combined_name = __get_combined_name(zs, is_commutative=is_commutative)# TODO should sort when op is commutative return "$(op)_$(string(hash(combined_name), base=16))" end +# combine children for Boolean n-ary ops +function __bool_nary_op(zs::Array{T}, op::Symbol, ReturnType::Type, __is_commutative=false, __try_flatten=false) where T <: BoolExpr + if length(zs) == 1 + return zs[1] + end + children, name = __combine(zs, op, __is_commutative, __try_flatten) + if __is_commutative && length(children)>1 # clear duplicates + children = unique(children) + name = __get_hash_name(op, children, is_commutative=__is_commutative) + end + # TODO here we should compute the value + return ReturnType(op, children, nothing, name, __is_commutative=__is_commutative) +end + + ##### LOGICAL OPERATIONS ##### """ @@ -45,13 +48,13 @@ Return the logical negation of `z`. Note: Broacasting a unary operator requires the syntax `.¬z` which can be confusing to new Julia users. We define `¬(z::Array{BoolExpr})` for convenience. ```julia - @satvariable(z[1:n], :Bool) + @satvariable(z[1:n], Bool) ¬z # syntactic sugar for map(¬, z) .¬z # also valid ``` """ -not(z::BoolExpr) = BoolExpr(:NOT, [z], isnothing(z.value) ? nothing : !(z.value), __get_hash_name(:NOT, [z])) +not(z::BoolExpr) = BoolExpr(:not, [z], isnothing(z.value) ? nothing : !(z.value), __get_hash_name(:not, [z])) not(zs::Array{T}) where T <: BoolExpr = map(not, zs) ¬(z::BoolExpr) = not(z) ¬(zs::Array{T}) where T <: BoolExpr = not(zs) @@ -60,10 +63,7 @@ not(zs::Array{T}) where T <: BoolExpr = map(not, zs) ∨(z1::BoolExpr, z2::BoolExpr) = or([z1, z2]) -function and(zs_mixed::Array{T}; broadcast_type=:Elementwise) where T - - zs, literals = __check_inputs_nary_op(zs_mixed) - +function and(zs::Array{T}, literals=Bool[]) where T <: BoolExpr if length(literals) > 0 if !all(literals) # if any literal is 0 return false @@ -71,17 +71,12 @@ function and(zs_mixed::Array{T}; broadcast_type=:Elementwise) where T return true end end - # having passed this processing of literals, we'll check for base cases - if length(zs) == 0 - return nothing - elseif length(zs) == 1 - return zs[1] - end - + # now the remaining are BoolExpr - child_values = getproperty.(zs, :value) - value = any(isnothing.(child_values)) ? nothing : reduce(&, child_values) - return BoolExpr(:AND, zs, value, __get_hash_name(:AND, zs)) + expr = __bool_nary_op(zs, :and, BoolExpr, true, true) + values = getproperty.(expr.children, :value) + expr.value = length(values) > 0 && !any(isnothing.(values)) ? reduce(&, values) : nothing + return expr end """ @@ -92,8 +87,8 @@ end Returns the logical AND of two or more variables. Use dot broadcasting for vector-valued and matrix-valued Boolean expressions. ```julia -@satvariable(z1[1:n], :Bool) -@satvariable(z2[n, 1:m], :Bool) +@satvariable(z1[1:n], Bool) +@satvariable(z2[n, 1:m], Bool) z1 .∧ z2 and.(z1, z2) # equivalent to z1 .∧ z2 ``` @@ -103,12 +98,10 @@ Special cases: * `and(z, false)` returns `false`. * `and(z, true)` returns `z`. """ -and(zs::Vararg{Union{T, Bool}}; broadcast_type=:Elementwise) where T <: AbstractExpr = and(collect(zs)) +and(zs::Vararg{Union{T, Bool}}) where T <: BoolExpr = and(collect(zs)) # We need this declaration to enable the syntax and.([z1, z2,...,zn]) where z1, z2,...,zn are broadcast-compatible -function or(zs_mixed::Array{T}; broadcast_type=:Elementwise) where T - zs, literals = __check_inputs_nary_op(zs_mixed) - +function or(zs::Array{T}, literals=Bool[]) where T <: BoolExpr if length(literals) > 0 if any(literals) # if any literal is 1 return true @@ -116,16 +109,11 @@ function or(zs_mixed::Array{T}; broadcast_type=:Elementwise) where T return false end end - # having passed this processing of literals, we'll check for base cases - if length(zs)== 0 - return nothing - elseif length(zs) == 1 - return zs[1] - end - child_values = getproperty.(zs, :value) - value = any(isnothing.(child_values)) ? nothing : reduce(|, child_values) - return BoolExpr(:OR, zs, value, __get_hash_name(:OR, zs)) + expr = __bool_nary_op(zs, :or, BoolExpr, true, true) + values = getproperty.(expr.children, :value) + expr.value = length(values) > 0 && !any(isnothing.(values)) ? reduce(|, values) : nothing + return expr end """ @@ -136,8 +124,8 @@ end Returns the logical OR of two or more variables. Use dot broadcasting for vector-valued and matrix-valued Boolean expressions. ```julia -@satvariable(z1[1:n], :Bool) -@satvariable(z2[1:m, 1:n], :Bool) +@satvariable(z1[1:n], Bool) +@satvariable(z2[1:m, 1:n], Bool) z1 .∨ z2 or.(z1, z2) # equivalent to z1 .∨ z2 ``` @@ -149,7 +137,7 @@ Special cases: **Note that ∨ (`\\vee`) is NOT the ASCII character v.** """ -or(zs::Vararg{Union{T, Bool}}; broadcast_type=:Elementwise) where T <: AbstractExpr = or(collect(zs)) +or(zs::Vararg{Union{T, Bool}}) where T <: BoolExpr = or(collect(zs)) # We need this declaration to enable the syntax or.([z1, z2,...,zn]) where z1, z2,...,z are broadcast-compatible ##### ADDITIONAL OPERATORS IN THE SMT BOOL CORE SPEC ##### @@ -167,32 +155,32 @@ Special cases: * `xor(true, true, z)` returns `false`. """ function xor(zs_mixed::Array{T}; broadcast_type=:Elementwise) where T - zs, literals = __check_inputs_nary_op(zs_mixed) + zs, literals = __check_inputs_nary_op(zs_mixed, expr_type=BoolExpr) if length(literals) > 0 if sum(literals)>1 # more than one literal is true, so xor automatically is false return false - elseif sum(literals) == 1 && length(zs) > 0 # exactly one literal is true and there are variables - # conversion is needed because zs has type Array{AbstractExpr} when it's returned from __check_inputs_nary_op - return and(¬convert(Array{BoolExpr}, zs)) # then all variables must be false - elseif length(zs) == 0 # only literals - return xor(literals...) + elseif sum(literals) == 1 + if length(zs) > 0 # exactly one literal is true and there are variables + # conversion is needed because zs has type Array{AbstractExpr} when it's returned from __check_inputs_nary_op + return and(¬convert(Array{BoolExpr}, zs)) # then all variables must be false + else # only literals + return true + end end - end - # having passed this processing of literals, we'll check for base cases - if length(zs)== 0 - return nothing - elseif length(zs) == 1 - return zs[1] + # if sum(literals) == 0 they're all false so we move on end + expr = __bool_nary_op(zs, :xor, BoolExpr, true, false) child_values = getproperty.(zs, :value) - value = any(isnothing.(child_values)) ? nothing : reduce(xor, child_values) - return BoolExpr(:XOR, zs, value, __get_hash_name(:XOR, zs)) + expr.value = any(isnothing.(child_values)) ? nothing : xor(child_values) + return expr end # We need this extra line to enable the syntax xor.([z1, z2,...,zn]) where z1, z2,...,z are broadcast-compatible -xor(zs::Vararg{Union{T, Bool}}; broadcast_type=:Elementwise) where T <: AbstractExpr = xor(collect(zs)) +xor(zs::Vararg{Union{T, Bool}}) where T <: AbstractExpr = xor(collect(zs)) + # this is the const version +xor(values::Union{BitVector, Array{T}}) where T <: Bool = sum(values) == 1 """ z1 ⟹ z2 @@ -202,8 +190,8 @@ Returns the expression z1 IMPLIES z2. Use dot broadcasting for vector-valued and """ function implies(z1::BoolExpr, z2::BoolExpr) zs = BoolExpr[z1, z2] - value = isnothing(z1.value) || isnothing(z2.value) ? nothing : !(z1.value) | z2.value - return BoolExpr(:IMPLIES, zs, value, __get_hash_name(:IMPLIES, zs)) + value = isnothing(z1.value) || isnothing(z2.value) ? nothing : implies(z1.value, z2.value) + return BoolExpr(:implies, zs, value, __get_hash_name(:implies, zs)) end """ @@ -214,11 +202,10 @@ Bidirectional implication between z1 and z2. Equivalent to `and(z1 ⟹ z2, z2 """ function iff(z1::BoolExpr, z2::BoolExpr) zs = BoolExpr[z1, z2] - value = isnothing(z1.value) || isnothing(z2.value) ? nothing : z1.value == z2.value - return BoolExpr(:IFF, zs, value, __get_hash_name(:IFF, zs)) + value = isnothing(z1.value) || isnothing(z2.value) ? nothing : iff(z1.value, z2.value) + return BoolExpr(:iff, zs, value, __get_hash_name(:iff, zs), __is_commutative=true) end -⟺(z1::Union{BoolExpr, Bool}, z2::Union{BoolExpr, Bool}) = iff(z1, z2) """ ite(x::BoolExpr, y::BoolExpr, z::BoolExpr) @@ -232,7 +219,7 @@ function ite(x::Union{BoolExpr, Bool}, y::Union{BoolExpr, Bool}, z::Union{BoolEx end value = any(isnothing.([x.value, y.value, z.value])) ? nothing : (x.value & y.value) | (!(x.value) & z.value) - return BoolExpr(:ITE, zs, value, __get_hash_name(:ITE, zs)) + return BoolExpr(:ite, zs, value, __get_hash_name(:ite, zs)) end @@ -263,44 +250,14 @@ implies(z1::Bool, z2::BoolExpr) = z1 ? z2 : true # not(z1) or z2 implies(z1::BoolExpr, z2::Bool) = z2 ? true : not(z1) # not(z1) or z2 implies(z1::Bool, z2::Bool) = !z1 | z2 +⟺(z1::Union{BoolExpr, Bool}, z2::Union{BoolExpr, Bool}) = iff(z1, z2) iff(z1::BoolExpr, z2::Bool) = z2 ? z1 : ¬z1 # if z2 is true z1 must be true and if z2 is false z1 must be false iff(z1::Bool, z2::BoolExpr) = z1 ? z2 : ¬z2 iff(z1::Bool, z2::Bool) = z1 == z2 - ##### ADDITIONAL OPERATIONS ##### -"combine is used for both all() and any() since those are fundamentally the same with different operations." -function __combine(zs::Array{T}, op::Symbol) where T <: BoolExpr - if length(zs) == 0 - error("Cannot iterate over zero-length array.") - elseif length(zs) == 1 - return zs[1] - end - - # Now we need to take an array of statements and decide how to combine them - if all(getproperty.(zs, :op) .== :IDENTITY) - children = flatten(zs) - name = __get_hash_name(op, zs) - elseif all(getproperty.(zs, :op) .== op) - # if op matches (e.g. any(or(z1, z2)) or all(and(z1, z2))) then flatten it. - # Returm a combined operator - # this line gets a list with no duplicates of all children - children = union(cat(map( (e) -> flatten(e.children), zs)..., dims=1)) - name = __get_hash_name(op, children) - else # op doesn't match, so we won't flatten it but will combine all the children - name = __get_hash_name(op, zs) - children = flatten(zs) - end - - return BoolExpr(op, children, nothing, name) -end - -"combine(z, op) where z is an n x m matrix of BoolExprs first flattens z, then combines it with op. -combine([z1 z2; z3 z4], or) = or([z1; z2; z3; z4])." -__combine(zs::Matrix{T}, op::Symbol) where T <: BoolExpr = __combine(flatten(zs), op) - """ all([z1,...,zn]) @@ -310,12 +267,7 @@ Examples: * `and([and(z1, z2), and(z3, z4)]) == and(z1, z2, z3, z4)` * `and([or(z1, z3), z3, z4]) == and(or(z1, z3), z3, z4)` """ -function all(zs::Array{T}) where T <: BoolExpr - expr = __combine(zs, :AND) - values = getproperty.(expr.children, :value) - expr.value = length(values) > 0 && !any(isnothing.(values)) ? reduce(&, values) : nothing - return expr -end +all(zs::Array{T}) where T <: BoolExpr = and(zs) """ any([z1,...,zn]) @@ -325,13 +277,7 @@ Examples: * `any([or(z1, z2), or(z3, z4)]) == or(z1, z2, z3, z4)` * `any([and(z1, z3), z3, z4]) == or(and(z1, z3), z3, z4)` """ -function any(zs::Array{T}) where T <: BoolExpr - expr = __combine(zs, :OR) - values = getproperty.(expr.children, :value) - expr.value = length(values) > 0 && !any(isnothing.(values)) ? reduce(|, values) : nothing - return expr -end - +any(zs::Array{T}) where T <: BoolExpr = or(zs) """ value(z::BoolExpr) diff --git a/src/BooleanSatisfiability.jl b/src/BooleanSatisfiability.jl index 625215e..dcb023c 100644 --- a/src/BooleanSatisfiability.jl +++ b/src/BooleanSatisfiability.jl @@ -5,6 +5,8 @@ export AbstractExpr, IntExpr, @satvariable, RealExpr, + AbstractBitVectorExpr, + BitVectorExpr, isequal, hash, # required by isequal (?) in # specialize to use isequal instead of == @@ -18,12 +20,34 @@ export iff, ⟺, ite, value + export ==, <, <=, >, >= export +, -, *, / +# BitVector specific functions +export + nextsize, + bitcount, + div, + urem, + <<, + >>, + >>>, + &, |, ~, + srem, + smod, + nor, + nand, + xnor, + slt, sle, + sgt, sge, + concat, + bv2int, int2bv, + bvconst + export smt, save @@ -55,12 +79,17 @@ include("BooleanOperations.jl") =# include("IntExpr.jl") +include("BitVectorExpr.jl") + +# include @satvariable later because we need some functions from BitVector to declare that type +include("smt_macros.jl") +include("multiple_dispatch_ops.jl") -__EXPR_TYPES = [BoolExpr, RealExpr, IntExpr] +__EXPR_TYPES = [BoolExpr, RealExpr, IntExpr, BitVectorExpr] # Track the user-declared BoolExpr names so the user doesn't make duplicates. # This will NOT contain hash names. If the user declares x = Bool("x"); y = Bool("y"); xy = and(x,y) -# GLOBAL_VARNAMES will contain "x" and "y", but not __get_hash_name(:AND, [x,y]). +# GLOBAL_VARNAMES will contain "x" and "y", but not __get_hash_name(:AND, [x,y], is_commutative=true). global GLOBAL_VARNAMES = Dict(t => String[] for t in __EXPR_TYPES) # When false, no warnings will be issued global WARN_DUPLICATE_NAMES = false diff --git a/src/IntExpr.jl b/src/IntExpr.jl index 5efd3e3..eb04941 100644 --- a/src/IntExpr.jl +++ b/src/IntExpr.jl @@ -1,4 +1,3 @@ -import Base.Int, Base.Real import Base.<, Base.<=, Base.>, Base.<=, Base.+, Base.-, Base.*, Base./, Base.== abstract type NumericExpr <: AbstractExpr end @@ -9,23 +8,23 @@ mutable struct IntExpr <: NumericExpr children :: Array{AbstractExpr} value :: Union{Int, Bool, Nothing, Missing} name :: String + __is_commutative :: Bool + + # for convenience + IntExpr(op::Symbol, + children::Array{T}, + value::Union{Int, Bool, Nothing, Missing}, + name::String; + __is_commutative = false) where T <: AbstractExpr = new(op, children, value, name, __is_commutative) end -""" - Int("a") - -Construct a single Int variable with name "a". -```julia - Int(n, "a") - Int(m, n, "a") -``` - -Construct a vector-valued or matrix-valued Int variable with name "a". +""" +IntExpr("a") -Vector and matrix-valued Ints use Julia's built-in array functionality: calling `Int(n,"a")` returns a `Vector{IntExpr}`, while calling `Int(m, n, "a")` returns a `Matrix{IntExpr}`. +Construct a single IntExpr variable with name "a". """ -function Base.Int(name::String) :: IntExpr +function IntExpr(name::String) :: IntExpr # This unsightly bit enables warning when users define two variables with the same string name. global GLOBAL_VARNAMES global WARN_DUPLICATE_NAMES @@ -34,34 +33,31 @@ function Base.Int(name::String) :: IntExpr else push!(GLOBAL_VARNAMES[IntExpr], name) end - return IntExpr(:IDENTITY, Array{AbstractExpr}[], nothing, "$(name)") + return IntExpr(:identity, AbstractExpr[], nothing, "$(name)") end -Int(n::Int, name::String) :: Vector{IntExpr} = IntExpr[Int("$(name)_$(i)") for i=1:n] -Int(m::Int, n::Int, name::String) :: Matrix{IntExpr} = IntExpr[Int("$(name)_$(i)_$(j)") for i=1:m, j=1:n] mutable struct RealExpr <: NumericExpr op :: Symbol children :: Array{AbstractExpr} - value :: Union{Float64, Bool, Nothing, Missing} + value :: Union{Float64, Nothing, Missing} name :: String + __is_commutative :: Bool + + # for convenience + RealExpr(op::Symbol, + children::Array{T}, + value::Union{Float64, Nothing, Missing}, + name::String; + __is_commutative = false) where T <: AbstractExpr = new(op, children, value, name, __is_commutative) end """ - Real("r") - -Construct a single Int variable with name "r". +RealExpr("r") -```julia - Real(n, "r") - Real(m, n, "r") -``` - -Construct a vector-valued or matrix-valued Real variable with name "r". - -Vector and matrix-valued Reals use Julia's built-in array functionality: calling `Real(n,"a")` returns a `Vector{RealExpr}`, while calling `Real(m, n, "r")` returns a `Matrix{RealExpr}`. +Construct a single Real variable with name "r". """ -function Base.Real(name::String) :: RealExpr +function RealExpr(name::String) :: RealExpr # This unsightly bit enables warning when users define two variables with the same string name. global GLOBAL_VARNAMES global WARN_DUPLICATE_NAMES @@ -70,10 +66,8 @@ function Base.Real(name::String) :: RealExpr else push!(GLOBAL_VARNAMES[RealExpr], name) end - return RealExpr(:IDENTITY, Array{AbstractExpr}[], nothing, "$(name)") + return RealExpr(:identity, AbstractExpr[], nothing, "$(name)") end -Real(n::Int, name::String) :: Vector{RealExpr} = RealExpr[Real("$(name)_$(i)") for i=1:n] -Real(m::Int, n::Int, name::String) :: Matrix{RealExpr} = RealExpr[Real("$(name)_$(i)_$(j)") for i=1:m, j=1:n] # These are necessary for defining interoperability between IntExpr, RealExpr, BoolExpr and built-in types such as Int, Bool, and Float. @@ -81,8 +75,8 @@ NumericInteroperableExpr = Union{NumericExpr, BoolExpr} NumericInteroperableConst = Union{Bool, Int, Float64} NumericInteroperable = Union{NumericInteroperableExpr, NumericInteroperableConst} -__wrap_const(c::Float64) = RealExpr(:CONST, AbstractExpr[], c, "const_$c") -__wrap_const(c::Union{Int, Bool}) = IntExpr(:CONST, AbstractExpr[], c, "const_$c") +__wrap_const(c::Float64) = RealExpr(:const, AbstractExpr[], c, "const_$c") +__wrap_const(c::Union{Int, Bool}) = IntExpr(:const, AbstractExpr[], c, "const_$c") ##### COMPARISON OPERATIONS #### @@ -95,17 +89,17 @@ __wrap_const(c::Union{Int, Bool}) = IntExpr(:CONST, AbstractExpr[], c, "const_$c Returns the Boolean expression a < b. Use dot broadcasting for vector-valued and matrix-valued expressions. ```julia -@satvariable(a[1:n], :Int) -@satvariable(b[1:n, 1:m], :Int) +@satvariable(a[1:n], Int) +@satvariable(b[1:n, 1:m], Int) a .< b -@satvariable(z, :Bool) +@satvariable(z, Bool) a .< z ``` """ -function Base.:<(e1::AbstractExpr, e2::AbstractExpr) +function Base.:<(e1::NumericInteroperableExpr, e2::NumericInteroperableExpr) value = isnothing(e1.value) || isnothing(e2.value) ? nothing : e1.value < e2.value - name = __get_hash_name(:LT, [e1, e2]) - return BoolExpr(:LT, [e1, e2], value, name) + name = __get_hash_name(:lt, [e1, e2]) + return BoolExpr(:lt, [e1, e2], value, name) end """ @@ -115,17 +109,17 @@ end Returns the Boolean expression a <= b. Use dot broadcasting for vector-valued and matrix-valued expressions. ```julia -@satvariable(a[1:n], :Int) -@satvariable(b[1:n, 1:m], :Int) +@satvariable(a[1:n], Int) +@satvariable(b[1:n, 1:m], Int) a .<= b -@satvariable(z, :Bool) +@satvariable(z, Bool) a .<= z ``` """ -function Base.:<=(e1::AbstractExpr, e2::AbstractExpr) +function Base.:<=(e1::NumericInteroperableExpr, e2::NumericInteroperableExpr) value = isnothing(e1.value) || isnothing(e2.value) ? nothing : e1.value <= e2.value - name = __get_hash_name(:LEQ, [e1, e2]) - return BoolExpr(:LEQ, [e1, e2], value, name) + name = __get_hash_name(:leq, [e1, e2]) + return BoolExpr(:leq, [e1, e2], value, name) end """ @@ -135,17 +129,17 @@ end Returns the Boolean expression a >= b. Use dot broadcasting for vector-valued and matrix-valued expressions. ```julia -@satvariable(a[1:n], :Int) -@satvariable(b[1:n, 1:m], :Int) +@satvariable(a[1:n], Int) +@satvariable(b[1:n, 1:m], Int) a .>= b -@satvariable(z, :Bool) +@satvariable(z, Bool) a .>= z ``` """ -function Base.:>=(e1::AbstractExpr, e2::AbstractExpr) +function Base.:>=(e1::NumericInteroperableExpr, e2::NumericInteroperableExpr) value = isnothing(e1.value) || isnothing(e2.value) ? nothing : e1.value >= e2.value - name = __get_hash_name(:GEQ, [e1, e2]) - return BoolExpr(:GEQ, [e1, e2], value, name) + name = __get_hash_name(:geq, [e1, e2]) + return BoolExpr(:geq, [e1, e2], value, name) end """ @@ -155,17 +149,17 @@ end Returns the Boolean expression a > b. Use dot broadcasting for vector-valued and matrix-valued expressions. ```julia -@satvariable(a[1:n], :Int) -@satvariable(b[1:n, 1:m], :Int) +@satvariable(a[1:n], Int) +@satvariable(b[1:n, 1:m], Int) a .> b -@satvariable(z, :Bool) +@satvariable(z, Bool) a .> z ``` """ -function Base.:>(e1::AbstractExpr, e2::AbstractExpr) +function Base.:>(e1::NumericInteroperableExpr, e2::NumericInteroperableExpr) value = isnothing(e1.value) || isnothing(e2.value) ? nothing : e1.value > e2.value - name = __get_hash_name(:GT, [e1, e2]) - return BoolExpr(:GT, [e1, e2], value, name) + name = __get_hash_name(:gt, [e1, e2]) + return BoolExpr(:gt, [e1, e2], value, name) end # IMPORTANT NOTE @@ -180,32 +174,32 @@ end Returns the Boolean expression a == b (arithmetic equivalence). Use dot broadcasting for vector-valued and matrix-valued expressions. ```julia -@satvariable(a[1:n], :Int) -@satvariable(b[1:n, 1:m], :Int) +@satvariable(a[1:n], Int) +@satvariable(b[1:n, 1:m], Int) a .== b ``` **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`. """ -function Base.:(==)(e1::T, e2::T) where T <: AbstractExpr +function Base.:(==)(e1::NumericInteroperableExpr, e2::NumericInteroperableExpr) value = isnothing(e1.value) || isnothing(e2.value) ? nothing : e1.value == e2.value - name = __get_hash_name(:EQ, [e1, e2]) - return BoolExpr(:EQ, [e1, e2], value, name) + name = __get_hash_name(:eq, [e1, e2], is_commutative=true) + return BoolExpr(:eq, [e1, e2], value, name, __is_commutative=true) end # INTEROPERABILITY FOR COMPARISON OPERATIONS -Base.:>(e1::AbstractExpr, e2::NumericInteroperableConst) = e1 > __wrap_const(e2) -Base.:>(e1::NumericInteroperableConst, e2::AbstractExpr) = __wrap_const(e1) > e2 -Base.:>=(e1::AbstractExpr, e2::NumericInteroperableConst) = e1 >= __wrap_const(e2) -Base.:>=(e1::NumericInteroperableConst, e2::AbstractExpr) = __wrap_const(e1) >= e2 +Base.:>(e1::NumericInteroperableExpr, e2::NumericInteroperableConst) = e1 > __wrap_const(e2) +Base.:>(e1::NumericInteroperableConst, e2::NumericInteroperableExpr) = __wrap_const(e1) > e2 +Base.:>=(e1::NumericInteroperableExpr, e2::NumericInteroperableConst) = e1 >= __wrap_const(e2) +Base.:>=(e1::NumericInteroperableConst, e2::NumericInteroperableExpr) = __wrap_const(e1) >= e2 -Base.:<(e1::AbstractExpr, e2::NumericInteroperableConst) = e1 < __wrap_const(e2) -Base.:<(e1::NumericInteroperableConst, e2::AbstractExpr) = __wrap_const(e1) < e2 -Base.:<=(e1::AbstractExpr, e2::NumericInteroperableConst) = e1 <= __wrap_const(e2) -Base.:<=(e1::NumericInteroperableConst, e2::AbstractExpr) = __wrap_const(e1) <= e2 +Base.:<(e1::NumericInteroperableExpr, e2::NumericInteroperableConst) = e1 < __wrap_const(e2) +Base.:<(e1::NumericInteroperableConst, e2::NumericInteroperableExpr) = __wrap_const(e1) < e2 +Base.:<=(e1::NumericInteroperableExpr, e2::NumericInteroperableConst) = e1 <= __wrap_const(e2) +Base.:<=(e1::NumericInteroperableConst, e2::NumericInteroperableExpr) = __wrap_const(e1) <= e2 -Base.:(==)(e1::AbstractExpr, e2::NumericInteroperableConst) = e1 == __wrap_const(e2) -Base.:(==)(e1::NumericInteroperableConst, e2::AbstractExpr) = __wrap_const(e1) == e2 +Base.:(==)(e1::NumericInteroperableExpr, e2::NumericInteroperableConst) = e1 == __wrap_const(e2) +Base.:(==)(e1::NumericInteroperableConst, e2::NumericInteroperableExpr) = __wrap_const(e1) == e2 ##### UNARY OPERATIONS ##### @@ -216,13 +210,13 @@ Base.:(==)(e1::NumericInteroperableConst, e2::AbstractExpr) = __wrap_const(e1) = Return the negative of an Int or Real expression. ```julia -@satvariable(a[1:n, 1:m], :Int) +@satvariable(a[1:n, 1:m], Int) -a # this also works ``` """ -Base.:-(e::IntExpr) = IntExpr(:NEG, IntExpr[e,], isnothing(e.value) ? nothing : -e.value, __get_hash_name(:NEG, [e,])) -Base.:-(e::RealExpr) = RealExpr(:NEG, RealExpr[e,], isnothing(e.value) ? nothing : -e.value, __get_hash_name(:NEG, [e,])) +Base.:-(e::IntExpr) = IntExpr(:neg, IntExpr[e,], isnothing(e.value) ? nothing : -e.value, __get_hash_name(:neg, [e,])) +Base.:-(e::RealExpr) = RealExpr(:neg, RealExpr[e,], isnothing(e.value) ? nothing : -e.value, __get_hash_name(:neg, [e,])) # Define array version for convenience because the syntax .- for unary operators is confusing. Base.:-(es::Array{T}) where T <: NumericExpr = .-es @@ -232,59 +226,47 @@ Base.:-(es::Array{T}) where T <: NumericExpr = .-es # These return Int values. We would say they have sort Int. # See figure 3.3 in the SMT-LIB standard. -# If literal is != 0, add a :CONST expr to es representing literal +# If literal is != 0, add a :const expr to es representing literal function __add_const!(es::Array{T}, literal::Real) where T <: AbstractExpr if literal != 0 - const_expr = isa(literal, Float64) ? RealExpr(:CONST, AbstractExpr[], literal, "const_$literal") : IntExpr(:CONST, AbstractExpr[], literal, "const_$literal") + const_expr = isa(literal, Float64) ? RealExpr(:const, AbstractExpr[], literal, "const_$literal") : IntExpr(:const, AbstractExpr[], literal, "const_$literal") push!(es, const_expr) end end -# If there is more than one :CONST expr in es, merge them into one +# If there is more than one :const expr in es, merge them into one function __merge_const!(es::Array{T}) where T <: AbstractExpr - const_exprs = filter( (e) -> e.op == :CONST, es) + const_exprs = filter( (e) -> e.op == :const, es) if length(const_exprs) > 1 - filter!( (e) -> e.op != :CONST, es) + filter!( (e) -> e.op != :const, es) __add_const!(es, sum(getproperty.(const_exprs, :value))) end end -# This is NOT a recursive function. It will only unnest one level. -function __unnest(es::Array{T}, op::Symbol) where T <: AbstractExpr - # this is all the child operators that aren't CONST or IDENTITY - child_operators = filter( (op) -> op != :IDENTITY && op != :CONST, getproperty.(es, :op)) - - if length(child_operators) > 0 && all(child_operators .== op) - children = AbstractExpr[] - map( (e) -> length(e.children) > 0 ? append!(children, e.children) : push!(children, e), es) - return children - else - return es - end -end - -# This works for any n_ary op that takes as input NumericInteroperable arguments. -function __numeric_n_ary_op(es_mixed::Array, op::Symbol) +# This works for any n_ary op that takes as input NumericInteroperable arguments +function __numeric_n_ary_op(es_mixed::Array, op::Symbol; __is_commutative=false, __try_flatten=false) # clean up types! This guarantees es::Array{AbstractExpr} es, literals = __check_inputs_nary_op(es_mixed, const_type=NumericInteroperableConst, expr_type=NumericInteroperableExpr) - literal = length(literals) > 0 ? sum(literals) : 0 + literals = __is_commutative && length(literals) > 0 ? [sum(literals)] : literals - # flatten nestings, this prevents unsightly things like and(x, and(y, and(z, true))) - es = __unnest(es, op) # now we are guaranteed all es are valid exprs and all literals have been condensed to one - # hack to store literals - __add_const!(es, literal) - - # Now it is possible we have several CONST exprs. This occurs if, for example, one writes 1 + a + true - # TO clean up, we should merge the CONST exprs - __merge_const!(es) - - # Now everything is in es and we are all cleaned up. + for l in literals + __add_const!(es, l) + end + # Determine return expr type. Note that / promotes to RealExpr because the SMT theory of integers doesn't include it - ReturnExpr = any(isa.(es, RealExpr)) || op == :DIV ? RealExpr : IntExpr - + ReturnType = any(isa.(es, RealExpr)) || op == :div ? RealExpr : IntExpr + children, name = __combine(es, op, __is_commutative, __try_flatten) + + # Now it is possible we have several CONST exprs. This occurs if, for example, one writes (a+1) + (b+1) which flattens to a+1+b+1 + # TO clean up, we should merge the CONST exprs + if __is_commutative + __merge_const!(children) + name = __get_hash_name(op, children, is_commutative=__is_commutative) + end + # TODO should call a function indexed by op value = any(isnothing.(getproperty.(es, :value))) ? nothing : sum(getproperty.(es, :value)) - return ReturnExpr(op, es, value, __get_hash_name(op, es)) + return ReturnType(op, children, value, name, __is_commutative=__is_commutative) end @@ -301,23 +283,23 @@ Return the `Int` | `Real` expression `a+b` (inherits the type of `a+b`). Use dot ```julia -@satvariable(a[1:n], :Int) -@satvariable(b[1:n, 1:m], :Int) +@satvariable(a[1:n], Int) +@satvariable(b[1:n, 1:m], Int) a .+ b println("typeof a+b: \$(typeof(a[1] + b[1]))") -@satvariable(c, :Real) +@satvariable(c, Real) println("typeof a+c: \$(typeof(a[1] + c))") -@satvariable(z, :Bool) +@satvariable(z, Bool) a .+ z println("typeof a+z: \$(typeof(a[1] + z))") ``` """ -Base.:+(e1::Union{NumericInteroperableExpr}, e2::NumericInteroperableExpr) = __numeric_n_ary_op([e1, e2], :ADD) -Base.:+(e1::Union{NumericInteroperableExpr}, e2::NumericInteroperableConst) = __numeric_n_ary_op([e1, e2], :ADD) -Base.:+(e1::Union{NumericInteroperableConst}, e2::NumericInteroperableExpr) = e2 + e1 +Base.:+(e1::Union{NumericInteroperableExpr}, e2::NumericInteroperableExpr) = __numeric_n_ary_op([e1, e2], :add, __is_commutative=true, __try_flatten=true) +Base.:+(e1::Union{NumericInteroperableExpr}, e2::NumericInteroperableConst) = __numeric_n_ary_op([e1, e2], :add, __is_commutative=true, __try_flatten=true) +Base.:+(e1::Union{NumericInteroperableConst}, e2::NumericInteroperableExpr) = __numeric_n_ary_op([e1, e2], :add, __is_commutative=true, __try_flatten=true) """ a - b @@ -326,22 +308,22 @@ Base.:+(e1::Union{NumericInteroperableConst}, e2::NumericInteroperableExpr) = e2 Returns the `Int` | `Real` expression `a-b` (inherits the type of `a-b`). Use dot broadcasting for vector-valued and matrix-valued Boolean expressions. ```julia -@satvariable(a[1:n], :Int) -@satvariable(b[1:n, 1:m], :Int) +@satvariable(a[1:n], Int) +@satvariable(b[1:n, 1:m], Int) a .- b println("typeof a-b: \$(typeof(a[1] - b[1]))") -@satvariable(c, :Real) +@satvariable(c, Real) println("typeof a-c: \$(typeof(a[1] - c))") -@satvariable(z, :Bool) +@satvariable(z, Bool) a .- z println("typeof a-z: \$(typeof(a[1] - z))") ``` """ -Base.:-(e1::Union{NumericInteroperableExpr}, e2::NumericInteroperableExpr) = __numeric_n_ary_op([e1, e2], :SUB) -Base.:-(e1::Union{NumericInteroperableExpr}, e2::NumericInteroperableConst) = __numeric_n_ary_op([e1, e2], :SUB) -Base.:-(e1::Union{NumericInteroperableConst}, e2::NumericInteroperableExpr) = __numeric_n_ary_op([e1, e2], :SUB) +Base.:-(e1::Union{NumericInteroperableExpr}, e2::NumericInteroperableExpr) = __numeric_n_ary_op([e1, e2], :sub) +Base.:-(e1::Union{NumericInteroperableExpr}, e2::NumericInteroperableConst) = __numeric_n_ary_op([e1, e2], :sub) +Base.:-(e1::Union{NumericInteroperableConst}, e2::NumericInteroperableExpr) = __numeric_n_ary_op([e1, e2], :sub) """ a * b @@ -350,22 +332,22 @@ Base.:-(e1::Union{NumericInteroperableConst}, e2::NumericInteroperableExpr) = __ Returns the `Int` | `Real` multiplication expression `a*b` (inherits the type of `a*b`). Use dot broadcasting for vector-valued and matrix-valued Boolean expressions. ```julia -@satvariable(a[1:n], :Int) -@satvariable(b[1:n, 1:m], :Int) +@satvariable(a[1:n], Int) +@satvariable(b[1:n, 1:m], Int) a .* b println("typeof a*b: \$(typeof(a[1]*b[1]))") -@satvariable(c, :Real) +@satvariable(c, Real) println("typeof a*c: \$(typeof(a[1]*c))") -@satvariable(z, :Bool) +@satvariable(z, Bool) a .- z println("typeof a*z: \$(typeof(a[1]*z))") ``` """ -Base.:*(e1::Union{NumericInteroperableExpr}, e2::NumericInteroperableExpr) = __numeric_n_ary_op([e1, e2], :MUL) -Base.:*(e1::Union{NumericInteroperableExpr}, e2::NumericInteroperableConst) = __numeric_n_ary_op([e1, e2], :MUL) -Base.:*(e1::Union{NumericInteroperableConst}, e2::NumericInteroperableExpr) = e2 * e1 +Base.:*(e1::Union{NumericInteroperableExpr}, e2::NumericInteroperableExpr) = __numeric_n_ary_op([e1, e2], :mul, __is_commutative=true, __try_flatten=true) +Base.:*(e1::Union{NumericInteroperableExpr}, e2::NumericInteroperableConst) = __numeric_n_ary_op([e1, e2], :mul, __is_commutative=true, __try_flatten=true) +Base.:*(e1::Union{NumericInteroperableConst}, e2::NumericInteroperableExpr) = __numeric_n_ary_op([e1, e2], :mul, __is_commutative=true, __try_flatten=true) """ a / b @@ -374,12 +356,12 @@ Base.:*(e1::Union{NumericInteroperableConst}, e2::NumericInteroperableExpr) = e2 Returns the `Real` division expression `a/b`. Note: `a` and `b` must be `Real`). Use dot broadcasting for vector-valued and matrix-valued Boolean expressions. ```julia -@satvariable(a[1:n], :Real) -@satvariable(b[1:n, 1:m], :Real) +@satvariable(a[1:n], Real) +@satvariable(b[1:n, 1:m], Real) a ./ b println("typeof a/b: \$(typeof(a[1]/b[1]))") ``` """ -Base.:/(e1::Union{NumericInteroperableExpr}, e2::NumericInteroperableExpr) = __numeric_n_ary_op([e1, e2], :DIV) -Base.:/(e1::Union{NumericInteroperableExpr}, e2::NumericInteroperableConst) = __numeric_n_ary_op([e1, e2], :DIV) -Base.:/(e1::Union{NumericInteroperableConst}, e2::NumericInteroperableExpr) = __numeric_n_ary_op([e1, e2], :DIV) \ No newline at end of file +Base.:/(e1::Union{NumericInteroperableExpr}, e2::NumericInteroperableExpr) = __numeric_n_ary_op([e1, e2], :div) +Base.:/(e1::Union{NumericInteroperableExpr}, e2::NumericInteroperableConst) = __numeric_n_ary_op([e1, e2], :div) +Base.:/(e1::Union{NumericInteroperableConst}, e2::NumericInteroperableExpr) = __numeric_n_ary_op([e1, e2], :div) \ No newline at end of file diff --git a/src/call_solver.jl b/src/call_solver.jl index d0e60e1..f9e0df0 100644 --- a/src/call_solver.jl +++ b/src/call_solver.jl @@ -7,9 +7,13 @@ end # some instantiation options Solver(name::String, cmd::Cmd) = Solver(name, cmd, Dict{String, Any}()) -Z3() = Solver("Z3", `z3 -smt2 -in`, Dict{String, Any}()) -CVC5() = Solver("CVC5", `cvc5 --interactive --produce-models`, Dict{String, Any}()) - +if Sys.iswindows() + Z3() = Solver("Z3", `z3.exe -smt2 -in`, Dict{String, Any}()) + CVC5() = Solver("CVC5", `cvc5.exe --interactive --produce-models`, Dict{String, Any}()) +else + Z3() = Solver("Z3", `z3 -smt2 -in`, Dict{String, Any}()) + CVC5() = Solver("CVC5", `cvc5 --interactive --produce-models`, Dict{String, Any}()) +end ##### INVOKE AND TALK TO SOLVER ##### @@ -42,13 +46,13 @@ end Open a solver in a new process with in, out, and err pipes. Uses Base.process. Check the source code to see the exact implementation. """ -function send_command(pstdin::Base.Pipe, pstdout::Base.Pipe, cmd::String; is_done = f(output::String) = false) +function send_command(pstdin::Base.Pipe, pstdout::Base.Pipe, cmd::String; is_done = f(output::String) = false, line_ending='\n') # f() is required because Task can only schedule functions with no inputs f() = __wait_for_result(pstdout, is_done) t = Task(f) schedule(t) # now send the command - write(pstdin, cmd*"\n") # in case the input is missing \n + write(pstdin, cmd*line_ending) # in case the input is missing a line ending output = fetch(t) # throws automatically if t fails return output @@ -75,12 +79,13 @@ end function talk_to_solver(input::String, s::Solver) + line_ending = Sys.iswindows() ? "\r\n" : '\n' proc, pstdin, pstdout, pstderr = open_solver(s) is_sat_or_unsat(output) = occursin("sat", output) - output = send_command(pstdin, pstdout, input, is_done=is_sat_or_unsat) + output = send_command(pstdin, pstdout, input, is_done=is_sat_or_unsat, line_ending=line_ending) - @debug "Solver output for (check-sat):\n\"$output\"" + @debug "Solver output for (check-sat):$line_ending\"$output\"" if length(output) == 0 @error "Unable to retrieve solver output." return :ERROR, Dict{String, Bool}(), proc @@ -89,20 +94,20 @@ function talk_to_solver(input::String, s::Solver) @error "Solver crashed on input! Please file a bug report." return :ERROR, Dict{String, Bool}(), proc end - + original_output = deepcopy(output) output = filter(isletter, output) if output == "unsat" # the problem was successfully given to Z3, but it is UNSAT return :UNSAT, Dict{String, Bool}(), proc elseif output == "sat" # the problem is satisfiable - output = send_command(pstdin, pstdout, "(get-model)\n", is_done=nested_parens_match) - @debug "Solver output for (get-model):\n\"$output\"" + output = send_command(pstdin, pstdout, "(get-model)$line_ending", is_done=nested_parens_match, line_ending=line_ending) + @debug "Solver output for (get-model):$line_ending\"$output\"" satisfying_assignment = parse_smt_output(output) return :SAT, satisfying_assignment, proc else - @error "Solver error:\n$(output)" + @error "Solver error:$line_ending $(original_output)" return :ERROR, Dict{String, Bool}(), proc end end diff --git a/src/multiple_dispatch_ops.jl b/src/multiple_dispatch_ops.jl new file mode 100644 index 0000000..20e905a --- /dev/null +++ b/src/multiple_dispatch_ops.jl @@ -0,0 +1,17 @@ +# This allows and() to be used in multiple theories +# in a context-dependent manner + +and(es_mixed::Array{T}) where T = __multidispatch_op(and, es_mixed) +or(es_mixed::Array{T}) where T = __multidispatch_op(or, es_mixed) + +function __multidispatch_op(op::Function, es_mixed::Array{T}) where T + zs, literals = __check_inputs_nary_op(es_mixed, const_type=Bool, expr_type=BoolExpr) + if !isnothing(zs) # successfully found the type + return op(zs, literals) + end + zs, literals = __check_inputs_nary_op(es_mixed, const_type=Integer, expr_type=BitVectorExpr) + if !isnothing(zs) + return op(zs, literals) + end + @error("Unable to operate on mixed type inputs $es_mixed") +end \ No newline at end of file diff --git a/src/ops.jl b/src/ops.jl deleted file mode 100644 index 4a8c776..0000000 --- a/src/ops.jl +++ /dev/null @@ -1,30 +0,0 @@ -##### CONSTANTS FOR USE IN THIS FILE ##### -# Dictionary of opnames with n>=2 operands. This is necessary because not all opnames are valid symbols -# For example, iff is = and := is an invalid symbol. -__smt_n_opnames = Dict( - :AND => "and", - :OR => "or", - :XOR => "xor", - :IMPLIES => "=>", - :IFF => "=", - :ITE => "ite", - :LT => "<", - :LEQ => "<=", - :GT => ">", - :GEQ => ">=", - :EQ => "=", - :ADD => "+", - :SUB => "-", - :MUL => "*", - :DIV => "/", -) - -__commutative_ops = [:AND, :OR, :XOR, :IFF, :EQ, :ADD, :MUL] - -# Dictionary of opnames with 1 operand. -__smt_1_opnames = Dict( - :NOT => "not", - :NEG => "neg", -) - -__boolean_ops = [:AND, :OR, :XOR, :IMPLIES, :IFF, :ITE, :LT, :LEQ, :GT, :GEQ, :EQ, :NOT] diff --git a/src/sat.jl b/src/sat.jl index 8ee5fa7..f4c9ac0 100644 --- a/src/sat.jl +++ b/src/sat.jl @@ -39,43 +39,70 @@ sat!(zs::Array, solver::Solver) = sat!(zs...; solver=Solver) # see discussion on why this is the way it is # https://docs.julialang.org/en/v1/manual/performance-tips/#The-dangers-of-abusing-multiple-dispatch-(aka,-more-on-types-with-values-as-parameters) # https://groups.google.com/forum/#!msg/julia-users/jUMu9A3QKQQ/qjgVWr7vAwAJ +#= __reductions = Dict( - :NOT => (values) -> !(values[1]), - :AND => (values) -> reduce(&, values), - :OR => (values) -> reduce(|, values), - :XOR => (values) -> sum(values) == 1, - :IMPLIES => (values) -> !(values[1]) | values[2], - :IFF => (values) -> values[1] == values[2], - :ITE => (values) -> (values[1] & values[2]) | (values[1] & values[3]), - :EQ => (values) -> values[1] == values[2], - :LT => (values) -> values[1] < values[2], - :LEQ => (values) -> values[1] <= values[2], - :GT => (values) -> values[1] > values[2], - :GEQ => (values) -> values[1] >= values[2], - :ADD => (values) -> sum(values), - :SUB => (values) -> values[1] - sum(values[2:end]) , - :MUL => (values) -> prod(values), - :DIV => (values) -> values[1] / prod(values[2:end]), + :not => (values) -> !(values[1]), + :and => (values) -> reduce(&, values), + :or => (values) -> reduce(|, values), + :xor => (values) -> sum(values) == 1, + :implies => (values) -> !(values[1]) | values[2], + :iff => (values) -> values[1] == values[2], + :ite => (values) -> (values[1] & values[2]) | (values[1] & values[3]), + :eq => (values) -> values[1] == values[2], + :lt => (values) -> values[1] < values[2], + :leq => (values) -> values[1] <= values[2], + :gt => (values) -> values[1] > values[2], + :geq => (values) -> values[1] >= values[2], + :add => (values) -> sum(values), + :sub => (values) -> values[1] - sum(values[2:end]) , + :mul => (values) -> prod(values), + :div => (values) -> values[1] / prod(values[2:end]), ) +=# + +__julia_symbolic_ops = Dict( + :eq => ==, + :add => +, + :sub => -, + :mul => *, + :div => /, + :neg => -, + :lt => <, + :leq => <=, + :geq => >=, + :gt => >, + :bv2int => Int, +) +# This is the default function for propagating the values back up in __assign! (called when a problem is sat and a satisfying assignment is found). +# This function should be specialized as necessary. +function __propagate_value!(z::AbstractExpr) + op = z.op ∈ keys(__julia_symbolic_ops) ? __julia_symbolic_ops[z.op] : eval(z.op) + vs = getproperty.(z.children, :value) + if length(vs)>1 + z.value = op(vs...) + else + z.value = op(vs[1]) + end +end function __assign!(z::T, values::Dict) where T <: AbstractExpr - if z.op == :IDENTITY + if z.op == :identity if z.name ∈ keys(values) z.value = values[z.name] else + @warn "Value not found for variable $(z.name)." z.value = missing # this is better than nothing because & and | automatically skip it (three-valued logic). end - elseif z.op == :CONST - ; # CONST already has .value set so do nothing + elseif z.op == :const + ; # const already has .value set so do nothing else - map( (z) -> __assign!(z, values), z.children) - values = getproperty.(z.children, :value) - if z.op ∈ keys(__reductions) - z.value = __reductions[z.op](values) + if any(ismissing.(map( (z) -> __assign!(z, values), z.children))) + z.value = missing else - @error("Unknown operator $(z.op)") + __propagate_value!(z) end end + return z.value end function __clear_assignment!(z::AbstractExpr) diff --git a/src/smt_macros.jl b/src/smt_macros.jl new file mode 100644 index 0000000..9196d08 --- /dev/null +++ b/src/smt_macros.jl @@ -0,0 +1,57 @@ +# SMT-LIB theories http://smtlib.cs.uiowa.edu/theories.shtml +__valid_vartypes = [:Bool, :Int, :Real, :BitVector, :FloatingPoint, :String, :Array] +""" + @satvariable(z, Bool) + @satvariable(a[1:n], Int) + @satvariable(b, BitVector 32) + +Construct a SAT variable with name z, optional array dimensions, and specified type (`Bool`, `Int`, `Real` or `BitVector`). +Note that some require an optional third parameter. + +One and two-dimensional arrays of variables can be constructed with the following syntax. The result will be a native Julia array. +```julia +@satvariable(a[1:n], Int) # an Int vector of length n +@satvariable(x[1:m, 1:n], Real) # an m x n Int matrix +``` +""" +macro satvariable(expr, typename, arrsize=1) + # check typename + if !isa(typename, Symbol) || !(typename ∈ __valid_vartypes) # unknown + @error "Unknown expression type $typename" + end + # append Expr to typename + typename = Symbol(typename, "Expr") + + # inside here name and t are exprs + if isa(expr, Symbol) # one variable, eg @Bool(x) + name = string(expr) + # this line resolves to something like x = Bool("x") + # special handling of parametric BitVector + if typename == :BitVectorExpr + return esc(:($expr = $(typename)($(name),$(arrsize)))) + else + return esc(:($expr = $(typename)($name))) + end + + elseif length(expr.args) == 2 && isa(expr.args[1], Symbol) + stem = expr.args[1] + name = string(stem) + iterable = expr.args[2] + if typename == :BitVectorExpr + return esc(:($stem = [$(typename)("$(:($$name))_$(i)",$(arrsize)) for i in $iterable])) + else + return esc(:($stem = [$(typename)("$(:($$name))_$(i)") for i in $iterable])) + end + elseif length(expr.args) == 3 + stem = expr.args[1] + name = string(stem) + iterable1, iterable2 = expr.args[2], expr.args[3] + if typename == :BitVectorExpr + return esc(:($stem = [$(typename)("$(:($$name))_$(i)_$(j)",$(arrsize)) for i in $iterable1, j in $iterable2])) + else + return esc(:($stem = [$(typename)("$(:($$name))_$(i)_$(j)") for i in $iterable1, j in $iterable2])) + end + else + @error "Unable to create variable from expression $expr. Recommended usage: \"@satvariable(x, Bool)\", \"@satvariable(x[1:n], Int)\", or \"@satvariable(x[1:m, 1:n], Bool)\"." + end +end diff --git a/src/smt_representation.jl b/src/smt_representation.jl index 6e06f78..5c88d7e 100644 --- a/src/smt_representation.jl +++ b/src/smt_representation.jl @@ -1,73 +1,110 @@ -include("ops.jl") - # Mapping of Julia Expr types to SMT names. This is necessary because to distinguish from native types Bool, Int, Real, etc, we call ours BoolExpr, IntExpr, RealExpr, etc. -__smt_typenames = Dict( - BoolExpr => "Bool", - IntExpr => "Int", - RealExpr => "Real", +__smt_typestr(e::BoolExpr) = "Bool" +__smt_typestr(e::IntExpr) = "Int" +__smt_typestr(e::RealExpr) = "Real" +__smt_typestr(e::AbstractBitVectorExpr) = "(_ BitVec $(e.length))" + +# Dictionary of opnames with n>=2 operands. This is necessary because not all opnames are valid symbols +# For example, iff is = and := is an invalid symbol. +function __smt_opnames(e::AbstractExpr) + op = e.op + if op ∈ keys(__smt_symbolic_ops) + return __smt_symbolic_ops[op] + elseif op ∈ keys(__smt_generated_ops) + return __smt_generated_ops[op](e) + else + return op + end +end +# These special cases arise because the SMT-LIB specification requires names to be ASCII +# thus we have to name these to successfully name things in (define-fun ) +# but the SMT-LIB operators are symbolic. +__smt_symbolic_ops = Dict( + :implies => "=>", + :iff => "=", + :eq => "=", + :add => "+", + :sub => "-", + :mul => "*", + :div => "/", + :neg => "-", + :lt => "<", + :leq => "<=", + :geq => ">=", + :gt => ">", +) + +# These are extra-special cases where the operator name is not ASCII and has to be generated at runtime +__smt_generated_ops = Dict( + :int2bv => (e::AbstractBitVectorExpr) -> "(_ int2bv $(e.length))", + :extract => (e::AbstractBitVectorExpr) -> "(_ extract $(last(e.range)-1) $(first(e.range)-1))", ) +# Finally, we provide facilities for correct encoding of consts +function __format_smt_const(exprtype::Type, c::AbstractExpr) + # there's no such thing as a Bool const because all Bool consts are simplifiable + if exprtype <: IntExpr || exprtype <: RealExpr + return string(c.value) # automatically does the right thing for Ints and Reals + elseif exprtype <: AbstractBitVectorExpr + if c.length % 4 == 0 # can be a hex string + return "#x$(string(c.value, base=16, pad=div(c.length,4)))" + else + return "#b$(string(c.value, base=2, pad=c.length))" + end + else + error("Unable to encode constant $c for expression of type $exprtype.") + end +end + + ##### GENERATING SMTLIB REPRESENTATION ##### """ - declare(z) + declare(z; line_ending='\n') -Generate SMT variable declarations for a BoolExpr variable (operation = :IDENTITY). +Generate SMT variable declarations for a BoolExpr variable (operation = :identity). Examples: * `declare(a::IntExpr)` returns `"(declare-const a Int)\\n"` * `declare(and(z1, z2))` returns `"(declare-const z1 Bool)\\n(declare-const z2 Bool)\\n"`. """ -function declare(z::AbstractExpr) +function declare(z::AbstractExpr; line_ending='\n') # There is only one variable - vartype = __smt_typenames[typeof(z)] + vartype = __smt_typestr(z) if length(z) == 1 - return "(declare-const $(z.name) $vartype)\n" + return "(declare-const $(z.name) $vartype)$line_ending" # Variable is 1D elseif length(size(z)) == 1 - return join(map( (i) -> "(declare-const $(z.name)_$i $vartype)\n", 1:size(z)[1])) + return join(map( (i) -> "(declare-const $(z.name)_$i $vartype)$line_ending", 1:size(z)[1])) # Variable is 2D elseif length(size(z)) == 2 declarations = String[] # map over 2D variable rows, then cols inside m,n = size(z) map(1:m) do i - append_unique!(declarations, map( (j) -> "(declare-const $(z.name)_$(i)_$j $vartype)\n", 1:size(z)[2])) + append_unique!(declarations, map( (j) -> "(declare-const $(z.name)_$(i)_$j $vartype)$line_ending", 1:size(z)[2])) end return join(declarations) else error("Invalid size $(z.shape) for variable!") end - join(declarations, '\n') + join(declarations, line_ending) end -declare(zs::Array{T}) where T <: AbstractExpr = reduce(*, map(declare, zs)) +declare(zs::Array{T}; line_ending='\n') where T <: AbstractExpr = reduce(*, declare.(zs; line_ending=line_ending)) -# Determine the return type of an expression with operation op and children zs -function __return_type(op::Symbol, zs::Array{T}) where T <: AbstractExpr - if op ∈ __boolean_ops - return "Bool" - else - if any(typeof.(zs) .== RealExpr) - return "Real" - else # all are IntExpr - return "Int" - end - end -end - # Return either z.name or the correct (as z.name Type) if z.name is defined for multiple types # This multiple name misbehavior is allowed in SMT2; the expression (as z.name Type) is called a fully qualified name. -# It would arise if someone wrote something like @satvariable(x, :Bool); x = xb; @satvariable(x, :Int) +# It would arise if someone wrote something like @satvariable(x, Bool); x = xb; @satvariable(x, Int) function __get_smt_name(z::AbstractExpr) - if z.op == :CONST - return string(z.value) + if z.op == :const + return __format_smt_const(typeof(z), z) end global GLOBAL_VARNAMES appears_in = map( (t) -> z.name ∈ GLOBAL_VARNAMES[t], __EXPR_TYPES) if sum(appears_in) > 1 - return "(as $(z.name) $(__smt_typenames[typeof(z)]))" + return "(as $(z.name) $(__smt_typestr(z)))" else # easy case, one variable with z.name is defined return z.name end @@ -77,50 +114,55 @@ end cache is a Dict where each value is an SMT statement and its key is the hash of the statement. This allows us to avoid two things: 1. Redeclaring SMT statements, which causes the solver to emit errors. 2. Re-using named functions. For example if we \"(define-fun FUNC_NAME or(z1, z2))\" and then the expression or(z1, z2) re-appears later in the expression \"and(or(z1, z2), z3)\", we can write and(FUNC_NAME, z3)." -function __define_n_op!(zs::Array{T}, op::Symbol, cache::Dict{UInt64, String}, depth::Int) where T <: AbstractExpr - if length(zs) == 0 +function __define_n_op!(z::T, cache::Dict{UInt64, String}, depth::Int; assert=true, line_ending='\n') where T <: AbstractExpr + children = z.children + if length(children) == 0 # silly case but we should handle it return "" - - elseif length(zs) == 1 - return depth == 0 ? "(assert ($(zs[1].name)))\n" : "" - - else - fname = __get_hash_name(op, zs) - # if the expr is a :CONST it will have a value (e.g. 2 or 1.5), otherwise use its name + end + if assert && depth == 0 && typeof(z) != BoolExpr + @warn("Cannot assert non-Boolean expression $z") + end + + # done error checking + #if length(children) == 1 + # return assert && depth == 0 ? "(assert ($(children[1].name)))$line_ending" : "" + #else + fname = __get_hash_name(z.op, children, is_commutative=z.__is_commutative) + # if the expr is a :const it will have a value (e.g. 2 or 1.5), otherwise use its name # This yields a list like String["z_1", "z_2", "1"]. - varnames = __get_smt_name.(zs) - outname = __return_type(op, zs) - if op ∈ __commutative_ops + varnames = __get_smt_name.(children) + outname = __smt_typestr(z) + if z.__is_commutative varnames = sort(varnames) end - declaration = "(define-fun $fname () $outname ($(__smt_n_opnames[op]) $(join(varnames, " "))))\n" + declaration = "(define-fun $fname () $outname ($(__smt_opnames(z)) $(join(varnames, " "))))$line_ending" cache_key = hash(declaration) # we use this to find out if we already declared this item prop = "" if cache_key in keys(cache) prop = depth == 0 ? cache[cache_key] : "" else - if op ∈ __boolean_ops && depth == 0 - prop = declaration*"(assert $fname)\n" + if assert && typeof(z) == BoolExpr && depth == 0 + prop = declaration*"(assert $fname)$line_ending" # the proposition is generated and cached now. - cache[cache_key] = "(assert $fname)\n" + cache[cache_key] = "(assert $fname)$line_ending" else prop = declaration end end return prop - end + # end end -function __define_1_op!(z::AbstractExpr, op::Symbol, cache::Dict{UInt64, String}, depth::Int) - fname = __get_hash_name(op, z.children) - outname = __return_type(op, [z]) +function __define_1_op!(z::AbstractExpr, cache::Dict{UInt64, String}, depth::Int; assert=true, line_ending='\n') + fname = __get_hash_name(z.op, z.children) + outtype = __smt_typestr(z) prop = "" - declaration = "(define-fun $fname () $outname ($(__smt_1_opnames[op]) $(__get_smt_name(z.children[1]))))\n" + declaration = "(define-fun $fname () $outtype ($(__smt_opnames(z)) $(__get_smt_name(z.children[1]))))$line_ending" cache_key = hash(declaration) - if depth == 0 && !isa(z, BoolEx) - @warn("Cannot assert non-Boolean expression\n$z") + if assert && depth == 0 && typeof(z) != BoolExpr + @warn("Cannot assert non-Boolean expression $z") end if cache_key in keys(cache) && depth == 0 @@ -128,10 +170,10 @@ function __define_1_op!(z::AbstractExpr, op::Symbol, cache::Dict{UInt64, String} else # if depth = 0 that means we are at the top-level of a nested expression. # thus, if the expr is Boolean we should assert it. - if op ∈ __boolean_ops && depth == 0 - prop = declaration*"(assert $fname)\n" + if assert && typeof(z) == BoolExpr && depth == 0 + prop = declaration*"(assert $fname)$line_ending" # the proposition is generated and cached now. - cache[cache_key] = "(assert $fname)\n" + cache[cache_key] = "(assert $fname)$line_ending" else prop = declaration end @@ -143,28 +185,36 @@ end "smt!(prob, declarations, propositions) is an INTERNAL version of smt(prob). We use it to iteratively build a list of declarations and propositions. -Users should call smt(prob)." -function smt!(z::AbstractExpr, declarations::Array{T}, propositions::Array{T}, cache::Dict{UInt64, String}, depth::Int) :: Tuple{Array{T}, Array{T}} where T <: String - if z.op == :IDENTITY +Users should call smt(prob, line_ending)." +function smt!(z::AbstractExpr, declarations::Array{T}, propositions::Array{T}, cache::Dict{UInt64, String}, depth::Int; assert=true, line_ending='\n') :: Tuple{Array{T}, Array{T}} where T <: String + if z.op == :identity # a single variable n = length(declarations) - push_unique!(declarations, declare(z)) - elseif z.op == :CONST - ; - else - map( (c) -> smt!(c, declarations, propositions, cache, depth+1) , z.children) + push_unique!(declarations, declare(z; line_ending=line_ending)) + if assert && depth == 0 + if typeof(z) != BoolExpr + @warn("Cannot assert non-Boolean expression $z") + else + push_unique!(propositions, "(assert $(z.name))$line_ending") + end + end + + elseif z.op == :const + ; # do nothing, constants don't need declarations + + else # an expression with operators and children + map( (c) -> smt!(c, declarations, propositions, cache, depth+1, assert=assert, line_ending=line_ending) , z.children) - if z.op ∈ keys(__smt_1_opnames) - props = [__define_1_op!(z, z.op, cache, depth),] + if length(z.children) == 1 + prop = __define_1_op!(z, cache, depth, assert=assert, line_ending=line_ending) - elseif z.op ∈ keys(__smt_n_opnames) # all n-ary ops where n >= 2 - props = broadcast((zs::Vararg{AbstractExpr}) -> __define_n_op!(collect(zs), z.op, cache, depth), z.children...) + else # all n-ary ops where n >= 2 + prop = __define_n_op!(z, cache, depth, assert=assert, line_ending=line_ending) #n = length(propositions) - props = collect(props) - else - error("Unknown operation $(z.op)!") + #else + # error("Unknown operation $(z.op)!") end - append_unique!(propositions, props) + push_unique!(propositions, prop) end return declarations, propositions end @@ -173,7 +223,7 @@ end # Example: # * `smt(and(z1, z2))` yields the statements `(declare-const z1 Bool)\n(declare-const z2 Bool)\n(define-fun AND_31df279ea7439224 Bool (and z1 z2))\n(assert AND_31df279ea7439224)\n` """ - smt(z::AbstractExpr) + smt(z::AbstractExpr; line_ending='\n') smt(z1,...,zn) smt([z1,...,zn]) @@ -181,43 +231,53 @@ Generate the SMT representation of `z` or `and(z1,...,zn)`. When calling `smt([z1,...,zn])`, the array must have type `Array{AbstractExpr}`. Note that list comprehensions do not preserve array typing. For example, if `z` is an array of `BoolExpr`, `[z[i] for i=1:n]` will be an array of type `Any`. To preserve the correct type, use `BoolExpr[z[i] for i=1:n]`. """ -function smt(zs::Array{T}) where T <: AbstractExpr +function smt(zs::Array{T}; assert=true, line_ending=nothing) where T <: AbstractExpr + if isnothing(line_ending) + line_ending = Sys.iswindows() ? "\r\n" : '\n' + end + declarations = String[] propositions = String[] cache = Dict{UInt64, String}() if length(zs) == 1 - declarations, propositions = smt!(zs[1], declarations, propositions, cache, 0) + declarations, propositions = smt!(zs[1], declarations, propositions, cache, 0, assert=assert, line_ending=line_ending) else - map((z) -> smt!(z, declarations, propositions, cache, 0), zs) + map((z) -> smt!(z, declarations, propositions, cache, 0, assert=assert, line_ending=line_ending), zs) end # this expression concatenates all the strings in row 1, then all the strings in row 2, etc. return reduce(*, declarations)*reduce(*,propositions) end -smt(zs::Vararg{Union{Array{T}, T}}) where T <: AbstractExpr = smt(collect(zs)) +smt(zs::Vararg{Union{Array{T}, T}}; assert=true, line_ending=nothing) where T <: AbstractExpr = smt(collect(zs), assert=assert, line_ending=line_ending) ##### WRITE TO FILE ##### """ - save(z::AbstractExpr, filename) - save(z::Array{AbstractExpr}, filename=filename) + save(z::AbstractExpr, filename; line_ending='\n') + save(z::Array{AbstractExpr}, filename=filename, line_ending='\n') save(z1, z2,..., filename) # z1, z2,... are type AbstractExpr Write the SMT representation of `z` or `and(z1,...,zn)` to filename.smt. """ -function save(prob::AbstractExpr, filename="out") - if !isa(prob, BoolExpr) +function save(prob::AbstractExpr, filename="out"; assert=true, check_sat=true, line_ending=nothing) + if isnothing(line_ending) + line_ending = Sys.iswindows() ? "\r\n" : '\n' + end + + if assert && typeof(prob) != BoolExpr @warn "Top-level expression must be Boolean to produce a valid SMT program." end open("$filename.smt", "w") do io - write(io, smt(prob)) - write(io, "(check-sat)\n") + write(io, smt(prob, assert=assert, line_ending=line_ending)) + if check_sat + write(io, "(check-sat)$line_ending") + end end end # this is the version that accepts a list of exprs, for example save(z1, z2, z3). This is necessary because if z1::BoolExpr and z2::Array{BoolExpr}, etc, then the typing is too difficult to make an array. -save(zs::Vararg{Union{Array{T}, T}}; filename="out") where T <: AbstractExpr = save(__flatten_nested_exprs(all, zs...), filename) +save(zs::Vararg{Union{Array{T}, T}}; filename="out", assert=true, check_sat=true, line_ending=nothing) where T <: AbstractExpr = save(__flatten_nested_exprs(all, zs...), filename, assert=assert, check_sat=check_sat, line_ending=line_ending) # array version for convenience. THIS DOES NOT ACCEPT ARRAYS OF MIXED AbstractExpr and Array{AbstractExpr}. -save(zs::Array{T}, filename="out") where T <: AbstractExpr = save(all(zs), filename) +save(zs::Array{T}, filename="out"; assert=true, check_sat=true, line_ending=nothing) where T <: AbstractExpr = save(all(zs), filename, assert=assert, check_sat=check_sat, line_ending=line_ending) diff --git a/src/utilities.jl b/src/utilities.jl index 04830e1..68246f5 100644 --- a/src/utilities.jl +++ b/src/utilities.jl @@ -15,14 +15,50 @@ end function __check_inputs_nary_op(zs_mixed::Array{T}; const_type=Bool, expr_type=AbstractExpr) where T # Check for wrong type inputs if any((z) -> !(isa(z, const_type) || isa(z, expr_type)), zs_mixed) - error("Unrecognized type in list") + return nothing, nothing end # separate literals and const_type literals = filter((z) -> isa(z, const_type), zs_mixed) - zs = Array{AbstractExpr}(filter((z) -> isa(z, expr_type), zs_mixed)) + zs = Array{expr_type}(filter((z) -> isa(z, expr_type), zs_mixed)) return zs, literals end +# this is a very generic function to combine children of operands in any theory +function __combine(zs::Array{T}, op::Symbol, __is_commutative=false, __try_flatten=false) where T <: AbstractExpr + if length(zs) == 0 + error("Cannot iterate over zero-length array.") + elseif length(zs) == 1 + if __try_flatten && zs[1].op == op + return zs[1].children, zs[1].name + else + return zs[1:1], zs[1].name + end + end + + # Now we need to take an array of statements and decide how to combine them + # if this is an op where it makes sense to flatten (eg, and(and(x,y), and(y,z)) then flatten it) + ops = getproperty.(zs, :op) + if __try_flatten && (all(ops .== op) || + (__is_commutative && all(map( (o) -> o in [:identity, :const, op], ops)))) + # Returm a combined operator + # this line merges childless operators and children, eg and(x, and(y,z)) yields [x, y, z] + children = cat(map( (e) -> length(e.children) > 0 ? e.children : [e], zs)..., dims=1) + else # op doesn't match, so we won't flatten it + children = zs + end + if __is_commutative + children = sort(children, by=(c) -> c.name) + end + name = __get_hash_name(op, children, is_commutative=__is_commutative) + + return children, name +end + +"combine(z, op) where z is an n x m matrix of BoolExprs first flattens z, then combines it with op. +combine([z1 z2; z3 z4], or) = or([z1; z2; z3; z4])." +__combine(zs::Matrix{T}, op::Symbol, __is_commutative=false, __try_flatten=false) where T <: AbstractExpr = __combine(flatten(zs), op, __is_commutative, __try_flatten) + + "is_permutation(a::Array, b::Array) returns True if a is a permutation of b. is_permutation([1,2,3], [3,2,1]) == true is_permutation([1,2,3], [1,3]) == false" @@ -47,68 +83,6 @@ end ##### PARSING SMT OUTPUT ##### -#= -"Utility function for parsing SMT output. Split lines based on parentheses" -function __split_line(output, ptr) - stack = 0 - while ptr < length(output) - lp = findnext("(", output, ptr) - rp = findnext(")", output, ptr) - if isnothing(lp) || isnothing(rp) - return nothing - end - lp, rp = lp[1], rp[1] - if lp < rp - ptr = lp+1 # move past the next ( - stack += 1 - else - ptr = rp+1 # move past the next ) - stack -= 1 - end - if stack == 0 - return ptr - end - end -end - - -"Utility function for parsing SMT output. Read lines of the form '(define-fun x () Bool true)' -and extract the name (x) and the value (true)." -function __read_line!(line, values) - line = join(filter( (c) -> c != '\n', line),"") - line = split(line[1:end-1], " ") # strip ( and ) - name = line[4] # TODO fix - if line[end] == "true" - values[name] = true - elseif line[end] == "false" - values[name] = false - end -end - -"Utility function for parsing SMT output. Takes output of (get-model) and returns a dict of values like {'x' => true, 'y' => false}. -If a variable is not set to true or false by get-model, it will not appear in the dictionary keys." -function __parse_smt_output(output::String) - values = Dict{String, Bool}() - # there's one line with just ( - ptr = findnext("(\n", output, 1)[2] # skip it - # lines 3 - n-1 are the model definitions - next_ptr = ptr - - while ptr < length(output) - next_ptr = __split_line(output, ptr) - if isnothing(next_ptr) - break - end - #println(output[ptr:next_ptr]) - __read_line!(output[ptr:next_ptr], values) - ptr = next_ptr - end - # line n is the closing ) - return values -end -=# - -##### NEW OUTPUT PARSER ##### # Given a string consisting of a set of statements (statement-1) \n(statement-2) etc, split into an array of strings, stripping \n and (). # Split one level only, so "(a(b))(c)(d)" returns ["a(b)", "c", "d"] @@ -164,6 +138,8 @@ function __parse_line(line::String) ptr = findnext(')', line, ptr+1) # skip the next part () # figure out what the return type is return_type = nothing + + #@debug "line = $(line[ptr+1:end])" if startswith(line[ptr+1:end], "Bool") return_type = Bool ptr += 4 @@ -173,6 +149,10 @@ function __parse_line(line::String) elseif startswith(line[ptr+1:end], "Real") return_type = Float64 ptr += 4 + elseif startswith(line[ptr+1:end], "(_BitVec") + tmp_ptr = ptr + length("(_BitVec") + ptr = findnext(')', line, tmp_ptr+1) # move past the type declaration (_ BitVec [0-9]+) + return_type = nextsize(parse(Int, line[tmp_ptr+1:ptr-1])) # this figures out the unsigned int type of the SMT-LIB BitVec size else @error "Unable to parse return type of \"$original_line\"" end @@ -181,6 +161,7 @@ function __parse_line(line::String) return name, value # value may be nothing if it's a function and not a variable catch @error "Unable to parse value of type $return_type in \"$original_line\"" + rethrow() end end @@ -198,16 +179,20 @@ function __parse_value(value_type::Type, line::String) # trim the () line = line[l+1:findlast(')', line)-1] end + if value_type <: Unsigned || value_type <: BigInt # these both correspond to BitVectors + # the dumb thing here is Z3 returns them with the syntax #x0f instead of 0x0f + line = "0"*line[2:end] + end return parse(value_type, line) end -function parse_smt_output(output::String) +function parse_smt_output(original_output::String) #println(output) assignments = Dict() # recall the whole output will be surrounded by () - output = __split_statements(output) + output = __split_statements(original_output) if length(output) > 1 # something is wrong! - @error "Unable to parse output\n\"$output\"" + @error "Unable to parse output\n\"$original_output\"" return assignments end # now we've cleared the outer (), so iterating will go over each line in the model diff --git a/test/bitvector_tests.jl b/test/bitvector_tests.jl new file mode 100644 index 0000000..59c01f9 --- /dev/null +++ b/test/bitvector_tests.jl @@ -0,0 +1,154 @@ +using BooleanSatisfiability +using Test + +CLEAR_VARNAMES!() + +@testset "Construct BitVector variables and exprs" begin + # a few basics + @test nextsize(16) == UInt16 + @test nextsize(17) == UInt32 + @test nextsize(15) == UInt16 + @test bitcount(0x01) == 1 + @test bitcount(0b10010) == 5 + + @satvariable(a, BitVector, 16) + @satvariable(b, BitVector, 16) + @satvariable(c, BitVector, 12) + @satvariable(d, BitVector, 4) + # can make vectors + @satvariable(bv[1:2], BitVector, 4) + @satvariable(cv[1:2, 1:2], BitVector, 4) + + # unary minus + @test (-d).op == :bvneg + # combining ops + ops = [+, -, *, div, urem, <<, >>, srem, smod, >>>, nor, nand, xnor] + names = [:bvadd, :bvsub, :bvmul, :bvudiv, :bvurem, :bvshl, :bvashr, :bvsrem, :bvsmod, :bvlshr, :bvnor, :bvnand, :bvxnor] + for (op, name) in zip(ops, names) + @test isequal(op(a,b), BitVectorExpr{UInt16}(name, [a,b], nothing, BooleanSatisfiability.__get_hash_name(name, [a,b]), 16)) + end + + # three special cases! the native Julia bitwise ops have weird forms (&)(a,b) because they are short circuitable + @test isequal(a & b, BitVectorExpr{UInt16}(:bvand, [a,b], nothing, BooleanSatisfiability.__get_hash_name(:bvand, [a,b], is_commutative=true), 16)) + @test isequal(a | b, BitVectorExpr{UInt16}(:bvor, [a,b], nothing, BooleanSatisfiability.__get_hash_name(:bvor, [a,b], is_commutative=true), 16)) + @test isequal(~a, BitVectorExpr{UInt16}(:bvnot, [a], nothing, BooleanSatisfiability.__get_hash_name(:bvnot, [a]), 16)) + + # n-ary ops + @satvariable(e, BitVector, 16) + ops = [+, *, and, or] + names = [:bvadd, :bvmul, :bvand, :bvor] + ct = BooleanSatisfiability.bvconst(0x00ff, 16) + for (op, name) in zip(ops, names) + @test isequal(op(a,b,0x00ff,e), BitVectorExpr{UInt16}(name, [a,b,ct, e], nothing, BooleanSatisfiability.__get_hash_name(name, [a,b,ct,e]), 16)) + end + @test isequal(xnor(a,b,0x00ff,e), BitVectorExpr{UInt16}(:bvxnor, [a,b,ct,e], nothing, BooleanSatisfiability.__get_hash_name(:bvxnor, [a,b,ct,e]), 16)) + + # logical ops + ops = [<, <=, >, >=, ==, slt, sle, sgt, sge] + names = [:bvult, :bvule, :bvugt, :bvuge, :eq, :bvslt, :bvsle, :bvsgt, :bvsge] + for (op, name) in zip(ops, names) + @test isequal(op(a,b), BoolExpr(name, [a,b], nothing, BooleanSatisfiability.__get_hash_name(name, [a,b]))) + end + + # concat + @test concat(c, d).length == 16 + @test (concat(c, d) + a).length == 16 + + # indexing + @test (a[2:4]).range == UnitRange(2,4) + @test_throws ErrorException a[0:2] + @test_throws ErrorException a[15:30] + + # bv2int and int2bv + @test isequal(bv2int(a), IntExpr(:bv2int, [a], nothing, BooleanSatisfiability.__get_hash_name(:bv2int, [a]))) + @satvariable(e, Int) + @test isequal(int2bv(e, 32), BitVectorExpr{UInt32}(:int2bv, [e], nothing, BooleanSatisfiability.__get_hash_name(:int2bv, [e]), 32)) +end + +@testset "Interoperability with constants" begin + @satvariable(a, BitVector, 8) + @satvariable(b, BitVector, 8) + + @test isequal(a + 0xff, 255 + a) + @test isequal(b - 0x02, b - 2) + @test_throws ErrorException b + -1 + a + + a.value = 0xff + @test concat(bvconst(0x01, 8), bvconst(0x04, 4)).value == 0x014 + @test isequal(concat(a, 0x1).value, 0x1ff) # because 0x1 is read as one bit + @test isequal(concat(a, bvconst(0x01, 8)).value, 0xff01) + @test isequal(concat(a, bvconst(0x01, 6)).value, 0b11111111000001) + + @test isequal(0x1 == a, 0x01 == a) +end + +@testset "Spot checks for SMT generation" begin + + @test BooleanSatisfiability.__format_smt_const(BitVectorExpr, bvconst(0x04, 6)) == "#b000100" + @test BooleanSatisfiability.__format_smt_const(BitVectorExpr, bvconst(255, 12)) == "#x0ff" + + @satvariable(a, BitVector, 8) + @satvariable(b, BitVector, 8) + + @test smt(concat(a, b, a), assert=false) == "(declare-const a (_ BitVec 8)) +(declare-const b (_ BitVec 8)) +(define-fun concat_17d687cb15cd0d00 () (_ BitVec 24) (concat a b a))\n" + @test smt((a + b) << 0x2, assert=false) == "(declare-const a (_ BitVec 8)) +(declare-const b (_ BitVec 8)) +(define-fun bvadd_e2cecf976dd1f170 () (_ BitVec 8) (bvadd a b)) +(define-fun bvshl_e76bba3dcff1a5b9 () (_ BitVec 8) (bvshl bvadd_e2cecf976dd1f170 #x02))\n" + + @test smt(0xff >= b) == "(declare-const b (_ BitVec 8)) +(define-fun bvuge_7d54a0b390b2b8bc () Bool (bvuge #xff b)) +(assert bvuge_7d54a0b390b2b8bc)\n" + + @test smt(0xff == a) == "(declare-const a (_ BitVec 8)) +(define-fun eq_51725a0a6dd23455 () Bool (= #xff a)) +(assert eq_51725a0a6dd23455)\n" + +end + +@testset "BitVector special cases for SMT generation" begin + @satvariable(a, BitVector, 8) + @satvariable(b, BitVector, 8) + + @satvariable(c, Int) + @test smt(int2bv(c, 64), assert=false) == "(declare-const c Int) +(define-fun int2bv_1a6e7a9c3b2f1483 () (_ BitVec 64) ((_ int2bv 64) (as c Int)))\n" + + @test smt(bv2int(b) < 1) == "(declare-const b (_ BitVec 8)) +(define-fun bv2int_9551acae52440d48 () Int (bv2int b)) +(define-fun lt_6154633d9e26b5a1 () Bool (< bv2int_9551acae52440d48 1)) +(assert lt_6154633d9e26b5a1)\n" + + @test smt(a[1:8] == 0xff) == "(declare-const a (_ BitVec 8)) +(define-fun extract_fa232f94411b00cd () (_ BitVec 8) ((_ extract 7 0) a)) +(define-fun eq_43f451e68918e86b () Bool (= extract_fa232f94411b00cd #xff)) +(assert eq_43f451e68918e86b)\n" +end + +@testset "BitVector result parsing" begin + # this output is the result of the two prior tests, bv2int(b) < 1 and a[1:8] == 0xff + output = "( + (define-fun b () (_ BitVec 8) + #x00) + (define-fun bv2int_9551acae52440d48 () Int + (bv2int b)) + (define-fun lt_6154633d9e26b5a1 () Bool + (< (bv2int b) 1)) + (define-fun extract_fa232f94411b00cd () (_ BitVec 8) + ((_ extract 7 0) a)) + (define-fun eq_b1e0ef160af6310 () Bool + (= #xff ((_ extract 7 0) a))) + (define-fun a () (_ BitVec 8) + #xff) + )" + @satvariable(a, BitVector, 8) + @satvariable(b, BitVector, 8) + expr = and(a[1:8] == 0xff, bv2int(b) < 1) + vals = BooleanSatisfiability.parse_smt_output(output) + BooleanSatisfiability.__assign!(expr, vals) + @test a.value == 0xff + @test b.value == 0x00 + +end \ No newline at end of file diff --git a/test/boolean_operation_tests.jl b/test/boolean_operation_tests.jl index f8ddd6c..c69a97b 100644 --- a/test/boolean_operation_tests.jl +++ b/test/boolean_operation_tests.jl @@ -3,18 +3,19 @@ using Test @testset "Construct variables" begin # Write your tests here. - @satvariable(z1, :Bool) - @test isa(z1,BoolExpr) + @satvariable(z1, Bool) + @test size(z1) == 1 + @test_throws UndefVarError @satvariable(x, faketype) - @satvariable(z32[1:3, 1:2], :Bool) + @satvariable(z32[1:3, 1:2], Bool) @test isa(z32,Array{BoolExpr}) @test size(z32) == (3,2) - @satvariable(z23[1:2,1:3], :Bool) + @satvariable(z23[1:2,1:3], Bool) # Sizes are broadcastable - @satvariable(z12[1:1,1:2], :Bool) - @satvariable(z21[1:2,1:1], :Bool) + @satvariable(z12[1:1,1:2], Bool) + @satvariable(z21[1:2,1:1], Bool) # (1,) broadcasts with (1,2) @test all(size(z1 .∨ z12) .== (1,2)) # (1,) broadcasts with (2,3) @@ -32,69 +33,72 @@ using Test # Nested wrong sizes also aren't broadcastable @test_throws DimensionMismatch (z1.∨z23) .∨ z32 + + # printing works + @satvariable(z, Bool) + @test string(not(z)) == "not_25ec308d1df79cdc\n | z\n" end @testset "Print variables" begin - @satvariable(z[1:2, 1:3], :Bool) + @satvariable(z[1:2, 1:3], Bool) string_z = "BoolExpr[z_1_1\n z_1_2\n z_1_3\n; z_2_1\n z_2_2\n z_2_3\n]" @test string(z) == string_z - @satvariable(z1, :Bool) + @satvariable(z1, Bool) z1.value = true @test string(z1) == "z1 = true\n" end -@testset "Logical operations" begin - # ensures test coverage of Bool() syntax - z1 = Bool(1, "z1") - z12 = Bool(1,2, "z12") - z32 = Bool(3,2, "z32") +@testset "Logical operations" begin + @satvariable(z1[1:1], Bool) + @satvariable(z12[1:1, 1:2], Bool) + @satvariable(z32[1:3, 1:2], Bool) # 1 and 0 cases @test isequal(and([z1[1]]), z1[1]) - @test isnothing(and(AbstractExpr[])) + @test_throws ErrorException and(AbstractExpr[]) # Can construct with 2 exprs - @test all( isequal.((z1 .∧ z32)[1].children, [z1[1], z32[1]] )) - @test (z1 .∧ z32)[1].name == BooleanSatisfiability.__get_hash_name(:AND, [z1[1], z32[1]]) - @test all( isequal.((z1 .∨ z32)[2,1].children, [z1[1], z32[2,1]] )) - @test (z1 .∨ z32)[1].name == BooleanSatisfiability.__get_hash_name(:OR, [z1[1], z32[1]]) + @test BooleanSatisfiability.__is_permutation((z1 .∧ z32)[1].children, [z1[1], z32[1]] ) + @test (z1 .∧ z32)[1].name == BooleanSatisfiability.__get_hash_name(:and, [z1[1], z32[1]], is_commutative=true) + @test BooleanSatisfiability.__is_permutation((z1 .∨ z32)[2,1].children, [z1[1], z32[2,1]] ) + @test (z1 .∨ z32)[1].name == BooleanSatisfiability.__get_hash_name(:or, [z1[1], z32[1]], is_commutative=true) # Can construct with N>2 exprs or_N = or.(z1, z12, z32) and_N = and.(z1, z12, z32) - @test all( isequal.(or_N[3,2].children, [z1[1], z12[1,2], z32[3,2]] )) - @test and_N[1].name == BooleanSatisfiability.__get_hash_name(:AND, and_N[1].children) + @test BooleanSatisfiability.__is_permutation(or_N[3,2].children, [z1[1], z12[1,2], z32[3,2]] ) + @test and_N[1].name == BooleanSatisfiability.__get_hash_name(:and, and_N[1].children, is_commutative=true) - @test all( isequal.(or_N[1].children, [z1[1], z12[1], z32[1]] )) - @test or_N[1].name == BooleanSatisfiability.__get_hash_name(:OR, and_N[1].children) + @test BooleanSatisfiability.__is_permutation(or_N[1].children, [z1[1], z12[1], z32[1]] ) + @test or_N[1].name == BooleanSatisfiability.__get_hash_name(:or, and_N[1].children, is_commutative=true) # Can construct negation - @test isequal((¬z32)[1].children, [z32[1]]) + @test isequal((not(z32))[1].children, [z32[1]]) # Can construct Implies @test isequal((z1 .⟹ z1)[1].children, [z1[1], z1[1]]) # Can construct all() and any() statements @test isequal(any(z1), z1[1]) - @test isequal(any(z1 .∨ z12), BoolExpr(:OR, [z12[1,1], z1[1], z12[1,2]], nothing, BooleanSatisfiability.__get_hash_name(:OR, [z1 z12]))) - @test isequal(all(z1 .∧ z12), BoolExpr(:AND, [z12[1,1], z1[1], z12[1,2]], nothing, BooleanSatisfiability.__get_hash_name(:AND, [z1 z12]))) + @test isequal(any(z1 .∨ z12), or(z1 .∨ z12)) + @test isequal(all(z1 .∧ z12), and(z1 .∧ z12)) # mismatched all() and any() - @test isequal(any(z1 .∧ z12), BoolExpr(:OR, [z1[1] ∧ z12[1,1], z1[1] ∧ z12[1,2]], nothing, BooleanSatisfiability.__get_hash_name(:OR, z1.∧ z12))) - @test isequal(and(z12 .∨ z1), BoolExpr(:AND, [z1[1] ∨ z12[1,1], z1[1] ∨ z12[1,2]], nothing, BooleanSatisfiability.__get_hash_name(:AND, z1.∨ z12))) + @test isequal(any(z1 .∧ z12), BoolExpr(:or, [z1[1] ∧ z12[1,2], z1[1] ∧ z12[1,1]], nothing, BooleanSatisfiability.__get_hash_name(:or, z1.∧ z12, is_commutative=true))) + @test isequal(and(z12 .∨ z1), BoolExpr(:and, [z1[1] ∨ z12[1,2], z1[1] ∨ z12[1,1]], nothing, BooleanSatisfiability.__get_hash_name(:and, z1.∨ z12, is_commutative=true))) end @testset "Additional operations" begin - @satvariable(z, :Bool) - @satvariable(z1[1:1], :Bool) - @satvariable(z12[1:1, 1:2], :Bool) + @satvariable(z, Bool) + @satvariable(z1[1:1], Bool) + @satvariable(z12[1:1, 1:2], Bool) # xor @test all(isequal.(xor.(z1, z12), BoolExpr[xor(z12[1,1], z1[1]) xor(z12[1,2], z1[1])])) # weird cases - @test isnothing(xor(AbstractExpr[])) + @test_throws ErrorException xor(AbstractExpr[]) @test all(isequal.(xor(z1), z1)) @test xor(true, true, z) == false @test xor(true, false) == true @@ -114,7 +118,7 @@ end end @testset "Operations with 1D literals and 1D exprs" begin - @satvariable(z, :Bool) + @satvariable(z, Bool) # Can operate on all literals @test all([not(false), ¬(¬(true))]) @@ -124,20 +128,20 @@ end # Can operate on mixed literals and BoolExprs @test isequal(and(true, z), z) - @test and(z, false) == false - @test or(true, z) == true + @test z ∧ false == false + @test true ∨ z == true @test isequal(or(z, false, false), z) @test isequal(implies(z, false), ¬z) #or(¬z, false) == ¬z - @test isequal(implies(true, z), z) + @test isequal(true ⟹ z, z) end @testset "Operations with 1D literals and nxm exprs" begin - @satvariable(z[1:2, 1:3], :Bool) + @satvariable(z[1:2, 1:3], Bool) # Can operate on mixed literals and BoolExprs - @test isequal(and.(true, z), z) + @test isequal(true .∧ z, z) @test and.(z, false) == [false false false; false false false] - @test or.(true, z) == [true true true; true true true] + @test z .∨ true == [true true true; true true true] @test isequal(or.(z, false, false), z) @test isequal(implies.(z, false), ¬z) #or(¬z, false) == ¬z @test isequal(implies.(true, z), z) @@ -146,8 +150,8 @@ end @testset "Operations with nxm literals and nxm exprs" begin A = [true false false; false true true] B = [true true true; true true true] - @satvariable(z1, :Bool) - @satvariable(z[1:2, 1:3], :Bool) + @satvariable(z1, Bool) + @satvariable(z[1:2, 1:3], Bool) # Can operate on all literal matrices @test any([not(A); ¬(¬(A))]) @@ -168,7 +172,7 @@ end @testset "More operations with literals" begin A = [true false false; false true true] - @satvariable(z[1:1], :Bool) + @satvariable(z[1:1], Bool) @test !any(xor.(A, A)) # all false @test all(isequal.(xor.(A, z), [¬z z z; z ¬z ¬z])) @@ -176,7 +180,7 @@ end @test all(isequal.(iff.(A, z), [z ¬z ¬z; ¬z z z])) @test all(isequal.(iff.(z, A), iff.(A, z))) - y = @satvariable(y[1:1], :Bool) + y = @satvariable(y[1:1], Bool) @test all( isequal.(ite.(z, true, false), or.(and.(z, true), and.(¬z, false)) )) @test all( isequal.(ite.(false, y, z), or.(and.(false, y), and.(true, z)) )) end \ No newline at end of file diff --git a/test/int_parse_tests.jl b/test/int_parse_tests.jl index 3d09080..2789669 100644 --- a/test/int_parse_tests.jl +++ b/test/int_parse_tests.jl @@ -3,22 +3,22 @@ using Test @testset "Solving an integer-valued problem" begin CLEAR_VARNAMES!() -@satvariable(a, :Int) -@satvariable(b, :Int) +@satvariable(a, Int) +@satvariable(b, Int) expr1 = a + b + 2 -@test smt(expr1) == "(declare-const a Int) +@test smt(expr1, assert=false) == "(declare-const a Int) (declare-const b Int) -(define-fun ADD_99dce5c325207b7 () Int (+ 2 a b))\n" +(define-fun add_99dce5c325207b7 () Int (+ 2 a b))\n" expr = and(expr1 <= a, b + 1 >= b) -result = "(declare-const a Int) -(declare-const b Int) -(define-fun ADD_99dce5c325207b7 () Int (+ 2 a b)) -(define-fun LEQ_d476c845a7be63a () Bool (<= ADD_99dce5c325207b7 a)) -(define-fun ADD_f0a93f0b97da1ab2 () Int (+ 1 b)) -(define-fun GEQ_d3e5e06dff9812ca () Bool (>= ADD_f0a93f0b97da1ab2 b)) -(define-fun AND_20084a5e2cc43534 () Bool (and GEQ_d3e5e06dff9812ca LEQ_d476c845a7be63a)) -(assert AND_20084a5e2cc43534)\n" +result = "(declare-const b Int) +(declare-const a Int) +(define-fun add_f0a93f0b97da1ab2 () Int (+ 1 b)) +(define-fun geq_e1bd460e008a4d8b () Bool (>= add_f0a93f0b97da1ab2 b)) +(define-fun add_99dce5c325207b7 () Int (+ 2 a b)) +(define-fun leq_a64c028ce18b2942 () Bool (<= add_99dce5c325207b7 a)) +(define-fun and_79376630b5dc2f7c () Bool (and geq_e1bd460e008a4d8b leq_a64c028ce18b2942)) +(assert and_79376630b5dc2f7c)\n" @test smt(expr) == result status = sat!(expr) @@ -30,26 +30,27 @@ end @testset "Parse some z3 output with ints and floats" begin output = "( - (define-fun GEQ_d3e5e06dff9812ca () Bool - (>= (+ 1 b) b)) - (define-fun ADD_f0a93f0b97da1ab2 () Int - (+ 1 b)) - (define-fun LEQ_d476c845a7be63a () Bool - (<= (+ 2 a b) a)) - (define-fun AND_20084a5e2cc43534 () Bool - (and (>= (+ 1 b) b) (<= (+ 2 a b) a))) - (define-fun b () Int - (- 2)) - (define-fun ADD_99dce5c325207b7 () Int - (+ 2 a b)) - (define-fun a () Int - 0) -)" +(define-fun b () Int + (- 2)) +(define-fun a () Int + 0) +(define-fun geq_e1bd460e008a4d8b () Bool + (>= (+ 1 b) b)) +(define-fun and_8014e2e143374eea () Bool + (and (>= (+ 1 b) b) (<= (+ 2 a b) a))) +(define-fun add_99dce5c325207b7 () Int + (+ 2 a b)) +(define-fun add_f0a93f0b97da1ab2 () Int + (+ 1 b)) +(define-fun leq_8df5432ee845c9e8 () Bool + (<= (+ 2 a b) a)) +) + " result = BooleanSatisfiability.parse_smt_output(output) @test result == Dict("b" => -2, "a" => 0) output = "((define-fun b () Real (- 2.5)) -(define-fun ADD_99dce5c325207b7 () Real +(define-fun add_99dce5c325207b7 () Real (+ 2 a b)) (define-fun a () Real 0.0) @@ -60,11 +61,11 @@ end # Who would do this?? But it's supported anyway. @testset "Define fully-qualified names" begin - @satvariable(a, :Int) + @satvariable(a, Int) b = a - @satvariable(a, :Real) - hashname = BooleanSatisfiability.__get_hash_name(:ADD, [b, a]) - @test smt(b+a) == "(declare-const a Int) + @satvariable(a, Real) + hashname = BooleanSatisfiability.__get_hash_name(:add, [b, a], is_commutative=true) + @test smt(b+a, assert=false) == "(declare-const a Int) (declare-const a Real) (define-fun $hashname () Real (+ (as a Int) (as a Real))) " diff --git a/test/int_real_tests.jl b/test/int_real_tests.jl index bd66d90..34ebfc8 100644 --- a/test/int_real_tests.jl +++ b/test/int_real_tests.jl @@ -2,24 +2,24 @@ using BooleanSatisfiability using Test @testset "Construct Int and Real expressions" begin - @satvariable(a, :Int) - @satvariable(b[1:2], :Int) - @satvariable(c[1:1,1:2], :Int) + @satvariable(a, Int) + @satvariable(b[1:2], Int) + @satvariable(c[1:1,1:2], Int) - @satvariable(ar, :Real) - @satvariable(br[1:2], :Real) - @satvariable(cr[1:1,1:2], :Real) + @satvariable(ar, Real) + @satvariable(br[1:2], Real) + @satvariable(cr[1:1,1:2], Real) a.value = 2; b[1].value = 1 - @test isequal((a .< b)[1], BoolExpr(:LT, AbstractExpr[a, b[1]], false, BooleanSatisfiability.__get_hash_name(:LT, [a,b[1]]))) - @test isequal((a .>= b)[1], BoolExpr(:GEQ, AbstractExpr[a, b[1]], true, BooleanSatisfiability.__get_hash_name(:GEQ, [a,b[1]]))) + @test isequal((a .< b)[1], BoolExpr(:lt, AbstractExpr[a, b[1]], false, BooleanSatisfiability.__get_hash_name(:lt, [a,b[1]]))) + @test isequal((a .>= b)[1], BoolExpr(:geq, AbstractExpr[a, b[1]], true, BooleanSatisfiability.__get_hash_name(:geq, [a,b[1]]))) ar.value = 2.1; br[1].value = 0.9 - @test isequal((ar .> br)[1], BoolExpr(:GT, AbstractExpr[ar, br[1]], true, BooleanSatisfiability.__get_hash_name(:GT, [ar,br[1]]))) - @test isequal((ar .<= br)[1], BoolExpr(:LEQ, AbstractExpr[ar, br[1]], false, BooleanSatisfiability.__get_hash_name(:LEQ, [ar,br[1]]))) + @test isequal((ar .> br)[1], BoolExpr(:gt, AbstractExpr[ar, br[1]], true, BooleanSatisfiability.__get_hash_name(:gt, [ar,br[1]]))) + @test isequal((ar .<= br)[1], BoolExpr(:leq, AbstractExpr[ar, br[1]], false, BooleanSatisfiability.__get_hash_name(:leq, [ar,br[1]]))) - @test isequal((-c)[1,2], IntExpr(:NEG, [c[1,2]], nothing, BooleanSatisfiability.__get_hash_name(:NEG, [c[1,2]]))) - @test isequal((-cr)[1,2], RealExpr(:NEG, [cr[1,2]], nothing, BooleanSatisfiability.__get_hash_name(:NEG, [cr[1,2]]))) + @test isequal((-c)[1,2], IntExpr(:neg, [c[1,2]], nothing, BooleanSatisfiability.__get_hash_name(:neg, [c[1,2]]))) + @test isequal((-cr)[1,2], RealExpr(:neg, [cr[1,2]], nothing, BooleanSatisfiability.__get_hash_name(:neg, [cr[1,2]]))) # Construct with constants on RHS c[1,2].value = 1 @@ -27,8 +27,8 @@ using Test @test isequal((c .>= 0)[1,1] , c[1,1] >= 0) && isequal((c .<= 0.0)[1,1] , c[1,1] <= 0.0) @test isequal((c .== 0)[1,1] , c[1,1] == 0) @test isequal((c .< 0)[1,1] , c[1,1] < 0) && isequal((c .> 0)[1,1] , c[1,1] > 0) - @test isequal((c .- 1)[1,1], c[1,1] - 1) && isequal((c .* 2)[1,1], 2 * c[1,1]) && isequal((br ./ 2)[1], br[1] / 2) + # Construct with constants on LHS @test isequal((0 .>= c)[1,1] , 0 >= c[1,1]) && isequal((0.0 .<= c)[1,1] , 0.0 <= c[1,1]) @test isequal((0 .== c)[1,1] , c[1,1] == 0) @@ -37,10 +37,10 @@ using Test end @testset "Construct n-ary ops" begin - @satvariable(a, :Int) - @satvariable(b[1:2], :Int) - @satvariable(ar, :Real) - @satvariable(br[1:2], :Real) + @satvariable(a, Int) + @satvariable(b[1:2], Int) + @satvariable(ar, Real) + @satvariable(br[1:2], Real) # Operations with expressions only @test all(isa.(a .+ b, IntExpr)) @@ -51,17 +51,20 @@ end # Operations with mixed constants and type promotion # Adding Int and Bool types results in an IntExpr - children = [a, IntExpr(:CONST, AbstractExpr[], 2, "const_2")] - @test isequal(sum([a, 1, true]), IntExpr(:ADD, children, nothing, BooleanSatisfiability.__get_hash_name(:ADD, children))) + children = [a, IntExpr(:const, AbstractExpr[], 2, "const_2")] + @test isequal(sum([a, 1, true]), IntExpr(:add, children, nothing, BooleanSatisfiability.__get_hash_name(:add, children, is_commutative=true))) # Type promotion to RealExpr works when we add a float-valued literal - children = [a, RealExpr(:CONST, AbstractExpr[], 3., "const_3.0")] - @test isequal(sum([1.0, a, true, 1]), RealExpr(:ADD, children, nothing, BooleanSatisfiability.__get_hash_name(:ADD, children))) + children = [a, RealExpr(:const, AbstractExpr[], 3., "const_3.0")] + @test isequal(sum([1.0, a, true, 1]), RealExpr(:add, children, nothing, BooleanSatisfiability.__get_hash_name(:add, children, is_commutative=true))) # Type promotion to RealExpr works when we add a real-valued expr - children = [a, b[1], IntExpr(:CONST, AbstractExpr[], 2, "const_2.0")] - @test isequal(sum([a, 1.0, 1, false, b[1]]), RealExpr(:ADD, children, nothing, BooleanSatisfiability.__get_hash_name(:ADD, children))) + children = [a, b[1], IntExpr(:const, AbstractExpr[], 2, "const_2.0")] + @test isequal(sum([a, 1.0, 1, false, b[1]]), RealExpr(:add, children, nothing, BooleanSatisfiability.__get_hash_name(:add, children, is_commutative=true))) # Sum works automatically @test isequal(1 + a + b[1] + true, sum([1, a, b[1], true])) + + @test all(isequal.((a - 3).children, [a, IntExpr(:const, AbstractExpr[], 3, "const_3")])) + @test all(isequal.((ar/3.0).children, [ar, RealExpr(:const, AbstractExpr[], 3., "const_3.0")])) end \ No newline at end of file diff --git a/test/runtests.jl b/test/runtests.jl index 0de90fa..3ad570c 100644 --- a/test/runtests.jl +++ b/test/runtests.jl @@ -1,5 +1,9 @@ +push!(LOAD_PATH, "../src") +push!(LOAD_PATH, "./") using BooleanSatisfiability using Test, Logging +SET_DUPLICATE_NAME_WARNING!(false) +CLEAR_VARNAMES!() # Constructing Boolean expressions include("boolean_operation_tests.jl") @@ -7,7 +11,7 @@ include("boolean_operation_tests.jl") # Constructiong Int and Real exprs include("int_real_tests.jl") -# Generating SMT expressions +# Generating SMT expressionsexit() include("smt_representation_tests.jl") # Calling Z3 and interpreting the result @@ -16,18 +20,20 @@ include("solver_interface_tests.jl") # Test with int and real problems include("int_parse_tests.jl") +include("bitvector_tests.jl") + # Extra: Check that defining duplicate variables yields a warning @testset "Duplicate variable warning" begin SET_DUPLICATE_NAME_WARNING!(true) - @satvariable(z, :Bool) - @test_logs (:warn, "Duplicate variable name z of type Bool") Bool("z") + @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 Bool("z") + @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 Bool("z") + @test_logs min_level=Logging.Warn @satvariable(z, Bool) end \ No newline at end of file diff --git a/test/smt_representation_tests.jl b/test/smt_representation_tests.jl index 43f7840..3fc3ce4 100644 --- a/test/smt_representation_tests.jl +++ b/test/smt_representation_tests.jl @@ -1,100 +1,92 @@ +push!(LOAD_PATH, "../src") using BooleanSatisfiability using Test @testset "Individual SMTLIB2 statements" begin - @satvariable(z1, :Bool) - @satvariable(z2[1:1], :Bool) - @satvariable(z12[1:1, 1:2], :Bool) + @satvariable(z1, Bool) + @satvariable(z2[1:1], Bool) + @satvariable(z12[1:1, 1:2], Bool) # indexed expression correctly declared - @test smt(z12[1,2]) == "(declare-const z12_1_2 Bool)\n" - #1d and 2d expression - @test smt(z2) == "(declare-const z2_1 Bool)\n" - @test smt(z12) == "(declare-const z12_1_1 Bool)\n(declare-const z12_1_2 Bool)\n" + @test smt(z12[1,2]) == "(declare-const z12_1_2 Bool)\n(assert z12_1_2)\n" + #1d and 2d expression, with and without assert + @test smt(z2) == "(declare-const z2_1 Bool)\n(assert z2_1)\n" + @test smt(z12, assert=false) == "(declare-const z12_1_1 Bool)\n(declare-const z12_1_2 Bool)\n" # idea from https://microsoft.github.io/z3guide/docs/logic/propositional-logic # broadcast expression correctly generated - hashname = BooleanSatisfiability.__get_hash_name(:AND, [z1, z2[1]]) - @test smt(z1 .∧ z2) == smt(z1)*smt(z2)*"(define-fun $hashname () Bool (and z1 z2_1))\n(assert $hashname)\n" + hashname = BooleanSatisfiability.__get_hash_name(:and, [z1, z2[1]], is_commutative=true) + @test smt(z1 .∧ z2) == smt(z1, assert=false)*smt(z2, assert=false)*"(define-fun $hashname () Bool (and z1 z2_1))\n(assert $hashname)\n" # indexing creates a 1d expression - hashname = BooleanSatisfiability.__get_hash_name(:AND, [z1, z12[1,2]]) - @test smt(z1 ∧ z12[1,2]) == smt(z1)*smt(z12[1,2])*"(define-fun $hashname () Bool (and z1 z12_1_2))\n(assert $hashname)\n" - hashname = BooleanSatisfiability.__get_hash_name(:AND, z12) - @test smt(z12[1,1] ∧ z12[1,2]) == smt(z12[1,1])*smt(z12[1,2])*"(define-fun $hashname () Bool (and z12_1_1 z12_1_2))\n(assert $hashname)\n" + hashname = BooleanSatisfiability.__get_hash_name(:and, [z1, z12[1,2]], is_commutative=true) + @test smt(z1 ∧ z12[1,2]) == smt(z1, assert=false)*smt(z12[1,2], assert=false)*"(define-fun $hashname () Bool (and z1 z12_1_2))\n(assert $hashname)\n" + hashname = BooleanSatisfiability.__get_hash_name(:and, z12, is_commutative=true) + @test smt(z12[1,1] ∧ z12[1,2]) == smt(z12[1,1], assert=false)*smt(z12[1,2], assert=false)*"(define-fun $hashname () Bool (and z12_1_1 z12_1_2))\n(assert $hashname)\n" # all() and any() work - hashname = BooleanSatisfiability.__get_hash_name(:OR, [z1 z12]) - @test smt(any(z1 .∨ z12)) == smt(z1)*smt(z12)*"(define-fun $hashname () Bool (or z1 z12_1_1 z12_1_2))\n(assert $hashname)\n" + hashname = BooleanSatisfiability.__get_hash_name(:or, [z1 z12], is_commutative=true) + @test smt(any(z1 .∨ z12)) == smt(z1, assert=false)*smt(z12, assert=false)*"(define-fun $hashname () Bool (or z1 z12_1_1 z12_1_2))\n(assert $hashname)\n" - hashname = BooleanSatisfiability.__get_hash_name(:AND, [z1 z12]) - @test smt(all(z1 .∧ z12)) == smt(z1)*smt(z12)*"(define-fun $hashname () Bool (and z1 z12_1_1 z12_1_2))\n(assert $hashname)\n" + hashname = BooleanSatisfiability.__get_hash_name(:and, [z1 z12], is_commutative=true) + @test smt(all(z1 .∧ z12)) == smt(z1, assert=false)*smt(z12, assert=false)*"(define-fun $hashname () Bool (and z1 z12_1_1 z12_1_2))\n(assert $hashname)\n" - # cross all() and any() terms - # TESTS DO NOT WORK - # inner = z1.∨ z12 - #hashname = BooleanSatisfiability.__get_hash_name(:AND, inner) - #@test smt(all(inner)) == smt(inner)*"(define-fun $hashname () Bool (and $(inner#[1].name) $(inner![2].name)))\n(assert $hashname)\n" - - # inner = z1.∧ z12 - #hashname = BooleanSatisfiability.__get_hash_name(:OR, inner) - #@test smt(any(inner)) == smt(inner)*"(define-fun $hashname () Bool (or $(inner#[1].name) $(inner[2].name)))\n(assert $hashname)\n" end @testset "Generate additional exprs" begin - @satvariable(z1, :Bool) - @satvariable(z12[1:1, 1:2], :Bool) + @satvariable(z1, Bool) + @satvariable(z12[1:1, 1:2], Bool) - # implies - hashname = BooleanSatisfiability.__get_hash_name(:IMPLIES, [z1, z12[1,2]]) - @test smt(z1 ⟹ z12[1,2]) == smt(z1)*smt(z12[1,2])*"(define-fun $hashname () Bool (=> z1 z12_1_2))\n(assert $hashname)\n" + # implies, also tests \r\n + hashname = BooleanSatisfiability.__get_hash_name(:implies, [z1, z12[1,2]]) + @test smt(z1 ⟹ z12[1,2], line_ending="\r\n") == "(declare-const z1 Bool)\r\n(declare-const z12_1_2 Bool)\r\n(define-fun $hashname () Bool (=> z1 z12_1_2))\r\n(assert $hashname)\r\n" - # iff - hashname = BooleanSatisfiability.__get_hash_name(:IFF, [z1, z12[1,2]]) - @test smt(z1 ⟺ z12[1,2]) == smt(z1)*smt(z12[1,2])*"(define-fun $hashname () Bool (= z1 z12_1_2))\n(assert $hashname)\n" + # iff, also tests \r\n + hashname = BooleanSatisfiability.__get_hash_name(:iff, [z1, z12[1,2]]) + @test smt(z1 ⟺ z12[1,2], line_ending="\r\n") == smt(z1, assert=false, line_ending="\r\n")*smt(z12[1,2], assert=false, line_ending="\r\n")*"(define-fun $hashname () Bool (= z1 z12_1_2))\r\n(assert $hashname)\r\n" # xor - hashname = BooleanSatisfiability.__get_hash_name(:XOR, z12) - @test smt(xor(z12[1,1], z12[1,2])) == smt(z12[1,1])*smt(z12[1,2])*"(define-fun $hashname () Bool (xor z12_1_1 z12_1_2))\n(assert $hashname)\n" + hashname = BooleanSatisfiability.__get_hash_name(:xor, z12, is_commutative=true) + @test smt(xor(z12[1,1], z12[1,2])) == smt(z12[1,1], assert=false)*smt(z12[1,2], assert=false)*"(define-fun $hashname () Bool (xor z12_1_1 z12_1_2))\n(assert $hashname)\n" # if-then-else - @satvariable(x, :Bool) - @satvariable(y, :Bool) - @satvariable(z, :Bool) - hashname = BooleanSatisfiability.__get_hash_name(:ITE, [x,y,z]) - @test smt(ite(x,y,z)) == smt(x)*smt(y)*smt(z)*"(define-fun $hashname () Bool (ite x y z))\n(assert $hashname)\n" + @satvariable(x, Bool) + @satvariable(y, Bool) + @satvariable(z, Bool) + hashname = BooleanSatisfiability.__get_hash_name(:ite, [x,y,z]) + @test smt(ite(x,y,z)) == smt(x, assert=false)*smt(y, assert=false)*smt(z, assert=false)*"(define-fun $hashname () Bool (ite x y z))\n(assert $hashname)\n" end @testset "Generate nested expr without duplications" begin - @satvariable(x, :Bool) - @satvariable(y, :Bool) + @satvariable(x, Bool) + @satvariable(y, Bool) - xyname = BooleanSatisfiability.__get_hash_name(:AND, [x,y]) + xyname = BooleanSatisfiability.__get_hash_name(:and, [x,y], is_commutative=true) xy = and(x,y) yx = and(y,x) - topname = BooleanSatisfiability.__get_hash_name(:OR, [xy, yx]) - @test smt(or(xy, yx)) == smt(x)*smt(y)* + topname = BooleanSatisfiability.__get_hash_name(:or, [xy], is_commutative=true) + @test smt(or(xy, yx)) == smt(x, assert=false)*smt(y, assert=false)* "(define-fun $xyname () Bool (and x y)) -(define-fun $topname () Bool (or $xyname $xyname)) +(define-fun $topname () Bool (or $xyname)) (assert $topname)\n" # Generate a nested expr with not (1-ary op) without duplicating statements - xname = BooleanSatisfiability.__get_hash_name(:NOT, [x]) + xname = BooleanSatisfiability.__get_hash_name(:not, [x]) nx = ¬x - xyname = BooleanSatisfiability.__get_hash_name(:AND, [nx, nx]) - @test smt(and(¬x, ¬x)) == smt(x)* + xyname = BooleanSatisfiability.__get_hash_name(:and, [nx], is_commutative=true) + @test smt(and(¬x, ¬x)) == smt(x, assert=false)* "(define-fun $xname () Bool (not x)) -(define-fun $xyname () Bool (and $xname $xname)) +(define-fun $xyname () Bool (and $xname)) (assert $xyname)\n" end @testset "Generate SMT file" begin - @satvariable(z1, :Bool) - @satvariable(z12[1:1, 1:2], :Bool) + @satvariable(z1, Bool) + @satvariable(z12[1:1, 1:2], Bool) save(z1 .∧ z12, "outfile") text = read(open("outfile.smt", "r"), String) @test text == smt(all(z1 .∧ z12))*"(check-sat)\n" - a = Int("a") - @test_logs (:warn, "Top-level expression must be Boolean to produce a valid SMT program.") save(a+1) + @satvariable(a, Int) + @test_logs (:warn, "Top-level expression must be Boolean to produce a valid SMT program.") match_mode=:any save(a) end \ No newline at end of file diff --git a/test/solver_interface_tests.jl b/test/solver_interface_tests.jl index c20b53c..96ba842 100644 --- a/test/solver_interface_tests.jl +++ b/test/solver_interface_tests.jl @@ -3,9 +3,9 @@ using Test, Logging # assign is used after calling the solver so it belongs here. @testset "Assign values" begin - @satvariable(x[1:3], :Bool) - @satvariable(y[1:2], :Bool) - @satvariable(z, :Bool) + @satvariable(x[1:3], Bool) + @satvariable(y[1:2], Bool) + @satvariable(z, Bool) prob = and( all(x), @@ -17,78 +17,89 @@ using Test, Logging "y_1" => 0, "y_2" => 0,) BooleanSatisfiability.__assign!(prob, values) @test ismissing(value(z)) + z.value = 0 + @test all(value(x) .== [1, 1 ,1]) @test all(value(y) .== [0, 0]) - # Creating a new expression where all children have assigned values also yields assigned values @test all(value(x .∨ [y; z]) .== 1) + @test all(value(xor.(x, [y; z])) .== 1) + @test all(value(x .∧ [y; z]) .== 0) @test value(and(prob.children[1], prob.children[2])) == 1 # Test other assignments, especially reducing child values - test_expr = BoolExpr(:XOR, x, nothing, "test") + test_expr = BoolExpr(:xor, x, nothing, "test") BooleanSatisfiability.__assign!(test_expr, values) @test value(test_expr) == false - test_expr.op = :ITE + test_expr.op = :ite BooleanSatisfiability.__assign!(test_expr, values) @test value(test_expr) == true - test_expr = BoolExpr(:IMPLIES, y, nothing, "test") + test_expr = BoolExpr(:implies, y, nothing, "test") BooleanSatisfiability.__assign!(test_expr, values) @test value(test_expr) == true - test_expr.op = :IFF + test_expr.op = :iff BooleanSatisfiability.__assign!(test_expr, values) @test value(test_expr) == true # done with Booleans, now test Int assignments - values = Dict("a_1"=>1, "a_2"=>2, "a_3"=>3) - test_expr = IntExpr(:EQ, Int(2,"a"), nothing, "test") + values = Dict("a2_1"=>1, "a2_2"=>2, "a2_3"=>3) + @satvariable(a2[1:2], Int) + test_expr = IntExpr(:eq, a2, nothing, "test") BooleanSatisfiability.__assign!(test_expr, values) @test value(test_expr) == false - test_expr.op = :LT + test_expr.op = :lt BooleanSatisfiability.__assign!(test_expr, values) @test value(test_expr) == true - test_expr.op = :GT + test_expr.op = :gt BooleanSatisfiability.__assign!(test_expr, values) @test value(test_expr) == false - test_expr.op = :LEQ + test_expr.op = :leq BooleanSatisfiability.__assign!(test_expr, values) @test value(test_expr) == true - test_expr.op = :GEQ + test_expr.op = :geq BooleanSatisfiability.__assign!(test_expr, values) @test value(test_expr) == false # Arithmetic operations - test_expr = IntExpr(:ADD, Int(3,"a"), nothing, "test") + values = Dict("a3_1"=>1, "a3_2"=>2, "a3_3"=>3) + @satvariable(a3[1:3], Int) + test_expr = IntExpr(:add, a3, nothing, "test") BooleanSatisfiability.__assign!(test_expr, values) @test value(test_expr) == 6 - test_expr.op = :SUB + + test_expr.op = :mul BooleanSatisfiability.__assign!(test_expr, values) - @test value(test_expr) == -4 + @test value(test_expr) == 6 - test_expr.op = :MUL + test_expr.op = :sub; test_expr.children = test_expr.children[1:2] BooleanSatisfiability.__assign!(test_expr, values) - @test value(test_expr) == 6 + @test value(test_expr) == -1 - values = Dict("a_1"=>1., "a_2"=>2., "a_3"=>3., "a"=>0.) - test_expr = RealExpr(:DIV, Real(3,"a"), nothing, "test") + values = Dict("ar2_1"=>1., "ar2_2"=>2.) + @satvariable(ar2[1:2], Real) + test_expr = RealExpr(:div, ar2, nothing, "test") BooleanSatisfiability.__assign!(test_expr, values) - @test value(test_expr) == (1. / 2. / 3.) + @test value(test_expr) == (1. / 2.) # Can't assign nonexistent operator - test_expr = RealExpr(:fakeop, Real(1,"a"), nothing, "test") - @test_logs (:error, "Unknown operator fakeop") BooleanSatisfiability.__assign!(test_expr, values) + #test_expr = RealExpr(:fakeop, Real(1,"a"), nothing, "test") + #@test_logs (:error, "Unknown operator fakeop") BooleanSatisfiability.__assign!(test_expr, values) # Missing value assigned to missing - b = Int("b") + @satvariable(b, Int) @test ismissing(BooleanSatisfiability.__assign!(b, values)) end @testset "Solving a SAT problem" begin - @satvariable(x[1:3], :Bool) - @satvariable(y[1:2], :Bool) - @satvariable(z, :Bool) + # can initialize cvc5 + s = CVC5() + + @satvariable(x[1:3], Bool) + @satvariable(y[1:2], Bool) + @satvariable(z, Bool) exprs = BoolExpr[ all(x), @@ -112,22 +123,25 @@ end end @testset "Custom solver interactions" begin - @satvariable(x[1:3], :Bool) - @satvariable(y[1:2], :Bool) + @satvariable(x[1:3], Bool) + @satvariable(y[1:2], Bool) exprs = BoolExpr[ all(x), all(x[1:2] .∨ y), all(¬y), ] - input = smt(exprs...)*"(check-sat)\n" + line_ending = Sys.iswindows() ? "\r\n" : "\n" + input = smt(exprs...)*"(check-sat)$line_ending" # Set up a custom solver that doesn't work (it should be z3) - solver = Solver("Z3", `Z3 -smt2 -in`) - @test_throws Base.IOError open_solver(solver) + if !Sys.iswindows() # this test doesn't work on Windows, probably because Windows cmd sucks + solver = Solver("Z3", `Z3 -smt2 -in`) + @test_throws Base.IOError open_solver(solver) + end # Interact using send_command proc, pstdin, pstdout, pstderr = open_solver(Z3()) output = send_command(pstdin, pstdout, input, is_done=nested_parens_match) - @test output == "sat\n" + @test output == "sat$line_ending" end \ No newline at end of file