module Hermod.ReCon.Presburger.Decide (eval, quote) where

import           Hermod.ReCon.Presburger.Formula (Formula (Bottom, Top))
import           Hermod.ReCon.Presburger.Internal.CooperQE (eliminate)
import qualified Hermod.ReCon.Presburger.Internal.IR.ForallFree as F
import qualified Hermod.ReCon.Presburger.Internal.IR.QuantifierFree as Q

-- | Decide a closed Formula by eliminating all quantifiers and
-- evaluating the resulting ground QuantifierFree formula.
eval :: Formula -> Bool
eval :: Formula -> Bool
eval = QuantifierFree -> Bool
Q.eval (QuantifierFree -> Bool)
-> (Formula -> QuantifierFree) -> Formula -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ForallFree -> QuantifierFree
eliminate (ForallFree -> QuantifierFree)
-> (Formula -> ForallFree) -> Formula -> QuantifierFree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Formula -> ForallFree
F.fromFormula

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