{- |
This module provides functions for counting symbolic formulas and creating cardinality-constraints.

Internally this converts each given 'Expr' 'BoolSort' into a numerical 'Expr' using 'ite', then sums them up:

@
  count :: forall t f. (Functor f, Foldable f, Num (Expr t)) => f (Expr BoolSort) -> Expr t
  count = sum . fmap (\\b -> ite b 1 0)
@

Therefore additional information for the temporal summation may need to be provided.

E.g. if your logic is \"QF_LIA\" you would want @'count'' \@'IntSort' $ ...@

It is worth noting that some cardinality constraints use optimized encodings, such as @'atLeast' 1 ≡ 'or'@.
-}
module Language.Hasmtlib.Counting
(
  -- * Count
  count, count'

  -- * At-Least
, atLeast

  -- * Exactly
, exactly

  -- * At-Most
, atMost
)
where

import Prelude hiding (not, (&&), (||), or)
import Language.Hasmtlib.Type.SMTSort
import Language.Hasmtlib.Type.Expr
import Language.Hasmtlib.Boolean
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, KnownSMTSort t, Num (HaskellType t), Ord (HaskellType t)) => Expr t -> f (Expr BoolSort) -> Expr BoolSort
atMost :: forall (t :: SMTSort) (f :: * -> *).
(Functor f, Foldable f, KnownSMTSort t, Num (HaskellType t),
 Ord (HaskellType t)) =>
Expr t -> f (Expr 'BoolSort) -> Expr 'BoolSort
atMost (Constant Value t
0) = f (Expr 'BoolSort) -> Expr 'BoolSort
forall (t :: * -> *) b. (Foldable t, Boolean b) => t b -> b
nand
atMost (Constant Value t
1) = f (Expr 'BoolSort) -> Expr 'BoolSort
forall (t :: * -> *) b. (Foldable t, Boolean b) => t b -> b
atMostOneLinear
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
{-# INLINE atMost #-}

atMostOneLinear :: (Foldable f, Boolean b) => f b -> b
atMostOneLinear :: forall (t :: * -> *) b. (Foldable t, Boolean b) => t b -> b
atMostOneLinear f b
xs =
  let (b
_, b
sz) = (b -> (b, b) -> (b, b)) -> (b, b) -> f b -> (b, b)
forall a b. (a -> b -> b) -> b -> f a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((b, b) -> (b, b) -> (b, b)
forall {b}. Boolean b => (b, b) -> (b, b) -> (b, b)
plus ((b, b) -> (b, b) -> (b, b))
-> (b -> (b, b)) -> b -> (b, b) -> (b, b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (, b
forall b. Boolean b => b
false)) (b
forall b. Boolean b => b
false, b
forall b. Boolean b => b
false) f b
xs
   in b -> b
forall b. Boolean b => b -> b
not b
sz
  where
    plus :: (b, b) -> (b, b) -> (b, b)
plus (b
xe, b
xz) (b
ye, b
yz) = (b
xe b -> b -> b
forall b. Boolean b => b -> b -> b
|| b
ye, b
xz b -> b -> b
forall b. Boolean b => b -> b -> b
|| b
yz b -> b -> b
forall b. Boolean b => b -> b -> b
|| (b
xe b -> b -> b
forall b. Boolean b => b -> b -> b
&& b
ye))

-- | 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, KnownSMTSort t, Num (HaskellType t), Ord (HaskellType t)) => Expr t -> f (Expr BoolSort) -> Expr BoolSort
atLeast :: forall (t :: SMTSort) (f :: * -> *).
(Functor f, Foldable f, KnownSMTSort t, Num (HaskellType t),
 Ord (HaskellType t)) =>
Expr t -> f (Expr 'BoolSort) -> Expr 'BoolSort
atLeast (Constant Value t
0) = Expr 'BoolSort -> f (Expr 'BoolSort) -> Expr 'BoolSort
forall a b. a -> b -> a
const Expr 'BoolSort
forall b. Boolean b => b
true
atLeast (Constant Value t
1) = f (Expr 'BoolSort) -> Expr 'BoolSort
forall (t :: * -> *) b. (Foldable t, Boolean b) => t b -> b
or
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
{-# INLINE 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, KnownSMTSort t, Num (HaskellType t), Ord (HaskellType t)) => Expr t -> f (Expr BoolSort) -> Expr BoolSort
exactly :: forall (t :: SMTSort) (f :: * -> *).
(Functor f, Foldable f, KnownSMTSort t, Num (HaskellType t),
 Ord (HaskellType t)) =>
Expr t -> f (Expr 'BoolSort) -> Expr 'BoolSort
exactly (Constant Value t
0) = f (Expr 'BoolSort) -> Expr 'BoolSort
forall (t :: * -> *) b. (Foldable t, Boolean b) => t b -> b
nand
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
{-# INLINE exactly #-}