-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.Misc.FirstOrderLogic
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Proves various first-order logic properties using SBV. The properties we
-- prove all come from <https://en.wikipedia.org/wiki/First-order_logic>
-----------------------------------------------------------------------------

{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE DeriveAnyClass      #-}
{-# LANGUAGE DeriveDataTypeable  #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving  #-}
{-# LANGUAGE TemplateHaskell     #-}
{-# LANGUAGE TypeApplications    #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.Misc.FirstOrderLogic where

import Data.SBV

-- $setup
-- >>> -- For doctest purposes only, ignore.
-- >>> import Data.SBV
-- >>> :set -XDataKinds

-- | An uninterpreted sort for demo purposes, named 'U'
data U
mkUninterpretedSort ''U

-- | An uninterpreted sort for demo purposes, named 'V'
data V
mkUninterpretedSort ''V

-- | An enumerated type for demo purposes, named 'E'
data E = A | B | C
mkSymbolicEnumeration ''E

-- | Helper to turn quantified formula to a regular boolean. We
-- can think of this as quantifier elimination, hence the name 'qe'.
qe :: QuantifiedBool a => a -> SBool
qe :: forall a. QuantifiedBool a => a -> SBool
qe = a -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool

-- * Pushing negation over quantifiers
{- $negUniv
\(\lnot \forall x\,P(x)\Leftrightarrow \exists x\,\lnot P(x)\)

>>> let p = uninterpret "P" :: SU -> SBool
>>> prove $ sNot (qe (\(Forall x) -> p x)) .<=> qe (\(Exists x) -> sNot (p x))
Q.E.D.

\(\lnot \exists x\,P(x)\Leftrightarrow \forall x\,\lnot P(x)\)

>>> let p = uninterpret "P" :: SU -> SBool
>>> prove $ sNot (qe (\(Exists x) -> p x)) .<=> qe (\(Forall x) -> sNot (p x))
Q.E.D.
-}

-- * Interchanging quantifiers
{- $interchange
\(\forall x\,\forall y\,P(x,y)\Leftrightarrow \forall y\,\forall x\,P(x,y)\)

>>> let p = uninterpret "P" :: (SU, SV) -> SBool
>>> prove $ qe (\(Forall x) (Forall y) -> p (x, y)) .<=> qe (\(Forall y) (Forall x) -> p (x, y))
Q.E.D.

\(\exists x\,\exists y\,P(x,y)\Leftrightarrow \exists y\,\exists x\,P(x,y)\)

>>> let p = uninterpret "P" :: (SU, SV) -> SBool
>>> prove $ qe (\(Exists x) (Exists y) -> p (x, y)) .<=> qe (\(Exists y) (Exists x) -> p (x, y))
Q.E.D.
-}

-- * Merging quantifiers
{- $mergeQuants
\(\forall x\,P(x)\land \forall x\,Q(x)\Leftrightarrow \forall x\,(P(x)\land Q(x))\)

>>> let p = uninterpret "P" :: SU -> SBool
>>> let q = uninterpret "Q" :: SU -> SBool
>>> prove $ (qe (\(Forall x) -> p x) .&& qe (\(Forall x) -> q x)) .<=> qe (\(Forall x) -> p x .&& q x)
Q.E.D.

\(\exists x\,P(x)\lor \exists x\,Q(x)\Leftrightarrow \exists x\,(P(x)\lor Q(x))\)

>>> let p = uninterpret "P" :: SU -> SBool
>>> let q = uninterpret "Q" :: SU -> SBool
>>> prove $ (qe (\(Exists x) -> p x) .|| qe (\(Exists x) -> q x)) .<=> qe (\(Exists x) -> p x .|| q x)
Q.E.D.
-}

-- * Scoping over quantifiers
{- $scopeOverQuants
Provided \(x\) is not free in \(P\): \(P\land \exists x\,Q(x)\Leftrightarrow \exists x\,(P\land Q(x))\)

>>> let p = uninterpret "P" :: SBool
>>> let q = uninterpret "Q" :: SU -> SBool
>>> prove $ (p .&& qe (\(Exists x) -> q x)) .<=> qe (\(Exists x) -> p .&& q x)
Q.E.D.

Provided \(x\) is not free in \(P\): \(P\lor \forall x\,Q(x)\Leftrightarrow \forall x\,(P\lor Q(x))\)

>>> let p = uninterpret "P" :: SBool
>>> let q = uninterpret "Q" :: SU -> SBool
>>> prove $ (p .|| qe (\(Forall x) -> q x)) .<=> qe (\(Forall x) -> p .|| q x)
Q.E.D.
-}

-- * A non-identity
{- $nonIdentity
It's instructive to look at an example where the proof actually fails. Consider, for instance, an
example of a merging quantifiers like we did above, except when the equality doesn't hold. That
is, we try to prove the "correct" sounding, but incorrect conjecture:

\(\forall x\,P(x)\lor \forall x\,Q(x)\Leftrightarrow \forall x\,(P(x)\lor Q(x))\)

We have:

>>> let p = uninterpret "P" :: SU -> SBool
>>> let q = uninterpret "Q" :: SU -> SBool
>>> prove $ (qe (\(Forall x) -> p x) .|| qe (\(Forall x) -> q x)) .<=> qe (\(Forall x) -> p x .|| q x)
Falsifiable. Counter-example:
  P :: U -> Bool
  P U!val!2 = True
  P U!val!0 = True
  P _       = False
<BLANKLINE>
  Q :: U -> Bool
  Q U!val!2 = False
  Q U!val!0 = False
  Q _       = True

The solver found us a falsifying instance: Pick a domain with at least three elements. We'll call
the first element @U!val!2@, and the second element @U!val!0@, without naming the others. (Unfortunately the solver picks nonintuitive names, but you can substitute better names if you like. They're just names of two distinct
objects that belong to the domain \(U\) with no other meaning.)

Arrange so that \(P\) is true on @U!val!2@ and @U!val!0@, but false for everything else.
Also arrange so that \(Q\) is false on these two elements, but true for everything else.

With this
assignment, the right hand side of our conjecture
is true no matter which element you pick, because either \(P\) or \(Q\) is true on any
given element. (Actually, only one will be true on any element, but that is tangential.)
But left-hand-side is not a tautology: Clearly neither \(P\) nor \(Q\) are true for all elements, and
hence both disjuncts are false. Thus, the alleged conjecture is not an equivalence in first order logic.
-}

-- * Exists unique
{- $existsUnique
We can use the 'ExistsUnique' constructor to indicate a value must exists uniquely. For instance,
we can prove that there is an element in 'E' that's less than 'C', but it's not unique. However,
there's a unique element that's less than all the elements in 'E':

>>> prove $ \(Exists       (me :: SE)) -> me .<= sC
Q.E.D.
>>> prove $ \(ExistsUnique (me :: SE)) -> me .<= sC
Falsifiable
>>> prove $ \(ExistsUnique (me :: SE)) (Forall e) -> me .<= e
Q.E.D.
-}

-- * Skolemization
{- $skolemization
Given a formula, skolemization produces an equisatisfiable formula that has no existential quantifiers. Instead,
the existentials are replaced by uninterpreted functions.
Skolemization is useful when we want to see the instantiation of nested existential variables. Interpretation for such variables will be
functions of the enclosing universals.
-}

-- | Consider the formula \(\forall x\,\exists y\, x \ge y\), over bit-vectors of size 8. We can ask SBV to satisfy it:
--
-- >>> sat skolemEx1
-- Satisfiable
--
-- But this isn't really illimunating. We can first skolemize, and then ask to satisfy:
--
-- >>> sat $ skolemize skolemEx1
-- Satisfiable. Model:
--   y :: Word8 -> Word8
--   y x = x
--
-- which is much better We are told that we can have the witness as the value given for each choice of @x@.
skolemEx1 :: Forall "x" Word8 -> Exists "y" Word8 -> SBool
skolemEx1 :: Forall "x" Word8 -> Exists "y" Word8 -> SBool
skolemEx1 (Forall SBV Word8
x) (Exists SBV Word8
y) = SBV Word8
x SBV Word8 -> SBV Word8 -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV Word8
y

-- | Consider the formula \(\forall a\,\exists b\,\forall c\,\exists d\, a + b >= c + d\), over bit-vectors of size 8. We can ask SBV to satisfy it:
--
-- >>> sat skolemEx2
-- Satisfiable
--
-- Again, we're left in the dark as to why this is satisfiable. Let's skolemize first, and then call 'sat' on it:
--
-- >>> sat $ skolemize skolemEx2
-- Satisfiable. Model:
--   b :: Word8 -> Word8
--   b _ = 0
-- <BLANKLINE>
--   d :: Word8 -> Word8 -> Word8
--   d a c = a + (255 * c)
--
-- Let's see what the solver said. It suggested we should use the value of @0@ for @b@, regardless of the
-- choice of @a@. (Note how @b@ is a function of one variable, i.e., of @a@)
-- And it suggested using @a + (255 * c)@ for @d@,
-- for whatever we choose for @a@ and @c@. Why does this work? Well, given
-- arbitrary @a@ and @c@, we end up with:
--
-- @
--     a + b >= c + d
--     --> substitute b = 0 and d = a + 255c as suggested by the solver
--     a + 0 >= c + a + 255c
--     a >= 256c + a
--     a >= a
-- @
--
-- showing the formula is satisfiable for whatever values you pick for @a@ and @c@. Note that @256@ is simply
-- @0@ when interpreted modulo @2^8@. Clever!
skolemEx2 :: Forall "a" Word8 -> Exists "b" Word8 -> Forall "c" Word8 -> Exists "d" Word8 -> SBool
skolemEx2 :: Forall "a" Word8
-> Exists "b" Word8
-> Forall "c" Word8
-> Exists "d" Word8
-> SBool
skolemEx2 (Forall SBV Word8
a) (Exists SBV Word8
b) (Forall SBV Word8
c) (Exists SBV Word8
d) = SBV Word8
a SBV Word8 -> SBV Word8 -> SBV Word8
forall a. Num a => a -> a -> a
+ SBV Word8
b SBV Word8 -> SBV Word8 -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV Word8
c SBV Word8 -> SBV Word8 -> SBV Word8
forall a. Num a => a -> a -> a
+ SBV Word8
d

-- | A common proof technique to show validity is to show that the negation is unsatisfiable. Note
-- that if you want to skolemize during this process, you should first /negate/ and then skolemize!
--
-- This example demonstrates the possible pitfall. The 'skolemEx3' function
-- encodes \(\exists x\, \forall y\, y \ge x\) for 8-bit bitvectors; which is a valid statement since
-- @x = 0@ acts as the witness. We can directly prove this in SBV:
--
-- >>> prove skolemEx3
-- Q.E.D.
--
-- Or, we can ask if the negation is unsatisfiable:
--
-- >>> sat (qNot skolemEx3)
-- Unsatisfiable
--
-- If we want, we can skolemize after the negation step:
--
-- >>> sat (skolemize (qNot skolemEx3))
-- Unsatisfiable
--
-- and get the same result. However, it would be __unsound__ to skolemize first and then negate:
--
-- >>> sat (qNot (skolemize skolemEx3))
-- Satisfiable. Model:
--   x = 1 :: Word8
--
-- And that would be the incorrect conclusion that our formula is invalid with a counter-example! You
-- can see the same by doing:
--
-- >>> prove (skolemize skolemEx3)
-- Falsifiable. Counter-example:
--   x = 1 :: Word8
--
-- So, if you want to check validity and want to also perform skolemization; you should negate your
-- formula first and then skolemize, not the other way around!
skolemEx3 :: Exists "x" Word8 -> Forall "y" Word8 -> SBool
skolemEx3 :: Exists "x" Word8 -> Forall "y" Word8 -> SBool
skolemEx3 (Exists SBV Word8
x) (Forall SBV Word8
y) = SBV Word8
y SBV Word8 -> SBV Word8 -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV Word8
x

-- | If you skolemize different formulas that share the same name for their existentials, then SBV will
-- get confused and will think those represent the same skolem function. This is unfortunate, but it follows
-- the requirement that uninterpreted function names should be unique. In this particular case, however, since
-- SBV creates these functions, it is harder to control the internal names. In such cases, use the function
-- 'taggedSkolemize' to provide a name to prefix the skolem functions. As demonstrated by 'skolemEx4'. We get:
--
-- >>> skolemEx4
-- Satisfiable. Model:
--   c1_y :: Integer -> Integer
--   c1_y x = x
-- <BLANKLINE>
--   c2_y :: Integer -> Integer
--   c2_y x = 1 + x
--
-- Note how the internal skolem functions are named according to the tag given. If you use regular 'skolemize'
-- this program will essentially do the wrong thing by assuming the skolem functions for both predicates are
-- the same, and will return unsat. Beware!
-- All skolem functions should be named differently in your program for your deductions to be sound.
skolemEx4 :: IO SatResult
skolemEx4 :: IO SatResult
skolemEx4 = ConstraintSet -> IO SatResult
forall a. Satisfiable a => a -> IO SatResult
sat ConstraintSet
cs
  where cs :: ConstraintSet
        cs :: ConstraintSet
cs = do (Forall "x" Integer -> SBool) -> ConstraintSet
forall a. QuantifiedBool a => a -> ConstraintSet
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain ((Forall "x" Integer -> SBool) -> ConstraintSet)
-> (Forall "x" Integer -> SBool) -> ConstraintSet
forall a b. (a -> b) -> a -> b
$ String
-> (Forall "x" Integer -> Exists "y" Integer -> SBool)
-> SkolemsTo (Forall "x" Integer -> Exists "y" Integer -> SBool)
forall a.
(Skolemize a, Constraint (SymbolicT IO) (SkolemsTo a),
 Skolemize a) =>
String -> a -> SkolemsTo a
taggedSkolemize String
"c1" ((Forall "x" Integer -> Exists "y" Integer -> SBool)
 -> SkolemsTo (Forall "x" Integer -> Exists "y" Integer -> SBool))
-> (Forall "x" Integer -> Exists "y" Integer -> SBool)
-> SkolemsTo (Forall "x" Integer -> Exists "y" Integer -> SBool)
forall a b. (a -> b) -> a -> b
$ \(Forall @"x" SBV Integer
x) (Exists @"y" SBV Integer
y) -> SBV Integer
x SBV Integer -> SBV Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SBV Integer
y   :: SInteger)
                (Forall "x" Integer -> SBool) -> ConstraintSet
forall a. QuantifiedBool a => a -> ConstraintSet
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain ((Forall "x" Integer -> SBool) -> ConstraintSet)
-> (Forall "x" Integer -> SBool) -> ConstraintSet
forall a b. (a -> b) -> a -> b
$ String
-> (Forall "x" Integer -> Exists "y" Integer -> SBool)
-> SkolemsTo (Forall "x" Integer -> Exists "y" Integer -> SBool)
forall a.
(Skolemize a, Constraint (SymbolicT IO) (SkolemsTo a),
 Skolemize a) =>
String -> a -> SkolemsTo a
taggedSkolemize String
"c2" ((Forall "x" Integer -> Exists "y" Integer -> SBool)
 -> SkolemsTo (Forall "x" Integer -> Exists "y" Integer -> SBool))
-> (Forall "x" Integer -> Exists "y" Integer -> SBool)
-> SkolemsTo (Forall "x" Integer -> Exists "y" Integer -> SBool)
forall a b. (a -> b) -> a -> b
$ \(Forall @"x" SBV Integer
x) (Exists @"y" SBV Integer
y) -> SBV Integer
x SBV Integer -> SBV Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SBV Integer
ySBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
-SBV Integer
1 :: SInteger)

-- * Special relations

-- ** Partial orders
{- $partialOrder
A partial order is a reflexive, antisymmetic, and a transitive relation. We can prove these properties
for relations that are checked by the 'isPartialOrder' predicate in SBV:

\(\forall x\,R(x,x)\)

\(\forall x\,\forall y\, R(x, y) \land R(y, x) \Rightarrow x = y\)

\(\forall x\,\forall y\, \forall z\, R(x, y) \land R(y, z) \Rightarrow R(x, z)\)

>>> let r         = uninterpret "R" :: Relation U
>>> let isPartial = isPartialOrder "poR" r
>>> prove $ \(Forall x) -> isPartial .=> r (x, x)
Q.E.D.
>>> prove $ \(Forall x) (Forall y) -> isPartial .=> (r (x, y) .&& r (y, x) .=> x .== y)
Q.E.D.
>>> prove $ \(Forall x) (Forall y) (Forall z) -> isPartial .=> (r (x, y) .&& r (y, z) .=> r (x, z))
Q.E.D.
-}

-- | Demonstrates creating a partial order. We have:
--
-- >>> poExample
-- Q.E.D.
poExample :: IO ThmResult
poExample :: IO ThmResult
poExample = SymbolicT IO SBool -> IO ThmResult
forall a. Provable a => a -> IO ThmResult
prove (SymbolicT IO SBool -> IO ThmResult)
-> SymbolicT IO SBool -> IO ThmResult
forall a b. (a -> b) -> a -> b
$ do
  let r :: Relation E
r = String -> Relation E
forall a. SMTDefinable a => String -> a
uninterpret String
"R" :: Relation E
  SBool -> ConstraintSet
forall a. QuantifiedBool a => a -> ConstraintSet
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> ConstraintSet) -> SBool -> ConstraintSet
forall a b. (a -> b) -> a -> b
$ String -> Relation E -> SBool
forall a. SymVal a => String -> Relation a -> SBool
isPartialOrder String
"poR" Relation E
r

  SBool -> SymbolicT IO SBool
forall a. a -> SymbolicT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SBool -> SymbolicT IO SBool) -> SBool -> SymbolicT IO SBool
forall a b. (a -> b) -> a -> b
$ (Forall Any E -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
qe (\(Forall SBV E
x) -> Relation E
r (SBV E
x, SBV E
x)) :: Predicate

-- ** Linear orders
{- $linearOrder
A linear order, ensured by the predicate 'isLinearOrder', satisfies the following axioms:

\(\forall x\,R(x,x)\)

\(\forall x\,\forall y\, R(x, y) \land R(y, x) \Rightarrow x = y\)

\(\forall x\,\forall y\, \forall z\, R(x, y) \land R(y, z) \Rightarrow R(x, z)\)

\(\forall x\,\forall y\, R(x, y) \lor R(y, x)\)

>>> let r        = uninterpret "R" :: Relation U
>>> let isLinear = isLinearOrder "loR" r
>>> prove $ \(Forall x) -> isLinear .=> r (x, x)
Q.E.D.
>>> prove $ \(Forall x) (Forall y) -> isLinear .=> (r (x, y) .&& r (y, x) .=> x .== y)
Q.E.D.
>>> prove $ \(Forall x) (Forall y) (Forall z) -> isLinear .=> (r (x, y) .&& r (y, z) .=> r (x, z))
Q.E.D.
>>> prove $ \(Forall x) (Forall y) -> isLinear .=> (r (x, y) .|| r (y, x))
Q.E.D.
-}

-- ** Tree orders
{- $treeOrder
A tree order, ensured by the predicate 'isTreeOrder', satisfies the following axioms:

\(\forall x\,R(x,x)\)

\(\forall x\,\forall y\, R(x, y) \land R(y, x) \Rightarrow x = y\)

\(\forall x\,\forall y\, \forall z\, R(x, y) \land R(y, z) \Rightarrow R(x, z)\)

\(\forall x\,\forall y\,\forall z\, (R(y, x) \land R(z, z)) \Rightarrow (R (y, z) \lor R (z, y))\)

>>> let r      = uninterpret "R" :: Relation U
>>> let isTree = isTreeOrder "toR" r
>>> prove $ \(Forall x) -> isTree .=> r (x, x)
Q.E.D.
>>> prove $ \(Forall x) (Forall y) -> isTree .=> (r (x, y) .&& r (y, x) .=> x .== y)
Q.E.D.
>>> prove $ \(Forall x) (Forall y) (Forall z) -> isTree .=> (r (x, y) .&& r (y, z) .=> r (x, z))
Q.E.D.
>>> prove $ \(Forall x) (Forall y) (Forall z) -> isTree .=> ((r (y, x) .&& r (z, x)) .=> (r (y, z) .|| r (z, y)))
Q.E.D.
-}

-- ** Piecewise linear orders
{- $piecewiseLinear
A piecewise linear order, ensured by the predicate 'isPiecewiseLinearOrder', satisfies the following axioms:

\(\forall x\,R(x,x)\)

\(\forall x\,\forall y\, R(x, y) \land R(y, x) \Rightarrow x = y\)

\(\forall x\,\forall y\, \forall z\, R(x, y) \land R(y, z) \Rightarrow R(x, z)\)

\(\forall x\,\forall y\,\forall z\, (R(x, y) \land R(x, z)) \Rightarrow (R (y, z) \lor R (z, y))\)

\(\forall x\,\forall y\,\forall z\, (R(y, x) \land R(z, x)) \Rightarrow (R (y, z) \lor R (z, y))\)

>>> let r           = uninterpret "R" :: Relation U
>>> let isPiecewise = isPiecewiseLinearOrder "plR" r
>>> prove $ \(Forall x) -> isPiecewise .=> r (x, x)
Q.E.D.
>>> prove $ \(Forall x) (Forall y) -> isPiecewise .=> (r (x, y) .&& r (y, x) .=> x .== y)
Q.E.D.
>>> prove $ \(Forall x) (Forall y) (Forall z) -> isPiecewise .=> (r (x, y) .&& r (y, z) .=> r (x, z))
Q.E.D.
>>> prove $ \(Forall x) (Forall y) (Forall z) -> isPiecewise .=> ((r (x, y) .&& r (x, z)) .=> (r (y, z) .|| r (z, y)))
Q.E.D.
>>> prove $ \(Forall x) (Forall y) (Forall z) -> isPiecewise .=> ((r (y, x) .&& r (z, x)) .=> (r (y, z) .|| r (z, y)))
Q.E.D.
-}

-- ** Transitive closures
{- $transitiveClosures
The transitive closure of a relation can be created using 'mkTransitiveClosure'. Transitive closures
are not first-order axiomatizable. That is, we cannot write first-order formulas to uniquely
describe them. However, we can check some of the expected properties:

>>> let r   = uninterpret "R" :: Relation U
>>> let tcR = mkTransitiveClosure "tcR" r
>>> prove $ \(Forall x) (Forall y) -> r (x, y) .=> tcR (x, y)
Q.E.D.
>>> prove $ \(Forall x) (Forall y) (Forall z) -> r (x, y) .&& r (y, z) .=> tcR (x, z)
Q.E.D.

What's missing here is the check that if the transitive closure relates two elements, then they are
connected transitively in the original relation. This requirement is not axiomatizable in first order logic.
-}

-- | Create a transitive relation of a simple relation and show that transitive connections are respected.
-- We have:
--
-- >>> tcExample1
-- Q.E.D.
tcExample1 :: IO ThmResult
tcExample1 :: IO ThmResult
tcExample1 = SymbolicT IO SBool -> IO ThmResult
forall a. Provable a => a -> IO ThmResult
prove (SymbolicT IO SBool -> IO ThmResult)
-> SymbolicT IO SBool -> IO ThmResult
forall a b. (a -> b) -> a -> b
$ do
  SBV U
a :: SU <- String -> Symbolic (SBV U)
forall a. SymVal a => String -> Symbolic (SBV a)
free String
"a"
  SBV U
b :: SU <- String -> Symbolic (SBV U)
forall a. SymVal a => String -> Symbolic (SBV a)
free String
"b"
  SBV U
c :: SU <- String -> Symbolic (SBV U)
forall a. SymVal a => String -> Symbolic (SBV a)
free String
"c"

  let r :: Relation U
r   = String -> Relation U
forall a. SMTDefinable a => String -> a
uninterpret String
"R"
      tcR :: Relation U
tcR = String -> Relation U -> Relation U
forall a. SymVal a => String -> Relation a -> Relation a
mkTransitiveClosure String
"tcR" Relation U
r

  -- Add R(a, b), R(b, c), but explicitly state ~R(a, c)
  SBool -> ConstraintSet
forall a. QuantifiedBool a => a -> ConstraintSet
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> ConstraintSet) -> SBool -> ConstraintSet
forall a b. (a -> b) -> a -> b
$ Relation U
r (SBV U
a, SBV U
b)
  SBool -> ConstraintSet
