fp.to_sbv is not printed correctly #149
Description
Hello,
I've noticed a minor issue when printing terms with Kind::FP_TO_SBV and Kind::FP_TO_UBV. Here is a quick example:
#include <bitwuzla/cpp/bitwuzla.h>
#include <bitwuzla/cpp/parser.h>
#include <string>
#include <fstream>
#include <cassert>
using namespace bitwuzla;
using namespace bitwuzla::parser;
#include <gtest/gtest.h>
class BitwuzlaTest : public testing::Test {
protected:
TermManager mgr = TermManager();
Options options = Options();
Parser parser = Parser(mgr, options);
Sort sort = mgr.mk_fp_sort(8, 24);
Term rm = mgr.mk_rm_value(RoundingMode::RNE);
Term fp = mgr.mk_fp_value(sort, rm, "1");
};
TEST_F(BitwuzlaTest, fromFPtoSBVTest) {
Term t1 = mgr.mk_term(Kind::FP_TO_SBV, {rm, fp}, {32});
std::cout << t1 << std::endl; // prints ((_ to_sbv 32) RNE (fp #b0 #b01111111 #b00000000000000000000000))
// should be `fp.to_sbv`
Term t2 = parser.parse_term(t1.str());
EXPECT_EQ(t1, t2);
}
TEST_F(BitwuzlaTest, fromFPtoUBVTest) {
Term t1 = mgr.mk_term(Kind::FP_TO_UBV, {rm, fp}, {32});
std::cout << t1 << std::endl; // prints ((_ to_ubv 32) RNE (fp #b0 #b01111111 #b00000000000000000000000))
// should be `fp.to_ubv`
Term t2 = parser.parse_term(t1.str());
EXPECT_EQ(t1, t2);
}
In both tests t1.str() will print the function name without the fp. prefix. This is not the proper SMTLIB name, and it will cause the Bitwuzla parser to fail when trying to read back its own output.
Could this be fixed so that the output is always SMTLIB compliant?