Skip to content

Commit

Permalink
Merge pull request #23 from elsoroka/dev
Browse files Browse the repository at this point in the history 
Explicitly promote BoolExprs and IntExprs in mixed int/real arithmetic using `to_real` and `ite`.
  • Loading branch information
@elsoroka
elsoroka authored Dec 2, 2023
2 parents bef8b17 + 125a965 commit bedd606
Show file tree
Hide file tree
Showing 13 changed files with 408 additions and 114 deletions.
62 changes: 36 additions & 26 deletions docs/src/functions.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ An **uninterpreted function** is a function where the mapping between input and


## Logical operations
These are operations in the theory of propositional logic. For a formal definition of this theory, see Figure 3.2 in *The SMT-LIB Standard, Version 2.6* or the SMT-LIB [Core theory declaration](http://smtlib.cs.uiowa.edu/theories.shtml).
These are operations in the theory of propositional logic. For a formal definition of this theory, see Figure 3.2 in [*The SMT-LIB Standard, Version 2.6*](https://smtlib.cs.uiowa.edu/standard.shtml) or the SMT-LIB [Core theory declaration](http://smtlib.cs.uiowa.edu/theories.shtml).
```@docs
not(z::BoolExpr)
and(z1::BoolExpr, z2::BoolExpr)
Expand All @@ -25,21 +25,24 @@ xor(zs_mixed::Array{T}; broadcast_type=:Elementwise) where T
implies(z1::BoolExpr, z2::BoolExpr)
iff(z1::BoolExpr, z2::BoolExpr)
ite(x::Union{BoolExpr, Bool}, y::Union{BoolExpr, Bool}, z::Union{BoolExpr, Bool})
ite(x::BoolExpr, y::BoolExpr, z::BoolExpr)
distinct(z1::BoolExpr, z2::BoolExpr)
```

## Arithmetic operations
These are operations in the theory of integer and real-valued arithmetic.

Note that `+`, `-`, and `*` follow type promotion rules: if both `a` and `b` are `IntExpr`s, `a+b` will have type `IntExpr`. If either `a` or `b` is a `RealExpr`, the result will have type `RealExpr`. Division `\` is defined only in the theory of real-valued arithmetic, thus it always has return type `RealExpr`.
Note that `+`, `-`, and `*` follow type promotion rules: if both `a` and `b` are `IntExpr`s, `a+b` will have type `IntExpr`. If either `a` or `b` is a `RealExpr`, the result will have type `RealExpr`. Integer division `div(a,b)` is defined only for `IntExpr`s. Real-valued division `a\b` is defined only in the theory of real-valued arithmetic.
For a formal definition of the theory of integer arithmetic, see Figure 3.3 in *The SMT-LIB Standard, Version 2.6*.

```@docs
Base.:-(a::IntExpr)
Base.abs(a::IntExpr)
Base.:+(a::IntExpr, b::IntExpr)
Base.:-(a::IntExpr, b::IntExpr)
Base.:*(a::RealExpr, b::RealExpr)
div(a::IntExpr, b::IntExpr)
mod(a::IntExpr, b::IntExpr)
Base.:/(a::RealExpr, b::RealExpr)
```

Expand All @@ -57,6 +60,12 @@ Base.:>(a::IntExpr, b::IntExpr)
Base.:>=(a::IntExpr, b::IntExpr)
```

### Conversion operators
```@docs
to_int(a::RealExpr)
to_real(a::IntExpr)
```

## BitVector
```julia
@satvariable(a, BitVector, 16)
Expand All @@ -68,9 +77,10 @@ The SMT-LIB standard BitVector is often used to represent operations on fixed-si

### Bitwise operators
In addition to supporting the comparison operators above and arithmetic operators `+`, `-`, and `*`, the following BitVector-specific operators are available.
Note that unsigned integer division is available using `div`.
Note that unsigned integer division is available using `div`. Signed division is `sdiv`.
```@docs
Base.div(a::BitVectorExpr{UInt8}, b::BitVectorExpr{UInt8})
sdiv(a::BitVectorExpr{UInt8}, b::BitVectorExpr{UInt8})
```

The bitwise logical operator symbols `&`, `~` and `|` are provided for BitVector types instead of the Boolean logic symbols. This matches Julia's use of bitwise logical operators for Unsigned integer types.
Expand All @@ -79,17 +89,36 @@ The bitwise logical operator symbols `&`, `~` and `|` are provided for BitVector
Base.:~(a::BitVectorExpr{UInt8})
Base.:|(a::BitVectorExpr{UInt8}, b::BitVectorExpr{UInt8})
Base.:&(a::BitVectorExpr{UInt8}, b::BitVectorExpr{UInt8})
nor(a::BitVectorExpr{UInt8}, b::BitVectorExpr{UInt8})
nand(a::BitVectorExpr{UInt8}, b::BitVectorExpr{UInt8})
xnor(a::BitVectorExpr{UInt8}, b::BitVectorExpr{UInt8})
Base.:<<(a::BitVectorExpr{UInt8}, b::BitVectorExpr{UInt8})
Base.:>>(a::BitVectorExpr{UInt8}, b::BitVectorExpr{UInt8})
Base.:>>>(a::BitVectorExpr{UInt8}, b::BitVectorExpr{UInt8})
urem(a::BitVectorExpr{UInt8}, b::BitVectorExpr{UInt8})
srem(a::BitVectorExpr{UInt8}, b::BitVectorExpr{UInt8})
smod(a::BitVectorExpr{UInt8}, b::BitVectorExpr{UInt8})
```
Signed comparisons.
```@docs
slt(a::BitVectorExpr{UInt8}, b::BitVectorExpr{UInt8})
sle(a::BitVectorExpr{UInt8}, b::BitVectorExpr{UInt8})
sgt(a::BitVectorExpr{UInt8}, b::BitVectorExpr{UInt8})
sge(a::BitVectorExpr{UInt8}, b::BitVectorExpr{UInt8})
```

The following word-level operations are also available in the SMT-LIB standard.
The following word-level operations are also available in the SMT-LIB standard, either as core operations or defined in the [SMT-LIB BitVector logic](https://smtlib.cs.uiowa.edu/logics-all.shtml#QF_BV).
```@docs
concat(a::BitVectorExpr{UInt8}, b::BitVectorExpr{UInt8})
concat(a::Array{T}) where T
repeat(a::BitVectorExpr{UInt8}, n::Int64)
Base.getindex(a::BitVectorExpr{UInt8}, ind::UnitRange{Int64})
bv2int(a::BitVectorExpr{UInt8})
int2bv(a::IntExpr, s::Int)
bvcomp(a::BitVectorExpr{UInt8}, b::BitVectorExpr{UInt8})
zero_extend(a::BitVectorExpr{UInt8}, n::Int64)
sign_extend(a::BitVectorExpr{UInt8}, n::Int64)
rotate_left(a::BitVectorExpr{UInt8}, n::Int64)
rotate_right(a::BitVectorExpr{UInt8}, n::Int64)
```

### Utility functions for BitVectors
Expand All @@ -99,30 +128,11 @@ nextsize(n::Integer)
bvconst(c::Integer, size::Int)
```

### Additional Z3 BitVector operators.
Z3 implements the following signed comparisons for BitVectors. Note that these are not part of the SMT-LIB standard and other solvers may not support them.
```@docs
Base.:>>(a::BitVectorExpr{UInt8}, b::BitVectorExpr{UInt8})
srem(a::BitVectorExpr{UInt8}, b::BitVectorExpr{UInt8})
smod(a::BitVectorExpr{UInt8}, b::BitVectorExpr{UInt8})
nor(a::BitVectorExpr{UInt8}, b::BitVectorExpr{UInt8})
nand(a::BitVectorExpr{UInt8}, b::BitVectorExpr{UInt8})
xnor(a::BitVectorExpr{UInt8}, b::BitVectorExpr{UInt8})
```

Signed comparisons are also Z3-specific.
```@docs
slt(a::BitVectorExpr{UInt8}, b::BitVectorExpr{UInt8})
sle(a::BitVectorExpr{UInt8}, b::BitVectorExpr{UInt8})
sgt(a::BitVectorExpr{UInt8}, b::BitVectorExpr{UInt8})
sge(a::BitVectorExpr{UInt8}, b::BitVectorExpr{UInt8})
```

## Generating the SMT representation of a problem

```@docs
smt(zs::Array{T}) where T <: BoolExpr
save(prob::BoolExpr, io::IO)
save(prob::BoolExpr)
```
## Solving a SAT problem

Expand Down
Loading

0 comments on commit bedd606

Please sign in to comment.