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

Copyright(c) Galois Inc 2015-2020
LicenseBSD3
MaintainerRob Dockins <rdockins@galois.com>
Stabilityprovisional
Safe HaskellNone
LanguageHaskell2010

What4.Solver.Yices

Contents

Description

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

Synopsis

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
SMTReadWriter Connection Source # 
Instance details

Defined in What4.Solver.Yices

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 #

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 #

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

declareCommand :: f Connection -> Text -> Assignment TypeMap args -> TypeMap rtp -> Command Connection Source #

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

declareStructDatatype :: WriterConn t Connection -> Assignment TypeMap args -> IO () Source #

structCtor :: Assignment TypeMap args -> [Term Connection] -> Term Connection Source #

structProj :: Assignment TypeMap args -> Index args tp -> Term Connection -> Term Connection Source #

stringTerm :: ByteString -> 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 #

OnlineSolver Connection Source # 
Instance details

Defined in What4.Solver.Yices

type Command Connection Source # 
Instance details

Defined in What4.Solver.Yices

type Term Connection Source # 
Instance details

Defined in What4.Solver.Yices

newConnection Source #

Arguments

:: OutputStream Text 
-> InputStream Text 
-> (IORef (Maybe Int) -> AcknowledgementAction t Connection) 
-> ProblemFeatures

Indicates the problem features to support.

-> Integer 
-> 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.

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.

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 #

data YicesException Source #

Exceptions that can occur when reading responses from Yices

Constructors

YicesUnsupported YicesCommand 
YicesError YicesCommand Text 
YicesParseError YicesCommand Text 

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

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.

yicesEnableInteractive :: ConfigOption BaseBoolType Source #

Enable interactive mode (necessary for per-goal timeouts)

yicesGoalTimeout :: ConfigOption BaseIntegerType Source #

Set a per-goal timeout in seconds.