Repository: dreal/dreal4 (language: python)

Issue:
ToPrefix generates non-SMTLIB-compliant strings
- A negative constant `-c` should be formatted as `(- c)`. https://github.com/dreal/dreal4/blob/db12dd0ff02c34701aec8f7061947c6706d217db/dreal/symbolic/prefix_printer.cc#L50-L58


Discussion / hints:

Fix patch:
diff --git a/dreal/symbolic/prefix_printer.cc b/dreal/symbolic/prefix_printer.cc
index 53b55851..16550824 100644
--- a/dreal/symbolic/prefix_printer.cc
+++ b/dreal/symbolic/prefix_printer.cc
@@ -26,6 +26,17 @@ using std::string;
 
 namespace dreal {
 
+namespace {
+ostream& print_constant(ostream& os, double c) {
+  if (c >= 0) {
+    return os << c;
+  } else {
+    return os << "(- " << (-c) << ")";
+  }
+}
+
+}  // namespace
+
 PrefixPrinter::PrefixPrinter(ostream& os)
     : os_{os}, old_precision_{os.precision()} {
   // See
@@ -48,13 +59,13 @@ ostream& PrefixPrinter::VisitVariable(const Expression& e) {
 }
 
 ostream& PrefixPrinter::VisitConstant(const Expression& e) {
-  return os_ << get_constant_value(e);
+  return print_constant(os_, get_constant_value(e));
 }
 
 ostream& PrefixPrinter::VisitRealConstant(const Expression& e) {
   const double mid{get_lb_of_real_constant(e) / 2.0 +
                    get_ub_of_real_constant(e) / 2.0};
-  return os_ << mid;
+  return print_constant(os_, mid);
 }
 
 ostream& PrefixPrinter::VisitUnaryFunction(const std::string& name,
@@ -77,7 +88,8 @@ ostream& PrefixPrinter::VisitAddition(const Expression& e) {
   const double constant{get_constant_in_addition(e)};
   os_ << "(+";
   if (constant != 0.0) {
-    os_ << " " << constant;
+    os_ << " ";
+    print_constant(os_, constant);
   }
   for (const auto& p : get_expr_to_coeff_map_in_addition(e)) {
     const Expression& e_i{p.first};
@@ -86,7 +98,9 @@ ostream& PrefixPrinter::VisitAddition(const Expression& e) {
     if (c_i == 1.0) {
       Print(e_i);
     } else {
-      os_ << "(* " << c_i << " ";
+      os_ << "(* ";
+      print_constant(os_, c_i);
+      os_ << " ";
       Print(e_i);
       os_ << ")";
     }
@@ -98,7 +112,8 @@ ostream& PrefixPrinter::VisitMultiplication(const Expression& e) {
   const double constant{get_constant_in_multiplication(e)};
   os_ << "(*";
   if (constant != 1.0) {
-    os_ << " " << constant;
+    os_ << " ";
+    print_constant(os_, constant);
   }
   for (const auto& p : get_base_to_exponent_map_in_multiplication(e)) {
     const Expression& b_i{p.first};


Test patch:
diff --git a/dreal/symbolic/test/prefix_printer_test.cc b/dreal/symbolic/test/prefix_printer_test.cc
index 5ed0dec2..03c79a26 100644
--- a/dreal/symbolic/test/prefix_printer_test.cc
+++ b/dreal/symbolic/test/prefix_printer_test.cc
@@ -52,14 +52,24 @@ TEST_F(PrefixPrinterTest, Constant2) {
   EXPECT_EQ(ToPrefix(e), "3.141592653589793116");
 }
 
+TEST_F(PrefixPrinterTest, Constant3) {
+  const Expression e{-3.0};
+  EXPECT_EQ(ToPrefix(e), "(- 3)");
+}
+
+TEST_F(PrefixPrinterTest, Constant4) {
+  const Expression e{-M_PI};
+  EXPECT_EQ(ToPrefix(e), "(- 3.141592653589793116)");
+}
+
 TEST_F(PrefixPrinterTest, Addition) {
-  const Expression e{x_ + 2 * y_ + 3 * z_};
-  EXPECT_EQ(ToPrefix(e), "(+ x (* 2 y) (* 3 z))");
+  const Expression e{-3 + x_ - 2 * y_ + 3 * z_};
+  EXPECT_EQ(ToPrefix(e), "(+ (- 3) x (* (- 2) y) (* 3 z))");
 }
 
 TEST_F(PrefixPrinterTest, Multiplication) {
-  const Expression e{pow(x_, 2) * 2 * y_ * 3 * pow(z_, 5)};
-  EXPECT_EQ(ToPrefix(e), "(* 6 (^ x 2) y (^ z 5))");
+  const Expression e{-2 * pow(x_, -2) * 2 * y_ * 3 * pow(z_, 5)};
+  EXPECT_EQ(ToPrefix(e), "(* (- 12) (^ x (- 2)) y (^ z 5))");
 }
 
 TEST_F(PrefixPrinterTest, Division) {