{-# LANGUAGE CPP #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}

{-# OPTIONS_HADDOCK not-home #-}
--------------------------------------------------------------------
-- |
-- Copyright :  © Edward Kmett 2010-2014, Johan Kiviniemi 2013
-- License   :  BSD3
-- Maintainer:  Edward Kmett <ekmett@gmail.com>
-- Stability :  experimental
-- Portability: non-portable
--
--------------------------------------------------------------------
module Ersatz.Internal.Formula
  (
  -- * Clauses
    Clause(..), clauseLiterals, fromLiteral
  -- * Formulas
  , Formula(..)
  , formulaEmpty, formulaLiteral, fromClause
  , formulaNot, formulaAnd, formulaOr, formulaXor, formulaMux
  , formulaFAS, formulaFAC
  ) where

import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet
import qualified Data.List as List (intersperse)
import Ersatz.Internal.Literal

import Data.Sequence (Seq)
import qualified Data.Sequence as Seq
import Data.Foldable (toList)

#if !(MIN_VERSION_base(4,11,0))
import Data.Semigroup (Semigroup(..))
#endif

------------------------------------------------------------------------------
-- Clauses
------------------------------------------------------------------------------

-- | A disjunction of possibly negated atoms. Negated atoms are represented
-- by negating the identifier.
newtype Clause = Clause { Clause -> IntSet
clauseSet :: IntSet }
  deriving (Clause -> Clause -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Clause -> Clause -> Bool
$c/= :: Clause -> Clause -> Bool
== :: Clause -> Clause -> Bool
$c== :: Clause -> Clause -> Bool
Eq, Eq Clause
Clause -> Clause -> Bool
Clause -> Clause -> Ordering
Clause -> Clause -> Clause
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
min :: Clause -> Clause -> Clause
$cmin :: Clause -> Clause -> Clause
max :: Clause -> Clause -> Clause
$cmax :: Clause -> Clause -> Clause
>= :: Clause -> Clause -> Bool
$c>= :: Clause -> Clause -> Bool
> :: Clause -> Clause -> Bool
$c> :: Clause -> Clause -> Bool
<= :: Clause -> Clause -> Bool
$c<= :: Clause -> Clause -> Bool
< :: Clause -> Clause -> Bool
$c< :: Clause -> Clause -> Bool
compare :: Clause -> Clause -> Ordering
$ccompare :: Clause -> Clause -> Ordering
Ord)

-- | Extract the (possibly negated) atoms referenced by a 'Clause'.
clauseLiterals :: Clause -> [Literal]
clauseLiterals :: Clause -> [Literal]
clauseLiterals (Clause IntSet
is) = Int -> Literal
Literal forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IntSet -> [Int]
IntSet.toList IntSet
is

instance Semigroup Clause where
  Clause IntSet
x <> :: Clause -> Clause -> Clause
<> Clause IntSet
y = IntSet -> Clause
Clause (IntSet
x forall a. Semigroup a => a -> a -> a
<> IntSet
y)

instance Monoid Clause where
  mempty :: Clause
mempty = IntSet -> Clause
Clause forall a. Monoid a => a
mempty
#if !(MIN_VERSION_base(4,11,0))
  mappend = (<>)
#endif

fromLiteral :: Literal -> Clause
fromLiteral :: Literal -> Clause
fromLiteral Literal
l = Clause { clauseSet :: IntSet
clauseSet = Int -> IntSet
IntSet.singleton forall a b. (a -> b) -> a -> b
$ Literal -> Int
literalId Literal
l }

------------------------------------------------------------------------------
-- Formulas
------------------------------------------------------------------------------

-- | A conjunction of clauses
newtype Formula = Formula { Formula -> Seq Clause
formulaSet :: Seq Clause }
  deriving (Formula -> Formula -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Formula -> Formula -> Bool
$c/= :: Formula -> Formula -> Bool
== :: Formula -> Formula -> Bool
$c== :: Formula -> Formula -> Bool
Eq, Eq Formula
Formula -> Formula -> Bool
Formula -> Formula -> Ordering
Formula -> Formula -> Formula
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
min :: Formula -> Formula -> Formula
$cmin :: Formula -> Formula -> Formula
max :: Formula -> Formula -> Formula
$cmax :: Formula -> Formula -> Formula
>= :: Formula -> Formula -> Bool
$c>= :: Formula -> Formula -> Bool
> :: Formula -> Formula -> Bool
$c> :: Formula -> Formula -> Bool
<= :: Formula -> Formula -> Bool
$c<= :: Formula -> Formula -> Bool
< :: Formula -> Formula -> Bool
$c< :: Formula -> Formula -> Bool
compare :: Formula -> Formula -> Ordering
$ccompare :: Formula -> Formula -> Ordering
Ord)

instance Semigroup Formula where
  Formula Seq Clause
x <> :: Formula -> Formula -> Formula
<> Formula Seq Clause
y = Seq Clause -> Formula
Formula (Seq Clause
x forall a. Semigroup a => a -> a -> a
<> Seq Clause
y)

instance Monoid Formula where
  mempty :: Formula
mempty = Seq Clause -> Formula
Formula forall a. Monoid a => a
mempty
#if !(MIN_VERSION_base(4,11,0))
  mappend = (<>)
#endif

instance Show Formula where
  showsPrec :: Int -> Formula -> ShowS
showsPrec Int
p = Bool -> ShowS -> ShowS
showParen (Int
p forall a. Ord a => a -> a -> Bool
> Int
2) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) forall a. a -> a
id
              forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> [a] -> [a]
List.intersperse (String -> ShowS
showString String
" & ") forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (forall a. Show a => Int -> a -> ShowS
showsPrec Int
3)
              forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> [a]
Data.Foldable.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. Formula -> Seq Clause
formulaSet

instance Show Clause where
  showsPrec :: Int -> Clause -> ShowS
showsPrec Int
p = Bool -> ShowS -> ShowS
showParen (Int
p forall a. Ord a => a -> a -> Bool
> Int
1) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) forall a. a -> a
id
              forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> [a] -> [a]
