Merge pull request #27 from elsoroka/dev

Fix Docs build issue and minor issues

.github/workflows/docs.yml

@@ -4,7 +4,6 @@ on:
   push:
     branches:
       - main
-      - dev-unittests
 
 jobs:
   Documenter:

README.md

@@ -1,6 +1,6 @@
 # [Satisfiability.jl](https://elsoroka.github.io/Satisfiability.jl)
 
-[![build status](https://github.com/elsoroka/Satisfiability.jl/actions/workflows/ci.yml/badge.svg?branch=main)](https://github.com/elsoroka/Satisfiability.jl/actions/workflows/CI.yml?query=branch%3Amain) [![docs](https://github.com/elsoroka/Satisfiability.jl/actions/workflows/docs.yml/badge.svg)](https://elsoroka.github.io/Satisfiability.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/Satisfiability.jl/actions/workflows/ci.yml/badge.svg?branch=main)](https://github.com/elsoroka/Satisfiability.jl/actions/workflows/CI.yml?query=branch%3Amain) [![docs](https://github.com/elsoroka/Satisfiability.jl/actions/workflows/docs.yml/badge.svg)](https://elsoroka.github.io/Satisfiability.jl/) [![codecov](https://codecov.io/gh/elsoroka/Satisfiability.jl/branch/main/graph/badge.svg?token=84BIREQL46)](https://codecov.io/gh/elsoroka/Satisfiability.jl)
 
 Satisfiability.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, uninterpreted functions, 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).
 

docs/make.jl

@@ -1,6 +1,6 @@
 # CALL THIS FILE FROM ../ (call `julia docs/make.jl`)
 using Documenter
-push!(LOAD_PATH,"src/")
+push!(LOAD_PATH, "$(pwd())/src/")
 
 using Satisfiability
 
@@ -12,6 +12,7 @@ clean=true,
 draft=false,
 root="docs",
 source  = "src",
+workdir=pwd(),
 modules = [Satisfiability],
 pages = [
         "index.md",

docs/src/example_bv_lcg.md

@@ -11,14 +11,16 @@ A linear congruential generator (LCG) is an algorithm for generating pseudo-rand
 
 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
+```@example 1
 using Satisfiability
 
 @satvariable(states[1:10], BitVector, 32)
 @satvariable(output_prev, BitVector, 32)
 @satvariable(output_next, BitVector, 32)
 ```
-```@example
+
+Define the transitions between states.
+```@example 1
 transitions = BoolExpr[states[i+1] == states[i] * 214013+2531011 for i=1:9]
 remainders = BoolExpr[
     output_prev == urem(( states[1] >> 16 ) & 0x7FFF, 100),
@@ -32,9 +34,11 @@ remainders = BoolExpr[
     urem(( states[9] >> 16) & 0x7FFF, 100) == 61,
     output_next == urem(( states[10] >> 16) & 0x7FFF, 100),
 ]
-```
-```@example
+
 expr = and(and(transitions), and(remainders))
+```
+Solve the problem and inspect the solution.
+```@example 1
 status = sat!(expr, solver=CVC5())
 println("status = $status")
 

docs/src/example_job_shop.md

@@ -15,7 +15,7 @@ We'd like to find a solution such that all three jobs can be completed in an 8-h
 
 * Define two vector-valued variables d1 and d2 such that dj[i] is the duration of job i for worker j.
 
-```@example
+```@example 1
 using Satisfiability
 n = 3 # number of jobs
 m = 2 # number of tasks per job
@@ -25,24 +25,24 @@ d1 = [2; 3; 2]
 d2 = [1; 1; 3]
 ```
 A start time of 0 corresponds to the first hour of the workday, and an end time of 8 corresponds to the last hour of the workday.
-```@example
+```@example 1
 working_hours = and(and.(t1 .>= 0, t2 .+ d2 .<= 8))
 ```
 
 Sequencing constraint: For each job, A must complete the first task before B can start the second task
-```@example
+```@example 1
 sequencing = and(t2 .>= t1 .+ d1)
 ```
 
 Overlap constraint between all permutations
-```@example
+```@example 1
 overlaps = [(1,2), (1,3), (2,3)]
 overlap_1 = and(or( t1[i] >= t1[j] + d1[j], t1[j] >= t1[i] + d1[i]) for (i,j) in overlaps)
 overlap_2 = and(or( t2[i] >= t2[j] + d2[j], t2[j] >= t2[i] + d2[i]) for (i,j) in overlaps)
 ```
 
 Solve the problem
-```@example
+```@example 1
 status = sat!(working_hours, sequencing, overlap_1, overlap_2, solver=Z3())
 println("status = $status")
 if status == :SAT

docs/src/example_scheduling.md

@@ -11,7 +11,7 @@ Rules:
 
 ### Setup
 We concatenate the availability row vectors into a 5 x 8 Boolean matrix ``\bar A``.
-```@example
+```@example 1
 using Satisfiability
 
 n = 5 # number of people
@@ -31,19 +31,19 @@ A_bar = Bool[
 
 ```
 The `index_sets` represent which meeting attendees are required at each meeting ``\mathcal{I_j}``.
-```@example
+```@example 1
 index_sets = [[1,2,3], [3,4,5], [1,3,5], [1,4]]
 J = length(index_sets) # number of meetings
 ```
 
 ### Logical constraints
 If attendee ``i`` is unavailable at time ``t`` (``\bar A_{it} = 0``) then they cannot be in a meeting at time ``t``.
-```@example
+```@example 1
 unavailability = and(¬A_bar .⟹ ¬A)
 ```
 
 For each meeting ``j``, all attendees in index set ``\mathcal{I_j}`` must be available at some time ``t`` and not attending another meeting.
-```@example
+```@example 1
 M = [and(A[index_sets[j], t]) for j=1:J, t=1:T]
 
 # get a list of conflicts
@@ -52,16 +52,16 @@ no_double_booking = and(M[j,t] ⟹ ¬or(M[conflicts[j],t]) for j=1:J, t=1:T)
 ```
 
 All meetings must be scheduled.
-```@example
+```@example 1
 require_one_time = and(or(M[j,:]) for j=1:J)
 ```
 No attendee should have more than 2 consecutive hours of meetings.
-```@example
+```@example 1
 time_limit = and(¬and(A[i,t:t+2]) for i=1:n, t=1:T-2)
 ```
 
 ### Solving the problem
-```@example
+```@example 1
 # solve
 exprs = [no_double_booking, require_one_time, unavailability, time_limit]
 status = sat!(exprs, solver=Z3())

docs/src/tutorial.md

@@ -7,7 +7,8 @@ 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
+```@example 1
+using Satisfiability 
 @satvariable(a, Bool)
 @satvariable(b, Bool)
 
@@ -18,7 +19,7 @@ status = sat!(¬conjecture, solver=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
+```@example 1
 @satvariable(p, Bool)
 @satvariable(q, Bool)
 @satvariable(r, Bool)
@@ -28,7 +29,7 @@ status = sat!(¬conjecture, solver=Z3())
 ```
 Unlike the previous example the status is `:SAT`, indicating there is an assignment `p`, `q` and `r` that disproves the conjecture.
 
-```@example
+```@example 1
 println("p = $(value(p))")
 println("q = $(value(q))")
 println("r = $(value(r))")
@@ -40,8 +41,8 @@ The knapsack problem is a famous NP-complete problem in which you are packing a
 A simpler version, illustrated in this [classic XKCD strip](https://xkcd.com/287/), is to pack the bag to exactly its maximum weight (or spend a specific amount of money).
 In fact, the problem in the XKCD strip can be expressed as a linear equation over integers.
 
-```@example
-@satvariable(a[1:6], Bool)
+```@example 1
+@satvariable(a[1:6], Int)
 c = [215; 275; 335; 355; 420; 580]
 expr = and(and(a .>= 0), sum(a .* c) == 1505)
 sat!(expr, solver=Z3())
@@ -53,7 +54,7 @@ println("Check: $(sum(value(a) .* c))")
 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
+```@example 1
 println("Example 1 (should be SAT)")
 @satvariable(b, BitVector, 8)
 is_power_of_two = b & (b - 0x01) == 0

src/BitVectorExpr.jl

@@ -577,7 +577,7 @@ Specifically, when concatenating BitVectorExprs and constants, one should wrap t
 """
 function bvconst(c::Integer, size::Int)
     if c < 0
-        error("Cannot combine negative integer constant $c with BitVector")
+        error("Cannot combine negative integer constant $c with BitVector; use unsigned(c)")
     end
 
     minsize = bitcount(c)

src/IntExpr.jl

@@ -1,4 +1,4 @@
-import Base.<, Base.<=, Base.>, Base.<=, Base.+, Base.-, Base.*, Base./, Base.div, Base.mod, Base.abs, Base.==, Base.!=, Base.promote_rule, Base.convert
+import Base.<, Base.<=, Base.>, Base.<=, Base.+, Base.-, Base.*, Base./, Base.^, Base.div, Base.inv, Base.mod, Base.abs, Base.==, Base.!=, Base.promote_rule, Base.convert
 
 abstract type NumericExpr <: AbstractExpr end
 
@@ -301,6 +301,12 @@ end
 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)
+    if all(isa.(es, BoolExpr)) # this can happen for example if you have Bool x + Bool z
+        es[1] = ite(es[1], 1, 0) # convert one to IntExpr
+        es = collect(promote(es...))
+        literals = convert.(Int, literals)
+    end
+
     literals = __is_commutative && length(literals) > 0 ? [sum(literals)] : literals
 
     # now we are guaranteed all es are valid exprs and all literals have been condensed to one
@@ -403,6 +409,7 @@ Base.:*(e1::NumericInteroperableExpr, e2::NumericInteroperableExpr)  = __numeric
 Base.:*(e1::NumericInteroperableExpr, e2::NumericInteroperableConst) = __numeric_n_ary_op([e1, e2], :mul, __is_commutative=true, __try_flatten=true)
 Base.:*(e1::NumericInteroperableConst, e2::NumericInteroperableExpr) = __numeric_n_ary_op([e1, e2], :mul, __is_commutative=true, __try_flatten=true)
 
+Base.:^(e::NumericInteroperableExpr, n::Int)  = prod([e for i=1:n])
 
 """
     div(a, b)
@@ -448,6 +455,7 @@ Base.:/(e1::NumericInteroperableExpr, e2::NumericInteroperableExpr) =  __numeric
 Base.:/(e1::NumericInteroperableExpr, e2::NumericInteroperableConst) = __numeric_n_ary_op([convert(RealExpr, e1), __wrap_const(Float64(e2))], :rdiv)
 Base.:/(e1::NumericInteroperableConst, e2::NumericInteroperableExpr) = __numeric_n_ary_op([__wrap_const(Float64(e1)), convert(RealExpr, e2)], :rdiv)
 
+Base.inv(e::NumericInteroperableExpr) = 1.0 / e # this performs the correct promotion due to the float 1.0
 
 """
     to_real(a::IntExpr)

src/sat.jl

@@ -340,8 +340,12 @@ end
 assign!(zs::Array{T}, assignment::Dict) where T <: AbstractExpr = map((z) -> assign!(z, assignment), zs)
 
 function __clear_assignment!(z::AbstractExpr)
-    z.value = nothing
-    if length(z.children) > 0
-        map(__clear_assignment!, z.children)
+    if z.op == :const
+        return # do nothing
+    else
+        z.value = nothing
+        if length(z.children) > 0
+            map(__clear_assignment!, z.children)
+        end
     end
 end

test/int_real_tests.jl

@@ -13,6 +13,7 @@ using Test
     @satvariable(z, Bool)
     @test isequal(convert(IntExpr, z), ite(z, 1, 0))
     @test isequal(convert(RealExpr, z), ite(z, 1.0, 0.0))
+    @test isequal(z+z, ite(z, 1, 0) + ite(z, 1, 0))
 
     a.value = 2; b[1].value = 1
     @test isequal((a .< b)[1], BoolExpr(:lt, AbstractExpr[a, b[1]], false, Satisfiability.__get_hash_name(:lt, [a,b[1]])))
@@ -58,6 +59,9 @@ end
     @test all(isa.(br .* ar, RealExpr))
     @test all(isa.(a ./ b, RealExpr))
 
+    @test isequal(a*a*a, a^3)
+    @test isequal(a^(-1), 1.0/to_real(a))
+    @test isequal((1.0/ar)*(1.0/ar), ar^(-2))
 
     # Operations with mixed constants and type promotion
     # Adding Int and Bool types results in an IntExpr

test/solver_interface_tests.jl

@@ -141,6 +141,9 @@ end
     @test isnothing(value(z))
     @test all(map(isnothing, value(x)))
     @test all(map(isnothing, value(y)))
+
+    # doesn't solve empty problem
+    @test_throws(ErrorException, sat!(solver=Z3()))
 end
 
 @testset "Solving an integer-valued problem" begin