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

2 files changed, 18 insertions, 0 deletions

diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd
index 5bcc3c5c3..1c7071958 100644
--- 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 080f24c8b..fa5313f0e 100644
--- 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()