forall a. QuantifiedBool a => a -> ConstraintSet
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> ConstraintSet) -> SBool -> ConstraintSet
forall a b. (a -> b) -> a -> b
$ Relation U
r (SBV U
b, SBV U
c)
  SBool -> ConstraintSet
forall a. QuantifiedBool a => a -> ConstraintSet
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> ConstraintSet) -> SBool -> ConstraintSet
forall a b. (a -> b) -> a -> b
$ SBool -> SBool
sNot (SBool -> SBool) -> SBool -> SBool
forall a b. (a -> b) -> a -> b
$ Relation U
r (SBV U
a, SBV U
c)

  -- Show that in tcR, a and c are connected
  SBool -> SymbolicT IO SBool
forall a. a -> SymbolicT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SBool -> SymbolicT IO SBool) -> SBool -> SymbolicT IO SBool
forall a b. (a -> b) -> a -> b
$ Relation U
tcR (SBV U
a, SBV U
c)

-- | Another transitive-closure example, this time we show the transitive closure is the smallest
-- relation, i.e., doesn't have extra connections. We have:
--
-- >>> tcExample2
-- Q.E.D.
tcExample2 :: IO ThmResult
tcExample2 :: IO ThmResult
tcExample2 = SymbolicT IO SBool -> IO ThmResult
forall a. Provable a => a -> IO ThmResult
prove (SymbolicT IO SBool -> IO ThmResult)
-> SymbolicT IO SBool -> IO ThmResult
forall a b. (a -> b) -> a -> b
$ do
  let r :: Relation E
