{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE MultiParamTypeClasses #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.Data.FOL.Formula
-- Copyright   :  (c) Masahiro Sakai 2011-2015
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  non-portable
--
-- Formula of first order logic.
--
-----------------------------------------------------------------------------
module ToySolver.Data.FOL.Formula
  (
  -- * Overloaded operations for formula.
    module ToySolver.Data.Boolean

  -- * Concrete formula
  , Formula (..)
  , pushNot
  ) where

import qualified Data.IntSet as IS

import ToySolver.Data.Boolean
import ToySolver.Data.IntVar

-- ---------------------------------------------------------------------------

-- | formulas of first order logic
data Formula a
    = T
    | F
    | Atom a
    | And (Formula a) (Formula a)
    | Or (Formula a) (Formula a)
    | Not (Formula a)
    | Imply (Formula a) (Formula a)
    | Equiv (Formula a) (Formula a)
    | Forall Var (Formula a)
    | Exists Var (Formula a)
    deriving (Int -> Formula a -> ShowS
forall a. Show a => Int -> Formula a -> ShowS
forall a. Show a => [Formula a] -> ShowS
forall a. Show a => Formula a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Formula a] -> ShowS
$cshowList :: forall a. Show a => [Formula a] -> ShowS
show :: Formula a -> String
$cshow :: forall a. Show a => Formula a -> String
showsPrec :: Int -> Formula a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Formula a -> ShowS
Show, Formula a -> Formula a -> Bool
forall a. Eq a => Formula a -> Formula a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Formula a -> Formula a -> Bool
$c/= :: forall a. Eq a => Formula a -> Formula a -> Bool
== :: Formula a -> Formula a -> Bool
$c== :: forall a. Eq a => Formula a -> Formula a -> Bool
Eq, Formula a -> Formula a -> Ordering
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {a}. Ord a => Eq (Formula a)
forall a. Ord a => Formula a -> Formula a -> Bool
forall a. Ord a => Formula a -> Formula a -> Ordering
forall a. Ord a => Formula a -> Formula a -> Formula a
min :: Formula a -> Formula a -> Formula a
$cmin :: forall a. Ord a => Formula a -> Formula a -> Formula a
max :: Formula a -> Formula a -> Formula a
$cmax :: forall a. Ord a => Formula a -> Formula a -> Formula a
>= :: Formula a -> Formula a -> Bool
$c>= :: forall a. Ord a => Formula a -> Formula a -> Bool
> :: Formula a -> Formula a -> Bool
$c> :: forall a. Ord a => Formula a -> Formula a -> Bool
<= :: Formula a -> Formula a -> Bool
$c<= :: forall a. Ord a => Formula a -> Formula a -> Bool
< :: Formula a -> Formula a -> Bool
$c< :: forall a. Ord a => Formula a -> Formula a -> Bool
compare :: Formula a -> Formula a -> Ordering
$ccompare :: forall a. Ord a => Formula a -> Formula a -> Ordering
Ord)

instance Variables a => Variables (Formula a) where
  vars :: Formula a -> VarSet
vars Formula a
T = VarSet
IS.empty
  vars Formula a
F = VarSet
IS.empty
  vars (Atom a
a) = forall a. Variables a => a -> VarSet
vars a
a
  vars (And Formula a
a Formula a
b) = forall a. Variables a => a -> VarSet
vars Formula a
a VarSet -> VarSet -> VarSet
`IS.union` forall a. Variables a => a -> VarSet
vars Formula a
b
  vars (Or Formula a
a Formula a
b) = forall a. Variables a => a -> VarSet
vars Formula a
a VarSet -> VarSet -> VarSet
`IS.union` forall a. Variables a => a -> VarSet
vars Formula a
b
  vars (Not Formula a
a) = forall a. Variables a => a -> VarSet
vars Formula a
a
  vars (Imply Formula a
a Formula a
b) = forall a. Variables a => a -> VarSet
vars Formula a
a VarSet -> VarSet -> VarSet
`IS.union` forall a. Variables a => a -> VarSet
vars Formula a
b
  vars (Equiv Formula a
a Formula a
b) = forall a. Variables a => a -> VarSet
vars Formula a
a VarSet -> VarSet -> VarSet
`IS.union` forall a. Variables a => a -> VarSet
vars Formula a
b
  vars (Forall Int
v Formula a
a) = Int -> VarSet -> VarSet
IS.delete Int
v (forall a. Variables a => a -> VarSet
vars Formula a
a)
  vars (Exists Int
v Formula a
a) = Int -> VarSet -> VarSet
IS.delete Int
v (forall a. Variables a => a -> VarSet
vars Formula a
a)

