{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE MonadComprehensions #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE UnicodeSyntax #-}

module Z3.Tagged
  ( -- * Z3 monad
    Z3
  , module Z3.Opts
  , Logic(..)
  , evalZ3
  , evalZ3With
    -- ** Z3 enviroments
  , Z3Env
  , newEnv

  -- * Types
  , Symbol
  , AST
  , Sort
  , FuncDecl
  , App
  , Pattern
  , Constructor
  , Model
  , Base.Context
  , FuncInterp
  , FuncEntry
  , Params
  , Solver
  , SortKind(..)
  , ASTKind(..)
  -- ** Satisfiability result
  , Result(..)

  -- * Parameters
  , mkParams
  , paramsSetBool
  , paramsSetUInt
  , paramsSetDouble
  , paramsSetSymbol
  , paramsToString

  -- * Symbols
  , mkIntSymbol
  , mkStringSymbol

  -- * Sorts
  , mkUninterpretedSort
  , mkBoolSort
  , mkIntSort
  , mkRealSort
  , mkBvSort
  , mkFiniteDomainSort
  , mkArraySort
  , mkTupleSort
  , mkConstructor
  , mkDatatype
  , mkDatatypes
  , mkSetSort

  -- * Constants and Applications
  , mkFuncDecl
  , mkApp
  , mkConst
  , mkFreshConst
  , mkFreshFuncDecl
  -- ** Helpers
  , mkVar
  , mkBoolVar
  , mkRealVar
  , mkIntVar
  , mkBvVar
  , mkFreshVar
  , mkFreshBoolVar
  , mkFreshRealVar
  , mkFreshIntVar
  , mkFreshBvVar

  -- * Propositional Logic and Equality
  , mkTrue
  , mkFalse
  , mkEq
  , mkNot
  , mkIte
  , mkIff
  , mkImplies
  , mkXor
  , mkAnd
  , mkOr
  , mkDistinct
  -- ** Helpers
  , mkBool

  -- * Arithmetic: Integers and Reals
  , mkAdd
  , mkMul
  , mkSub
  , mkUnaryMinus
  , mkDiv
  , mkMod
  , mkRem
  , mkLt
  , mkLe
  , mkGt
  , mkGe
  , mkInt2Real
  , mkReal2Int
  , mkIsInt

  -- * Bit-vectors
  , mkBvnot
  , mkBvredand
  , mkBvredor
  , mkBvand
  , mkBvor
  , mkBvxor
  , mkBvnand
  , mkBvnor
  , mkBvxnor
  , mkBvneg
  , mkBvadd
  , mkBvsub
  , mkBvmul
  , mkBvudiv
  , mkBvsdiv
  , mkBvurem
  , mkBvsrem
  , mkBvsmod
  , mkBvult
  , mkBvslt
  , mkBvule
  , mkBvsle
  , mkBvuge
  , mkBvsge
  , mkBvugt
  , mkBvsgt
  , mkConcat
  , mkExtract
  , mkSignExt
  , mkZeroExt
  , mkRepeat
  , mkBvshl
  , mkBvlshr
  , mkBvashr
  , mkRotateLeft
  , mkRotateRight
  , mkExtRotateLeft
  , mkExtRotateRight
  , mkInt2bv
  , mkBv2int
  , mkBvnegNoOverflow
  , mkBvaddNoOverflow
  , mkBvaddNoUnderflow
  , mkBvsubNoOverflow
  , mkBvsubNoUnderflow
  , mkBvmulNoOverflow
  , mkBvmulNoUnderflow
  , mkBvsdivNoOverflow

  -- * Arrays
  , mkSelect
  , mkStore
  , mkConstArray
  , mkMap
  , mkArrayDefault

  -- * Sets
  , mkEmptySet
  , mkFullSet
  , mkSetAdd
  , mkSetDel
  , mkSetUnion
  , mkSetIntersect
  , mkSetDifference
  , mkSetComplement
  , mkSetMember
  , mkSetSubset

  -- * Numerals
  , mkNumeral
  , mkInt
  , mkReal
  , mkUnsignedInt
  , mkInt64
  , mkUnsignedInt64
  -- ** Helpers
  , mkIntegral
  , mkRational
  , mkFixed
  , mkRealNum
  , mkInteger
  , mkIntNum
  , mkBitvector
  , mkBvNum

  -- * Quantifiers
  , mkPattern
  , mkBound
  , mkForall
  , mkExists
  , mkForallConst
  , mkExistsConst

  -- * Accessors
  , getSymbolString
  , getSortKind
  , getBvSortSize
  , getDatatypeSortConstructors
  , getDatatypeSortRecognizers
  , getDatatypeSortConstructorAccessors
  , getDeclName
  , getArity
  , getDomain
  , getRange
  , appToAst
  , getAppDecl
  , getAppNumArgs
  , getAppArg
  , getAppArgs
  , getSort
  , getArraySortDomain
  , getArraySortRange
  , getBoolValue
  , getAstKind
  , isApp
  , toApp
  , getNumeralString
  , simplify
  , simplifyEx
  , getIndexValue
  , isQuantifierForall
  , isQuantifierExists
  , getQuantifierWeight
  , getQuantifierNumPatterns
  , getQuantifierPatternAST
  , getQuantifierPatterns
  , getQuantifierNumNoPatterns
  , getQuantifierNoPatternAST
  , getQuantifierNoPatterns
  , getQuantifierNumBound
  , getQuantifierBoundName
  , getQuantifierBoundSort
  , getQuantifierBoundVars
  , getQuantifierBody
  -- ** Helpers
  , getBool
  , getInt
  , getReal
  , getBv

  -- * Modifiers
  , substituteVars

  -- * Models
  , modelEval
  , evalArray
  , getConstInterp
  , getFuncInterp
  , hasInterp
  , numConsts
  , numFuncs
  , getConstDecl
  , getFuncDecl
  , getConsts
  , getFuncs
  , isAsArray
  , addFuncInterp
  , addConstInterp
  , getAsArrayFuncDecl
  , funcInterpGetNumEntries
  , funcInterpGetEntry
  , funcInterpGetElse
  , funcInterpGetArity
  , funcEntryGetValue
  , funcEntryGetNumArgs
  , funcEntryGetArg
  , modelToString
  , showModel
  -- ** Helpers
  , EvalAst
  , eval
  , evalBool
  , evalInt
  , evalReal
  , evalBv
  , evalT
  , mapEval
  , FuncModel(..)
  , evalFunc

  -- * Tactics
  , mkTactic
  , andThenTactic
  , orElseTactic
  , skipTactic
  , tryForTactic
  , mkQuantifierEliminationTactic
  , mkAndInverterGraphTactic
  , applyTactic
  , getApplyResultNumSubgoals
  , getApplyResultSubgoal
  , getApplyResultSubgoals
  , mkGoal
  , goalAssert
  , getGoalSize
  , getGoalFormula
  , getGoalFormulas

  -- * String Conversion
  , ASTPrintMode(..)
  , setASTPrintMode
  , astToString
  , patternToString
  , sortToString
  , funcDeclToString
  , benchmarkToSMTLibString

  -- * Parser interface
  , parseSMTLib2String
  , parseSMTLib2File

  -- * Error Handling
  , Base.Z3Error(..)
  , Base.Z3ErrorCode(..)

  -- * Miscellaneous
  , Version(..)
  , getVersion

  -- * Fixedpoint
  , Fixedpoint
  , fixedpointPush
  , fixedpointPop
  , fixedpointAddRule
  , fixedpointSetParams
  , fixedpointRegisterRelation
  , fixedpointQueryRelations
  , fixedpointGetAnswer
  , fixedpointGetAssertions

  -- * Solvers
  , solverGetHelp
  , solverSetParams
  , solverPush
  , solverPop
  , solverReset
  , solverGetNumScopes
  , solverAssertCnstr
  , solverAssertAndTrack
  , solverCheck
  , solverCheckAssumptions
  , solverGetModel
  , solverGetUnsatCore
  , solverGetReasonUnknown
  , solverToString
  -- ** Helpers
  , assert
  , check
  , checkAssumptions
  , solverCheckAndGetModel
  , solverCheckAssumptionsAndGetModel
  , getModel
  , withModel
  , getUnsatCore
  , push
  , pop
  , local
  , reset
  , getNumScopes
  )
  where

import Z3.Opts
import Z3.Base
  ( FuncModel(..)
  , Result(..)
  , Logic(..)
  , ASTPrintMode(..)
  , Version(..)
  , SortKind(..)
  , ASTKind(..)
  )

import qualified Z3.Base as Base

import Control.Monad ((>=>))
import Control.Monad.ST
import Control.Monad.ST.Unsafe
import Control.Monad.Trans.Class ( lift )
import Control.Monad.Trans.Reader ( ReaderT (..) )
import Data.Coerce ( Coercible, coerce )
import Data.Fixed ( Fixed, HasResolution )
import Data.Int ( Int64 )
import Data.List.NonEmpty ( NonEmpty (..) )
import Data.Traversable ( Traversable )
import qualified Data.Traversable as T
import Data.Word ( Word, Word64 )
import Foreign.Storable

liftF0 :: (Coercible a' a)
       => (Base.Context -> IO a') -> Z3 s a
liftF0 :: (Context -> IO a') -> Z3 s a
liftF0 f :: Context -> IO a'
f = (Z3Env s -> ST s a) -> Z3 s a
forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT ((Z3Env s -> ST s a) -> Z3 s a) -> (Z3Env s -> ST s a) -> Z3 s a
forall a b. (a -> b) -> a -> b
$ \ (Z3Env {..}) -> IO a -> ST s a
forall a s. IO a -> ST s a
unsafeIOToST (IO a -> ST s a) -> IO a -> ST s a
forall a b. (a -> b) -> a -> b
$ (Context -> IO a') -> Context s -> IO a
forall a b. Coercible a b => a -> b
coerce Context -> IO a'
f Context s
context

liftF1 :: (Coercible a' a, Coercible b' b)
       => (Base.Context -> a' -> IO b') -> a -> Z3 s b
liftF1 :: (Context -> a' -> IO b') -> a -> Z3 s b
liftF1 f :: Context -> a' -> IO b'
f a :: a
a = (Z3Env s -> ST s b) -> Z3 s b
forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT ((Z3Env s -> ST s b) -> Z3 s b) -> (Z3Env s -> ST s b) -> Z3 s b
forall a b. (a -> b) -> a -> b
$ \ (Z3Env {..}) -> IO b -> ST s b
forall a s. IO a -> ST s a
unsafeIOToST (IO b -> ST s b) -> IO b -> ST s b
forall a b. (a -> b) -> a -> b
$ (Context -> a' -> IO b') -> Context s -> a -> IO b
forall a b. Coercible a b => a -> b
coerce Context -> a' -> IO b'
f Context s
context a
a

liftF2 :: (Coercible a' a, Coercible b' b, Coercible c' c)
       => (Base.Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 :: (Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 f :: Context -> a' -> b' -> IO c'
f a :: a
a b :: b
b = (Z3Env s -> ST s c) -> Z3 s c
forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT ((Z3Env s -> ST s c) -> Z3 s c) -> (Z3Env s -> ST s c) -> Z3 s c
forall a b. (a -> b) -> a -> b
$ \ (Z3Env {..}) -> IO c -> ST s c
forall a s. IO a -> ST s a
unsafeIOToST (IO c -> ST s c) -> IO c -> ST s c
forall a b. (a -> b) -> a -> b
$ (Context -> a' -> b' -> IO c') -> Context s -> a -> b -> IO c
forall a b. Coercible a b => a -> b
coerce Context -> a' -> b' -> IO c'
f Context s
context a
a b
b

liftF3 :: (Coercible a' a, Coercible b' b, Coercible c' c, Coercible d' d)
       => (Base.Context -> a' -> b' -> c' -> IO d') -> a -> b -> c -> Z3 s d
liftF3 :: (Context -> a' -> b' -> c' -> IO d') -> a -> b -> c -> Z3 s d
liftF3 f :: Context -> a' -> b' -> c' -> IO d'
f a :: a
a b :: b
b c :: c
c = (Z3Env s -> ST s d) -> Z3 s d
forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT ((Z3Env s -> ST s d) -> Z3 s d) -> (Z3Env s -> ST s d) -> Z3 s d
forall a b. (a -> b) -> a -> b
$ \ (Z3Env {..}) -> IO d -> ST s d
forall a s. IO a -> ST s a
unsafeIOToST (IO d -> ST s d) -> IO d -> ST s d
forall a b. (a -> b) -> a -> b
$ (Context -> a' -> b' -> c' -> IO d')
-> Context s -> a -> b -> c -> IO d
forall a b. Coercible a b => a -> b
coerce Context -> a' -> b' -> c' -> IO d'
f Context s
context a
a b
b c
c

liftF4 :: (Coercible a' a, Coercible b' b, Coercible c' c, Coercible d' d, Coercible e' e)
       => (Base.Context -> a' -> b' -> c' -> d' -> IO e') -> a -> b -> c -> d -> Z3 s e
liftF4 :: (Context -> a' -> b' -> c' -> d' -> IO e')
-> a -> b -> c -> d -> Z3 s e
liftF4 f :: Context -> a' -> b' -> c' -> d' -> IO e'
f a :: a
a b :: b
b c :: c
c d :: d
d = (Z3Env s -> ST s e) -> Z3 s e
forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT ((Z3Env s -> ST s e) -> Z3 s e) -> (Z3Env s -> ST s e) -> Z3 s e
forall a b. (a -> b) -> a -> b
$ \ (Z3Env {..}) -> IO e -> ST s e
forall a s. IO a -> ST s a
unsafeIOToST (IO e -> ST s e) -> IO e -> ST s e
forall a b. (a -> b) -> a -> b
$ (Context -> a' -> b' -> c' -> d' -> IO e')
-> Context s -> a -> b -> c -> d -> IO e
forall a b. Coercible a b => a -> b
coerce Context -> a' -> b' -> c' -> d' -> IO e'
f Context s
context a
a b
b c
c d
d

liftF5 :: (Coercible a' a, Coercible b' b, Coercible c' c, Coercible d' d, Coercible e' e, Coercible f' f)
       => (Base.Context -> a' -> b' -> c' -> d' -> e' -> IO f') -> a -> b -> c -> d -> e -> Z3 s f
liftF5 :: (Context -> a' -> b' -> c' -> d' -> e' -> IO f')
-> a -> b -> c -> d -> e -> Z3 s f
liftF5 f :: Context -> a' -> b' -> c' -> d' -> e' -> IO f'
f a :: a
a b :: b
b c :: c
c d :: d
d e :: e
e = (Z3Env s -> ST s f) -> Z3 s f
forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT ((Z3Env s -> ST s f) -> Z3 s f) -> (Z3Env s -> ST s f) -> Z3 s f
forall a b. (a -> b) -> a -> b
$ \ (Z3Env {..}) -> IO f -> ST s f
forall a s. IO a -> ST s a
unsafeIOToST (IO f -> ST s f) -> IO f -> ST s f
forall a b. (a -> b) -> a -> b
$ (Context -> a' -> b' -> c' -> d' -> e' -> IO f')
-> Context s -> a -> b -> c -> d -> e -> IO f
forall a b. Coercible a b => a -> b
coerce Context -> a' -> b' -> c' -> d' -> e' -> IO f'
f Context s
context a
a b
b c
c d
d e
e

liftF6 :: (Coercible a' a, Coercible b' b, Coercible c' c, Coercible d' d, Coercible e' e, Coercible f' f, Coercible g' g)
       => (Base.Context -> a' -> b' -> c' -> d' -> e' -> f' -> IO g') -> a -> b -> c -> d -> e -> f -> Z3 s g
liftF6 :: (Context -> a' -> b' -> c' -> d' -> e' -> f' -> IO g')
-> a -> b -> c -> d -> e -> f -> Z3 s g
liftF6 φ :: Context -> a' -> b' -> c' -> d' -> e' -> f' -> IO g'
φ a :: a
a b :: b
b c :: c
c d :: d
d e :: e
e f :: f
f = (Z3Env s -> ST s g) -> Z3 s g
forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT ((Z3Env s -> ST s g) -> Z3 s g) -> (Z3Env s -> ST s g) -> Z3 s g
forall a b. (a -> b) -> a -> b
$ \ (Z3Env {..}) -> IO g -> ST s g
forall a s. IO a -> ST s a
unsafeIOToST (IO g -> ST s g) -> IO g -> ST s g
forall a b. (a -> b) -> a -> b
$ (Context -> a' -> b' -> c' -> d' -> e' -> f' -> IO g')
-> Context s -> a -> b -> c -> d -> e -> f -> IO g
forall a b. Coercible a b => a -> b
coerce Context -> a' -> b' -> c' -> d' -> e' -> f' -> IO g'
φ Context s
context a
a b
b c
c d
d e
e f
f

liftSolver0 :: (Coercible a' a)
            => (Base.Context -> Base.Solver -> IO a') -> Z3 s a
liftSolver0 :: (Context -> Solver -> IO a') -> Z3 s a
liftSolver0 f :: Context -> Solver -> IO a'
f = (Z3Env s -> ST s a) -> Z3 s a
forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT ((Z3Env s -> ST s a) -> Z3 s a) -> (Z3Env s -> ST s a) -> Z3 s a
forall a b. (a -> b) -> a -> b
$ \ (Z3Env {..}) -> IO a -> ST s a
forall a s. IO a -> ST s a
unsafeIOToST (IO a -> ST s a) -> IO a -> ST s a
forall a b. (a -> b) -> a -> b
$ (Context -> Solver -> IO a') -> Context s -> Solver s -> IO a
forall a b. Coercible a b => a -> b
coerce Context -> Solver -> IO a'
f Context s
context Solver s
solver

liftSolver1 :: (Coercible a' a, Coercible b' b)
            => (Base.Context -> Base.Solver -> a' -> IO b') -> a -> Z3 s b
liftSolver1 :: (Context -> Solver -> a' -> IO b') -> a -> Z3 s b
liftSolver1 f :: Context -> Solver -> a' -> IO b'
f a :: a
a = (Z3Env s -> ST s b) -> Z3 s b
forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT ((Z3Env s -> ST s b) -> Z3 s b) -> (Z3Env s -> ST s b) -> Z3 s b
forall a b. (a -> b) -> a -> b
$ \ (Z3Env {..}) -> IO b -> ST s b
forall a s. IO a -> ST s a
unsafeIOToST (IO b -> ST s b) -> IO b -> ST s b
forall a b. (a -> b) -> a -> b
$ (Context -> Solver -> a' -> IO b')
-> Context s -> Solver s -> a -> IO b
forall a b. Coercible a b => a -> b
coerce Context -> Solver -> a' -> IO b'
f Context s
context Solver s
solver a
a

liftSolver2 :: (Coercible a' a, Coercible b' b, Coercible c' c)
            => (Base.Context -> Base.Solver -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftSolver2 :: (Context -> Solver -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftSolver2 f :: Context -> Solver -> a' -> b' -> IO c'
f a :: a
a b :: b
b = (Z3Env s -> ST s c) -> Z3 s c
forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT ((Z3Env s -> ST s c) -> Z3 s c) -> (Z3Env s -> ST s c) -> Z3 s c
forall a b. (a -> b) -> a -> b
$ \ (Z3Env {..}) -> IO c -> ST s c
forall a s. IO a -> ST s a
unsafeIOToST (IO c -> ST s c) -> IO c -> ST s c
forall a b. (a -> b) -> a -> b
$ (Context -> Solver -> a' -> b' -> IO c')
-> Context s -> Solver s -> a -> b -> IO c
forall a b. Coercible a b => a -> b
coerce Context -> Solver -> a' -> b' -> IO c'
f Context s
context Solver s
solver a
a b
b

liftFixedpoint0 :: (Coercible a' a)
                => (Base.Context -> Base.Fixedpoint -> IO a') -> Z3 s a
liftFixedpoint0 :: (Context -> Fixedpoint -> IO a') -> Z3 s a
liftFixedpoint0 f :: Context -> Fixedpoint -> IO a'
f = (Z3Env s -> ST s a) -> Z3 s a
forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT ((Z3Env s -> ST s a) -> Z3 s a) -> (Z3Env s -> ST s a) -> Z3 s a
forall a b. (a -> b) -> a -> b
$ \ (Z3Env {..}) -> IO a -> ST s a
forall a s. IO a -> ST s a
unsafeIOToST (IO a -> ST s a) -> IO a -> ST s a
forall a b. (a -> b) -> a -> b
$ (Context -> Fixedpoint -> IO a')
-> Context s -> Fixedpoint s -> IO a
forall a b. Coercible a b => a -> b
coerce Context -> Fixedpoint -> IO a'
f Context s
context Fixedpoint s
fixedpoint

liftFixedpoint1 :: (Coercible a' a, Coercible b' b)
                => (Base.Context -> Base.Fixedpoint -> a' -> IO b') -> a -> Z3 s b
liftFixedpoint1 :: (Context -> Fixedpoint -> a' -> IO b') -> a -> Z3 s b
liftFixedpoint1 f :: Context -> Fixedpoint -> a' -> IO b'
f a :: a
a = (Z3Env s -> ST s b) -> Z3 s b
forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT ((Z3Env s -> ST s b) -> Z3 s b) -> (Z3Env s -> ST s b) -> Z3 s b
forall a b. (a -> b) -> a -> b
$ \ (Z3Env {..}) -> IO b -> ST s b
forall a s. IO a -> ST s a
unsafeIOToST (IO b -> ST s b) -> IO b -> ST s b
forall a b. (a -> b) -> a -> b
$ (Context -> Fixedpoint -> a' -> IO b')
-> Context s -> Fixedpoint s -> a -> IO b
forall a b. Coercible a b => a -> b
coerce Context -> Fixedpoint -> a' -> IO b'
f Context s
context Fixedpoint s
fixedpoint a
a

liftFixedpoint2 :: (Coercible a' a, Coercible b' b, Coercible c' c)
                => (Base.Context -> Base.Fixedpoint -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftFixedpoint2 :: (Context -> Fixedpoint -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftFixedpoint2 f :: Context -> Fixedpoint -> a' -> b' -> IO c'
f a :: a
a b :: b
b = (Z3Env s -> ST s c) -> Z3 s c
forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT ((Z3Env s -> ST s c) -> Z3 s c) -> (Z3Env s -> ST s c) -> Z3 s c
forall a b. (a -> b) -> a -> b
$ \ (Z3Env {..}) -> IO c -> ST s c
forall a s. IO a -> ST s a
unsafeIOToST (IO c -> ST s c) -> IO c -> ST s c
forall a b. (a -> b) -> a -> b
$ (Context -> Fixedpoint -> a' -> b' -> IO c')
-> Context s -> Fixedpoint s -> a -> b -> IO c
forall a b. Coercible a b => a -> b
coerce Context -> Fixedpoint -> a' -> b' -> IO c'
f Context s
context Fixedpoint s
fixedpoint a
a b
b

-------------------------------------------------
-- A simple Z3 monad.

type Z3 s = ReaderT (Z3Env s) (ST s)

-- | Z3 environment.
data Z3Env s = Z3Env { Z3Env s -> Solver s
solver :: Solver s, Z3Env s -> Context s
context :: Context s, Z3Env s -> Fixedpoint s
fixedpoint :: Fixedpoint s }

-- | Eval a Z3 script.
evalZ3With :: Maybe Logic -> Opts -> Z3 s a -> ST s a
evalZ3With :: Maybe Logic -> Opts -> Z3 s a -> ST s a
evalZ3With mbLogic :: Maybe Logic
mbLogic opts :: Opts
opts (ReaderT a :: Z3Env s -> ST s a
a) = Z3Env s -> ST s a
a (Z3Env s -> ST s a) -> ST s (Z3Env s) -> ST s a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Maybe Logic -> Opts -> ST s (Z3Env s)
forall s. Maybe Logic -> Opts -> ST s (Z3Env s)
newEnv Maybe Logic
mbLogic Opts
opts

-- | Eval a Z3 script with default configuration options.
evalZ3 :: Z3 s a -> ST s a
evalZ3 :: Z3 s a -> ST s a
evalZ3 = Maybe Logic -> Opts -> Z3 s a -> ST s a
forall s a. Maybe Logic -> Opts -> Z3 s a -> ST s a
evalZ3With Maybe Logic
forall a. Maybe a
Nothing Opts
stdOpts


newEnvWith :: (Base.Config -> IO Base.Context) -> Maybe Logic -> Opts -> ST s (Z3Env s)
newEnvWith :: (Config -> IO Context) -> Maybe Logic -> Opts -> ST s (Z3Env s)
newEnvWith mkContext :: Config -> IO Context
mkContext mbLogic :: Maybe Logic
mbLogic opts :: Opts
opts =
  IO (Z3Env s) -> ST s (Z3Env s)
forall a s. IO a -> ST s a
unsafeIOToST (IO (Z3Env s) -> ST s (Z3Env s))
-> ((Config -> IO (Z3Env s)) -> IO (Z3Env s))
-> (Config -> IO (Z3Env s))
-> ST s (Z3Env s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Config -> IO (Z3Env s)) -> IO (Z3Env s)
forall a. (Config -> IO a) -> IO a
Base.withConfig ((Config -> IO (Z3Env s)) -> ST s (Z3Env s))
-> (Config -> IO (Z3Env s)) -> ST s (Z3Env s)
forall a b. (a -> b) -> a -> b
$ \cfg :: Config
cfg -> do
    Config -> Opts -> IO ()
setOpts Config
cfg Opts
opts
    Context
ctx <- Config -> IO Context
mkContext Config
cfg
    [(Solver Any -> Context Any -> Fixedpoint Any -> Z3Env Any)
-> Solver -> Context -> Fixedpoint -> Z3Env s
forall a b. Coercible a b => a -> b
coerce Solver Any -> Context Any -> Fixedpoint Any -> Z3Env Any
forall k (s :: k). Solver s -> Context s -> Fixedpoint s -> Z3Env s
Z3Env Solver
solver Context
ctx Fixedpoint
fixedpoint
       | Solver
solver <- IO Solver -> (Logic -> IO Solver) -> Maybe Logic -> IO Solver
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Context -> IO Solver
Base.mkSolver Context
ctx) (Context -> Logic -> IO Solver
Base.mkSolverForLogic Context
ctx) Maybe Logic
mbLogic
       , Fixedpoint
fixedpoint <- Context -> IO Fixedpoint
Base.mkFixedpoint Context
ctx]

-- | Create a new Z3 environment.
newEnv :: Maybe Logic -> Opts -> ST s (Z3Env s)
newEnv :: Maybe Logic -> Opts -> ST s (Z3Env s)
newEnv = (Config -> IO Context) -> Maybe Logic -> Opts -> ST s (Z3Env s)
forall s.
(Config -> IO Context) -> Maybe Logic -> Opts -> ST s (Z3Env s)
newEnvWith Config -> IO Context
Base.mkContext

---------------------------------------------------------------------
-- * Parameters

-- | Create a Z3 (empty) parameter set.
--
-- Starting at Z3 4.0, parameter sets are used to configure many components
-- such as: simplifiers, tactics, solvers, etc.
mkParams :: Z3 s (Params s)
mkParams :: Z3 s (Params s)
mkParams = (Context -> IO Params) -> Z3 s (Params s)
forall a' a s. Coercible a' a => (Context -> IO a') -> Z3 s a
liftF0 Context -> IO Params
Base.mkParams

-- | Add a Boolean parameter /k/ with value /v/ to the parameter set /p/.
paramsSetBool :: Params s -> Symbol s -> Bool -> Z3 s ()
paramsSetBool :: Params s -> Symbol s -> Bool -> Z3 s ()
paramsSetBool = (Context -> Params -> Symbol -> Bool -> IO ())
-> Params s -> Symbol s -> Bool -> Z3 s ()
forall a' a b' b c' c d' d s.
(Coercible a' a, Coercible b' b, Coercible c' c, Coercible d' d) =>
(Context -> a' -> b' -> c' -> IO d') -> a -> b -> c -> Z3 s d
liftF3 Context -> Params -> Symbol -> Bool -> IO ()
Base.paramsSetBool

-- | Add a unsigned parameter /k/ with value /v/ to the parameter set /p/.
paramsSetUInt :: Params s -> Symbol s -> Word -> Z3 s ()
paramsSetUInt :: Params s -> Symbol s -> Word -> Z3 s ()
paramsSetUInt = (Context -> Params -> Symbol -> Word -> IO ())
-> Params s -> Symbol s -> Word -> Z3 s ()
forall a' a b' b c' c d' d s.
(Coercible a' a, Coercible b' b, Coercible c' c, Coercible d' d) =>
(Context -> a' -> b' -> c' -> IO d') -> a -> b -> c -> Z3 s d
liftF3 Context -> Params -> Symbol -> Word -> IO ()
Base.paramsSetUInt

-- | Add a double parameter /k/ with value /v/ to the parameter set /p/.
paramsSetDouble :: Params s -> Symbol s -> Double -> Z3 s ()
paramsSetDouble :: Params s -> Symbol s -> Double -> Z3 s ()
paramsSetDouble = (Context -> Params -> Symbol -> Double -> IO ())
-> Params s -> Symbol s -> Double -> Z3 s ()
forall a' a b' b c' c d' d s.
(Coercible a' a, Coercible b' b, Coercible c' c, Coercible d' d) =>
(Context -> a' -> b' -> c' -> IO d') -> a -> b -> c -> Z3 s d
liftF3 Context -> Params -> Symbol -> Double -> IO ()
Base.paramsSetDouble

-- | Add a symbol parameter /k/ with value /v/ to the parameter set /p/.
paramsSetSymbol :: Params s -> Symbol s -> Symbol s -> Z3 s ()
paramsSetSymbol :: Params s -> Symbol s -> Symbol s -> Z3 s ()
paramsSetSymbol = (Context -> Params -> Symbol -> Symbol -> IO ())
-> Params s -> Symbol s -> Symbol s -> Z3 s ()
forall a' a b' b c' c d' d s.
(Coercible a' a, Coercible b' b, Coercible c' c, Coercible d' d) =>
(Context -> a' -> b' -> c' -> IO d') -> a -> b -> c -> Z3 s d
liftF3 Context -> Params -> Symbol -> Symbol -> IO ()
Base.paramsSetSymbol

-- | Convert a parameter set into a string.
--
-- This function is mainly used for printing the contents of a parameter set.
paramsToString :: Params s -> Z3 s String
paramsToString :: Params s -> Z3 s String
paramsToString = (Context -> Params -> IO String) -> Params s -> Z3 s String
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> Params -> IO String
Base.paramsToString

-- TODO: Z3_params_validate

---------------------------------------------------------------------
-- Symbols

-- | Create a Z3 symbol using an integer.
mkIntSymbol :: ∀ i s . Integral i => i -> Z3 s (Symbol s)
mkIntSymbol :: i -> Z3 s (Symbol s)
mkIntSymbol = (Context -> i -> IO Symbol) -> i -> Z3 s (Symbol s)
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 (Integral i => Context -> i -> IO Symbol
forall int. Integral int => Context -> int -> IO Symbol
Base.mkIntSymbol @i)

-- | Create a Z3 symbol using a string.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#gafebb0d3c212927cf7834c3a20a84ecae>
mkStringSymbol :: String -> Z3 s (Symbol s)
mkStringSymbol :: String -> Z3 s (Symbol s)
mkStringSymbol = (Context -> String -> IO Symbol) -> String -> Z3 s (Symbol s)
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> String -> IO Symbol
Base.mkStringSymbol

---------------------------------------------------------------------
-- Sorts

-- | Create a free (uninterpreted) type using the given name (symbol).
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga736e88741af1c178cbebf94c49aa42de>
mkUninterpretedSort :: Symbol s -> Z3 s (Sort s)
mkUninterpretedSort :: Symbol s -> Z3 s (Sort s)
mkUninterpretedSort = (Context -> Symbol -> IO Sort) -> Symbol s -> Z3 s (Sort s)
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> Symbol -> IO Sort
Base.mkUninterpretedSort

-- | Create the /boolean/ type.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#gacdc73510b69a010b71793d429015f342>
mkBoolSort :: Z3 s (Sort s)
mkBoolSort :: Z3 s (Sort s)
mkBoolSort = (Context -> IO Sort) -> Z3 s (Sort s)
forall a' a s. Coercible a' a => (Context -> IO a') -> Z3 s a
liftF0 Context -> IO Sort
Base.mkBoolSort

-- | Create the /integer/ type.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga6cd426ab5748653b77d389fd3eac1015>
mkIntSort :: Z3 s (Sort s)
mkIntSort :: Z3 s (Sort s)
mkIntSort = (Context -> IO Sort) -> Z3 s (Sort s)
forall a' a s. Coercible a' a => (Context -> IO a') -> Z3 s a
liftF0 Context -> IO Sort
Base.mkIntSort

-- | Create the /real/ type.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga40ef93b9738485caed6dc84631c3c1a0>
mkRealSort :: Z3 s (Sort s)
mkRealSort :: Z3 s (Sort s)
mkRealSort = (Context -> IO Sort) -> Z3 s (Sort s)
forall a' a s. Coercible a' a => (Context -> IO a') -> Z3 s a
liftF0 Context -> IO Sort
Base.mkRealSort

-- | Create a bit-vector type of the given size.
--
-- This type can also be seen as a machine integer.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#gaeed000a1bbb84b6ca6fdaac6cf0c1688>
mkBvSort :: ∀ i s . Integral i => i -> Z3 s (Sort s)
mkBvSort :: i -> Z3 s (Sort s)
mkBvSort = (Context -> i -> IO Sort) -> i -> Z3 s (Sort s)
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 (Integral i => Context -> i -> IO Sort
forall int. Integral int => Context -> int -> IO Sort
Base.mkBvSort @i)

-- | Create a finite domain type.
mkFiniteDomainSort :: Symbol s -> Word64 -> Z3 s (Sort s)
mkFiniteDomainSort :: Symbol s -> Word64 -> Z3 s (Sort s)
mkFiniteDomainSort = (Context -> Symbol -> Word64 -> IO Sort)
-> Symbol s -> Word64 -> Z3 s (Sort s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> Symbol -> Word64 -> IO Sort
Base.mkFiniteDomainSort

-- | Create an array type
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#gafe617994cce1b516f46128e448c84445>
--
mkArraySort :: Sort s -> Sort s -> Z3 s (Sort s)
mkArraySort :: Sort s -> Sort s -> Z3 s (Sort s)
mkArraySort = (Context -> Sort -> Sort -> IO Sort)
-> Sort s -> Sort s -> Z3 s (Sort s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> Sort -> Sort -> IO Sort
Base.mkArraySort

-- | Create a tuple type
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga7156b9c0a76a28fae46c81f8e3cdf0f1>
mkTupleSort :: Symbol s                          -- ^ Name of the sort
            -> [(Symbol s, Sort s)]                -- ^ Name and sort of each field
            -> Z3 s (Sort s, FuncDecl s, [FuncDecl s]) -- ^ Resulting sort, and function
                                               -- declarations for the
                                               -- constructor and projections.
mkTupleSort :: Symbol s
-> [(Symbol s, Sort s)] -> Z3 s (Sort s, FuncDecl s, [FuncDecl s])
mkTupleSort = (Context
 -> Symbol -> [(Symbol, Sort)] -> IO (Sort, FuncDecl, [FuncDecl]))
-> Symbol s
-> [(Symbol s, Sort s)]
-> Z3 s (Sort s, FuncDecl s, [FuncDecl s])
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context
-> Symbol -> [(Symbol, Sort)] -> IO (Sort, FuncDecl, [FuncDecl])
Base.mkTupleSort

-- | Create a contructor
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#gaa779e39f7050b9d51857887954b5f9b0>
mkConstructor :: Symbol s                       -- ^ Name of the sonstructor
              -> Symbol s                       -- ^ Name of recognizer function
              -> [(Symbol s, Maybe (Sort s), Int)]  -- ^ Name, sort option, and sortRefs
              -> Z3 s (Constructor s)
mkConstructor :: Symbol s
-> Symbol s
-> [(Symbol s, Maybe (Sort s), Int)]
-> Z3 s (Constructor s)
mkConstructor = (Context
 -> Symbol
 -> Symbol
 -> [(Symbol, Maybe Sort, Int)]
 -> IO Constructor)
-> Symbol s
-> Symbol s
-> [(Symbol s, Maybe (Sort s), Int)]
-> Z3 s (Constructor s)
forall a' a b' b c' c d' d s.
(Coercible a' a, Coercible b' b, Coercible c' c, Coercible d' d) =>
(Context -> a' -> b' -> c' -> IO d') -> a -> b -> c -> Z3 s d
liftF3 Context
-> Symbol
-> Symbol
-> [(Symbol, Maybe Sort, Int)]
-> IO Constructor
Base.mkConstructor

-- | Create datatype, such as lists, trees, records, enumerations or unions of
--   records. The datatype may be recursive. Return the datatype sort.
--
-- Reference <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#gab6809d53327d807da9158abdf75df387>
mkDatatype :: Symbol s
           -> [Constructor s]
           -> Z3 s (Sort s)
mkDatatype :: Symbol s -> [Constructor s] -> Z3 s (Sort s)
mkDatatype = (Context -> Symbol -> [Constructor] -> IO Sort)
-> Symbol s -> [Constructor s] -> Z3 s (Sort s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> Symbol -> [Constructor] -> IO Sort
Base.mkDatatype

-- | Create mutually recursive datatypes, such as a tree and forest.
--
-- Returns the datatype sorts
mkDatatypes :: [Symbol s]
            -> [[Constructor s]]
            -> Z3 s [Sort s]
mkDatatypes :: [Symbol s] -> [[Constructor s]] -> Z3 s [Sort s]
mkDatatypes = (Context -> [Symbol] -> [[Constructor]] -> IO [Sort])
-> [Symbol s] -> [[Constructor s]] -> Z3 s [Sort s]
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> [Symbol] -> [[Constructor]] -> IO [Sort]
Base.mkDatatypes

-- | Create a set type
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga6865879523e7e882d7e50a2d8445ac8b>
--
mkSetSort :: Sort s -> Z3 s (Sort s)
mkSetSort :: Sort s -> Z3 s (Sort s)
mkSetSort = (Context -> Sort -> IO Sort) -> Sort s -> Z3 s (Sort s)
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> Sort -> IO Sort
Base.mkSetSort

---------------------------------------------------------------------
-- Constants and Applications

-- | A Z3 function
mkFuncDecl :: Symbol s -> [Sort s] -> Sort s -> Z3 s (FuncDecl s)
mkFuncDecl :: Symbol s -> [Sort s] -> Sort s -> Z3 s (FuncDecl s)
mkFuncDecl = (Context -> Symbol -> [Sort] -> Sort -> IO FuncDecl)
-> Symbol s -> [Sort s] -> Sort s -> Z3 s (FuncDecl s)
forall a' a b' b c' c d' d s.
(Coercible a' a, Coercible b' b, Coercible c' c, Coercible d' d) =>
(Context -> a' -> b' -> c' -> IO d') -> a -> b -> c -> Z3 s d
liftF3 Context -> Symbol -> [Sort] -> Sort -> IO FuncDecl
Base.mkFuncDecl

-- | Create a constant or function application.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga33a202d86bf628bfab9b6f437536cebe>
mkApp :: FuncDecl s -> [AST s] -> Z3 s (AST s)
mkApp :: FuncDecl s -> [AST s] -> Z3 s (AST s)
mkApp = (Context -> FuncDecl -> [AST] -> IO AST)
-> FuncDecl s -> [AST s] -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> FuncDecl -> [AST] -> IO AST
Base.mkApp

-- | Declare and create a constant.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga093c9703393f33ae282ec5e8729354ef>
mkConst :: Symbol s -> Sort s -> Z3 s (AST s)
mkConst :: Symbol s -> Sort s -> Z3 s (AST s)
mkConst = (Context -> Symbol -> Sort -> IO AST)
-> Symbol s -> Sort s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> Symbol -> Sort -> IO AST
Base.mkConst

-- | Declare and create a constant.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga093c9703393f33ae282ec5e8729354ef>
mkFreshConst :: String -> Sort s -> Z3 s (AST s)
mkFreshConst :: String -> Sort s -> Z3 s (AST s)
mkFreshConst = (Context -> String -> Sort -> IO AST)
-> String -> Sort s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> String -> Sort -> IO AST
Base.mkFreshConst

-- | Declare a fresh constant or function.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga1f60c7eb41c5603e55a188a14dc929ec>
mkFreshFuncDecl :: String -> [Sort s] -> Sort s -> Z3 s (FuncDecl s)
mkFreshFuncDecl :: String -> [Sort s] -> Sort s -> Z3 s (FuncDecl s)
mkFreshFuncDecl = (Context -> String -> [Sort] -> Sort -> IO FuncDecl)
-> String -> [Sort s] -> Sort s -> Z3 s (FuncDecl s)
forall a' a b' b c' c d' d s.
(Coercible a' a, Coercible b' b, Coercible c' c, Coercible d' d) =>
(Context -> a' -> b' -> c' -> IO d') -> a -> b -> c -> Z3 s d
liftF3 Context -> String -> [Sort] -> Sort -> IO FuncDecl
Base.mkFreshFuncDecl

-------------------------------------------------
-- ** Helpers

-- | Declare and create a variable (aka /constant/).
--
-- An alias for 'mkConst'.
mkVar :: Symbol s -> Sort s -> Z3 s (AST s)
mkVar :: Symbol s -> Sort s -> Z3 s (AST s)
mkVar = (Context -> Symbol -> Sort -> IO AST)
-> Symbol s -> Sort s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> Symbol -> Sort -> IO AST
Base.mkVar

-- | Declarate and create a variable of sort /bool/.
--
-- See 'mkVar'.
mkBoolVar :: Symbol s -> Z3 s (AST s)
mkBoolVar :: Symbol s -> Z3 s (AST s)
mkBoolVar = (Context -> Symbol -> IO AST) -> Symbol s -> Z3 s (AST s)
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> Symbol -> IO AST
Base.mkBoolVar

-- | Declarate and create a variable of sort /real/.
--
-- See 'mkVar'.
mkRealVar :: Symbol s -> Z3 s (AST s)
mkRealVar :: Symbol s -> Z3 s (AST s)
mkRealVar = (Context -> Symbol -> IO AST) -> Symbol s -> Z3 s (AST s)
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> Symbol -> IO AST
Base.mkRealVar

-- | Declarate and create a variable of sort /int/.
--
-- See 'mkVar'.
mkIntVar :: Symbol s -> Z3 s (AST s)
mkIntVar :: Symbol s -> Z3 s (AST s)
mkIntVar = (Context -> Symbol -> IO AST) -> Symbol s -> Z3 s (AST s)
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> Symbol -> IO AST
Base.mkIntVar

-- | Declarate and create a variable of sort /bit-vector/.
--
-- See 'mkVar'.
mkBvVar :: Symbol s
                   -> Int     -- ^ bit-width
                   -> Z3 s (AST s)
mkBvVar :: Symbol s -> Int -> Z3 s (AST s)
mkBvVar = (Context -> Symbol -> Int -> IO AST)
-> Symbol s -> Int -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> Symbol -> Int -> IO AST
Base.mkBvVar

-- | Declare and create a /fresh/ variable (aka /constant/).
--
-- An alias for 'mkFreshConst'.
mkFreshVar :: String -> Sort s -> Z3 s (AST s)
mkFreshVar :: String -> Sort s -> Z3 s (AST s)
mkFreshVar = (Context -> String -> Sort -> IO AST)
-> String -> Sort s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> String -> Sort -> IO AST
Base.mkFreshConst

-- | Declarate and create a /fresh/ variable of sort /bool/.
--
-- See 'mkFreshVar'.
mkFreshBoolVar :: String -> Z3 s (AST s)
mkFreshBoolVar :: String -> Z3 s (AST s)
mkFreshBoolVar = (Context -> String -> IO AST) -> String -> Z3 s (AST s)
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> String -> IO AST
Base.mkFreshBoolVar

-- | Declarate and create a /fresh/ variable of sort /real/.
--
-- See 'mkFreshVar'.
mkFreshRealVar :: String -> Z3 s (AST s)
mkFreshRealVar :: String -> Z3 s (AST s)
mkFreshRealVar = (Context -> String -> IO AST) -> String -> Z3 s (AST s)
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> String -> IO AST
Base.mkFreshRealVar

-- | Declarate and create a /fresh/ variable of sort /int/.
--
-- See 'mkFreshVar'.
mkFreshIntVar :: String -> Z3 s (AST s)
mkFreshIntVar :: String -> Z3 s (AST s)
mkFreshIntVar = (Context -> String -> IO AST) -> String -> Z3 s (AST s)
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> String -> IO AST
Base.mkFreshIntVar

-- | Declarate and create a /fresh/ variable of sort /bit-vector/.
--
-- See 'mkFreshVar'.
mkFreshBvVar :: String
                        -> Int     -- ^ bit-width
                        -> Z3 s (AST s)
mkFreshBvVar :: String -> Int -> Z3 s (AST s)
mkFreshBvVar = (Context -> String -> Int -> IO AST)
-> String -> Int -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> String -> Int -> IO AST
Base.mkFreshBvVar

---------------------------------------------------------------------
-- Propositional Logic and Equality

-- | Create an (AST s) node representing /true/.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#gae898e7380409bbc57b56cc5205ef1db7>
mkTrue :: Z3 s (AST s)
mkTrue :: Z3 s (AST s)
mkTrue = (Context -> IO AST) -> Z3 s (AST s)
forall a' a s. Coercible a' a => (Context -> IO a') -> Z3 s a
liftF0 Context -> IO AST
Base.mkTrue

-- | Create an (AST s) node representing /false/.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga5952ac17671117a02001fed6575c778d>
mkFalse :: Z3 s (AST s)
mkFalse :: Z3 s (AST s)
mkFalse = (Context -> IO AST) -> Z3 s (AST s)
forall a' a s. Coercible a' a => (Context -> IO a') -> Z3 s a
liftF0 Context -> IO AST
Base.mkFalse

-- | Create an (AST s) node representing /l = r/.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga95a19ce675b70e22bb0401f7137af37c>
mkEq :: AST s -> AST s -> Z3 s (AST s)
mkEq :: AST s -> AST s -> Z3 s (AST s)
mkEq = (Context -> AST -> AST -> IO AST) -> AST s -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> AST -> IO AST
Base.mkEq

-- | The distinct construct is used for declaring the arguments pairwise
-- distinct.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#gaa076d3a668e0ec97d61744403153ecf7>
mkDistinct :: NonEmpty (AST s) -> Z3 s (AST s)
mkDistinct :: NonEmpty (AST s) -> Z3 s (AST s)
mkDistinct = (Context -> NonEmpty AST -> IO AST)
-> NonEmpty (AST s) -> Z3 s (AST s)
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> NonEmpty AST -> IO AST
Base.mkDistinct1

-- | Create an (AST s) node representing /not(a)/.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga3329538091996eb7b3dc677760a61072>
mkNot :: AST s -> Z3 s (AST s)
mkNot :: AST s -> Z3 s (AST s)
mkNot = (Context -> AST -> IO AST) -> AST s -> Z3 s (AST s)
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> AST -> IO AST
Base.mkNot

-- | Create an (AST s) node representing an if-then-else: /ite(t1, t2, t3)/.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga94417eed5c36e1ad48bcfc8ad6e83547>
mkIte :: AST s -> AST s -> AST s -> Z3 s (AST s)
mkIte :: AST s -> AST s -> AST s -> Z3 s (AST s)
mkIte = (Context -> AST -> AST -> AST -> IO AST)
-> AST s -> AST s -> AST s -> Z3 s (AST s)
forall a' a b' b c' c d' d s.
(Coercible a' a, Coercible b' b, Coercible c' c, Coercible d' d) =>
(Context -> a' -> b' -> c' -> IO d') -> a -> b -> c -> Z3 s d
liftF3 Context -> AST -> AST -> AST -> IO AST
Base.mkIte

-- | Create an (AST s) node representing /t1 iff t2/.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga930a8e844d345fbebc498ac43a696042>
mkIff :: AST s -> AST s -> Z3 s (AST s)
mkIff :: AST s -> AST s -> Z3 s (AST s)
mkIff = (Context -> AST -> AST -> IO AST) -> AST s -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> AST -> IO AST
Base.mkIff

-- | Create an (AST s) node representing /t1 implies t2/.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#gac829c0e25bbbd30343bf073f7b524517>
mkImplies :: AST s -> AST s -> Z3 s (AST s)
mkImplies :: AST s -> AST s -> Z3 s (AST s)
mkImplies = (Context -> AST -> AST -> IO AST) -> AST s -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> AST -> IO AST
Base.mkImplies

-- | Create an (AST s) node representing /t1 xor t2/.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#gacc6d1b848032dec0c4617b594d4229ec>
mkXor :: AST s -> AST s -> Z3 s (AST s)
mkXor :: AST s -> AST s -> Z3 s (AST s)
mkXor = (Context -> AST -> AST -> IO AST) -> AST s -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> AST -> IO AST
Base.mkXor

-- | Create an (AST s) node representing args[0] and ... and args[num_args-1].
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#gacde98ce4a8ed1dde50b9669db4838c61>
mkAnd :: [AST s] -> Z3 s (AST s)
mkAnd :: [AST s] -> Z3 s (AST s)
mkAnd = (Context -> [AST] -> IO AST) -> [AST s] -> Z3 s (AST s)
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> [AST] -> IO AST
Base.mkAnd

-- | Create an (AST s) node representing args[0] or ... or args[num_args-1].
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga00866d16331d505620a6c515302021f9>
mkOr :: [AST s] -> Z3 s (AST s)
mkOr :: [AST s] -> Z3 s (AST s)
mkOr = (Context -> [AST] -> IO AST) -> [AST s] -> Z3 s (AST s)
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> [AST] -> IO AST
Base.mkOr

-------------------------------------------------
-- ** Helpers

-- | Create an (AST s) node representing the given boolean.
mkBool :: Bool -> Z3 s (AST s)
mkBool :: Bool -> Z3 s (AST s)
mkBool = (Context -> Bool -> IO AST) -> Bool -> Z3 s (AST s)
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> Bool -> IO AST
Base.mkBool

---------------------------------------------------------------------
-- Arithmetic: Integers and Reals

-- | Create an (AST s) node representing args[0] + ... + args[num_args-1].
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga4e4ac0a4e53eee0b4b0ef159ed7d0cd5>
mkAdd :: [AST s] -> Z3 s (AST s)
mkAdd :: [AST s] -> Z3 s (AST s)
mkAdd = (Context -> [AST] -> IO AST) -> [AST s] -> Z3 s (AST s)
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> [AST] -> IO AST
Base.mkAdd

-- | Create an (AST s) node representing args[0] * ... * args[num_args-1].
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#gab9affbf8401a18eea474b59ad4adc890>
mkMul :: [AST s] -> Z3 s (AST s)
mkMul :: [AST s] -> Z3 s (AST s)
mkMul = (Context -> [AST] -> IO AST) -> [AST s] -> Z3 s (AST s)
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> [AST] -> IO AST
Base.mkMul

-- | Create an (AST s) node representing args[0] - ... - args[num_args - 1].
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga4f5fea9b683f9e674fd8f14d676cc9a9>
mkSub :: NonEmpty (AST s) -> Z3 s (AST s)
mkSub :: NonEmpty (AST s) -> Z3 s (AST s)
mkSub = (Context -> NonEmpty AST -> IO AST)
-> NonEmpty (AST s) -> Z3 s (AST s)
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> NonEmpty AST -> IO AST
Base.mkSub1

-- | Create an (AST s) node representing -arg.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#gadcd2929ad732937e25f34277ce4988ea>
mkUnaryMinus :: AST s -> Z3 s (AST s)
mkUnaryMinus :: AST s -> Z3 s (AST s)
mkUnaryMinus = (Context -> AST -> IO AST) -> AST s -> Z3 s (AST s)
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> AST -> IO AST
Base.mkUnaryMinus

-- | Create an (AST s) node representing arg1 div arg2.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga1ac60ee8307af8d0b900375914194ff3>
mkDiv :: AST s -> AST s -> Z3 s (AST s)
mkDiv :: AST s -> AST s -> Z3 s (AST s)
mkDiv = (Context -> AST -> AST -> IO AST) -> AST s -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> AST -> IO AST
Base.mkDiv

-- | Create an (AST s) node representing arg1 mod arg2.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga8e350ac77e6b8fe805f57efe196e7713>
mkMod :: AST s -> AST s -> Z3 s (AST s)
mkMod :: AST s -> AST s -> Z3 s (AST s)
mkMod = (Context -> AST -> AST -> IO AST) -> AST s -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> AST -> IO AST
Base.mkMod

-- | Create an (AST s) node representing arg1 rem arg2.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga2fcdb17f9039bbdaddf8a30d037bd9ff>
mkRem :: AST s -> AST s -> Z3 s (AST s)
mkRem :: AST s -> AST s -> Z3 s (AST s)
mkRem = (Context -> AST -> AST -> IO AST) -> AST s -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> AST -> IO AST
Base.mkRem

-- | Create less than.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga58a3dc67c5de52cf599c346803ba1534>
mkLt :: AST s -> AST s -> Z3 s (AST s)
mkLt :: AST s -> AST s -> Z3 s (AST s)
mkLt = (Context -> AST -> AST -> IO AST) -> AST s -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> AST -> IO AST
Base.mkLt

-- | Create less than or equal to.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#gaa9a33d11096841f4e8c407f1578bc0bf>
mkLe :: AST s -> AST s -> Z3 s (AST s)
mkLe :: AST s -> AST s -> Z3 s (AST s)
mkLe = (Context -> AST -> AST -> IO AST) -> AST s -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> AST -> IO AST
Base.mkLe

-- | Create greater than.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga46167b86067586bb742c0557d7babfd3>
mkGt :: AST s -> AST s -> Z3 s (AST s)
mkGt :: AST s -> AST s -> Z3 s (AST s)
mkGt = (Context -> AST -> AST -> IO AST) -> AST s -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> AST -> IO AST
Base.mkGt

-- | Create greater than or equal to.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#gad9245cbadb80b192323d01a8360fb942>
mkGe :: AST s -> AST s -> Z3 s (AST s)
mkGe :: AST s -> AST s -> Z3 s (AST s)
mkGe = (Context -> AST -> AST -> IO AST) -> AST s -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> AST -> IO AST
Base.mkGe

-- | Coerce an integer to a real.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga7130641e614c7ebafd28ae16a7681a21>
mkInt2Real :: AST s -> Z3 s (AST s)
mkInt2Real :: AST s -> Z3 s (AST s)
mkInt2Real = (Context -> AST -> IO AST) -> AST s -> Z3 s (AST s)
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> AST -> IO AST
Base.mkInt2Real

-- | Coerce a real to an integer.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga759b6563ba1204aae55289009a3fdc6d>
mkReal2Int :: AST s -> Z3 s (AST s)
mkReal2Int :: AST s -> Z3 s (AST s)
mkReal2Int = (Context -> AST -> IO AST) -> AST s -> Z3 s (AST s)
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> AST -> IO AST
Base.mkReal2Int

-- | Check if a real number is an integer.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#gaac2ad0fb04e4900fdb4add438d137ad3>
mkIsInt :: AST s -> Z3 s (AST s)
mkIsInt :: AST s -> Z3 s (AST s)
mkIsInt = (Context -> AST -> IO AST) -> AST s -> Z3 s (AST s)
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> AST -> IO AST
Base.mkIsInt

---------------------------------------------------------------------
-- Bit-vectors

-- | Bitwise negation.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga36cf75c92c54c1ca633a230344f23080>
mkBvnot :: AST s -> Z3 s (AST s)
mkBvnot :: AST s -> Z3 s (AST s)
mkBvnot = (Context -> AST -> IO AST) -> AST s -> Z3 s (AST s)
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> AST -> IO AST
Base.mkBvnot

-- | Take conjunction of bits in vector, return vector of length 1.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#gaccc04f2b58903279b1b3be589b00a7d8>
mkBvredand :: AST s -> Z3 s (AST s)
mkBvredand :: AST s -> Z3 s (AST s)
mkBvredand = (Context -> AST -> IO AST) -> AST s -> Z3 s (AST s)
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> AST -> IO AST
Base.mkBvredand

-- | Take disjunction of bits in vector, return vector of length 1.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#gafd18e127c0586abf47ad9cd96895f7d2>
mkBvredor :: AST s -> Z3 s (AST s)
mkBvredor :: AST s -> Z3 s (AST s)
mkBvredor = (Context -> AST -> IO AST) -> AST s -> Z3 s (AST s)
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> AST -> IO AST
Base.mkBvredor

-- | Bitwise and.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#gab96e0ea55334cbcd5a0e79323b57615d>
mkBvand :: AST s -> AST s -> Z3 s (AST s)
mkBvand :: AST s -> AST s -> Z3 s (AST s)
mkBvand  = (Context -> AST -> AST -> IO AST) -> AST s -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> AST -> IO AST
Base.mkBvand

-- | Bitwise or.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga77a6ae233fb3371d187c6d559b2843f5>
mkBvor :: AST s -> AST s -> Z3 s (AST s)
mkBvor :: AST s -> AST s -> Z3 s (AST s)
mkBvor = (Context -> AST -> AST -> IO AST) -> AST s -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> AST -> IO AST
Base.mkBvor

-- | Bitwise exclusive-or.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga0a3821ea00b1c762205f73e4bc29e7d8>
mkBvxor :: AST s -> AST s -> Z3 s (AST s)
mkBvxor :: AST s -> AST s -> Z3 s (AST s)
mkBvxor = (Context -> AST -> AST -> IO AST) -> AST s -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> AST -> IO AST
Base.mkBvxor

-- | Bitwise nand.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga96dc37d36efd658fff5b2b4df49b0e61>
mkBvnand :: AST s -> AST s -> Z3 s (AST s)
mkBvnand :: AST s -> AST s -> Z3 s (AST s)
mkBvnand = (Context -> AST -> AST -> IO AST) -> AST s -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> AST -> IO AST
Base.mkBvnand

-- | Bitwise nor.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#gabf15059e9e8a2eafe4929fdfd259aadb>
mkBvnor :: AST s -> AST s -> Z3 s (AST s)
mkBvnor :: AST s -> AST s -> Z3 s (AST s)
mkBvnor = (Context -> AST -> AST -> IO AST) -> AST s -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> AST -> IO AST
Base.mkBvnor

-- | Bitwise xnor.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga784f5ca36a4b03b93c67242cc94b21d6>
mkBvxnor :: AST s -> AST s -> Z3 s (AST s)
mkBvxnor :: AST s -> AST s -> Z3 s (AST s)
mkBvxnor = (Context -> AST -> AST -> IO AST) -> AST s -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> AST -> IO AST
Base.mkBvxnor

-- | Standard two's complement unary minus.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga0c78be00c03eda4ed6a983224ed5c7b7
mkBvneg :: AST s -> Z3 s (AST s)
mkBvneg :: AST s -> Z3 s (AST s)
mkBvneg = (Context -> AST -> IO AST) -> AST s -> Z3 s (AST s)
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> AST -> IO AST
Base.mkBvneg

-- | Standard two's complement addition.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga819814e33573f3f9948b32fdc5311158>
mkBvadd :: AST s -> AST s -> Z3 s (AST s)
mkBvadd :: AST s -> AST s -> Z3 s (AST s)
mkBvadd = (Context -> AST -> AST -> IO AST) -> AST s -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> AST -> IO AST
Base.mkBvadd

-- | Standard two's complement subtraction.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga688c9aa1347888c7a51be4e46c19178e>
mkBvsub :: AST s -> AST s -> Z3 s (AST s)
mkBvsub :: AST s -> AST s -> Z3 s (AST s)
mkBvsub = (Context -> AST -> AST -> IO AST) -> AST s -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> AST -> IO AST
Base.mkBvsub

-- | Standard two's complement multiplication.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga6abd3dde2a1ceff1704cf7221a72258c>
mkBvmul :: AST s -> AST s -> Z3 s (AST s)
mkBvmul :: AST s -> AST s -> Z3 s (AST s)
mkBvmul = (Context -> AST -> AST -> IO AST) -> AST s -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> AST -> IO AST
Base.mkBvmul

-- | Unsigned division.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga56ce0cd61666c6f8cf5777286f590544>
mkBvudiv :: AST s -> AST s -> Z3 s (AST s)
mkBvudiv :: AST s -> AST s -> Z3 s (AST s)
mkBvudiv = (Context -> AST -> AST -> IO AST) -> AST s -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> AST -> IO AST
Base.mkBvudiv

-- | Two's complement signed division.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#gad240fedb2fda1c1005b8e9d3c7f3d5a0>
mkBvsdiv :: AST s -> AST s -> Z3 s (AST s)
mkBvsdiv :: AST s -> AST s -> Z3 s (AST s)
mkBvsdiv = (Context -> AST -> AST -> IO AST) -> AST s -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> AST -> IO AST
Base.mkBvsdiv

-- | Unsigned remainder.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga5df4298ec835e43ddc9e3e0bae690c8d>
mkBvurem :: AST s -> AST s -> Z3 s (AST s)
mkBvurem :: AST s -> AST s -> Z3 s (AST s)
mkBvurem = (Context -> AST -> AST -> IO AST) -> AST s -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> AST -> IO AST
Base.mkBvurem

-- | Two's complement signed remainder (sign follows dividend).
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga46c18a3042fca174fe659d3185693db1>
mkBvsrem :: AST s -> AST s -> Z3 s (AST s)
mkBvsrem :: AST s -> AST s -> Z3 s (AST s)
mkBvsrem = (Context -> AST -> AST -> IO AST) -> AST s -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> AST -> IO AST
Base.mkBvsrem

-- | Two's complement signed remainder (sign follows divisor).
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga95dac8e6eecb50f63cb82038560e0879>
mkBvsmod :: AST s -> AST s -> Z3 s (AST s)
mkBvsmod :: AST s -> AST s -> Z3 s (AST s)
mkBvsmod = (Context -> AST -> AST -> IO AST) -> AST s -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> AST -> IO AST
Base.mkBvsmod

-- | Unsigned less than.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga5774b22e93abcaf9b594672af6c7c3c4>
mkBvult :: AST s -> AST s -> Z3 s (AST s)
mkBvult :: AST s -> AST s -> Z3 s (AST s)
mkBvult = (Context -> AST -> AST -> IO AST) -> AST s -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> AST -> IO AST
Base.mkBvult

-- | Two's complement signed less than.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga8ce08af4ed1fbdf08d4d6e63d171663a>
mkBvslt :: AST s -> AST s -> Z3 s (AST s)
mkBvslt :: AST s -> AST s -> Z3 s (AST s)
mkBvslt = (Context -> AST -> AST -> IO AST) -> AST s -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> AST -> IO AST
Base.mkBvslt

-- | Unsigned less than or equal to.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#gab738b89de0410e70c089d3ac9e696e87>
mkBvule :: AST s -> AST s -> Z3 s (AST s)
mkBvule :: AST s -> AST s -> Z3 s (AST s)
mkBvule = (Context -> AST -> AST -> IO AST) -> AST s -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> AST -> IO AST
Base.mkBvule

-- | Two's complement signed less than or equal to.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#gab7c026feb93e7d2eab180e96f1e6255d>
mkBvsle :: AST s -> AST s -> Z3 s (AST s)
mkBvsle :: AST s -> AST s -> Z3 s (AST s)
mkBvsle = (Context -> AST -> AST -> IO AST) -> AST s -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> AST -> IO AST
Base.mkBvsle

-- | Unsigned greater than or equal to.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#gade58fbfcf61b67bf8c4a441490d3c4df>
mkBvuge :: AST s -> AST s -> Z3 s (AST s)
mkBvuge :: AST s -> AST s -> Z3 s (AST s)
mkBvuge = (Context -> AST -> AST -> IO AST) -> AST s -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> AST -> IO AST
Base.mkBvuge

-- | Two's complement signed greater than or equal to.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#gaeec3414c0e8a90a6aa5a23af36bf6dc5>
mkBvsge :: AST s -> AST s -> Z3 s (AST s)
mkBvsge :: AST s -> AST s -> Z3 s (AST s)
mkBvsge = (Context -> AST -> AST -> IO AST) -> AST s -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> AST -> IO AST
Base.mkBvsge

-- | Unsigned greater than.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga063ab9f16246c99e5c1c893613927ee3>
mkBvugt :: AST s -> AST s -> Z3 s (AST s)
mkBvugt :: AST s -> AST s -> Z3 s (AST s)
mkBvugt = (Context -> AST -> AST -> IO AST) -> AST s -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> AST -> IO AST
Base.mkBvugt

-- | Two's complement signed greater than.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga4e93a985aa2a7812c7c11a2c65d7c5f0>
mkBvsgt :: AST s -> AST s -> Z3 s (AST s)
mkBvsgt :: AST s -> AST s -> Z3 s (AST s)
mkBvsgt = (Context -> AST -> AST -> IO AST) -> AST s -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> AST -> IO AST
Base.mkBvsgt

-- | Concatenate the given bit-vectors.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#gae774128fa5e9ff7458a36bd10e6ca0fa>
mkConcat :: AST s -> AST s -> Z3 s (AST s)
mkConcat :: AST s -> AST s -> Z3 s (AST s)
mkConcat = (Context -> AST -> AST -> IO AST) -> AST s -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> AST -> IO AST
Base.mkConcat

-- | Extract the bits high down to low from a bitvector of size m to yield a new
-- bitvector of size /n/, where /n = high - low + 1/.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga32d2fe7563f3e6b114c1b97b205d4317>
mkExtract :: Int -> Int -> AST s -> Z3 s (AST s)
mkExtract :: Int -> Int -> AST s -> Z3 s (AST s)
mkExtract = (Context -> Int -> Int -> AST -> IO AST)
-> Int -> Int -> AST s -> Z3 s (AST s)
forall a' a b' b c' c d' d s.
(Coercible a' a, Coercible b' b, Coercible c' c, Coercible d' d) =>
(Context -> a' -> b' -> c' -> IO d') -> a -> b -> c -> Z3 s d
liftF3 Context -> Int -> Int -> AST -> IO AST
Base.mkExtract

-- | Sign-extend of the given bit-vector to the (signed) equivalent bitvector
-- of size /m+i/, where /m/ is the size of the given bit-vector.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#gad29099270b36d0680bb54b560353c10e>
mkSignExt :: Int -> AST s -> Z3 s (AST s)
mkSignExt :: Int -> AST s -> Z3 s (AST s)
mkSignExt = (Context -> Int -> AST -> IO AST) -> Int -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> Int -> AST -> IO AST
Base.mkSignExt

-- | Extend the given bit-vector with zeros to the (unsigned) equivalent
-- bitvector of size /m+i/, where /m/ is the size of the given bit-vector.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#gac9322fae11365a78640baf9078c428b3>
mkZeroExt :: Int -> AST s -> Z3 s (AST s)
mkZeroExt :: Int -> AST s -> Z3 s (AST s)
mkZeroExt = (Context -> Int -> AST -> IO AST) -> Int -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> Int -> AST -> IO AST
Base.mkZeroExt

-- | Repeat the given bit-vector up length /i/.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga03e81721502ea225c264d1f556c9119d>
mkRepeat :: Int -> AST s -> Z3 s (AST s)
mkRepeat :: Int -> AST s -> Z3 s (AST s)
mkRepeat = (Context -> Int -> AST -> IO AST) -> Int -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> Int -> AST -> IO AST
Base.mkRepeat

-- | Shift left.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#gac8d5e776c786c1172fa0d7dfede454e1>
mkBvshl :: AST s -> AST s -> Z3 s (AST s)
mkBvshl :: AST s -> AST s -> Z3 s (AST s)
mkBvshl = (Context -> AST -> AST -> IO AST) -> AST s -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> AST -> IO AST
Base.mkBvshl

-- | Logical shift right.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#gac59645a6edadad79a201f417e4e0c512>
mkBvlshr :: AST s -> AST s -> Z3 s (AST s)
mkBvlshr :: AST s -> AST s -> Z3 s (AST s)
mkBvlshr = (Context -> AST -> AST -> IO AST) -> AST s -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> AST -> IO AST
Base.mkBvlshr

-- | Arithmetic shift right.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga674b580ad605ba1c2c9f9d3748be87c4>
mkBvashr :: AST s -> AST s -> Z3 s (AST s)
mkBvashr :: AST s -> AST s -> Z3 s (AST s)
mkBvashr = (Context -> AST -> AST -> IO AST) -> AST s -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> AST -> IO AST
Base.mkBvashr

-- | Rotate bits of /t1/ to the left /i/ times.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga4932b7d08fea079dd903cd857a52dcda>
mkRotateLeft :: Int -> AST s -> Z3 s (AST s)
mkRotateLeft :: Int -> AST s -> Z3 s (AST s)
mkRotateLeft = (Context -> Int -> AST -> IO AST) -> Int -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> Int -> AST -> IO AST
Base.mkRotateLeft

-- | Rotate bits of /t1/ to the right /i/ times.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga3b94e1bf87ecd1a1858af8ebc1da4a1c>
mkRotateRight :: Int -> AST s -> Z3 s (AST s)
mkRotateRight :: Int -> AST s -> Z3 s (AST s)
mkRotateRight = (Context -> Int -> AST -> IO AST) -> Int -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> Int -> AST -> IO AST
Base.mkRotateRight

-- | Rotate bits of /t1/ to the left /t2/ times.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#gaf46f1cb80e5a56044591a76e7c89e5e7>
mkExtRotateLeft :: AST s -> AST s -> Z3 s (AST s)
mkExtRotateLeft :: AST s -> AST s -> Z3 s (AST s)
mkExtRotateLeft = (Context -> AST -> AST -> IO AST) -> AST s -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> AST -> IO AST
Base.mkExtRotateLeft

-- | Rotate bits of /t1/ to the right /t2/ times.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#gabb227526c592b523879083f12aab281f>
mkExtRotateRight :: AST s -> AST s -> Z3 s (AST s)
mkExtRotateRight :: AST s -> AST s -> Z3 s (AST s)
mkExtRotateRight = (Context -> AST -> AST -> IO AST) -> AST s -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> AST -> IO AST
Base.mkExtRotateRight

-- | Create an /n/ bit bit-vector from the integer argument /t1/.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga35f89eb05df43fbd9cce7200cc1f30b5>
mkInt2bv :: Int -> AST s -> Z3 s (AST s)
mkInt2bv :: Int -> AST s -> Z3 s (AST s)
mkInt2bv = (Context -> Int -> AST -> IO AST) -> Int -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> Int -> AST -> IO AST
Base.mkInt2bv

-- | Create an integer from the bit-vector argument /t1/. If /is_signed/ is false,
-- then the bit-vector /t1/ is treated as unsigned. So the result is non-negative
-- and in the range [0..2^/N/-1], where /N/ are the number of bits in /t1/.
-- If /is_signed/ is true, /t1/ is treated as a signed bit-vector.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#gac87b227dc3821d57258d7f53a28323d4>
mkBv2int :: AST s -> Bool -> Z3 s (AST s)
mkBv2int :: AST s -> Bool -> Z3 s (AST s)
mkBv2int = (Context -> AST -> Bool -> IO AST) -> AST s -> Bool -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> Bool -> IO AST
Base.mkBv2int

-- | Create a predicate that checks that the bit-wise addition of /t1/ and /t2/
-- does not overflow.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga88f6b5ec876f05e0d7ba51e96c4b077f>
mkBvaddNoOverflow :: AST s -> AST s -> Bool -> Z3 s (AST s)
mkBvaddNoOverflow :: AST s -> AST s -> Bool -> Z3 s (AST s)
mkBvaddNoOverflow = (Context -> AST -> AST -> Bool -> IO AST)
-> AST s -> AST s -> Bool -> Z3 s (AST s)
forall a' a b' b c' c d' d s.
(Coercible a' a, Coercible b' b, Coercible c' c, Coercible d' d) =>
(Context -> a' -> b' -> c' -> IO d') -> a -> b -> c -> Z3 s d
liftF3 Context -> AST -> AST -> Bool -> IO AST
Base.mkBvaddNoOverflow

-- | Create a predicate that checks that the bit-wise signed addition of /t1/
-- and /t2/ does not underflow.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga1e2b1927cf4e50000c1600d47a152947>
mkBvaddNoUnderflow :: AST s -> AST s -> Z3 s (AST s)
mkBvaddNoUnderflow :: AST s -> AST s -> Z3 s (AST s)
mkBvaddNoUnderflow = (Context -> AST -> AST -> IO AST) -> AST s -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> AST -> IO AST
Base.mkBvaddNoUnderflow

-- | Create a predicate that checks that the bit-wise signed subtraction of /t1/
-- and /t2/ does not overflow.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga785f8127b87e0b42130e6d8f52167d7c>
mkBvsubNoOverflow :: AST s -> AST s -> Z3 s (AST s)
mkBvsubNoOverflow :: AST s -> AST s -> Z3 s (AST s)
mkBvsubNoOverflow = (Context -> AST -> AST -> IO AST) -> AST s -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> AST -> IO AST
Base.mkBvsubNoOverflow

-- | Create a predicate that checks that the bit-wise subtraction of /t1/ and
-- /t2/ does not underflow.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga6480850f9fa01e14aea936c88ff184c4>
mkBvsubNoUnderflow :: AST s -> AST s -> Z3 s (AST s)
mkBvsubNoUnderflow :: AST s -> AST s -> Z3 s (AST s)
mkBvsubNoUnderflow = (Context -> AST -> AST -> IO AST) -> AST s -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> AST -> IO AST
Base.mkBvsubNoUnderflow

-- | Create a predicate that checks that the bit-wise signed division of /t1/
-- and /t2/ does not overflow.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#gaa17e7b2c33dfe2abbd74d390927ae83e>
mkBvsdivNoOverflow :: AST s -> AST s -> Z3 s (AST s)
mkBvsdivNoOverflow :: AST s -> AST s -> Z3 s (AST s)
mkBvsdivNoOverflow = (Context -> AST -> AST -> IO AST) -> AST s -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> AST -> IO AST
Base.mkBvsdivNoOverflow

-- | Check that bit-wise negation does not overflow when /t1/ is interpreted as
-- a signed bit-vector.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#gae9c5d72605ddcd0e76657341eaccb6c7>
mkBvnegNoOverflow :: AST s -> Z3 s (AST s)
mkBvnegNoOverflow :: AST s -> Z3 s (AST s)
mkBvnegNoOverflow = (Context -> AST -> IO AST) -> AST s -> Z3 s (AST s)
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> AST -> IO AST
Base.mkBvnegNoOverflow

-- | Create a predicate that checks that the bit-wise multiplication of /t1/ and
-- /t2/ does not overflow.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga86f4415719d295a2f6845c70b3aaa1df>
mkBvmulNoOverflow :: AST s -> AST s -> Bool -> Z3 s (AST s)
mkBvmulNoOverflow :: AST s -> AST s -> Bool -> Z3 s (AST s)
mkBvmulNoOverflow = (Context -> AST -> AST -> Bool -> IO AST)
-> AST s -> AST s -> Bool -> Z3 s (AST s)
forall a' a b' b c' c d' d s.
(Coercible a' a, Coercible b' b, Coercible c' c, Coercible d' d) =>
(Context -> a' -> b' -> c' -> IO d') -> a -> b -> c -> Z3 s d
liftF3 Context -> AST -> AST -> Bool -> IO AST
Base.mkBvmulNoOverflow

-- | Create a predicate that checks that the bit-wise signed multiplication of
-- /t1/ and /t2/ does not underflow.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga501ccc01d737aad3ede5699741717fda>
mkBvmulNoUnderflow :: AST s -> AST s -> Z3 s (AST s)
mkBvmulNoUnderflow :: AST s -> AST s -> Z3 s (AST s)
mkBvmulNoUnderflow = (Context -> AST -> AST -> IO AST) -> AST s -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> AST -> IO AST
Base.mkBvmulNoUnderflow

---------------------------------------------------------------------
-- Arrays

-- | Array read. The argument a is the array and i is the index of the array
-- that gets read.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga38f423f3683379e7f597a7fe59eccb67>
mkSelect :: AST s -> AST s -> Z3 s (AST s)
mkSelect :: AST s -> AST s -> Z3 s (AST s)
mkSelect = (Context -> AST -> AST -> IO AST) -> AST s -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> AST -> IO AST
Base.mkSelect

-- | Array update.   
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#gae305a4f54b4a64f7e5973ae6ccb13593>
mkStore :: AST s -> AST s -> AST s -> Z3 s (AST s)
mkStore :: AST s -> AST s -> AST s -> Z3 s (AST s)
mkStore = (Context -> AST -> AST -> AST -> IO AST)
-> AST s -> AST s -> AST s -> Z3 s (AST s)
forall a' a b' b c' c d' d s.
(Coercible a' a, Coercible b' b, Coercible c' c, Coercible d' d) =>
(Context -> a' -> b' -> c' -> IO d') -> a -> b -> c -> Z3 s d
liftF3 Context -> AST -> AST -> AST -> IO AST
Base.mkStore

-- | Create the constant array.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga84ea6f0c32b99c70033feaa8f00e8f2d>
mkConstArray :: Sort s -> AST s -> Z3 s (AST s)
mkConstArray :: Sort s -> AST s -> Z3 s (AST s)
mkConstArray = (Context -> Sort -> AST -> IO AST)
-> Sort s -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> Sort -> AST -> IO AST
Base.mkConstArray

-- | map f on the the argument arrays.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga9150242d9430a8c3d55d2ca3b9a4362d>
mkMap :: FuncDecl s -> [AST s] -> Z3 s (AST s)
mkMap :: FuncDecl s -> [AST s] -> Z3 s (AST s)
mkMap = (Context -> FuncDecl -> [AST] -> IO AST)
-> FuncDecl s -> [AST s] -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> FuncDecl -> [AST] -> IO AST
Base.mkMap

-- | Access the array default value. Produces the default range value, for
-- arrays that can be represented as finite maps with a default range value.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga78e89cca82f0ab4d5f4e662e5e5fba7d>
mkArrayDefault :: AST s -> Z3 s (AST s)
mkArrayDefault :: AST s -> Z3 s (AST s)
mkArrayDefault = (Context -> AST -> IO AST) -> AST s -> Z3 s (AST s)
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> AST -> IO AST
Base.mkArrayDefault

---------------------------------------------------------------------
-- Sets

-- | Create the empty set.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga358b6b80509a567148f1c0ca9252118c>
mkEmptySet :: Sort s -> Z3 s (AST s)
mkEmptySet :: Sort s -> Z3 s (AST s)
mkEmptySet = (Context -> Sort -> IO AST) -> Sort s -> Z3 s (AST s)
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> Sort -> IO AST
Base.mkEmptySet

-- | Create the full set.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga5e92662c657374f7332aa32ce4503dd2>
mkFullSet :: Sort s -> Z3 s (AST s)
mkFullSet :: Sort s -> Z3 s (AST s)
mkFullSet = (Context -> Sort -> IO AST) -> Sort s -> Z3 s (AST s)
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> Sort -> IO AST
Base.mkFullSet

-- | Add an element to a set.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga856c3d0e28ce720f53912c2bbdd76175>
mkSetAdd :: AST s -> AST s -> Z3 s (AST s)
mkSetAdd :: AST s -> AST s -> Z3 s (AST s)
mkSetAdd = (Context -> AST -> AST -> IO AST) -> AST s -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> AST -> IO AST
Base.mkSetAdd

-- | Remove an element from a set.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga80e883f39dd3b88f9d0745c8a5b91d1d>
mkSetDel :: AST s -> AST s -> Z3 s (AST s)
mkSetDel :: AST s -> AST s -> Z3 s (AST s)
mkSetDel = (Context -> AST -> AST -> IO AST) -> AST s -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> AST -> IO AST
Base.mkSetDel

-- | Take the union of a list of sets.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga4050162a13d539b8913200963bb4743c>
mkSetUnion :: [AST s] -> Z3 s (AST s)
mkSetUnion :: [AST s] -> Z3 s (AST s)
mkSetUnion = (Context -> [AST] -> IO AST) -> [AST s] -> Z3 s (AST s)
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> [AST] -> IO AST
Base.mkSetUnion

-- | Take the intersection of a list of sets.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga8a8abff0ebe6aeeaa6c919eaa013049d>
mkSetIntersect :: [AST s] -> Z3 s (AST s)
mkSetIntersect :: [AST s] -> Z3 s (AST s)
mkSetIntersect = (Context -> [AST] -> IO AST) -> [AST s] -> Z3 s (AST s)
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> [AST] -> IO AST
Base.mkSetIntersect

-- | Take the set difference between two sets.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#gabb49c62f70b8198362e1a29ba6d8bde1>
mkSetDifference :: AST s -> AST s -> Z3 s (AST s)
mkSetDifference :: AST s -> AST s -> Z3 s (AST s)
mkSetDifference = (Context -> AST -> AST -> IO AST) -> AST s -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> AST -> IO AST
Base.mkSetDifference

-- | Take the complement of a set.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga5c57143c9229cdf730c5103ff696590f>
mkSetComplement :: AST s -> Z3 s (AST s)
mkSetComplement :: AST s -> Z3 s (AST s)
mkSetComplement = (Context -> AST -> IO AST) -> AST s -> Z3 s (AST s)
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> AST -> IO AST
Base.mkSetComplement

-- | Check for set membership.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#gac6e516f3dce0bdd41095c6d6daf56063>
mkSetMember :: AST s -> AST s -> Z3 s (AST s)
mkSetMember :: AST s -> AST s -> Z3 s (AST s)
mkSetMember = (Context -> AST -> AST -> IO AST) -> AST s -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> AST -> IO AST
Base.mkSetMember

-- | Check if the first set is a subset of the second set.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga139c5803af0e86464adc7cedc53e7f3a>
mkSetSubset :: AST s -> AST s -> Z3 s (AST s)
mkSetSubset :: AST s -> AST s -> Z3 s (AST s)
mkSetSubset = (Context -> AST -> AST -> IO AST) -> AST s -> AST s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> AST -> IO AST
Base.mkSetSubset

---------------------------------------------------------------------
-- * Numerals

-- | Create a numeral of a given sort.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#gac8aca397e32ca33618d8024bff32948c>
mkNumeral :: String -> Sort s -> Z3 s (AST s)
mkNumeral :: String -> Sort s -> Z3 s (AST s)
mkNumeral = (Context -> String -> Sort -> IO AST)
-> String -> Sort s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> String -> Sort -> IO AST
Base.mkNumeral

-- | Create a numeral of sort /real/.
mkReal :: Int -> Int -> Z3 s (AST s)
mkReal :: Int -> Int -> Z3 s (AST s)
mkReal = (Context -> Int -> Int -> IO AST) -> Int -> Int -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> Int -> Int -> IO AST
Base.mkReal

-- | Create a numeral of an int, bit-vector, or finite-domain sort.
--
-- This function can be use to create numerals that fit in a
-- /machine integer/.
-- It is slightly faster than 'mkNumeral' since it is not necessary
-- to parse a string.
mkInt :: Int -> Sort s -> Z3 s (AST s)
mkInt :: Int -> Sort s -> Z3 s (AST s)
mkInt = (Context -> Int -> Sort -> IO AST) -> Int -> Sort s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> Int -> Sort -> IO AST
Base.mkInt

-- | Create a numeral of an int, bit-vector, or finite-domain sort.
--
-- This function can be use to create numerals that fit in a
-- /machine unsigned integer/.
-- It is slightly faster than 'mkNumeral' since it is not necessary
-- to parse a string.
mkUnsignedInt :: Word -> Sort s -> Z3 s (AST s)
mkUnsignedInt :: Word -> Sort s -> Z3 s (AST s)
mkUnsignedInt = (Context -> Word -> Sort -> IO AST)
-> Word -> Sort s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> Word -> Sort -> IO AST
Base.mkUnsignedInt

-- | Create a numeral of an int, bit-vector, or finite-domain sort.
--
-- This function can be use to create numerals that fit in a
-- /machine 64-bit integer/.
-- It is slightly faster than 'mkNumeral' since it is not necessary
-- to parse a string.
mkInt64 :: Int64 -> Sort s -> Z3 s (AST s)
mkInt64 :: Int64 -> Sort s -> Z3 s (AST s)
mkInt64 = (Context -> Int64 -> Sort -> IO AST)
-> Int64 -> Sort s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> Int64 -> Sort -> IO AST
Base.mkInt64

-- | Create a numeral of an int, bit-vector, or finite-domain sort.
--
-- This function can be use to create numerals that fit in a
-- /machine unsigned 64-bit integer/.
-- It is slightly faster than 'mkNumeral' since it is not necessary
-- to parse a string.
mkUnsignedInt64 :: Word64 -> Sort s -> Z3 s (AST s)
mkUnsignedInt64 :: Word64 -> Sort s -> Z3 s (AST s)
mkUnsignedInt64 = (Context -> Word64 -> Sort -> IO AST)
-> Word64 -> Sort s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> Word64 -> Sort -> IO AST
Base.mkUnsignedInt64

-------------------------------------------------
-- ** Helpers

-- | Create a numeral of an int, bit-vector, or finite-domain sort.
mkIntegral :: ∀ a s . (Integral a) => a -> Sort s -> Z3 s (AST s)
mkIntegral :: a -> Sort s -> Z3 s (AST s)
mkIntegral = (Context -> a -> Sort -> IO AST) -> a -> Sort s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 (Integral a => Context -> a -> Sort -> IO AST
forall a. Integral a => Context -> a -> Sort -> IO AST
Base.mkIntegral @a)

-- | Create a numeral of sort /real/ from a 'Rational'.
mkRational :: Rational -> Z3 s (AST s)
mkRational :: Rational -> Z3 s (AST s)
mkRational = (Context -> Rational -> IO AST) -> Rational -> Z3 s (AST s)
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> Rational -> IO AST
Base.mkRational

-- | Create a numeral of sort /real/ from a 'Fixed'.
mkFixed :: ∀ a s . (HasResolution a) => Fixed a -> Z3 s (AST s)
mkFixed :: Fixed a -> Z3 s (AST s)
mkFixed = (Context -> Fixed a -> IO AST) -> Fixed a -> Z3 s (AST s)
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 (HasResolution a => Context -> Fixed a -> IO AST
forall a. HasResolution a => Context -> Fixed a -> IO AST
Base.mkFixed @a)

-- | Create a numeral of sort /real/ from a 'Real'.
mkRealNum :: ∀ r s . (Real r) => r -> Z3 s (AST s)
mkRealNum :: r -> Z3 s (AST s)
mkRealNum = (Context -> r -> IO AST) -> r -> Z3 s (AST s)
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 (Real r => Context -> r -> IO AST
forall r. Real r => Context -> r -> IO AST
Base.mkRealNum @r)

-- | Create a numeral of sort /int/ from an 'Integer'.
mkInteger :: Integer -> Z3 s (AST s)
mkInteger :: Integer -> Z3 s (AST s)
mkInteger = (Context -> Integer -> IO AST) -> Integer -> Z3 s (AST s)
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> Integer -> IO AST
Base.mkInteger

-- | Create a numeral of sort /int/ from an 'Integral'.
mkIntNum :: ∀ a s . (Integral a) => a -> Z3 s (AST s)
mkIntNum :: a -> Z3 s (AST s)
mkIntNum = (Context -> a -> IO AST) -> a -> Z3 s (AST s)
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 (Integral a => Context -> a -> IO AST
forall a. Integral a => Context -> a -> IO AST
Base.mkIntNum @a)

-- | Create a numeral of sort /Bit-vector/ from an 'Integer'.
mkBitvector :: Int      -- ^ bit-width
                          -> Integer  -- ^ integer value
                          -> Z3 s (AST s)
mkBitvector :: Int -> Integer -> Z3 s (AST s)
mkBitvector = (Context -> Int -> Integer -> IO AST)
-> Int -> Integer -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> Int -> Integer -> IO AST
Base.mkBitvector

-- | Create a numeral of sort /Bit-vector/ from an 'Integral'.
mkBvNum :: ∀ i s .
           (Integral i) => Int    -- ^ bit-width
                        -> i      -- ^ integer value
                        -> Z3 s (AST s)
mkBvNum :: Int -> i -> Z3 s (AST s)
mkBvNum = (Context -> Int -> i -> IO AST) -> Int -> i -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 (Integral i => Context -> Int -> i -> IO AST
forall i. Integral i => Context -> Int -> i -> IO AST
Base.mkBvNum @i)

---------------------------------------------------------------------
-- Quantifiers

mkPattern :: [AST s] -> Z3 s (Pattern s)
mkPattern :: [AST s] -> Z3 s (Pattern s)
mkPattern = (Context -> [AST] -> IO Pattern) -> [AST s] -> Z3 s (Pattern s)
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> [AST] -> IO Pattern
Base.mkPattern

mkBound :: Int -> Sort s -> Z3 s (AST s)
mkBound :: Int -> Sort s -> Z3 s (AST s)
mkBound = (Context -> Int -> Sort -> IO AST) -> Int -> Sort s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> Int -> Sort -> IO AST
Base.mkBound

mkForall :: [Pattern s] -> [Symbol s] -> [Sort s] -> AST s -> Z3 s (AST s)
mkForall :: [Pattern s] -> [Symbol s] -> [Sort s] -> AST s -> Z3 s (AST s)
mkForall = (Context -> [Pattern] -> [Symbol] -> [Sort] -> AST -> IO AST)
-> [Pattern s] -> [Symbol s] -> [Sort s] -> AST s -> Z3 s (AST s)
forall a' a b' b c' c d' d e' e s.
(Coercible a' a, Coercible b' b, Coercible c' c, Coercible d' d,
 Coercible e' e) =>
(Context -> a' -> b' -> c' -> d' -> IO e')
-> a -> b -> c -> d -> Z3 s e
liftF4 Context -> [Pattern] -> [Symbol] -> [Sort] -> AST -> IO AST
Base.mkForall

mkForallConst :: [Pattern s] -> [App s] -> AST s -> Z3 s (AST s)
mkForallConst :: [Pattern s] -> [App s] -> AST s -> Z3 s (AST s)
mkForallConst = (Context -> [Pattern] -> [App] -> AST -> IO AST)
-> [Pattern s] -> [App s] -> AST s -> Z3 s (AST s)
forall a' a b' b c' c d' d s.
(Coercible a' a, Coercible b' b, Coercible c' c, Coercible d' d) =>
(Context -> a' -> b' -> c' -> IO d') -> a -> b -> c -> Z3 s d
liftF3 Context -> [Pattern] -> [App] -> AST -> IO AST
Base.mkForallConst

mkExistsConst :: [Pattern s] -> [App s] -> AST s -> Z3 s (AST s)
mkExistsConst :: [Pattern s] -> [App s] -> AST s -> Z3 s (AST s)
mkExistsConst = (Context -> [Pattern] -> [App] -> AST -> IO AST)
-> [Pattern s] -> [App s] -> AST s -> Z3 s (AST s)
forall a' a b' b c' c d' d s.
(Coercible a' a, Coercible b' b, Coercible c' c, Coercible d' d) =>
(Context -> a' -> b' -> c' -> IO d') -> a -> b -> c -> Z3 s d
liftF3 Context -> [Pattern] -> [App] -> AST -> IO AST
Base.mkExistsConst

mkExists :: [Pattern s] -> [Symbol s] -> [Sort s] -> AST s -> Z3 s (AST s)
mkExists :: [Pattern s] -> [Symbol s] -> [Sort s] -> AST s -> Z3 s (AST s)
mkExists = (Context -> [Pattern] -> [Symbol] -> [Sort] -> AST -> IO AST)
-> [Pattern s] -> [Symbol s] -> [Sort s] -> AST s -> Z3 s (AST s)
forall a' a b' b c' c d' d e' e s.
(Coercible a' a, Coercible b' b, Coercible c' c, Coercible d' d,
 Coercible e' e) =>
(Context -> a' -> b' -> c' -> d' -> IO e')
-> a -> b -> c -> d -> Z3 s e
liftF4 Context -> [Pattern] -> [Symbol] -> [Sort] -> AST -> IO AST
Base.mkExists

---------------------------------------------------------------------
-- Accessors

-- | Return the symbol name.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#gaf1683d9464f377e5089ce6ebf2a9bd31>
getSymbolString :: Symbol s -> Z3 s String
getSymbolString :: Symbol s -> Z3 s String
getSymbolString = (Context -> Symbol -> IO String) -> Symbol s -> Z3 s String
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> Symbol -> IO String
Base.getSymbolString

-- | Return the sort kind.
--
-- Reference: <http://z3prover.github.io/api/html/group__capi.html#gacd85d48842c7bfaa696596d16875681a>
getSortKind :: Sort s -> Z3 s SortKind
getSortKind :: Sort s -> Z3 s SortKind
getSortKind = (Context -> Sort -> IO SortKind) -> Sort s -> Z3 s SortKind
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> Sort -> IO SortKind
Base.getSortKind

-- | Return the size of the given bit-vector sort.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga8fc3550edace7bc046e16d1f96ddb419>
getBvSortSize :: Sort s -> Z3 s Int
getBvSortSize :: Sort s -> Z3 s Int
getBvSortSize = (Context -> Sort -> IO Int) -> Sort s -> Z3 s Int
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> Sort -> IO Int
Base.getBvSortSize

-- | Get list of constructors for datatype.
getDatatypeSortConstructors :: Sort s           -- ^ Datatype sort.
                            -> Z3 s [FuncDecl s]  -- ^ (Constructor s) declarations.
getDatatypeSortConstructors :: Sort s -> Z3 s [FuncDecl s]
getDatatypeSortConstructors = (Context -> Sort -> IO [FuncDecl]) -> Sort s -> Z3 s [FuncDecl s]
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> Sort -> IO [FuncDecl]
Base.getDatatypeSortConstructors

-- | Get list of recognizers for datatype.
getDatatypeSortRecognizers :: Sort s           -- ^ Datatype sort.
                           -> Z3 s [FuncDecl s]  -- ^ (Constructor s) recognizers.
getDatatypeSortRecognizers :: Sort s -> Z3 s [FuncDecl s]
getDatatypeSortRecognizers = (Context -> Sort -> IO [FuncDecl]) -> Sort s -> Z3 s [FuncDecl s]
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> Sort -> IO [FuncDecl]
Base.getDatatypeSortRecognizers

-- | Get list of accessors for datatype.
getDatatypeSortConstructorAccessors :: Sort s              -- ^ Datatype sort.
                                    -> Z3 s [[FuncDecl s]] -- ^ (Constructor s) recognizers.
getDatatypeSortConstructorAccessors :: Sort s -> Z3 s [[FuncDecl s]]
getDatatypeSortConstructorAccessors = (Context -> Sort -> IO [[FuncDecl]])
-> Sort s -> Z3 s [[FuncDecl s]]
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> Sort -> IO [[FuncDecl]]
Base.getDatatypeSortConstructorAccessors

-- | Return the constant declaration name as a symbol.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga741b1bf11cb92aa2ec9ef2fef73ff129>
getDeclName :: FuncDecl s -> Z3 s (Symbol s)
getDeclName :: FuncDecl s -> Z3 s (Symbol s)
getDeclName = (Context -> FuncDecl -> IO Symbol) -> FuncDecl s -> Z3 s (Symbol s)
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> FuncDecl -> IO Symbol
Base.getDeclName

-- | Returns the number of parameters of the given declaration
getArity :: FuncDecl s -> Z3 s Int
getArity :: FuncDecl s -> Z3 s Int
getArity = (Context -> FuncDecl -> IO Int) -> FuncDecl s -> Z3 s Int
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> FuncDecl -> IO Int
Base.getArity

-- | Returns the sort of the i-th parameter of the given function declaration
getDomain :: FuncDecl s         -- ^ A function declaration
          -> Int              -- ^ i
          -> Z3 s (Sort s)
getDomain :: FuncDecl s -> Int -> Z3 s (Sort s)
getDomain = (Context -> FuncDecl -> Int -> IO Sort)
-> FuncDecl s -> Int -> Z3 s (Sort s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> FuncDecl -> Int -> IO Sort
Base.getDomain

-- | Returns the range of the given declaration.
getRange :: FuncDecl s -> Z3 s (Sort s)
getRange :: FuncDecl s -> Z3 s (Sort s)
getRange = (Context -> FuncDecl -> IO Sort) -> FuncDecl s -> Z3 s (Sort s)
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> FuncDecl -> IO Sort
Base.getRange

-- | Convert an app into (AST s). This is just type casting.
appToAst :: App s -> Z3 s (AST s)
appToAst :: App s -> Z3 s (AST s)
appToAst = (Context -> App -> IO AST) -> App s -> Z3 s (AST s)
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> App -> IO AST
Base.appToAst

-- | Return the declaration of a constant or function application.
getAppDecl :: App s -> Z3 s (FuncDecl s)
getAppDecl :: App s -> Z3 s (FuncDecl s)
getAppDecl = (Context -> App -> IO FuncDecl) -> App s -> Z3 s (FuncDecl s)
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> App -> IO FuncDecl
Base.getAppDecl

-- | Return the number of argument of an application. If t is an constant, then the number of arguments is 0.
getAppNumArgs :: App s -> Z3 s Int
getAppNumArgs :: App s -> Z3 s Int
getAppNumArgs = (Context -> App -> IO Int) -> App s -> Z3 s Int
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> App -> IO Int
Base.getAppNumArgs

-- | Return the i-th argument of the given application.
getAppArg :: App s -> Int -> Z3 s (AST s)
getAppArg :: App s -> Int -> Z3 s (AST s)
getAppArg = (Context -> App -> Int -> IO AST) -> App s -> Int -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> App -> Int -> IO AST
Base.getAppArg

-- | Return a list of all the arguments of the given application.
getAppArgs :: App s -> Z3 s [AST s]
getAppArgs :: App s -> Z3 s [AST s]
getAppArgs = (Context -> App -> IO [AST]) -> App s -> Z3 s [AST s]
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> App -> IO [AST]
Base.getAppArgs

-- | Return the sort of an (AST s) node.
getSort :: AST s -> Z3 s (Sort s)
getSort :: AST s -> Z3 s (Sort s)
getSort = (Context -> AST -> IO Sort) -> AST s -> Z3 s (Sort s)
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> AST -> IO Sort
Base.getSort

getArraySortDomain :: Sort s -> Z3 s (Sort s)
getArraySortDomain :: Sort s -> Z3 s (Sort s)
getArraySortDomain = (Context -> Sort -> IO Sort) -> Sort s -> Z3 s (Sort s)
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> Sort -> IO Sort
Base.getArraySortDomain

getArraySortRange :: Sort s -> Z3 s (Sort s)
getArraySortRange :: Sort s -> Z3 s (Sort s)
getArraySortRange = (Context -> Sort -> IO Sort) -> Sort s -> Z3 s (Sort s)
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> Sort -> IO Sort
Base.getArraySortRange

-- | Returns @Just True@, @Just False@, or @Nothing@ for /undefined/.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga133aaa1ec31af9b570ed7627a3c8c5a4>
getBoolValue :: AST s -> Z3 s (Maybe Bool)
getBoolValue :: AST s -> Z3 s (Maybe Bool)
getBoolValue = (Context -> AST -> IO (Maybe Bool)) -> AST s -> Z3 s (Maybe Bool)
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> AST -> IO (Maybe Bool)
Base.getBoolValue

-- | Return the kind of the given (AST s).
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga4c43608feea4cae363ef9c520c239a5c>
getAstKind :: AST s -> Z3 s ASTKind
getAstKind :: AST s -> Z3 s ASTKind
getAstKind = (Context -> AST -> IO ASTKind) -> AST s -> Z3 s ASTKind
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> AST -> IO ASTKind
Base.getAstKind

-- | Return True if an ast is APP_AST, False otherwise.
isApp :: AST s -> Z3 s Bool
isApp :: AST s -> Z3 s Bool
isApp = (Context -> AST -> IO Bool) -> AST s -> Z3 s Bool
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> AST -> IO Bool
Base.isApp

-- | Cast (AST s) into an (App s).
toApp :: AST s -> Z3 s (App s)
toApp :: AST s -> Z3 s (App s)
toApp = (Context -> AST -> IO App) -> AST s -> Z3 s (App s)
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> AST -> IO App
Base.toApp

-- | Return numeral value, as a string of a numeric constant term.
getNumeralString :: AST s -> Z3 s String
getNumeralString :: AST s -> Z3 s String
getNumeralString = (Context -> AST -> IO String) -> AST s -> Z3 s String
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> AST -> IO String
Base.getNumeralString

getIndexValue :: AST s -> Z3 s Int
getIndexValue :: AST s -> Z3 s Int
getIndexValue = (Context -> AST -> IO Int) -> AST s -> Z3 s Int
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> AST -> IO Int
Base.getIndexValue

isQuantifierForall :: AST s -> Z3 s Bool
isQuantifierForall :: AST s -> Z3 s Bool
isQuantifierForall = (Context -> AST -> IO Bool) -> AST s -> Z3 s Bool
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> AST -> IO Bool
Base.isQuantifierForall

isQuantifierExists :: AST s -> Z3 s Bool
isQuantifierExists :: AST s -> Z3 s Bool
isQuantifierExists = (Context -> AST -> IO Bool) -> AST s -> Z3 s Bool
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> AST -> IO Bool
Base.isQuantifierExists

getQuantifierWeight :: AST s -> Z3 s Int
getQuantifierWeight :: AST s -> Z3 s Int
getQuantifierWeight = (Context -> AST -> IO Int) -> AST s -> Z3 s Int
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> AST -> IO Int
Base.getQuantifierWeight

getQuantifierNumPatterns :: AST s -> Z3 s Int
getQuantifierNumPatterns :: AST s -> Z3 s Int
getQuantifierNumPatterns = (Context -> AST -> IO Int) -> AST s -> Z3 s Int
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> AST -> IO Int
Base.getQuantifierNumPatterns

getQuantifierPatternAST :: AST s -> Int -> Z3 s (AST s)
getQuantifierPatternAST :: AST s -> Int -> Z3 s (AST s)
getQuantifierPatternAST = (Context -> AST -> Int -> IO AST) -> AST s -> Int -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> Int -> IO AST
Base.getQuantifierPatternAST

getQuantifierPatterns :: AST s -> Z3 s [AST s]
getQuantifierPatterns :: AST s -> Z3 s [AST s]
getQuantifierPatterns = (Context -> AST -> IO [AST]) -> AST s -> Z3 s [AST s]
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> AST -> IO [AST]
Base.getQuantifierPatterns

getQuantifierNumNoPatterns :: AST s -> Z3 s Int
getQuantifierNumNoPatterns :: AST s -> Z3 s Int
getQuantifierNumNoPatterns = (Context -> AST -> IO Int) -> AST s -> Z3 s Int
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> AST -> IO Int
Base.getQuantifierNumNoPatterns

getQuantifierNoPatternAST :: AST s -> Int -> Z3 s (AST s)
getQuantifierNoPatternAST :: AST s -> Int -> Z3 s (AST s)
getQuantifierNoPatternAST = (Context -> AST -> Int -> IO AST) -> AST s -> Int -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> Int -> IO AST
Base.getQuantifierNoPatternAST

getQuantifierNoPatterns :: AST s -> Z3 s [AST s]
getQuantifierNoPatterns :: AST s -> Z3 s [AST s]
getQuantifierNoPatterns = (Context -> AST -> IO [AST]) -> AST s -> Z3 s [AST s]
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> AST -> IO [AST]
Base.getQuantifierNoPatterns

getQuantifierNumBound :: AST s -> Z3 s Int
getQuantifierNumBound :: AST s -> Z3 s Int
getQuantifierNumBound = (Context -> AST -> IO Int) -> AST s -> Z3 s Int
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> AST -> IO Int
Base.getQuantifierNumBound

getQuantifierBoundName :: AST s -> Int -> Z3 s (Symbol s)
getQuantifierBoundName :: AST s -> Int -> Z3 s (Symbol s)
getQuantifierBoundName = (Context -> AST -> Int -> IO Symbol)
-> AST s -> Int -> Z3 s (Symbol s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> Int -> IO Symbol
Base.getQuantifierBoundName

getQuantifierBoundSort :: AST s -> Int -> Z3 s (Sort s)
getQuantifierBoundSort :: AST s -> Int -> Z3 s (Sort s)
getQuantifierBoundSort = (Context -> AST -> Int -> IO Sort) -> AST s -> Int -> Z3 s (Sort s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> Int -> IO Sort
Base.getQuantifierBoundSort

getQuantifierBoundVars :: AST s -> Z3 s [AST s]
getQuantifierBoundVars :: AST s -> Z3 s [AST s]
getQuantifierBoundVars = (Context -> AST -> IO [AST]) -> AST s -> Z3 s [AST s]
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> AST -> IO [AST]
Base.getQuantifierBoundVars

getQuantifierBody :: AST s -> Z3 s (AST s)
getQuantifierBody :: AST s -> Z3 s (AST s)
getQuantifierBody = (Context -> AST -> IO AST) -> AST s -> Z3 s (AST s)
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> AST -> IO AST
Base.getQuantifierBody

-- | Simplify the expression.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#gada433553406475e5dd6a494ea957844c>
simplify :: AST s -> Z3 s (AST s)
simplify :: AST s -> Z3 s (AST s)
simplify = (Context -> AST -> IO AST) -> AST s -> Z3 s (AST s)
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> AST -> IO AST
Base.simplify

-- | Simplify the expression using the given parameters.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga34329d4c83ca8c98e18b2884b679008c>
simplifyEx :: AST s -> Params s -> Z3 s (AST s)
simplifyEx :: AST s -> Params s -> Z3 s (AST s)
simplifyEx = (Context -> AST -> Params -> IO AST)
-> AST s -> Params s -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> Params -> IO AST
Base.simplifyEx

-------------------------------------------------
-- ** Helpers

-- | Read a 'Bool' value from an '(AST s)'
getBool :: AST s -> Z3 s Bool
getBool :: AST s -> Z3 s Bool
getBool = (Context -> AST -> IO Bool) -> AST s -> Z3 s Bool
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> AST -> IO Bool
Base.getBool

-- | Return the integer value
getInt :: AST s -> Z3 s Integer
getInt :: AST s -> Z3 s Integer
getInt = (Context -> AST -> IO Integer) -> AST s -> Z3 s Integer
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> AST -> IO Integer
Base.getInt

-- | Return rational value
getReal :: AST s -> Z3 s Rational
getReal :: AST s -> Z3 s Rational
getReal = (Context -> AST -> IO Rational) -> AST s -> Z3 s Rational
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> AST -> IO Rational
Base.getReal

-- | Read the 'Integer' value from an '(AST s)' of sort /bit-vector/.
--
-- See 'mkBv2int'.
getBv :: AST s
                    -> Bool  -- ^ signed?
                    -> Z3 s Integer
getBv :: AST s -> Bool -> Z3 s Integer
getBv = (Context -> AST -> Bool -> IO Integer)
-> AST s -> Bool -> Z3 s Integer
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> Bool -> IO Integer
Base.getBv


---------------------------------------------------------------------
-- Modifiers

substituteVars :: AST s -> [AST s] -> Z3 s (AST s)
substituteVars :: AST s -> [AST s] -> Z3 s (AST s)
substituteVars = (Context -> AST -> [AST] -> IO AST)
-> AST s -> [AST s] -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> AST -> [AST] -> IO AST
Base.substituteVars

---------------------------------------------------------------------
-- Models

-- | Evaluate an (AST s) node in the given model.
--
-- The evaluation may fail for the following reasons:
--
--     * /t/ contains a quantifier.
--     * the model /m/ is partial.
--     * /t/ is type incorrect.
modelEval :: Model s -> AST s
             -> Bool  -- ^ (Model s) completion?
             -> Z3 s (Maybe (AST s))
modelEval :: Model s -> AST s -> Bool -> Z3 s (Maybe (AST s))
modelEval = (Context -> Model -> AST -> Bool -> IO (Maybe AST))
-> Model s -> AST s -> Bool -> Z3 s (Maybe (AST s))
forall a' a b' b c' c d' d s.
(Coercible a' a, Coercible b' b, Coercible c' c, Coercible d' d) =>
(Context -> a' -> b' -> c' -> IO d') -> a -> b -> c -> Z3 s d
liftF3 Context -> Model -> AST -> Bool -> IO (Maybe AST)
Base.modelEval

-- | Get array as a list of argument/value pairs, if it is
-- represented as a function (ie, using as-array).
evalArray :: Model s -> AST s -> Z3 s (Maybe FuncModel)
evalArray :: Model s -> AST s -> Z3 s (Maybe FuncModel)
evalArray = (Context -> Model -> AST -> IO (Maybe FuncModel))
-> Model s -> AST s -> Z3 s (Maybe FuncModel)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> Model -> AST -> IO (Maybe FuncModel)
Base.evalArray

getConstInterp :: Model s -> FuncDecl s -> Z3 s (Maybe (AST s))
getConstInterp :: Model s -> FuncDecl s -> Z3 s (Maybe (AST s))
getConstInterp = (Context -> Model -> FuncDecl -> IO (Maybe AST))
-> Model s -> FuncDecl s -> Z3 s (Maybe (AST s))
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> Model -> FuncDecl -> IO (Maybe AST)
Base.getConstInterp

-- | Return the interpretation of the function f in the model m.
-- Return NULL, if the model does not assign an interpretation for f.
-- That should be interpreted as: the f does not matter.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#gafb9cc5eca9564d8a849c154c5a4a8633>
getFuncInterp :: Model s -> FuncDecl s -> Z3 s (Maybe (FuncInterp s))
getFuncInterp :: Model s -> FuncDecl s -> Z3 s (Maybe (FuncInterp s))
getFuncInterp = (Context -> Model -> FuncDecl -> IO (Maybe FuncInterp))
-> Model s -> FuncDecl s -> Z3 s (Maybe (FuncInterp s))
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> Model -> FuncDecl -> IO (Maybe FuncInterp)
Base.getFuncInterp

hasInterp :: Model s -> FuncDecl s -> Z3 s Bool
hasInterp :: Model s -> FuncDecl s -> Z3 s Bool
hasInterp = (Context -> Model -> FuncDecl -> IO Bool)
-> Model s -> FuncDecl s -> Z3 s Bool
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> Model -> FuncDecl -> IO Bool
Base.hasInterp

numConsts :: Model s -> Z3 s Word
numConsts :: Model s -> Z3 s Word
numConsts = (Context -> Model -> IO Word) -> Model s -> Z3 s Word
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> Model -> IO Word
Base.numConsts

numFuncs :: Model s -> Z3 s Word
numFuncs :: Model s -> Z3 s Word
numFuncs = (Context -> Model -> IO Word) -> Model s -> Z3 s Word
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> Model -> IO Word
Base.numFuncs

getConstDecl :: Model s -> Word -> Z3 s (FuncDecl s)
getConstDecl :: Model s -> Word -> Z3 s (FuncDecl s)
getConstDecl = (Context -> Model -> Word -> IO FuncDecl)
-> Model s -> Word -> Z3 s (FuncDecl s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> Model -> Word -> IO FuncDecl
Base.getConstDecl

getFuncDecl :: Model s -> Word -> Z3 s (FuncDecl s)
getFuncDecl :: Model s -> Word -> Z3 s (FuncDecl s)
getFuncDecl = (Context -> Model -> Word -> IO FuncDecl)
-> Model s -> Word -> Z3 s (FuncDecl s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> Model -> Word -> IO FuncDecl
Base.getFuncDecl

getConsts :: Model s -> Z3 s [FuncDecl s]
getConsts :: Model s -> Z3 s [FuncDecl s]
getConsts = (Context -> Model -> IO [FuncDecl]) -> Model s -> Z3 s [FuncDecl s]
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> Model -> IO [FuncDecl]
Base.getConsts

getFuncs :: Model s -> Z3 s [FuncDecl s]
getFuncs :: Model s -> Z3 s [FuncDecl s]
getFuncs = (Context -> Model -> IO [FuncDecl]) -> Model s -> Z3 s [FuncDecl s]
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> Model -> IO [FuncDecl]
Base.getFuncs

-- | The (_ as-array f) (AST s) node is a construct for assigning interpretations
-- for arrays in Z3. It is the array such that forall indices i we have that
-- (select (_ as-array f) i) is equal to (f i). This procedure returns Z3_TRUE
-- if the a is an as-array (AST s) node.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga4674da67d226bfb16861829b9f129cfa>
isAsArray :: AST s -> Z3 s Bool
isAsArray :: AST s -> Z3 s Bool
isAsArray = (Context -> AST -> IO Bool) -> AST s -> Z3 s Bool
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> AST -> IO Bool
Base.isAsArray

addFuncInterp :: Model s -> FuncDecl s -> AST s -> Z3 s (FuncInterp s)
addFuncInterp :: Model s -> FuncDecl s -> AST s -> Z3 s (FuncInterp s)
addFuncInterp = (Context -> Model -> FuncDecl -> AST -> IO FuncInterp)
-> Model s -> FuncDecl s -> AST s -> Z3 s (FuncInterp s)
forall a' a b' b c' c d' d s.
(Coercible a' a, Coercible b' b, Coercible c' c, Coercible d' d) =>
(Context -> a' -> b' -> c' -> IO d') -> a -> b -> c -> Z3 s d
liftF3 Context -> Model -> FuncDecl -> AST -> IO FuncInterp
Base.addFuncInterp

addConstInterp :: Model s -> FuncDecl s -> AST s -> Z3 s ()
addConstInterp :: Model s -> FuncDecl s -> AST s -> Z3 s ()
addConstInterp = (Context -> Model -> FuncDecl -> AST -> IO ())
-> Model s -> FuncDecl s -> AST s -> Z3 s ()
forall a' a b' b c' c d' d s.
(Coercible a' a, Coercible b' b, Coercible c' c, Coercible d' d) =>
(Context -> a' -> b' -> c' -> IO d') -> a -> b -> c -> Z3 s d
liftF3 Context -> Model -> FuncDecl -> AST -> IO ()
Base.addConstInterp


-- | Return the function declaration f associated with a (_ as_array f) node.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga7d9262dc6e79f2aeb23fd4a383589dda>
getAsArrayFuncDecl :: AST s -> Z3 s (FuncDecl s)
getAsArrayFuncDecl :: AST s -> Z3 s (FuncDecl s)
getAsArrayFuncDecl = (Context -> AST -> IO FuncDecl) -> AST s -> Z3 s (FuncDecl s)
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> AST -> IO FuncDecl
Base.getAsArrayFuncDecl

-- | Return the number of entries in the given function interpretation.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga2bab9ae1444940e7593729beec279844>
funcInterpGetNumEntries :: FuncInterp s -> Z3 s Int
funcInterpGetNumEntries :: FuncInterp s -> Z3 s Int
funcInterpGetNumEntries = (Context -> FuncInterp -> IO Int) -> FuncInterp s -> Z3 s Int
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> FuncInterp -> IO Int
Base.funcInterpGetNumEntries

-- | Return a "point" of the given function intepretation.
-- It represents the value of f in a particular point.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#gaf157e1e1cd8c0cfe6a21be6370f659da>
funcInterpGetEntry :: FuncInterp s -> Int -> Z3 s (FuncEntry s)
funcInterpGetEntry :: FuncInterp s -> Int -> Z3 s (FuncEntry s)
funcInterpGetEntry = (Context -> FuncInterp -> Int -> IO FuncEntry)
-> FuncInterp s -> Int -> Z3 s (FuncEntry s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> FuncInterp -> Int -> IO FuncEntry
Base.funcInterpGetEntry

-- | Return the 'else' value of the given function interpretation.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga46de7559826ba71b8488d727cba1fb64>
funcInterpGetElse :: FuncInterp s -> Z3 s (AST s)
funcInterpGetElse :: FuncInterp s -> Z3 s (AST s)
funcInterpGetElse = (Context -> FuncInterp -> IO AST) -> FuncInterp s -> Z3 s (AST s)
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> FuncInterp -> IO AST
Base.funcInterpGetElse

-- | Return the arity (number of arguments) of the given function
-- interpretation.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#gaca22cbdb6f7787aaae5d814f2ab383d8>
funcInterpGetArity :: FuncInterp s -> Z3 s Int
funcInterpGetArity :: FuncInterp s -> Z3 s Int
funcInterpGetArity = (Context -> FuncInterp -> IO Int) -> FuncInterp s -> Z3 s Int
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> FuncInterp -> IO Int
Base.funcInterpGetArity

-- | Return the value of this point.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga9fd65e2ab039aa8e40608c2ecf7084da>
funcEntryGetValue :: FuncEntry s -> Z3 s (AST s)
funcEntryGetValue :: FuncEntry s -> Z3 s (AST s)
funcEntryGetValue = (Context -> FuncEntry -> IO AST) -> FuncEntry s -> Z3 s (AST s)
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> FuncEntry -> IO AST
Base.funcEntryGetValue

-- | Return the number of arguments in a Z3_func_entry object.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga51aed8c5bc4b1f53f0c371312de3ce1a>
funcEntryGetNumArgs :: FuncEntry s -> Z3 s Int
funcEntryGetNumArgs :: FuncEntry s -> Z3 s Int
funcEntryGetNumArgs = (Context -> FuncEntry -> IO Int) -> FuncEntry s -> Z3 s Int
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> FuncEntry -> IO Int
Base.funcEntryGetNumArgs

-- | Return an argument of a Z3_func_entry object.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga6fe03fe3c824fceb52766a4d8c2cbeab>
funcEntryGetArg :: FuncEntry s -> Int -> Z3 s (AST s)
funcEntryGetArg :: FuncEntry s -> Int -> Z3 s (AST s)
funcEntryGetArg = (Context -> FuncEntry -> Int -> IO AST)
-> FuncEntry s -> Int -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> FuncEntry -> Int -> IO AST
Base.funcEntryGetArg

-- | Convert the given model into a string.
modelToString :: Model s -> Z3 s String
modelToString :: Model s -> Z3 s String
modelToString = (Context -> Model -> IO String) -> Model s -> Z3 s String
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> Model -> IO String
Base.modelToString

-- | Alias for 'modelToString'.
showModel :: Model s -> Z3 s String
showModel :: Model s -> Z3 s String
showModel = Model s -> Z3 s String
forall s. Model s -> Z3 s String
modelToString

-------------------------------------------------
-- ** Helpers

-- | Type of an evaluation function for '(AST s)'.
--
-- Evaluation may fail (i.e. return 'Nothing') for a few
-- reasons, see 'modelEval'.
type EvalAst s a = Model s -> AST s -> Z3 s (Maybe a)

-- | An alias for 'modelEval' with model completion enabled.
eval :: EvalAst s (AST s)
eval :: EvalAst s (AST s)
eval = (Context -> Model -> AST -> IO (Maybe AST)) -> EvalAst s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> Model -> AST -> IO (Maybe AST)
Base.eval

-- | Evaluate an (AST s) node of sort /bool/ in the given model.
--
-- See 'modelEval' and 'getBool'.
evalBool :: EvalAst s Bool
evalBool :: EvalAst s Bool
evalBool = (Context -> Model -> AST -> IO (Maybe Bool)) -> EvalAst s Bool
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> Model -> AST -> IO (Maybe Bool)
Base.evalBool

-- | Evaluate an (AST s) node of sort /int/ in the given model.
--
-- See 'modelEval' and 'getInt'.
evalInt :: EvalAst s Integer
evalInt :: EvalAst s Integer
evalInt = (Context -> Model -> AST -> IO (Maybe Integer))
-> EvalAst s Integer
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> Model -> AST -> IO (Maybe Integer)
Base.evalInt

-- | Evaluate an (AST s) node of sort /real/ in the given model.
--
-- See 'modelEval' and 'getReal'.
evalReal :: EvalAst s Rational
evalReal :: EvalAst s Rational
evalReal = (Context -> Model -> AST -> IO (Maybe Rational))
-> EvalAst s Rational
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> Model -> AST -> IO (Maybe Rational)
Base.evalReal

-- | Evaluate an (AST s) node of sort /bit-vector/ in the given model.
--
-- The flag /signed/ decides whether the bit-vector value is
-- interpreted as a signed or unsigned integer.
--
-- See 'modelEval' and 'getBv'.
evalBv :: Bool -- ^ signed?
                     -> EvalAst s Integer
evalBv :: Bool -> EvalAst s Integer
evalBv = (Context -> Bool -> Model -> AST -> IO (Maybe Integer))
-> Bool -> EvalAst s Integer
forall a' a b' b c' c d' d s.
(Coercible a' a, Coercible b' b, Coercible c' c, Coercible d' d) =>
(Context -> a' -> b' -> c' -> IO d') -> a -> b -> c -> Z3 s d
liftF3 Context -> Bool -> Model -> AST -> IO (Maybe Integer)
Base.evalBv

-- | Evaluate a collection of (AST s) nodes in the given model.
evalT :: ∀ t s . (Traversable t) => Model s -> t (AST s) -> Z3 s (Maybe (t (AST s)))
evalT :: Model s -> t (AST s) -> Z3 s (Maybe (t (AST s)))
evalT model :: Model s
model asts :: t (AST s)
asts = ((Maybe (t AST) -> Maybe (t (AST s)))
-> ReaderT (Z3Env s) (ST s) (Maybe (t AST))
-> Z3 s (Maybe (t (AST s)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Maybe (t AST) -> Maybe (t (AST s)))
 -> ReaderT (Z3Env s) (ST s) (Maybe (t AST))
 -> Z3 s (Maybe (t (AST s))))
-> ((AST -> AST s) -> Maybe (t AST) -> Maybe (t (AST s)))
-> (AST -> AST s)
-> ReaderT (Z3Env s) (ST s) (Maybe (t AST))
-> Z3 s (Maybe (t (AST s)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (t AST -> t (AST s)) -> Maybe (t AST) -> Maybe (t (AST s))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((t AST -> t (AST s)) -> Maybe (t AST) -> Maybe (t (AST s)))
-> ((AST -> AST s) -> t AST -> t (AST s))
-> (AST -> AST s)
-> Maybe (t AST)
-> Maybe (t (AST s))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AST -> AST s) -> t AST -> t (AST s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) AST -> AST s
forall a b. Coercible a b => a -> b
coerce (ReaderT (Z3Env s) (ST s) (Maybe (t AST))
 -> Z3 s (Maybe (t (AST s))))
-> ((Z3Env s -> ST s (Maybe (t AST)))
    -> ReaderT (Z3Env s) (ST s) (Maybe (t AST)))
-> (Z3Env s -> ST s (Maybe (t AST)))
-> Z3 s (Maybe (t (AST s)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Z3Env s -> ST s (Maybe (t AST)))
-> ReaderT (Z3Env s) (ST s) (Maybe (t AST))
forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT ((Z3Env s -> ST s (Maybe (t AST))) -> Z3 s (Maybe (t (AST s))))
-> (Z3Env s -> ST s (Maybe (t AST))) -> Z3 s (Maybe (t (AST s)))
forall a b. (a -> b) -> a -> b
$ \ (Z3Env {..}) -> IO (Maybe (t AST)) -> ST s (Maybe (t AST))
forall a s. IO a -> ST s a
unsafeIOToST (IO (Maybe (t AST)) -> ST s (Maybe (t AST)))
-> IO (Maybe (t AST)) -> ST s (Maybe (t AST))
forall a b. (a -> b) -> a -> b
$ Context -> Model -> t AST -> IO (Maybe (t AST))
forall (t :: * -> *).
Traversable t =>
Context -> Model -> t AST -> IO (Maybe (t AST))
Base.evalT (Context s -> Context
forall a b. Coercible a b => a -> b
coerce Context s
context) (Model s -> Model
forall a b. Coercible a b => a -> b
coerce Model s
model) (AST s -> AST
forall a b. Coercible a b => a -> b
coerce (AST s -> AST) -> t (AST s) -> t AST
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t (AST s)
asts)

-- | Run a evaluation function on a 'Traversable' data structure of '(AST s)'s
-- (e.g. @[(AST s)]@, @Vector (AST s)@, @Maybe (AST s)@, etc).
--
-- This a generic version of 'evalT' which can be used in combination with
-- other helpers. For instance, @mapEval evalInt@ can be used to obtain
-- the 'Integer' interpretation of a list of '(AST s)' of sort /int/.
mapEval :: (Traversable t) => EvalAst s a
                           -> Model s
                           -> t (AST s)
                           -> Z3 s (Maybe (t a))
mapEval :: EvalAst s a -> Model s -> t (AST s) -> Z3 s (Maybe (t a))
mapEval f :: EvalAst s a
f m :: Model s
m = (t (Maybe a) -> Maybe (t a))
-> ReaderT (Z3Env s) (ST s) (t (Maybe a)) -> Z3 s (Maybe (t a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap t (Maybe a) -> Maybe (t a)
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
T.sequence (ReaderT (Z3Env s) (ST s) (t (Maybe a)) -> Z3 s (Maybe (t a)))
-> (t (AST s) -> ReaderT (Z3Env s) (ST s) (t (Maybe a)))
-> t (AST s)
-> Z3 s (Maybe (t a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AST s -> ReaderT (Z3Env s) (ST s) (Maybe a))
-> t (AST s) -> ReaderT (Z3Env s) (ST s) (t (Maybe a))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
T.mapM (EvalAst s a
f Model s
m)

-- | Get function as a list of argument/value pairs.
evalFunc :: Model s -> FuncDecl s -> Z3 s (Maybe FuncModel)
evalFunc :: Model s -> FuncDecl s -> Z3 s (Maybe FuncModel)
evalFunc = (Context -> Model -> FuncDecl -> IO (Maybe FuncModel))
-> Model s -> FuncDecl s -> Z3 s (Maybe FuncModel)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> Model -> FuncDecl -> IO (Maybe FuncModel)
Base.evalFunc

---------------------------------------------------------------------
-- Tactics

mkTactic :: String -> Z3 s (Tactic s)
mkTactic :: String -> Z3 s (Tactic s)
mkTactic = (Context -> String -> IO Tactic) -> String -> Z3 s (Tactic s)
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> String -> IO Tactic
Base.mkTactic

andThenTactic ::Tactic s ->Tactic s -> Z3 s (Tactic s)
andThenTactic :: Tactic s -> Tactic s -> Z3 s (Tactic s)
andThenTactic = (Context -> Tactic -> Tactic -> IO Tactic)
-> Tactic s -> Tactic s -> Z3 s (Tactic s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> Tactic -> Tactic -> IO Tactic
Base.andThenTactic

orElseTactic ::Tactic s ->Tactic s -> Z3 s (Tactic s)
orElseTactic :: Tactic s -> Tactic s -> Z3 s (Tactic s)
orElseTactic = (Context -> Tactic -> Tactic -> IO Tactic)
-> Tactic s -> Tactic s -> Z3 s (Tactic s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> Tactic -> Tactic -> IO Tactic
Base.andThenTactic

skipTactic :: Z3 s (Tactic s)
skipTactic :: Z3 s (Tactic s)
skipTactic = (Context -> IO Tactic) -> Z3 s (Tactic s)
forall a' a s. Coercible a' a => (Context -> IO a') -> Z3 s a
liftF0 Context -> IO Tactic
Base.skipTactic

tryForTactic ::Tactic s -> Int -> Z3 s (Tactic s)
tryForTactic :: Tactic s -> Int -> Z3 s (Tactic s)
tryForTactic = (Context -> Tactic -> Int -> IO Tactic)
-> Tactic s -> Int -> Z3 s (Tactic s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> Tactic -> Int -> IO Tactic
Base.tryForTactic

mkQuantifierEliminationTactic :: Z3 s (Tactic s)
mkQuantifierEliminationTactic :: Z3 s (Tactic s)
mkQuantifierEliminationTactic = (Context -> IO Tactic) -> Z3 s (Tactic s)
forall a' a s. Coercible a' a => (Context -> IO a') -> Z3 s a
liftF0 Context -> IO Tactic
Base.mkQuantifierEliminationTactic

mkAndInverterGraphTactic :: Z3 s (Tactic s)
mkAndInverterGraphTactic :: Z3 s (Tactic s)
mkAndInverterGraphTactic = (Context -> IO Tactic) -> Z3 s (Tactic s)
forall a' a s. Coercible a' a => (Context -> IO a') -> Z3 s a
liftF0 Context -> IO Tactic
Base.mkAndInverterGraphTactic

applyTactic ::Tactic s ->Goal s -> Z3 s( ApplyResult s)
applyTactic :: Tactic s -> Goal s -> Z3 s (ApplyResult s)
applyTactic = (Context -> Tactic -> Goal -> IO ApplyResult)
-> Tactic s -> Goal s -> Z3 s (ApplyResult s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> Tactic -> Goal -> IO ApplyResult
Base.applyTactic

getApplyResultNumSubgoals ::ApplyResult s -> Z3 s Int
getApplyResultNumSubgoals :: ApplyResult s -> Z3 s Int
getApplyResultNumSubgoals = (Context -> ApplyResult -> IO Int) -> ApplyResult s -> Z3 s Int
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> ApplyResult -> IO Int
Base.getApplyResultNumSubgoals

getApplyResultSubgoal ::ApplyResult s -> Int -> Z3 s (Goal s)
getApplyResultSubgoal :: ApplyResult s -> Int -> Z3 s (Goal s)
getApplyResultSubgoal = (Context -> ApplyResult -> Int -> IO Goal)
-> ApplyResult s -> Int -> Z3 s (Goal s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> ApplyResult -> Int -> IO Goal
Base.getApplyResultSubgoal

getApplyResultSubgoals ::ApplyResult s -> Z3 s [Goal s]
getApplyResultSubgoals :: ApplyResult s -> Z3 s [Goal s]
getApplyResultSubgoals = (Context -> ApplyResult -> IO [Goal])
-> ApplyResult s -> Z3 s [Goal s]
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> ApplyResult -> IO [Goal]
Base.getApplyResultSubgoals

mkGoal :: Bool -> Bool -> Bool -> Z3 s( Goal s)
mkGoal :: Bool -> Bool -> Bool -> Z3 s (Goal s)
mkGoal = (Context -> Bool -> Bool -> Bool -> IO Goal)
-> Bool -> Bool -> Bool -> Z3 s (Goal s)
forall a' a b' b c' c d' d s.
(Coercible a' a, Coercible b' b, Coercible c' c, Coercible d' d) =>
(Context -> a' -> b' -> c' -> IO d') -> a -> b -> c -> Z3 s d
liftF3 Context -> Bool -> Bool -> Bool -> IO Goal
Base.mkGoal

goalAssert ::Goal s -> AST s -> Z3 s ()
goalAssert :: Goal s -> AST s -> Z3 s ()
goalAssert = (Context -> Goal -> AST -> IO ()) -> Goal s -> AST s -> Z3 s ()
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> Goal -> AST -> IO ()
Base.goalAssert

getGoalSize ::Goal s -> Z3 s Int
getGoalSize :: Goal s -> Z3 s Int
getGoalSize = (Context -> Goal -> IO Int) -> Goal s -> Z3 s Int
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> Goal -> IO Int
Base.getGoalSize

getGoalFormula ::Goal s -> Int -> Z3 s (AST s)
getGoalFormula :: Goal s -> Int -> Z3 s (AST s)
getGoalFormula = (Context -> Goal -> Int -> IO AST) -> Goal s -> Int -> Z3 s (AST s)
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftF2 Context -> Goal -> Int -> IO AST
Base.getGoalFormula

getGoalFormulas ::Goal s -> Z3 s [AST s]
getGoalFormulas :: Goal s -> Z3 s [AST s]
getGoalFormulas = (Context -> Goal -> IO [AST]) -> Goal s -> Z3 s [AST s]
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> Goal -> IO [AST]
Base.getGoalFormulas

---------------------------------------------------------------------
-- String Conversion

-- | Set the mode for converting expressions to strings.
setASTPrintMode :: ASTPrintMode -> Z3 s ()
setASTPrintMode :: ASTPrintMode -> Z3 s ()
setASTPrintMode = (Context -> ASTPrintMode -> IO ()) -> ASTPrintMode -> Z3 s ()
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> ASTPrintMode -> IO ()
Base.setASTPrintMode

-- | Convert an (AST s) to a string.
astToString :: AST s -> Z3 s String
astToString :: AST s -> Z3 s String
astToString = (Context -> AST -> IO String) -> AST s -> Z3 s String
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> AST -> IO String
Base.astToString

-- | Convert a pattern to a string.
patternToString :: Pattern s -> Z3 s String
patternToString :: Pattern s -> Z3 s String
patternToString = (Context -> Pattern -> IO String) -> Pattern s -> Z3 s String
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> Pattern -> IO String
Base.patternToString

-- | Convert a sort to a string.
sortToString :: Sort s -> Z3 s String
sortToString :: Sort s -> Z3 s String
sortToString = (Context -> Sort -> IO String) -> Sort s -> Z3 s String
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> Sort -> IO String
Base.sortToString

-- | Convert a (FuncDecl s) to a string.
funcDeclToString :: FuncDecl s -> Z3 s String
funcDeclToString :: FuncDecl s -> Z3 s String
funcDeclToString = (Context -> FuncDecl -> IO String) -> FuncDecl s -> Z3 s String
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> a' -> IO b') -> a -> Z3 s b
liftF1 Context -> FuncDecl -> IO String
Base.funcDeclToString

-- | Convert the given benchmark into SMT-LIB formatted string.
--
-- The output format can be configured via 'setASTPrintMode'.
benchmarkToSMTLibString ::
                               String   -- ^ name
                            -> String   -- ^ logic
                            -> String   -- ^ status
                            -> String   -- ^ attributes
                            -> [AST s]    -- ^ assumptions1
                            -> AST s      -- ^ formula
                            -> Z3 s String
benchmarkToSMTLibString :: String
-> String -> String -> String -> [AST s] -> AST s -> Z3 s String
benchmarkToSMTLibString = (Context
 -> String
 -> String
 -> String
 -> String
 -> [AST]
 -> AST
 -> IO String)
-> String
-> String
-> String
-> String
-> [AST s]
-> AST s
-> Z3 s String
forall a' a b' b c' c d' d e' e f' f g' g s.
(Coercible a' a, Coercible b' b, Coercible c' c, Coercible d' d,
 Coercible e' e, Coercible f' f, Coercible g' g) =>
(Context -> a' -> b' -> c' -> d' -> e' -> f' -> IO g')
-> a -> b -> c -> d -> e -> f -> Z3 s g
liftF6 Context
-> String
-> String
-> String
-> String
-> [AST]
-> AST
-> IO String
Base.benchmarkToSMTLibString


---------------------------------------------------------------------
-- Parser interface

-- | Parse SMT expressions from a string
--
-- The sort and declaration arguments allow parsing in a context in which variables and functions have already been declared. They are almost never used.
parseSMTLib2String ::
                      String     -- ^ string to parse
                   -> [Symbol s]   -- ^ sort names
                   -> [Sort s]     -- ^ sorts
                   -> [Symbol s]   -- ^ declaration names
                   -> [FuncDecl s] -- ^ declarations
                   -> Z3 s (AST s)
parseSMTLib2String :: String
-> [Symbol s]
-> [Sort s]
-> [Symbol s]
-> [FuncDecl s]
-> Z3 s (AST s)
parseSMTLib2String = (Context
 -> String
 -> [Symbol]
 -> [Sort]
 -> [Symbol]
 -> [FuncDecl]
 -> IO AST)
-> String
-> [Symbol s]
-> [Sort s]
-> [Symbol s]
-> [FuncDecl s]
-> Z3 s (AST s)
forall a' a b' b c' c d' d e' e f' f s.
(Coercible a' a, Coercible b' b, Coercible c' c, Coercible d' d,
 Coercible e' e, Coercible f' f) =>
(Context -> a' -> b' -> c' -> d' -> e' -> IO f')
-> a -> b -> c -> d -> e -> Z3 s f
liftF5 Context
-> String -> [Symbol] -> [Sort] -> [Symbol] -> [FuncDecl] -> IO AST
Base.parseSMTLib2String

-- | Parse SMT expressions from a file
--
-- The sort and declaration arguments allow parsing in a context in which variables and functions have already been declared. They are almost never used.
parseSMTLib2File ::
                    String     -- ^ string to parse
                 -> [Symbol s]   -- ^ sort names
                 -> [Sort s]     -- ^ sorts
                 -> [Symbol s]   -- ^ declaration names
                 -> [FuncDecl s] -- ^ declarations
                 -> Z3 s (AST s)
parseSMTLib2File :: String
-> [Symbol s]
-> [Sort s]
-> [Symbol s]
-> [FuncDecl s]
-> Z3 s (AST s)
parseSMTLib2File = (Context
 -> String
 -> [Symbol]
 -> [Sort]
 -> [Symbol]
 -> [FuncDecl]
 -> IO AST)
-> String
-> [Symbol s]
-> [Sort s]
-> [Symbol s]
-> [FuncDecl s]
-> Z3 s (AST s)
forall a' a b' b c' c d' d e' e f' f s.
(Coercible a' a, Coercible b' b, Coercible c' c, Coercible d' d,
 Coercible e' e, Coercible f' f) =>
(Context -> a' -> b' -> c' -> d' -> e' -> IO f')
-> a -> b -> c -> d -> e -> Z3 s f
liftF5 Context
-> String -> [Symbol] -> [Sort] -> [Symbol] -> [FuncDecl] -> IO AST
Base.parseSMTLib2File

---------------------------------------------------------------------
-- Miscellaneous

-- | Return Z3 version number information.
getVersion :: Z3 s Version
getVersion :: Z3 s Version
getVersion = ST s Version -> Z3 s Version
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ST s Version -> Z3 s Version)
-> (IO Version -> ST s Version) -> IO Version -> Z3 s Version
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IO Version -> ST s Version
forall a s. IO a -> ST s a
unsafeIOToST (IO Version -> Z3 s Version) -> IO Version -> Z3 s Version
forall a b. (a -> b) -> a -> b
$ IO Version
Base.getVersion

---------------------------------------------------------------------
-- Fixedpoint

fixedpointPush :: Z3 s ()
fixedpointPush :: Z3 s ()
fixedpointPush = (Context -> Fixedpoint -> IO ()) -> Z3 s ()
forall a' a s.
Coercible a' a =>
(Context -> Fixedpoint -> IO a') -> Z3 s a
liftFixedpoint0 Context -> Fixedpoint -> IO ()
Base.fixedpointPush

fixedpointPop :: Z3 s ()
fixedpointPop :: Z3 s ()
fixedpointPop = (Context -> Fixedpoint -> IO ()) -> Z3 s ()
forall a' a s.
Coercible a' a =>
(Context -> Fixedpoint -> IO a') -> Z3 s a
liftFixedpoint0 Context -> Fixedpoint -> IO ()
Base.fixedpointPush

fixedpointAddRule :: AST s -> Symbol s -> Z3 s ()
fixedpointAddRule :: AST s -> Symbol s -> Z3 s ()
fixedpointAddRule = (Context -> Fixedpoint -> AST -> Symbol -> IO ())
-> AST s -> Symbol s -> Z3 s ()
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> Fixedpoint -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftFixedpoint2 Context -> Fixedpoint -> AST -> Symbol -> IO ()
Base.fixedpointAddRule

fixedpointSetParams :: Params s -> Z3 s ()
fixedpointSetParams :: Params s -> Z3 s ()
fixedpointSetParams = (Context -> Fixedpoint -> Params -> IO ()) -> Params s -> Z3 s ()
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> Fixedpoint -> a' -> IO b') -> a -> Z3 s b
liftFixedpoint1 Context -> Fixedpoint -> Params -> IO ()
Base.fixedpointSetParams

fixedpointRegisterRelation :: FuncDecl s -> Z3 s ()
fixedpointRegisterRelation :: FuncDecl s -> Z3 s ()
fixedpointRegisterRelation = (Context -> Fixedpoint -> FuncDecl -> IO ())
-> FuncDecl s -> Z3 s ()
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> Fixedpoint -> a' -> IO b') -> a -> Z3 s b
liftFixedpoint1 Context -> Fixedpoint -> FuncDecl -> IO ()
Base.fixedpointRegisterRelation

fixedpointQueryRelations :: [FuncDecl s] -> Z3 s Result
fixedpointQueryRelations :: [FuncDecl s] -> Z3 s Result
fixedpointQueryRelations = (Context -> Fixedpoint -> [FuncDecl] -> IO Result)
-> [FuncDecl s] -> Z3 s Result
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> Fixedpoint -> a' -> IO b') -> a -> Z3 s b
liftFixedpoint1 Context -> Fixedpoint -> [FuncDecl] -> IO Result
Base.fixedpointQueryRelations

fixedpointGetAnswer :: Z3 s (AST s)
fixedpointGetAnswer :: Z3 s (AST s)
fixedpointGetAnswer = (Context -> Fixedpoint -> IO AST) -> Z3 s (AST s)
forall a' a s.
Coercible a' a =>
(Context -> Fixedpoint -> IO a') -> Z3 s a
liftFixedpoint0 Context -> Fixedpoint -> IO AST
Base.fixedpointGetAnswer

fixedpointGetAssertions :: Z3 s [AST s]
fixedpointGetAssertions :: Z3 s [AST s]
fixedpointGetAssertions = (Context -> Fixedpoint -> IO [AST]) -> Z3 s [AST s]
forall a' a s.
Coercible a' a =>
(Context -> Fixedpoint -> IO a') -> Z3 s a
liftFixedpoint0 Context -> Fixedpoint -> IO [AST]
Base.fixedpointGetAssertions

---------------------------------------------------------------------
-- * Solvers

-- mkSolver :: Context s -> ST s (Solver s)
-- mkSolver = liftF0 z3_mk_solver

-- mkSimpleSolver :: Context s -> ST s (Solver s)
-- mkSimpleSolver = liftF0 z3_mk_simple_solver

-- mkSolverForLogic :: Context s -> Logic -> ST s (Solver s)
-- mkSolverForLogic c logic = withContextError c $ \cPtr ->
--   do sym <- mkStringSymbol c (show logic)
--      c2h c =<< z3_mk_solver_for_logic cPtr (unSymbol sym)

-- | Return a string describing all solver available parameters.
solverGetHelp :: Z3 s String
solverGetHelp :: Z3 s String
solverGetHelp = (Context -> Solver -> IO String) -> Z3 s String
forall a' a s.
Coercible a' a =>
(Context -> Solver -> IO a') -> Z3 s a
liftSolver0 Context -> Solver -> IO String
Base.solverGetHelp

-- | Set the solver using the given parameters.
solverSetParams :: Params s -> Z3 s ()
solverSetParams :: Params s -> Z3 s ()
solverSetParams = (Context -> Solver -> Params -> IO ()) -> Params s -> Z3 s ()
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> Solver -> a' -> IO b') -> a -> Z3 s b
liftSolver1 Context -> Solver -> Params -> IO ()
Base.solverSetParams

-- | Create a backtracking point.
solverPush :: Z3 s ()
solverPush :: Z3 s ()
solverPush = (Context -> Solver -> IO ()) -> Z3 s ()
forall a' a s.
Coercible a' a =>
(Context -> Solver -> IO a') -> Z3 s a
liftSolver0 Context -> Solver -> IO ()
Base.solverPush

-- | Backtrack /n/ backtracking points.
solverPop :: Int -> Z3 s ()
solverPop :: Int -> Z3 s ()
solverPop = (Context -> Solver -> Int -> IO ()) -> Int -> Z3 s ()
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> Solver -> a' -> IO b') -> a -> Z3 s b
liftSolver1 Context -> Solver -> Int -> IO ()
Base.solverPop

solverReset :: Z3 s ()
solverReset :: Z3 s ()
solverReset = (Context -> Solver -> IO ()) -> Z3 s ()
forall a' a s.
Coercible a' a =>
(Context -> Solver -> IO a') -> Z3 s a
liftSolver0 Context -> Solver -> IO ()
Base.solverReset

-- | Number of backtracking points.
solverGetNumScopes :: Z3 s Int
solverGetNumScopes :: Z3 s Int
solverGetNumScopes = (Context -> Solver -> IO Int) -> Z3 s Int
forall a' a s.
Coercible a' a =>
(Context -> Solver -> IO a') -> Z3 s a
liftSolver0 Context -> Solver -> IO Int
Base.solverGetNumScopes

-- | Assert a constraing into the logical context.
--
-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#ga1a05ff73a564ae7256a2257048a4680a>
solverAssertCnstr :: AST s -> Z3 s ()
solverAssertCnstr :: AST s -> Z3 s ()
solverAssertCnstr = (Context -> Solver -> AST -> IO ()) -> AST s -> Z3 s ()
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> Solver -> a' -> IO b') -> a -> Z3 s b
liftSolver1 Context -> Solver -> AST -> IO ()
Base.solverAssertCnstr

-- | Assert a constraint a into the solver, and track it
-- (in the unsat) core using the Boolean constant /p/.
--
-- This API is an alternative to Z3_solver_check_assumptions
-- for extracting unsat cores. Both APIs can be used in the same
-- solver. The unsat core will contain a combination of the Boolean
-- variables provided using Z3_solver_assert_and_track and the
-- Boolean literals provided using Z3_solver_check_assumptions.
solverAssertAndTrack :: AST s -> AST s -> Z3 s ()
solverAssertAndTrack :: AST s -> AST s -> Z3 s ()
solverAssertAndTrack = (Context -> Solver -> AST -> AST -> IO ())
-> AST s -> AST s -> Z3 s ()
forall a' a b' b c' c s.
(Coercible a' a, Coercible b' b, Coercible c' c) =>
(Context -> Solver -> a' -> b' -> IO c') -> a -> b -> Z3 s c
liftSolver2 Context -> Solver -> AST -> AST -> IO ()
Base.solverAssertAndTrack

-- | Check whether the assertions in a given solver are consistent or not.
solverCheck :: Z3 s Result
solverCheck :: Z3 s Result
solverCheck = (Context -> Solver -> IO Result) -> Z3 s Result
forall a' a s.
Coercible a' a =>
(Context -> Solver -> IO a') -> Z3 s a
liftSolver0 Context -> Solver -> IO Result
Base.solverCheck

-- | Check whether the assertions in the given solver and optional assumptions are consistent or not.
solverCheckAssumptions :: [AST s] -> Z3 s Result
solverCheckAssumptions :: [AST s] -> Z3 s Result
solverCheckAssumptions = (Context -> Solver -> [AST] -> IO Result) -> [AST s] -> Z3 s Result
forall a' a b' b s.
(Coercible a' a, Coercible b' b) =>
(Context -> Solver -> a' -> IO b') -> a -> Z3 s b
liftSolver1 Context -> Solver -> [AST] -> IO Result
Base.solverCheckAssumptions

-- | Retrieve the model for the last 'solverCheck'.
--
-- The error handler is invoked if a model is not available because
-- the commands above were not invoked for the given solver,
-- or if the result was 'Unsat'.
solverGetModel :: Z3 s (Model s)
solverGetModel :: Z3 s (Model s)
solverGetModel = (Context -> Solver -> IO Model) -> Z3 s (Model s)
forall a' a s.
Coercible a' a =>
(Context -> Solver -> IO a') -> Z3 s a
liftSolver0 Context -> Solver -> IO Model
Base.solverGetModel

-- | Retrieve the unsat core for the last 'solverCheckAssumptions'; the unsat core is a subset of the assumptions
solverGetUnsatCore :: Z3 s [AST s]
solverGetUnsatCore :: Z3 s [AST s]
solverGetUnsatCore = (Context -> Solver -> IO [AST]) -> Z3 s [AST s]
forall a' a s.
Coercible a' a =>
(Context -> Solver -> IO a') -> Z3 s a
liftSolver0 Context -> Solver -> IO [AST]
Base.solverGetUnsatCore

-- | Return a brief justification for an 'Unknown' result for the commands 'solverCheck' and 'solverCheckAssumptions'.
solverGetReasonUnknown :: Z3 s String
solverGetReasonUnknown :: Z3 s String
solverGetReasonUnknown = (Context -> Solver -> IO String) -> Z3 s String
forall a' a s.
Coercible a' a =>
(Context -> Solver -> IO a') -> Z3 s a
liftSolver0 Context -> Solver -> IO String
Base.solverGetReasonUnknown

-- | Convert the given solver into a string.
solverToString :: Z3 s String
solverToString :: Z3 s String
solverToString = (Context -> Solver -> IO String) -> Z3 s String
forall a' a s.
Coercible a' a =>
(Context -> Solver -> IO a') -> Z3 s a
liftSolver0 Context -> Solver -> IO String
Base.solverToString

-------------------------------------------------
-- ** Helpers

-- | Create a backtracking point.
--
-- For @push; m; pop 1@ see 'local'.
push :: Z3 s ()
push :: Z3 s ()
push = Z3 s ()
forall s. Z3 s ()
solverPush

-- | Backtrack /n/ backtracking points.
--
-- Contrary to 'solverPop' this funtion checks whether /n/ is within
-- the size of the solver scope stack.
pop :: Int -> Z3 s ()
pop :: Int -> Z3 s ()
pop n :: Int
n = do
  Int
scopes <- Z3 s Int
forall s. Z3 s Int
solverGetNumScopes
  if Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
scopes
    then Int -> Z3 s ()
forall s. Int -> Z3 s ()
solverPop Int
n
    else String -> Z3 s ()
forall a. HasCallStack => String -> a
error "Z3.Monad.safePop: too many scopes to backtrack"

-- | Run a query and restore the initial logical context.
--
-- This is a shorthand for 'push', run the query, and 'pop'.
local :: Z3 s a -> Z3 s a
local :: Z3 s a -> Z3 s a
local q :: Z3 s a
q = Z3 s ()
forall s. Z3 s ()
push Z3 s () -> Z3 s a -> Z3 s a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Z3 s a
q Z3 s a -> Z3 s () -> Z3 s a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Int -> Z3 s ()
forall s. Int -> Z3 s ()
pop 1

-- | Backtrack all the way.
reset :: Z3 s ()
reset :: Z3 s ()
reset = Z3 s ()
forall s. Z3 s ()
solverReset

-- | Get number of backtracking points.
getNumScopes :: Z3 s Int
getNumScopes :: Z3 s Int
getNumScopes = (Context -> Solver -> IO Int) -> Z3 s Int
forall a' a s.
Coercible a' a =>
(Context -> Solver -> IO a') -> Z3 s a
liftSolver0 Context -> Solver -> IO Int
Base.solverGetNumScopes

assert :: AST s -> Z3 s ()
assert :: AST s -> Z3 s ()
assert = AST s -> Z3 s ()
forall s. AST s -> Z3 s ()
solverAssertCnstr

-- | Check whether the given logical context is consistent or not.
check :: Z3 s Result
check :: Z3 s Result
check = Z3 s Result
forall s. Z3 s Result
solverCheck

-- | Check whether the assertions in the given solver and optional assumptions are consistent or not.
checkAssumptions :: [AST s] -> Z3 s Result
checkAssumptions :: [AST s] -> Z3 s Result
checkAssumptions = [AST s] -> Z3 s Result
forall s. [AST s] -> Z3 s Result
solverCheckAssumptions

solverCheckAndGetModel :: Z3 s (Result, Maybe (Model s))
solverCheckAndGetModel :: Z3 s (Result, Maybe (Model s))
solverCheckAndGetModel = (Context -> Solver -> IO (Result, Maybe Model))
-> Z3 s (Result, Maybe (Model s))
forall a' a s.
Coercible a' a =>
(Context -> Solver -> IO a') -> Z3 s a
liftSolver0 Context -> Solver -> IO (Result, Maybe Model)
Base.solverCheckAndGetModel

solverCheckAssumptionsAndGetModel :: [AST s] -> Z3 s (Maybe (Either [AST s] (Model s)))
solverCheckAssumptionsAndGetModel :: [AST s] -> Z3 s (Maybe (Either [AST s] (Model s)))
solverCheckAssumptionsAndGetModel = [AST s] -> Z3 s Result
forall s. [AST s] -> Z3 s Result
checkAssumptions ([AST s] -> Z3 s Result)
-> (Result -> Z3 s (Maybe (Either [AST s] (Model s))))
-> [AST s]
-> Z3 s (Maybe (Either [AST s] (Model s)))
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> \ case
    Undef -> Maybe (Either [AST s] (Model s))
-> Z3 s (Maybe (Either [AST s] (Model s)))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Either [AST s] (Model s))
forall a. Maybe a
Nothing
    Unsat -> Either [AST s] (Model s) -> Maybe (Either [AST s] (Model s))
forall a. a -> Maybe a
Just (Either [AST s] (Model s) -> Maybe (Either [AST s] (Model s)))
-> ([AST s] -> Either [AST s] (Model s))
-> [AST s]
-> Maybe (Either [AST s] (Model s))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [AST s] -> Either [AST s] (Model s)
forall a b. a -> Either a b
Left  ([AST s] -> Maybe (Either [AST s] (Model s)))
-> ReaderT (Z3Env s) (ST s) [AST s]
-> Z3 s (Maybe (Either [AST s] (Model s)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT (Z3Env s) (ST s) [AST s]
forall s. Z3 s [AST s]
getUnsatCore
    Sat   -> Either [AST s] (Model s) -> Maybe (Either [AST s] (Model s))
forall a. a -> Maybe a
Just (Either [AST s] (Model s) -> Maybe (Either [AST s] (Model s)))
-> (Model s -> Either [AST s] (Model s))
-> Model s
-> Maybe (Either [AST s] (Model s))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Model s -> Either [AST s] (Model s)
forall a b. b -> Either a b
Right (Model s -> Maybe (Either [AST s] (Model s)))
-> ReaderT (Z3Env s) (ST s) (Model s)
-> Z3 s (Maybe (Either [AST s] (Model s)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT (Z3Env s) (ST s) (Model s)
forall s. Z3 s (Model s)
solverGetModel

-- | Get model.
--
-- Reference : <http://research.microsoft.com/en-us/um/redmond/projects/Z3 s/group__capi.html#gaff310fef80ac8a82d0a51417e073ec0a>
getModel :: Z3 s (Result, Maybe (Model s))
getModel :: Z3 s (Result, Maybe (Model s))
getModel = Z3 s (Result, Maybe (Model s))
forall s. Z3 s (Result, Maybe (Model s))
solverCheckAndGetModel

-- | Check satisfiability and, if /sat/, compute a value from the given model.
--
-- E.g.
-- @
-- withModel $ \\m ->
--   fromJust \<$\> evalInt m x
-- @
withModel :: (Model s -> Z3 s a) -> Z3 s (Result, Maybe a)
withModel :: (Model s -> Z3 s a) -> Z3 s (Result, Maybe a)
withModel f :: Model s -> Z3 s a
f = do
  (r :: Result
r,mb_m :: Maybe (Model s)
mb_m) <- Z3 s (Result, Maybe (Model s))
forall s. Z3 s (Result, Maybe (Model s))
getModel
  Maybe a
mb_e <- (Model s -> Z3 s a)
-> Maybe (Model s) -> ReaderT (Z3Env s) (ST s) (Maybe a)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
T.traverse Model s -> Z3 s a
f Maybe (Model s)
mb_m
  (Result, Maybe a) -> Z3 s (Result, Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Result
r, Maybe a
mb_e)

-- | Retrieve the unsat core for the last 'checkAssumptions'; the unsat core is a subset of the assumptions.
getUnsatCore :: Z3 s [AST s]
getUnsatCore :: Z3 s [AST s]
getUnsatCore = Z3 s [AST s]
forall s. Z3 s [AST s]
solverGetUnsatCore

newtype Config      s = Config      { Config s -> Config
_unConfig      :: Base.Config      } deriving (Config s -> Config s -> Bool
(Config s -> Config s -> Bool)
-> (Config s -> Config s -> Bool) -> Eq (Config s)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k (s :: k). Config s -> Config s -> Bool
/= :: Config s -> Config s -> Bool
$c/= :: forall k (s :: k). Config s -> Config s -> Bool
== :: Config s -> Config s -> Bool
$c== :: forall k (s :: k). Config s -> Config s -> Bool
Eq)
newtype Context     s = Context     { Context s -> Context
_unContext     :: Base.Context     } deriving (Context s -> Context s -> Bool
(Context s -> Context s -> Bool)
-> (Context s -> Context s -> Bool) -> Eq (Context s)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k (s :: k). Context s -> Context s -> Bool
/= :: Context s -> Context s -> Bool
$c/= :: forall k (s :: k). Context s -> Context s -> Bool
== :: Context s -> Context s -> Bool
$c== :: forall k (s :: k). Context s -> Context s -> Bool
Eq)
newtype Symbol      s = Symbol      { Symbol s -> Symbol
_unSymbol      :: Base.Symbol      } deriving (Symbol s -> Symbol s -> Bool
(Symbol s -> Symbol s -> Bool)
-> (Symbol s -> Symbol s -> Bool) -> Eq (Symbol s)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k (s :: k). Symbol s -> Symbol s -> Bool
/= :: Symbol s -> Symbol s -> Bool
$c/= :: forall k (s :: k). Symbol s -> Symbol s -> Bool
== :: Symbol s -> Symbol s -> Bool
$c== :: forall k (s :: k). Symbol s -> Symbol s -> Bool
Eq, Eq (Symbol s)
Eq (Symbol s) =>
(Symbol s -> Symbol s -> Ordering)
-> (Symbol s -> Symbol s -> Bool)
-> (Symbol s -> Symbol s -> Bool)
-> (Symbol s -> Symbol s -> Bool)
-> (Symbol s -> Symbol s -> Bool)
-> (Symbol s -> Symbol s -> Symbol s)
-> (Symbol s -> Symbol s -> Symbol s)
-> Ord (Symbol s)
Symbol s -> Symbol s -> Bool
Symbol s -> Symbol s -> Ordering
Symbol s -> Symbol s -> Symbol s
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall k (s :: k). Eq (Symbol s)
forall k (s :: k). Symbol s -> Symbol s -> Bool
forall k (s :: k). Symbol s -> Symbol s -> Ordering
forall k (s :: k). Symbol s -> Symbol s -> Symbol s
min :: Symbol s -> Symbol s -> Symbol s
$cmin :: forall k (s :: k). Symbol s -> Symbol s -> Symbol s
max :: Symbol s -> Symbol s -> Symbol s
$cmax :: forall k (s :: k). Symbol s -> Symbol s -> Symbol s
>= :: Symbol s -> Symbol s -> Bool
$c>= :: forall k (s :: k). Symbol s -> Symbol s -> Bool
> :: Symbol s -> Symbol s -> Bool
$c> :: forall k (s :: k). Symbol s -> Symbol s -> Bool
<= :: Symbol s -> Symbol s -> Bool
$c<= :: forall k (s :: k). Symbol s -> Symbol s -> Bool
< :: Symbol s -> Symbol s -> Bool
$c< :: forall k (s :: k). Symbol s -> Symbol s -> Bool
compare :: Symbol s -> Symbol s -> Ordering
$ccompare :: forall k (s :: k). Symbol s -> Symbol s -> Ordering
$cp1Ord :: forall k (s :: k). Eq (Symbol s)
Ord, Int -> Symbol s -> ShowS
[Symbol s] -> ShowS
Symbol s -> String
(Int -> Symbol s -> ShowS)
-> (Symbol s -> String) -> ([Symbol s] -> ShowS) -> Show (Symbol s)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (s :: k). Int -> Symbol s -> ShowS
forall k (s :: k). [Symbol s] -> ShowS
forall k (s :: k). Symbol s -> String
showList :: [Symbol s] -> ShowS
$cshowList :: forall k (s :: k). [Symbol s] -> ShowS
show :: Symbol s -> String
$cshow :: forall k (s :: k). Symbol s -> String
showsPrec :: Int -> Symbol s -> ShowS
$cshowsPrec :: forall k (s :: k). Int -> Symbol s -> ShowS
Show, Ptr b -> Int -> IO (Symbol s)
Ptr b -> Int -> Symbol s -> IO ()
Ptr (Symbol s) -> IO (Symbol s)
Ptr (Symbol s) -> Int -> IO (Symbol s)
Ptr (Symbol s) -> Int -> Symbol s -> IO ()
Ptr (Symbol s) -> Symbol s -> IO ()
Symbol s -> Int
(Symbol s -> Int)
-> (Symbol s -> Int)
-> (Ptr (Symbol s) -> Int -> IO (Symbol s))
-> (Ptr (Symbol s) -> Int -> Symbol s -> IO ())
-> (forall b. Ptr b -> Int -> IO (Symbol s))
-> (forall b. Ptr b -> Int -> Symbol s -> IO ())
-> (Ptr (Symbol s) -> IO (Symbol s))
-> (Ptr (Symbol s) -> Symbol s -> IO ())
-> Storable (Symbol s)
forall b. Ptr b -> Int -> IO (Symbol s)
forall b. Ptr b -> Int -> Symbol s -> IO ()
forall a.
(a -> Int)
-> (a -> Int)
-> (Ptr a -> Int -> IO a)
-> (Ptr a -> Int -> a -> IO ())
-> (forall b. Ptr b -> Int -> IO a)
-> (forall b. Ptr b -> Int -> a -> IO ())
-> (Ptr a -> IO a)
-> (Ptr a -> a -> IO ())
-> Storable a
forall k (s :: k). Ptr (Symbol s) -> IO (Symbol s)
forall k (s :: k). Ptr (Symbol s) -> Int -> IO (Symbol s)
forall k (s :: k). Ptr (Symbol s) -> Int -> Symbol s -> IO ()
forall k (s :: k). Ptr (Symbol s) -> Symbol s -> IO ()
forall k (s :: k). Symbol s -> Int
forall k (s :: k) b. Ptr b -> Int -> IO (Symbol s)
forall k (s :: k) b. Ptr b -> Int -> Symbol s -> IO ()
poke :: Ptr (Symbol s) -> Symbol s -> IO ()
$cpoke :: forall k (s :: k). Ptr (Symbol s) -> Symbol s -> IO ()
peek :: Ptr (Symbol s) -> IO (Symbol s)
$cpeek :: forall k (s :: k). Ptr (Symbol s) -> IO (Symbol s)
pokeByteOff :: Ptr b -> Int -> Symbol s -> IO ()
$cpokeByteOff :: forall k (s :: k) b. Ptr b -> Int -> Symbol s -> IO ()
peekByteOff :: Ptr b -> Int -> IO (Symbol s)
$cpeekByteOff :: forall k (s :: k) b. Ptr b -> Int -> IO (Symbol s)
pokeElemOff :: Ptr (Symbol s) -> Int -> Symbol s -> IO ()
$cpokeElemOff :: forall k (s :: k). Ptr (Symbol s) -> Int -> Symbol s -> IO ()
peekElemOff :: Ptr (Symbol s) -> Int -> IO (Symbol s)
$cpeekElemOff :: forall k (s :: k). Ptr (Symbol s) -> Int -> IO (Symbol s)
alignment :: Symbol s -> Int
$calignment :: forall k (s :: k). Symbol s -> Int
sizeOf :: Symbol s -> Int
$csizeOf :: forall k (s :: k). Symbol s -> Int
Storable)
newtype AST         s = AST         { AST s -> AST
_unAST         :: Base.AST         } deriving (AST s -> AST s -> Bool
(AST s -> AST s -> Bool) -> (AST s -> AST s -> Bool) -> Eq (AST s)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k (s :: k). AST s -> AST s -> Bool
/= :: AST s -> AST s -> Bool
$c/= :: forall k (s :: k). AST s -> AST s -> Bool
== :: AST s -> AST s -> Bool
$c== :: forall k (s :: k). AST s -> AST s -> Bool
Eq, Eq (AST s)
Eq (AST s) =>
(AST s -> AST s -> Ordering)
-> (AST s -> AST s -> Bool)
-> (AST s -> AST s -> Bool)
-> (AST s -> AST s -> Bool)
-> (AST s -> AST s -> Bool)
-> (AST s -> AST s -> AST s)
-> (AST s -> AST s -> AST s)
-> Ord (AST s)
AST s -> AST s -> Bool
AST s -> AST s -> Ordering
AST s -> AST s -> AST s
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall k (s :: k). Eq (AST s)
forall k (s :: k). AST s -> AST s -> Bool
forall k (s :: k). AST s -> AST s -> Ordering
forall k (s :: k). AST s -> AST s -> AST s
min :: AST s -> AST s -> AST s
$cmin :: forall k (s :: k). AST s -> AST s -> AST s
max :: AST s -> AST s -> AST s
$cmax :: forall k (s :: k). AST s -> AST s -> AST s
>= :: AST s -> AST s -> Bool
$c>= :: forall k (s :: k). AST s -> AST s -> Bool
> :: AST s -> AST s -> Bool
$c> :: forall k (s :: k). AST s -> AST s -> Bool
<= :: AST s -> AST s -> Bool
$c<= :: forall k (s :: k). AST s -> AST s -> Bool
< :: AST s -> AST s -> Bool
$c< :: forall k (s :: k). AST s -> AST s -> Bool
compare :: AST s -> AST s -> Ordering
$ccompare :: forall k (s :: k). AST s -> AST s -> Ordering
$cp1Ord :: forall k (s :: k). Eq (AST s)
Ord, Int -> AST s -> ShowS
[AST s] -> ShowS
AST s -> String
(Int -> AST s -> ShowS)
-> (AST s -> String) -> ([AST s] -> ShowS) -> Show (AST s)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (s :: k). Int -> AST s -> ShowS
forall k (s :: k). [AST s] -> ShowS
forall k (s :: k). AST s -> String
showList :: [AST s] -> ShowS
$cshowList :: forall k (s :: k). [AST s] -> ShowS
show :: AST s -> String
$cshow :: forall k (s :: k). AST s -> String
showsPrec :: Int -> AST s -> ShowS
$cshowsPrec :: forall k (s :: k). Int -> AST s -> ShowS
Show)
newtype Sort        s = Sort        { Sort s -> Sort
_unSort        :: Base.Sort        } deriving (Sort s -> Sort s -> Bool
(Sort s -> Sort s -> Bool)
-> (Sort s -> Sort s -> Bool) -> Eq (Sort s)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k (s :: k). Sort s -> Sort s -> Bool
/= :: Sort s -> Sort s -> Bool
$c/= :: forall k (s :: k). Sort s -> Sort s -> Bool
== :: Sort s -> Sort s -> Bool
$c== :: forall k (s :: k). Sort s -> Sort s -> Bool
Eq, Eq (Sort s)
Eq (Sort s) =>
(Sort s -> Sort s -> Ordering)
-> (Sort s -> Sort s -> Bool)
-> (Sort s -> Sort s -> Bool)
-> (Sort s -> Sort s -> Bool)
-> (Sort s -> Sort s -> Bool)
-> (Sort s -> Sort s -> Sort s)
-> (Sort s -> Sort s -> Sort s)
-> Ord (Sort s)
Sort s -> Sort s -> Bool
Sort s -> Sort s -> Ordering
Sort s -> Sort s -> Sort s
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall k (s :: k). Eq (Sort s)
forall k (s :: k). Sort s -> Sort s -> Bool
forall k (s :: k). Sort s -> Sort s -> Ordering
forall k (s :: k). Sort s -> Sort s -> Sort s
min :: Sort s -> Sort s -> Sort s
$cmin :: forall k (s :: k). Sort s -> Sort s -> Sort s
max :: Sort s -> Sort s -> Sort s
$cmax :: forall k (s :: k). Sort s -> Sort s -> Sort s
>= :: Sort s -> Sort s -> Bool
$c>= :: forall k (s :: k). Sort s -> Sort s -> Bool
> :: Sort s -> Sort s -> Bool
$c> :: forall k (s :: k). Sort s -> Sort s -> Bool
<= :: Sort s -> Sort s -> Bool
$c<= :: forall k (s :: k). Sort s -> Sort s -> Bool
< :: Sort s -> Sort s -> Bool
$c< :: forall k (s :: k). Sort s -> Sort s -> Bool
compare :: Sort s -> Sort s -> Ordering
$ccompare :: forall k (s :: k). Sort s -> Sort s -> Ordering
$cp1Ord :: forall k (s :: k). Eq (Sort s)
Ord, Int -> Sort s -> ShowS
[Sort s] -> ShowS
Sort s -> String
(Int -> Sort s -> ShowS)
-> (Sort s -> String) -> ([Sort s] -> ShowS) -> Show (Sort s)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (s :: k). Int -> Sort s -> ShowS
forall k (s :: k). [Sort s] -> ShowS
forall k (s :: k). Sort s -> String
showList :: [Sort s] -> ShowS
$cshowList :: forall k (s :: k). [Sort s] -> ShowS
show :: Sort s -> String
$cshow :: forall k (s :: k). Sort s -> String
showsPrec :: Int -> Sort s -> ShowS
$cshowsPrec :: forall k (s :: k). Int -> Sort s -> ShowS
Show)
newtype FuncDecl    s = FuncDecl    { FuncDecl s -> FuncDecl
_unFuncDecl    :: Base.FuncDecl    } deriving (FuncDecl s -> FuncDecl s -> Bool
(FuncDecl s -> FuncDecl s -> Bool)
-> (FuncDecl s -> FuncDecl s -> Bool) -> Eq (FuncDecl s)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k (s :: k). FuncDecl s -> FuncDecl s -> Bool
/= :: FuncDecl s -> FuncDecl s -> Bool
$c/= :: forall k (s :: k). FuncDecl s -> FuncDecl s -> Bool
== :: FuncDecl s -> FuncDecl s -> Bool
$c== :: forall k (s :: k). FuncDecl s -> FuncDecl s -> Bool
Eq, Eq (FuncDecl s)
Eq (FuncDecl s) =>
(FuncDecl s -> FuncDecl s -> Ordering)
-> (FuncDecl s -> FuncDecl s -> Bool)
-> (FuncDecl s -> FuncDecl s -> Bool)
-> (FuncDecl s -> FuncDecl s -> Bool)
-> (FuncDecl s -> FuncDecl s -> Bool)
-> (FuncDecl s -> FuncDecl s -> FuncDecl s)
-> (FuncDecl s -> FuncDecl s -> FuncDecl s)
-> Ord (FuncDecl s)
FuncDecl s -> FuncDecl s -> Bool
FuncDecl s -> FuncDecl s -> Ordering
FuncDecl s -> FuncDecl s -> FuncDecl s
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall k (s :: k). Eq (FuncDecl s)
forall k (s :: k). FuncDecl s -> FuncDecl s -> Bool
forall k (s :: k). FuncDecl s -> FuncDecl s -> Ordering
forall k (s :: k). FuncDecl s -> FuncDecl s -> FuncDecl s
min :: FuncDecl s -> FuncDecl s -> FuncDecl s
$cmin :: forall k (s :: k). FuncDecl s -> FuncDecl s -> FuncDecl s
max :: FuncDecl s -> FuncDecl s -> FuncDecl s
$cmax :: forall k (s :: k). FuncDecl s -> FuncDecl s -> FuncDecl s
>= :: FuncDecl s -> FuncDecl s -> Bool
$c>= :: forall k (s :: k). FuncDecl s -> FuncDecl s -> Bool
> :: FuncDecl s -> FuncDecl s -> Bool
$c> :: forall k (s :: k). FuncDecl s -> FuncDecl s -> Bool
<= :: FuncDecl s -> FuncDecl s -> Bool
$c<= :: forall k (s :: k). FuncDecl s -> FuncDecl s -> Bool
< :: FuncDecl s -> FuncDecl s -> Bool
$c< :: forall k (s :: k). FuncDecl s -> FuncDecl s -> Bool
compare :: FuncDecl s -> FuncDecl s -> Ordering
$ccompare :: forall k (s :: k). FuncDecl s -> FuncDecl s -> Ordering
$cp1Ord :: forall k (s :: k). Eq (FuncDecl s)
Ord, Int -> FuncDecl s -> ShowS
[FuncDecl s] -> ShowS
FuncDecl s -> String
(Int -> FuncDecl s -> ShowS)
-> (FuncDecl s -> String)
-> ([FuncDecl s] -> ShowS)
-> Show (FuncDecl s)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (s :: k). Int -> FuncDecl s -> ShowS
forall k (s :: k). [FuncDecl s] -> ShowS
forall k (s :: k). FuncDecl s -> String
showList :: [FuncDecl s] -> ShowS
$cshowList :: forall k (s :: k). [FuncDecl s] -> ShowS
show :: FuncDecl s -> String
$cshow :: forall k (s :: k). FuncDecl s -> String
showsPrec :: Int -> FuncDecl s -> ShowS
$cshowsPrec :: forall k (s :: k). Int -> FuncDecl s -> ShowS
Show)
newtype App         s = App         { App s -> App
_unApp         :: Base.App         } deriving (App s -> App s -> Bool
(App s -> App s -> Bool) -> (App s -> App s -> Bool) -> Eq (App s)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k (s :: k). App s -> App s -> Bool
/= :: App s -> App s -> Bool
$c/= :: forall k (s :: k). App s -> App s -> Bool
== :: App s -> App s -> Bool
$c== :: forall k (s :: k). App s -> App s -> Bool
Eq, Eq (App s)
Eq (App s) =>
(App s -> App s -> Ordering)
-> (App s -> App s -> Bool)
-> (App s -> App s -> Bool)
-> (App s -> App s -> Bool)
-> (App s -> App s -> Bool)
-> (App s -> App s -> App s)
-> (App s -> App s -> App s)
-> Ord (App s)
App s -> App s -> Bool
App s -> App s -> Ordering
App s -> App s -> App s
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall k (s :: k). Eq (App s)
forall k (s :: k). App s -> App s -> Bool
forall k (s :: k). App s -> App s -> Ordering
forall k (s :: k). App s -> App s -> App s
min :: App s -> App s -> App s
$cmin :: forall k (s :: k). App s -> App s -> App s
max :: App s -> App s -> App s
$cmax :: forall k (s :: k). App s -> App s -> App s
>= :: App s -> App s -> Bool
$c>= :: forall k (s :: k). App s -> App s -> Bool
> :: App s -> App s -> Bool
$c> :: forall k (s :: k). App s -> App s -> Bool
<= :: App s -> App s -> Bool
$c<= :: forall k (s :: k). App s -> App s -> Bool
< :: App s -> App s -> Bool
$c< :: forall k (s :: k). App s -> App s -> Bool
compare :: App s -> App s -> Ordering
$ccompare :: forall k (s :: k). App s -> App s -> Ordering
$cp1Ord :: forall k (s :: k). Eq (App s)
Ord, Int -> App s -> ShowS
[App s] -> ShowS
App s -> String
(Int -> App s -> ShowS)
-> (App s -> String) -> ([App s] -> ShowS) -> Show (App s)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (s :: k). Int -> App s -> ShowS
forall k (s :: k). [App s] -> ShowS
forall k (s :: k). App s -> String
showList :: [App s] -> ShowS
$cshowList :: forall k (s :: k). [App s] -> ShowS
show :: App s -> String
$cshow :: forall k (s :: k). App s -> String
showsPrec :: Int -> App s -> ShowS
$cshowsPrec :: forall k (s :: k). Int -> App s -> ShowS
Show)
newtype Pattern     s = Pattern     { Pattern s -> Pattern
_unPattern     :: Base.Pattern     } deriving (Pattern s -> Pattern s -> Bool
(Pattern s -> Pattern s -> Bool)
-> (Pattern s -> Pattern s -> Bool) -> Eq (Pattern s)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k (s :: k). Pattern s -> Pattern s -> Bool
/= :: Pattern s -> Pattern s -> Bool
$c/= :: forall k (s :: k). Pattern s -> Pattern s -> Bool
== :: Pattern s -> Pattern s -> Bool
$c== :: forall k (s :: k). Pattern s -> Pattern s -> Bool
Eq, Eq (Pattern s)
Eq (Pattern s) =>
(Pattern s -> Pattern s -> Ordering)
-> (Pattern s -> Pattern s -> Bool)
-> (Pattern s -> Pattern s -> Bool)
-> (Pattern s -> Pattern s -> Bool)
-> (Pattern s -> Pattern s -> Bool)
-> (Pattern s -> Pattern s -> Pattern s)
-> (Pattern s -> Pattern s -> Pattern s)
-> Ord (Pattern s)
Pattern s -> Pattern s -> Bool
Pattern s -> Pattern s -> Ordering
Pattern s -> Pattern s -> Pattern s
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall k (s :: k). Eq (Pattern s)
forall k (s :: k). Pattern s -> Pattern s -> Bool
forall k (s :: k). Pattern s -> Pattern s -> Ordering
forall k (s :: k). Pattern s -> Pattern s -> Pattern s
min :: Pattern s -> Pattern s -> Pattern s
$cmin :: forall k (s :: k). Pattern s -> Pattern s -> Pattern s
max :: Pattern s -> Pattern s -> Pattern s
$cmax :: forall k (s :: k). Pattern s -> Pattern s -> Pattern s
>= :: Pattern s -> Pattern s -> Bool
$c>= :: forall k (s :: k). Pattern s -> Pattern s -> Bool
> :: Pattern s -> Pattern s -> Bool
$c> :: forall k (s :: k). Pattern s -> Pattern s -> Bool
<= :: Pattern s -> Pattern s -> Bool
$c<= :: forall k (s :: k). Pattern s -> Pattern s -> Bool
< :: Pattern s -> Pattern s -> Bool
$c< :: forall k (s :: k). Pattern s -> Pattern s -> Bool
compare :: Pattern s -> Pattern s -> Ordering
$ccompare :: forall k (s :: k). Pattern s -> Pattern s -> Ordering
$cp1Ord :: forall k (s :: k). Eq (Pattern s)
Ord, Int -> Pattern s -> ShowS
[Pattern s] -> ShowS
Pattern s -> String
(Int -> Pattern s -> ShowS)
-> (Pattern s -> String)
-> ([Pattern s] -> ShowS)
-> Show (Pattern s)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (s :: k). Int -> Pattern s -> ShowS
forall k (s :: k). [Pattern s] -> ShowS
forall k (s :: k). Pattern s -> String
showList :: [Pattern s] -> ShowS
$cshowList :: forall k (s :: k). [Pattern s] -> ShowS
show :: Pattern s -> String
$cshow :: forall k (s :: k). Pattern s -> String
showsPrec :: Int -> Pattern s -> ShowS
$cshowsPrec :: forall k (s :: k). Int -> Pattern s -> ShowS
Show)
newtype Constructor s = Constructor { Constructor s -> Constructor
_unConstructor :: Base.Constructor } deriving (Constructor s -> Constructor s -> Bool
(Constructor s -> Constructor s -> Bool)
-> (Constructor s -> Constructor s -> Bool) -> Eq (Constructor s)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k (s :: k). Constructor s -> Constructor s -> Bool
/= :: Constructor s -> Constructor s -> Bool
$c/= :: forall k (s :: k). Constructor s -> Constructor s -> Bool
== :: Constructor s -> Constructor s -> Bool
$c== :: forall k (s :: k). Constructor s -> Constructor s -> Bool
Eq, Eq (Constructor s)
Eq (Constructor s) =>
(Constructor s -> Constructor s -> Ordering)
-> (Constructor s -> Constructor s -> Bool)
-> (Constructor s -> Constructor s -> Bool)
-> (Constructor s -> Constructor s -> Bool)
-> (Constructor s -> Constructor s -> Bool)
-> (Constructor s -> Constructor s -> Constructor s)
-> (Constructor s -> Constructor s -> Constructor s)
-> Ord (Constructor s)
Constructor s -> Constructor s -> Bool
Constructor s -> Constructor s -> Ordering
Constructor s -> Constructor s -> Constructor s
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall k (s :: k). Eq (Constructor s)
forall k (s :: k). Constructor s -> Constructor s -> Bool
forall k (s :: k). Constructor s -> Constructor s -> Ordering
forall k (s :: k). Constructor s -> Constructor s -> Constructor s
min :: Constructor s -> Constructor s -> Constructor s
$cmin :: forall k (s :: k). Constructor s -> Constructor s -> Constructor s
max :: Constructor s -> Constructor s -> Constructor s
$cmax :: forall k (s :: k). Constructor s -> Constructor s -> Constructor s
>= :: Constructor s -> Constructor s -> Bool
$c>= :: forall k (s :: k). Constructor s -> Constructor s -> Bool
> :: Constructor s -> Constructor s -> Bool
$c> :: forall k (s :: k). Constructor s -> Constructor s -> Bool
<= :: Constructor s -> Constructor s -> Bool
$c<= :: forall k (s :: k). Constructor s -> Constructor s -> Bool
< :: Constructor s -> Constructor s -> Bool
$c< :: forall k (s :: k). Constructor s -> Constructor s -> Bool
compare :: Constructor s -> Constructor s -> Ordering
$ccompare :: forall k (s :: k). Constructor s -> Constructor s -> Ordering
$cp1Ord :: forall k (s :: k). Eq (Constructor s)
Ord, Int -> Constructor s -> ShowS
[Constructor s] -> ShowS
Constructor s -> String
(Int -> Constructor s -> ShowS)
-> (Constructor s -> String)
-> ([Constructor s] -> ShowS)
-> Show (Constructor s)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (s :: k). Int -> Constructor s -> ShowS
forall k (s :: k). [Constructor s] -> ShowS
forall k (s :: k). Constructor s -> String
showList :: [Constructor s] -> ShowS
$cshowList :: forall k (s :: k). [Constructor s] -> ShowS
show :: Constructor s -> String
$cshow :: forall k (s :: k). Constructor s -> String
showsPrec :: Int -> Constructor s -> ShowS
$cshowsPrec :: forall k (s :: k). Int -> Constructor s -> ShowS
Show)
newtype Model       s = Model       { Model s -> Model
_unModel       :: Base.Model       } deriving (Model s -> Model s -> Bool
(Model s -> Model s -> Bool)
-> (Model s -> Model s -> Bool) -> Eq (Model s)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k (s :: k). Model s -> Model s -> Bool
/= :: Model s -> Model s -> Bool
$c/= :: forall k (s :: k). Model s -> Model s -> Bool
== :: Model s -> Model s -> Bool
$c== :: forall k (s :: k). Model s -> Model s -> Bool
Eq)
newtype FuncInterp  s = FuncInterp  { FuncInterp s -> FuncInterp
_unFuncInterp  :: Base.FuncInterp  } deriving (FuncInterp s -> FuncInterp s -> Bool
(FuncInterp s -> FuncInterp s -> Bool)
-> (FuncInterp s -> FuncInterp s -> Bool) -> Eq (FuncInterp s)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k (s :: k). FuncInterp s -> FuncInterp s -> Bool
/= :: FuncInterp s -> FuncInterp s -> Bool
$c/= :: forall k (s :: k). FuncInterp s -> FuncInterp s -> Bool
== :: FuncInterp s -> FuncInterp s -> Bool
$c== :: forall k (s :: k). FuncInterp s -> FuncInterp s -> Bool
Eq)
newtype FuncEntry   s = FuncEntry   { FuncEntry s -> FuncEntry
_unFuncEntry   :: Base.FuncEntry   } deriving (FuncEntry s -> FuncEntry s -> Bool
(FuncEntry s -> FuncEntry s -> Bool)
-> (FuncEntry s -> FuncEntry s -> Bool) -> Eq (FuncEntry s)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k (s :: k). FuncEntry s -> FuncEntry s -> Bool
/= :: FuncEntry s -> FuncEntry s -> Bool
$c/= :: forall k (s :: k). FuncEntry s -> FuncEntry s -> Bool
== :: FuncEntry s -> FuncEntry s -> Bool
$c== :: forall k (s :: k). FuncEntry s -> FuncEntry s -> Bool
Eq)
newtype Tactic      s = Tactic      { Tactic s -> Tactic
_unTactic      :: Base.Tactic      } deriving (Tactic s -> Tactic s -> Bool
(Tactic s -> Tactic s -> Bool)
-> (Tactic s -> Tactic s -> Bool) -> Eq (Tactic s)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k (s :: k). Tactic s -> Tactic s -> Bool
/= :: Tactic s -> Tactic s -> Bool
$c/= :: forall k (s :: k). Tactic s -> Tactic s -> Bool
== :: Tactic s -> Tactic s -> Bool
$c== :: forall k (s :: k). Tactic s -> Tactic s -> Bool
Eq)
newtype Goal        s = Goal        { Goal s -> Goal
_unGoal        :: Base.Goal        } deriving (Goal s -> Goal s -> Bool
(Goal s -> Goal s -> Bool)
-> (Goal s -> Goal s -> Bool) -> Eq (Goal s)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k (s :: k). Goal s -> Goal s -> Bool
/= :: Goal s -> Goal s -> Bool
$c/= :: forall k (s :: k). Goal s -> Goal s -> Bool
== :: Goal s -> Goal s -> Bool
$c== :: forall k (s :: k). Goal s -> Goal s -> Bool
Eq)
newtype ApplyResult s = ApplyResult { ApplyResult s -> ApplyResult
_unApplyResult :: Base.ApplyResult } deriving (ApplyResult s -> ApplyResult s -> Bool
(ApplyResult s -> ApplyResult s -> Bool)
-> (ApplyResult s -> ApplyResult s -> Bool) -> Eq (ApplyResult s)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k (s :: k). ApplyResult s -> ApplyResult s -> Bool
/= :: ApplyResult s -> ApplyResult s -> Bool
$c/= :: forall k (s :: k). ApplyResult s -> ApplyResult s -> Bool
== :: ApplyResult s -> ApplyResult s -> Bool
$c== :: forall k (s :: k). ApplyResult s -> ApplyResult s -> Bool
Eq)
newtype Params      s = Params      { Params s -> Params
_unParams      :: Base.Params      } deriving (Params s -> Params s -> Bool
(Params s -> Params s -> Bool)
-> (Params s -> Params s -> Bool) -> Eq (Params s)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k (s :: k). Params s -> Params s -> Bool
/= :: Params s -> Params s -> Bool
$c/= :: forall k (s :: k). Params s -> Params s -> Bool
== :: Params s -> Params s -> Bool
$c== :: forall k (s :: k). Params s -> Params s -> Bool
Eq)
newtype Solver      s = Solver      { Solver s -> Solver
_unSolver      :: Base.Solver      } deriving (Solver s -> Solver s -> Bool
(Solver s -> Solver s -> Bool)
-> (Solver s -> Solver s -> Bool) -> Eq (Solver s)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k (s :: k). Solver s -> Solver s -> Bool
/= :: Solver s -> Solver s -> Bool
$c/= :: forall k (s :: k). Solver s -> Solver s -> Bool
== :: Solver s -> Solver s -> Bool
$c== :: forall k (s :: k). Solver s -> Solver s -> Bool
Eq)
newtype Fixedpoint  s = Fixedpoint  { Fixedpoint s -> Fixedpoint
_unFixedpoint  :: Base.Fixedpoint  } deriving (Fixedpoint s -> Fixedpoint s -> Bool
(Fixedpoint s -> Fixedpoint s -> Bool)
-> (Fixedpoint s -> Fixedpoint s -> Bool) -> Eq (Fixedpoint s)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k (s :: k). Fixedpoint s -> Fixedpoint s -> Bool
/= :: Fixedpoint s -> Fixedpoint s -> Bool
$c/= :: forall k (s :: k). Fixedpoint s -> Fixedpoint s -> Bool
== :: Fixedpoint s -> Fixedpoint s -> Bool
$c== :: forall k (s :: k). Fixedpoint s -> Fixedpoint s -> Bool
Eq)