* 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)

1 files changed, 100 insertions, 10 deletions

diff --git a/src/util/sexpr.h b/src/util/sexpr.h
index 63ce23874..005d9411d 100644
--- 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,22 +55,57 @@ 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.
@@ -68,23 +113,68 @@ public:
   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;
 }