Functions

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

@satvariable(a[1:n], Int) # an Int vector of length n
@satvariable(x[1:m, 1:n], Real) # an m x n Int matrix

BoolExpr("z")

Construct a single Boolean variable with name "z".

IntExpr("a")

Construct a single IntExpr variable with name "a".

RealExpr("r")

Construct a single Real variable with name "r".

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.

@uninterpreted(f, Int, Bool) # f takes as input IntExpr and returns BoolExpr
@uninterpreted(g, (BitVector, 32), (BitVector, 32)) # g's input and output values are BitVectors of length 32

Define an SMT-LIB uninterpreted function. An uninterpreted function can be thought of as an unknown mapping between input and output values. The task of the SMT solver is then to determine whether a mapping exists such that some Boolean statement is true.

For example, we can ask whether there exists a function f(x)such thatf(f(x)) == x,f(x) == yandx != y`.

@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")

not(z::BoolExpr)
¬z

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.

    @satvariable(z[1:n], Bool)
    ¬z  # syntactic sugar for map(¬, z)
    .¬z # also valid

z1 ∧ z2
and(z1,...,zn)
and([z1,...,zn])

Returns the logical AND of two or more variables. Use dot broadcasting for vector-valued and matrix-valued Boolean expressions.

@satvariable(z1[1:n], Bool)
@satvariable(z2[n, 1:m], Bool)
z1 .∧ z2
and.(z1, z2) # equivalent to z1 .∧ z2

Special cases:

• and(z) returns z.
• and(z, false) returns false.
• and(z, true) returns z.

z1 ∨ z2
or(z1,...,zn)
or([z1,...,zn])

Returns the logical OR of two or more variables. Use dot broadcasting for vector-valued and matrix-valued Boolean expressions.

@satvariable(z1[1:n], Bool)
@satvariable(z2[1:m, 1:n], Bool)
z1 .∨ z2
or.(z1, z2) # equivalent to z1 .∨ z2

Special cases:

• or(z) returns z.
• or(z, false) returns z.
• or(z, true) returns true.

Note that ∨ (\vee) is NOT the ASCII character v.

xor(z1,...,zn)
⊻(z1,...zn)

XOR (exclusive or) is true if exactly one of z1,...,zn is true and false otherwise. Use dot broadcasting across arrays.

Special cases:

• xor(z) returns z.
• xor(false, z) returns z.
• xor(true, z) returns ¬z.
• xor(true, true, z) returns false.

z1 ⟹ z2
implies(z1, z2)

Returns the expression z1 IMPLIES z2. Use dot broadcasting for vector-valued and matrix-valued Boolean expressions. Note: implies(z1, z2) is equivalent to or(not(z1), z2).

iff(z1::BoolExpr, z2::BoolExpr)
z1 ⟺ z2

Bidirectional implication between z1 and z2. Equivalent to and(z1 ⟹ z2, z2 ⟹ z1).

ite(x::BoolExpr, y::AbstractExpr, z::AbstractExpr)

If-then-else statement. When x, y, and z are Bool, equivalent to or(x ∧ y, ¬x ∧ z). Note that y and z may be other expression types. For example, given the variables BoolExpr z and IntExpr a, Satisfiability.jl rewrites z + a as ite(z, 1, 0) + a.

distinct(x, y)
distinct(zs::Array{AbstractExpr})

Returns the SMT-LIB distinct operator. distinct(x, y) is semantically equal to x != y or not(x == y). The syntax distinct(exprs) where exprs is an array of expressions is shorthand for "every element of zs is unique". Thus,

```julia @satvariable(a[1:3], Int)

this statement is true

isequal( distinct(a) and(distinct(a[1], a[2]), distinct(a[1], a[3]), distinct(a[2], a[3])) ) ````

-(a::IntExpr)
-(r::RealExpr)

Return the negative of an Int or Real expression.

@satvariable(a[1:n, 1:m], Int)
-a # this also works

