module Hermod.ReCon.Presburger.Internal.IR.DNF(DNFConjunct(..), DNFDisjunct, DNF, fromCompNF, quoteDNF) where


import           Hermod.ReCon.Common.Types (NatValue)
import           Hermod.ReCon.Integer.Polynomial.Term
import qualified Hermod.ReCon.Presburger.Formula as Rel
import           Hermod.ReCon.Presburger.Internal.IR.CompNF (CompNF)
import qualified Hermod.ReCon.Presburger.Internal.IR.CompNF as C
import           Hermod.ReCon.Presburger.Internal.IR.QuantifierFree (QuantifierFree)
import qualified Hermod.ReCon.Presburger.Internal.IR.QuantifierFree as Q

-- | A single conjunct in a DNF clause: either a strict less-than inequality
--   or a (possibly negated) divisibility atom.  All comparison relations have
--   already been reduced to @<@ (see
--   'Hermod.ReCon.Presburger.Internal.IR.CompNF.CompNF').
--
--   A 'DNF' is a disjunction (@[DNFDisjunct]@) of conjunctions
--   (@[DNFConjunct]@).  The empty disjunct list represents ⊥; a list
--   containing one empty conjunct represents ⊤.
data DNFConjunct =
     -- | i < i
     IntLt IntTerm IntTerm
     -- | ℕ⁺ \| i  (divisibility relation, first argument is a non-zero ℕ)
   | IntDiv NatValue IntTerm
     -- | ¬ (ℕ⁺ \| i)
   | IntNegDiv NatValue IntTerm deriving (Int -> DNFConjunct -> ShowS
[DNFConjunct] -> ShowS
DNFConjunct -> String
(Int -> DNFConjunct -> ShowS)
-> (DNFConjunct -> String)
-> ([DNFConjunct] -> ShowS)
-> Show DNFConjunct
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DNFConjunct -> ShowS
showsPrec :: Int -> DNFConjunct -> ShowS
$cshow :: DNFConjunct -> String
show :: DNFConjunct -> String
$cshowList :: [DNFConjunct] -> ShowS
showList :: [DNFConjunct] -> ShowS
Show, DNFConjunct -> DNFConjunct -> Bool
(DNFConjunct -> DNFConjunct -> Bool)
-> (DNFConjunct -> DNFConjunct -> Bool) -> Eq DNFConjunct
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: DNFConjunct -> DNFConjunct -> Bool
== :: DNFConjunct -> DNFConjunct -> Bool
$c/= :: DNFConjunct -> DNFConjunct -> Bool
/= :: DNFConjunct -> DNFConjunct -> Bool
Eq, Eq DNFConjunct
Eq DNFConjunct =>
(DNFConjunct -> DNFConjunct -> Ordering)
-> (DNFConjunct -> DNFConjunct -> Bool)
-> (DNFConjunct -> DNFConjunct -> Bool)
-> (DNFConjunct -> DNFConjunct -> Bool)
-> (DNFConjunct -> DNFConjunct -> Bool)
-> (DNFConjunct -> DNFConjunct -> DNFConjunct)
-> (DNFConjunct -> DNFConjunct -> DNFConjunct)
-> Ord DNFConjunct
DNFConjunct -> DNFConjunct -> Bool
DNFConjunct -> DNFConjunct -> Ordering
DNFConjunct -> DNFConjunct -> DNFConjunct
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
$ccompare :: DNFConjunct -> DNFConjunct -> Ordering
compare :: DNFConjunct -> DNFConjunct -> Ordering
$c< :: DNFConjunct -> DNFConjunct -> Bool
< :: DNFConjunct -> DNFConjunct -> Bool
$c<= :: DNFConjunct -> DNFConjunct -> Bool
<= :: DNFConjunct -> DNFConjunct -> Bool
$c> :: DNFConjunct -> DNFConjunct -> Bool
> :: DNFConjunct -> DNFConjunct -> Bool
$c>= :: DNFConjunct -> DNFConjunct -> Bool
>= :: DNFConjunct -> DNFConjunct -> Bool
$cmax :: DNFConjunct -> DNFConjunct -> DNFConjunct
max :: DNFConjunct -> DNFConjunct -> DNFConjunct
$cmin :: DNFConjunct -> DNFConjunct -> DNFConjunct
min :: DNFConjunct -> DNFConjunct -> DNFConjunct
Ord)

