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.

diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index 5cc6f1c658b7c069a9a8e1a0693f7b5921bd9e65..da78b1888b7030f28f3f8e4150a0acb8964dc916 100644 (file)
--- 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 81809b5647afc911fa876d4159a6423b79417178..637f46cd3e37d68c071bb30ef129b011c7ddc9c9 100644 (file)
--- 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 16f3fa180afe773e0c17d4c89f563a73582dd67e..75cac1375b3a91d7e52e6ced698644c5d509bac8 100644 (file)
--- 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()