cryptol-2.8.0: Cryptol: The Language of Cryptography

Copyright(c) 2013-2016 Galois Inc.
LicenseBSD3
Maintainercryptol@galois.com
Stabilityprovisional
Portabilityportable
Safe HaskellSafe
LanguageHaskell2010

Cryptol.TypeCheck.Solver.SMT

Contents

Description

 
Synopsis

Setup

data Solver Source #

An SMT solver packed with a logger for debugging.

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

Execute a computation with a fresh solver instance.

isNumeric :: Prop -> Bool Source #

Assumes no And

Debugging

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

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

Proving stuff

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

Returns goals that were not proved

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

Check if the given goals are known to be unsolvable.

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

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