Module

Z3.Internal

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

#Z3 Source

data Z3 t0

#Em Source

data Em t0

#Context Source

data Context t0

#Solver Source

data Solver t0

#initz3 Source

initz3 :: forall r. Effect (Promise (Z3 r))

#em Source

em :: forall r. EffectFn1 (Z3 r) (Em r)

#context Source

context :: forall r. EffectFn2 (Z3 r) String (Context r)

#freshContext Source

freshContext :: forall r. EffectFn1 (Z3 r) (Context r)

#solver Source

solver :: forall r. EffectFn1 (Context r) (Solver r)

#optimize Source

optimize :: forall r. EffectFn1 (Context r) (Solver r)

#solverAdd Source

solverAdd :: forall r. EffectFn2 (Solver r) (Z3Bool r) Unit

#solverAddSoft Source

solverAddSoft :: forall r. EffectFn4 (Solver r) (Z3Bool r) Int String Unit

#solverCheck Source

solverCheck :: forall r. EffectFn1 (Solver r) (Promise String)

#maximize Source

maximize :: forall r a. EffectFn2 (Solver r) a Unit

#minimize Source

minimize :: forall r a. EffectFn2 (Solver r) a Unit

#solverModel Source

solverModel :: forall r. EffectFn1 (Solver r) (Model r)

#showModel Source

showModel :: forall r. EffectFn1 (Model r) String

#evalInt Source

evalInt :: forall r. EffectFn2 (Model r) (Z3Int r) BigInt

#evalBool Source

evalBool :: forall r. EffectFn2 (Model r) (Z3Bool r) Boolean

#mkIntVar Source

mkIntVar :: forall r. EffectFn2 (Context r) String (Z3Int r)

#mkIntVal Source

mkIntVal :: forall r. EffectFn2 (Context r) Int (Z3Int r)

#mkIntSort Source

mkIntSort :: forall r. EffectFn1 (Context r) (Z3Sort r (Z3Int r))

#mkBoolVar Source

mkBoolVar :: forall r. EffectFn2 (Context r) String (Z3Bool r)

#mkBoolVal Source

mkBoolVal :: forall r. EffectFn2 (Context r) Boolean (Z3Bool r)

#mkBoolSort Source

mkBoolSort :: forall r. EffectFn1 (Context r) (Z3Sort r (Z3Bool r))

#mkRealVar Source

mkRealVar :: forall r. EffectFn2 (Context r) String (Z3Real r)

#mkRealVal Source

mkRealVal :: forall r. EffectFn2 (Context r) Number (Z3Real r)

#mkRealSort Source

mkRealSort :: forall r. EffectFn1 (Context r) (Z3Sort r (Z3Real r))

#mkArrayVar Source

mkArrayVar :: forall r idx val. EffectFn4 (Context r) String (Z3Sort r idx) (Z3Sort r val) (Z3Array r idx val)

#mkArraySort Source

mkArraySort :: forall r idx val. EffectFn3 (Context r) (Z3Sort r idx) (Z3Sort r val) (Z3Sort r (Z3Array r idx val))

#mkFunDecl Source

mkFunDecl :: forall r dom img. EffectFn4 (Context r) String (Z3Sort r dom) (Z3Sort r img) (Z3Function r dom img)

#mkFunDecl2 Source

mkFunDecl2 :: forall r dom1 dom2 img. EffectFn5 (Context r) String (Z3Sort r dom1) (Z3Sort r dom2) (Z3Sort r img) (Z3Function2 r dom1 dom2 img)

#and Source

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

#or Source

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

#xor Source

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

#implies Source

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

#not_ Source

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

#distinct Source

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

#sum Source

sum :: forall a. Array a -> a

#product Source

product :: forall a. Array a -> a

#unsafeForall Source

unsafeForall :: forall a r. Array a -> Z3Bool r -> Z3Bool r

#unsafeExists Source

unsafeExists :: forall a r. Array a -> Z3Bool r -> Z3Bool r

#unsafeEq Source

unsafeEq :: forall r a b. a -> b -> Z3Bool r

#unsafeNeq Source

unsafeNeq :: forall r a b. a -> b -> Z3Bool r

#unsafeLe Source

unsafeLe :: forall r a b. a -> b -> Z3Bool r

#unsafeGe Source

unsafeGe :: forall r a b. a -> b -> Z3Bool r

#unsafeLt Source

unsafeLt :: forall r a b. a -> b -> Z3Bool r

#unsafeGt Source

unsafeGt :: forall r a b. a -> b -> Z3Bool r

#unsafeAdd Source

unsafeAdd :: forall a b c. a -> b -> c

#unsafeMul Source

unsafeMul :: forall a b c. a -> b -> c

#unsafeSub Source

unsafeSub :: forall a b c. a -> b -> c

#unsafeDiv Source

unsafeDiv :: forall a b c. a -> b -> c

#unsafeMod Source

unsafeMod :: forall a b c. a -> b -> c

#unsafePow Source

unsafePow :: forall a b c. a -> b -> c

#toReal Source

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

#store Source

store :: forall r idx val. Fn3 (Z3Array r idx val) idx val (Z3Array r idx val)

#select Source

select :: forall r idx val. Fn2 (Z3Array r idx val) idx val

#apply Source

apply :: forall r dom img. Fn2 (Z3Function r dom img) dom img

#apply2 Source

apply2 :: forall r dom1 dom2 img. Fn3 (Z3Function2 r dom1 dom2 img) dom1 dom2 img

#killThreads Source

killThreads :: forall r. EffectFn1 (Em r) Unit

Modules: Z3; Z3.Internal; Z3.Types