Data.SBV.Control

User queries

data Query a

query

Create a fresh variable

freshVar_

freshVar

Checking satisfiability

data CheckSatResult

checkSat

checkSatUsing

checkSatAssuming

checkSatAssumingWithUnsatisfiableSet

Querying the solver

Extracting values

class SMTValue a

getValue

getUninterpretedValue

getModel

getAssignment

getSMTResult

getUnknownReason

Extracting the unsat core

getUnsatCore

Extracting a proof

getProof

Extracting assertions

getAssertions

Getting solver information

data SMTInfoFlag

data SMTErrorBehavior

data SMTReasonUnknown

data SMTInfoResponse

getInfo

getOption

Entering and exiting assertion stack

getAssertionStackDepth

push

pop

inNewAssertionStack

Tactics

caseSplit

Resetting the solver state

resetAssertions

Communicating results back

Constructing assignments

(|->)

Miscellaneous

echo

Terminating the query

mkSMTResult

exit

Controlling the solver behavior

ignoreExitCode

timeout

Performing actions

io

Solver options

data SMTOption

Logics supported

data Logic