From: Andrew Reynolds Date: Mon, 21 May 2018 22:52:26 +0000 (-0500) Subject: Improvements in parsing and printing related to mixed int/real (#1879) X-Git-Tag: cvc5-1.0.0~5028 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e50e09efa679c2d0c835cbf794a7b0743347552a;p=cvc5.git Improvements in parsing and printing related to mixed int/real (#1879) This eliminates some hacks for dealing with Int/Real. - Eliminates the use of "to_real" to cast decimals like "2.0" that happen to be Int. We now replace these by (/ 2 1) instead of (to_real 2), which has the advantage of being smt-lib compliant for all theories, including QF_LRA. - Eliminates the use of a hack to use "type ascriptions" when returning values from a get-value command. Instead, we use division with 1 when necessary. This affects the output of a few regressions, but we remain smt-lib compliant. - Addresses a bug with printing arbitrary type ascriptions for smt2 terms. This partially addresses #1852. - Updates our printing of negative rationals to be (/ (- n) m) instead of (- (/ n m)), which is consistent with the smt lib standard for real values (http://smtlib.cs.uiowa.edu/theories-Reals.shtml). --- diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index a4333c81d..5aa9079b9 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -2164,7 +2164,10 @@ simpleTerm[CVC4::Expr& f] | DECIMAL_LITERAL { f = MK_CONST(AntlrInput::tokenToRational($DECIMAL_LITERAL)); if(f.getType().isInteger()) { - f = MK_EXPR(kind::TO_REAL, f); + // Must cast to Real to ensure correct type is passed to parametric type constructors. + // We do this cast using division with 1. + // This has the advantage wrt using TO_REAL since (constant) division is always included in the theory. + f = MK_EXPR(kind::DIVISION, f, MK_CONST(Rational(1))); } } | INTEGER_LITERAL { f = MK_CONST(AntlrInput::tokenToInteger($INTEGER_LITERAL)); } diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 5afb2c316..d6b5af324 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -2310,8 +2310,10 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] // valid GMP rational string expr = MK_CONST( AntlrInput::tokenToRational($DECIMAL_LITERAL) ); if(expr.getType().isInteger()) { - //must cast to Real to ensure correct type is passed to parametric type constructors - expr = MK_EXPR(kind::TO_REAL, expr); + // Must cast to Real to ensure correct type is passed to parametric type constructors. + // We do this cast using division with 1. + // This has the advantage wrt using TO_REAL since (constant) division is always included in the theory. + expr = MK_EXPR(kind::DIVISION, expr, MK_CONST(Rational(1))); } } diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 73357bdef..320496b91 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -55,7 +55,8 @@ static void printFpParameterizedOp(std::ostream& out, TNode n); static void toStreamRational(std::ostream& out, const Rational& r, - bool decimal); + bool decimal, + Variant v); void Smt2Printer::toStream( std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const @@ -204,29 +205,8 @@ void Smt2Printer::toStream(std::ostream& out, break; case kind::CONST_RATIONAL: { const Rational& r = n.getConst(); - if(d_variant == sygus_variant ){ - if(r < 0) { - out << "-" << -r; - }else{ - toStreamRational(out, r, !force_nt.isNull() && !force_nt.isInteger()); - } - }else{ - toStreamRational(out, r, !force_nt.isNull() && !force_nt.isInteger()); - } - // 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() << ')'; - // } - // } + toStreamRational( + out, r, !force_nt.isNull() && !force_nt.isInteger(), d_variant); break; } @@ -322,30 +302,51 @@ void Smt2Printer::toStream(std::ostream& out, return; } - if (!force_nt.isNull()) + // determine if we are printing out a type ascription, store the argument of + // the type ascription into type_asc_arg. + Node type_asc_arg; + if (n.getKind() == kind::APPLY_TYPE_ASCRIPTION) + { + force_nt = TypeNode::fromType( + n.getOperator().getConst().getType()); + type_asc_arg = n[0]; + } + else if (!force_nt.isNull() && n.getType() != force_nt) { - if (n.getType() != force_nt) + type_asc_arg = n; + } + if (!type_asc_arg.isNull()) + { + if (force_nt.isReal()) { - if (force_nt.isReal()) + // we prefer using (/ x 1) instead of (to_real x) here. + // the reason is that (/ x 1) is SMT-LIB compliant when x is a constant + // or the logic is non-linear, whereas (to_real x) is compliant when + // the logic is mixed int/real. The former occurs more frequently. + bool is_int = force_nt.isInteger(); + out << "(" + << smtKindString(is_int ? kind::TO_INTEGER : kind::DIVISION, + d_variant) + << " "; + toStream(out, type_asc_arg, toDepth, types, TypeNode::null()); + if (!is_int) { - out << "(" << smtKindString(force_nt.isInteger() ? kind::TO_INTEGER - : kind::TO_REAL, - d_variant) - << " "; - toStream(out, n, toDepth, types, TypeNode::null()); - out << ")"; + out << " 1"; } - else - { - Node nn = NodeManager::currentNM()->mkNode( - kind::APPLY_TYPE_ASCRIPTION, - NodeManager::currentNM()->mkConst( - AscriptionType(force_nt.toType())), - n); - toStream(out, nn, toDepth, types, TypeNode::null()); - } - return; + out << ")"; + } + else + { + // use type ascription + out << "(as "; + toStream(out, + type_asc_arg, + toDepth < 0 ? toDepth : toDepth - 1, + types, + TypeNode::null()); + out << " " << force_nt << ")"; } + return; } // variable @@ -659,31 +660,6 @@ void Smt2Printer::toStream(std::ostream& out, stillNeedToPrintParams = false; break; - // datatypes - case kind::APPLY_TYPE_ASCRIPTION: { - TypeNode t = TypeNode::fromType(n.getOperator().getConst().getType()); - if(t.getKind() == kind::TYPE_CONSTANT && - t.getConst() == REAL_TYPE && - 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. - - // 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 "; - toStream(out, n[0], toDepth < 0 ? toDepth : toDepth - 1, types, TypeNode::null()); - out << ' ' << (t.isFunctionLike() ? t.getRangeType() : t) << ')'; - return; - } - break; - case kind::APPLY_CONSTRUCTOR: { typeChildren = true; @@ -1349,127 +1325,106 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m) const } } -namespace { - -void DeclareTypeCommandToStream(std::ostream& out, - const theory::TheoryModel& model, - const DeclareTypeCommand& command, - Variant variant) +void Smt2Printer::toStream(std::ostream& out, + const Model& model, + const Command* command) const { - TypeNode tn = TypeNode::fromType(command.getType()); - const std::vector* type_refs = model.getRepSet()->getTypeRepsOrNull(tn); - if (options::modelUninterpDtEnum() && tn.isSort() && type_refs != nullptr) - { - if (isVariant_2_6(variant)) - { - out << "(declare-datatypes ((" << command.getSymbol() << " 0)) ("; - } - else - { - out << "(declare-datatypes () ((" << command.getSymbol() << " "; - } - for (Node type_ref : *type_refs) - { - out << "(" << type_ref << ")"; - } - out << ")))" << endl; - } - else if (tn.isSort() && type_refs != nullptr) + const theory::TheoryModel* theory_model = + dynamic_cast(&model); + AlwaysAssert(theory_model != nullptr); + if (const DeclareTypeCommand* dtc = + dynamic_cast(command)) { - // print the cardinality - out << "; cardinality of " << tn << " is " << type_refs->size() << endl; - out << command << endl; - // print the representatives - for (Node type_ref : *type_refs) + // print out the DeclareTypeCommand + TypeNode tn = TypeNode::fromType((*dtc).getType()); + const std::vector* type_refs = + theory_model->getRepSet()->getTypeRepsOrNull(tn); + if (options::modelUninterpDtEnum() && tn.isSort() && type_refs != nullptr) { - if (type_ref.isVar()) + if (isVariant_2_6(d_variant)) { - out << "(declare-fun " << quoteSymbol(type_ref) << " () " << tn << ")" - << endl; + out << "(declare-datatypes ((" << (*dtc).getSymbol() << " 0)) ("; } else { - out << "; rep: " << type_ref << endl; + out << "(declare-datatypes () ((" << (*dtc).getSymbol() << " "; } + for (Node type_ref : *type_refs) + { + out << "(" << type_ref << ")"; + } + out << ")))" << endl; } - } - else - { - out << command << endl; - } -} - -void DeclareFunctionCommandToStream(std::ostream& out, - const theory::TheoryModel& model, - const DeclareFunctionCommand& command) -{ - Node n = Node::fromExpr(command.getFunction()); - if (command.getPrintInModelSetByUser()) - { - if (!command.getPrintInModel()) + else if (tn.isSort() && type_refs != nullptr) { - return; + // print the cardinality + out << "; cardinality of " << tn << " is " << type_refs->size() << endl; + out << (*dtc) << endl; + // print the representatives + for (Node type_ref : *type_refs) + { + if (type_ref.isVar()) + { + out << "(declare-fun " << quoteSymbol(type_ref) << " () " << tn << ")" + << endl; + } + else + { + out << "; rep: " << type_ref << endl; + } + } + } + else + { + out << (*dtc) << endl; } } - else if (n.getKind() == kind::SKOLEM) - { - // don't print out internal stuff - return; - } - Node val = Node::fromExpr(model.getSmtEngine()->getValue(n.toExpr())); - if (val.getKind() == kind::LAMBDA) - { - out << "(define-fun " << n << " " << val[0] << " " - << n.getType().getRangeType() << " " << val[1] << ")" << endl; - } - else + else if (const DeclareFunctionCommand* dfc = + dynamic_cast(command)) { - if (options::modelUninterpDtEnum() && val.getKind() == kind::STORE) + // print out the DeclareFunctionCommand + Node n = Node::fromExpr((*dfc).getFunction()); + if ((*dfc).getPrintInModelSetByUser()) { - TypeNode tn = val[1].getType(); - const std::vector* type_refs = - model.getRepSet()->getTypeRepsOrNull(tn); - if (tn.isSort() && type_refs != nullptr) + if (!(*dfc).getPrintInModel()) { - Cardinality indexCard(type_refs->size()); - val = theory::arrays::TheoryArraysRewriter::normalizeConstant( - val, indexCard); + return; } } - out << "(define-fun " << n << " () " << n.getType() << " "; - if (val.getType().isInteger() && n.getType().isReal() - && !n.getType().isInteger()) + else if (n.getKind() == kind::SKOLEM) + { + // don't print out internal stuff + return; + } + Node val = + Node::fromExpr(theory_model->getSmtEngine()->getValue(n.toExpr())); + if (val.getKind() == kind::LAMBDA) { - // toStreamReal(out, val, true); - toStreamRational(out, val.getConst(), true); - // out << val << ".0"; + out << "(define-fun " << n << " " << val[0] << " " + << n.getType().getRangeType() << " "; + // call toStream and force its type to be proper + toStream(out, val[1], -1, false, n.getType().getRangeType()); + out << ")" << endl; } else { - out << val; + if (options::modelUninterpDtEnum() && val.getKind() == kind::STORE) + { + TypeNode tn = val[1].getType(); + const std::vector* type_refs = + theory_model->getRepSet()->getTypeRepsOrNull(tn); + if (tn.isSort() && type_refs != nullptr) + { + Cardinality indexCard(type_refs->size()); + val = theory::arrays::TheoryArraysRewriter::normalizeConstant( + val, indexCard); + } + } + out << "(define-fun " << n << " () " << n.getType() << " "; + // call toStream and force its type to be proper + toStream(out, val, -1, false, n.getType()); + out << ")" << endl; } - out << ")" << endl; - } -} - -} // namespace - -void Smt2Printer::toStream(std::ostream& out, - const Model& model, - const Command* command) const -{ - const theory::TheoryModel* theory_model = - dynamic_cast(&model); - AlwaysAssert(theory_model != nullptr); - if (const DeclareTypeCommand* dtc = - dynamic_cast(command)) - { - DeclareTypeCommandToStream(out, *theory_model, *dtc, d_variant); - } - else if (const DeclareFunctionCommand* dfc = - dynamic_cast(command)) - { - DeclareFunctionCommandToStream(out, *theory_model, *dfc); } else if (const DatatypeDeclarationCommand* datatype_declaration_command = dynamic_cast(command)) @@ -1737,59 +1692,41 @@ static void toStream(std::ostream& out, const DefineFunctionRecCommand* c) out << ")"; } -static void toStreamRational(std::ostream& out, const Rational& r, bool decimal) +static void toStreamRational(std::ostream& out, + const Rational& r, + bool decimal, + Variant v) { 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 << "(- "; } - + // Print the rational, possibly as decimal. + // Notice that we print (/ (- 5) 3) instead of (- (/ 5 3)), + // the former is compliant with real values in the smt lib standard. if(r.isIntegral()) { - if (neg) { - out << (-r); - }else { + if (neg) + { + out << (v == sygus_variant ? "-" : "(- ") << -r; + } + else + { out << r; } if (decimal) { out << ".0"; } + if (neg) + { + out << (v == sygus_variant ? "" : ")"); + } }else{ out << "(/ "; if(neg) { Rational abs_r = (-r); - out << abs_r.getNumerator(); - if(decimal) { out << ".0"; } - out << ' ' << abs_r.getDenominator(); - if(decimal) { out << ".0"; } + out << (v == sygus_variant ? "-" : "(- ") << abs_r.getNumerator(); + out << (v == sygus_variant ? " " : ") ") << abs_r.getDenominator(); }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) diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 847221979..f8e28a994 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -1408,12 +1408,10 @@ void GetValueCommand::invoke(SmtEngine* smtEngine) Node value = Node::fromExpr(smtEngine->getValue(e)); if (value.getType().isInteger() && request.getType() == nm->realType()) { - // Need to wrap in special marker so that output printers know this + // Need to wrap in division-by-one so that output printers know this // is an integer-looking constant that really should be output as - // a rational. Necessary for SMT-LIB standards compliance, but ugly. - value = nm->mkNode(kind::APPLY_TYPE_ASCRIPTION, - nm->mkConst(AscriptionType(em->realType())), - value); + // a rational. Necessary for SMT-LIB standards compliance. + value = nm->mkNode(kind::DIVISION, value, nm->mkConst(Rational(1))); } result.push_back(nm->mkNode(kind::SEXPR, request, value).toExpr()); } diff --git a/test/regress/regress0/get-value-reals-ints.smt2 b/test/regress/regress0/get-value-reals-ints.smt2 index 53337c5d3..8dec35073 100644 --- a/test/regress/regress0/get-value-reals-ints.smt2 +++ b/test/regress/regress0/get-value-reals-ints.smt2 @@ -1,6 +1,6 @@ ; 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))) +; EXPECT: ((pos_int 5) (pos_real_int_value (/ 3 1)) (pos_rat (/ 1 3)) (zero (/ 0 1)) (neg_rat (/ (- 2) 3)) (neg_real_int_value (/ (- 2) 1)) (neg_int (- 6))) (set-info :smt-lib-version 2.0) (set-option :produce-models true) (set-logic QF_LIRA) @@ -24,4 +24,4 @@ (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 +(get-value (pos_int pos_real_int_value pos_rat zero neg_rat neg_real_int_value neg_int)) diff --git a/test/regress/regress0/get-value-reals.smt2 b/test/regress/regress0/get-value-reals.smt2 index 487670158..6fa542668 100644 --- a/test/regress/regress0/get-value-reals.smt2 +++ b/test/regress/regress0/get-value-reals.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: ; EXPECT: sat -; EXPECT: ((pos_int 3.0) (pos_rat (/ 1 3)) (zero 0.0) (neg_rat (- (/ 2 3))) (neg_int (- 2.0))) +; EXPECT: ((pos_int (/ 3 1)) (pos_rat (/ 1 3)) (zero (/ 0 1)) (neg_rat (/ (- 2) 3)) (neg_int (/ (- 2) 1))) (set-info :smt-lib-version 2.0) (set-option :produce-models true) (set-logic QF_LRA) @@ -19,4 +19,4 @@ (assert (= neg_int (- 2))) (check-sat) -(get-value (pos_int pos_rat zero neg_rat neg_int)) \ No newline at end of file +(get-value (pos_int pos_rat zero neg_rat neg_int))