Module

Z3

Package: purescript-z3
Repository: gbagan/purescript-z3

#Z3 Source

newtype Z3 r mode a

A monad which represents a Z3 computation under a specific context. The `Z3`` monad uses a phantom type to prevent that the computation leaks any Z3 object references to the surrounding computation.

Instances

Functor (Z3 r mode)
Apply (Z3 r mode)
Applicative (Z3 r mode)
Bind (Z3 r mode)
Monad (Z3 r mode)
MonadEffect (Z3 r mode)
MonadAff (Z3 r mode)

#OptMode Source

data OptMode

#Expr Source

class Expr r a | a -> r where

is the class of Z3 expressions (i.e. Z3 ASTs)

Members

sort :: forall (mode :: Type). Z3 r mode (Z3Sort r a)
sort represents the type of a Z3 expression

Instances

Expr r (Z3Int r)
Expr r (Z3Bool r)
Expr r (Z3Real r)
(Expr r idx, Expr r val) => Expr r (Z3Array r idx val)

#Arith Source

class Arith :: forall k1 k2 k3 k4. k1 -> k2 -> k3 -> k4 -> Constraintclass Arith a b c r | a b -> c r

Instances

Arith (Z3Int r) Int (Z3Int r) r
Arith (Z3Int r) BigInt (Z3Int r) r
Arith (Z3Int r) (Z3Int r) (Z3Int r) r
Arith Int (Z3Int r) (Z3Int r) r
Arith BigInt (Z3Int r) (Z3Int r) r
Arith (Z3Real r) (Z3Real r) (Z3Real r) r
Arith (Z3Real r) Number (Z3Real r) r
Arith Number (Z3Real r) (Z3Real r) r

#Equality Source

class Equality :: forall k1 k2 k3. k1 -> k2 -> k3 -> Constraintclass Equality a b r | a b -> r

Instances

Equality (Z3Bool r) (Z3Bool r) r
Equality (Z3Int r) Int r
Equality (Z3Int r) BigInt r
Equality Int (Z3Int r) r
Equality BigInt (Z3Int r) r
Equality (Z3Int r) (Z3Int r) r
Equality (Z3Real r) (Z3Real r) r
Equality (Z3Real r) Number r
Equality Number (Z3Real r) r
Equality (Z3Array r idx val) (Z3Array r idx val) r

#Eval Source

class Eval a b r | a -> b r where

Members

eval :: forall (mode :: Type). Model r -> a -> Z3 r mode b

Instances

Eval (Z3Int r) BigInt r
Eval (Z3Bool r) Boolean r
(Eval a b r) => Eval (Array a) (Array b) r
(RowToList a al, EvalRL al a b r) => Eval (Record a) (Record b) r

#EvalRL Source

class EvalRL :: RowList Type -> Row Type -> Row Type -> Type -> Constraintclass EvalRL aL a b r | aL -> a b r where

Members

evalRL :: forall (mode :: Type). Proxy aL -> Model r -> Record a -> Z3 r mode (Record b)

Instances

EvalRL Nil () () r
(EvalRL tail aTail bTail r, Eval a b r, IsSymbol sym, Lacks sym aTail, Lacks sym bTail, Cons sym a aTail aRow, Cons sym b bTail bRow) => EvalRL (Cons sym a tail) aRow bRow r

#and Source

and :: forall r. Z3Bool r -> Z3Bool r -> Z3Bool r

boolean and between two Z3 expressions

#or Source

or :: forall r. Z3Bool r -> Z3Bool r -> Z3Bool r

boolean or between two Z3 expressions

#xor Source

xor :: forall r. Z3Bool r -> Z3Bool r -> Z3Bool r

boolean xor between two Z3 expressions

#not_ Source

not_ :: forall r. Z3Bool r -> Z3Bool r

boolean not

#implies Source

implies :: forall r. Z3Bool r -> Z3Bool r -> Z3Bool r

boolean imply operator between two Z3 expressions

#eq Source

eq :: forall a b r. Equality a b r => a -> b -> Z3Bool r

#neq Source

neq :: forall a b r. Equality a b r => a -> b -> Z3Bool r

#le Source

le :: forall a b c r. Arith a b c r => a -> b -> Z3Bool r

#ge Source

ge :: forall a b c r. Arith a b c r => a -> b -> Z3Bool r

#lt Source

lt :: forall a b c r. Arith a b c r => a -> b -> Z3Bool r

#gt Source

gt :: forall a b c r. Arith a b c r => a -> b -> Z3Bool r

#add Source

add :: forall a b c r. Arith a b c r => a -> b -> c

#sub Source

sub :: forall a b c r. Arith a b c r => a -> b -> c

#mul Source

mul :: forall a b c r. Arith a b c r => a -> b -> c

#div Source

div :: forall a b c r. Arith a b c r => a -> b -> c

#mod_ Source

mod_ :: forall a b c r. Arith a b c r => a -> b -> c

#pow Source

pow :: forall a b c r. Arith a b c r => a -> b -> c

#distinct Source

distinct :: forall a r. Expr r a => Array a -> Z3Bool r

asserts that all Z3 expressions in the array are distinct

#sum Source

sum :: forall a r. Arith a a a r => Array a -> a

#product Source

product :: forall a r. Arith a a a r => Array a -> a

#forall_ Source

forall_ :: forall a r. Expr r a => Array a -> Z3Bool r -> Z3Bool r

this function does not work with the current latest repository of z3-solver in NPM

#exists Source

exists :: forall a r. Expr r a => Array a -> Z3Bool r -> Z3Bool r

#bool Source

bool :: forall r mode. Z3 r mode (Z3Bool r)

Create a boolean Z3 variable with a fresh name

#boolVal Source

boolVal :: forall r mode. Boolean -> Z3 r mode (Z3Bool r)

Create a boolean Z3 value

#boolVector Source

boolVector :: forall r mode. Int -> Z3 r mode (Array (Z3Bool r))

Create an array of n boolean Z3 variables

#int Source

int :: forall r mode. Z3 r mode (Z3Int r)

Create an integer Z3 variable with a fresh name

#intVal Source

intVal :: forall r mode. Int -> Z3 r mode (Z3Int r)

Create an integer Z3 value

#intVector Source

intVector :: forall r mode. Int -> Z3 r mode (Array (Z3Int r))

Create an array of n integer Z3 variables

#real Source

real :: forall r mode. Z3 r mode (Z3Real r)

Create a boolean Z3 variable with a fresh name

#realVal Source

realVal :: forall r mode. Number -> Z3 r mode (Z3Real r)

Create a real Z3 value

#realVector Source

realVector :: forall r mode. Int -> Z3 r mode (Array (Z3Real r))

Create an array of n real Z3 variables

#toReal Source

toReal :: forall r. Z3Int r -> Z3Real r

#array Source

array :: forall r mode idx val. Expr r idx => Expr r val => Z3 r mode (Z3Array r idx val)

Create an array Z3 variable (not to be confused with an array of Z3 variables)

#function Source

function :: forall r mode dom img. Expr r dom => Expr r img => Z3 r mode (Z3Function r dom img)

declare a function of arity 1

#function2 Source

function2 :: forall r mode dom1 dom2 img. Expr r dom1 => Expr r dom2 => Expr r img => Z3 r mode (Z3Function2 r dom1 dom2 img)

declare a function of arity 2

#apply Source

apply :: forall r dom img. Expr r dom => Expr r img => Z3Function r dom img -> dom -> img

#apply2 Source

apply2 :: forall r dom1 dom2 img. Expr r dom1 => Expr r dom2 => Expr r img => Z3Function2 r dom1 dom2 img -> dom1 -> dom2 -> img

#select Source

select :: forall r idx val. Expr r idx => Expr r val => Z3Array r idx val -> idx -> val

#store Source

store :: forall r idx val. Expr r idx => Expr r val => Z3Array r idx val -> idx -> val -> Z3Array r idx val

#assert Source

assert :: forall r mode. Z3Bool r -> Z3 r mode Unit

Add a new assertion to the solver

#assertSoft Source

assertSoft :: forall r. Z3Bool r -> Int -> String -> Z3 r OptMode Unit

Add a new assertion to the solver

#assertAll Source

assertAll :: forall r mode. Array (Z3Bool r) -> Z3 r mode Unit

Add an array of assertions to the solver

#withModel Source

withModel :: forall r mode a. (Model r -> Z3 r mode a) -> Z3 r mode (Maybe a)

Check if the assertions are satisfiable. If satisfiable, compute a value from the given model

withModel \m → eval m [x, y, z]

#showModel Source

showModel :: forall r mode. Model r -> Z3 r mode String

#minimize Source

minimize :: forall a r. Arith a a a r => a -> Z3 r OptMode Unit

Add objective function to minimize.

#maximize Source

maximize :: forall a r. Arith a a a r => a -> Z3 r OptMode Unit

Add objective function to maximize.

#run Source

run :: forall a. (forall r mode. Z3 r mode a) -> Aff a

Run a Z3 computation.

#runOpt Source

runOpt :: forall a. (forall r. Z3 r OptMode a) -> Aff a

Run a Z3 optimization computation.

Re-exports from Z3.Types

#Z3Sort Source

data Z3Sort t0 t1

#Z3Real Source

data Z3Real t0

#Z3Int Source

data Z3Int t0

#Z3Function2 Source

data Z3Function2 t0 t1 t2 t3

#Z3Function Source

data Z3Function t0 t1 t2

#Z3Bool Source

data Z3Bool t0

#Z3Array Source

data Z3Array t0 t1 t2

#Model Source

data Model t0

Modules: Z3; Z3.Internal; Z3.Types