diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -6,6 +6,11 @@
 The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
 and this project adheres to [PVP versioning](https://pvp.haskell.org/).
 
+## v1.3.0 _(2024-07-12)_
+
+### Added
+- Added cardinality constraints with `Language.Hasmtlib.Counting`
+
 ## v1.2.0 _(2024-07-11)_
 
 ### Added
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -62,7 +62,7 @@
   ```haskell
     data SMTSort = BoolSort | IntSort | RealSort | BvSort Nat | ArraySort SMTSort SMTSort
     data Expr (t :: SMTSort) where ...
-  
+
     ite :: Expr BoolSort -> Expr t -> Expr t -> Expr t
   ```
 - [x] Full SMTLib 2.6 standard support for Sorts Int, Real, Bool, unsigned BitVec & Array
@@ -76,7 +76,7 @@
       setLogic "QF_BV"
       x <- var @(BvSort 16)
       y <- var
-      assert $ x - (maxBound `mod` 8) === y * y 
+      assert $ x - (maxBound `mod` 8) === y * y
       return (x,y)
   ```
 - [x] Add your own solvers via the [Solver type](https://github.com/bruderj15/Hasmtlib/blob/master/src/Language/Hasmtlib/Type/Solution.hs)
@@ -87,14 +87,15 @@
 - [x] Solvers via external processes: CVC5, Z3, Yices2-SMT & MathSAT
   ```haskell
     (result, solution) <- solveWith (solver mathsat) $ do
-      setLogic "QF_LIA" 
+      setLogic "QF_LIA"
       assert $ ...
   ```
 - [x] Incremental solving
   ```haskell
       cvc5Living <- interactiveSolver cvc5
       interactiveWith cvc5Living $ do
-        setLogic "QF_LIA"    
+        setLogic "QF_LIA"
+        setOption $ Incremental True
         setOption $ ProduceModels True
         x <- var @IntSort
         assert $ x === 42
diff --git a/hasmtlib.cabal b/hasmtlib.cabal
--- a/hasmtlib.cabal
+++ b/hasmtlib.cabal
@@ -1,7 +1,7 @@
 cabal-version:         3.0
 
 name:                  hasmtlib
-version:               1.2.0
+version:               1.3.0
 synopsis:              A monad for interfacing with external SMT solvers
 description:           Hasmtlib is a library for generating SMTLib2-problems using a monad.
   It takes care of encoding your problem, marshaling the data to an external solver and parsing and interpreting the result into Haskell types.
@@ -30,6 +30,7 @@
                      , Language.Hasmtlib.Iteable
                      , Language.Hasmtlib.Boolean
                      , Language.Hasmtlib.Variable
+                     , Language.Hasmtlib.Counting
                      , Language.Hasmtlib.Equatable
                      , Language.Hasmtlib.Orderable
                      , Language.Hasmtlib.Integraled
diff --git a/src/Language/Hasmtlib.hs b/src/Language/Hasmtlib.hs
--- a/src/Language/Hasmtlib.hs
+++ b/src/Language/Hasmtlib.hs
@@ -14,6 +14,7 @@
   , module Language.Hasmtlib.Equatable
   , module Language.Hasmtlib.Orderable
   , module Language.Hasmtlib.Codec
+  , module Language.Hasmtlib.Counting
   , module Language.Hasmtlib.Variable
   , module Language.Hasmtlib.Solver.Common
   , module Language.Hasmtlib.Solver.CVC5
@@ -37,6 +38,7 @@
 import Language.Hasmtlib.Equatable
 import Language.Hasmtlib.Orderable
 import Language.Hasmtlib.Codec
+import Language.Hasmtlib.Counting
 import Language.Hasmtlib.Variable
 import Language.Hasmtlib.Solver.Common
 import Language.Hasmtlib.Solver.CVC5
diff --git a/src/Language/Hasmtlib/Counting.hs b/src/Language/Hasmtlib/Counting.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Hasmtlib/Counting.hs
@@ -0,0 +1,23 @@
+module Language.Hasmtlib.Counting where
+
+import Prelude hiding (not, (&&), (||), or)
+import Language.Hasmtlib.Internal.Expr.Num ()
+import Language.Hasmtlib.Internal.Expr
+import Language.Hasmtlib.Equatable
+import Language.Hasmtlib.Orderable
+import Language.Hasmtlib.Iteable
+
+-- | 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  k = (<=? k) . sum . fmap (\b -> ite b 1 0)
+{-# 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 k = (>=? k) . sum . fmap (\b -> ite b 1 0)
+{-# 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 k = (=== k) . sum . fmap (\b -> ite b 1 0)
+{-# INLINEABLE exactly #-}