diff options
Diffstat (limited to 'src/api/cvc4cpp.h')
| -rw-r--r-- | src/api/cvc4cpp.h | 27 |
1 files changed, 27 insertions, 0 deletions
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 2cb042540..c66113f31 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -387,6 +387,12 @@ class CVC4_PUBLIC Sort bool isSet() const; /** + * Is this a Bag sort? + * @return true if the sort is a Bag sort + */ + bool isBag() const; + + /** * Is this a Sequence sort? * @return true if the sort is a Sequence sort */ @@ -525,6 +531,13 @@ class CVC4_PUBLIC Sort */ Sort getSetElementSort() const; + /* Bag sort ------------------------------------------------------------ */ + + /** + * @return the element sort of a bag sort + */ + Sort getBagElementSort() const; + /* Sequence sort ------------------------------------------------------- */ /** @@ -2304,6 +2317,13 @@ class CVC4_PUBLIC Solver Sort mkSetSort(Sort elemSort) const; /** + * Create a bag sort. + * @param elemSort the sort of the bag elements + * @return the bag sort + */ + Sort mkBagSort(Sort elemSort) const; + + /** * Create a sequence sort. * @param elemSort the sort of the sequence elements * @return the sequence sort @@ -2569,6 +2589,13 @@ class CVC4_PUBLIC Solver Term mkEmptySet(Sort s) const; /** + * Create a constant representing an empty bag of the given sort. + * @param s the sort of the bag elements. + * @return the empty bag constant + */ + Term mkEmptyBag(Sort s) const; + + /** * Create a separation logic nil term. * @param sort the sort of the nil term * @return the separation logic nil term |