* Fix ITEs and functions in CVC language printer.

* Permit "BOOL = BOOL" in CVC language parser (auto-replaced with IFF
  internally, except in strict mode).
* SExpr atoms now can be string-, integer-, or rational-valued.
* SmtEngine::setInfo(":status", ...) now properly dumps a
  SetBenchmarkStatusCommand rather than a SetInfoCommand.
* Some dumping fixes (resolves bug 313)

diff --git a/src/expr/command.h b/src/expr/command.h
index 6bb6fba3dc174d5e018649fc79cd3e92fcc3e68c..a6f22fe2010175c0f3a104a301f2e2a3b64f1fe6 100644 (file)
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -57,7 +57,7 @@ enum BenchmarkStatus {
   SMT_UNSATISFIABLE,
   /** The status of the benchmark is unknown */
   SMT_UNKNOWN
-};
+};/* enum BenchmarkStatus */
 
 std::ostream& operator<<(std::ostream& out,
                          BenchmarkStatus status) throw() CVC4_PUBLIC;

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 657a2fe2c3757515ae14d8b60046855d054bda9d..411a0aea1916ee80f685c822bb4832ce40f7e0f2 100644 (file)
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -351,7 +351,7 @@ unsigned findPivot(const std::vector<unsigned>& operators,
   return pivot;
 }/* findPivot() */
 
