From bcd2e8e2fd28e30cddac35a466bf6ca797e2aa51 Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Fri, 14 May 2021 04:34:38 -0700 Subject: [PATCH] Add getId function to python API (#6523) (Z3 exposes it to facilitate custom hashes) --- examples/api/python/CMakeLists.txt | 1 + examples/api/python/id.py | 35 ++++++++++++++++++++++++++++++ 2 files changed, 36 insertions(+) create mode 100644 examples/api/python/id.py 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() -- 2.30.2