Add Term::substitute to Python bindings (#4499)

diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd
index 5bcc3c5c388c7f8cfbc3af1b7551daff22521464..1c7071958a4d76ffb1b71b9e254d19d4f4a28274 100644 (file)
--- a/src/api/python/cvc4.pxd
+++ b/src/api/python/cvc4.pxd
@@ -243,6 +243,7 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api":
         bint operator!=(const Term&) except +
         Kind getKind() except +
         Sort getSort() except +
+        Term substitute(const vector[Term] es, const vector[Term] & reps) except +
         bint hasOp() except +
         Op getOp() except +
         bint isNull() except +

diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi
index 080f24c8b6e6029a60a947bd77ebc44e0bf90c0f..fa5313f0ec3ad56acc1b118e2c2ea8aada603e8d 100644 (file)
--- a/src/api/python/cvc4.pxi
+++ b/src/api/python/cvc4.pxi
@@ -1080,6 +1080,23 @@ cdef class Term:
         sort.csort = self.cterm.getSort()
         return sort
 
+    def substitute(self, list es, list replacements):
+        cdef vector[c_Term] ces
+        cdef vector[c_Term] creplacements
+        cdef Term term = Term()
+
+        if len(es) != len(replacements):
+            raise RuntimeError("Expecting list inputs to substitute to "
+                               "have the same length but got: "
+                               "{} and {}".format(len(es), len(replacements)))
+
+        for e, r in zip(es, replacements):
+            ces.push_back((<Term?> e).cterm)
+            creplacements.push_back((<Term?> r).cterm)
+
+        term.cterm = self.cterm.substitute(ces, creplacements)
+        return term
+
     def hasOp(self):
         return self.cterm.hasOp()