Add getId function to python API (#6523)

(Z3 exposes it to facilitate custom hashes)

diff --git a/examples/api/python/CMakeLists.txt b/examples/api/python/CMakeLists.txt
index 0eed825ebaade0d7bab33da6728f89abc6019503..95e5fb80e1933d32f796ceb1b66b961d1dc3f138 100644 (file)
--- a/examples/api/python/CMakeLists.txt
+++ b/examples/api/python/CMakeLists.txt
@@ -29,6 +29,7 @@ set(EXAMPLES_API_PYTHON
   sygus-fun
   sygus-grammar
   sygus-inv
+  id
 )
 
 find_package(PythonInterp ${CVC5_BINDINGS_PYTHON_VERSION} REQUIRED)

diff --git a/examples/api/python/id.py b/examples/api/python/id.py
new file mode 100644 (file)
index 0000000..fb3672d
--- /dev/null
+++ b/examples/api/python/id.py
@@ -0,0 +1,35 @@
+#!/usr/bin/env python
+###############################################################################
+# Top contributors (to current version):
+#   Alex Ozdemir
+#
+# This file is part of the cvc5 project.
+#
+# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+# in the top-level source directory and their institutional affiliations.
+# All rights reserved.  See the file COPYING in the top-level source
+# directory for licensing information.
+# #############################################################################
+#
+# A simple demonstration of the getId function exposed by the cvc5 terms python
+# API
+##
+
+import pycvc5
+from pycvc5 import kinds
+
+if __name__ == "__main__":
+    slv = pycvc5.Solver()
+
+    integer = slv.getIntegerSort()
+    set_ = slv.mkSetSort(integer)
+
+    A = slv.mkConst(set_, "A")
+    B = slv.mkConst(set_, "B")
+    C = slv.mkConst(set_, "C")
+
+    assert A.getId() != B.getId()
+    assert C.getId() != B.getId()
+    assert A.getId() == A.getId()
+    assert B.getId() == B.getId()
+    assert C.getId() == C.getId()