Language.REST.SMT

Documentation

type Z3Model = Map String String

parens :: Stream s m Char => ParsecT s u m a -> ParsecT s u m a

parseFunDef :: Stream s m Char => ParsecT s u m (String, String)

modelParser :: Stream s m Char => ParsecT s u m Z3Model

readModel :: Handle -> IO String

parseModel :: String -> Z3Model

newtype SMTVar a

Constructors

SMTVar Text

Instances

Eq (SMTVar a)

Defined in Language.REST.SMT

Methods

(==) :: SMTVar a -> SMTVar a -> Bool

(/=) :: SMTVar a -> SMTVar a -> Bool

Ord (SMTVar a)

Defined in Language.REST.SMT

Methods

compare :: SMTVar a -> SMTVar a -> Ordering

(<) :: SMTVar a -> SMTVar a -> Bool

(<=) :: SMTVar a -> SMTVar a -> Bool

(>) :: SMTVar a -> SMTVar a -> Bool

(>=) :: SMTVar a -> SMTVar a -> Bool

max :: SMTVar a -> SMTVar a -> SMTVar a

min :: SMTVar a -> SMTVar a -> SMTVar a

data SMTExpr a where

Constructors

And :: [SMTExpr Bool] -> SMTExpr Bool

Add :: [SMTExpr Int] -> SMTExpr Int

Or :: [SMTExpr Bool] -> SMTExpr Bool

Equal :: [SMTExpr a] -> SMTExpr Bool

Greater :: SMTExpr Int -> SMTExpr Int -> SMTExpr Bool

GTE :: SMTExpr Int -> SMTExpr Int -> SMTExpr Bool

Implies :: SMTExpr Bool -> SMTExpr Bool -> SMTExpr Bool

Var :: SMTVar a -> SMTExpr a

Const :: Int -> SMTExpr Int

Instances

Eq (SMTExpr a)

Defined in Language.REST.SMT

Methods

(==) :: SMTExpr a -> SMTExpr a -> Bool

(/=) :: SMTExpr a -> SMTExpr a -> Bool

Ord (SMTExpr a)

Defined in Language.REST.SMT

Methods

compare :: SMTExpr a -> SMTExpr a -> Ordering

(<) :: SMTExpr a -> SMTExpr a -> Bool

(<=) :: SMTExpr a -> SMTExpr a -> Bool

(>) :: SMTExpr a -> SMTExpr a -> Bool

(>=) :: SMTExpr a -> SMTExpr a -> Bool

max :: SMTExpr a -> SMTExpr a -> SMTExpr a

min :: SMTExpr a -> SMTExpr a -> SMTExpr a

Show (SMTExpr a)

Defined in Language.REST.SMT

Methods

showsPrec :: Int -> SMTExpr a -> ShowS

show :: SMTExpr a -> String

showList :: [SMTExpr a] -> ShowS

Hashable (SMTExpr a)

Defined in Language.REST.SMT

Methods

hashWithSalt :: Int -> SMTExpr a -> Int

hash :: SMTExpr a -> Int

data UntypedExpr

Constructors

UAnd [UntypedExpr]

UAdd [UntypedExpr]

UOr [UntypedExpr]

UEqual [UntypedExpr]

UGreater UntypedExpr UntypedExpr

UGTE UntypedExpr UntypedExpr

UImplies UntypedExpr UntypedExpr

UVar Text

UConst Int

Instances

Eq UntypedExpr

Defined in Language.REST.SMT

Methods

(==) :: UntypedExpr -> UntypedExpr -> Bool

(/=) :: UntypedExpr -> UntypedExpr -> Bool

Ord UntypedExpr

Defined in Language.REST.SMT

Methods

compare :: UntypedExpr -> UntypedExpr -> Ordering

(<) :: UntypedExpr -> UntypedExpr -> Bool

(<=) :: UntypedExpr -> UntypedExpr -> Bool

(>) :: UntypedExpr -> UntypedExpr -> Bool

(>=) :: UntypedExpr -> UntypedExpr -> Bool