List.intersperse (String -> ShowS
showString String
" | ") forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (forall a. Show a => Int -> a -> ShowS
showsPrec Int
2)
              forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntSet -> [Int]
IntSet.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> IntSet
clauseSet


-- | A formula with no clauses
formulaEmpty :: Formula
formulaEmpty :: Formula
formulaEmpty = forall a. Monoid a => a
mempty

-- | Assert a literal
formulaLiteral :: Literal -> Formula
formulaLiteral :: Literal -> Formula
formulaLiteral (Literal Int
l) = Clause -> Formula
fromClause (IntSet -> Clause
Clause (Int -> IntSet
IntSet.singleton Int
l))

fromClause :: Clause -> Formula
fromClause :: Clause -> Formula
fromClause Clause
c = Formula { formulaSet :: Seq Clause
formulaSet = forall a. a -> Seq a
Seq.singleton Clause
c }


-- | The boolean /not/ operation
--
-- Derivation of the Tseitin transformation:
--
-- @
-- O ≡ ¬A
-- (O → ¬A) & (¬O → A)
-- (¬O | ¬A) & (O | A)
-- @
formulaNot :: Literal  -- ^ Output
           -> Literal  -- ^ Input
           -> Formula
{-# inlineable formulaNot #-}
formulaNot :: Literal -> Literal -> Formula
formulaNot (Literal Int
out) (Literal Int
inp) = [[Int]] -> Formula
formulaFromList [[Int]]
cls
  where
    cls :: [[Int]]
cls = [ [-Int
out, -Int
inp], [Int
out, Int
inp] ]

-- | The boolean /and/ operation
--
-- Derivation of the Tseitin transformation:
--
-- @
-- O ≡ (A & B & C)
-- (O → (A & B & C)) & (¬O → ¬(A & B & C))
-- (¬O | (A & B & C)) & (O | ¬(A & B & C))
-- (¬O | A) & (¬O | B) & (¬O | C) & (O | ¬A | ¬B | ¬C)
-- @
formulaAnd :: Literal    -- ^ Output
           -> [Literal]  -- ^ Inputs
           -> Formula
{-# inlineable formulaAnd #-}
formulaAnd :: Literal -> [Literal] -> Formula
formulaAnd (Literal Int
out) [Literal]
inpLs = [[Int]] -> Formula
formulaFromList [[Int]]
cls
  where
    cls :: [[Int]]
cls = (Int
out forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map forall a. Num a => a -> a
negate [Int]
inps) forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map (\Int
inp -> [-Int
out, Int
inp]) [Int]
inps
    inps :: [Int]
inps = forall a b. (a -> b) -> [a] -> [b]
map Literal -> Int
literalId [Literal]
inpLs

-- | The boolean /or/ operation
--
-- Derivation of the Tseitin transformation:
--
-- @
-- O ≡ (A | B | C)
-- (O → (A | B | C)) & (¬O → ¬(A | B | C))
-- (¬O | (A | B | C)) & (O | ¬(A | B | C))
-- (¬O | A | B | C) & (O | (¬A & ¬B & ¬C))
-- (¬O | A | B | C) & (O | ¬A) & (O | ¬B) & (O | ¬C)
-- @
formulaOr :: Literal    -- ^ Output
          -> [Literal]  -- ^ Inputs
          -> Formula
{-# inlineable formulaOr #-}
formulaOr :: Literal -> [Literal] -> Formula
formulaOr (Literal Int
out) [Literal]
inpLs = [[Int]] -> Formula
formulaFromList [[Int]]
cls
  where
    cls :: [[Int]]
cls = (-Int
out forall a. a -> [a] -> [a]
: [Int]
inps)
        forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map (\Int
inp -> [Int
out, -Int
inp]) [Int]
inps
    inps :: [Int]
inps = forall a b. (a -> b) -> [a] -> [b]
map Literal -> Int
literalId [Literal]
inpLs

-- | The boolean /xor/ operation
--
-- Derivation of the Tseitin transformation:
--
-- @
-- O ≡ A ⊕ B
-- O ≡ ((¬A & B) | (A & ¬B))
-- (O → ((¬A & B) | (A & ¬B))) & (¬O → ¬((¬A & B) | (A & ¬B)))
-- @
--
-- Left hand side:
--
-- @
-- O → ((¬A & B) | (A & ¬B))
-- ¬O | ((¬A & B) | (A & ¬B))
-- ¬O | ((¬A | A) & (¬A | ¬B) & (A | B) & (¬B | B))
-- ¬O | ((¬A | ¬B) & (A | B))
-- (¬O | ¬A | ¬B) & (¬O | A | B)
-- @
--
-- Right hand side:
--
-- @
-- ¬O → ¬((¬A & B) | (A & ¬B))
-- O | ¬((¬A & B) | (A & ¬B))
-- O | (¬(¬A & B) & ¬(A & ¬B))
-- O | ((A | ¬B) & (¬A | B))
-- (O | ¬A | B) & (O | A | ¬B)
-- @
--
-- Result:
--
-- @
-- (¬O | ¬A | ¬B) & (¬O | A | B) & (O | ¬A | B) & (O | A | ¬B)
-- @
formulaXor :: Literal  -- ^ Output
           -> Literal  -- ^ Input
           -> Literal  -- ^ Input
           -> Formula
{-# inlineable formulaXor #-}
formulaXor :: Literal -> Literal -> Literal -> Formula
formulaXor (Literal Int
out) (Literal Int
inpA) (Literal Int
inpB) = [[Int]] -> Formula
formulaFromList [[Int]]
cls
  where
    cls :: [[Int]]
cls = [ [-Int
out, -Int
inpA, -Int
inpB]
          , [-Int
out,  Int
inpA,  Int
inpB]
          , [ Int
out, -Int
inpA,  Int
inpB]
          , [ Int
out,  Int
inpA, -Int
inpB]
          ]

-- | The boolean /else-then-if/ or /mux/ operation
--
-- Derivation of the Tseitin transformation:
--
-- @
-- O ≡ (F & ¬P) | (T & P)
-- (O → ((F & ¬P) | (T & P))) & (¬O → ¬((F & ¬P) | (T & P)))
-- @
--
-- Left hand side:
--
-- @
-- O → ((F & ¬P) | (T & P))
-- ¬O | ((F & ¬P) | (T & P))
-- ¬O | ((F | T) & (F | P) & (T | ¬P) & (¬P | P))
-- ¬O | ((F | T) & (F | P) & (T | ¬P))
-- (¬O | F | T) & (¬O | F | P) & (¬O | T | ¬P)
-- @
--
-- Right hand side:
--
-- @
-- ¬O → ¬((F & ¬P) | (T & P))
-- O | ¬((F & ¬P) | (T & P))
-- O | (¬(F & ¬P) & ¬(T & P))
-- O | ((¬F | P) & (¬T | ¬P))
-- (O | ¬F | P) & (O | ¬T | ¬P)
-- @
--
-- Result:
--
-- @
-- (¬O | F | T) & (¬O | F | P) & (¬O | T | ¬P) & (O | ¬F | P) & (O | ¬T | ¬P)
-- @
formulaMux :: Literal  -- ^ Output
           -> Literal  -- ^ False branch
           -> Literal  -- ^ True branch
           -> Literal  -- ^ Predicate/selector
           -> Formula
{-# inlineable formulaMux #-}
-- | with redundant clauses, cf. discussion in
--   Een and Sorensen, Translating Pseudo Boolean Constraints ..., p. 7
-- http://minisat.se/Papers.html
formulaMux :: Literal -> Literal -> Literal -> Literal -> Formula
formulaMux (Literal Int
x) (Literal Int
f) (Literal Int
t) (Literal Int
s) =
  [[Int]] -> Formula
formulaFromList [[Int]]
cls
  where
    cls :: [[Int]]
cls = [ [-Int
s, -Int
t,  Int
x], [ Int
s, -Int
f,  Int
x], {- red -} [-Int
t, -Int
f,  Int
x]
          , [-Int
s,  Int
t, -Int
x], [ Int
s,  Int
f, -Int
x], {- red -} [ Int
t,  Int
f, -Int
x]
          ]

formulaFAS :: Literal -> Literal -> Literal -> Literal -> Formula
formulaFAS :: Literal -> Literal -> Literal -> Literal -> Formula
formulaFAS (Literal Int
x) (Literal Int
a) (Literal Int
b) (Literal Int
c) =
  [[Int]] -> Formula
formulaFromList [[Int]]
cls
  where
    cls :: [[Int]]
cls =
      [ [ Int
a,  Int
b,  Int
c, -Int
x], [-Int
a, -Int
b, -Int
c, Int
x]
      , [ Int
a, -Int
b, -Int
c, -Int
x], [-Int
a,  Int
b,  Int
c, Int
x]
      , [-Int
a,  Int
b, -Int
c, -Int
x], [ Int
a, -Int
b,  Int
c, Int
x]
      , [-Int
a, -Int
b,  Int
c, -Int
x], [ Int
a,  Int
b, -Int
c, Int
x]
      ]

formulaFAC :: Literal -> Literal -> Literal -> Literal -> Formula
formulaFAC :: Literal -> Literal -> Literal -> Literal -> Formula
formulaFAC (Literal Int
x) (Literal Int
a) (Literal Int
b) (Literal Int
c) =
  [[Int]] -> Formula
formulaFromList [[Int]]
cls
  where
    cls :: [[Int]]
cls =
      [ [ -Int
b, -Int
c, Int
x], [Int
b, Int
c, -Int
x]
      , [ -Int
a, -Int
c, Int
x], [Int
a, Int
c, -Int
x]
      , [ -Int
a, -Int
b, Int
x], [Int
a, Int
b, -Int
x]
      ]

formulaFromList :: [[Int]] -> Formula
{-# inline formulaFromList #-}
formulaFromList :: [[Int]] -> Formula
formulaFromList = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (  Clause -> Formula
fromClause forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntSet -> Clause
Clause forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Int] -> IntSet
IntSet.fromList )