module Hermod.ReCon.Presburger.Internal.IR.AffineDNF(IntLtForm(..), IntDivForm(..), AffineDNFConjunct(..), AffineDNFDisjunct, AffineDNF, fromDNF) where
import           Hermod.ReCon.Common.Types (NatValue)
import           Hermod.ReCon.Integer.Polynomial.Term
import           Hermod.ReCon.Integer.Polynomial.Value
import qualified Hermod.ReCon.Integer.Polynomial.Value as Value
import           Hermod.ReCon.Presburger.Internal.IR.DNF (DNF, DNFConjunct)
import qualified Hermod.ReCon.Presburger.Internal.IR.DNF as DNF

import qualified Data.Map.Strict as Map
import           Data.Maybe (fromMaybe)

-- | A @<@-atom in a DNF conjunct classified by how the variable @x@ being
--   eliminated appears in it.  Coefficients on @x@ may be non-unit positive
--   naturals.
data IntLtForm =
    -- | h · x < i, where h ∈ ℕ⁺, i ∈ ℤ[x̄\{x}]
    LtL NatValue IntTerm
    -- | i < h · x, where h ∈ ℕ⁺, i ∈ ℤ⟦x̄\{x}⟧
  | LtR IntTerm NatValue
    -- i < j, where i, j ∈ ℤ⟦x̄\{x}⟧
  | LtC IntTerm IntTerm deriving (Int -> IntLtForm -> ShowS
[IntLtForm] -> ShowS
IntLtForm -> String
(Int -> IntLtForm -> ShowS)
-> (IntLtForm -> String)
-> ([IntLtForm] -> ShowS)
-> Show IntLtForm
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> IntLtForm -> ShowS
showsPrec :: Int -> IntLtForm -> ShowS
$cshow :: IntLtForm -> String
show :: IntLtForm -> String
$cshowList :: [IntLtForm] -> ShowS
showList :: [IntLtForm] -> ShowS
Show, IntLtForm -> IntLtForm -> Bool
(IntLtForm -> IntLtForm -> Bool)
-> (IntLtForm -> IntLtForm -> Bool) -> Eq IntLtForm
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: IntLtForm -> IntLtForm -> Bool
== :: IntLtForm -> IntLtForm -> Bool
$c/= :: IntLtForm -> IntLtForm -> Bool
/= :: IntLtForm -> IntLtForm -> Bool
Eq, Eq IntLtForm
Eq IntLtForm =>
(IntLtForm -> IntLtForm -> Ordering)
-> (IntLtForm -> IntLtForm -> Bool)
-> (IntLtForm -> IntLtForm -> Bool)
-> (IntLtForm -> IntLtForm -> Bool)
-> (IntLtForm -> IntLtForm -> Bool)
-> (IntLtForm -> IntLtForm -> IntLtForm)
-> (IntLtForm -> IntLtForm -> IntLtForm)
-> Ord IntLtForm
IntLtForm -> IntLtForm -> Bool
IntLtForm -> IntLtForm -> Ordering
IntLtForm -> IntLtForm -> IntLtForm
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 :: IntLtForm -> IntLtForm -> Ordering
compare :: IntLtForm -> IntLtForm -> Ordering
$c< :: IntLtForm -> IntLtForm -> Bool
< :: IntLtForm -> IntLtForm -> Bool
$c<= :: IntLtForm -> IntLtForm -> Bool
<= :: IntLtForm -> IntLtForm -> Bool
$c> :: IntLtForm -> IntLtForm -> Bool
> :: IntLtForm -> IntLtForm -> Bool
$c>= :: IntLtForm -> IntLtForm -> Bool
>= :: IntLtForm -> IntLtForm -> Bool
$cmax :: IntLtForm -> IntLtForm -> IntLtForm
max :: IntLtForm -> IntLtForm -> IntLtForm
$cmin :: IntLtForm -> IntLtForm -> IntLtForm
min :: IntLtForm -> IntLtForm -> IntLtForm
Ord)

