Safe Haskell	Safe-Inferred
Language	Haskell2010

Language.REST.SMT

Documentation

type Z3Model = Map String String Source #

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

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

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

readModel :: Handle -> IO String Source #

parseModel :: String -> Z3Model Source #

newtype SMTVar a Source #

Constructors

SMTVar Text

Instances

Instances details

Eq (SMTVar a) Source #
Instance details Defined in Language.REST.SMT Methods (==) :: SMTVar a -> SMTVar a -> Bool # (/=) :: SMTVar a -> SMTVar a -> Bool #
Ord (SMTVar a) Source #
Instance details 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 Source #

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

Instances details

Eq (SMTExpr a) Source #
Instance details Defined in Language.REST.SMT Methods (==) :: SMTExpr a -> SMTExpr a -> Bool # (/=) :: SMTExpr a -> SMTExpr a -> Bool #
Ord (SMTExpr a) Source #
Instance details 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) Source #
Instance details Defined in Language.REST.SMT Methods showsPrec :: Int -> SMTExpr a -> ShowS # show :: SMTExpr a -> String # showList :: [SMTExpr a] -> ShowS #
Hashable (SMTExpr a) Source #
Instance details Defined in Language.REST.SMT Methods hashWithSalt :: Int -> SMTExpr a -> Int # hash :: SMTExpr a -> Int #

data UntypedExpr Source #

Constructors

UAnd [UntypedExpr]
UAdd [UntypedExpr]
UOr [UntypedExpr]
UEqual [UntypedExpr]
UGreater UntypedExpr UntypedExpr
UGTE UntypedExpr UntypedExpr
UImplies UntypedExpr UntypedExpr
UVar Text
UConst Int

Instances

Instances details

Eq UntypedExpr Source #
Instance details Defined in Language.REST.SMT Methods (==) :: UntypedExpr -> UntypedExpr -> Bool # (/=) :: UntypedExpr -> UntypedExpr -> Bool #
Ord UntypedExpr Source #
Instance details 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 Source #
Instance details Defined in Language.REST.SMT Methods showsPrec :: Int -> UntypedExpr -> ShowS # show :: UntypedExpr -> String # showList :: [UntypedExpr] -> ShowS #
Generic UntypedExpr Source #
Instance details 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 Source #
Instance details Defined in Language.REST.SMT Methods hashWithSalt :: Int -> UntypedExpr -> Int # hash :: UntypedExpr -> Int #
type Rep UntypedExpr Source #
Instance details 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 Source #

toFormula :: SMTExpr a -> Text Source #

vars :: SMTExpr a -> Set Text Source #

data SMTCommand Source #

Constructors

SMTAssert (SMTExpr Bool)
DeclareVar Text
CheckSat
Push
Pop

smtFalse :: SMTExpr Bool Source #

smtTrue :: SMTExpr Bool Source #

smtAdd :: [SMTExpr Int] -> SMTExpr Int Source #

smtAnd :: SMTExpr Bool -> SMTExpr Bool -> SMTExpr Bool Source #

smtGTE :: SMTExpr Int -> SMTExpr Int -> SMTExpr Bool Source #

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

exprString :: SMTExpr a -> Text Source #

commandString :: SMTCommand -> Text Source #

askCmds :: SMTExpr Bool -> [SMTCommand] Source #

type SolverHandle = (Handle, Handle) Source #

spawnZ3 :: IO (Handle, Handle) Source #

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

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

getModel :: Handle -> IO () Source #

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

checkSat :: SMTExpr Bool -> IO Bool Source #

class ToSMTVar a b | a -> b where Source #

Methods

toSMTVar :: a -> SMTVar b Source #

Instances

Instances details

ToSMTVar Op Int Source #
Instance details Defined in Language.REST.Op Methods toSMTVar :: Op -> SMTVar Int Source #

class ToSMT a b where Source #

Methods

toSMT :: a -> SMTExpr b Source #

Instances

Instances details

ToSMT Int Int Source #
Instance details Defined in Language.REST.SMT Methods toSMT :: Int -> SMTExpr Int Source #
ToSMTVar a b => ToSMT a b Source #
Instance details Defined in Language.REST.SMT Methods toSMT :: a -> SMTExpr b Source #
ToSMTVar a Int => ToSMT (WQO a) Bool Source #
Instance details Defined in Language.REST.Internal.WQO Methods toSMT :: WQO a -> SMTExpr Bool Source #
ToSMTVar a Int => ToSMT (ConstraintsADT a) Bool Source #
Instance details Defined in Language.REST.WQOConstraints.ADT Methods toSMT :: ConstraintsADT a -> SMTExpr Bool Source #