what4-1.5.1: Solver-agnostic symbolic values support for issuing queries

Copyright | (c) Galois Inc 2015-2020
License | BSD3
Maintainer | Rob Dockins <rdockins@galois.com>
Stability | provisional
Safe Haskell | Safe-Inferred
Language | Haskell2010

What4.Solver.Yices

Contents

- Low-level interface
- Live connection
- Solver adapter interface

Description

SMTWriter interface for Yices, using the Yices-specific input language. This language shares many features with SMTLib2, but is not quite compatible.

Synopsis

- data Connection
- newConnection :: OutputStream Text -> InputStream Text -> (IORef (Maybe Int) -> AcknowledgementAction t Connection) -> ProblemFeatures -> SolverGoalTimeout -> SymbolVarBimap t -> IO (WriterConn t Connection)
- assume :: SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
- sendCheck :: WriterConn t Connection -> IO ()
- sendCheckExistsForall :: WriterConn t Connection -> IO ()
- eval :: WriterConn t Connection -> Term Connection -> IO ()
- push :: SMTReadWriter solver => SolverProcess scope solver -> IO ()
- pop :: SMTReadWriter solver => SolverProcess scope solver -> IO ()
- inNewFrame :: (MonadIO m, MonadMask m, SMTReadWriter solver) => SolverProcess scope solver -> m a -> m a
- setParam :: WriterConn t Connection -> ConfigValue -> IO ()
- setYicesParams :: WriterConn t Connection -> Config -> IO ()
- data HandleReader
- startHandleReader :: Handle -> Maybe (OutputStream Text) -> IO HandleReader
- yicesType :: TypeMap tp -> YicesType
- assertForall :: WriterConn t Connection -> [(Text, YicesType)] -> Expr -> IO ()
- efSolveCommand :: Command Connection
- data YicesException
  - = YicesUnsupported YicesCommand
  - | YicesError YicesCommand Text
  - | YicesParseError YicesCommand Text
- yicesEvalBool :: Eval s Bool
- addCommand :: SMTWriter h => WriterConn t h -> Command h -> IO ()
- yicesAdapter :: SolverAdapter t
- runYicesInOverride :: ExprBuilder t st fs -> LogData -> [BoolExpr t] -> (SatResult (GroundEvalFn t) () -> IO a) -> IO a
- writeYicesFile :: ExprBuilder t st fs -> FilePath -> BoolExpr t -> IO ()
- yicesPath :: ConfigOption (BaseStringType Unicode)
- yicesOptions :: [ConfigDesc]
- yicesDefaultFeatures :: ProblemFeatures
- yicesEnableMCSat :: ConfigOption BaseBoolType
- yicesEnableInteractive :: ConfigOption BaseBoolType
- yicesGoalTimeout :: ConfigOption BaseIntegerType

# Low-level interface

data Connection Source #

This is a tag used to indicate that a `WriterConn` is a connection to a specific Yices process.

#### Instances

Instances details

OnlineSolver Connection Source # |
Instance details Defined in What4.Solver.Yices Methods startSolverProcess :: forall scope (st :: Type -> Type) fs. ProblemFeatures -> Maybe Handle -> ExprBuilder scope st fs -> IO (SolverProcess scope Connection) Source # shutdownSolverProcess :: SolverProcess scope Connection -> IO (ExitCode, Text) Source #
SMTReadWriter Connection Source # |

Instance details

Defined in What4.Solver.Yices

Methods

smtEvalFuns :: WriterConn t Connection -> InputStream Text -> SMTEvalFunctions Connection Source #

smtSatResult :: f Connection -> WriterConn t Connection -> IO (SatResult () ()) Source #

smtUnsatCoreResult :: f Connection -> WriterConn t Connection -> IO [Text] Source #

smtAbductResult :: f Connection -> WriterConn t Connection -> Text -> Term Connection -> IO String Source #

smtAbductNextResult :: f Connection -> WriterConn t Connection -> IO String Source #

