Copyright	(c) Levent Erkok
License	BSD3
Maintainer	erkokl@gmail.com
Stability	experimental
Safe Haskell	None
Language	Haskell2010

Documentation.SBV.Examples.TP.TautologyChecker

Contents

Formula representation
Measuring formulas
Normalization
Variable bindings
Formula evaluation
Tautology checking
Soundness
Normalization correctness
Main soundness theorem
Completeness
Completeness lemmas
Main completeness theorem

Description

A verified tautology checker (unordered BDD-style SAT solver) in SBV. This is a port of the Imandra proof by Grant Passmore, originally inspired by Boyer-Moore '79. See https://raw.githubusercontent.com/imandra-ai/imandrax-examples/refs/heads/main/src/tautology.iml

We define a simple formula type with If-then-else, normalize formulas into a canonical form, and prove both soundness and completeness of the tautology checker. The canonical form is essentially an unordered-BDD, making it easy to evaluate it.

Synopsis

data Formula
- = FTrue
- | FFalse
- | Var {
  - fVar :: Integer
  }
- | If {
  - ifCond :: Formula
  - ifThen :: Formula
  - ifElse :: Formula
  }
cv2Formula :: String -> [CV] -> Formula
_undefiner_Formula :: a
type SFormula = SBV Formula
sFTrue :: SBV Formula
sFFalse :: SBV Formula
sVar :: SBV Integer -> SBV Formula
sIf :: SBV Formula -> SBV Formula -> SBV Formula -> SBV Formula
isFTrue :: SBV Formula -> SBool
isFFalse :: SBV Formula -> SBool
isVar :: SBV Formula -> SBool
isIf :: SBV Formula -> SBool
getVar_1 :: SBV Formula -> SBV Integer
sfVar :: SBV Formula -> SBV Integer
getIf_1 :: SBV Formula -> SBV Formula
sifCond :: SBV Formula -> SBV Formula
getIf_2 :: SBV Formula -> SBV Formula
sifThen :: SBV Formula -> SBV Formula
getIf_3 :: SBV Formula -> SBV Formula
sifElse :: SBV Formula -> SBV Formula
sCaseFormula :: Mergeable result => SBV Formula -> result -> result -> (SBV Integer -> result) -> (SBV Formula -> SBV Formula -> SBV Formula -> result) -> result
ifDepth :: SFormula -> SInteger
ifDepthNonNeg :: TP (Proof (Forall "f" Formula -> SBool))
ifComplexity :: SFormula -> SInteger
ifComplexityPos :: TP (Proof (Forall "f" Formula -> SBool))
ifComplexitySmaller :: TP (Proof (Forall "c" Formula -> Forall "l" Formula -> Forall "r" Formula -> SBool))
isNormal :: SFormula -> SBool
normalize :: SFormula -> SFormula
normalizePreservesComplexity :: TP (Proof (Forall "p" Formula -> Forall "q" Formula -> Forall "s" Formula -> Forall "l" Formula -> Forall "r" Formula -> SBool))
data Binding = Binding {
- varId :: Integer
- value :: Bool
}
cv2Binding :: String -> [CV] -> Binding
_undefiner_Binding :: a
type SBinding = SBV Binding
sBinding :: SBV Integer -> SBV Bool -> SBV Binding
isBinding :: SBV Binding -> SBool
getBinding_1 :: SBV Binding -> SBV Integer
svarId :: SBV Binding -> SBV Integer
getBinding_2 :: SBV Binding -> SBV Bool
svalue :: SBV Binding -> SBV Bool
sCaseBinding :: Mergeable result => SBV Binding -> (SBV Integer -> SBV Bool -> result) -> result
lookUp :: SInteger -> SList Binding -> SBool
isAssigned :: SInteger -> SList Binding -> SBool
assumeTrue :: SInteger -> SList Binding -> SList Binding
assumeFalse :: SInteger -> SList Binding -> SList Binding
isAssignedExtends :: TP (Proof (Forall "i" Integer -> Forall "n" Integer -> Forall "v" Bool -> Forall "bs" [Binding] -> SBool))
lookUpExtends :: TP (Proof (Forall "i" Integer -> Forall "n" Integer -> Forall "v" Bool -> Forall "bs" [Binding] -> SBool))
lookUpSame :: TP (Proof (Forall "n" Integer -> Forall "v" Bool -> Forall "bs" [Binding] -> SBool))
isAssignedSame :: TP (Proof (Forall "n" Integer -> Forall "v" Bool -> Forall "bs" [Binding] -> SBool))
eval :: SFormula -> SList Binding -> SBool
isTautology' :: SFormula -> SList Binding -> SBool
isTautology :: SFormula -> SBool
lookUpStable :: TP (Proof (Forall "a" [Binding] -> Forall "x" Integer -> Forall "b" [Binding] -> SBool))
trueIsAssigned :: TP (Proof (Forall "a" [Binding] -> Forall "x" Integer -> SBool))
evalStable :: TP (Proof (Forall "f" Formula -> Forall "x" Integer -> Forall "v" Bool -> Forall "bs" [Binding] -> SBool))
tautologyImpliesEval :: TP (Proof (Forall "f" Formula -> Forall "a" [Binding] -> Forall "b" [Binding] -> SBool))
normalizeCorrect :: TP (Proof (Forall "f" Formula -> SBool))
normalizeSame :: TP (Proof (Forall "f" Formula -> SBool))
normalizeRespectsTruth :: TP (Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool))
soundness :: TP (Proof (Forall "f" Formula -> Forall "bindings" [Binding] -> SBool))
data FalsifyResult = FalsifyResult {
- falsified :: Bool
- cex :: [Binding]
}
cv2FalsifyResult :: String -> [CV] -> FalsifyResult
_undefiner_FalsifyResult :: a
type SFalsifyResult = SBV FalsifyResult
sFalsifyResult :: SBV Bool -> SBV [Binding] -> SBV FalsifyResult
isFalsifyResult :: SBV FalsifyResult -> SBool
getFalsifyResult_1 :: SBV FalsifyResult -> SBV Bool
sfalsified :: SBV FalsifyResult -> SBV Bool
getFalsifyResult_2 :: SBV FalsifyResult -> SBV [Binding]
scex :: SBV FalsifyResult -> SBV [Binding]
sCaseFalsifyResult :: Mergeable result => SBV FalsifyResult -> (SBV Bool -> SBV [Binding] -> result) -> result
falsify' :: SFormula -> SList Binding -> SFalsifyResult
falsify :: SFormula -> SFalsifyResult
nonTautIsFalsified :: TP (Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool))
falsifyExtendsBindings :: TP (Proof (Forall "f" Formula -> Forall "bs" [Binding] -> Forall "i" Integer -> SBool))
falsifyFalsifies :: TP (Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool))
completenessHelper :: TP (Proof (Forall "f" Formula -> SBool))
completeness :: TP (Proof (Forall "f" Formula -> SBool))

