Add an API method to get the raw name of a term. (#7618)

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 7976c19ef2073b1fb577d85a42cb2650f43983f3..18879a4eb9495e14789a6f15443c57e4afe25ac9 100644 (file)
--- 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 ab9a4de25c33a0f2a73ce120580bea200f3c5ae9..46678b0d8757dc1e83c78cac469cb378b6fcd1a1 100644 (file)
--- 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 bbed609f7f3b4413098ce9f8718151c41b896094..fc09767eda3df7fe8912d7f1361664b0b9f7b609 100644 (file)
--- 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<Term>, 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 d54b0a2b57d05cf5833b46049215990ce579a4dd..702a5064d408895f55b9c01349871eabe070c621 100644 (file)
--- 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<Term*>(pointer);
+  return static_cast<jboolean>(current->hasSymbol());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(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<Term*>(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 9dae7da969c914dbed993b444f99085e38bf1f9d..f5dc2aca22b2870aa7cc988ca0cd4f93875da747 100644 (file)
--- 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 1df252e8635ca9340cc428916564c92880eec327..3d24b5dbdd72a7225eabac72b33f044b36997f3b 100644 (file)
--- 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 b66ae57289694d5deda1bfb4ad25eb6babaaf757..16b626e3046926e030b174bcffb8f72c5f572e02 100644 (file)
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -16,6 +16,7 @@
 
 #include <string>
 
+#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 f4180aa3497b81e8145220612add301ca8e1a614..c76182e479e597eb4a18941f277096aecded71d5 100644 (file)
--- 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 bf0beb024486b556f331f87ebef7470b06257c98..b7f11142807c20f61bb48572579020866c963364 100644 (file)
--- 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 34a79d59727e19a9f2fffa4fefb39342eaedf6fb..49314638f9832ca453ef58bd94e51c8f91121cae 100644 (file)
--- 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()