Merge branch 'master' into fix_warnsfix_warns

6 files changed, 84 insertions, 185 deletions

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index d778ccc2b..f9cd7db83 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -385,6 +385,12 @@ void CvcPrinter::toStream(
           return;
         }else{
           toStream(op, n.getOperator(), depth, types, false);
+          if (n.getNumChildren() == 0)
+          {
+            // for datatype constants d, we print "d" and not "d()"
+            out << op.str();
+            return;
+          }
         }
       }
       break;
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index e8ebadeb8..439649725 100644
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -21,7 +21,6 @@
 #include "options/language.h"
 #include "printer/ast/ast_printer.h"
 #include "printer/cvc/cvc_printer.h"
-#include "printer/smt1/smt1_printer.h"
 #include "printer/smt2/smt2_printer.h"
 #include "printer/tptp/tptp_printer.h"
 
@@ -36,9 +35,6 @@ unique_ptr<Printer> Printer::makePrinter(OutputLanguage lang)
   using namespace CVC4::language::output;
 
   switch(lang) {
-  case LANG_SMTLIB_V1: // TODO the printer
-    return unique_ptr<Printer>(new printer::smt1::Smt1Printer());
-
   case LANG_SMTLIB_V2_0:
     return unique_ptr<Printer>(
         new printer::smt2::Smt2Printer(printer::smt2::smt2_0_variant));
@@ -50,6 +46,10 @@ unique_ptr<Printer> Printer::makePrinter(OutputLanguage lang)
     return unique_ptr<Printer>(
         new printer::smt2::Smt2Printer(printer::smt2::smt2_6_variant));
 
+  case LANG_SMTLIB_V2_6_1:
+    return unique_ptr<Printer>(
+        new printer::smt2::Smt2Printer(printer::smt2::smt2_6_1_variant));
+
   case LANG_TPTP:
     return unique_ptr<Printer>(new printer::tptp::TptpPrinter());
 
diff --git a/src/printer/smt1/smt1_printer.cpp b/src/printer/smt1/smt1_printer.cpp
deleted file mode 100644
index ac3c2f970..000000000
--- a/src/printer/smt1/smt1_printer.cpp
+++ /dev/null
@@ -1,69 +0,0 @@
-/*********************                                                        */
-/*! \file smt1_printer.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Tim King, Paul Meng
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief The pretty-printer interface for the SMT output language
- **
- ** The pretty-printer interface for the SMT output language.
- **/
-#include "printer/smt1/smt1_printer.h"
-
-#include <iostream>
-#include <string>
-#include <typeinfo>
-#include <vector>
-
-#include "expr/expr.h" // for ExprSetDepth etc..
-#include "expr/node_manager.h" // for VarNameAttr
-#include "options/language.h" // for LANG_AST
-#include "smt/command.h"
-
-using namespace std;
-
-namespace CVC4 {
-namespace printer {
-namespace smt1 {
-
-void Smt1Printer::toStream(
-    std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const
-{
-  n.toStream(out, toDepth, types, dag, language::output::LANG_SMTLIB_V2_5);
-}/* Smt1Printer::toStream() */
-
-void Smt1Printer::toStream(std::ostream& out,
-                           const Command* c,
-                           int toDepth,
-                           bool types,
-                           size_t dag) const
-{
-  c->toStream(out, toDepth, types, dag, language::output::LANG_SMTLIB_V2_5);
-}/* Smt1Printer::toStream() */
-
-void Smt1Printer::toStream(std::ostream& out, const CommandStatus* s) const
-{
-  s->toStream(out, language::output::LANG_SMTLIB_V2_5);
-}/* Smt1Printer::toStream() */
-
-void Smt1Printer::toStream(std::ostream& out, const Model& m) const
-{
-  Printer::getPrinter(language::output::LANG_SMTLIB_V2_5)->toStream(out, m);
-}
-
-void Smt1Printer::toStream(std::ostream& out,
-                           const Model& m,
-                           const Command* c) const
-{
-  // shouldn't be called; only the non-Command* version above should be
-  Unreachable();
-}
-
-}/* CVC4::printer::smt1 namespace */
-}/* CVC4::printer namespace */
-}/* CVC4 namespace */
diff --git a/src/printer/smt1/smt1_printer.h b/src/printer/smt1/smt1_printer.h
deleted file mode 100644
index 560393b81..000000000
--- a/src/printer/smt1/smt1_printer.h
+++ /dev/null
@@ -1,57 +0,0 @@
-/*********************                                                        */
-/*! \file smt1_printer.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Paul Meng
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief The pretty-printer interface for the SMT output language
- **
- ** The pretty-printer interface for the SMT output language.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__PRINTER__SMT1_PRINTER_H
-#define __CVC4__PRINTER__SMT1_PRINTER_H
-
-#include <iostream>
-
-#include "printer/printer.h"
-
-namespace CVC4 {
-namespace printer {
-namespace smt1 {
-
-class Smt1Printer : public CVC4::Printer {
- public:
-  using CVC4::Printer::toStream;
-  void toStream(std::ostream& out,
-                TNode n,
-                int toDepth,
-                bool types,
-                size_t dag) const override;
-  void toStream(std::ostream& out,
-                const Command* c,
-                int toDepth,
-                bool types,
-                size_t dag) const override;
-  void toStream(std::ostream& out, const CommandStatus* s) const override;
-  void toStream(std::ostream& out, const Model& m) const override;
-
- private:
-  void toStream(std::ostream& out,
-                const Model& m,
-                const Command* c) const override;
-  void toStream(std::ostream& out, const SExpr& sexpr) const;
-};/* class Smt1Printer */
-
-}/* CVC4::printer::smt1 namespace */
-}/* CVC4::printer namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__PRINTER__SMT1_PRINTER_H */
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 8c9680a74..5d2b8972d 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -42,7 +42,13 @@ namespace smt2 {
 
 static OutputLanguage variantToLanguage(Variant v);
 
-static string smtKindString(Kind k);
+static string smtKindString(Kind k, Variant v);
+
+/** returns whether the variant is smt-lib 2.6 or greater */
+bool isVariant_2_6(Variant v)
+{
+  return v == smt2_6_variant || v == smt2_6_1_variant;
+}
 
 static void printBvParameterizedOp(std::ostream& out, TNode n);
 static void printFpParameterizedOp(std::ostream& out, TNode n);
@@ -191,10 +197,10 @@ void Smt2Printer::toStream(std::ostream& out,
       out << (n.getConst<bool>() ? "true" : "false");
       break;
     case kind::BUILTIN:
-      out << smtKindString(n.getConst<Kind>());
+      out << smtKindString(n.getConst<Kind>(), d_variant);
       break;
     case kind::CHAIN_OP:
-      out << smtKindString(n.getConst<Chain>().getOperator());
+      out << smtKindString(n.getConst<Chain>().getOperator(), d_variant);
       break;
     case kind::CONST_RATIONAL: {
       const Rational& r = n.getConst<Rational>();
@@ -323,7 +329,8 @@ void Smt2Printer::toStream(std::ostream& out,
       if (force_nt.isReal())
       {
         out << "(" << smtKindString(force_nt.isInteger() ? kind::TO_INTEGER
-                                                         : kind::TO_REAL)
+                                                         : kind::TO_REAL,
+                                    d_variant)
             << " ";
         toStream(out, n, toDepth, types, TypeNode::null());
         out << ")";
@@ -385,8 +392,8 @@ void Smt2Printer::toStream(std::ostream& out,
     // builtin theory
   case kind::APPLY: break;
   case kind::EQUAL:
-  case kind::DISTINCT: 
-    out << smtKindString(k) << " "; 
+  case kind::DISTINCT:
+    out << smtKindString(k, d_variant) << " ";
     parametricTypeChildren = true;
     break;
   case kind::CHAIN: break;
@@ -407,14 +414,16 @@ void Smt2Printer::toStream(std::ostream& out,
   case kind::IMPLIES:
   case kind::OR:
   case kind::XOR:
-  case kind::ITE: out << smtKindString(k) << " "; break;
+  case kind::ITE:
+    out << smtKindString(k, d_variant) << " ";
+    break;
 
-    // uf theory
+  // uf theory
   case kind::APPLY_UF: typeChildren = true; break;
   // higher-order
   case kind::HO_APPLY: break;
   case kind::LAMBDA:
-    out << smtKindString(k) << " ";
+    out << smtKindString(k, d_variant) << " ";
     break;
 
   // arith theory
@@ -453,7 +462,7 @@ void Smt2Printer::toStream(std::ostream& out,
   case kind::TO_REAL:
   case kind::POW: 
     parametricTypeChildren = true;
-    out << smtKindString(k) << " "; 
+    out << smtKindString(k, d_variant) << " ";
     break;
 
   case kind::DIVISIBLE:
@@ -466,9 +475,11 @@ void Smt2Printer::toStream(std::ostream& out,
   case kind::STORE: typeChildren = true;
   case kind::PARTIAL_SELECT_0:
   case kind::PARTIAL_SELECT_1:
-  case kind::ARRAY_TYPE: out << smtKindString(k) << " "; break;
+  case kind::ARRAY_TYPE:
+    out << smtKindString(k, d_variant) << " ";
+    break;
 
-    // string theory
+  // string theory
   case kind::STRING_CONCAT:
     if(d_variant == z3str_variant) {
       out << "Concat ";
@@ -499,30 +510,30 @@ void Smt2Printer::toStream(std::ostream& out,
       out << ")";
       return;
     }
-    out << "str.in.re ";
+    out << smtKindString(k, d_variant) << " ";
     break;
   }
-  case kind::STRING_LENGTH: out << (d_variant == z3str_variant ? "Length " : "str.len "); break;
-  case kind::STRING_SUBSTR: out << "str.substr "; break;
-  case kind::STRING_CHARAT: out << "str.at "; break;
-  case kind::STRING_STRCTN: out << "str.contains "; break;
-  case kind::STRING_STRIDOF: out << "str.indexof "; break;
-  case kind::STRING_STRREPL: out << "str.replace "; break;
-  case kind::STRING_PREFIX: out << "str.prefixof "; break;
-  case kind::STRING_SUFFIX: out << "str.suffixof "; break;
-  case kind::STRING_ITOS: out << "int.to.str "; break;
-  case kind::STRING_STOI: out << "str.to.int "; break;
-  case kind::STRING_TO_REGEXP: out << "str.to.re "; break;
-  case kind::REGEXP_CONCAT: out << "re.++ "; break;
-  case kind::REGEXP_UNION: out << "re.union "; break;
-  case kind::REGEXP_INTER: out << "re.inter "; break;
-  case kind::REGEXP_STAR: out << "re.* "; break;
-  case kind::REGEXP_PLUS: out << "re.+ "; break;
-  case kind::REGEXP_OPT: out << "re.opt "; break;
-  case kind::REGEXP_RANGE: out << "re.range "; break;
-  case kind::REGEXP_LOOP: out << "re.loop "; break;
-  case kind::REGEXP_EMPTY: out << "re.nostr "; break;
-  case kind::REGEXP_SIGMA: out << "re.allchar "; break;
+  case kind::STRING_LENGTH:
+  case kind::STRING_SUBSTR:
+  case kind::STRING_CHARAT:
+  case kind::STRING_STRCTN:
+  case kind::STRING_STRIDOF:
+  case kind::STRING_STRREPL:
+  case kind::STRING_PREFIX:
+  case kind::STRING_SUFFIX:
+  case kind::STRING_ITOS:
+  case kind::STRING_STOI:
+  case kind::STRING_TO_REGEXP:
+  case kind::REGEXP_CONCAT:
+  case kind::REGEXP_UNION:
+  case kind::REGEXP_INTER:
+  case kind::REGEXP_STAR:
+  case kind::REGEXP_PLUS:
+  case kind::REGEXP_OPT:
+  case kind::REGEXP_RANGE:
+  case kind::REGEXP_LOOP:
+  case kind::REGEXP_EMPTY:
+  case kind::REGEXP_SIGMA: out << smtKindString(k, d_variant) << " "; break;
 
   case kind::CARDINALITY_CONSTRAINT: out << "fmf.card "; break;
   case kind::CARDINALITY_VALUE: out << "fmf.card.val "; break;
@@ -586,12 +597,12 @@ void Smt2Printer::toStream(std::ostream& out,
   case kind::TRANSPOSE:
   case kind::TCLOSURE:
     parametricTypeChildren = true;
-    out << smtKindString(k) << " "; 
+    out << smtKindString(k, d_variant) << " ";
     break;
   case kind::MEMBER: typeChildren = true;
   case kind::SET_TYPE:
   case kind::SINGLETON:
-  case kind::COMPLEMENT:out << smtKindString(k) << " "; break;
+  case kind::COMPLEMENT: out << smtKindString(k, d_variant) << " "; break;
   case kind::UNIVERSE_SET:out << "(as univset " << n.getType() << ")";break;
 
     // fp theory
@@ -621,7 +632,8 @@ void Smt2Printer::toStream(std::ostream& out,
   case kind::FLOATINGPOINT_ISNEG:
   case kind::FLOATINGPOINT_ISPOS:
   case kind::FLOATINGPOINT_TO_REAL:
-    out << smtKindString(k) << ' '; break;
+    out << smtKindString(k, d_variant) << ' ';
+    break;
 
   case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR:
   case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT:
@@ -681,7 +693,7 @@ void Smt2Printer::toStream(std::ostream& out,
     case kind::SEP_EMP:
     case kind::SEP_PTO:
     case kind::SEP_STAR:
-    case kind::SEP_WAND: out << smtKindString(k) << " "; break;
+    case kind::SEP_WAND: out << smtKindString(k, d_variant) << " "; break;
 
     case kind::SEP_NIL:
       out << "(as sep.nil " << n.getType() << ")";
@@ -773,7 +785,8 @@ void Smt2Printer::toStream(std::ostream& out,
       }else if( n.getKind()==kind::APPLY_TESTER ){
         unsigned cindex = Datatype::indexOf(n.getOperator().toExpr());
         const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr());
-        if( d_variant==smt2_6_variant ){
+        if (isVariant_2_6(d_variant))
+        {
           out << "(_ is ";
           toStream(out, Node::fromExpr(dt[cindex].getConstructor()), toDepth < 0 ? toDepth : toDepth - 1, types, TypeNode::null());
           out << ")";
@@ -856,7 +869,7 @@ void Smt2Printer::toStream(std::ostream& out,
       if(forceBinary && i < n.getNumChildren() - 1) {
         // not going to work properly for parameterized kinds!
         Assert(n.getMetaKind() != kind::metakind::PARAMETERIZED);
-        out << " (" << smtKindString(n.getKind()) << ' ';
+        out << " (" << smtKindString(n.getKind(), d_variant) << ' ';
         parens << ')';
         ++c;
       } else {
@@ -869,7 +882,7 @@ void Smt2Printer::toStream(std::ostream& out,
   }
 }/* Smt2Printer::toStream(TNode) */
 
-static string smtKindString(Kind k)
+static string smtKindString(Kind k, Variant v)
 {
   switch(k) {
     // builtin theory
@@ -1039,7 +1052,7 @@ static string smtKindString(Kind k)
 
   //string theory
   case kind::STRING_CONCAT: return "str.++";
-  case kind::STRING_LENGTH: return "str.len";
+  case kind::STRING_LENGTH: return v == z3str_variant ? "Length" : "str.len";
   case kind::STRING_SUBSTR: return "str.substr" ;
   case kind::STRING_STRCTN: return "str.contains" ;
   case kind::STRING_CHARAT: return "str.at" ;
@@ -1047,10 +1060,14 @@ static string smtKindString(Kind k)
   case kind::STRING_STRREPL: return "str.replace" ;
   case kind::STRING_PREFIX: return "str.prefixof" ;
   case kind::STRING_SUFFIX: return "str.suffixof" ;
-  case kind::STRING_ITOS: return "int.to.str" ;
-  case kind::STRING_STOI: return "str.to.int" ;
-  case kind::STRING_IN_REGEXP: return "str.in.re";
-  case kind::STRING_TO_REGEXP: return "str.to.re";
+  case kind::STRING_ITOS:
+    return v == smt2_6_1_variant ? "str.from-int" : "int.to.str";
+  case kind::STRING_STOI:
+    return v == smt2_6_1_variant ? "str.to-int" : "str.to.int";
+  case kind::STRING_IN_REGEXP:
+    return v == smt2_6_1_variant ? "str.in-re" : "str.in.re";
+  case kind::STRING_TO_REGEXP:
+    return v == smt2_6_1_variant ? "str.to-re" : "str.to.re";
   case kind::REGEXP_CONCAT: return "re.++";
   case kind::REGEXP_UNION: return "re.union";
   case kind::REGEXP_INTER: return "re.inter";
@@ -1310,7 +1327,7 @@ void DeclareTypeCommandToStream(std::ostream& out,
   const std::vector<Node>* type_refs = model.getRepSet()->getTypeRepsOrNull(tn);
   if (options::modelUninterpDtEnum() && tn.isSort() && type_refs != nullptr)
   {
-    if (variant == smt2_6_variant)
+    if (isVariant_2_6(variant))
     {
       out << "(declare-datatypes ((" << command.getSymbol() << " 0)) (";
     }
@@ -1893,7 +1910,7 @@ static void toStream(std::ostream& out,
     out << "co";
   }
   out << "datatypes";
-  if (v == smt2_6_variant)
+  if (isVariant_2_6(v))
   {
     out << " (";
     for (vector<DatatypeType>::const_iterator i = datatypes.begin(),
diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
index 922b69a9e..1d281aed4 100644
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -27,14 +27,16 @@ namespace CVC4 {
 namespace printer {
 namespace smt2 {
 
-enum Variant {
+enum Variant
+{
   no_variant,
-  smt2_0_variant, // old-style 2.0 syntax, when it makes a difference
-  smt2_6_variant, // new-style 2.6 syntax, when it makes a difference
-  z3str_variant, // old-style 2.0 and also z3str syntax
-  sygus_variant  // variant for sygus
-};/* enum Variant */
-
+  smt2_0_variant,    // old-style 2.0 syntax, when it makes a difference
+  smt2_6_variant,    // new-style 2.6 syntax, when it makes a difference
+  smt2_6_1_variant,  // new-style 2.6 syntax, when it makes a difference, with
+                     // support for the string standard
+  z3str_variant,     // old-style 2.0 and also z3str syntax
+  sygus_variant      // variant for sygus
+};                   /* enum Variant */
 class Smt2Printer : public CVC4::Printer {
  public:
   Smt2Printer(Variant variant = no_variant) : d_variant(variant) { }