-- | A divisibility atom classified by whether @x@ appears in it.
data IntDivForm =
    -- | (h | k · x + i), where h, k ∈ ℕ⁺, i ∈ ℤ[x̄\{x}]
    DivL NatValue NatValue IntTerm
    -- | (h | i), where h ∈ ℕ⁺, i ∈ ℤ[x̄\{x}]
  | DivC NatValue IntTerm deriving (Int -> IntDivForm -> ShowS
[IntDivForm] -> ShowS
IntDivForm -> String
(Int -> IntDivForm -> ShowS)
-> (IntDivForm -> String)
-> ([IntDivForm] -> ShowS)
-> Show IntDivForm
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> IntDivForm -> ShowS
showsPrec :: Int -> IntDivForm -> ShowS
$cshow :: IntDivForm -> String
show :: IntDivForm -> String
$cshowList :: [IntDivForm] -> ShowS
showList :: [IntDivForm] -> ShowS
Show, IntDivForm -> IntDivForm -> Bool
(IntDivForm -> IntDivForm -> Bool)
-> (IntDivForm -> IntDivForm -> Bool) -> Eq IntDivForm
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: IntDivForm -> IntDivForm -> Bool
== :: IntDivForm -> IntDivForm -> Bool
$c/= :: IntDivForm -> IntDivForm -> Bool
/= :: IntDivForm -> IntDivForm -> Bool
Eq, Eq IntDivForm
Eq IntDivForm =>
(IntDivForm -> IntDivForm -> Ordering)
-> (IntDivForm -> IntDivForm -> Bool)
-> (IntDivForm -> IntDivForm -> Bool)
-> (IntDivForm -> IntDivForm -> Bool)
-> (IntDivForm -> IntDivForm -> Bool)
-> (IntDivForm -> IntDivForm -> IntDivForm)
-> (IntDivForm -> IntDivForm -> IntDivForm)
-> Ord IntDivForm
IntDivForm -> IntDivForm -> Bool
IntDivForm -> IntDivForm -> Ordering
IntDivForm -> IntDivForm -> IntDivForm
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 :: IntDivForm -> IntDivForm -> Ordering
compare :: IntDivForm -> IntDivForm -> Ordering
$c< :: IntDivForm -> IntDivForm -> Bool
< :: IntDivForm -> IntDivForm -> Bool
$c<= :: IntDivForm -> IntDivForm -> Bool
<= :: IntDivForm -> IntDivForm -> Bool
$c> :: IntDivForm -> IntDivForm -> Bool
> :: IntDivForm -> IntDivForm -> Bool
$c>= :: IntDivForm -> IntDivForm -> Bool
>= :: IntDivForm -> IntDivForm -> Bool
$cmax :: IntDivForm -> IntDivForm -> IntDivForm
max :: IntDivForm -> IntDivForm -> IntDivForm
$cmin :: IntDivForm -> IntDivForm -> IntDivForm
min :: IntDivForm -> IntDivForm -> IntDivForm
Ord)

