From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Wed, 24 Nov 2021 22:17:43 +0000 (-0800)
Subject: examples: Update python api datatypes example. (#7692)
X-Git-Tag: cvc5-1.0.0~769
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=923c9a6b864922dda739f46981664ec0611bec8d;p=cvc5.git

examples: Update python api datatypes example. (#7692)

The C++ datatypes example was extended in #7689. This updates the Python
API datatypes example accordingly.
---

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".