This is a Julia wrapper for the dReal SMT solver.
dReal allows you to answer satisfiability problems. That is, you can ask questions of the form: **is there some assignment to my variables `julia-observer-quote-cut-paste-0**work`,`

julia-observer-quote-cut-paste-1_*work ,julia-observer-quote-cut-paste-2*

dReal also allows you to do non-linear, constrained, optimisation.

- Linux or OSX: DReal does not support Windows
- libstdc++6: In Ubuntu, please do the following install to install it.
`sudo add-apt-repository --yes ppa:ubuntu-toolchain-r/test # needed for 12.04 sudo apt-get update sudo apt-get install libstdc++6`

You can easily install DReal from a Julia repl with

```
Pkg.update()
Pkg.add("DReal")
```

DReal can then be loaded with:

```
using DReal
```

To ask is there some Integer `x`

and some Integer `y`

such that `x > 2`

and `y < 10`

and `x + 2*y ==7`

, y ou could write:

```
using DReal
x = Var(Int, "x")
y = Var(Int)
add!((x > 2) & (y < 10) & (x + 2*y == 7))
is_satisfiable()
```

The function `Var(Int,"x")`

creates an integer variable named `x`

. You can ommit the name and it will be automatically generated for you; for the most part you won't need to see the name. `x`

will have type `Ex{Int}`

, and when we apply functions to variables we also get back typed `Ex{T}`

values. For instance `x+2y`

will also have type `Ex{Int}`

, but the main constraint `(x > 2) & (y < 10) & (x + 2*y == 7)`

will have type `Ex{Bool}`

, i.e. it is a *proposition*.

Use `add!`

to assert that any proposition `Ex{Bool}`

value must be true. We then use `is_satisfiable`

to solve the system to determine whether there is any assignment to our variables `x`

and `y`

that can makes the expression `x > 2 & y < 10 & x + 2*y == 7`

true.

Similarly to the previous example, we can use create models using Real (`Float64`

) variables:

```
x = Var(Float64,-100.0,100.0)
y = Var(Float64,-100.0,100.0)
add!((x^2 + y^2 > 4) & (x^3 + y < 5))
x,y = model(x,y)
```

This example also shows how to extract a *model*. A model is an assignment of values to variables that makes the model satisfiable. Use `model`

, and any variable used in the system to extract relevant variables in a model. **Note**: `model`

only makes sense when the system is satisfiable, otherwise it will throw an error.

The feature which distinguishes dReal in comparison to other SMT solvers is its powerful support for nonlinear real arithmetic.

Consider an example which slighly modifies a formula from the Flyspeck project benchmarks, taken from the dReal homepage.

```
x1 = Var(Float64, 3.0, 3.14)
x2 = Var(Float64, -7.0, 5.0)
c = (2π - 2*x1*asin(cos(0.797) * sin(π/x1))) <= (-0.591 - 0.0331 *x2 + 0.506 + 1.0)
add!(c)
is_satisfiable() # false
```

dReal supports boolean operators: And (`&`

), Or (`|`

), Not (`!`

), implies (`implies`

or → (`\rightarrow`

)) and if-then-else (`ifelse`

). Biimplications are
represented using equality `==`

. The following example shows how to solve a simple set of Boolean constraints.

```
a = Var(Bool)
b = Var(Bool)
add!(a → b) # \rightarrow - equivalent to implies(a,b)
a,b = model(a,b)
```