From 8e3892ebe308712ad645848b551219f95e550b61 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 27 Jan 2022 17:35:13 -0600 Subject: [PATCH] Document substitute in API (#7904) --- src/api/cpp/cvc5.h | 24 ++++++++++++++++++++++- src/api/java/io/github/cvc5/api/Sort.java | 12 ++++++++++++ src/api/java/io/github/cvc5/api/Term.java | 10 ++++++++++ src/api/python/cvc5.pxi | 16 +++++++++++++++ 4 files changed, 61 insertions(+), 1 deletion(-) diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index ad0054606..901bc9f64 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -589,6 +589,13 @@ class CVC5_EXPORT Sort * Substitution of Sorts. * @param sort the subsort to be substituted within this sort. * @param replacement the sort replacing the substituted subsort. + * + * Note that this replacement is applied during a pre-order traversal and + * only once to the sort. It is not run until fix point. + * + * For example, + * (Array A B).substitute({A, C}, {(Array C D), (Array A B)}) will + * return (Array (Array C D) B). */ Sort substitute(const Sort& sort, const Sort& replacement) const; @@ -596,6 +603,11 @@ class CVC5_EXPORT Sort * Simultaneous substitution of Sorts. * @param sorts the subsorts to be substituted within this sort. * @param replacements the sort replacing the substituted subsorts. + * + * Note that this replacement is applied during a pre-order traversal and + * only once to the sort. It is not run until fix point. In the case that + * sorts contains duplicates, the replacement earliest in the vector takes + * priority. */ Sort substitute(const std::vector& sorts, const std::vector& replacements) const; @@ -1130,13 +1142,23 @@ class CVC5_EXPORT Term Sort getSort() const; /** - * @return the result of replacing 'term' by 'replacement' in this term + * @return the result of replacing 'term' by 'replacement' in this term. + * + * Note that this replacement is applied during a pre-order traversal and + * only once to the term. It is not run until fix point. */ Term substitute(const Term& term, const Term& replacement) const; /** * @return the result of simultaneously replacing 'terms' by 'replacements' * in this term + * + * Note that this replacement is applied during a pre-order traversal and + * only once to the term. It is not run until fix point. In the case that + * terms contains duplicates, the replacement earliest in the vector takes + * priority. For example, calling substitute on f(x,y) with + * terms = { x, z }, replacements = { g(z), w } + * results in the term f(g(z),y). */ Term substitute(const std::vector& terms, const std::vector& replacements) const; diff --git a/src/api/java/io/github/cvc5/api/Sort.java b/src/api/java/io/github/cvc5/api/Sort.java index 326920a4e..549ad6c25 100644 --- a/src/api/java/io/github/cvc5/api/Sort.java +++ b/src/api/java/io/github/cvc5/api/Sort.java @@ -454,6 +454,9 @@ public class Sort extends AbstractPointer implements Comparable * Substitution of Sorts. * @param sort the subsort to be substituted within this sort. * @param replacement the sort replacing the substituted subsort. + * + * Note that this replacement is applied during a pre-order traversal and + * only once to the sort. It is not run until fix point. */ public Sort substitute(Sort sort, Sort replacement) { @@ -467,6 +470,15 @@ public class Sort extends AbstractPointer implements Comparable * Simultaneous substitution of Sorts. * @param sorts the subsorts to be substituted within this sort. * @param replacements the sort replacing the substituted subsorts. + * + * Note that this replacement is applied during a pre-order traversal and + * only once to the sort. It is not run until fix point. In the case that + * sorts contains duplicates, the replacement earliest in the list takes + * priority. + * + * For example, + * (Array A B).substitute({A, C}, {(Array C D), (Array A B)}) will + * return (Array (Array C D) B). */ public Sort substitute(Sort[] sorts, Sort[] replacements) { diff --git a/src/api/java/io/github/cvc5/api/Term.java b/src/api/java/io/github/cvc5/api/Term.java index be792548e..7fddc49be 100644 --- a/src/api/java/io/github/cvc5/api/Term.java +++ b/src/api/java/io/github/cvc5/api/Term.java @@ -137,6 +137,9 @@ public class Term extends AbstractPointer implements Comparable, Iterable< /** * @return the result of replacing 'term' by 'replacement' in this term + * + * Note that this replacement is applied during a pre-order traversal and + * only once to the term. It is not run until fix point. */ public Term substitute(Term term, Term replacement) { @@ -149,6 +152,13 @@ public class Term extends AbstractPointer implements Comparable, Iterable< /** * @return the result of simultaneously replacing 'terms' by 'replacements' * in this term + * + * Note that this replacement is applied during a pre-order traversal and + * only once to the term. It is not run until fix point. In the case that + * terms contains duplicates, the replacement earliest in the vector takes + * priority. For example, calling substitute on f(x,y) with + * terms = { x, z }, replacements = { g(z), w } + * results in the term f(g(z),y). */ public Term substitute(List terms, List replacements) { diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index d5aedd0a4..10f697196 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -2631,6 +2631,15 @@ cdef class Sort: :param sort_or_list_1: the subsort or subsorts to be substituted within this sort. :param sort_or_list_2: the sort or list of sorts replacing the substituted subsort. + + Note that this replacement is applied during a pre-order traversal and + only once to the sort. It is not run until fix point. In the case that + sort_or_list_1 contains duplicates, the replacement earliest in the list + takes priority. + + For example, + (Array A B) .substitute([A, C], [(Array C D), (Array A B)]) will + return (Array (Array C D) B). """ # The resulting sort after substitution @@ -2953,6 +2962,13 @@ cdef class Term: def substitute(self, term_or_list_1, term_or_list_2): """ :return: the result of simultaneously replacing the term(s) stored in ``term_or_list_1`` by the term(s) stored in ``term_or_list_2`` in this term. + + Note that this replacement is applied during a pre-order traversal and + only once to the term. It is not run until fix point. In the case that + terms contains duplicates, the replacement earliest in the list takes + priority. For example, calling substitute on f(x,y) with + term_or_list_1 = [ x, z ], term_or_list_2 = [ g(z), w ] + results in the term f(g(z),y). """ # The resulting term after substitution cdef Term term = Term(self.solver) -- 2.30.2