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 a4333c81d4f6b44630e29a3e161647254aa4e65b..5aa9079b918f464bcfd1fb2a76913891fd4bd750 100644 (file)
--- 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 5afb2c3169e4b79217d3257872a0963ee189cf18..d6b5af3242bd759cf38c324bb2a953bc38a20473 100644 (file)
--- 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 73357bdef829409553d4e67e8a8f1728831e3122..320496b9128209c1333344bc6fc521619980c027 100644 (file)
--- 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<Rational>();
-      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<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() << ')';
-      //   }
-      // }
+      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<AscriptionType>().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<AscriptionType>().getType());
-      if(t.getKind() == kind::TYPE_CONSTANT &&
-         t.getConst<TypeConstant>() == 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<Rational>(), 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<Node>* 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<const theory::TheoryModel*>(&model);
+  AlwaysAssert(theory_model != nullptr);
+  if (const DeclareTypeCommand* dtc =
+          dynamic_cast<const DeclareTypeCommand*>(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<Node>* 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<const DeclareFunctionCommand*>(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<Node>* 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<Rational>(), 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<Node>* 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<const theory::TheoryModel*>(&model);
-  AlwaysAssert(theory_model != nullptr);
-  if (const DeclareTypeCommand* dtc =
-          dynamic_cast<const DeclareTypeCommand*>(command))
-  {
-    DeclareTypeCommandToStream(out, *theory_model, *dtc, d_variant);
-  }
-  else if (const DeclareFunctionCommand* dfc =
-               dynamic_cast<const DeclareFunctionCommand*>(command))
-  {
-    DeclareFunctionCommandToStream(out, *theory_model, *dfc);
   }
   else if (const DatatypeDeclarationCommand* datatype_declaration_command =
                dynamic_cast<const DatatypeDeclarationCommand*>(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 8472219794f434dfe148fb71744d68498449eaeb..f8e28a994bb7b44bb534db62e24d1ecdb32cb422 100644 (file)
--- 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 53337c5d39c84e5813fa4fc8d7e311d11bb17450..8dec350733aa3876a6db944029fb3dd5ad3ee111 100644 (file)
--- 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 48767015852194c6a7401190c438d0fd12058aa6..6fa5426682edc8bbc137dae7180b6c609e5cb56c 100644 (file)
--- 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))