-Expr createPrecedenceTree(ExprManager* em,
+Expr createPrecedenceTree(Parser* parser, ExprManager* em,
                           const std::vector<CVC4::Expr>& expressions,
                           const std::vector<unsigned>& operators,
                           unsigned startIndex, unsigned stopIndex) {
@@ -368,17 +368,20 @@ Expr createPrecedenceTree(ExprManager* em,
   //Debug("prec") << "pivot[" << startIndex << "," << stopIndex - 1 << "] at " << pivot << std::endl;
   bool negate;
   Kind k = getOperatorKind(operators[pivot], negate);
-  Expr lhs = createPrecedenceTree(em, expressions, operators, startIndex, pivot);
-  Expr rhs = createPrecedenceTree(em, expressions, operators, pivot + 1, stopIndex);
+  Expr lhs = createPrecedenceTree(parser, em, expressions, operators, startIndex, pivot);
+  Expr rhs = createPrecedenceTree(parser, em, expressions, operators, pivot + 1, stopIndex);
   if(k == kind::EQUAL && lhs.getType().isBoolean()) {
-    WarningOnce() << "Warning: converting BOOL = BOOL to BOOL <=> BOOL" << std::endl;
-    k = kind::IFF;
+    if(parser->strictModeEnabled()) {
+      WarningOnce() << "Warning: in strict parsing mode, will not convert BOOL = BOOL to BOOL <=> BOOL" << std::endl;
+    } else {
+      k = kind::IFF;
+    }
   }
   Expr e = em->mkExpr(k, lhs, rhs);
   return negate ? em->mkExpr(kind::NOT, e) : e;
 }/* createPrecedenceTree() recursive variant */
 
-Expr createPrecedenceTree(ExprManager* em,
+Expr createPrecedenceTree(Parser* parser, ExprManager* em,
                           const std::vector<CVC4::Expr>& expressions,
                           const std::vector<unsigned>& operators) {
   if(Debug.isOn("prec") && operators.size() > 1) {
@@ -391,7 +394,7 @@ Expr createPrecedenceTree(ExprManager* em,
     Debug("prec") << std::endl;
   }
 
-  Expr e = createPrecedenceTree(em, expressions, operators, 0, expressions.size() - 1);
+  Expr e = createPrecedenceTree(parser, em, expressions, operators, 0, expressions.size() - 1);
   if(Debug.isOn("prec") && operators.size() > 1) {
     Expr::setlanguage::Scope ls(Debug("prec"), language::output::LANG_AST);
     Debug("prec") << "=> " << e << std::endl;
@@ -749,9 +752,9 @@ simpleSymbolicExpr[CVC4::SExpr& sexpr]
   CVC4::Rational r;
 }
   : INTEGER_LITERAL
-    { sexpr = SExpr(AntlrInput::tokenText($INTEGER_LITERAL)); }
+    { sexpr = SExpr(AntlrInput::tokenToInteger($INTEGER_LITERAL)); }
   | DECIMAL_LITERAL
-    { sexpr = SExpr(AntlrInput::tokenText($DECIMAL_LITERAL)); }
+    { sexpr = SExpr(AntlrInput::tokenToRational($DECIMAL_LITERAL)); }
   | HEX_LITERAL
     { sexpr = SExpr(AntlrInput::tokenText($HEX_LITERAL)); }
   | BINARY_LITERAL
@@ -1197,7 +1200,7 @@ formula[CVC4::Expr& f]
         expressions.push_back(f);
       }
       i=morecomparisons[expressions,operators]?
-      { f = createPrecedenceTree(EXPR_MANAGER, expressions, operators); }
+      { f = createPrecedenceTree(PARSER_STATE, EXPR_MANAGER, expressions, operators); }
     )
   ;
 
@@ -1321,7 +1324,7 @@ comparison[CVC4::Expr& f]
   : term[f] { expressions.push_back(f); }
     ( comparisonBinop[op] term[f]
       { operators.push_back(op); expressions.push_back(f); } )*
-    { f = createPrecedenceTree(EXPR_MANAGER, expressions, operators); }
+    { f = createPrecedenceTree(PARSER_STATE, EXPR_MANAGER, expressions, operators); }
   ;
 
 comparisonBinop[unsigned& op]
@@ -1345,7 +1348,7 @@ term[CVC4::Expr& f]
 }
   : storeTerm[f] { expressions.push_back(f); }
     ( arithmeticBinop[op] storeTerm[f] { operators.push_back(op); expressions.push_back(f); } )*
-    { f = createPrecedenceTree(EXPR_MANAGER, expressions, operators); }
+    { f = createPrecedenceTree(PARSER_STATE, EXPR_MANAGER, expressions, operators); }
   ;
 
 arithmeticBinop[unsigned& op]
@@ -1500,7 +1503,7 @@ bvBinaryOpTerm[CVC4::Expr& f]
 }
   : bvNegTerm[f] { expressions.push_back(f); }
     ( bvBinop[op] bvNegTerm[f] { operators.push_back(op); expressions.push_back(f); } )*
-    { f = createPrecedenceTree(EXPR_MANAGER, expressions, operators); }
+    { f = createPrecedenceTree(PARSER_STATE, EXPR_MANAGER, expressions, operators); }
   ;
 bvBinop[unsigned& op]
 @init {

diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g
index 53a05a9a4d71e380fde6b78aa97d97d2fbdd4402..5a80083b349f9c2f88d54aba0586a2bd42ec240b 100644 (file)
--- a/src/parser/smt/Smt.g
+++ b/src/parser/smt/Smt.g
@@ -536,6 +536,7 @@ annotation[CVC4::Command*& smt_command]
       { std::string value = AntlrInput::tokenText($USER_VALUE);
         Assert(*value.begin() == '{');
         Assert(*value.rbegin() == '}');
+        // trim whitespace
         value.erase(value.begin(), value.begin() + 1);
         value.erase(value.begin(), std::find_if(value.begin(), value.end(), std::not1(std::ptr_fun<int, int>(std::isspace))));
         value.erase(value.end() - 1);

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 926ce17182396389751fc787a6e1886a641321fb..d478bd843ffe4d1be3a5b6494f14e44718041858 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -405,9 +405,9 @@ simpleSymbolicExpr[CVC4::SExpr& sexpr]
   std::string s;
 }
   : INTEGER_LITERAL
-    { sexpr = SExpr(AntlrInput::tokenText($INTEGER_LITERAL)); }
+    { sexpr = SExpr(AntlrInput::tokenToInteger($INTEGER_LITERAL)); }
   | DECIMAL_LITERAL
-    { sexpr = SExpr(AntlrInput::tokenText($DECIMAL_LITERAL)); }
+    { sexpr = SExpr(AntlrInput::tokenToRational($DECIMAL_LITERAL)); }
   | str[s]
     { sexpr = SExpr(s); }
   | SYMBOL

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 04690f500b9138f1747c9436727d5f14aef31298..a3d15f822592904690d71478ed76c887ca2e7b09 100644 (file)
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -173,6 +173,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       toStream(out, n[1], depth, types, true);
       out << " ELSE ";
       toStream(out, n[2], depth, types, true);
+      out << " ENDIF";
       return;
       break;
     case kind::TUPLE_TYPE:
@@ -237,18 +238,18 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
         if (n.getNumChildren() > 2) {
           out << '(';
         }
-        for (unsigned i = 0; i < n.getNumChildren(); ++ i) {
-          if (i > 0) {
+        for (unsigned i = 1; i < n.getNumChildren(); ++i) {
+          if (i > 1) {
             out << ", ";
           }
-          toStream(out, n[i], depth, types, false);
+          toStream(out, n[i - 1], depth, types, false);
         }
         if (n.getNumChildren() > 2) {
           out << ')';
         }
       }
       out << " -> ";
-      toStream(out, n[n.getNumChildren()-1], depth, types, false);
+      toStream(out, n[n.getNumChildren() - 1], depth, types, false);
       return;
       break;
 
@@ -630,6 +631,29 @@ void CvcPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw
 
 }/* CvcPrinter::toStream(CommandStatus*) */
 
+static void toStream(std::ostream& out, const SExpr& sexpr) throw() {
+  if(sexpr.isInteger()) {
+    out << sexpr.getIntegerValue();
+  } else if(sexpr.isRational()) {
+    out << sexpr.getRationalValue();
+  } else if(sexpr.isString()) {
+    string s = sexpr.getValue();
+    // escape backslash and quote
+    for(string::iterator i = s.begin(); i != s.end(); ++i) {
+      if(*i == '"') {
+        s.replace(i, i + 1, "\\\"");
+        ++i;
+      } else if(*i == '\\') {
+        s.replace(i, i + 1, "\\\\");
+        ++i;
+      }
+    }
+    out << "\"" << s << "\"";
+  } else {
+    out << sexpr;
+  }
+}
+
 static void toStream(std::ostream& out, const AssertCommand* c) throw() {
   out << "ASSERT " << c->getExpr() << ";";
 }
@@ -756,7 +780,9 @@ static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c) throw
 }
 
 static void toStream(std::ostream& out, const SetInfoCommand* c) throw() {
-  out << "% (set-info " << c->getFlag() << " " << c->getSExpr() << ")";
+  out << "% (set-info " << c->getFlag() << " ";
+  toStream(out, c->getSExpr());
+  out << ")";
 }
 
 static void toStream(std::ostream& out, const GetInfoCommand* c) throw() {
@@ -764,7 +790,9 @@ static void toStream(std::ostream& out, const GetInfoCommand* c) throw() {
 }
 
 static void toStream(std::ostream& out, const SetOptionCommand* c) throw() {
-  out << "% (set-option " << c->getFlag() << " " << c->getSExpr() << ")";
+  out << "% (set-option " << c->getFlag() << " ";
+  toStream(out, c->getSExpr());
+  out << ")";
 }
 
 static void toStream(std::ostream& out, const GetOptionCommand* c) throw() {

diff --git a/src/printer/smt/smt_printer.cpp b/src/printer/smt/smt_printer.cpp
index 2ac514988831efcc19e2508ecf433081a496e9e9..e6490de638177fa4844efbda27c5a4f53b023094 100644 (file)
--- a/src/printer/smt/smt_printer.cpp
+++ b/src/printer/smt/smt_printer.cpp
@@ -45,7 +45,7 @@ void SmtPrinter::toStream(std::ostream& out, const Command* c,
 
 void SmtPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw() {
   s->toStream(out, language::output::LANG_SMTLIB_V2);
-}
+}/* SmtPrinter::toStream() */
 
 }/* CVC4::printer::smt namespace */
 }/* CVC4::printer namespace */

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 691e96ed7406e1661667fe1c8b878adf9f608c44..218654a1930547e9a83f190e1ae5e16ba31776c8 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -427,6 +427,29 @@ void Smt2Printer::toStream(std::ostream& out, const Command* c,
 
 }/* Smt2Printer::toStream(Command*) */
 
