copilot-theorem-4.8: k-induction for Copilot.

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 Source # show :: SmtLib -> String Source # showList :: [SmtLib] -> ShowS Source #

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 Source # show :: Tptp -> String Source # showList :: [Tptp] -> ShowS Source #

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 Source #

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