From 66daf10d1bf4cb2f1846f599fe11e27312ac2069 Mon Sep 17 00:00:00 2001 From: Tim King Date: Mon, 19 Jan 2015 18:57:29 +0100 Subject: [PATCH] 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. --- src/printer/smt2/smt2_printer.cpp | 101 +++++++++++++++--- test/regress/regress0/Makefile.am | 3 + test/regress/regress0/get-value-ints.smt2 | 19 ++++ .../regress0/get-value-reals-ints.smt2 | 27 +++++ test/regress/regress0/get-value-reals.smt2 | 22 ++++ 5 files changed, 155 insertions(+), 17 deletions(-) create mode 100644 test/regress/regress0/get-value-ints.smt2 create mode 100644 test/regress/regress0/get-value-reals-ints.smt2 create mode 100644 test/regress/regress0/get-value-reals.smt2 diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 72a64ab78..999dc870f 100644 --- 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().getOperator()); break; case kind::CONST_RATIONAL: { - Rational r = n.getConst(); - 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(); + toStreamRational(out, r, false); + // Rational r = n.getConst(); + // 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(), 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(), 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 128072f24..9003ef636 100644 --- 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 index 000000000..4497b7a80 --- /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 index 000000000..53337c5d3 --- /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 index 000000000..487670158 --- /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 -- 2.30.2