summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/api/cpp/cvc5.cpp24
-rw-r--r--src/api/cpp/cvc5.h11
-rw-r--r--src/api/java/io/github/cvc5/api/Term.java21
-rw-r--r--src/api/java/jni/term.cpp30
-rw-r--r--src/api/python/cvc5.pxd2
-rw-r--r--src/api/python/cvc5.pxi6
-rw-r--r--src/printer/printer.cpp6
-rw-r--r--test/unit/api/cpp/term_black.cpp15
-rw-r--r--test/unit/api/java/TermTest.java15
-rw-r--r--test/unit/api/python/test_term.py17
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
@@ -1128,6 +1128,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
*/
bool isNull() const;
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
@@ -201,6 +201,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
*/
public boolean isNull()
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
@@ -247,6 +247,36 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Term_getOp(JNIEnv* env,
/*
* 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
* Signature: (J)Z
*/
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 <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 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()
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback