Merge pull request #12 from elsoroka/dev

Uninterpreted functions and interactive solving

docs/make.jl

@@ -16,17 +16,23 @@ modules = [Satisfiability],
 pages = [
         "index.md",
         "installation.md",
+        "Tutorial" => [
         "tutorial.md",
+        "interactive.md",
+        "example_uninterpreted_func.md",
+        "advanced.md",
+        ],
         "faq.md",
         "Examples" => [
             "example_scheduling.md",
             "example_job_shop.md",
             "example_bv_lcg.md",
+            "example_graph_coloring.md",
+            "example_bad_assertions.md",
         ],
         "Library" => [
         "functions.md"
-        ],
-        "advanced.md",
+        ]
     ],
 format=fmt,
 )

docs/server.sh

@@ -0,0 +1 @@
+python3 -m http.server --bind localhost

docs/src/advanced.md

@@ -14,47 +14,55 @@ solver = Solver("My Solver", `program_name --option1 --option2`)
 sat!(problem, solver) # sat! will use your provided command to invoke the solver
 ```
 
-The command you provide must launch a solver that accepts SMTLIB2-formatted commands and can respond to `(get-model)` in SAT mode. (An example of a command that does NOT work is `cvc5 --interactive`, because `cvc5` cannot answer `(get-model)` without the `--produce-models` option.)
+The command you provide must launch a solver that accepts SMTLIB2-formatted commands and can respond to `(get-model)` in SAT mode. (An example of a command that does NOT work is `cvc5 --interactive`, because `CVC5` cannot answer `(get-model)` without the `--produce-models` option.)
 
-To familiarize yourself with what this means, you may use `save` to generate a small SMT file for a satisfiable problem, then [call a solver from the terminal](installation.md#installing-a-solver), paste in the contents of your SMT file, and issue the command `(get-model)`. This is exactly what BooleanSatisfiability.jl does when you call  `sat!`. Armed with this knowledge, go forth and customize your solver command.
+To familiarize yourself with what this means, you may use `save` to generate a small SMT file for a satisfiable problem, then [call a solver from the terminal](installation.md#installing-a-solver), paste in the contents of your SMT file, and issue the command `(get-model)`. This is exactly what Satisfiability.jl does when you call  `sat!`. Armed with this knowledge, go forth and customize your solver command.
 
-### Custom interactions with solvers
-BooleanSatisfiability provides an interface to issue SMT2 commands and receive SMT2-formatted solver responses programmatically. This is useful if you wish to build your own decision logic or parser using advanced solver functionality.
+### Custom interactions using `send_command`
+Satisfiability.jl provides an interface to issue SMT-LIB commands and receive SMT-LIB-formatted solver responses programmatically. This is useful if you wish to build your own decision logic or parser using advanced solver functionality.
 
-!!! note SMT2 solver modes.
-In the SMT2 specification, after entering a problem and issuing the command `(check-sat)` the solver will be in either `sat` or `unsat` mode. The solver mode determines which commands are valid: for example, `(get-unsat-core)` is only valid in `unsat` mode and `(get-model)` is only valid in `sat` mode. You can find descriptions of modes and listings of valid commands in the latest [SMT-LIB Standard](http://www.smtlib.org/).
+If you just want to use an SMT solver interactively, for example by `push`ing or `pop`ping assertions, check out [Interactive Solving](interactive.md).
+
+!!! note SMT-LIB solver modes.
+In the SMT-LIB specification, after entering a problem and issuing the command `(check-sat)` the solver will be in either `sat` or `unsat` mode. The solver mode determines which commands are valid: for example, `(get-unsat-core)` is only valid in `unsat` mode and `(get-model)` is only valid in `sat` mode. You can find descriptions of modes and listings of valid commands in the latest [SMT-LIB Standard](http://www.smtlib.org/).
 
 Here's an example.
 ```julia
 @satvariable(x[1:2], Bool)
 expr = (x[1] ∧ ¬x[1]) ∧ any(x) # unsat
 
-solver = Z3()
-proc, pstdin, pstdout, pstderr = open_process(solver)
+interactive_solver = open(Z3())
+
+send_command(interactive_solver, "(set-option :produce-unsat-cores true)", dont_wait=true)
 
 # smt() adds the command (check-sat), so Z3 will be in either `sat` or `unsat` mode after this command.