smtUnsatAssumptionsResult :: f Connection -> WriterConn t Connection -> IO [(Bool, Text)] Source #

SMTWriter Connection Source # |

Instance details

Defined in What4.Solver.Yices

Methods

forallExpr :: [(Text, Some TypeMap)] -> Term Connection -> Term Connection Source #

existsExpr :: [(Text, Some TypeMap)] -> Term Connection -> Term Connection Source #

arrayConstant :: Maybe (ArrayConstantFn (Term Connection)) Source #

arraySelect :: Term Connection -> [Term Connection] -> Term Connection Source #

arrayUpdate :: Term Connection -> [Term Connection] -> Term Connection -> Term Connection Source #

commentCommand :: f Connection -> Builder -> Command Connection Source #

assertCommand :: f Connection -> Term Connection -> Command Connection Source #

assertNamedCommand :: f Connection -> Term Connection -> Text -> Command Connection Source #

pushCommand :: f Connection -> Command Connection Source #

popCommand :: f Connection -> Command Connection Source #

push2Command :: f Connection -> Command Connection Source #

pop2Command :: f Connection -> Command Connection Source #

popManyCommands :: f Connection -> Int -> [Command Connection] Source #

resetCommand :: f Connection -> Command Connection Source #

checkCommands :: f Connection -> [Command Connection] Source #

checkWithAssumptionsCommands :: f Connection -> [Text] -> [Command Connection] Source #

getUnsatAssumptionsCommand :: f Connection -> Command Connection Source #

getUnsatCoreCommand :: f Connection -> Command Connection Source #

getAbductCommand :: f Connection -> Text -> Term Connection -> Command Connection Source #

getAbductNextCommand :: f Connection -> Command Connection Source #

setOptCommand :: f Connection -> Text -> Text -> Command Connection Source #

declareCommand :: forall f (args :: Ctx BaseType) (rtp :: BaseType). f Connection -> Text -> Assignment TypeMap args -> TypeMap rtp -> Command Connection Source #

defineCommand :: forall f (rtp :: BaseType). f Connection -> Text -> [(Text, Some TypeMap)] -> TypeMap rtp -> Term Connection -> Command Connection Source #

synthFunCommand :: forall f (tp :: BaseType). f Connection -> Text -> [(Text, Some TypeMap)] -> TypeMap tp -> Command Connection Source #

declareVarCommand :: forall f (tp :: BaseType). f Connection -> Text -> TypeMap tp -> Command Connection Source #

constraintCommand :: f Connection -> Term Connection -> Command Connection Source #

declareStructDatatype :: forall t (args :: Ctx BaseType). WriterConn t Connection -> Assignment TypeMap args -> IO () Source #

structCtor :: forall (args :: Ctx BaseType). Assignment TypeMap args -> [Term Connection] -> Term Connection Source #

structProj :: forall (args :: Ctx BaseType) (tp :: BaseType). Assignment TypeMap args -> Index args tp -> Term Connection -> Term Connection Source #

stringTerm :: Text -> Term Connection Source #

stringLength :: Term Connection -> Term Connection Source #

stringIndexOf :: Term Connection -> Term Connection -> Term Connection -> Term Connection Source #

stringContains :: Term Connection -> Term Connection -> Term Connection Source #

stringIsPrefixOf :: Term Connection -> Term Connection -> Term Connection Source #

stringIsSuffixOf :: Term Connection -> Term Connection -> Term Connection Source #

stringSubstring :: Term Connection -> Term Connection -> Term Connection -> Term Connection Source #

stringAppend :: [Term Connection] -> Term Connection Source #

resetDeclaredStructs :: WriterConn t Connection -> IO () Source #

writeCommand :: WriterConn t Connection -> Command Connection -> IO () Source #

type Command Connection Source # |
Instance details Defined in What4.Solver.Yices type Command Connection
type Term Connection Source # |
Instance details Defined in What4.Solver.Yices type Term Connection

newConnection Source #

Arguments

