Fixed solver output retrieval correctly so it always works even if z3…

… takes a long

time.

TODOS.txt

@@ -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)).
+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

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
@@ -79,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
@@ -123,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
@@ -186,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
@@ -280,7 +280,7 @@ function __combine(zs::Array{T}, op::Symbol) where T <: BoolExpr
     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)
+    if !all(getproperty.(zs, :op) .== zs[1].op)
         error("Cannot combine array with mismatched operations.")
     end
     # (2) Combine them
@@ -335,6 +335,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/IntExpr.jl

@@ -124,25 +124,6 @@ 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 op is nested, such as and(x, and(y, and(z, true))), flatten it. In the example we would get and(x, y, z, true).
-#= function flatten(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, map( (e) -> e.op, es))
-    
-    if length(child_operators) > 0 && all(child_operators .== op)
-        # This line flattens the children of expr e unless e has no children, in which case we keep e
-        children = flatten(AbstractExpr[e.children for e in es])
-        println("children =", children)
-        return children
-    else
-        return es
-    end
-
-end
-=#
 # 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
@@ -156,14 +137,14 @@ function merge_const!(es::Array{T}) where T <: AbstractExpr
     const_exprs = filter( (e) -> e.op == :CONST, es)
     if length(const_exprs) > 1
         filter!( (e) -> e.op != :CONST, es)
-        add_const!(es, sum(map( (e) -> e.value, const_exprs)))
+        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, map( (e) -> e.op, es))
+    child_operators = filter( (op) -> op != :IDENTITY && op != :CONST, getproperty.(es, :op))
 
     if length(child_operators) > 0 && all(child_operators .== op)
         children = AbstractExpr[]
@@ -192,9 +173,9 @@ function __numeric_n_ary_op(es_mixed::Array, op::Symbol)
 
     # Now everything is in es and we are all cleaned up.
     # Determine return expr type. Note that / promotes to RealExpr because the SMT theory of integers doesn't include it
-    ReturnExpr = any(map((e) -> isa(e, RealExpr), es)) || op == :DIV ? RealExpr : IntExpr
+    ReturnExpr = any(isa.(es, RealExpr)) || op == :DIV ? RealExpr : IntExpr
 
-    value = any(isnothing.(map( (e) -> e.value, es))) ? nothing : sum(values)
+    value = any(isnothing.(getproperty.(es, :value))) ? nothing : sum(values)
     return ReturnExpr(op, es, value, __get_hash_name(op, es))
 end
 

src/call_solver.jl

@@ -13,13 +13,28 @@ function talk_to_solver(input::String, cmd)
         return :ERROR, Dict{String, Bool}(), proc
     end
 
+    function get_result()
+        output = ""
+        stack = 0
+        while true
+            new_bytes = String(readavailable(pstdout))
+            stack += length(filter( (c) -> c == '(', new_bytes)) - length(filter( (c) -> c == ')', new_bytes))
+            output = output*new_bytes
+            if length(new_bytes) > 0 && stack == 0
+                return output
+            end
+            sleep(0.002)
+        end
+    end
+    t = Task(get_result)
+    schedule(t)
+
     # now we have a pipe open that we can communicate to z3 with
     write(pstdin, input)
     write(pstdin, "\n") # in case the input is missing \n
 
-    # read only the bytes in the buffer, otherwise it hangs
-    output = String(readavailable(pstdout))
-
+    output = fetch(t) # throws automatically if t fails
+    @debug "Solver output for (check-sat):\n\"$output\""
     if length(output) == 0
         @error "Unable to retrieve solver output."
         return :ERROR, Dict{String, Bool}(), proc
@@ -33,15 +48,18 @@ function talk_to_solver(input::String, cmd)
         return :UNSAT, Dict{String, Bool}(), proc
 
     elseif startswith(output, "sat") # the problem is satisfiable
+        t = Task(get_result)
+        schedule(t)
+
         write(pstdin, "(get-model)\n")
-        sleep(0.01) # IDK WHY WE NEED THIS BUT IF WE DON'T HAVE IT, pstdout HAS 0 BYTES BUFFERED 
-        # This has something to do with z3 and we need to fix it more correctly.
-        output = String(readavailable(pstdout))
+        output = fetch(t) # throws automatically if t fails
+        @debug "Solver output for (get-model):\n\"$output\""
+
         satisfying_assignment = parse_smt_output(output)
         return :SAT, satisfying_assignment, proc
 
     else
         @error "Solver error:\n$(output)"
         return :ERROR, Dict{String, Bool}(), proc
     end
-end
+end

src/sat.jl

@@ -69,7 +69,7 @@ function __assign!(z::T, values::Dict) where T <: AbstractExpr
         ; # CONST already has .value set so do nothing
     else
         map( (z) -> __assign!(z, values), z.children)
-        values = map( (z) -> z.value, z.children)
+        values = getproperty.(z.children, :value)
         if z.op ∈ keys(__reductions)
             z.value = __reductions[z.op](values)
         else

src/smt_representation.jl

@@ -78,8 +78,7 @@ function __return_type(op::Symbol, zs::Array{T}) where T <: AbstractExpr
     if op ∈ __boolean_ops
         return "Bool"
     else
-        types = map(typeof, zs)
-        if any(types .== RealExpr)
+        if any(typeof.(zs) .== RealExpr)
             return "Real"
         else # all are IntExpr
             return "Int"
@@ -118,7 +117,7 @@ function __define_n_op!(zs::Array{T}, op::Symbol, cache::Dict{UInt64, String}, d
         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
         # This yields a list like String["z_1", "z_2", "1"].
-        varnames = map(__get_smt_name, zs)
+        varnames = __get_smt_name.(zs)
         outname = __return_type(op, zs)
         if op ∈ __commutative_ops
             varnames = sort(varnames)
@@ -146,7 +145,7 @@ function __define_1_op!(z::AbstractExpr, op::Symbol, cache::Dict{UInt64, String}
     fname = __get_hash_name(op, z.children)
     outname = __return_type(op, [z])
     prop = ""
-    declaration = "(define-fun $fname () $outname ($(__smt_1_opnames[op]) $(__get_smt_name(z.children)))\n"
+    declaration = "(define-fun $fname () $outname ($(__smt_1_opnames[op]) $(__get_smt_name(z.children[1]))))\n"
     cache_key = hash(declaration)
 
     if depth == 0 && !isa(z, BoolEx)

src/utilities.jl

@@ -202,7 +202,7 @@ function __parse_value(value_type::Type, line::String)
 end
 
 function parse_smt_output(output::String)
-    println(output)
+    #println(output)
     assignments = Dict()
     # recall the whole output will be surrounded by ()
     output = __split_statements(output)

test/int_parse_tests.jl

@@ -9,7 +9,7 @@ expr1 = a + b + 2
 (declare-const b Int)
 (define-fun ADD_99dce5c325207b7 () Int (+ 2 a b))\n"
 
-expr = and(expr1 <= a, b >= b + 1)
+expr = and(expr1 <= a, b + 1 >= b)
 result = "(declare-const a Int)
 (declare-const b Int)
 (define-fun ADD_99dce5c325207b7 () Int (+ 2 a b))