From 6e0326d6f2d450329591b551d10742a5ebcb6fe5 Mon Sep 17 00:00:00 2001
From: yoni206 <yoni206@users.noreply.github.com>
Date: Wed, 30 Mar 2022 09:55:56 +0300
Subject: [PATCH] Add information for cardinality constraint to the Python API
 (#8444)

This PR complements #8422 by adding a tester and a getter for cardinality constraints to the python API. The corresponding test from solver_black is translated and included.
---
 src/api/python/cvc5.pxd           |  2 ++
 src/api/python/cvc5.pxi           | 21 +++++++++++++++++++++
 test/unit/api/python/test_term.py | 16 ++++++++++++++++
 3 files changed, 39 insertions(+)

diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index 5cc6f1c65..da78b1888 100644
--- a/src/api/python/cvc5.pxd
+++ b/src/api/python/cvc5.pxd
@@ -494,6 +494,8 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5":
             Term operator*() except +
         const_iterator begin() except +
         const_iterator end() except +
+        bint isCardinalityConstraint() except +
+        pair[Sort, uint32_t] getCardinalityConstraint() except +
 
         bint isConstArray() except +
         bint isBooleanValue() except +
diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index 81809b564..637f46cd3 100644
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -3633,6 +3633,27 @@ cdef class Term:
             elems.append(term)
         return elems
 
+    def isCardinalityConstraint(self):
+        """
+        .. warning:: This method is experimental and may change in future
+                     versions.
+	:return: True if the term is a cardinality constraint.
+	"""
+        return self.cterm.isCardinalityConstraint()
+
+    def getCardinalityConstraint(self):
+        """
+        .. warning:: This method is experimental and may change in future
+                     versions.
+	:return: the sort the cardinality constraint is for and its upper bound.
+	"""
+        cdef pair[c_Sort, uint32_t] p
+        p = self.cterm.getCardinalityConstraint()
+        cdef Sort sort = Sort(self.solver)
+        sort.csort = p.first
+        return (sort, p.second)
+
+
     def isUninterpretedSortValue(self):
         """:return: True iff this term is a value from an uninterpreted sort."""
         return self.cterm.isUninterpretedSortValue()
diff --git a/test/unit/api/python/test_term.py b/test/unit/api/python/test_term.py
index 16f3fa180..75cac1375 100644
--- a/test/unit/api/python/test_term.py
+++ b/test/unit/api/python/test_term.py
@@ -1296,6 +1296,22 @@ def test_const_sequence_elements(solver):
     with pytest.raises(RuntimeError):
         su.getSequenceValue()
 
+def test_get_cardinality_constraint(solver):
+  su = solver.mkUninterpretedSort("u")
+  t = solver.mkCardinalityConstraint(su, 3)
+  assert t.isCardinalityConstraint()
+  cc = t.getCardinalityConstraint()
+  assert cc[0] == su
+  assert cc[1] == 3
+  x = solver.mkConst(solver.getIntegerSort(), "x")
+  assert not x.isCardinalityConstraint()
+  with pytest.raises(RuntimeError):
+    x.getCardinalityConstraint()
+  nullt = cvc5.Term(solver)
+  with pytest.raises(RuntimeError):
+    nullt.isCardinalityConstraint()
+
+
 
 def test_term_scoped_to_string(solver):
     intsort = solver.getIntegerSort()
-- 
2.30.2