Formula representation

data Formula Source #

A propositional formula with variables and if-then-else.

Constructors

FTrue
FFalse
Var
Fields fVar :: Integer
If
Fields ifCond :: Formula ifThen :: Formula ifElse :: Formula

Instances

Instances details

Arbitrary Formula Source #
Instance details Defined in Documentation.SBV.Examples.TP.TautologyChecker Methods arbitrary :: Gen Formula # shrink :: Formula -> [Formula] #
SymVal Formula Source #
Instance details Defined in Documentation.SBV.Examples.TP.TautologyChecker Methods mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV Formula) Source # mkSymValInit :: State -> SBV Formula -> IO () Source # literal :: Formula -> SBV Formula Source # fromCV :: CV -> Formula Source # isConcretely :: SBV Formula -> (Formula -> Bool) -> Bool Source # minMaxBound :: Maybe (Formula, Formula) Source # free :: MonadSymbolic m => String -> m (SBV Formula) Source # free_ :: MonadSymbolic m => m (SBV Formula) Source # mkFreeVars :: MonadSymbolic m => Int -> m [SBV Formula] Source # symbolic :: MonadSymbolic m => String -> m (SBV Formula) Source # symbolics :: MonadSymbolic m => [String] -> m [SBV Formula] Source # unliteral :: SBV Formula -> Maybe Formula Source # unlitCV :: SBV Formula -> Maybe (Kind, CVal) Source # isConcrete :: SBV Formula -> Bool Source # isSymbolic :: SBV Formula -> Bool Source #
HasKind Formula Source #
Instance details Defined in Documentation.SBV.Examples.TP.TautologyChecker Methods kindOf :: Formula -> Kind Source # hasSign :: Formula -> Bool Source # intSizeOf :: Formula -> Int Source # isBoolean :: Formula -> Bool Source # isBounded :: Formula -> Bool Source # isReal :: Formula -> Bool Source # isFloat :: Formula -> Bool Source # isDouble :: Formula -> Bool Source # isRational :: Formula -> Bool Source # isFP :: Formula -> Bool Source # isUnbounded :: Formula -> Bool Source # isADT :: Formula -> Bool Source # isChar :: Formula -> Bool Source # isString :: Formula -> Bool Source # isList :: Formula -> Bool Source # isSet :: Formula -> Bool Source # isTuple :: Formula -> Bool Source # isArray :: Formula -> Bool Source # isRoundingMode :: Formula -> Bool Source # isUninterpreted :: Formula -> Bool Source # showType :: Formula -> String Source #
HasInductionSchema (Forall ta Formula -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.TP.TautologyChecker Methods inductionSchema :: (Forall ta Formula -> SBool) -> ProofObj Source #
SymVal extraT => HasInductionSchema (Forall ta Formula -> Forall extraS extraT -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.TP.TautologyChecker Methods inductionSchema :: (Forall ta Formula -> Forall extraS extraT -> SBool) -> ProofObj Source #
(SymVal extraT1, SymVal extraT2) => HasInductionSchema (Forall ta Formula -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.TP.TautologyChecker Methods inductionSchema :: (Forall ta Formula -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> SBool) -> ProofObj Source #
(SymVal extraT1, SymVal extraT2, SymVal extraT3) => HasInductionSchema (Forall ta Formula -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.TP.TautologyChecker Methods inductionSchema :: (Forall ta Formula -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> SBool) -> ProofObj Source #
(SymVal extraT1, SymVal extraT2, SymVal extraT3, SymVal extraT4) => HasInductionSchema (Forall ta Formula -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.TP.TautologyChecker Methods inductionSchema :: (Forall ta Formula -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> SBool) -> ProofObj Source #
(SymVal extraT1, SymVal extraT2, SymVal extraT3, SymVal extraT4, SymVal extraT5) => HasInductionSchema (Forall ta Formula -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> Forall extraS5 extraT5 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.TP.TautologyChecker Methods inductionSchema :: (Forall ta Formula -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> Forall extraS5 extraT5 -> SBool) -> ProofObj Source #

cv2Formula :: String -> [CV] -> Formula Source #

Conversion from SMT values to Formula values.

_undefiner_Formula :: a Source #

Autogenerated definition to avoid unused-variable warnings from GHC.

type SFormula = SBV Formula Source #

Symbolic version of the type Formula.

sFTrue :: SBV Formula Source #

Symbolic version of the constructor FTrue.

sFFalse :: SBV Formula Source #

Symbolic version of the constructor FFalse.

sVar :: SBV Integer -> SBV Formula Source #

Symbolic version of the constructor Var.

sIf :: SBV Formula -> SBV Formula -> SBV Formula -> SBV Formula Source #

Symbolic version of the constructor If.

isFTrue :: SBV Formula -> SBool Source #

Field recognizer predicate.

isFFalse :: SBV Formula -> SBool Source #

Field recognizer predicate.

isVar :: SBV Formula -> SBool Source #

Field recognizer predicate.

isIf :: SBV Formula -> SBool Source #

Field recognizer predicate.

getVar_1 :: SBV Formula -> SBV Integer Source #

Field accessor function.

sfVar :: SBV Formula -> SBV Integer Source #

Field accessor function.

getIf_1 :: SBV Formula -> SBV Formula Source #

Field accessor function.

sifCond :: SBV Formula -> SBV Formula Source #

Field accessor function.

getIf_2 :: SBV Formula -> SBV Formula Source #

Field accessor function.

sifThen :: SBV Formula -> SBV Formula Source #

Field accessor function.

getIf_3 :: SBV Formula -> SBV Formula Source #

Field accessor function.

sifElse :: SBV Formula -> SBV Formula Source #

Field accessor function.

sCaseFormula :: Mergeable result => SBV Formula -> result -> result -> (SBV Integer -> result) -> (SBV Formula -> SBV Formula -> SBV Formula -> result) -> result Source #

Case analyzer for the type Formula.

Measuring formulas

ifDepth :: SFormula -> SInteger Source #

Depth of nested If constructors in the condition position.

ifDepthNonNeg :: TP (Proof (Forall "f" Formula -> SBool)) Source #

\(\mathit{ifDepth}(f) \geq 0\)

>>> runTP ifDepthNonNeg
Lemma: ifDepthNonNeg                    Q.E.D.
[Proven] ifDepthNonNeg :: Ɐf ∷ Formula → Bool

ifComplexity :: SFormula -> SInteger Source #

Complexity of a formula (for termination measure).

ifComplexityPos :: TP (Proof (Forall "f" Formula -> SBool)) Source #

\(\mathit{ifComplexity}(f) > 0\)

>>> runTP ifComplexityPos
Lemma: ifComplexityPos                  Q.E.D.
[Proven] ifComplexityPos :: Ɐf ∷ Formula → Bool

ifComplexitySmaller :: TP (Proof (Forall "c" Formula -> Forall "l" Formula -> Forall "r" Formula -> SBool)) Source #

The branches of an If have smaller complexity than the whole.

\(\mathit{ifComplexity}(c) < \mathit{ifComplexity}(\mathit{If}(c, l, r)) \land \mathit{ifComplexity}(l) < \mathit{ifComplexity}(\mathit{If}(c, l, r)) \land \mathit{ifComplexity}(r) < \mathit{ifComplexity}(\mathit{If}(c, l, r))\)

>>> runTP ifComplexitySmaller
Lemma: ifComplexityPos                  Q.E.D.
Lemma: ifComplexitySmaller              Q.E.D.
[Proven] ifComplexitySmaller :: Ɐc ∷ Formula → Ɐl ∷ Formula → Ɐr ∷ Formula → Bool

Normalization

isNormal :: SFormula -> SBool Source #

Check if a formula is in normal form (no nested If in condition position).

normalize :: SFormula -> SFormula Source #

Normalize a formula by eliminating nested Ifs in condition position.

The key transformation is:

  If (If (p, q, r), left, right)
    =
  If (p, If (q, left, right), If (r, left, right))

Note that this transformation increases the size of the formula, but reduces its complexity.

normalizePreservesComplexity :: TP (Proof (Forall "p" Formula -> Forall "q" Formula -> Forall "s" Formula -> Forall "l" Formula -> Forall "r" Formula -> SBool)) Source #

The normalization transformation preserves complexity.

\(\mathit{ifComplexity}(\mathit{If}(p, \mathit{If}(q, l, r), \mathit{If}(s, l, r))) = \mathit{ifComplexity}(\mathit{If}(\mathit{If}(p, q, s), l, r))\)

>>> runTP normalizePreservesComplexity
Lemma: helper                           Q.E.D.
Lemma: normalizePreservesComplexity
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Step: 4                               Q.E.D.
  Step: 5                               Q.E.D.
  Step: 6                               Q.E.D.
  Step: 7                               Q.E.D.
  Result:                               Q.E.D.
[Proven] normalizePreservesComplexity :: Ɐp ∷ Formula → Ɐq ∷ Formula → Ɐs ∷ Formula → Ɐl ∷ Formula → Ɐr ∷ Formula → Bool

Variable bindings

data Binding Source #

A binding associates a variable ID with a boolean value.

Constructors

Binding
Fields varId :: Integer value :: Bool

Instances

Instances details

Arbitrary Binding Source #
Instance details Defined in Documentation.SBV.Examples.TP.TautologyChecker Methods arbitrary :: Gen Binding # shrink :: Binding -> [Binding] #
SymVal Binding Source #
Instance details Defined in Documentation.SBV.Examples.TP.TautologyChecker Methods mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV Binding) Source # mkSymValInit :: State -> SBV Binding -> IO () Source # literal :: Binding -> SBV Binding Source # fromCV :: CV -> Binding Source # isConcretely :: SBV Binding -> (Binding -> Bool) -> Bool Source # minMaxBound :: Maybe (Binding, Binding) Source # free :: MonadSymbolic m => String -> m (SBV Binding) Source # free_ :: MonadSymbolic m => m (SBV Binding) Source # mkFreeVars :: MonadSymbolic m => Int -> m [SBV Binding] Source # symbolic :: MonadSymbolic m => String -> m (SBV Binding) Source # symbolics :: MonadSymbolic m => [String] -> m [SBV Binding] Source # unliteral :: SBV Binding -> Maybe Binding Source # unlitCV :: SBV Binding -> Maybe (Kind, CVal) Source # isConcrete :: SBV Binding -> Bool Source # isSymbolic :: SBV Binding -> Bool Source #
HasKind Binding Source #
Instance details Defined in Documentation.SBV.Examples.TP.TautologyChecker Methods kindOf :: Binding -> Kind Source # hasSign :: Binding -> Bool Source # intSizeOf :: Binding -> Int Source # isBoolean :: Binding -> Bool Source # isBounded :: Binding -> Bool Source # isReal :: Binding -> Bool Source # isFloat :: Binding -> Bool Source # isDouble :: Binding -> Bool Source # isRational :: Binding -> Bool Source # isFP :: Binding -> Bool Source # isUnbounded :: Binding -> Bool Source # isADT :: Binding -> Bool Source # isChar :: Binding -> Bool Source # isString :: Binding -> Bool Source # isList :: Binding -> Bool Source # isSet :: Binding -> Bool Source # isTuple :: Binding -> Bool Source # isArray :: Binding -> Bool Source # isRoundingMode :: Binding -> Bool Source # isUninterpreted :: Binding -> Bool Source # showType :: Binding -> String Source #
HasInductionSchema (Forall ta Binding -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.TP.TautologyChecker Methods inductionSchema :: (Forall ta Binding -> SBool) -> ProofObj Source #
SymVal extraT => HasInductionSchema (Forall ta Binding -> Forall extraS extraT -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.TP.TautologyChecker Methods inductionSchema :: (Forall ta Binding -> Forall extraS extraT -> SBool) -> ProofObj Source #
(SymVal extraT1, SymVal extraT2) => HasInductionSchema (Forall ta Binding -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.TP.TautologyChecker Methods inductionSchema :: (Forall ta Binding -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> SBool) -> ProofObj Source #
(SymVal extraT1, SymVal extraT2, SymVal extraT3) => HasInductionSchema (Forall ta Binding -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.TP.TautologyChecker Methods inductionSchema :: (Forall ta Binding -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> SBool) -> ProofObj Source #
(SymVal extraT1, SymVal extraT2, SymVal extraT3, SymVal extraT4) => HasInductionSchema (Forall ta Binding -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.TP.TautologyChecker Methods inductionSchema :: (Forall ta Binding -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> SBool) -> ProofObj Source #
(SymVal extraT1, SymVal extraT2, SymVal extraT3, SymVal extraT4, SymVal extraT5) => HasInductionSchema (Forall ta Binding -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> Forall extraS5 extraT5 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.TP.TautologyChecker Methods inductionSchema :: (Forall ta Binding -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> Forall extraS5 extraT5 -> SBool) -> ProofObj Source #

cv2Binding :: String -> [CV] -> Binding Source #

Conversion from SMT values to Binding values.

_undefiner_Binding :: a Source #

Autogenerated definition to avoid unused-variable warnings from GHC.

type SBinding = SBV Binding Source #

Symbolic version of the type Binding.

sBinding :: SBV Integer -> SBV Bool -> SBV Binding Source #

Symbolic version of the constructor Binding.

isBinding :: SBV Binding -> SBool Source #

Field recognizer predicate.

getBinding_1 :: SBV Binding -> SBV Integer Source #

Field accessor function.

svarId :: SBV Binding -> SBV Integer Source #

Field accessor function.

getBinding_2 :: SBV Binding -> SBV Bool Source #

Field accessor function.

svalue :: SBV Binding -> SBV Bool Source #

Field accessor function.

sCaseBinding :: Mergeable result => SBV Binding -> (SBV Integer -> SBV Bool -> result) -> result Source #

Case analyzer for the type Binding.

lookUp :: SInteger -> SList Binding -> SBool Source #

Look up a variable in the binding list. If it's not in the list, then it's false.

isAssigned :: SInteger -> SList Binding -> SBool Source #

Check if a variable is assigned in the bindings.

assumeTrue :: SInteger -> SList Binding -> SList Binding Source #

Add a binding assuming the variable is true.

assumeFalse :: SInteger -> SList Binding -> SList Binding Source #

Add a binding assuming the variable is false.

isAssignedExtends :: TP (Proof (Forall "i" Integer -> Forall "n" Integer -> Forall "v" Bool -> Forall "bs" [Binding] -> SBool)) Source #

Adding a binding preserves existing assignments.

>>> runTP isAssignedExtends
Lemma: isAssignedExtends                Q.E.D.
[Proven] isAssignedExtends :: Ɐi ∷ Integer → Ɐn ∷ Integer → Ɐv ∷ Bool → Ɐbs ∷ [Binding] → Bool

lookUpExtends :: TP (Proof (Forall "i" Integer -> Forall "n" Integer -> Forall "v" Bool -> Forall "bs" [Binding] -> SBool)) Source #

Looking up a variable in extended bindings: if already assigned, value is preserved.

>>> runTP lookUpExtends
Lemma: lookUpExtends                    Q.E.D.
[Proven] lookUpExtends :: Ɐi ∷ Integer → Ɐn ∷ Integer → Ɐv ∷ Bool → Ɐbs ∷ [Binding] → Bool

lookUpSame :: TP (Proof (Forall "n" Integer -> Forall "v" Bool -> Forall "bs" [Binding] -> SBool)) Source #

Looking up a variable that was just added returns the added value.

>>> runTP lookUpSame
Lemma: lookUpSame                       Q.E.D.
[Proven] lookUpSame :: Ɐn ∷ Integer → Ɐv ∷ Bool → Ɐbs ∷ [Binding] → Bool

isAssignedSame :: TP (Proof (Forall "n" Integer -> Forall "v" Bool -> Forall "bs" [Binding] -> SBool)) Source #

Adding a binding for a variable makes it assigned.

>>> runTP isAssignedSame
Lemma: isAssignedSame                   Q.E.D.
[Proven] isAssignedSame :: Ɐn ∷ Integer → Ɐv ∷ Bool → Ɐbs ∷ [Binding] → Bool

Formula evaluation

eval :: SFormula -> SList Binding -> SBool Source #

Evaluate a formula under a binding environment.

Tautology checking

isTautology' :: SFormula -> SList Binding -> SBool Source #

Check if a normalized formula is a tautology.

isTautology :: SFormula -> SBool Source #

Main tautology checker.

Soundness

lookUpStable :: TP (Proof (Forall "a" [Binding] -> Forall "x" Integer -> Forall "b" [Binding] -> SBool)) Source #

\(\mathit{lookUp}(x, a \mathbin{+\!\!+} b) = \mathit{if } \mathit{isAssigned}(x, a) \mathit{ then } \mathit{lookUp}(x, a) \mathit{ else } \mathit{lookUp}(x, b)\)

If we look up a variable in a concatenated binding list, we first check the first list, and only if not found there, check the second.

>>> runTP lookUpStable
Inductive lemma: lookUpStable
  Step: Base                            Q.E.D.
  Step: 1 (2 way case split)
    Step: 1.1.1                         Q.E.D.
    Step: 1.1.2                         Q.E.D.
    Step: 1.2.1                         Q.E.D.
    Step: 1.2.2                         Q.E.D.
    Step: 1.Completeness                Q.E.D.
  Result:                               Q.E.D.
[Proven] lookUpStable :: Ɐa ∷ [Binding] → Ɐx ∷ Integer → Ɐb ∷ [Binding] → Bool

trueIsAssigned :: TP (Proof (Forall "a" [Binding] -> Forall "x" Integer -> SBool)) Source #

\(\mathit{lookUp}(x, a) \implies \mathit{isAssigned}(x, a)\)

>>> runTP trueIsAssigned
Inductive lemma: trueIsAssigned
  Step: Base                            Q.E.D.
  Step: 1 (2 way case split)
    Step: 1.1                           Q.E.D.
    Step: 1.2.1                         Q.E.D.
    Step: 1.2.2                         Q.E.D.
    Step: 1.Completeness                Q.E.D.
  Result:                               Q.E.D.
[Proven] trueIsAssigned :: Ɐa ∷ [Binding] → Ɐx ∷ Integer → Bool

evalStable :: TP (Proof (Forall "f" Formula -> Forall "x" Integer -> Forall "v" Bool -> Forall "bs" [Binding] -> SBool)) Source #

\(\mathit{value} = \mathit{lookUp}(x, bs) \implies \mathit{eval}(f, \{x \mapsto \mathit{value}\} :: bs) = \mathit{eval}(f, bs)\)

If we add a redundant binding (same id and value) to the front, evaluation doesn't change.

>>> runTPWith cvc5 evalStable
Lemma: ifComplexityPos                  Q.E.D.
Lemma: ifComplexitySmaller              Q.E.D.
Inductive lemma (strong): evalStable
  Step: Measure is non-negative         Q.E.D.
  Step: 1 (4 way case split)
    Step: 1.1                           Q.E.D.
    Step: 1.2                           Q.E.D.
    Step: 1.3                           Q.E.D.
    Step: 1.4.1                         Q.E.D.
    Step: 1.4.2                         Q.E.D.
    Step: 1.4.3                         Q.E.D.
    Step: 1.4.4                         Q.E.D.
    Step: 1.4.5                         Q.E.D.
    Step: 1.4.6                         Q.E.D.
    Step: 1.Completeness                Q.E.D.
  Result:                               Q.E.D.
[Proven] evalStable :: Ɐf ∷ Formula → Ɐx ∷ Integer → Ɐv ∷ Bool → Ɐbs ∷ [Binding] → Bool

tautologyImpliesEval :: TP (Proof (Forall "f" Formula -> Forall "a" [Binding] -> Forall "b" [Binding] -> SBool)) Source #

Key soundness lemma: If a normalized formula is a tautology under bindings b, then it evaluates to true under b ++ a for any a.

>>> runTPWith (tpRibbon 50 cvc5) tautologyImpliesEval
Lemma: ifComplexityPos                            Q.E.D.
Lemma: ifComplexitySmaller                        Q.E.D.
Lemma: lookUpStable                               Q.E.D.
Lemma: trueIsAssigned                             Q.E.D.
Lemma: evalStable                                 Q.E.D.
Inductive lemma (strong): tautologyImpliesEval
  Step: Measure is non-negative                   Q.E.D.
  Step: 1 (4 way case split)
    Step: 1.1                                     Q.E.D.
    Step: 1.2                                     Q.E.D.
    Step: 1.3.1                                   Q.E.D.
    Step: 1.3.2                                   Q.E.D.
    Step: 1.3.3                                   Q.E.D.
    Step: 1.3.4                                   Q.E.D.
    Step: 1.3.5                                   Q.E.D.
    Step: 1.4 (4 way case split)
      Step: 1.4.1.1                               Q.E.D.
      Step: 1.4.1.2                               Q.E.D.
      Step: 1.4.2.1                               Q.E.D.
      Step: 1.4.2.2                               Q.E.D.
      Step: 1.4.2.3                               Q.E.D.
      Step: 1.4.3 (2 way case split)
        Step: 1.4.3.1.1                           Q.E.D.
        Step: 1.4.3.1.2                           Q.E.D.
        Step: 1.4.3.1.3                           Q.E.D.
        Step: 1.4.3.1.4                           Q.E.D.
        Step: 1.4.3.2 (2 way case split)
          Step: 1.4.3.2.1.1                       Q.E.D.
          Step: 1.4.3.2.1.2                       Q.E.D.
          Step: 1.4.3.2.1.3                       Q.E.D.
          Step: 1.4.3.2.1.4                       Q.E.D.
          Step: 1.4.3.2.1.5                       Q.E.D.
          Step: 1.4.3.2.1.6                       Q.E.D.
          Step: 1.4.3.2.1.7                       Q.E.D.
          Step: 1.4.3.2.1.8                       Q.E.D.
          Step: 1.4.3.2.2.1                       Q.E.D.
          Step: 1.4.3.2.2.2                       Q.E.D.
          Step: 1.4.3.2.2.3                       Q.E.D.
          Step: 1.4.3.2.2.4                       Q.E.D.
          Step: 1.4.3.2.2.5                       Q.E.D.
          Step: 1.4.3.2.2.6                       Q.E.D.
          Step: 1.4.3.2.2.7                       Q.E.D.
          Step: 1.4.3.2.2.8                       Q.E.D.
          Step: 1.4.3.2.Completeness              Q.E.D.
        Step: 1.4.3.Completeness                  Q.E.D.
      Step: 1.4.4                                 Q.E.D.
      Step: 1.4.Completeness                      Q.E.D.
    Step: 1.Completeness                          Q.E.D.
  Result:                                         Q.E.D.
[Proven] tautologyImpliesEval :: Ɐf ∷ Formula → Ɐa ∷ [Binding] → Ɐb ∷ [Binding] → Bool

Normalization correctness

normalizeCorrect :: TP (Proof (Forall "f" Formula -> SBool)) Source #

\(\mathit{isNormal}(\mathit{normalize}(f))\)

Normalization produces normalized formulas.

>>> runTPWith (tpRibbon 50 z3) normalizeCorrect
Lemma: ifComplexityPos                            Q.E.D.
Lemma: ifComplexitySmaller                        Q.E.D.
Lemma: normalizePreservesComplexity               Q.E.D.
Lemma: ifDepthNonNeg                              Q.E.D.
Inductive lemma (strong): normalizeCorrect
  Step: Measure is non-negative                   Q.E.D.
  Step: 1 (4 way case split)
    Step: 1.1                                     Q.E.D.
    Step: 1.2                                     Q.E.D.
    Step: 1.3                                     Q.E.D.
    Step: 1.4 (2 way case split)
      Step: 1.4.1.1                               Q.E.D.
      Step: 1.4.1.2                               Q.E.D.
      Step: 1.4.2.1                               Q.E.D.
      Step: 1.4.2.2                               Q.E.D.
      Step: 1.4.2.3                               Q.E.D.
      Step: 1.4.2.4                               Q.E.D.
      Step: 1.4.2.5                               Q.E.D.
      Step: 1.4.Completeness                      Q.E.D.
    Step: 1.Completeness                          Q.E.D.
  Result:                                         Q.E.D.
[Proven] normalizeCorrect :: Ɐf ∷ Formula → Bool

normalizeSame :: TP (Proof (Forall "f" Formula -> SBool)) Source #

\(\mathit{isNormal}(f) \implies \mathit{normalize}(f) = f\)

Normalizing a normalized formula is the identity.

>>> runTPWith (tpRibbon 50 z3) normalizeSame
Lemma: ifComplexityPos                            Q.E.D.
Lemma: ifComplexitySmaller                        Q.E.D.
Inductive lemma (strong): normalizeSame
  Step: Measure is non-negative                   Q.E.D.
  Step: 1 (4 way case split)
    Step: 1.1                                     Q.E.D.
    Step: 1.2                                     Q.E.D.
    Step: 1.3                                     Q.E.D.
    Step: 1.4.1                                   Q.E.D.
    Step: 1.4.2                                   Q.E.D.
    Step: 1.Completeness                          Q.E.D.
  Result:                                         Q.E.D.
[Proven] normalizeSame :: Ɐf ∷ Formula → Bool

normalizeRespectsTruth :: TP (Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)) Source #

\(\mathit{eval}(\mathit{normalize}(f), bs) = \mathit{eval}(f, bs)\)

Normalization preserves semantics.

>>> runTPWith (tpRibbon 50 z3) normalizeRespectsTruth
Lemma: ifComplexityPos                            Q.E.D.
Lemma: ifComplexitySmaller                        Q.E.D.
Lemma: normalizePreservesComplexity               Q.E.D.
Lemma: ifDepthNonNeg                              Q.E.D.
Inductive lemma (strong): normalizeRespectsTruth
  Step: Measure is non-negative                   Q.E.D.
  Step: 1 (4 way case split)
    Step: 1.1                                     Q.E.D.
    Step: 1.2                                     Q.E.D.
    Step: 1.3                                     Q.E.D.
    Step: 1.4 (2 way case split)
      Step: 1.4.1                                 Q.E.D.
      Step: 1.4.2.1                               Q.E.D.
      Step: 1.4.2.2                               Q.E.D.
      Step: 1.4.2.3                               Q.E.D.
      Step: 1.4.Completeness                      Q.E.D.
    Step: 1.Completeness                          Q.E.D.
  Result:                                         Q.E.D.
[Proven] normalizeRespectsTruth :: Ɐf ∷ Formula → Ɐbs ∷ [Binding] → Bool

Main soundness theorem

soundness :: TP (Proof (Forall "f" Formula -> Forall "bindings" [Binding] -> SBool)) Source #

\(\mathit{isTautology}(f) \implies \mathit{eval}(f, \mathit{bindings})\)

If the tautology checker says a formula is a tautology, then it evaluates to true under any binding environment. This is the soundness theorem.

>>> runTP soundness
Lemma: tautologyImpliesEval             Q.E.D.
Lemma: normalizeRespectsTruth           Q.E.D.
Lemma: normalizeCorrect                 Q.E.D.
Lemma: soundness
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Result:                               Q.E.D.
[Proven] soundness :: Ɐf ∷ Formula → Ɐbindings ∷ [Binding] → Bool

Completeness

data FalsifyResult Source #

Result of attempting to falsify a formula.

Constructors

FalsifyResult
Fields falsified :: Bool cex :: [Binding]

Instances

Instances details

Arbitrary FalsifyResult Source #
Instance details Defined in Documentation.SBV.Examples.TP.TautologyChecker Methods arbitrary :: Gen FalsifyResult # shrink :: FalsifyResult -> [FalsifyResult] #
SymVal FalsifyResult Source #
Instance details Defined in Documentation.SBV.Examples.TP.TautologyChecker Methods mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV FalsifyResult) Source # mkSymValInit :: State -> SBV FalsifyResult -> IO () Source # literal :: FalsifyResult -> SBV FalsifyResult Source # fromCV :: CV -> FalsifyResult Source # isConcretely :: SBV FalsifyResult -> (FalsifyResult -> Bool) -> Bool Source # minMaxBound :: Maybe (FalsifyResult, FalsifyResult) Source # free :: MonadSymbolic m => String -> m (SBV FalsifyResult) Source # free_ :: MonadSymbolic m => m (SBV FalsifyResult) Source # mkFreeVars :: MonadSymbolic m => Int -> m [SBV FalsifyResult] Source # symbolic :: MonadSymbolic m => String -> m (SBV FalsifyResult) Source # symbolics :: MonadSymbolic m => [String] -> m [SBV FalsifyResult] Source # unliteral :: SBV FalsifyResult -> Maybe FalsifyResult Source # unlitCV :: SBV FalsifyResult -> Maybe (Kind, CVal) Source # isConcrete :: SBV FalsifyResult -> Bool Source # isSymbolic :: SBV FalsifyResult -> Bool Source #
HasKind FalsifyResult Source #
Instance details Defined in Documentation.SBV.Examples.TP.TautologyChecker Methods kindOf :: FalsifyResult -> Kind Source # hasSign :: FalsifyResult -> Bool Source # intSizeOf :: FalsifyResult -> Int Source # isBoolean :: FalsifyResult -> Bool Source # isBounded :: FalsifyResult -> Bool Source # isReal :: FalsifyResult -> Bool Source # isFloat :: FalsifyResult -> Bool Source # isDouble :: FalsifyResult -> Bool Source # isRational :: FalsifyResult -> Bool Source # isFP :: FalsifyResult -> Bool Source # isUnbounded :: FalsifyResult -> Bool Source # isADT :: FalsifyResult -> Bool Source # isChar :: FalsifyResult -> Bool Source # isString :: FalsifyResult -> Bool Source # isList :: FalsifyResult -> Bool Source # isSet :: FalsifyResult -> Bool Source # isTuple :: FalsifyResult -> Bool Source # isArray :: FalsifyResult -> Bool Source # isRoundingMode :: FalsifyResult -> Bool Source # isUninterpreted :: FalsifyResult -> Bool Source # showType :: FalsifyResult -> String Source #
HasInductionSchema (Forall ta FalsifyResult -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.TP.TautologyChecker Methods inductionSchema :: (Forall ta FalsifyResult -> SBool) -> ProofObj Source #
SymVal extraT => HasInductionSchema (Forall ta FalsifyResult -> Forall extraS extraT -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.TP.TautologyChecker Methods inductionSchema :: (Forall ta FalsifyResult -> Forall extraS extraT -> SBool) -> ProofObj Source #
(SymVal extraT1, SymVal extraT2) => HasInductionSchema (Forall ta FalsifyResult -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.TP.TautologyChecker Methods inductionSchema :: (Forall ta FalsifyResult -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> SBool) -> ProofObj Source #
(SymVal extraT1, SymVal extraT2, SymVal extraT3) => HasInductionSchema (Forall ta FalsifyResult -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.TP.TautologyChecker Methods inductionSchema :: (Forall ta FalsifyResult -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> SBool) -> ProofObj Source #
(SymVal extraT1, SymVal extraT2, SymVal extraT3, SymVal extraT4) => HasInductionSchema (Forall ta FalsifyResult -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.TP.TautologyChecker Methods inductionSchema :: (Forall ta FalsifyResult -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> SBool) -> ProofObj Source #
(SymVal extraT1, SymVal extraT2, SymVal extraT3, SymVal extraT4, SymVal extraT5) => HasInductionSchema (Forall ta FalsifyResult -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> Forall extraS5 extraT5 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.TP.TautologyChecker Methods inductionSchema :: (Forall ta FalsifyResult -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> Forall extraS5 extraT5 -> SBool) -> ProofObj Source #

cv2FalsifyResult :: String -> [CV] -> FalsifyResult Source #

Conversion from SMT values to FalsifyResult values.

_undefiner_FalsifyResult :: a Source #

Autogenerated definition to avoid unused-variable warnings from GHC.

type SFalsifyResult = SBV FalsifyResult Source #

Symbolic version of the type FalsifyResult.

sFalsifyResult :: SBV Bool -> SBV [Binding] -> SBV FalsifyResult Source #

Symbolic version of the constructor FalsifyResult.

isFalsifyResult :: SBV FalsifyResult -> SBool Source #

Field recognizer predicate.

getFalsifyResult_1 :: SBV FalsifyResult -> SBV Bool Source #

Field accessor function.

sfalsified :: SBV FalsifyResult -> SBV Bool Source #

Field accessor function.

getFalsifyResult_2 :: SBV FalsifyResult -> SBV [Binding] Source #

Field accessor function.

scex :: SBV FalsifyResult -> SBV [Binding] Source #

Field accessor function.

sCaseFalsifyResult :: Mergeable result => SBV FalsifyResult -> (SBV Bool -> SBV [Binding] -> result) -> result Source #

Case analyzer for the type FalsifyResult.

falsify' :: SFormula -> SList Binding -> SFalsifyResult Source #

Attempt to falsify a normalized formula under given bindings. Returns whether falsification succeeded and the counterexample bindings.

falsify :: SFormula -> SFalsifyResult Source #

Falsify a formula by first normalizing it.

Completeness lemmas

nonTautIsFalsified :: TP (Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)) Source #

If a normalized formula is not a tautology, then falsify' returns falsified = true.

>>> runTPWith (tpRibbon 50 cvc5) nonTautIsFalsified
Lemma: ifComplexityPos                            Q.E.D.
Lemma: ifComplexitySmaller                        Q.E.D.
Inductive lemma (strong): nonTautIsFalsified
  Step: Measure is non-negative                   Q.E.D.
  Step: 1 (4 way case split)
    Step: 1.1                                     Q.E.D.
    Step: 1.2                                     Q.E.D.
    Step: 1.3                                     Q.E.D.
    Step: 1.4                                     Q.E.D.
    Step: 1.Completeness                          Q.E.D.
  Result:                                         Q.E.D.
[Proven] nonTautIsFalsified :: Ɐf ∷ Formula → Ɐbs ∷ [Binding] → Bool

falsifyExtendsBindings :: TP (Proof (Forall "f" Formula -> Forall "bs" [Binding] -> Forall "i" Integer -> SBool)) Source #

If a variable is assigned in the input bindings and falsify' succeeds, the lookup value is preserved in the output bindings.

>>> runTPWith (tpRibbon 50 cvc5) falsifyExtendsBindings
Lemma: ifComplexityPos                            Q.E.D.
Lemma: ifComplexitySmaller                        Q.E.D.
Lemma: isAssignedExtends                          Q.E.D.
Lemma: lookUpExtends                              Q.E.D.
Inductive lemma (strong): falsifyExtendsBindings
  Step: Measure is non-negative                   Q.E.D.
  Step: 1 (4 way case split)
    Step: 1.1                                     Q.E.D.
    Step: 1.2                                     Q.E.D.
    Step: 1.3                                     Q.E.D.
    Step: 1.4                                     Q.E.D.
    Step: 1.Completeness                          Q.E.D.
  Result:                                         Q.E.D.
[Proven] falsifyExtendsBindings :: Ɐf ∷ Formula → Ɐbs ∷ [Binding] → Ɐi ∷ Integer → Bool

falsifyFalsifies :: TP (Proof (Forall "f" Formula -> Forall "bs" [Binding] -> SBool)) Source #

If falsify' returns falsified = true, then evaluating the formula with the returned bindings gives false.

>>> runTPWith (tpRibbon 50 cvc5) falsifyFalsifies
Lemma: ifComplexityPos                            Q.E.D.
Lemma: ifComplexitySmaller                        Q.E.D.
Lemma: falsifyExtendsBindings                     Q.E.D.
Lemma: lookUpSame                                 Q.E.D.
Lemma: isAssignedSame                             Q.E.D.
Inductive lemma (strong): falsifyFalsifies
  Step: Measure is non-negative                   Q.E.D.
  Step: 1 (4 way case split)
    Step: 1.1.1                                   Q.E.D.
    Step: 1.1.2                                   Q.E.D.
    Step: 1.1.3                                   Q.E.D.
    Step: 1.2.1                                   Q.E.D.
    Step: 1.2.2                                   Q.E.D.
    Step: 1.2.3                                   Q.E.D.
    Step: 1.3.1                                   Q.E.D.
    Step: 1.3.2                                   Q.E.D.
    Step: 1.3.3                                   Q.E.D.
    Step: 1.4 (4 way case split)
      Step: 1.4.1                                 Q.E.D.
      Step: 1.4.2                                 Q.E.D.
      Step: 1.4.3 (2 way case split)
        Step: 1.4.3.1 (2 way case split)
          Step: 1.4.3.1.1                         Q.E.D.
          Step: 1.4.3.1.2                         Q.E.D.
          Step: 1.4.3.1.Completeness              Q.E.D.
        Step: 1.4.3.2 (2 way case split)
          Step: 1.4.3.2.1                         Q.E.D.
          Step: 1.4.3.2.2                         Q.E.D.
          Step: 1.4.3.2.Completeness              Q.E.D.
        Step: 1.4.3.Completeness                  Q.E.D.
      Step: 1.4.4                                 Q.E.D.
      Step: 1.4.Completeness                      Q.E.D.
    Step: 1.Completeness                          Q.E.D.
  Result:                                         Q.E.D.
[Proven] falsifyFalsifies :: Ɐf ∷ Formula → Ɐbs ∷ [Binding] → Bool

completenessHelper :: TP (Proof (Forall "f" Formula -> SBool)) Source #

Helper lemma for completeness: If a formula is not a tautology, evaluating its normalization with falsify's bindings gives false.

>>> runTPWith cvc5 completenessHelper
Lemma: falsifyFalsifies                 Q.E.D.
Lemma: nonTautIsFalsified               Q.E.D.
Lemma: normalizeCorrect                 Q.E.D.
Lemma: completenessHelper               Q.E.D.
[Proven] completenessHelper :: Ɐf ∷ Formula → Bool

Main completeness theorem

completeness :: TP (Proof (Forall "f" Formula -> SBool)) Source #

\(\lnot\mathit{isTautology}(f) \implies \lnot\mathit{eval}(f, \mathit{falsify}(f).\mathit{bindings})\)

If the tautology checker says a formula is not a tautology, then there exists a binding environment (provided by falsify) under which it evaluates to false. This is the completeness theorem.

>>> runTPWith cvc5 completeness
Lemma: completenessHelper               Q.E.D.
Lemma: normalizeRespectsTruth           Q.E.D.
Lemma: completeness                     Q.E.D.
[Proven] completeness :: Ɐf ∷ Formula → Bool