instance Complement (Formula a) where
  notB :: Formula a -> Formula a
notB = forall a. Formula a -> Formula a
Not

instance MonotoneBoolean (Formula c) where
  true :: Formula c
true  = forall c. Formula c
T
  false :: Formula c
false = forall c. Formula c
F
  .&&. :: Formula c -> Formula c -> Formula c
(.&&.) = forall c. Formula c -> Formula c -> Formula c
And
  .||. :: Formula c -> Formula c -> Formula c
(.||.) = forall c. Formula c -> Formula c -> Formula c
Or

instance IfThenElse (Formula c) (Formula c) where
  ite :: Formula c -> Formula c -> Formula c -> Formula c
ite = forall a. Boolean a => a -> a -> a -> a
iteBoolean

instance Boolean (Formula c) where
  .=>. :: Formula c -> Formula c -> Formula c
(.=>.)  = forall c. Formula c -> Formula c -> Formula c
Imply
  .<=>. :: Formula c -> Formula c -> Formula c
(.<=>.) = forall c. Formula c -> Formula c -> Formula c
Equiv

-- | convert a formula into negation normal form
pushNot :: Complement a => Formula a -> Formula a
pushNot :: forall a. Complement a => Formula a -> Formula a
pushNot Formula a
T = forall c. Formula c
F
pushNot Formula a
F = forall c. Formula c
T
pushNot (Atom a
a) = forall a. a -> Formula a
Atom forall a b. (a -> b) -> a -> b
$ forall a. Complement a => a -> a
notB a
a
pushNot (And Formula a
a Formula a
b) = forall a. Complement a => Formula a -> Formula a
pushNot Formula a
a forall a. MonotoneBoolean a => a -> a -> a
.||. forall a. Complement a => Formula a -> Formula a
pushNot Formula a
b
pushNot (Or Formula a
a Formula a
b) = forall a. Complement a => Formula a -> Formula a
pushNot Formula a
a forall a. MonotoneBoolean a => a -> a -> a
.&&. forall a. Complement a => Formula a -> Formula a
pushNot Formula a
b
pushNot (Not Formula a
a) = Formula a
a
pushNot (Imply Formula a
a Formula a
b) = Formula a
a forall a. MonotoneBoolean a => a -> a -> a
.&&. forall a. Complement a => Formula a -> Formula a
pushNot Formula a
b
pushNot (Equiv Formula a
a Formula a
b) = Formula a
a forall a. MonotoneBoolean a => a -> a -> a
.&&. forall a. Complement a => Formula a -> Formula a
pushNot Formula a
b forall a. MonotoneBoolean a => a -> a -> a
.||. Formula a
b forall a. MonotoneBoolean a => a -> a -> a
.&&. forall a. Complement a => Formula a -> Formula a
pushNot Formula a
a
pushNot (Forall Int
v Formula a
a) = forall a. Int -> Formula a -> Formula a
Exists Int
v (forall a. Complement a => Formula a -> Formula a
pushNot Formula a
a)
pushNot (Exists Int
v Formula a
a) = forall a. Int -> Formula a -> Formula a
Forall Int
v (forall a. Complement a => Formula a -> Formula a
pushNot Formula a
a)