From 923c9a6b864922dda739f46981664ec0611bec8d Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Wed, 24 Nov 2021 14:17:43 -0800 Subject: [PATCH] examples: Update python api datatypes example. (#7692) The C++ datatypes example was extended in #7689. This updates the Python API datatypes example accordingly. --- examples/api/python/datatypes.py | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/examples/api/python/datatypes.py b/examples/api/python/datatypes.py index 5b897c1b2..96116da08 100644 --- a/examples/api/python/datatypes.py +++ b/examples/api/python/datatypes.py @@ -61,6 +61,19 @@ def test(slv, consListSort): print(" + args:", j) print() + # You can also define a tester term for constructor 'cons': (_ is cons) + t_is_cons = slv.mkTerm( + kinds.ApplyTester, consList["cons"].getTesterTerm(), t) + print("t_is_cons is {}\n\n".format(t_is_cons)) + slv.assertFormula(t_is_cons) + # Updating t at 'head' with value 1 is defined as follows: + t_updated = slv.mkTerm(kinds.ApplyUpdater, + consList["cons"]["head"].getUpdaterTerm(), + t, + slv.mkInteger(1)) + print("t_updated is {}\n\n".format(t_updated)) + slv.assertFormula(slv.mkTerm(kinds.Distinct, t, t_updated)) + # You can also define parameterized datatypes. # This example builds a simple parameterized list of sort T, with one # constructor "cons". -- 2.30.2