-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | A simple way to interact with an SMT solver process.
--   
--   A simple way to interact with an SMT solver process.
@package simple-smt
@version 0.9.5


-- | A module for interacting with an SMT solver, using SmtLib-2 format.
module SimpleSMT

-- | An interactive solver process.
data Solver
Solver :: (SExpr -> IO SExpr) -> IO ExitCode -> Solver

-- | Send a command to the solver.
[command] :: Solver -> SExpr -> IO SExpr

-- | Terminate the solver.
[stop] :: Solver -> IO ExitCode

-- | Start a new solver process.
newSolver :: String -> [String] -> Maybe Logger -> IO Solver

-- | A command with no interesting result.
ackCommand :: Solver -> SExpr -> IO ()

-- | A command entirely made out of atoms, with no interesting result.
simpleCommand :: Solver -> [String] -> IO ()

-- | Run a command and return True if successful, and False if unsupported.
--   This is useful for setting options that unsupported by some solvers,
--   but used by others.
simpleCommandMaybe :: Solver -> [String] -> IO Bool

-- | Load the contents of a file.
loadFile :: Solver -> FilePath -> IO ()

-- | Load a raw SMT string.
loadString :: Solver -> String -> IO ()

-- | S-expressions. These are the basic format for SmtLib-2.
data SExpr
Atom :: String -> SExpr
List :: [SExpr] -> SExpr

-- | Show an s-expression.
showsSExpr :: SExpr -> ShowS

-- | Show an S-expression in a somewhat readbale fashion.
ppSExpr :: SExpr -> ShowS

-- | Parse an s-expression.
readSExpr :: String -> Maybe (SExpr, String)

-- | Log messages with minimal formatting. Mostly for debugging.
data Logger
Logger :: (String -> IO ()) -> IO Int -> (Int -> IO ()) -> IO () -> IO () -> Logger

-- | Log a message.
[logMessage] :: Logger -> String -> IO ()
[logLevel] :: Logger -> IO Int
[logSetLevel] :: Logger -> Int -> IO ()

-- | Increase indentation.
[logTab] :: Logger -> IO ()

-- | Decrease indentation.
[logUntab] :: Logger -> IO ()

-- | A simple stdout logger. Shows only messages logged at a level that is
--   greater than or equal to the passed level.
newLogger :: Int -> IO Logger

-- | Run an IO action with the logger set to a specific level, restoring it
--   when done.
withLogLevel :: Logger -> Int -> IO a -> IO a

-- | Log a message at a specific log level.
logMessageAt :: Logger -> Int -> String -> IO ()
logIndented :: Logger -> IO a -> IO a

-- | Set the solver's logic. Usually, this should be done first.
setLogic :: Solver -> String -> IO ()

-- | Set the solver's logic, returning False if the logic is unsupported.
setLogicMaybe :: Solver -> String -> IO Bool

-- | Set a solver option.
setOption :: Solver -> String -> String -> IO ()

-- | Set a solver option, returning False if the option is unsupported.
setOptionMaybe :: Solver -> String -> String -> IO Bool

-- | Request unsat cores. Returns if the solver supports them.
produceUnsatCores :: Solver -> IO Bool
named :: String -> SExpr -> SExpr

-- | Checkpoint state. A special case of <a>pushMany</a>.
push :: Solver -> IO ()

-- | Push multiple scopes.
pushMany :: Solver -> Integer -> IO ()

-- | Restore to last check-point. A special case of <a>popMany</a>.
pop :: Solver -> IO ()

-- | Pop multiple scopes.
popMany :: Solver -> Integer -> IO ()

-- | Execute the IO action in a new solver scope (push before, pop after)
inNewScope :: Solver -> IO a -> IO a

-- | Declare a constant. A common abbreviation for <a>declareFun</a>. For
--   convenience, returns an the declared name as a constant expression.
declare :: Solver -> String -> SExpr -> IO SExpr

-- | Declare a function or a constant. For convenience, returns an the
--   declared name as a constant expression.
declareFun :: Solver -> String -> [SExpr] -> SExpr -> IO SExpr

-- | Declare an ADT using the format introduced in SmtLib 2.6.
declareDatatype :: Solver -> String -> [String] -> [(String, [(String, SExpr)])] -> IO ()

