From: Alex Ozdemir <aozdemir@hmc.edu>
Date: Fri, 14 May 2021 11:34:38 +0000 (-0700)
Subject: Add getId function to python API (#6523)
X-Git-Tag: cvc5-1.0.0~1761
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bcd2e8e2fd28e30cddac35a466bf6ca797e2aa51;p=cvc5.git

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 0eed825eb..95e5fb80e 100644
--- 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
index 000000000..fb3672dbc
--- /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()