Safe Haskell	Trustworthy
Language	Haskell2010

Copilot.Theorem.Prover.SMT

Contents

Backends
Tactics
Auxiliary

Description

Connections to various SMT solvers and theorem provers.

Synopsis

data Backend a
class Show a => SmtFormat a
data SmtLib
data Tptp
yices :: Backend SmtLib
dReal :: Backend SmtLib
altErgo :: Backend SmtLib
metit :: String -> Backend Tptp
z3 :: Backend SmtLib
cvc4 :: Backend SmtLib
mathsat :: Backend SmtLib
data Options = Options {
- startK :: Word32
- maxK :: Word32
- debug :: Bool
}
induction :: SmtFormat a => Options -> Backend a -> Proof Universal
kInduction :: SmtFormat a => Options -> Backend a -> Proof Universal
onlySat :: SmtFormat a => Options -> Backend a -> Proof Existential
onlyValidity :: SmtFormat a => Options -> Backend a -> Proof Universal
module Data.Default

Backends

data Backend a Source #

Backend to an SMT solver or theorem prover.

class Show a => SmtFormat a Source #

Format of SMT-Lib commands.

Minimal complete definition

push, pop, checkSat, setLogic, declFun, assert

Instances

Instances details

SmtFormat SmtLib Source #	Interface for SMT-Lib conforming backends.
Instance details Defined in Copilot.Theorem.Prover.SMTLib Methods push :: SmtLib pop :: SmtLib checkSat :: SmtLib setLogic :: String -> SmtLib declFun :: String -> Type -> [Type] -> SmtLib assert :: Expr -> SmtLib
SmtFormat Tptp Source #
Instance details Defined in Copilot.Theorem.Prover.TPTP Methods push :: Tptp pop :: Tptp checkSat :: Tptp setLogic :: String -> Tptp declFun :: String -> Type -> [Type] -> Tptp assert :: Expr -> Tptp

data SmtLib Source #

Type used to represent SMT-lib commands.

Use the interface in SmtFormat to create such commands.

Instances

Instances details

SmtFormat SmtLib Source #	Interface for SMT-Lib conforming backends.
Instance details Defined in Copilot.Theorem.Prover.SMTLib Methods push :: SmtLib pop :: SmtLib checkSat :: SmtLib setLogic :: String -> SmtLib declFun :: String -> Type -> [Type] -> SmtLib assert :: Expr -> SmtLib
Show SmtLib Source #
Instance details Defined in Copilot.Theorem.Prover.SMTLib Methods showsPrec :: Int -> SmtLib -> ShowS # show :: SmtLib -> String # showList :: [SmtLib] -> ShowS #

data Tptp Source #

Type used to represent TPTP expressions.

Although this type implements the SmtFormat interface, only assert is actually used.

Instances

Instances details

SmtFormat Tptp Source #
Instance details Defined in Copilot.Theorem.Prover.TPTP Methods push :: Tptp pop :: Tptp checkSat :: Tptp setLogic :: String -> Tptp declFun :: String -> Type -> [Type] -> Tptp assert :: Expr -> Tptp
Show Tptp Source #
Instance details Defined in Copilot.Theorem.Prover.TPTP Methods showsPrec :: Int -> Tptp -> ShowS # show :: Tptp -> String # showList :: [Tptp] -> ShowS #

yices :: Backend SmtLib Source #

Backend to the Yices 2 SMT solver.

It enables non-linear arithmetic (QF_NRA), which means MCSat will be used.

The command yices-smt2 must be in the user's PATH.

dReal :: Backend SmtLib Source #

Backend to the dReal SMT solver.

It enables non-linear arithmetic (QF_NRA).

The libraries for dReal must be installed and perl must be in the user's PATH.

altErgo :: Backend SmtLib Source #

Backend to the Alt-Ergo SMT solver.

It enables support for uninterpreted functions and mixed nonlinear arithmetic (QF_NIRA).

The command alt-ergo.opt must be in the user's PATH.

metit :: String -> Backend Tptp Source #

Backend to the MetiTaski theorem prover.

The command metit must be in the user's PATH.

The argument string is the path to the tptp subdirectory of the metitarski install location.

z3 :: Backend SmtLib Source #

Backend to the Z3 theorem prover.

The command z3 must be in the user's PATH.

cvc4 :: Backend SmtLib Source #

Backend to the cvc4 SMT solver.

It enables support for uninterpreted functions and mixed nonlinear arithmetic (QF_NIRA).

The command cvc4 must be in the user's PATH.

mathsat :: Backend SmtLib Source #

Backend to the Mathsat SMT solver.

It enables non-linear arithmetic (QF_NRA).

The command mathsat must be in the user's PATH.

Tactics

data Options Source #

Options to configure the provers.

Constructors

Options
Fields startK :: Word32 Initial `k` for the k-induction algorithm. maxK :: Word32 The maximum number of steps of the k-induction algorithm the prover runs before giving up. debug :: Bool If `debug` is set to `True`, the SMTLib/TPTP queries produced by the prover are displayed in the standard output.

Instances

Instances details

Default Options Source #	Default `Options` with a `0` `k` and a max of `10` steps, and that produce no debugging info.
Instance details Defined in Copilot.Theorem.Prover.SMT Methods def :: Options #

induction :: SmtFormat a => Options -> Backend a -> Proof Universal Source #

Tactic to find a proof by standard 1-induction.

The values for startK and maxK in the options are ignored.

kInduction :: SmtFormat a => Options -> Backend a -> Proof Universal Source #

Tactic to find a proof by k-induction.

onlySat :: SmtFormat a => Options -> Backend a -> Proof Existential Source #

Tactic to find only a proof of satisfiability.

onlyValidity :: SmtFormat a => Options -> Backend a -> Proof Universal Source #

Tactic to find only a proof of validity.

Auxiliary

module Data.Default