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

Safe Haskell | Trustworthy
Language | Haskell2010

Copilot.Theorem.Kind2.Prover

Description

A prover backend based on Kind2.

Synopsis

- module Data.Default
- data Options = Options {
  - bmcMax :: Int
  }
- kind2Prover :: Options -> Prover

# Documentation

module Data.Default

data Options Source #

Options for Kind2

Constructors

Options |

Fields

- bmcMax :: Int

  Upper bound on the number of unrolling that base and step will perform (passed to Kind2 via its `--unroll_max` option). A value of 0 means unlimited.

#### Instances

Instances details

Default Options Source # | Default options with unlimited unrolling for base and step.
Instance details Defined in Copilot.Theorem.Kind2.Prover Methods def :: Options Source #

kind2Prover :: Options -> Prover Source #

A prover backend based on Kind2.

The executable `kind2` must exist and its location be in the `PATH`. Kind2 version 1.0 or newer is required: the native input format and the command-line options this prover uses were introduced in Kind2 1.0, and remain supported as of Kind2 3.0.