r   = String -> Relation E
forall a. SMTDefinable a => String -> a
uninterpret String
"r"
      tcR :: Relation E
tcR = String -> Relation E -> Relation E
forall a. SymVal a => String -> Relation a -> Relation a
mkTransitiveClosure String
"tcR" Relation E
r

  -- Add R(A, B), ~R(A, C), ~R(B, C) then it shouldn't be the case that R(a, c)
  SBool -> ConstraintSet
forall a. QuantifiedBool a => a -> ConstraintSet
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> ConstraintSet) -> SBool -> ConstraintSet
forall a b. (a -> b) -> a -> b
$ Relation E
r (SBV E
sA, SBV E
sB)
  SBool -> ConstraintSet
forall a. QuantifiedBool a => a -> ConstraintSet
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> ConstraintSet) -> SBool -> ConstraintSet
forall a b. (a -> b) -> a -> b
$ SBool -> SBool
sNot (SBool -> SBool) -> SBool -> SBool
forall a b. (a -> b) -> a -> b
$ Relation E
r (SBV E
sA, SBV E
sC)
  SBool -> ConstraintSet
forall a. QuantifiedBool a => a -> ConstraintSet
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> ConstraintSet) -> SBool -> ConstraintSet
forall a b. (a -> b) -> a -> b
$ SBool -> SBool
sNot (SBool -> SBool) -> SBool -> SBool
forall a b. (a -> b) -> a -> b
$ Relation E
r (SBV E
sB, SBV E
sC)

  -- Show that in tcR, a and c cannot be connected
  SBool -> SymbolicT IO SBool
