Merge pull request #3 from elsoroka/dev-ints-reals

Merge ints and reals into dev

TODOS.txt

@@ -47,7 +47,7 @@ Add capability to provide a custom command command string when invoking z3. This
 Clean up code by splitting it into files - done 6/22/23
 Add the operators xor, iff, and ite (if-then-else) which are in the SMT propositional logic spec - done 6/23/23
 Updated implies to use its own operator (=>) - done 6/23/23
-Add functionality to warn about duplicate names
+Add functionality to warn about duplicate names - done 6/23/23
 
 # BEFORE RELEASING
 Determine which functions aren't covered by unittests - done 6/22/23
@@ -57,3 +57,8 @@ Use @warn and @error correctly for non-breaking errors.
 Check compliance with the Julia style guide. https://docs.julialang.org/en/v1/manual/style-guide/
 Generate documentation - started 6/21/23
 Publish documentation
+
+# TODO 6/29/23
+Fix any() and all() for mismatched operators, eg any(or(x,y),z,and(a,b)) - done 6/30/23
+Fix all instances of map( (x) -> x.property, xs) to getproperty.(x, :property) - done 6/30/23
+Fix retrieving solver output, again! - done 6/30/23

examples/job_shop_scheduling.jl

@@ -0,0 +1,38 @@
+push!(LOAD_PATH,"../src/")
+using BooleanSatisfiability
+
+# From https://microsoft.github.io/z3guide/docs/theories/Arithmetic/
+# Job shop scheduling problem is a linear integer problem arising in operations research.
+# Suppose you are managing a machine shop with several different jobs in progress.
+# Each job consists of a series of tasks. Some of the tasks have ordering constraints: e.g. parts must be manufactured before they can be installed in a larger assembly.
+# Due to equipment constraints, you cannot schedule two tasks requiring the same machine at the same time.
+# Additionally, all tasks must have a worker assigned to complete them.
+
+# In this problem we have three jobs, each consisting of one task to be completed first by worker A and one to be completed next by worker B.
+# Each task has an integer-valued duration. Workers cannot work on two tasks at once or take each others' tasks.
+# We'd like to find a solution such that all three jobs can be completed in an 8-hour workday.
+# Define two vector-valued variables t1 and t2 such that tj[i] is the start time of job i for worker j.
+# Define two vector-valued variables d1 and d2 such that dj[i] is the duration of job i for worker j.
+
+n = 3 # number of jobs
+m = 2 # number of tasks per job
+t1 = Int(n,"t1")
+t2 = Int(n, "t2")
+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.
+working_hours = all(and.(t1 .>= 0, t2 .+ d2 .<= 8))
+
+# Sequencing constraint: For each job, A must complete the first task before B can start the second task
+sequencing = and(t2 .>= t1 .+ d1)
+
+# Overlap constraint between all permutations
+overlaps = [(1,2), (1,3), (2,3)]
+overlap_1 = all([or( t1[i] >= t1[j] + d1[j], t1[j] >= t1[i] + d1[i]) for (i,j) in overlaps])
+overlap_2 = all([or( t2[i] >= t2[j] + d2[j], t2[j] >= t2[i] + d2[i]) for (i,j) in overlaps])
+
+status = sat!(working_hours, sequencing, overlap_1, overlap_2)
+println("status = $status")
+println("t1 = $(value(t1))")
+println("t2 = $(value(t2))")

src/BoolExpr.jl

@@ -1,4 +1,4 @@
-import Base.length, Base.size, Base.show, Base.string, Base.==, Base.broadcastable
+import Base.length, Base.size, Base.show, Base.string, Base.isequal, Base.hash, Base.broadcastable
 
 ##### TYPE DEFINITIONS #####
 