-input = smt(expr)
-response = send_command(pstdin, pstdout, input, is_done=nested_parens_match)
+input = smt(expr)*"\n(check-sat)\n"
+response = send_command(interactive_solver, input, is_done=is_sat_or_unsat)
 
-println("status = $response") # :UNSAT
+println("status = $response") # "unsat"
 
-response = send_command(pstdin, pstdout, "(get-unsat-core)", is_done=nested_parens_match)
+response = send_command(interactive_solver, "(get-unsat-core)", is_done=nested_parens_match)
 println(response)
 
 # more interactions via `send_command`...
 
-# it's good form to clean up your process
-close(proc)
+# it's good form to clean up your open solver process
+close(interactive_solver)
 ```
 
-When using this functionality, you are responsible for keeping track of the solver mode and parsing the result of `send_command`.
+When using this functionality, you are responsible for keeping track of the solver mode and parsing the result of `send_command`. For convenience, `parse_model(model::String)` can parse the result of the SMT-LIB command `(get-model)`, returning a dictionary with variable names as keys and satisfying assignments as values.
+
 
 **Checking if the response is complete**
+Receiving a complete solver response is not as simple as it sounds, for two reasons.
+1. The solver may take a long time to respond, for example when calling `(check-sat)`.
+2. The solver's response may be large, thus it may be received in several chunks.
 
-The `send_command` function has an optional argument `is_done` for checking whether the full response has been received. The default is `nested_parens_match(output::String)` which returns `true` if `response` contains at least 1 matching pair of parentheses. This ensures the entire output is returned when issuing commands such as `(get-model)` where the response is wrapped in at least 1 set of parentheses.
+The `send_command` function has an optional argument `is_done` for checking whether the full response has been received. Two convenience functions are provided: `nested_parens_match(response::String)` returns `true` if `response` begins with `(` and ends with a matching `)`. This ensures the entire output is returned when issuing commands such as `(get-model)` where the entire response is wrapped in 1 set of parentheses. Many solver responses follow this format.
+`is_sat_or_unsat` is very simple: if the response contains `sat` or `unsat` it returns `true`, otherwise it's `false`.
 
 !!! warning Multiple parenthesized statements
-If your command produces a response with multiple separate statements, for example `(statement_1)\n(statement_2)`, `nested_parens_match` is not guaranteed to return the entire response. The intended use case is `((statement_1)\n(statement_2))`.
+If your command produces a response with multiple separate statements, for example `(statement_1)\n(statement_2)`, `nested_parens_match` is not guaranteed to return the entire response. The intended use case is `((statement_1)\n(statement_2))`. This should only happen if you issue two SMT-LIB commands at once.
 
 **Customizing `is_done`**
 
@@ -64,4 +72,4 @@ A custom function `is_done(response::String)::Bool`, should have the following b
 
 SAT solvers can be slow and some commands produce long outputs. Without `is_done`, `send_command` could receive a partial response and prematurely return.
 
-For full implementation details, please see the [source code](https://github.com/elsoroka/BooleanSatisfiability.jl/blob/main/src/call_solver.jl) of `call_solver.jl`.
+For full implementation details, please see the [source code](https://github.com/elsoroka/Satisfiability.jl/blob/main/src/call_solver.jl) of `call_solver.jl`.

docs/src/example_bad_assertions.md

@@ -0,0 +1,72 @@
+# Pushing and popping assertions
+In this problem we have some expressions we need to satisfy, and some that we would like to satisfy (but we can't satisfy them all).
+We want to figure out which expressions we can satisfy using push() and pop() to assert and remove them as necessary.
+
+```julia
+using Satisfiability
+@satvariable(x, Bool)
+@satvariable(y, Bool)
+@satvariable(z, Bool)
+necessary_exprs = or(and(not(x), y, z), and(not(y), x, z))
+
+interactive_solver = open(Z3())
+```
+We assert this at the first level, since we always have to have it.
+```julia
+assert!(interactive_solver, necessary_exprs)
+```
+
+Here are some conflicting expressions. One of them is satisfiable when `necessary_exprs` is true; the others are not.
+```julia
+conflicting_exprs = [
+    not(z),
+    and(not(x), not(y)),
+    not(x),
+    and(x,y),
+]
+```
+
+We'll use `push` and `pop` to add and remove them one at a time.
+```julia
+for e in conflicting_exprs
+    # Push one assertion level on the stack
+    push!(interactive_solver, 1)
+
+    # Now assert an expression that might make the problem unsatisfiable
+    assert!(interactive_solver, e)
+    status, assignment = sat!(interactive_solver)
+
+    if status == :SAT
+        println("We found it! Expr \n$e \nis satisfiable.")
+        assign!(necessary_exprs, assignment)
+        assign!(conflicting_exprs, assignment)
+    else
+        # Pop one level off the stack, removing the problematic assertion.
+        pop!(interactive_solver, 1)
+    end
+end
+```
+
+### Another way to do this.
+Let's reset the solver so we can try another way to do the same thing. This command clears all assertions, including the first one we made at level 1.
+```julia
+reset_assertions!(interactive_solver)
+```
+
+This time, we use `sat!(solver, exprs...)` which is equivalent to the SMT-LIB command `(check-sat-assuming exprs...)`. Thus the expression is not asserted but is assumed within the scope of the `sat!` call.
+```julia
+assert!(interactive_solver, necessary_exprs)
+# Here's an equivalent way to do this by passing exprs into sat!. This is equivalent to the SMT-LIB syntax "(check-sat-assuming (exprs...))", which does not (assert) the expressions but assumes they should be satisfied.
+for e in conflicting_exprs
+    status, assignment = sat!(interactive_solver, e)
+    println("status = $status")
+    if status == :SAT
+        println("We found it! Expr \n$e \nis satisfiable.")
+        assign!(necessary_exprs, assignment)
+        assign!(conflicting_exprs, assignment)
+    end
+end
+
+# We're done, so don't forget to clean up.
+close(interactive_solver)
+```

docs/src/example_bv_lcg.md

@@ -35,7 +35,7 @@ remainders = BoolExpr[
 ```
 ```@example
 expr = and(all(transitions), all(remainders))
-status = sat!(expr, solver=cvc5())
+status = sat!(expr, solver=CVC5())
 println("status = $status")
 
 for (i,state) in enumerate(states)

docs/src/example_graph_coloring.md

@@ -0,0 +1,56 @@
+# Graph coloring
+A classic problem in graph theory is figuring out how to color nodes of a graph such that no two adjacent nodes have the same color.
+This is useful for things like mapmaking (imagine if your map had two adjacent countries sharing a color!)
+The [chromatic polynomial](https://en.wikipedia.org/wiki/Graph_coloring) counts the number of ways a graph can be colored using n colors. For example, this graph
+```
+ (a)
+  | \
+  | (c)--(d)
+  | /
+ (b)
+```
+can be colored using exactly 3 colors in 12 different ways. Let's use SMT to find all 12 ways to color this graph.
+
+```julia
+using Satisfiability
+@satvariable(nodes[1:4], Int)
+
+# "There are 3 colors available"
+limits = and.(nodes .>= 1, nodes .<= 3)
+
+# "No adjacent nodes can share a color"
+(a, b, c, d) = nodes
+connections = and(a != b, a != c, b != c, c != d)
+
+# "All 3 colors must be used"
+# (If you leave this out you can find 24 colorings. But 12 of them will use only 2 colors.)
+all3 = and(or(nodes .== i) for i=1:3)
+```
+
+To find **all** the solutions, we have to exclude solutions as we find them. Suppose we find a satisfying assignment `[vars] = [values]`. Adding the negation `not(and(vars .== values))` to the list of assertions excludes that specific assignment from being found again. Remember: when excluding solutions, negate the whole expression. An easy mistake is `and(not(nodes .== value(nodes)))`, which excludes each node from taking on the particular value we just found (for example, saying "a cannot be 1", "b cannot be 2"...) instead of excluding the specific combination of all 4 values ("a cannot be 1 when b is 2,...").
+
+```julia
+function findall()
+
+    solutions = []
+    open(Z3()) do interactive_solver # the do syntax closes the solver
+        assert!(interactive_solver, limits, connections, all3)
+        i = 1
+        status, assignment = sat!(interactive_solver)
+        while status == :SAT
+            # Try to solve the problem
+            push!(solutions, assignment)
+            println("i = $i, status = $status, assignment = $assignment")
+            assign!(nodes, assignment)
+
+            # Use assert! to exclude the solution we just found.
+            assert!(interactive_solver, not(and(nodes .== value(nodes))))
+            status, assignment = sat!(interactive_solver)
+            i += 1
+        end
+    end
+    println("Found them all!")
+end
+
+findall()
+```

docs/src/example_scheduling.md

@@ -53,11 +53,11 @@ no_double_booking = all([M[j,t] ⟹ ¬or(M[conflicts[j],t]) for j=1:J, t=1:T])
 
 All meetings must be scheduled.
 ```@example