-- | Declare a constant. A common abbreviation for <a>declareFun</a>. For
--   convenience, returns the defined name as a constant expression.
define :: Solver -> String -> SExpr -> SExpr -> IO SExpr

-- | Define a function or a constant. For convenience, returns an the
--   defined name as a constant expression.
defineFun :: Solver -> String -> [(String, SExpr)] -> SExpr -> SExpr -> IO SExpr

-- | Assume a fact.
assert :: Solver -> SExpr -> IO ()

-- | Check if the current set of assertion is consistent.
check :: Solver -> IO Result

-- | Results of checking for satisfiability.
data Result

-- | The assertions are satisfiable
Sat :: Result

-- | The assertions are unsatisfiable
Unsat :: Result

-- | The result is inconclusive
Unknown :: Result

-- | Get the values of some s-expressions. Only valid after a <a>Sat</a>
--   result.
getExprs :: Solver -> [SExpr] -> IO [(SExpr, Value)]

-- | Get the value of a single expression.
getExpr :: Solver -> SExpr -> IO Value

-- | Get the values of some constants in the current model. A special case
--   of <a>getExprs</a>. Only valid after a <a>Sat</a> result.
getConsts :: Solver -> [String] -> IO [(String, Value)]

-- | Get the value of a single constant.
getConst :: Solver -> String -> IO Value

-- | Returns the names of the (named) formulas involved in a contradiction.
getUnsatCore :: Solver -> IO [String]

-- | Common values returned by SMT solvers.
data Value

-- | Boolean value
Bool :: !Bool -> Value

-- | Integral value
Int :: !Integer -> Value

-- | Rational value
Real :: !Rational -> Value

-- | Bit vector: width, value
Bits :: !Int -> !Integer -> Value

-- | Some other value
Other :: !SExpr -> Value

-- | Convert an s-expression to a value.
sexprToVal :: SExpr -> Value

-- | A constant, corresponding to a family indexed by some integers.
fam :: String -> [Integer] -> SExpr

-- | An SMT function.
fun :: String -> [SExpr] -> SExpr

-- | An SMT constant. A special case of <a>fun</a>.
const :: String -> SExpr

-- | The type of integers.
tInt :: SExpr

-- | The type of booleans.
tBool :: SExpr

-- | The type of reals.
tReal :: SExpr

-- | The type of arrays.
tArray :: SExpr -> SExpr -> SExpr

-- | The type of bit vectors.
tBits :: Integer -> SExpr

-- | Integer literals.
int :: Integer -> SExpr

-- | Real (well, rational) literals.
real :: Rational -> SExpr

-- | Boolean literals.
bool :: Bool -> SExpr

-- | A bit vector represented in binary.
--   
--   <ul>
--   <li>If the value does not fit in the bits, then the bits will be
--   increased.</li>
--   <li>The width should be strictly positive.</li>
--   </ul>
bvBin :: Int -> Integer -> SExpr

-- | A bit vector represented in hex.
--   
--   <ul>
--   <li>If the value does not fit in the bits, the bits will be increased
--   to the next multiple of 4 that will fit the value.</li>
--   <li>If the width is not a multiple of 4, it will be rounded up so that
--   it is.</li>
--   <li>The width should be strictly positive.</li>
--   </ul>
bvHex :: Int -> Integer -> SExpr

-- | Render a value as an expression. Bit-vectors are rendered in hex, if
--   their width is a multiple of 4, and in binary otherwise.
value :: Value -> SExpr

-- | Logical negation.
not :: SExpr -> SExpr

-- | Conjunction.
and :: SExpr -> SExpr -> SExpr
andMany :: [SExpr] -> SExpr

-- | Disjunction.
or :: SExpr -> SExpr -> SExpr
orMany :: [SExpr] -> SExpr

-- | Exclusive-or.
xor :: SExpr -> SExpr -> SExpr

-- | Implication.
implies :: SExpr -> SExpr -> SExpr

-- | If-then-else. This is polymorphic and can be used to construct any
--   term.
ite :: SExpr -> SExpr -> SExpr -> SExpr

-- | Equality.
eq :: SExpr -> SExpr -> SExpr
distinct :: [SExpr] -> SExpr

-- | Greater-then
gt :: SExpr -> SExpr -> SExpr