@@ -39,10 +39,10 @@ function Bool(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
-	if name ∈ GLOBAL_VARNAMES
-        if WARN_DUPLICATE_NAMES @warn("Duplicate variable name $name") end
+	if name ∈ GLOBAL_VARNAMES[BoolExpr]
+        if WARN_DUPLICATE_NAMES @warn("Duplicate variable name $name of type Bool") end
     else
-        push!(GLOBAL_VARNAMES, name)
+        push!(GLOBAL_VARNAMES[BoolExpr], name)
     end
 	return BoolExpr(:IDENTITY, Array{AbstractExpr}[], nothing, "$(name)")
 end
@@ -53,15 +53,15 @@ Bool(m::Int, n::Int, name::String) :: Matrix{BoolExpr} = BoolExpr[Bool("$(name)_
 ##### BASE FUNCTIONS #####
 
 # Base calls
-Base.size(e::BoolExpr) = 1
+Base.size(e::AbstractExpr) = 1
 Base.length(e::AbstractExpr) = 1
 Broadcast.broadcastable(e::AbstractExpr) = (e,)
 
 # Printing behavior https://docs.julialang.org/en/v1/base/io-network/#Base.print
 Base.show(io::IO, expr::AbstractExpr) = print(io, string(expr))
 
 # This helps us print nested exprs
-function Base.string(expr::BoolExpr, indent=0)::String
+function Base.string(expr::AbstractExpr, indent=0)::String
 	if expr.op == :IDENTITY	
 		return "$(repeat(" | ", indent))$(expr.name)$(isnothing(expr.value) ? "" : " = $(expr.value)")\n"
 	else
@@ -74,6 +74,16 @@ function Base.string(expr::BoolExpr, indent=0)::String
 end
 
 "Test equality of two BoolExprs."
-function (==)(expr1::BoolExpr, expr2::BoolExpr)
+function Base.isequal(expr1::AbstractExpr, expr2::AbstractExpr)
     return (expr1.op == expr2.op) && all(expr1.value .== expr2.value) && (expr1.name == expr2.name) && (__is_permutation(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))")
+end
+
+# Overload because Base.in uses == which se used to construct equality expressions
+function Base.in(expr::T, exprs::Array{T}) where T <: AbstractExpr
+	return any(isequal.(expr, exprs))
 end

src/BooleanOperations.jl

@@ -20,7 +20,7 @@ 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(map( (e)-> e.name, zs )))
+    names = sort(vec(getproperty.(zs, :name)))
     if length(names) > max_items
         return "$(names[1])_to_$(names[end])"
     else
@@ -59,16 +59,6 @@ not(zs::Array{T}) where T <: BoolExpr  = map(not, zs)
 ∧(z1::BoolExpr, z2::BoolExpr) = and([z1, z2])
 ∨(z1::BoolExpr, z2::BoolExpr) = or([z1, z2])
 
-function __check_inputs_nary_op(zs_mixed::Array{T}) where T
-    # Check for wrong type inputs
-    if any((z) -> !(isa(z, Bool) || isa(z, BoolExpr)), zs_mixed)
-        error("Unrecognized type in list")
-    end
-    # separate literals and BoolExpr
-    literals = filter((z) -> isa(z, Bool), zs_mixed)
-    zs = Array{BoolExpr}(filter((z) -> isa(z, AbstractExpr), zs_mixed))
-    return zs, literals
-end
 
 function and(zs_mixed::Array{T}; broadcast_type=:Elementwise) where T
 
@@ -89,7 +79,7 @@ function and(zs_mixed::Array{T}; broadcast_type=:Elementwise) where T
     end    
 
     # now the remaining are BoolExpr
-    child_values = map((z) -> z.value, zs)
+    child_values = getproperty.(zs, :value)
     value = any(isnothing.(child_values)) ? nothing : reduce(&, child_values)
     return BoolExpr(:AND, zs, value, __get_hash_name(:AND, zs))
 end
@@ -133,7 +123,7 @@ function or(zs_mixed::Array{T}; broadcast_type=:Elementwise) where T
         return zs[1]
     end
 
-    child_values = map((z) -> z.value, zs)
+    child_values = getproperty.(zs, :value)
     value = any(isnothing.(child_values)) ? nothing : reduce(|, child_values)
     return BoolExpr(:OR, zs, value, __get_hash_name(:OR, zs))
 end
@@ -183,7 +173,8 @@ function xor(zs_mixed::Array{T}; broadcast_type=:Elementwise) where T
         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
-            return and(¬zs) # then all variables must be false
+            # 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...)
         end
@@ -195,7 +186,7 @@ function xor(zs_mixed::Array{T}; broadcast_type=:Elementwise) where T
         return zs[1]
     end
 
-    child_values = map((z) -> z.value, zs)
+    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))
 end