:: OutputStream Text |
-> InputStream Text |
-> (IORef (Maybe Int) -> AcknowledgementAction t Connection) |
-> ProblemFeatures | Indicates the problem features to support.
-> SolverGoalTimeout |
-> SymbolVarBimap t |
-> IO (WriterConn t Connection) |

assume :: SMTWriter h => WriterConn t h -> BoolExpr t -> IO () Source #

Write assume formula predicates for asserting predicate holds.

sendCheck :: WriterConn t Connection -> IO () Source #

Send a check command to Yices.

sendCheckExistsForall :: WriterConn t Connection -> IO () Source #

eval :: WriterConn t Connection -> Term Connection -> IO () Source #

push :: SMTReadWriter solver => SolverProcess scope solver -> IO () Source #

Push a new solver assumption frame.

pop :: SMTReadWriter solver => SolverProcess scope solver -> IO () Source #

Pop a previous solver assumption frame.

inNewFrame :: (MonadIO m, MonadMask m, SMTReadWriter solver) => SolverProcess scope solver -> m a -> m a Source #

Perform an action in the scope of a solver assumption frame.

setParam :: WriterConn t Connection -> ConfigValue -> IO () Source #

setYicesParams :: WriterConn t Connection -> Config -> IO () Source #

data HandleReader Source #

Wrapper to help with reading from another process's standard out and stderr.

We want to be able to read from another process's stderr and stdout without causing the process to stall because `stdout` or `stderr` becomes full. This data type will read from either of the handles, and buffer as much data as needed in the queue. It then provides a line-based method for reading that data as strict bytestrings.

startHandleReader :: Handle -> Maybe (OutputStream Text) -> IO HandleReader Source #

Create a new handle reader for reading the given handle.

yicesType :: TypeMap tp -> YicesType Source #

assertForall :: WriterConn t Connection -> [(Text, YicesType)] -> Expr -> IO () Source #

efSolveCommand :: Command Connection Source #

data YicesException Source #

Exceptions that can occur when reading responses from Yices

Constructors

YicesUnsupported YicesCommand |
YicesError YicesCommand Text |
YicesParseError YicesCommand Text |

#### Instances

Instances details

Exception YicesException Source # |
Instance details Defined in What4.Solver.Yices Methods toException :: YicesException -> SomeException Source # fromException :: SomeException -> Maybe YicesException Source # displayException :: YicesException -> String Source #
Show YicesException Source # |
Instance details Defined in What4.Solver.Yices Methods showsPrec :: Int -> YicesException -> ShowS Source # show :: YicesException -> String Source # showList :: [YicesException] -> ShowS Source #

# Live connection

yicesEvalBool :: Eval s Bool Source #

Call eval to get a Boolean term.

addCommand :: SMTWriter h => WriterConn t h -> Command h -> IO () Source #

Write a command to the connection along with position information if it differs from the last position.

# Solver adapter interface

yicesAdapter :: SolverAdapter t Source #

runYicesInOverride :: ExprBuilder t st fs -> LogData -> [BoolExpr t] -> (SatResult (GroundEvalFn t) () -> IO a) -> IO a Source #

Run writer and get a yices result.

writeYicesFile Source #

Arguments

:: ExprBuilder t st fs | Builder for getting current bindings.
-> FilePath | Path to file
-> BoolExpr t | Predicate to check
-> IO () |

Write a yices file that checks the satisfiability of the given predicate.

yicesPath :: ConfigOption (BaseStringType Unicode) Source #

Path to yices

yicesOptions :: [ConfigDesc] Source #

yicesDefaultFeatures :: ProblemFeatures Source #

yicesEnableMCSat :: ConfigOption BaseBoolType Source #

Enable the MC-SAT solver

yicesEnableInteractive :: ConfigOption BaseBoolType Source #

Enable interactive mode (necessary for per-goal timeouts)

yicesGoalTimeout :: ConfigOption BaseIntegerType Source #

Set a per-goal timeout in seconds.