From 860164fa178cd8fa848ce3796c242fdde5838650 Mon Sep 17 00:00:00 2001 From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> Date: Thu, 11 Nov 2021 16:01:24 -0600 Subject: [PATCH] Add an API method to get the raw name of a term. (#7618) --- src/api/cpp/cvc5.cpp | 24 ++++++++++++++++++ src/api/cpp/cvc5.h | 11 +++++++++ src/api/java/io/github/cvc5/api/Term.java | 21 ++++++++++++++++ src/api/java/jni/term.cpp | 30 +++++++++++++++++++++++ src/api/python/cvc5.pxd | 2 ++ src/api/python/cvc5.pxi | 6 +++++ src/printer/printer.cpp | 6 ++--- test/unit/api/cpp/term_black.cpp | 15 ++++++++++++ test/unit/api/java/TermTest.java | 15 ++++++++++++ test/unit/api/python/test_term.py | 17 +++++++++++++ 10 files changed, 144 insertions(+), 3 deletions(-) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 7976c19ef..18879a4eb 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -53,6 +53,7 @@ #include "expr/node_algorithm.h" #include "expr/node_builder.h" #include "expr/node_manager.h" +#include "expr/node_manager_attributes.h" #include "expr/sequence.h" #include "expr/type_node.h" #include "expr/uninterpreted_constant.h" @@ -2535,6 +2536,29 @@ Op Term::getOp() const CVC5_API_TRY_CATCH_END; } +bool Term::hasSymbol() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + //////// all checks before this line + return d_node->hasAttribute(expr::VarNameAttr()); + //////// + CVC5_API_TRY_CATCH_END; +} + +std::string Term::getSymbol() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + CVC5_API_CHECK(d_node->hasAttribute(expr::VarNameAttr())) + << "Invalid call to '" << __PRETTY_FUNCTION__ + << "', expected the term to have a symbol."; + //////// all checks before this line + return d_node->getAttribute(expr::VarNameAttr()); + //////// + CVC5_API_TRY_CATCH_END; +} + bool Term::isNull() const { CVC5_API_TRY_CATCH_BEGIN; diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index ab9a4de25..46678b0d8 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -1127,6 +1127,17 @@ class CVC5_EXPORT Term */ Op getOp() const; + /** + * @return true if the term has a symbol. + */ + bool hasSymbol() const; + + /** + * Asserts hasSymbol(). + * @return the raw symbol of the term. + */ + std::string getSymbol() const; + /** * @return true if this Term is a null term */ diff --git a/src/api/java/io/github/cvc5/api/Term.java b/src/api/java/io/github/cvc5/api/Term.java index bbed609f7..fc09767ed 100644 --- a/src/api/java/io/github/cvc5/api/Term.java +++ b/src/api/java/io/github/cvc5/api/Term.java @@ -200,6 +200,27 @@ public class Term extends AbstractPointer implements Comparable, Iterable< private native long getOp(long pointer); + /** + * @return true if the term has a symbol. + */ + public boolean hasSymbol() + { + return hasSymbol(pointer); + } + + private native boolean hasSymbol(long pointer); + + /** + * Asserts hasSymbol(). + * @return the raw symbol of the term. + */ + public String getSymbol() + { + return getSymbol(pointer); + } + + private native String getSymbol(long pointer); + /** * @return true if this Term is a null term */ diff --git a/src/api/java/jni/term.cpp b/src/api/java/jni/term.cpp index d54b0a2b5..702a5064d 100644 --- a/src/api/java/jni/term.cpp +++ b/src/api/java/jni/term.cpp @@ -245,6 +245,36 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Term_getOp(JNIEnv* env, CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } +/* + * Class: io_github_cvc5_api_Term + * Method: hasSymbol + * Signature: (J)Z + */ +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Term_hasSymbol(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Term* current = reinterpret_cast(pointer); + return static_cast(current->hasSymbol()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(false)); +} + +/* + * Class: io_github_cvc5_api_Term + * Method: getSymbol + * Signature: (J)Ljava/lang/String; + */ +JNIEXPORT jstring JNICALL Java_io_github_cvc5_api_Term_getSymbol(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Term* current = reinterpret_cast(pointer); + return env->NewStringUTF(current->getSymbol().c_str()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr); +} + /* * Class: io_github_cvc5_api_Term * Method: isNull diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index 9dae7da96..f5dc2aca2 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -391,6 +391,8 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": Term substitute(const vector[Term] & es, const vector[Term] & reps) except + bint hasOp() except + Op getOp() except + + bint hasSymbol() except + + string getSymbol() except + bint isNull() except + Term getConstArrayBase() except + Term notTerm() except + diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 1df252e86..3d24b5dbd 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -2839,6 +2839,12 @@ cdef class Term: op.cop = self.cterm.getOp() return op + def hasSymbol(self): + return self.cterm.hasSymbol() + + def getSymbol(self): + return self.cterm.getSymbol().decode() + def isNull(self): return self.cterm.isNull() diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index b66ae5728..16b626e30 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -16,6 +16,7 @@ #include +#include "expr/node_manager_attributes.h" #include "options/base_options.h" #include "options/language.h" #include "printer/ast/ast_printer.h" @@ -201,9 +202,8 @@ void Printer::toStreamCmdDeclareFunction(std::ostream& out, void Printer::toStreamCmdDeclareFunction(std::ostream& out, const Node& v) const { - std::stringstream vs; - vs << v; - toStreamCmdDeclareFunction(out, vs.str(), v.getType()); + std::string vs = v.getAttribute(expr::VarNameAttr()); + toStreamCmdDeclareFunction(out, vs, v.getType()); } void Printer::toStreamCmdDeclarePool(std::ostream& out, diff --git a/test/unit/api/cpp/term_black.cpp b/test/unit/api/cpp/term_black.cpp index f4180aa34..c76182e47 100644 --- a/test/unit/api/cpp/term_black.cpp +++ b/test/unit/api/cpp/term_black.cpp @@ -212,6 +212,21 @@ TEST_F(TestApiBlackTerm, getOp) ASSERT_EQ(headTerm, d_solver.mkTerm(headTerm.getOp(), children)); } +TEST_F(TestApiBlackTerm, hasGetSymbol) +{ + Term n; + Term t = d_solver.mkBoolean(true); + Term c = d_solver.mkConst(d_solver.getBooleanSort(), "|\\|"); + + ASSERT_THROW(n.hasSymbol(), CVC5ApiException); + ASSERT_FALSE(t.hasSymbol()); + ASSERT_TRUE(c.hasSymbol()); + + ASSERT_THROW(n.getSymbol(), CVC5ApiException); + ASSERT_THROW(t.getSymbol(), CVC5ApiException); + ASSERT_EQ(c.getSymbol(), "|\\|"); +} + TEST_F(TestApiBlackTerm, isNull) { Term x; diff --git a/test/unit/api/java/TermTest.java b/test/unit/api/java/TermTest.java index bf0beb024..b7f111428 100644 --- a/test/unit/api/java/TermTest.java +++ b/test/unit/api/java/TermTest.java @@ -219,6 +219,21 @@ class TermTest Term nilOpTerm = list.getConstructorTerm("nil"); } + @Test void hasGetSymbol() throws CVC5ApiException + { + Term n = d_solver.getNullTerm(); + Term t = d_solver.mkBoolean(true); + Term c = d_solver.mkConst(d_solver.getBooleanSort(), "|\\|"); + + assertThrows(CVC5ApiException.class, () -> n.hasSymbol()); + assertFalse(t.hasSymbol()); + assertTrue(c.hasSymbol()); + + assertThrows(CVC5ApiException.class, () -> n.getSymbol()); + assertThrows(CVC5ApiException.class, () -> t.getSymbol()); + assertEquals(c.getSymbol(), "|\\|"); + } + @Test void isNull() throws CVC5ApiException { Term x = d_solver.getNullTerm(); diff --git a/test/unit/api/python/test_term.py b/test/unit/api/python/test_term.py index 34a79d597..49314638f 100644 --- a/test/unit/api/python/test_term.py +++ b/test/unit/api/python/test_term.py @@ -208,6 +208,23 @@ def test_get_op(solver): assert headTerm == solver.mkTerm(headTerm.getOp(), children) +def test_has_get_symbol(solver): + n = Term(solver) + t = solver.mkBoolean(True) + c = solver.mkConst(solver.getBooleanSort(), "|\\|") + + with pytest.raises(RuntimeError): + n.hasSymbol() + assert not t.hasSymbol() + assert c.hasSymbol() + + with pytest.raises(RuntimeError): + n.getSymbol() + with pytest.raises(RuntimeError): + t.getSymbol() + assert c.getSymbol() == "|\\|" + + def test_is_null(solver): x = Term(solver) assert x.isNull() -- 2.30.2