abs(a::IntExpr)

Return the absolute value of an IntExpr.

When called on a RealExpr, abs(a::RealExpr) returns ite(a >= 0, a, -a). This design decision was made because Z3 allows abs to be called on a real-valued expression and returns that result, but abs is only defined in the SMT-LIB standard for integer variables. Thus, users may call abs on real-valued expressions.

a + b
a + 1 + true

Return the Int | Real expression a+b (inherits the type of a+b). Use dot broadcasting for vector-valued and matrix-valued expressions.

@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)
println("typeof a+c: $(typeof(a[1] + c))")

@satvariable(z, Bool)
a .+ z
println("typeof a+z: $(typeof(a[1] + z))")

a - b
a - 2

Returns the Int | Real expression a-b (inherits the type of a-b). Use dot broadcasting for vector-valued and matrix-valued expressions.

@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)
println("typeof a-c: $(typeof(a[1] - c))")

@satvariable(z, Bool)
a .- z
println("typeof a-z: $(typeof(a[1] - z))")

a * b
a * 2

Returns the Int | Real multiplication expression a*b (inherits the type of a*b). Use dot broadcasting for vector-valued and matrix-valued expressions.

@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)
println("typeof a*c: $(typeof(a[1]*c))")

@satvariable(z, Bool)
a .- z
println("typeof a*z: $(typeof(a[1]*z))")

div(a, b)
div(a, 2)

Returns the Int division expression div(a,b). Note: a and b will be converted to IntExpr. Use dot broadcasting for vector-valued and matrix-valued expressions.

@satvariable(a[1:n], Int)
@satvariable(b[1:n, 1:m], Int)
div.(a, b)
println("typeof div(a,b): $(typeof(div(a[1],b[1])))")

mod(a, b)
mod(a, 2)

Returns the Int modulus expression mod(a,b). Note: a and b will be converted to IntExpr. Use dot broadcasting for vector-valued and matrix-valued expressions.

a / b
a / 2.0

Returns the Real division expression a/b. Note: a and b will be converted to RealExpr. Use dot broadcasting for vector-valued and matrix-valued expressions.

@satvariable(a[1:n], Real)
@satvariable(b[1:n, 1:m], Real)
a ./ b
println("typeof a/b: $(typeof(a[1]/b[1]))")

a  == b
a == 1.0

Returns the Boolean expression a == b (arithmetic equivalence). Use dot broadcasting for vector-valued and matrix-valued expressions.

@satvariable(a[1:n], Int)
@satvariable(b[1:n, 1:m], Int)
a .== b

Note: To test whether two AbstractExprs are eqivalent (in the sense that all properties are equal, not in the shared-memory-location sense of ===), use isequal.

a < b
a < 0

Returns the Boolean expression a < b. Use dot broadcasting for vector-valued and matrix-valued expressions.

@satvariable(a[1:n], Int)
@satvariable(b[1:n, 1:m], Int)
a .< b
@satvariable(z, Bool)
a .< z

a <= b
a <= 0

Returns the Boolean expression a <= b. Use dot broadcasting for vector-valued and matrix-valued expressions.

@satvariable(a[1:n], Int)
@satvariable(b[1:n, 1:m], Int)
a .<= b
@satvariable(z, Bool)
a .<= z

a > b
a > 0

Returns the Boolean expression a > b. Use dot broadcasting for vector-valued and matrix-valued expressions.

@satvariable(a[1:n], Int)
@satvariable(b[1:n, 1:m], Int)
a .> b
@satvariable(z, Bool)
a .> z

a >= b
a >= 0

Returns the Boolean expression a >= b. Use dot broadcasting for vector-valued and matrix-valued expressions.

@satvariable(a[1:n], Int)
@satvariable(b[1:n, 1:m], Int)
a .>= b
@satvariable(z, Bool)
a .>= z

to_int(a::RealExpr)

