Language.Hasmtlib.Counting

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.

Count

count :: forall t f. (Functor f, Foldable f, Num (Expr t)) => f (Expr BoolSort) -> Expr t

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)) => Proxy t -> f (Expr BoolSort) -> Expr t

Wrapper for count which takes a Proxy.

At-Least

atLeast :: forall t f. (Functor f, Foldable f, KnownSMTSort t, Num (HaskellType t), Ord (HaskellType t)) => Expr t -> f (Expr BoolSort) -> Expr BoolSort

Out of many bool-expressions build a formula which encodes that at least k of them are true.

Exactly

exactly :: forall t f. (Functor f, Foldable f, KnownSMTSort t, Num (HaskellType t), Ord (HaskellType t)) => Expr t -> f (Expr BoolSort) -> Expr BoolSort

Out of many bool-expressions build a formula which encodes that exactly k of them are true.

At-Most

atMost :: forall t f. (Functor f, Foldable f, KnownSMTSort t, Num (HaskellType t), Ord (HaskellType t)) => Expr t -> f (Expr BoolSort) -> Expr BoolSort

Out of many bool-expressions build a formula which encodes that at most k of them are true.