-- | A DNF conjunct in affine form: each atom has been rewritten so that the
--   variable @x@ being eliminated appears at most once, with its coefficient
--   explicit.  An 'AffineDNF' is a @[AffineDNFDisjunct]@ (disjunction) of
--   @[AffineDNFConjunct]@ (conjunction).
--   Produced from 'Hermod.ReCon.Presburger.Internal.IR.DNF.DNF' by 'fromDNF'.
data AffineDNFConjunct =
     -- | h · x < i | i < h · x | i < j
     IntLt IntLtForm
     -- | (h | k · x + i) | (h | i)
   | IntDiv IntDivForm
     -- | ¬ (h | k · x + i) | ¬ (h | i)
   | IntNegDiv IntDivForm
   deriving (Int -> AffineDNFConjunct -> ShowS
[AffineDNFConjunct] -> ShowS
AffineDNFConjunct -> String
(Int -> AffineDNFConjunct -> ShowS)
-> (AffineDNFConjunct -> String)
-> ([AffineDNFConjunct] -> ShowS)
-> Show AffineDNFConjunct
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> AffineDNFConjunct -> ShowS
showsPrec :: Int -> AffineDNFConjunct -> ShowS
$cshow :: AffineDNFConjunct -> String
show :: AffineDNFConjunct -> String
$cshowList :: [AffineDNFConjunct] -> ShowS
showList :: [AffineDNFConjunct] -> ShowS
Show, AffineDNFConjunct -> AffineDNFConjunct -> Bool
(AffineDNFConjunct -> AffineDNFConjunct -> Bool)
-> (AffineDNFConjunct -> AffineDNFConjunct -> Bool)
-> Eq AffineDNFConjunct
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: AffineDNFConjunct -> AffineDNFConjunct -> Bool
== :: AffineDNFConjunct -> AffineDNFConjunct -> Bool
$c/= :: AffineDNFConjunct -> AffineDNFConjunct -> Bool
/= :: AffineDNFConjunct -> AffineDNFConjunct -> Bool
Eq, Eq AffineDNFConjunct
Eq AffineDNFConjunct =>
(AffineDNFConjunct -> AffineDNFConjunct -> Ordering)
-> (AffineDNFConjunct -> AffineDNFConjunct -> Bool)
-> (AffineDNFConjunct -> AffineDNFConjunct -> Bool)
-> (AffineDNFConjunct -> AffineDNFConjunct -> Bool)
-> (AffineDNFConjunct -> AffineDNFConjunct -> Bool)
-> (AffineDNFConjunct -> AffineDNFConjunct -> AffineDNFConjunct)
-> (AffineDNFConjunct -> AffineDNFConjunct -> AffineDNFConjunct)
-> Ord AffineDNFConjunct
AffineDNFConjunct -> AffineDNFConjunct -> Bool
AffineDNFConjunct -> AffineDNFConjunct -> Ordering
AffineDNFConjunct -> AffineDNFConjunct -> AffineDNFConjunct
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 :: AffineDNFConjunct -> AffineDNFConjunct -> Ordering
compare :: AffineDNFConjunct -> AffineDNFConjunct -> Ordering
$c< :: AffineDNFConjunct -> AffineDNFConjunct -> Bool
< :: AffineDNFConjunct -> AffineDNFConjunct -> Bool
$c<= :: AffineDNFConjunct -> AffineDNFConjunct -> Bool
<= :: AffineDNFConjunct -> AffineDNFConjunct -> Bool
$c> :: AffineDNFConjunct -> AffineDNFConjunct -> Bool
> :: AffineDNFConjunct -> AffineDNFConjunct -> Bool
$c>= :: AffineDNFConjunct -> AffineDNFConjunct -> Bool
>= :: AffineDNFConjunct -> AffineDNFConjunct -> Bool
$cmax :: AffineDNFConjunct -> AffineDNFConjunct -> AffineDNFConjunct
max :: AffineDNFConjunct -> AffineDNFConjunct -> AffineDNFConjunct
$cmin :: AffineDNFConjunct -> AffineDNFConjunct -> AffineDNFConjunct
min :: AffineDNFConjunct -> AffineDNFConjunct -> AffineDNFConjunct
Ord)

type AffineDNFDisjunct = [AffineDNFConjunct]

type AffineDNF = [AffineDNFDisjunct]

classifyIntLt :: VariableIdentifier -> IntTerm -> IntTerm -> IntLtForm
classifyIntLt :: VariableIdentifier -> IntTerm -> IntTerm -> IntLtForm
classifyIntLt VariableIdentifier
x IntTerm
a IntTerm
b =
  let nfa :: IntTermNF
nfa = IntTerm -> IntTermNF
eval IntTerm
a in
  let nfb :: IntTermNF
nfb = IntTerm -> IntTermNF
eval IntTerm
b in
  let ka :: IntValue
