parser and core support for SMT-LIBv2 commands get-info, set-option, get-option, get-assertions, get-value, define-sort, define-fun, and declare-sort with arity > 0; SmtEngine doesn't yet support most of these, but will shortly...

2 files changed, 37 insertions, 20 deletions

diff --git a/src/util/options.h b/src/util/options.h
index c79bc93b1..c504177bf 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -65,21 +65,34 @@ struct CVC4_PUBLIC Options {
   /** Should we strictly enforce the language standard while parsing? */
   bool strictParsing;
 
-  Options() : binary_name(),
-              statistics(false),
-              out(0),
-              err(0),
-              verbosity(0),
-              lang(parser::LANG_AUTO),
-              uf_implementation(MORGAN),
-              parseOnly(false),
-              semanticChecks(true),
-              memoryMap(false),
-              strictParsing(false)
-  {}
+  /** Whether we're in interactive mode or not */
+  bool interactive;
+
+  /**
+   * Whether we're in interactive mode (or not) due to explicit user
+   * setting (if false, we inferred the proper default setting).
+   */
+  bool interactiveSetByUser;
+
+  Options() :
+    binary_name(),
+    statistics(false),
+    out(0),
+    err(0),
+    verbosity(0),
+    lang(parser::LANG_AUTO),
+    uf_implementation(MORGAN),
+    parseOnly(false),
+    semanticChecks(true),
+    memoryMap(false),
+    strictParsing(false),
+    interactive(false),
+    interactiveSetByUser(false) {
+  }
 };/* struct Options */
 
-inline std::ostream& operator<<(std::ostream& out, Options::UfImplementation uf) {
+inline std::ostream& operator<<(std::ostream& out,
+                                Options::UfImplementation uf) {
   switch(uf) {
   case Options::TIM:
     out << "TIM";
diff --git a/src/util/sexpr.h b/src/util/sexpr.h
index d3681f471..9821664bd 100644
--- a/src/util/sexpr.h
+++ b/src/util/sexpr.h
@@ -29,8 +29,8 @@
 namespace CVC4 {
 
 /**
- * A simple S-expression. An S-expression is either an atom with a string value, or a
- * list of other S-expressions.
+ * A simple S-expression. An S-expression is either an atom with a
+ * string value, or a list of other S-expressions.
  */
 class CVC4_PUBLIC SExpr {
 
@@ -61,13 +61,15 @@ public:
   /** Is this S-expression an atom? */
   bool isAtom() const;
 
-  /** Get the string value of this S-expression. This will cause an error if this S-expression
-   * is not an atom.
+  /**
+   * 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 children of this S-expression. This will cause an error if this S-expression
-   * is not a list.
+  /**
+   * 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;
 };
@@ -93,7 +95,9 @@ inline std::ostream& operator<<(std::ostream& out, const SExpr& sexpr) {
     std::vector<SExpr> children = sexpr.getChildren();
     out << "(";
     bool first = true;
-    for( std::vector<SExpr>::iterator it = children.begin(); it != children.end(); ++it ) {
+    for( std::vector<SExpr>::iterator it = children.begin();
+         it != children.end();
+         ++it ) {
       if( first ) {
         first = false;
       } else {