Cryptol.TypeCheck.Solver.SMT

Setup

data Solver

An SMT solver packed with a logger for debugging.

withSolver :: SolverConfig -> (Solver -> IO a) -> IO a

Execute a computation with a fresh solver instance.

isNumeric :: Prop -> Bool

Assumes no And

Debugging

debugBlock :: Solver -> String -> IO a -> IO a

debugLog :: DebugLog t => Solver -> t -> IO ()

Proving stuff

proveImp :: Solver -> [Prop] -> [Goal] -> IO [Goal]

Returns goals that were not proved

checkUnsolvable :: Solver -> [Goal] -> IO Bool

Check if the given goals are known to be unsolvable.

tryGetModel :: Solver -> [TVar] -> [Prop] -> IO (Maybe [(TVar, Nat')])

shrinkModel :: Solver -> [TVar] -> [Prop] -> [(TVar, Nat')] -> IO [(TVar, Nat')]