+static void toStream(std::ostream& out, const SExpr& sexpr) throw() {
+  if(sexpr.isInteger()) {
+    out << sexpr.getIntegerValue();
+  } else if(sexpr.isRational()) {
+    out << sexpr.getRationalValue();
+  } else if(sexpr.isString()) {
+    string s = sexpr.getValue();
+    // escape backslash and quote
+    for(size_t i = 0; i < s.length(); ++i) {
+      if(s[i] == '"') {
+        s.replace(i, 1, "\\\"");
+        ++i;
+      } else if(s[i] == '\\') {
+        s.replace(i, 1, "\\\\");
+        ++i;
+      }
+    }
+    out << "\"" << s << "\"";
+  } else {
+    out << sexpr;
+  }
+}
+
 template <class T>
 static bool tryToStream(std::ostream& out, const CommandStatus* s) throw();
 
@@ -576,7 +599,9 @@ static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c) throw
 }
 
 static void toStream(std::ostream& out, const SetInfoCommand* c) throw() {
-  out << "(set-info " << c->getFlag() << " " << c->getSExpr() << ")";
+  out << "(set-info " << c->getFlag() << " ";
+  toStream(out, c->getSExpr());
+  out << ")";
 }
 
 static void toStream(std::ostream& out, const GetInfoCommand* c) throw() {
@@ -584,7 +609,9 @@ static void toStream(std::ostream& out, const GetInfoCommand* c) throw() {
 }
 
 static void toStream(std::ostream& out, const SetOptionCommand* c) throw() {
-  out << "(set-option " << c->getFlag() << " " << c->getSExpr() << ")";
+  out << "(set-option " << c->getFlag() << " ";
+  toStream(out, c->getSExpr());
+  out << ")";
 }
 
 static void toStream(std::ostream& out, const GetOptionCommand* c) throw() {

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 57a8c2f230bb64a7c2a68cb46db3a81b14003dec..2b6eb39155affa9ffbc3ba25e8ca20596789bb56 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -383,7 +383,15 @@ void SmtEngine::setInfo(const std::string& key, const SExpr& value)
   throw(BadOptionException, ModalException) {
   Trace("smt") << "SMT setInfo(" << key << ", " << value << ")" << endl;
   if(Dump.isOn("benchmark")) {
-    Dump("benchmark") << SetInfoCommand(key, value);
+    if(key == ":status") {
+      std::string s = value.getValue();
+      BenchmarkStatus status =
+        (s == "sat") ? SMT_SATISFIABLE :
+          ((s == "unsat") ? SMT_UNSATISFIABLE : SMT_UNKNOWN);
+      Dump("benchmark") << SetBenchmarkStatusCommand(status);
+    } else {
+      Dump("benchmark") << SetInfoCommand(key, value);
+    }
   }
 
   // Check for CVC4-specific info keys (prefixed with "cvc4-" or "cvc4_")

diff --git a/src/util/sexpr.h b/src/util/sexpr.h
index 63ce23874be0fc0fdce5a9afc4a76c7f9ef848e0..005d9411dcc62da5932757230b228339fb73dddd 100644 (file)
--- a/src/util/sexpr.h
+++ b/src/util/sexpr.h
@@ -34,8 +34,18 @@ namespace CVC4 {
  */
 class CVC4_PUBLIC SExpr {
 
-  /** Flag telling us if this is an atom or a list. */
-  bool d_isAtom;
+  enum {
+    SEXPR_STRING,
+    SEXPR_INTEGER,
+    SEXPR_RATIONAL,
+    SEXPR_NOT_ATOM
+  } d_atomType;
+
+  /** The value of an atomic integer-valued S-expression. */
+  Integer d_integerValue;
+
+  /** The value of an atomic rational-valued S-expression. */
+  Rational d_rationalValue;
 
   /** The value of an atomic S-expression. */
   std::string d_stringValue;
@@ -45,46 +55,126 @@ class CVC4_PUBLIC SExpr {
 
 public:
   SExpr() :
-    d_isAtom(true) {
+    d_atomType(SEXPR_STRING),
+    d_integerValue(0),
+    d_rationalValue(0),
+    d_stringValue(""),
+    d_children() {
+  }
+
+  SExpr(const Integer& value) :
+    d_atomType(SEXPR_INTEGER),
+    d_integerValue(value),
+    d_rationalValue(0),
+    d_stringValue(""),
+    d_children() {
+  }
+
+  SExpr(const Rational& value) :
+    d_atomType(SEXPR_RATIONAL),
+    d_integerValue(0),
+    d_rationalValue(value),
+    d_stringValue(""),
+    d_children() {
   }
 
   SExpr(const std::string& value) :
-    d_isAtom(true),
-    d_stringValue(value) {
+    d_atomType(SEXPR_STRING),
+    d_integerValue(0),
+    d_rationalValue(0),
+    d_stringValue(value),
+    d_children() {
   }
 
   SExpr(const std::vector<SExpr> children) :
-    d_isAtom(false),
+    d_atomType(SEXPR_NOT_ATOM),
+    d_integerValue(0),
+    d_rationalValue(0),
+    d_stringValue(""),
     d_children(children) {
   }
 
   /** Is this S-expression an atom? */
   bool isAtom() const;
 
+  /** Is this S-expression an integer? */
+  bool isInteger() const;
+
+  /** Is this S-expression a rational? */
+  bool isRational() const;
+
+  /** Is this S-expression a string? */
+  bool isString() const;
+
   /**
    * Get the string value of this S-expression. This will cause an
    * error if this S-expression is not an atom.
    */
   const std::string getValue() const;
 
+  /**
+   * Get the integer value of this S-expression. This will cause an
+   * error if this S-expression is not an integer.
+   */
+  const Integer& getIntegerValue() const;
+
+  /**
+   * Get the rational value of this S-expression. This will cause an
+   * error if this S-expression is not a rational.
+   */
+  const Rational& getRationalValue() const;
+
   /**
    * Get the children of this S-expression. This will cause an error
    * if this S-expression is not a list.
    */
   const std::vector<SExpr> getChildren() const;
-};
+
+};/* class SExpr */
 
 inline bool SExpr::isAtom() const {
-  return d_isAtom;
+  return d_atomType != SEXPR_NOT_ATOM;
+}
+
+inline bool SExpr::isInteger() const {
+  return d_atomType == SEXPR_INTEGER;
+}
+
+inline bool SExpr::isRational() const {
+  return d_atomType == SEXPR_RATIONAL;
+}
+
+inline bool SExpr::isString() const {
+  return d_atomType == SEXPR_STRING;
 }
 
 inline const std::string SExpr::getValue() const {
-  AlwaysAssert( d_isAtom );
+  AlwaysAssert( isAtom() );
+  switch(d_atomType) {
+  case SEXPR_INTEGER:
+    return d_integerValue.toString();
+  case SEXPR_RATIONAL:
+    return d_rationalValue.toString();
+  case SEXPR_STRING:
+    return d_stringValue;
+  default:
+    Unhandled(d_atomType);
+  }
   return d_stringValue;
 }
 
+inline const Integer& SExpr::getIntegerValue() const {
+  AlwaysAssert( isInteger() );
+  return d_integerValue;
+}
+
+inline const Rational& SExpr::getRationalValue() const {
+  AlwaysAssert( isRational() );
+  return d_rationalValue;
+}
+
 inline const std::vector<SExpr> SExpr::getChildren() const {
-  AlwaysAssert( !d_isAtom );
+  AlwaysAssert( !isAtom() );
   return d_children;
 }