| Safe Haskell | Trustworthy |
|---|---|
| Language | Haskell2010 |
Copilot.Theorem.Prover.SMT
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 {}
- 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
- class Default a where
- def :: a
Backends
class Show a => SmtFormat a Source #
Format of SMT-Lib commands.
Minimal complete definition
push, pop, checkSat, setLogic, declFun, assert
Type used to represent SMT-lib commands.
Use the interface in SmtFormat to create such commands.
Type used to represent TPTP expressions.
Although this type implements the SmtFormat interface, only assert is
actually used.
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.
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
Options to configure the provers.
Constructors
| 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
A class for types with a default value.
Minimal complete definition
Nothing