Adding tests for get-value output for arithmetic.

Fixing bug where (- 1).0 was printed by get-value. Thanks to Christoph Sticksel for the bug report.

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 72a64ab78fe05fe25f06604ec260ff9d53f24269..999dc870ff282772dd4034592488148028bd2eff 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -44,6 +44,8 @@ static string smtKindString(Kind k) throw();
 static void printBvParameterizedOp(std::ostream& out, TNode n) throw();
 static void printFpParameterizedOp(std::ostream& out, TNode n) throw();
 
+static void toStreamRational(std::ostream& out, const Rational& r, bool decimal) throw();
+  
 void Smt2Printer::toStream(std::ostream& out, TNode n,
                            int toDepth, bool types, size_t dag) const throw() {
   if(dag != 0) {
@@ -197,20 +199,22 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
       out << smtKindString(n.getConst<Chain>().getOperator());
       break;
     case kind::CONST_RATIONAL: {
-      Rational r = n.getConst<Rational>();
-      if(r < 0) {
-        if(r.isIntegral()) {
-          out << "(- " << -r << ')';
-        } else {
-          out << "(- (/ " << (-r).getNumerator() << ' ' << (-r).getDenominator() << "))";
-        }
-      } else {
-        if(r.isIntegral()) {
-          out << r;
-        } else {
-          out << "(/ " << r.getNumerator() << ' ' << r.getDenominator() << ')';
-        }
-      }
+      const Rational& r = n.getConst<Rational>();
+      toStreamRational(out, r, false);
+      // Rational r = n.getConst<Rational>();
+      // if(r < 0) {
+      //   if(r.isIntegral()) {
+      //     out << "(- " << -r << ')';
+      //   } else {
+      //     out << "(- (/ " << (-r).getNumerator() << ' ' << (-r).getDenominator() << "))";
+      //   }
+      // } else {
+      //   if(r.isIntegral()) {
+      //     out << r;
+      //   } else {
+      //     out << "(/ " << r.getNumerator() << ' ' << r.getDenominator() << ')';
+      //   }
+      // }
       break;
     }
 
@@ -522,8 +526,14 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
          n[0].getType().isInteger()) {
         // Special case, in model output integer constants that should be
         // Real-sorted are wrapped in a type ascription.  Handle that here.
-        toStream(out, n[0], -1, false);
-        out << ".0";
+
+       // Note: This is Tim making a guess about Morgan's Code.
+       Assert(n[0].getKind() == kind::CONST_RATIONAL); 
+       toStreamRational(out, n[0].getConst<Rational>(), true);
+
+        //toStream(out, n[0], -1, false);
+        //out << ".0";
+       
         return;
       }
       out << "(as ";
@@ -1043,7 +1053,9 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m, const Command* c)
       out << "(define-fun " << n << " () "
           << n.getType() << " ";
       if(val.getType().isInteger() && n.getType().isReal() && !n.getType().isInteger()) {
-        out << val << ".0";
+       //toStreamReal(out, val, true);
+       toStreamRational(out, val.getConst<Rational>(), true);
+       //out << val << ".0";   
       } else {
         out << val;
       }
@@ -1196,6 +1208,61 @@ static void toStream(std::ostream& out, const DefineFunctionCommand* c) throw()
   out << ") " << type << " " << formula << ")";
 }
 
+static void toStreamRational(std::ostream& out, const Rational& r, bool decimal) throw() {
+  bool neg = r.sgn() < 0;
+  
+  // TODO:
+  // We are currently printing (- (/ 5 3))
+  // instead of (/ (- 5) 3) which is what is in the SMT-LIB value in the theory definition.
+  // Before switching, I'll keep to what was there and send an email.
+
+  // Tim: Apologies for the ifs on one line but in this case they are cleaner.
+  
+  if (neg) { out << "(- "; }
+  
+  if(r.isIntegral()) {
+    if (neg) {
+      out << (-r);
+    }else {
+      out << r;
+    }
+    if (decimal) { out << ".0"; }
+  }else{
+    out << "(/ ";
+    if(neg) {
+      Rational abs_r = (-r);
+      out << abs_r.getNumerator();
+      if(decimal) { out << ".0"; }
+      out << ' ' << abs_r.getDenominator();
+      if(decimal) { out << ".0"; }
+    }else{
+      out << r.getNumerator();
+      if(decimal) { out << ".0"; }
+      out << ' ' << r.getDenominator();
+      if(decimal) { out << ".0"; }
+    }
+    out << ')';
+  }
+
+  if (neg) { out << ')';}
+
+  // if(r < 0) {
+  //   Rational abs_r = -r;
+  //   if(r.isIntegral()) {
+  //     out << "(- " << abs_r << ')';
+  //   } else {
+  //     out << "(- (/ " << (-r).getNumerator() << ' ' << (-r).getDenominator() << "))";
+  //   }
+  // } else {
+  //   if(r.isIntegral()) {
+  //         out << r;
+  //       } else {
+  //         out << "(/ " << r.getNumerator() << ' ' << r.getDenominator() << ')';
+  //       }
+  //     }
+}
+
+
 static void toStream(std::ostream& out, const DeclareTypeCommand* c) throw() {
   out << "(declare-sort " << c->getSymbol() << " " << c->getArity() << ")";
 }

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 128072f2438737362bb845f4c15e3f838167dda4..9003ef636cef397a96e2e44b5fe094f5ec7c6f0c 100644 (file)
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -61,6 +61,9 @@ SMT2_TESTS = \
        simplification_bug4.smt2 \
        parallel-let.smt2 \
        get-value-incremental.smt2 \
