module Language.Hasmtlib.Counting where

import Prelude hiding (not, (&&), (||), or)
import Language.Hasmtlib.Internal.Expr.Num ()
import Language.Hasmtlib.Internal.Expr
import Language.Hasmtlib.Type.SMTSort
import Language.Hasmtlib.Equatable
import Language.Hasmtlib.Orderable
import Language.Hasmtlib.Iteable
import Data.Proxy

-- | Wrapper for 'count' which takes a 'Proxy'.
count' :: forall t f. (Functor f, Foldable f, Num (Expr t)) => Proxy t -> f (Expr BoolSort) -> Expr t
count' :: forall (t :: SMTSort) (f :: * -> *).
(Functor f, Foldable f, Num (Expr t)) =>
Proxy t -> f (Expr 'BoolSort) -> Expr t
count' Proxy t
_ = f (Expr t) -> Expr t
forall a. Num a => f a -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum (f (Expr t) -> Expr t)
-> (f (Expr 'BoolSort) -> f (Expr t))
-> f (Expr 'BoolSort)
-> Expr t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr 'BoolSort -> Expr t) -> f (Expr 'BoolSort) -> f (Expr t)
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Expr 'BoolSort
b -> Expr 'BoolSort -> Expr t -> Expr t -> Expr t
forall b a. Iteable b a => b -> a -> a -> a
ite Expr 'BoolSort
b Expr t
1 Expr t
0)
{-# INLINEABLE count' #-}

-- | Out of many bool-expressions build a formula which encodes how many of them are 'true'.
count :: forall t f. (Functor f, Foldable f, Num (Expr t)) => f (Expr BoolSort) -> Expr t
count :: forall (t :: SMTSort) (f :: * -> *).
(Functor f, Foldable f, Num (Expr t)) =>
f (Expr 'BoolSort) -> Expr t
count = Proxy t -> f (Expr 'BoolSort) -> Expr t
forall (t :: SMTSort) (f :: * -> *).
(Functor f, Foldable f, Num (Expr t)) =>
Proxy t -> f (Expr 'BoolSort) -> Expr t
count' (forall {k} (t :: k). Proxy t
forall (t :: SMTSort). Proxy t
Proxy @t)
{-# INLINE count #-}

-- | Out of many bool-expressions build a formula which encodes that __at most__ 'k' of them are 'true'.
atMost  :: forall t f. (Functor f, Foldable f, Num (Expr t), Orderable (Expr t)) => Expr t -> f (Expr BoolSort) -> Expr BoolSort
atMost :: forall (t :: SMTSort) (f :: * -> *).
(Functor f, Foldable f, Num (Expr t), Orderable (Expr t)) =>
Expr t -> f (Expr 'BoolSort) -> Expr 'BoolSort
atMost  Expr t
k = (Expr t -> Expr t -> Expr 'BoolSort
forall a. Orderable a => a -> a -> Expr 'BoolSort
<=? Expr t
k) (Expr t -> Expr 'BoolSort)
-> (f (Expr 'BoolSort) -> Expr t)
-> f (Expr 'BoolSort)
-> Expr 'BoolSort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Expr 'BoolSort) -> Expr t
forall (t :: SMTSort) (f :: * -> *).
(Functor f, Foldable f, Num (Expr t)) =>
f (Expr 'BoolSort) -> Expr t
count
{-# INLINEABLE atMost #-}

-- | Out of many bool-expressions build a formula which encodes that __at least__ 'k' of them are 'true'.
atLeast :: forall t f. (Functor f, Foldable f, Num (Expr t), Orderable (Expr t)) => Expr t -> f (Expr BoolSort) -> Expr BoolSort
atLeast :: forall (t :: SMTSort) (f :: * -> *).
(Functor f, Foldable f, Num (Expr t), Orderable (Expr t)) =>
Expr t -> f (Expr 'BoolSort) -> Expr 'BoolSort
atLeast Expr t
k = (Expr t -> Expr t -> Expr 'BoolSort
forall a. Orderable a => a -> a -> Expr 'BoolSort
>=? Expr t
k) (Expr t -> Expr 'BoolSort)
-> (f (Expr 'BoolSort) -> Expr t)
-> f (Expr 'BoolSort)
-> Expr 'BoolSort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Expr 'BoolSort) -> Expr t
forall (t :: SMTSort) (f :: * -> *).
(Functor f, Foldable f, Num (Expr t)) =>
f (Expr 'BoolSort) -> Expr t
count
{-# INLINEABLE atLeast #-}

-- | Out of many bool-expressions build a formula which encodes that __exactly__ 'k' of them are 'true'.
exactly :: forall t f. (Functor f, Foldable f, Num (Expr t), Orderable (Expr t)) => Expr t -> f (Expr BoolSort) -> Expr BoolSort
exactly :: forall (t :: SMTSort) (f :: * -> *).
(Functor f, Foldable f, Num (Expr t), Orderable (Expr t)) =>
Expr t -> f (Expr 'BoolSort) -> Expr 'BoolSort
exactly Expr t
k = (Expr t -> Expr t -> Expr 'BoolSort
forall a. Equatable a => a -> a -> Expr 'BoolSort
=== Expr t
k) (Expr t -> Expr 'BoolSort)
-> (f (Expr 'BoolSort) -> Expr t)
-> f (Expr 'BoolSort)
-> Expr 'BoolSort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Expr 'BoolSort) -> Expr t
forall (t :: SMTSort) (f :: * -> *).
(Functor f, Foldable f, Num (Expr t)) =>
f (Expr 'BoolSort) -> Expr t
count
{-# INLINEABLE exactly #-}