| Copyright | (c) Galois Inc 2015-2020 |
|---|---|
| License | BSD3 |
| Maintainer | Rob Dockins <rdockins@galois.com> |
| Stability | provisional |
| Safe Haskell | None |
| Language | Haskell2010 |
What4.Solver.Yices
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
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.
assertForall :: WriterConn t Connection -> [(Text, YicesType)] -> Expr -> IO () Source #
data YicesException Source #
Exceptions that can occur when reading responses from Yices
Constructors
| YicesUnsupported YicesCommand | |
| YicesError YicesCommand Text | |
| YicesParseError YicesCommand Text |
Instances
| Show YicesException Source # | |
Defined in What4.Solver.Yices Methods showsPrec :: Int -> YicesException -> ShowS # show :: YicesException -> String # showList :: [YicesException] -> ShowS # | |
| Exception YicesException Source # | |
Defined in What4.Solver.Yices Methods toException :: YicesException -> SomeException # | |
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.
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 #
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.