What4.Solver.Yices

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

Low-level interface

data Connection

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

Instances

OnlineSolver Connection

Defined in What4.Solver.Yices

Methods

startSolverProcess :: forall scope (st :: Type -> Type) fs. ProblemFeatures -> Maybe Handle -> ExprBuilder scope st fs -> IO (SolverProcess scope Connection)

shutdownSolverProcess :: SolverProcess scope Connection -> IO (ExitCode, Text)

SMTReadWriter Connection

Defined in What4.Solver.Yices

Methods

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

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

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

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

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

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

SMTWriter Connection

Defined in What4.Solver.Yices

Methods

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

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

arrayConstant :: Maybe (ArrayConstantFn (Term Connection))

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

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

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

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

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

pushCommand :: f Connection -> Command Connection

popCommand :: f Connection -> Command Connection

push2Command :: f Connection -> Command Connection

pop2Command :: f Connection -> Command Connection

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

resetCommand :: f Connection -> Command Connection

checkCommands :: f Connection -> [Command Connection]

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

getUnsatAssumptionsCommand :: f Connection -> Command Connection

getUnsatCoreCommand :: f Connection -> Command Connection

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

getAbductNextCommand :: f Connection -> Command Connection

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

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

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

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

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

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

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

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

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

stringTerm :: Text -> Term Connection

stringLength :: Term Connection -> Term Connection

stringIndexOf :: Term Connection -> Term Connection -> Term Connection -> Term Connection

stringContains :: Term Connection -> Term Connection -> Term Connection

stringIsPrefixOf :: Term Connection -> Term Connection -> Term Connection

stringIsSuffixOf :: Term Connection -> Term Connection -> Term Connection

stringSubstring :: Term Connection -> Term Connection -> Term Connection -> Term Connection

stringAppend :: [Term Connection] -> Term Connection

resetDeclaredStructs :: WriterConn t Connection -> IO ()

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

type Command Connection

Defined in What4.Solver.Yices

type Command Connection

type Term Connection

Defined in What4.Solver.Yices

type Term Connection

newConnection

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 ()

Write assume formula predicates for asserting predicate holds.

sendCheck :: WriterConn t Connection -> IO ()

Send a check command to Yices.

sendCheckExistsForall :: WriterConn t Connection -> IO ()

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

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

Push a new solver assumption frame.

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

Pop a previous solver assumption frame.

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

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

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

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

data HandleReader

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

Create a new handle reader for reading the given handle.

yicesType :: TypeMap tp -> YicesType

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

efSolveCommand :: Command Connection

data YicesException

Exceptions that can occur when reading responses from Yices

Constructors

YicesUnsupported YicesCommand

YicesError YicesCommand Text

YicesParseError YicesCommand Text

Instances

Exception YicesException

Defined in What4.Solver.Yices

Methods

toException :: YicesException -> SomeException

fromException :: SomeException -> Maybe YicesException

displayException :: YicesException -> String

Show YicesException

Defined in What4.Solver.Yices

Methods

showsPrec :: Int -> YicesException -> ShowS

show :: YicesException -> String

showList :: [YicesException] -> ShowS

Live connection

yicesEvalBool :: Eval s Bool

Call eval to get a Boolean term.

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

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

Solver adapter interface

yicesAdapter :: SolverAdapter t

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

Run writer and get a yices result.

writeYicesFile

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)

Path to yices

yicesOptions :: [ConfigDesc]

yicesDefaultFeatures :: ProblemFeatures

yicesEnableMCSat :: ConfigOption BaseBoolType

Enable the MC-SAT solver

yicesEnableInteractive :: ConfigOption BaseBoolType

Enable interactive mode (necessary for per-goal timeouts)

yicesGoalTimeout :: ConfigOption BaseIntegerType

Set a per-goal timeout in seconds.