-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.Uninterpreted.Deduce
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Demonstrates uninterpreted sorts and how they can be used for deduction.
-- This example is inspired by the discussion at <http://stackoverflow.com/questions/10635783/using-axioms-for-deductions-in-z3>,
-- essentially showing how to show the required deduction using SBV.
-----------------------------------------------------------------------------

{-# LANGUAGE DeriveAnyClass     #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell    #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.Uninterpreted.Deduce where

import Data.SBV

-- we will have our own "uninterpreted" functions corresponding
-- to not/or/and, so hide their Prelude counterparts.
import Prelude hiding (not, or, and)

-----------------------------------------------------------------------------
-- * Representing uninterpreted booleans
-----------------------------------------------------------------------------

-- | The uninterpreted sort 'B', corresponding to the carrier.
data B

-- | Make this sort uninterpreted. This splice will automatically introduce
-- the type 'SB' into the environment, as a synonym for 'SBV' 'B'.
mkUninterpretedSort ''B

-----------------------------------------------------------------------------
-- * Uninterpreted connectives over 'B'
-----------------------------------------------------------------------------

-- | Uninterpreted logical connective 'and'
and :: SB -> SB -> SB
and :: SB -> SB -> SB
and = String -> SB -> SB -> SB
forall a. SMTDefinable a => String -> a
uninterpret String
"AND"

-- | Uninterpreted logical connective 'or'
or :: SB -> SB -> SB
or :: SB -> SB -> SB
or  = String -> SB -> SB -> SB
forall a. SMTDefinable a => String -> a
uninterpret String
"OR"

-- | Uninterpreted logical connective 'not'
not :: SB -> SB
not :: SB -> SB
not = String -> SB -> SB
forall a. SMTDefinable a => String -> a
uninterpret String
"NOT"

-----------------------------------------------------------------------------
-- * Demonstrated deduction
-----------------------------------------------------------------------------

-- | Proves the equivalence @NOT (p OR (q AND r)) == (NOT p AND NOT q) OR (NOT p AND NOT r)@,
-- following from the axioms we have specified above. We have:
--
-- >>> test
-- Q.E.D.
test :: IO ThmResult
test :: IO ThmResult
test = 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 (Forall (ZonkAny 0) B
 -> Forall (ZonkAny 1) B -> Forall (ZonkAny 2) B -> SBool)
-> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain ((Forall (ZonkAny 0) B
  -> Forall (ZonkAny 1) B -> Forall (ZonkAny 2) B -> SBool)
 -> SymbolicT IO ())
-> (Forall (ZonkAny 0) B
    -> Forall (ZonkAny 1) B -> Forall (ZonkAny 2) B -> SBool)
-> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ \(Forall SB
p) (Forall SB
q) (Forall SB
r) -> (SB
p SB -> SB -> SB
`or` SB
q) SB -> SB -> SB
`and` (SB
p SB -> SB -> SB
`or` SB
r) SB -> SB -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SB
p SB -> SB -> SB
`or` (SB
q SB -> SB -> SB
`and` SB
r)
                  (Forall (ZonkAny 3) B -> Forall (ZonkAny 4) B -> SBool)
-> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain ((Forall (ZonkAny 3) B -> Forall (ZonkAny 4) B -> SBool)
 -> SymbolicT IO ())
-> (Forall (ZonkAny 3) B -> Forall (ZonkAny 4) B -> SBool)
-> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ \(Forall SB
p) (Forall SB
q)            -> SB -> SB
not (SB
p SB -> SB -> SB
`or` SB
q) SB -> SB -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SB -> SB
not SB
p SB -> SB -> SB
`and` SB -> SB
not SB
q
                  (Forall (ZonkAny 5) B -> SBool) -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain ((Forall (ZonkAny 5) B -> SBool) -> SymbolicT IO ())
-> (Forall (ZonkAny 5) B -> SBool) -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ \(Forall SB
p)                       -> SB -> SB
not (SB -> SB
not SB
p) SB -> SB -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SB
p
                  p <- String -> Symbolic SB
forall a. SymVal a => String -> Symbolic (SBV a)
free String
"p"
                  q <- free "q"
                  r <- free "r"
                  return $   not (p `or` (q `and` r))
                         .== (not p `and` not q) `or` (not p `and` not r)

-- Hlint gets confused and thinks the use of @not@ above is from the prelude. Sigh.
{- HLint ignore test "Redundant not" -}