Cryptol.TypeCheck.Solver.SMT

Setup

data Solver

An SMT solver packed with a logger for debugging.

data SolverConfig

Instances

Show SolverConfig

Defined in Cryptol.TypeCheck.InferTypes

Methods

showsPrec :: Int -> SolverConfig -> ShowS

show :: SolverConfig -> String

showList :: [SolverConfig] -> ShowS

Generic SolverConfig

Defined in Cryptol.TypeCheck.InferTypes

Associated Types

type Rep SolverConfig :: Type -> Type

Methods

from :: SolverConfig -> Rep SolverConfig x

to :: Rep SolverConfig x -> SolverConfig

NFData SolverConfig

Defined in Cryptol.TypeCheck.InferTypes

Methods

rnf :: SolverConfig -> ()

type Rep SolverConfig

Defined in Cryptol.TypeCheck.InferTypes

type Rep SolverConfig = D1 ('MetaData "SolverConfig" "Cryptol.TypeCheck.InferTypes" "cryptol-2.12.0-1cEC2pVyc8sLwNRndAigau" 'False) (C1 ('MetaCons "SolverConfig" 'PrefixI 'True) ((S1 ('MetaSel ('Just "solverPath") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FilePath) :*: S1 ('MetaSel ('Just "solverArgs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [String])) :*: (S1 ('MetaSel ('Just "solverVerbose") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :*: S1 ('MetaSel ('Just "solverPreludePath") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [FilePath]))))

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

Execute a computation with a fresh solver instance.

startSolver :: IO () -> SolverConfig -> IO Solver

Start a fresh solver instance

stopSolver :: Solver -> IO ()

Shut down a solver instance

isNumeric :: Prop -> Bool

Assumes no And

resetSolver :: Solver -> SolverConfig -> IO ()

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')]