{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
{-# HLINT ignore "Eta reduce" #-}
module Hermod.ReCon.Presburger.Internal.IR.QuantifierFree
  ( QuantifierFree(..)
  , unfoldImplies
  , eval
  , quote
  ) where

import           Hermod.ReCon.Common.Types (NatValue)
import           Hermod.ReCon.Integer.Polynomial.Term
import           Hermod.ReCon.Presburger.Formula (BinRel (..))

-- | The quantifier-free fragment of Presburger arithmetic: propositional
--   connectives over atomic comparisons (@IntBinRel@) and divisibility
--   (@IntDiv@), with no quantifiers.
--   This is both the target form produced by Cooper's quantifier elimination
--   and the evaluation domain: 'eval' reduces a closed 'QuantifierFree'
--   sentence to a 'Bool'.
data QuantifierFree =
     -- | φ ∨ ψ
     Or QuantifierFree QuantifierFree
     -- | φ ∧ ψ
   | And QuantifierFree QuantifierFree
     -- | ¬ φ
   | Not QuantifierFree
     -- | φ ⇒ ψ
   | Implies QuantifierFree QuantifierFree
     -- | T
   | Top
     -- | ⊥
   | Bottom
     -- | i = i | i < i | i ≤ i | i > i | i ≥ i
   | IntBinRel BinRel IntTerm IntTerm
     -- | ℕ⁺ \| i  (divisibility relation, first argument is a non-zero ℕ)
   | IntDiv NatValue IntTerm deriving (Int -> QuantifierFree -> ShowS
[QuantifierFree] -> ShowS
QuantifierFree -> [Char]
(Int -> QuantifierFree -> ShowS)
-> (QuantifierFree -> [Char])
-> ([QuantifierFree] -> ShowS)
-> Show QuantifierFree
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> QuantifierFree -> ShowS
showsPrec :: Int -> QuantifierFree -> ShowS
$cshow :: QuantifierFree -> [Char]
show :: QuantifierFree -> [Char]
$cshowList :: [QuantifierFree] -> ShowS
showList :: [QuantifierFree] -> ShowS
Show, QuantifierFree -> QuantifierFree -> Bool
(QuantifierFree -> QuantifierFree -> Bool)
-> (QuantifierFree -> QuantifierFree -> Bool) -> Eq QuantifierFree
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: QuantifierFree -> QuantifierFree -> Bool
== :: QuantifierFree -> QuantifierFree -> Bool
$c/= :: QuantifierFree -> QuantifierFree -> Bool
/= :: QuantifierFree -> QuantifierFree -> Bool
Eq, Eq QuantifierFree
Eq QuantifierFree =>
(QuantifierFree -> QuantifierFree -> Ordering)
-> (QuantifierFree -> QuantifierFree -> Bool)
-> (QuantifierFree -> QuantifierFree -> Bool)
-> (QuantifierFree -> QuantifierFree -> Bool)
-> (QuantifierFree -> QuantifierFree -> Bool)
-> (QuantifierFree -> QuantifierFree -> QuantifierFree)
-> (QuantifierFree -> QuantifierFree -> QuantifierFree)
-> Ord QuantifierFree
QuantifierFree -> QuantifierFree -> Bool
QuantifierFree -> QuantifierFree -> Ordering
QuantifierFree -> QuantifierFree -> QuantifierFree
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 :: QuantifierFree -> QuantifierFree -> Ordering
compare :: QuantifierFree -> QuantifierFree -> Ordering
$c< :: QuantifierFree -> QuantifierFree -> Bool
< :: QuantifierFree -> QuantifierFree -> Bool
$c<= :: QuantifierFree -> QuantifierFree -> Bool
<= :: QuantifierFree -> QuantifierFree -> Bool
$c> :: QuantifierFree -> QuantifierFree -> Bool
> :: QuantifierFree -> QuantifierFree -> Bool
$c>= :: QuantifierFree -> QuantifierFree -> Bool
>= :: QuantifierFree -> QuantifierFree -> Bool
$cmax :: QuantifierFree -> QuantifierFree -> QuantifierFree
max :: QuantifierFree -> QuantifierFree -> QuantifierFree
$cmin :: QuantifierFree -> QuantifierFree -> QuantifierFree
min :: QuantifierFree -> QuantifierFree -> QuantifierFree
Ord)

unfoldImplies :: QuantifierFree -> QuantifierFree -> QuantifierFree
unfoldImplies :: QuantifierFree -> QuantifierFree -> QuantifierFree
unfoldImplies QuantifierFree
a QuantifierFree
b = QuantifierFree -> QuantifierFree -> QuantifierFree
Or (QuantifierFree -> QuantifierFree
Not QuantifierFree
a) QuantifierFree
b

-- | Evaluate a closed QuantifierFree formula to a Bool.
-- Precondition: no free variables (IntVar nodes must not appear in any IntTerm).
eval :: QuantifierFree -> Bool
eval :: QuantifierFree -> Bool
eval (Or QuantifierFree
a QuantifierFree
b)          = QuantifierFree -> Bool
eval QuantifierFree
a Bool -> Bool -> Bool
|| QuantifierFree -> Bool
eval QuantifierFree
b
eval (And QuantifierFree
a QuantifierFree
b)         = QuantifierFree -> Bool
eval QuantifierFree
a Bool -> Bool -> Bool
&& QuantifierFree -> Bool
eval QuantifierFree
b
eval (Not QuantifierFree
a)           = Bool -> Bool
not (QuantifierFree -> Bool
eval QuantifierFree
a)
eval (Implies QuantifierFree
a QuantifierFree
b)     = Bool -> Bool
not (QuantifierFree -> Bool
eval QuantifierFree
a) Bool -> Bool -> Bool
|| QuantifierFree -> Bool
eval QuantifierFree
b
eval QuantifierFree
Top               = Bool
True
eval QuantifierFree
Bottom            = Bool
False
eval (IntBinRel BinRel
r IntTerm
i IntTerm
j) = BinRel -> IntValue -> IntValue -> Bool
evalRel BinRel
r (IntTerm -> IntValue
evalTerm IntTerm
i) (IntTerm -> IntValue
evalTerm IntTerm
j)
eval (IntDiv NatValue
k IntTerm
t)      = IntTerm -> IntValue
evalTerm IntTerm
t IntValue -> IntValue -> IntValue
forall a. Integral a => a -> a -> a
`mod` NatValue -> IntValue
forall a b. (Integral a, Num b) => a -> b
fromIntegral NatValue
k IntValue -> IntValue -> Bool
forall a. Eq a => a -> a -> Bool
== IntValue
0

evalRel :: BinRel -> IntValue -> IntValue -> Bool
evalRel :: BinRel -> IntValue -> IntValue -> Bool
evalRel BinRel
Eq  IntValue
i IntValue
j = IntValue
i IntValue -> IntValue -> Bool
forall a. Eq a => a -> a -> Bool
== IntValue
j
evalRel BinRel
Lt  IntValue
i IntValue
j = IntValue
i IntValue -> IntValue -> Bool
forall a. Ord a => a -> a -> Bool
<  IntValue
j
evalRel BinRel
Lte IntValue
i IntValue
j = IntValue
i IntValue -> IntValue -> Bool
forall a. Ord a => a -> a -> Bool
<= IntValue
j
evalRel BinRel
Gt  IntValue
i IntValue
j = IntValue
i IntValue -> IntValue -> Bool
forall a. Ord a => a -> a -> Bool
>  IntValue
j
evalRel BinRel
Gte IntValue
i IntValue
j = IntValue
i IntValue -> IntValue -> Bool
forall a. Ord a => a -> a -> Bool
>= IntValue
j

-- | Evaluate a closed IntTerm to an integer value.
-- Precondition: no IntVar nodes.
evalTerm :: IntTerm -> IntValue
evalTerm :: IntTerm -> IntValue
evalTerm (IntConst IntValue
k)  = IntValue
k
evalTerm (IntSum IntTerm
a IntTerm
b)  = IntTerm -> IntValue
evalTerm IntTerm
a IntValue -> IntValue -> IntValue
forall a. Num a => a -> a -> a
+ IntTerm -> IntValue
evalTerm IntTerm
b
evalTerm (IntVar IntValue
_ VariableIdentifier
x)  = [Char] -> IntValue
forall a. HasCallStack => [Char] -> a
error ([Char] -> IntValue) -> [Char] -> IntValue
forall a b. (a -> b) -> a -> b
$ [Char]
"evalTerm: free variable " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> VariableIdentifier -> [Char]
forall a. Show a => a -> [Char]
show VariableIdentifier
x

-- | Embed a Bool into QuantifierFree.
quote :: Bool -> QuantifierFree
quote :: Bool -> QuantifierFree
quote Bool
True  = QuantifierFree
Top
quote Bool
False = QuantifierFree
Bottom