forall a. a -> SymbolicT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SBool -> SymbolicT IO SBool) -> SBool -> SymbolicT IO SBool
forall a b. (a -> b) -> a -> b
$ SBool -> SBool
sNot (SBool -> SBool) -> SBool -> SBool
forall a b. (a -> b) -> a -> b
$ Relation E
tcR (SBV E
sA, SBV E
sC) :: Predicate

-- | Demonstrates computing the transitive closure of existing relations. We have:
--
-- >>> tcExample3
-- Q.E.D.
tcExample3 :: IO ThmResult
tcExample3 :: IO ThmResult
tcExample3 = SymbolicT IO SBool -> IO ThmResult
forall a. Provable a => a -> IO ThmResult
prove (SymbolicT IO SBool -> IO ThmResult)
-> SymbolicT IO SBool -> IO ThmResult
forall a b. (a -> b) -> a -> b
$ do

        -- Define a relation over the type 'E', which only relates 'A' to 'B'.
        let rel :: Relation E
            rel :: Relation E
rel (SBV E, SBV E)
xy = (SBV E, SBV E)
xy (SBV E, SBV E) -> Relation E
forall a. EqSymbolic a => a -> a -> SBool
.== (SBV E
sA, SBV E
sB)

        -- Create a relation and its transitive closure, and associate it with our function:
        let tcR :: Relation E
tcR = String -> Relation E -> Relation E
forall a. SymVal a => String -> Relation a -> Relation a
mkTransitiveClosure String
"R" Relation E
rel

        -- Show that in tcR, a and c cannot be connected
        SBool -> SymbolicT IO SBool
forall a. a -> SymbolicT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SBool -> SymbolicT IO SBool) -> SBool -> SymbolicT IO SBool
forall a b. (a -> b) -> a -> b
$ SBool -> SBool
sNot (SBool -> SBool) -> SBool -> SBool
forall a b. (a -> b) -> a -> b
$ Relation E
tcR (SBV E
sA, SBV E
sC) :: Predicate