cryptol-2.9.1: Cryptol: The Language of Cryptography

Copyright	(c) 2013-2016 Galois Inc.
License	BSD3
Maintainer	cryptol@galois.com
Stability	provisional
Portability	portable
Safe Haskell	Safe
Language	Haskell2010

Cryptol.TypeCheck.Solver.SMT

Contents

Setup
Debugging
Proving stuff

Description

Synopsis

data Solver
withSolver :: SolverConfig -> (Solver -> IO a) -> IO a
isNumeric :: Prop -> Bool
debugBlock :: Solver -> String -> IO a -> IO a
debugLog :: DebugLog t => Solver -> t -> IO ()
proveImp :: Solver -> [Prop] -> [Goal] -> IO [Goal]
checkUnsolvable :: Solver -> [Goal] -> IO Bool
tryGetModel :: Solver -> [TVar] -> [Prop] -> IO (Maybe [(TVar, Nat')])
shrinkModel :: Solver -> [TVar] -> [Prop] -> [(TVar, Nat')] -> IO [(TVar, Nat')]

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 #