diff options
| author | Alex Ozdemir <aozdemir@hmc.edu> | 2021-05-14 04:34:38 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-05-14 11:34:38 +0000 |
| commit | bcd2e8e2fd28e30cddac35a466bf6ca797e2aa51 (patch) | |
| tree | c3718626243b8a082669caf3a658f9413cdbd3b1 | |
| parent | ce851ed5aea5ee4bd36ffbba9f86052025434126 (diff) | |
Add getId function to python API (#6523)
(Z3 exposes it to facilitate custom hashes)
| -rw-r--r-- | examples/api/python/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | examples/api/python/id.py | 35 |
2 files changed, 36 insertions, 0 deletions
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() |