@@ -287,18 +278,14 @@ function __combine(zs::Array{T}, op::Symbol) where T <: BoolExpr
     elseif length(zs) == 1
         return zs[1]
     end
-    # Now we need to take an array of statements and...
-    # (1) Verify they are all the same operator
-    if !all(map( (e) -> e.op, zs) .== zs[1].op)
-        error("Cannot combine array with mismatched operations.")
-    end
-    # (2) Combine them
-    if zs[1].op == :IDENTITY
-        name = __get_hash_name(op, zs)#"$(op)_$(__get_name_stem(zs))"
+
+    # Now we need to take an array of statements and decide how to combine them
+    if all(getproperty.(zs, :op) .== :IDENTITY)
         children = flatten(zs)
-    elseif zs[1].op == op
+        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.
-        # (3) Returm a combined operator
+        # 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)
@@ -323,7 +310,12 @@ 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)`
 """
-all(zs::Array{T}) where T <: BoolExpr = __combine(zs, :AND)
+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
 
 """
     any([z1,...,zn])
@@ -333,7 +325,12 @@ 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)`
 """
-any(zs::Array{T}) where T <: BoolExpr = __combine(zs, :OR)
+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
 
 
 """
@@ -344,6 +341,6 @@ Returns the satisfying assignment of `z`, or `nothing` if no satisfying assignme
 
 It's possible to return an array of mixed `Bool` and `nothing`. This could occur if some variables in an array do not appear in a problem, because `sat!(problem)` will not set the values of variables that do not appear in `problem`.
 """
-value(zs::Array{T}) where T <: AbstractExpr = map( (z) -> z.value, zs)
+value(zs::Array{T}) where T <: AbstractExpr = getproperty.(zs, :value)
 
 value(z::AbstractExpr) = z.value

src/BooleanSatisfiability.jl

@@ -2,6 +2,10 @@ module BooleanSatisfiability
 
 export AbstractExpr,
        BoolExpr,
+       IntExpr,
+       RealExpr
+
+export
        and, ∧,
        or,  ∨,
        not, ¬,
@@ -10,6 +14,18 @@ export AbstractExpr,
        iff, ⟺,
        ite,
        value
+export
+       eq,
+       le, <,
+       leq, <=,
+       ge, >,
+       geq, >=
+
+export
+       add, +,
+       sub, -,
+       mul, *,
+       div, /
 
 export smt,
        save
@@ -21,29 +37,38 @@ DEFAULT_SOLVER_CMDS = Dict(
     :Z3 => `z3 -smt2 -in`
 )
 
+#=  INCLUDES
+    * BoolExpr.jl (definition of BoolExpr)
+    * utilities.jl (internal, no public-facing functions)
+    * Logical operators and, or, not, implies
+    * Logical operators any and all
+=#
+include("BooleanOperations.jl")
+
+#= INCLUDES
+    * Declarations for IntExpr and RealExpr
+    * Operations for IntExpr and RealExpr
+=#
+include("IntExpr.jl")
+
+
+__EXPR_TYPES = [BoolExpr, RealExpr, IntExpr]
+
 # 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 GLOBAL_VARNAMES = String[]
+global GLOBAL_VARNAMES = Dict(t => String[] for t in __EXPR_TYPES)
 # When false, no warnings will be issued
 global WARN_DUPLICATE_NAMES = false
 
 SET_DUPLICATE_NAME_WARNING!(value::Bool) = global WARN_DUPLICATE_NAMES = value
 
 # this might be useful when solving something in a loop
-CLEAR_VARNAMES!() = global GLOBAL_VARNAMES = String[]
+CLEAR_VARNAMES!() = global GLOBAL_VARNAMES = Dict(t => String[] for t in __EXPR_TYPES)
 
 export GLOBAL_VARNAMES,
        SET_DUPLICATE_NAME_WARNING!,
        CLEAR_VARNAMES!
-
-#=  INCLUDES
-    * BoolExpr.jl (definition of BoolExpr)
-    * utilities.jl (internal, no public-facing functions)
-    * Logical operators and, or, not, implies
-    * Logical operators any and all
-=#
-include("BooleanOperations.jl")
 
 #=  INCLUDES
     * declare (generate SMT variable declarations for expression)