-----------------------------------------------------------------------------
-- |
-- 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 :: SBV B -> SBV B -> SBV B
and = String -> SBV B -> SBV B -> SBV B
forall a. Uninterpreted a => String -> a
uninterpret String
"AND"

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

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

-----------------------------------------------------------------------------
-- * Axioms of the logical system
-----------------------------------------------------------------------------

-- | Distributivity of OR over AND, as an axiom in terms of
-- the uninterpreted functions we have introduced. Note how
-- variables range over the uninterpreted sort 'B'.
ax1 :: [String]
ax1 :: [String]
ax1 = [ String
"(assert (forall ((p B) (q B) (r B))"
      , String
"   (= (AND (OR p q) (OR p r))"
      , String
"      (OR p (AND q r)))))"
      ]

-- | One of De Morgan's laws, again as an axiom in terms
-- of our uninterpeted logical connectives.
ax2 :: [String]
ax2 :: [String]
ax2 = [ String
"(assert (forall ((p B) (q B))"
      , String
"   (= (NOT (OR p q))"
      , String
"      (AND (NOT p) (NOT q)))))"
      ]

-- | Double negation axiom, similar to the above.
ax3 :: [String]
ax3 :: [String]
ax3 = [String
"(assert (forall ((p B)) (= (NOT (NOT p)) p)))"]

-----------------------------------------------------------------------------
-- * 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 String -> [String] -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => String -> [String] -> m ()
addAxiom String
"OR distributes over AND" [String]
ax1
                  String -> [String] -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => String -> [String] -> m ()
addAxiom String
"de Morgan"               [String]
ax2
                  String -> [String] -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => String -> [String] -> m ()
addAxiom String
"double negation"         [String]
ax3
                  SBV B
p <- String -> Symbolic (SBV B)
forall a. SymVal a => String -> Symbolic (SBV a)
free String
"p"
                  SBV B
q <- String -> Symbolic (SBV B)
forall a. SymVal a => String -> Symbolic (SBV a)
free String
"q"
                  SBV B
r <- String -> Symbolic (SBV B)
forall a. SymVal a => String -> Symbolic (SBV a)
free String
"r"
                  SBool -> SymbolicT IO SBool
forall (m :: * -> *) a. Monad m => a -> m a
return (SBool -> SymbolicT IO SBool) -> SBool -> SymbolicT IO SBool
forall a b. (a -> b) -> a -> b
$   SBV B -> SBV B
not (SBV B
p SBV B -> SBV B -> SBV B
`or` (SBV B
q SBV B -> SBV B -> SBV B
`and` SBV B
r))
                         SBV B -> SBV B -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SBV B -> SBV B
not SBV B
p SBV B -> SBV B -> SBV B
`and` SBV B -> SBV B
not SBV B
q) SBV B -> SBV B -> SBV B
`or` (SBV B -> SBV B
not SBV B
p SBV B -> SBV B -> SBV B
`and` SBV B -> SBV B
not SBV B
r)