what4-1.7.1.0: Solver-agnostic symbolic values support for issuing queries
Copyright(c) Galois Inc 2015-2020
LicenseBSD3
MaintainerJoe Hendrix <jhendrix@galois.com>
Stabilityprovisional
Safe HaskellSafe-Inferred
LanguageHaskell2010

What4.SatResult

Description

 

Documentation

data SatResult mdl core Source #

Constructors

Sat mdl 
Unsat core 
Unknown 

Instances

Instances details
Generic (SatResult mdl core) Source # 
Instance details

Defined in What4.SatResult

Associated Types

type Rep (SatResult mdl core) 
Instance details

Defined in What4.SatResult

type Rep (SatResult mdl core) = D1 ('MetaData "SatResult" "What4.SatResult" "what4-1.7.1.0-6kQTtE7QElt3pWV2ufmv7F" '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)))

Methods

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

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

(Show mdl, Show core) => Show (SatResult mdl core) Source # 
Instance details

Defined in What4.SatResult

Methods

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

show :: SatResult mdl core -> String #

showList :: [SatResult mdl core] -> ShowS #

type Rep (SatResult mdl core) Source # 
Instance details

Defined in What4.SatResult

type Rep (SatResult mdl core) = D1 ('MetaData "SatResult" "What4.SatResult" "what4-1.7.1.0-6kQTtE7QElt3pWV2ufmv7F" '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 Source #

isUnsat :: SatResult mdl core -> Bool Source #

isUnknown :: SatResult mdl core -> Bool Source #

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

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