-require_one_time = all([or(M[j,:]) for j=1:J])
+require_one_time = and(or(M[j,:]) for j=1:J)
 ```
 No attendee should have more than 2 consecutive hours of meetings.
 ```@example
-time_limit = all([¬and(A[i,t:t+2]) for i=1:n, t=1:T-2])
+time_limit = and(¬and(A[i,t:t+2]) for i=1:n, t=1:T-2)
 ```
 
 ### Solving the problem
@@ -69,7 +69,8 @@ status = sat!(exprs, Z3())
 println("status = $status") # for this example we know it's SAT
 times = ["9a", "10a", "11a", "12p", "1p", "2p", "3p", "4p"]
 for j=1:J
-    println("Meeting with attendees $(index_sets[j]) can occur at $(times[findall(value(M[j,:]) .== true)])")
+    Mj_value = value(M[j,:])
+    println("Meeting with attendees $(index_sets[j]) can occur at $(times[filter((i) -> Mj_value[i], 1:length(Mj_value))]) .== true)])")
 end
 
 println("Value A: $(value(A))")

docs/src/example_uninterpreted_func.md

@@ -0,0 +1,37 @@
+# Uninterpreted Functions
+
+
+An uninterpreted function is a function where the mapping between input and output is not known. The task of the SMT solver is then to determine a mapping such that some SMT expression holds true.
+
+Satisfiability.jl represents uninterpreted functions as callable structs. This enables the simple syntax:
+```julia
+@uninterpreted(myfunc, Int, Int)
+
+# we can call myfunc on an Int constant or variable
+@satvariable(a, Int)
+myfunc(a)
+myfunc(-2) # returns 
+
+# we cannot call myfunc on the wrong type
+# myfunc(true) yields an error
+# myfunc(1.5) yields an error
+```
+
+As a small example, we can ask whether there exists a function `f(x)` such that `f(f(x)) == x`, `f(x) == y` and `x != y`.
+
+```julia
+@satvariable(x, Bool)
+@satvariable(y, Bool)
+@uninterpreted(f, Bool, Bool)
+
+status = sat!(distinct(x,y), f(x) == y, f(f(x)) == x, solver=Z3())
+println("status = \$status")
+```
+
+It turns out there is. Since the satisfying assignment for an uninterpreted function is itself a function, Satisfiability.jl represents this by setting the value of `f` to this function. Now calling `f(value)` will return the value of this satisfying assignment.
+
+```julia
+println(f(x.value)) # prints 0
+println(f(x.value) == y.value) # true
+println(f(f(x.value)) == x.value) # true
+```

docs/src/faq.md

@@ -20,7 +20,7 @@ If you have a problem with only discrete variables, especially a large one, you
 
 * Similarly, Java has [JavaSMT](https://github.com/sosy-lab/java-smt).
 
-* CVC5 has [APIs](https://cvc5.github.io/docs/cvc5-1.0.2/api/api.html) for C++, Java, and Python.
+* Solver-specific APIs include [CVC5 APIs](https://cvc5.github.io/docs/cvc5-1.0.2/api/api.html) for C++, Java, and Python.
 
 * Z3 has [APIs](https://z3prover.github.io/api/html/index.html) for C, C++, .NET, Java, Python, and ML/OCaml. Additionally, Microsoft Research provides [tutorials](https://microsoft.github.io/z3guide/programming/Z3%20JavaScript%20Examples) for using Z3 in Python and JavaScript.
 
@@ -52,19 +52,3 @@ We provide a high-level interface to SMT solvers. SMT solvers can accept input i
 ## Why is `sat!` so slow for real-valued variables?
 Because the SMT theory of real-valued variables is incomplete.
 
-## Where do all the long, ugly names in the SMT file come from?
-To prevent names from being duplicated, Satisfiability.jl names new expressions using the Julia `hash` of their child expressions.
-
-For example, suppose you have
-```@example
-@satvariable(a, Int)
-@satvariable(b, Int)
-expr = a <= b
-print(smt(expr))
-```
-The (long, ugly) name of the combined expression `a <= b` is generated by hashing the names `a` and `b`.
-
-**Q:** Why don't you just concatenate `a` and `b` and call it `LEQ_a_b`?
-
-**A:** Because what if we have `a = Int(10,"a"); expr = sum(a)`? 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.
-