+       get-value-reals.smt2 \
+       get-value-ints.smt2 \
+       get-value-reals-ints.smt2 \
        hung13sdk_output1.smt2 \
        hung10_itesdk_output2.smt2 \
        hung10_itesdk_output1.smt2 \

diff --git a/test/regress/regress0/get-value-ints.smt2 b/test/regress/regress0/get-value-ints.smt2
new file mode 100644 (file)
index 0000000..4497b7a
--- /dev/null
+++ b/test/regress/regress0/get-value-ints.smt2
@@ -0,0 +1,19 @@
+; COMMAND-LINE:
+; EXPECT: sat
+; EXPECT: ((pos 1) (zero 0) (neg (- 6)))
+(set-info :smt-lib-version 2.0)
+(set-option :produce-models true)
+(set-logic QF_LIA)
+
+; This output changes if the smt2 printer output for Ints changes.
+
+(declare-fun pos () Int)
+(declare-fun zero () Int)
+(declare-fun neg () Int)
+
+(assert (= pos 1))
+(assert (= zero 0))
+(assert (= neg (- 6)))
+
+(check-sat)
+(get-value (pos zero neg))

diff --git a/test/regress/regress0/get-value-reals-ints.smt2 b/test/regress/regress0/get-value-reals-ints.smt2
new file mode 100644 (file)
index 0000000..53337c5
--- /dev/null
+++ b/test/regress/regress0/get-value-reals-ints.smt2
@@ -0,0 +1,27 @@
+; COMMAND-LINE:
+; EXPECT: sat
+; EXPECT: ((pos_int 5) (pos_real_int_value 3.0) (pos_rat (/ 1 3)) (zero 0.0) (neg_rat (- (/ 2 3))) (neg_real_int_value (- 2.0)) (neg_int (- 6)))
+(set-info :smt-lib-version 2.0)
+(set-option :produce-models true)
+(set-logic QF_LIRA)
+
+; This output changes if the smt2 printer output for Reals_Ints changes.
+
+(declare-fun pos_int () Int)
+(declare-fun pos_real_int_value () Real)
+(declare-fun pos_rat () Real)
+(declare-fun zero () Real)
+(declare-fun neg_rat () Real)
+(declare-fun neg_real_int_value () Real)
+(declare-fun neg_int () Int)
+
+(assert (= pos_int 5))
+(assert (= pos_real_int_value 3))
+(assert (= pos_rat (/ 1 3)))
+(assert (= zero 0))
+(assert (= neg_rat (/ (- 2) 3)))
+(assert (= neg_real_int_value (- 2)))
+(assert (= neg_int (- 6)))
+
+(check-sat)
+(get-value (pos_int pos_real_int_value pos_rat zero neg_rat neg_real_int_value neg_int))
\ No newline at end of file

diff --git a/test/regress/regress0/get-value-reals.smt2 b/test/regress/regress0/get-value-reals.smt2
new file mode 100644 (file)
index 0000000..4876701
--- /dev/null
+++ b/test/regress/regress0/get-value-reals.smt2
@@ -0,0 +1,22 @@
+; COMMAND-LINE:
+; EXPECT: sat
+; EXPECT: ((pos_int 3.0) (pos_rat (/ 1 3)) (zero 0.0) (neg_rat (- (/ 2 3))) (neg_int (- 2.0)))
+(set-info :smt-lib-version 2.0)
+(set-option :produce-models true)
+(set-logic QF_LRA)
+
+; This output changes if the smt2 printer output for Reals changes.
+(declare-fun pos_int () Real)
+(declare-fun pos_rat () Real)
+(declare-fun zero () Real)
+(declare-fun neg_rat () Real)
+(declare-fun neg_int () Real)
+
+(assert (= pos_int 3))
+(assert (= pos_rat (/ 1 3)))
+(assert (= zero 0))
+(assert (= neg_rat (/ (- 2) 3)))
+(assert (= neg_int (- 2)))
+
+(check-sat)
+(get-value (pos_int pos_rat zero neg_rat neg_int))
\ No newline at end of file