ka = IntValue -> Maybe IntValue -> IntValue
forall a. a -> Maybe a -> a
fromMaybe IntValue
0 (Maybe IntValue -> IntValue) -> Maybe IntValue -> IntValue
forall a b. (a -> b) -> a -> b
$ VariableIdentifier
-> Map VariableIdentifier IntValue -> Maybe IntValue
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup VariableIdentifier
x IntTermNF
nfa.coeff in
  let kb :: IntValue
kb = IntValue -> Maybe IntValue -> IntValue
forall a. a -> Maybe a -> a
fromMaybe IntValue
0 (Maybe IntValue -> IntValue) -> Maybe IntValue -> IntValue
forall a b. (a -> b) -> a -> b
$ VariableIdentifier
-> Map VariableIdentifier IntValue -> Maybe IntValue
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup VariableIdentifier
x IntTermNF
nfb.coeff in
  case IntValue -> IntValue -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (IntValue
ka IntValue -> IntValue -> IntValue
forall a. Num a => a -> a -> a
- IntValue
kb) IntValue
0 of
    -- (k(a) - k(b)) · x < ...
    Ordering
GT -> NatValue -> IntTerm -> IntLtForm
LtL (IntValue -> NatValue
forall a b. (Integral a, Num b) => a -> b
fromIntegral (IntValue -> NatValue) -> IntValue -> NatValue
forall a b. (a -> b) -> a -> b
$ IntValue
ka IntValue -> IntValue -> IntValue
forall a. Num a => a -> a -> a
- IntValue
kb)
              (IntTermNF -> IntTerm
quote (VariableIdentifier -> IntTermNF -> IntTermNF
nullify VariableIdentifier
x IntTermNF
nfb IntTermNF -> IntTermNF -> IntTermNF
`minus` VariableIdentifier -> IntTermNF -> IntTermNF
nullify VariableIdentifier
x IntTermNF
nfa))
    -- ... < ...
    Ordering
EQ -> IntTerm -> IntTerm -> IntLtForm
LtC (IntTermNF -> IntTerm
quote (IntTermNF -> IntTerm) -> IntTermNF -> IntTerm
forall a b. (a -> b) -> a -> b
$ VariableIdentifier -> IntTermNF -> IntTermNF
nullify VariableIdentifier
x IntTermNF
nfa) (IntTermNF -> IntTerm
quote (IntTermNF -> IntTerm) -> IntTermNF -> IntTerm
forall a b. (a -> b) -> a -> b
$ VariableIdentifier -> IntTermNF -> IntTermNF
nullify VariableIdentifier
x IntTermNF
nfb)
    -- ... < (k(b) - k(a)) · x
    Ordering
LT -> IntTerm -> NatValue -> IntLtForm
LtR (IntTermNF -> IntTerm
quote (VariableIdentifier -> IntTermNF -> IntTermNF
nullify VariableIdentifier
x IntTermNF
nfa IntTermNF -> IntTermNF -> IntTermNF
`minus` VariableIdentifier -> IntTermNF -> IntTermNF
nullify VariableIdentifier
x IntTermNF
nfb))
              (IntValue -> NatValue
forall a b. (Integral a, Num b) => a -> b
fromIntegral (IntValue -> NatValue) -> IntValue -> NatValue
forall a b. (a -> b) -> a -> b
$ IntValue
kb IntValue -> IntValue -> IntValue
forall a. Num a => a -> a -> a
- IntValue
ka)

classifyIntDiv :: VariableIdentifier -> NatValue -> IntTerm -> IntDivForm
classifyIntDiv :: VariableIdentifier -> NatValue -> IntTerm -> IntDivForm
classifyIntDiv VariableIdentifier
x NatValue
k IntTerm
t =
  let nft :: IntTermNF
nft  = IntTerm -> IntTermNF
eval IntTerm
t
      coef :: IntValue
