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

Safe HaskellNone
LanguageHaskell2010

Copilot.Theorem.Prover.SMT

Synopsis

Documentation

module Data.Default

data Options Source

Tactics

Constructors

Options 

Fields

startK :: Word32
 
maxK :: Word32
 
debug :: Bool
 

Instances

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

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

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

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

yices :: Backend SmtLib Source

Backends

dReal :: Backend SmtLib Source

altErgo :: Backend SmtLib Source

metit :: String -> Backend Tptp Source

z3 :: Backend SmtLib Source

cvc4 :: Backend SmtLib Source

mathsat :: Backend SmtLib Source

data Backend a Source

class Show a => SmtFormat a Source

Minimal complete definition

push, pop, checkSat, setLogic, declFun, assert

Instances

data SmtLib Source

Instances

data Tptp Source

Instances