-- | Less-then.
lt :: SExpr -> SExpr -> SExpr

-- | Greater-than-or-equal-to.
geq :: SExpr -> SExpr -> SExpr

-- | Less-than-or-equal-to.
leq :: SExpr -> SExpr -> SExpr

-- | Unsigned less-than on bit-vectors.
bvULt :: SExpr -> SExpr -> SExpr

-- | Unsigned less-than-or-equal on bit-vectors.
bvULeq :: SExpr -> SExpr -> SExpr

-- | Signed less-than on bit-vectors.
bvSLt :: SExpr -> SExpr -> SExpr

-- | Signed less-than-or-equal on bit-vectors.
bvSLeq :: SExpr -> SExpr -> SExpr

-- | Addition. See also <a>bvAdd</a>
add :: SExpr -> SExpr -> SExpr
addMany :: [SExpr] -> SExpr

-- | Subtraction.
sub :: SExpr -> SExpr -> SExpr

-- | Arithmetic negation for integers and reals. See also <a>bvNeg</a>.
neg :: SExpr -> SExpr

-- | Multiplication.
mul :: SExpr -> SExpr -> SExpr

-- | Absolute value.
abs :: SExpr -> SExpr

-- | Integer division.
div :: SExpr -> SExpr -> SExpr

-- | Modulus.
mod :: SExpr -> SExpr -> SExpr

-- | Is the number divisible by the given constant.
divisible :: SExpr -> Integer -> SExpr

-- | Division of real numbers.
realDiv :: SExpr -> SExpr -> SExpr

-- | Satisfies <tt>toInt x &lt;= x</tt> (i.e., this is like Haskell's
--   <a>floor</a>)
toInt :: SExpr -> SExpr

-- | Promote an integer to a real
toReal :: SExpr -> SExpr

-- | Bit vector concatenation.
concat :: SExpr -> SExpr -> SExpr

-- | Extract a sub-sequence of a bit vector.
extract :: SExpr -> Integer -> Integer -> SExpr

-- | Bitwise negation.
bvNot :: SExpr -> SExpr

-- | Bit vector arithmetic negation.
bvNeg :: SExpr -> SExpr

-- | Bitwise conjuction.
bvAnd :: SExpr -> SExpr -> SExpr

-- | Bitwise exclusive or.
bvXOr :: SExpr -> SExpr -> SExpr

-- | Bitwise disjunction.
bvOr :: SExpr -> SExpr -> SExpr

-- | Addition of bit vectors.
bvAdd :: SExpr -> SExpr -> SExpr

-- | Subtraction of bit vectors.
bvSub :: SExpr -> SExpr -> SExpr

-- | Multiplication of bit vectors.
bvMul :: SExpr -> SExpr -> SExpr

-- | Bit vector unsigned division.
bvUDiv :: SExpr -> SExpr -> SExpr

-- | Bit vector unsigned reminder.
bvURem :: SExpr -> SExpr -> SExpr

-- | Bit vector signed division.
bvSDiv :: SExpr -> SExpr -> SExpr

-- | Bit vector signed reminder.
bvSRem :: SExpr -> SExpr -> SExpr

-- | Shift left.
bvShl :: SExpr -> SExpr -> SExpr

-- | Logical shift right.
bvLShr :: SExpr -> SExpr -> SExpr

-- | Arithemti shift right (copies most significant bit).
bvAShr :: SExpr -> SExpr -> SExpr

-- | Extend to the signed equivalent bitvector by <tt>i</tt> bits
signExtend :: Integer -> SExpr -> SExpr

-- | Extend with zeros to the unsigned equivalent bitvector by <tt>i</tt>
--   bits
zeroExtend :: Integer -> SExpr -> SExpr

-- | Get an elemeent of an array.
select :: SExpr -> SExpr -> SExpr

-- | Update an array
store :: SExpr -> SExpr -> SExpr -> SExpr
instance GHC.Show.Show SimpleSMT.Value
instance GHC.Classes.Eq SimpleSMT.Value
instance GHC.Show.Show SimpleSMT.SExpr
instance GHC.Classes.Ord SimpleSMT.SExpr
instance GHC.Classes.Eq SimpleSMT.SExpr
instance GHC.Show.Show SimpleSMT.Result
instance GHC.Classes.Eq SimpleSMT.Result