Performs manual conversion of a RealExpr to an IntExpr. Equivalent to Julia Int(floor(a)).

to_real(a::IntExpr)

Performs manual conversion of an IntExpr to a RealExpr. Note that Satisfiability.jl automatically promotes types in arithmetic and comparison expressions, so this function is usually unnecessary to explicitly call.

div(a::BitVectorExpr, b::BitVectorExpr)

Unsigned integer division of two BitVectors.

sdiv(a::BitVectorExpr, b::BitVectorExpr)

Signed integer division of two BitVectors.

~a

Bitwise not.

a | b
or(a, b, c...)

Bitwise or. For n>2 variables, use the or(...) notation.

a & b
and(a, b, c...)

Bitwise and. For n>2 variables, use the and(...) notation.

nor(a, b)
a ⊽ b

Bitwise nor.

nand(a, b)
a ⊼ b

Bitwise nand.

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]).

a << b

Logical left shift a << b.

a >> b

Arithmetic right shift a >> b.

a >>> b

Logical right shift a >>> b.

urem(a::BitVectorExpr, b::BitVectorExpr)

Unsigned remainder of BitVector a divided by BitVector b.

srem(a::BitVectorExpr, b::BitVectorExpr)

Signed remainder of BitVector a divided by BitVector b.

smod(a::BitVectorExpr, b::BitVectorExpr)

Signed modulus of BitVector a divided by BitVector b.

" slt(a::BitVectorExpr, b::BitVectorExpr)

Signed less-than. This is not the same as a < b (unsigned BitVectorExpr comparison).

sle(a::BitVectorExpr, b::BitVectorExpr)

Signed less-than-or-equal. This is not the same as a <+ b (unsigned BitVectorExpr comparison).

sgt(a::BitVectorExpr, b::BitVectorExpr)

Signed greater-than. This is not the same as a > b (unsigned BitVectorExpr comparison).

sge(a::BitVectorExpr, b::BitVectorExpr)

Signed greater-than-or-equal. This is not the same as a >= b (unsigned BitVectorExpr comparison).

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:

    expr = concat(bvconst(0x01, 8), bvconst(0x02, 8), bvconst(0x03, 4))
    println(expr.length) # 20
    println(expr.value) # 0x01023

repeat(a::BitVectorExpr, n)
repeat(bvconst(0xffff, 16), n)

Repeat bitvector a n times.

@satvariable(a, BitVector, 8)
a[4:8] # has length 5
a[3]

Slice or index into a BitVectorExpr, returning a new BitVectorExpr with the appropriate length. This corresponds to the SMT-LIB operation extract.

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

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

bvcomp(a, b)
bvcomp(a, bvconst(a, 0xffff, 16))

Bitwise comparator: iff all bits of a and b are equal, bvcomp(a,b) = 0b1, otherwise 0b0.

zero_extend(a::BitVectorExpr, n::Int)

Pad BitVectorExpr a with zeros. n specifies the number of bits and must be nonnegative.

sign_extend(a::BitVectorExpr, n::Int)

Pad BitVectorExpr a with 0 or 1 depending on its sign. n specifies the number of bits and must be nonnegative.

rotate_left(a::BitVectorExpr, n::Int)

Rotate BitVectorExpr a by n bits left. n must be nonnegative.

rotate_right(a::BitVectorExpr, n::Int)

Rotate BitVectorExpr a by n bits right. n must be nonnegative.

bitcount(a::Integer)

Returns the minimum number of bits required to store the number a.

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.

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.

smt(z::AbstractExpr)
smt(z1,...,zn; assert=true)
smt([z1,...,zn]; assert=true, line_ending='

', as_list=true)

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].

Optional keyword arguments are:

1. assert = true|false: default true. Whether to generate the (assert ...) SMT-LIB statement, which asserts that an expression must be true. This option is only valid if smt is called on a Boolean expression.
2. line_ending: If not set, this defaults to "

" on Windows and ' ' everywhere else.