type DNFDisjunct = [DNFConjunct]
type DNF = [DNFDisjunct]

fromCompNF :: CompNF -> DNF
fromCompNF :: CompNF -> DNF
fromCompNF (C.Or CompNF
a CompNF
b) = CompNF -> DNF
fromCompNF CompNF
a DNF -> DNF -> DNF
forall a. [a] -> [a] -> [a]
++ CompNF -> DNF
fromCompNF CompNF
b
fromCompNF (C.And CompNF
a CompNF
b) = [[DNFConjunct]
p [DNFConjunct] -> [DNFConjunct] -> [DNFConjunct]
forall a. [a] -> [a] -> [a]
++ [DNFConjunct]
q | [DNFConjunct]
p <- CompNF -> DNF
fromCompNF CompNF
a, [DNFConjunct]
q <- CompNF -> DNF
fromCompNF CompNF
b]
fromCompNF CompNF
C.Top = [[]]
fromCompNF CompNF
C.Bottom = []
fromCompNF (C.IntLt IntTerm
i IntTerm
j) = [[IntTerm -> IntTerm -> DNFConjunct
IntLt IntTerm
i IntTerm
j]]
fromCompNF (C.IntDiv NatValue
n IntTerm
i) = [[NatValue -> IntTerm -> DNFConjunct
IntDiv NatValue
n IntTerm
i]]
fromCompNF (C.IntNegDiv NatValue
n IntTerm
i) = [[NatValue -> IntTerm -> DNFConjunct
IntNegDiv NatValue
n IntTerm
i]]

-- | Embed a DNF back into QuantifierFree.
-- [] (empty disjunct list) = ⊥
-- [[]] (one empty conjunct) = ⊤
quoteDNF :: DNF -> QuantifierFree
quoteDNF :: DNF -> QuantifierFree
quoteDNF []  = QuantifierFree
Q.Bottom
quoteDNF DNF
xss = (QuantifierFree -> QuantifierFree -> QuantifierFree)
-> [QuantifierFree] -> QuantifierFree
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 QuantifierFree -> QuantifierFree -> QuantifierFree
Q.Or (([DNFConjunct] -> QuantifierFree) -> DNF -> [QuantifierFree]
forall a b. (a -> b) -> [a] -> [b]
map [DNFConjunct] -> QuantifierFree
quoteDisjunct DNF
xss)
  where
    quoteDisjunct :: [DNFConjunct] -> QuantifierFree
quoteDisjunct [] = QuantifierFree
Q.Top
    quoteDisjunct [DNFConjunct]
cs = (QuantifierFree -> QuantifierFree -> QuantifierFree)
-> [QuantifierFree] -> QuantifierFree
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 QuantifierFree -> QuantifierFree -> QuantifierFree
Q.And ((DNFConjunct -> QuantifierFree)
-> [DNFConjunct] -> [QuantifierFree]
forall a b. (a -> b) -> [a] -> [b]
map DNFConjunct -> QuantifierFree
quoteConjunct [DNFConjunct]
cs)
    quoteConjunct :: DNFConjunct -> QuantifierFree
quoteConjunct (IntLt IntTerm
i IntTerm
j)     = BinRel -> IntTerm -> IntTerm -> QuantifierFree
Q.IntBinRel BinRel
Rel.Lt IntTerm
i IntTerm
j
    quoteConjunct (IntDiv NatValue
h IntTerm
t)    = NatValue -> IntTerm -> QuantifierFree
Q.IntDiv NatValue
h IntTerm
t
    quoteConjunct (IntNegDiv NatValue
h IntTerm
t) = QuantifierFree -> QuantifierFree
Q.Not (NatValue -> IntTerm -> QuantifierFree
Q.IntDiv NatValue
h IntTerm
t)