From 6dd4efeea9fa0d9975fcffecd5af03bc081b68e7 Mon Sep 17 00:00:00 2001 From: makaimann Date: Tue, 2 Jun 2020 18:10:18 -0700 Subject: [PATCH] Add Term::substitute to Python bindings (#4499) --- src/api/python/cvc4.pxd | 1 + src/api/python/cvc4.pxi | 17 +++++++++++++++++ 2 files changed, 18 insertions(+) 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(( e).cterm) + creplacements.push_back(( r).cterm) + + term.cterm = self.cterm.substitute(ces, creplacements) + return term + def hasOp(self): return self.cterm.hasOp() -- 2.30.2