max :: UntypedExpr -> UntypedExpr -> UntypedExpr

min :: UntypedExpr -> UntypedExpr -> UntypedExpr

Show UntypedExpr

Defined in Language.REST.SMT

Methods

showsPrec :: Int -> UntypedExpr -> ShowS

show :: UntypedExpr -> String

showList :: [UntypedExpr] -> ShowS

Generic UntypedExpr

Defined in Language.REST.SMT

Associated Types

type Rep UntypedExpr :: Type -> Type

Methods

from :: UntypedExpr -> Rep UntypedExpr x

to :: Rep UntypedExpr x -> UntypedExpr

Hashable UntypedExpr

Defined in Language.REST.SMT

Methods

hashWithSalt :: Int -> UntypedExpr -> Int

hash :: UntypedExpr -> Int

type Rep UntypedExpr

Defined in Language.REST.SMT

type Rep UntypedExpr = D1 ('MetaData "UntypedExpr" "Language.REST.SMT" "rest-rewrite-0.3.0-C58P8WPn3kHJiQCBn16Zwt" 'False) (((C1 ('MetaCons "UAnd" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [UntypedExpr])) :+: C1 ('MetaCons "UAdd" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [UntypedExpr]))) :+: (C1 ('MetaCons "UOr" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [UntypedExpr])) :+: C1 ('MetaCons "UEqual" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [UntypedExpr])))) :+: ((C1 ('MetaCons "UGreater" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UntypedExpr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UntypedExpr)) :+: C1 ('MetaCons "UGTE" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UntypedExpr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UntypedExpr))) :+: (C1 ('MetaCons "UImplies" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UntypedExpr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UntypedExpr)) :+: (C1 ('MetaCons "UVar" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text)) :+: C1 ('MetaCons "UConst" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int))))))

toUntyped :: SMTExpr a -> UntypedExpr

toFormula :: SMTExpr a -> Text

vars :: SMTExpr a -> Set Text

data SMTCommand

Constructors

SMTAssert (SMTExpr Bool)

DeclareVar Text

CheckSat

Push

Pop

smtFalse :: SMTExpr Bool

smtTrue :: SMTExpr Bool

smtAdd :: [SMTExpr Int] -> SMTExpr Int

smtAnd :: SMTExpr Bool -> SMTExpr Bool -> SMTExpr Bool

smtGTE :: SMTExpr Int -> SMTExpr Int -> SMTExpr Bool

app :: Text -> [SMTExpr a] -> Text

exprString :: SMTExpr a -> Text

commandString :: SMTCommand -> Text

askCmds :: SMTExpr Bool -> [SMTCommand]

type SolverHandle = (Handle, Handle)

spawnZ3 :: IO (Handle, Handle)

killZ3 :: (Handle, b) -> IO ()

withZ3 :: MonadIO m => ((Handle, Handle) -> m b) -> m b

getModel :: Handle -> IO ()

checkSat' :: (Handle, Handle) -> SMTExpr Bool -> IO Bool

checkSat :: SMTExpr Bool -> IO Bool

class ToSMTVar a b | a -> b where

Methods

toSMTVar :: a -> SMTVar b

Instances

ToSMTVar Op Int

Defined in Language.REST.Op

Methods

toSMTVar :: Op -> SMTVar Int

class ToSMT a b where

Methods

toSMT :: a -> SMTExpr b

Instances

ToSMT Int Int

Defined in Language.REST.SMT

Methods

toSMT :: Int -> SMTExpr Int

ToSMTVar a b => ToSMT a b

Defined in Language.REST.SMT

Methods

toSMT :: a -> SMTExpr b

ToSMTVar a Int => ToSMT (WQO a) Bool

Defined in Language.REST.Internal.WQO

Methods

toSMT :: WQO a -> SMTExpr Bool

ToSMTVar a Int => ToSMT (ConstraintsADT a) Bool

Defined in Language.REST.WQOConstraints.ADT

Methods

toSMT :: ConstraintsADT a -> SMTExpr Bool