coef = IntValue -> Maybe IntValue -> IntValue
forall a. a -> Maybe a -> a
fromMaybe IntValue
0 (Maybe IntValue -> IntValue) -> Maybe IntValue -> IntValue
forall a b. (a -> b) -> a -> b
$ VariableIdentifier
-> Map VariableIdentifier IntValue -> Maybe IntValue
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup VariableIdentifier
x IntTermNF
nft.coeff in
  if IntValue
coef IntValue -> IntValue -> Bool
forall a. Eq a => a -> a -> Bool
== IntValue
0
    then NatValue -> IntTerm -> IntDivForm
DivC NatValue
k (IntTerm -> IntTerm
normalise IntTerm
t)
    else let rest :: IntTermNF
rest = VariableIdentifier -> IntTermNF -> IntTermNF
nullify VariableIdentifier
x IntTermNF
nft
         in NatValue -> NatValue -> IntTerm -> IntDivForm
DivL NatValue
k (IntValue -> NatValue
forall a b. (Integral a, Num b) => a -> b
fromIntegral (IntValue -> NatValue) -> IntValue -> NatValue
forall a b. (a -> b) -> a -> b
$ IntValue -> IntValue
forall a. Num a => a -> a
abs IntValue
coef)
                   (IntTermNF -> IntTerm
quote (IntTermNF -> IntTerm) -> IntTermNF -> IntTerm
forall a b. (a -> b) -> a -> b
$ if IntValue
coef IntValue -> IntValue -> Bool
forall a. Ord a => a -> a -> Bool
> IntValue
0 then IntTermNF
rest else IntValue -> IntTermNF -> IntTermNF
Value.mul (-IntValue
1) IntTermNF
rest)

fromDNFConjunct :: VariableIdentifier -> DNFConjunct -> AffineDNFConjunct
fromDNFConjunct :: VariableIdentifier -> DNFConjunct -> AffineDNFConjunct
fromDNFConjunct VariableIdentifier
x (DNF.IntLt IntTerm
i IntTerm
j) = IntLtForm -> AffineDNFConjunct
IntLt (IntLtForm -> AffineDNFConjunct) -> IntLtForm -> AffineDNFConjunct
forall a b. (a -> b) -> a -> b
$ VariableIdentifier -> IntTerm -> IntTerm -> IntLtForm
classifyIntLt VariableIdentifier
x IntTerm
i IntTerm
j
fromDNFConjunct VariableIdentifier
x (DNF.IntDiv NatValue
k IntTerm
i) = IntDivForm -> AffineDNFConjunct
IntDiv (IntDivForm -> AffineDNFConjunct)
-> IntDivForm -> AffineDNFConjunct
forall a b. (a -> b) -> a -> b
$ VariableIdentifier -> NatValue -> IntTerm -> IntDivForm
classifyIntDiv VariableIdentifier
x NatValue
k IntTerm
i
fromDNFConjunct VariableIdentifier
x (DNF.IntNegDiv NatValue
k IntTerm
i) = IntDivForm -> AffineDNFConjunct
IntNegDiv (IntDivForm -> AffineDNFConjunct)
-> IntDivForm -> AffineDNFConjunct
forall a b. (a -> b) -> a -> b
$ VariableIdentifier -> NatValue -> IntTerm -> IntDivForm
classifyIntDiv VariableIdentifier
x NatValue
k IntTerm
i

fromDNF :: VariableIdentifier -> DNF -> AffineDNF
fromDNF :: VariableIdentifier -> DNF -> AffineDNF
fromDNF VariableIdentifier
x = (DNFDisjunct -> [AffineDNFConjunct]) -> DNF -> AffineDNF
forall a b. (a -> b) -> [a] -> [b]
map ((DNFConjunct -> AffineDNFConjunct)
-> DNFDisjunct -> [AffineDNFConjunct]
forall a b. (a -> b) -> [a] -> [b]
map (VariableIdentifier -> DNFConjunct -> AffineDNFConjunct
fromDNFConjunct VariableIdentifier
x))