diff options
author | makaimann <makaim@stanford.edu> | 2020-06-02 18:10:18 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-02 20:10:18 -0500 |
commit | 6dd4efeea9fa0d9975fcffecd5af03bc081b68e7 (patch) | |
tree | ed4a96921f4f2d82ea5113934acd35df83838a55 /src | |
parent | 37d97be56ccba9c8da9b58fc5a7309ba2f4b1765 (diff) |
Add Term::substitute to Python bindings (#4499)
Diffstat (limited to 'src')
-rw-r--r-- | src/api/python/cvc4.pxd | 1 | ||||
-rw-r--r-- | src/api/python/cvc4.pxi | 17 |
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() |