1. as_list = true|false: default false. When true, smt returns a list of commands instead of a single line_ending-separated string.

save(z1, z2,..., io=open("out.smt", "w"))
save(z1, z2,..., io=open("out.smt", "w", line_ending='

', startcommands=nothing, endcommands=nothing)

Write the SMT representation of z or and(z1,...,zn) to an IO object. Keyword arguments:

• io is a Julia IO object, for example an open file for writing.
• line_ending configures the line ending character. If left off, the default is `

on Windows systems and ` everywhere else.

• start_commands are inserted before smt(z). Typically one uses this to include (set-info ...) or (set-option ...) statements.
• end_commands are inserted after (check-sat). This tends to be less useful unless you already know whether your problem is satisfiable.

sat!(z::BoolExpr, solver=Z3())
sat!(z1, z2,..., solver=CVC5())

Solve the SAT problem using a Solver. If the problem is satisfiable, update the values of all BoolExprs in prob with their satisfying assignments.

Possible return values are :SAT, :UNSAT, or :ERROR. prob is only modified to add Boolean values if the return value is :SAT. By default, sat! will reset the values of expressions in prob to nothing if prob is unsatisfiable. To change this behavior use the keyword argument clear_values_if_unsat. For example,sat!(prob, solver=CVC5(), clear_values_if_unsat=false).

Alternate usage:

    io = open("some_file.smt")
    status, values = sat!(io::IO, solver=CVC5())
    status, values = sat!(filename::String, solver=CVC5())

In io mode, sat! reads the contents of the Julia IO object and passes them to the solver. Thus, users must ensure read(io) will return a complete and correct string of SMT-LIB commands, including (check-sat) or equivalent. Alternatively, one can pass in a filename to be opened and closed within sat!. Because the expressions are not passed into the function, sat! returns a dictionary containing the satisfying assignment.

Optional keyword arguments:

• solver::Solver: The Solver to use. Defaults to Z3().
• logic: Manually set the solver logic. Must be a string corresponding to a valid SMT-LIB logic. If you're unsure how to set this option, don't set it - most solvers can infer the logic to use on their own!
• line_ending::String: The line ending to use after each SMT-LIB command. Defaults to "\r\n" on Windows and "\n" everywhere else.
• clear_values_if_unsat=true: If true and the expression is unsat, reset its values to nothing.
• start_commands::String: Additional SMT-LIB commands to be included before the expression, for example (set-logic LOGIC).
• end_commands::String : Additional SMT-LIB commands to be included after the expression.

interactive_solver = open(Z3()) # open an InteractiveSolver process
status, values = sat!(interactive_solver, exprs...) # check satisfiability of exprs

When working with an InteractiveSolver process, issues the (check-sat) command. The optional exprs, if provided, will be assumed when (check-sat) is issued but not asserted on the stack. This is equivalent to the SMT-LIB (check-sat-assuming expr1, expr2,...) command.

If no assertions have been made, sat! throws an error.

Note that in this mode, sat! can only set the values of exprs provided in the function call That means if you assert(expr1) and then call sat!(interactive_solver, expr2), value(expr1) will be nothing even if the problem is SAT. To alleviate this, sat! returns (status, values) where values is a Dict of variable names and satisfying assignments. To assign the values of expr1, call assign!(values, expr1).

Optional keyword arguments:

• logic: Manually set the solver logic. Must be a string corresponding to a valid SMT-LIB logic. If you're unsure how to set this option, don't set it - most solvers can infer the logic to use on their own!
• line_ending::String: The line ending to use after each SMT-LIB command. Defaults to "\r\n" on Windows and "\n" everywhere else.

value(z::BoolExpr)
value(z::Array{BoolExpr})

Returns the satisfying assignment of z, or nothing if no satisfying assignment is known. In the array-valued case, returns Array{Bool} or Array{nothing}.

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.

interactive_solver = open(s::Solver)

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.

close(s::InteractiveSolver)

Close an InteractiveSolver, cleaning up and terminating its processes and pipes.

push!(solver::InteractiveSolver, n=1)

Push n empty assertion levels onto the solver's assertion stack. Usually push!(solver, 1) is sufficient. If n is 0, no assertion levels are pushed. This corresponds exactly to the SMT-LIB command (push n).

pop!(solver::InteractiveSolver, n=1)

Pop n empty assertion levels off the solver's assertion stack. If n is 0, no assertion levels are pushed. This corresponds exactly to the SMT-LIB command (pop n).

assert!(interactive_solver, expr1, expr2...)
assert!(interactive_solver, exprs::Array)

Assert some expressions. interactive_solver must be an open InteractiveSolver process.

interactive_solver = open(Z3()) # open an InteractiveSolver process
status, values = sat!(interactive_solver, exprs...) # check satisfiability of exprs

When working with an InteractiveSolver process, issues the (check-sat) command. The optional exprs, if provided, will be assumed when (check-sat) is issued but not asserted on the stack. This is equivalent to the SMT-LIB (check-sat-assuming expr1, expr2,...) command.

If no assertions have been made, sat! throws an error.

Note that in this mode, sat! can only set the values of exprs provided in the function call That means if you assert(expr1) and then call sat!(interactive_solver, expr2), value(expr1) will be nothing even if the problem is SAT. To alleviate this, sat! returns (status, values) where values is a Dict of variable names and satisfying assignments. To assign the values of expr1, call assign!(values, expr1).

Optional keyword arguments:

• logic: Manually set the solver logic. Must be a string corresponding to a valid SMT-LIB logic. If you're unsure how to set this option, don't set it - most solvers can infer the logic to use on their own!
• line_ending::String: The line ending to use after each SMT-LIB command. Defaults to "\r\n" on Windows and "\n" everywhere else.

send_command(pstdin::Base.Pipe, pstdout::Base.Pipe, cmd::String; is_done=nested_parens_match, timeout=Inf, line_ending='

')

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.

nested_parens_match(output::String)

Return true if output has > 0 length and an equal number of left ( and right ), which can be 0.

is_sat_or_unsat(output::String)

Return true if output contains "sat" or "unsat".

output = "(
(define-fun x () Bool true)
(define-fun y () Bool false)
(define-fun f ((x!0 Bool)) Bool (ite (= x!0 false) true false))"
dict = parse_model(output)

Parse the SMT-LIB-formatted output of (get-model), returning a Dict of names and values. Values will be of the correct type; thus, in the example dict["x"] will be true. Uninterpreted function values will be Julia functions themselves, thus dict["f"] is a function that accepts a Bool and returns a Bool.

This function is primarily useful when working with InteractiveSolvers.

assign!(e::AbstractExpr, assignment::Dict)
assign!(exprs::Array, assignment::Dict)

Assigns the values of expressions in e (including nested expressions and variables) using assignment, a Dict where every key is a string corresponding to an expression name, and the corresponding value is its satisfying assignment.

assign! is intended to be useful in two cases.

1. Using an assignment dict returned by sat! in interactive mode.This looks like:

    # define some exprs
    interactive_solver = open(solver)
    assert(interactive_solver, exprs...)
    status, assignment = sat!(interactive_solver)
    assign!.(exprs, assignment)

1. Using an assignment dict returned by parse_model, which parses the raw SMT-LIB output of "(get-model)".

reset!(solver::InteractiveSolver)

Resets the solver to its state when first opened, clearning InteractiveSolver.command_history. See section 4.2.1 of the SMT-LIB standard.

reset_assertions!(solver::InteractiveSolver)

Removes all assertions, popping n levels off the solver's assertion stack. After this command, the stack will be at level 1 and there will be no assertions set. See section 4.2.1 of the SMT-LIB standard.

Test equality of two AbstractExprs. To construct an equality constraint, use ==.