What4.SatResult

Documentation

data SatResult mdl core

Constructors

Sat mdl

Unsat core

Unknown

Instances

(Show mdl, Show core) => Show (SatResult mdl core)

Defined in What4.SatResult

Methods

showsPrec :: Int -> SatResult mdl core -> ShowS

show :: SatResult mdl core -> String

showList :: [SatResult mdl core] -> ShowS

Generic (SatResult mdl core)

Defined in What4.SatResult

Associated Types

type Rep (SatResult mdl core) :: Type -> Type

Methods

from :: SatResult mdl core -> Rep (SatResult mdl core) x

to :: Rep (SatResult mdl core) x -> SatResult mdl core

type Rep (SatResult mdl core)

Defined in What4.SatResult

type Rep (SatResult mdl core) = D1 (MetaData "SatResult" "What4.SatResult" "what4-1.0-IcCGmY3T3YeXUBLCM24Pe" False) (C1 (MetaCons "Sat" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 mdl)) :+: (C1 (MetaCons "Unsat" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 core)) :+: C1 (MetaCons "Unknown" PrefixI False) (U1 :: Type -> Type)))

isSat :: SatResult mdl core -> Bool

isUnsat :: SatResult mdl core -> Bool

isUnknown :: SatResult mdl core -> Bool

forgetModelAndCore :: SatResult a b -> SatResult () ()

traverseSatResult :: Applicative t => (a -> t q) -> (b -> t r) -> SatResult a b -> t (SatResult q r)