19 files changed, 83 insertions, 114 deletions
diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp
index 1d2dbd736..21e48b19e 100644
--- a/src/parser/antlr_input.cpp
+++ b/src/parser/antlr_input.cpp
@@ -18,23 +18,22 @@
 #include <antlr3.h>
 #include <stdint.h>
 
+#include "base/output.h"
+#include "expr/type.h"
 #include "parser/antlr_input.h"
-#include "parser/input.h"
+#include "parser/antlr_line_buffered_input.h"
 #include "parser/bounded_token_buffer.h"
 #include "parser/bounded_token_factory.h"
-#include "parser/antlr_line_buffered_input.h"
+#include "parser/cvc/cvc_input.h"
+#include "parser/input.h"
 #include "parser/memory_mapped_input_buffer.h"
-#include "parser/parser_exception.h"
 #include "parser/parser.h"
-
-#include "expr/command.h"
-#include "expr/type.h"
-#include "parser/cvc/cvc_input.h"
+#include "parser/parser_exception.h"
 #include "parser/smt1/smt1_input.h"
 #include "parser/smt2/smt2_input.h"
 #include "parser/smt2/sygus_input.h"
 #include "parser/tptp/tptp_input.h"
-#include "util/output.h"
+#include "smt_util/command.h"
 
 using namespace std;
 using namespace CVC4;
diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h
index 2086db714..baec46e6f 100644
--- a/src/parser/antlr_input.h
+++ b/src/parser/antlr_input.h
@@ -36,14 +36,14 @@
 #include <vector>
 #include <cassert>
 
+#include "base/output.h"
 #include "parser/bounded_token_buffer.h"
-#include "parser/parser_exception.h"
 #include "parser/input.h"
-
+#include "parser/parser_exception.h"
 #include "util/bitvector.h"
 #include "util/integer.h"
 #include "util/rational.h"
-#include "util/output.h"
+
 
 namespace CVC4 {
 
diff --git a/src/parser/antlr_line_buffered_input.cpp b/src/parser/antlr_line_buffered_input.cpp
index 33589110f..cc1d499fb 100644
--- a/src/parser/antlr_line_buffered_input.cpp
+++ b/src/parser/antlr_line_buffered_input.cpp
@@ -29,7 +29,7 @@
 #include <string>
 #include <cassert>
 
-#include "util/output.h"
+#include "base/output.h"
 #include "parser/antlr_line_buffered_input.h"
 
 namespace CVC4 {
diff --git a/src/parser/antlr_tracing.h b/src/parser/antlr_tracing.h
index a94cd4f2f..1709e99a2 100644
--- a/src/parser/antlr_tracing.h
+++ b/src/parser/antlr_tracing.h
@@ -23,7 +23,8 @@
 
 #include <iostream>
 #include <string>
-#include "util/output.h"
+
+#include "base/output.h"
 
 /* The ANTLR lexer generator, as of v3.2, puts Java trace commands
  * into our beautiful generated C lexer!  How awful!  This is clearly
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 0c356ca57..460b1ee03 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -476,10 +476,10 @@ Expr addNots(ExprManager* em, size_t n, Expr e) {
 #  define ANTLR3_INLINE_INPUT_8BIT
 #endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
 
-#include "parser/antlr_tracing.h"
-#include "util/integer.h"
 #include "parser/antlr_input.h"
+#include "parser/antlr_tracing.h"
 #include "parser/parser.h"
+#include "util/integer.h"
 
 }/* @lexer::includes */
 
@@ -487,10 +487,10 @@ Expr addNots(ExprManager* em, size_t n, Expr e) {
 
 #include <stdint.h>
 #include <cassert>
-#include "expr/command.h"
+#include "parser/antlr_tracing.h"
 #include "parser/parser.h"
+#include "smt_util/command.h"
 #include "util/subrange_bound.h"
-#include "parser/antlr_tracing.h"
 
 namespace CVC4 {
   class Expr;
@@ -541,16 +541,17 @@ namespace CVC4 {
 
 @parser::postinclude {
 
+#include <sstream>
+#include <string>
+#include <vector>
+
+#include "base/output.h"
 #include "expr/expr.h"
 #include "expr/kind.h"
 #include "expr/type.h"
 #include "parser/antlr_input.h"
 #include "parser/parser.h"
-#include "util/output.h"
 
-#include <vector>
-#include <string>
-#include <sstream>
 
 #define REPEAT_COMMAND(k, CommandCtor)                      \
   ({                                                        \
diff --git a/src/parser/input.cpp b/src/parser/input.cpp
index 09f71800b..82b6dd32f 100644
--- a/src/parser/input.cpp
+++ b/src/parser/input.cpp
@@ -18,10 +18,11 @@
 #include "parser/parser_exception.h"
 #include "parser/parser.h"
 
-#include "expr/command.h"
+#include "base/output.h"
+#include "smt_util/command.h"
 #include "expr/type.h"
 #include "parser/antlr_input.h"
-#include "util/output.h"
+
 
 using namespace std;
 using namespace CVC4;
diff --git a/src/parser/input.h b/src/parser/input.h
index 312bc92f1..dcb54d256 100644
--- a/src/parser/input.h
+++ b/src/parser/input.h
@@ -20,14 +20,14 @@
 #define __CVC4__PARSER__INPUT_H
 
 #include <iostream>
-#include <string>
 #include <stdio.h>
+#include <string>
 #include <vector>
 
+#include "options/language.h"
 #include "expr/expr.h"
 #include "expr/expr_manager.h"
 #include "parser/parser_exception.h"
-#include "util/language.h"
 
 namespace CVC4 {
 
diff --git a/src/parser/memory_mapped_input_buffer.cpp b/src/parser/memory_mapped_input_buffer.cpp
index 9dcab2085..7be1c9aba 100644
--- a/src/parser/memory_mapped_input_buffer.cpp
+++ b/src/parser/memory_mapped_input_buffer.cpp
@@ -28,8 +28,8 @@
 
 #endif /* _WIN32 */
 
+#include "base/exception.h"
 #include "parser/memory_mapped_input_buffer.h"
-#include "util/exception.h"
 
 namespace CVC4 {
 namespace parser {
diff --git a/src/parser/options b/src/parser/options
deleted file mode 100644
index 66e95889f..000000000
--- a/src/parser/options
+++ /dev/null
@@ -1,34 +0,0 @@
-#
-# Option specification file for CVC4
-# See src/options/base_options for a description of this file format
-#
-
-module PARSER "parser/options.h" Parser
-
-common-option strictParsing --strict-parsing bool
- be less tolerant of non-conforming inputs
-
-option memoryMap --mmap bool
- memory map file input
-
-option semanticChecks /--no-checking bool :default DO_SEMANTIC_CHECKS_BY_DEFAULT :link /--no-type-checking
- disable ALL semantic checks, including type checks
-
-option globalDeclarations global-declarations bool :default false
- force all declarations and definitions to be global
-
-# this is to support security in the online version, and in other similar contexts
-# (--no-include-file disables filesystem access in TPTP and SMT2 parsers)
-# the name --no-include-file is legacy: it also now limits any filesystem access
-# (read or write) for example by using --dump-to (or the equivalent set-option) or
-# set-option :regular-output-channel/:diagnostic-output-channel.  However, the main
-# driver is still permitted to read the input file given on the command-line if any.
-# creation/use of temp files are still permitted (but the paths aren't given by the
-# user).  Also note this is only safe for the version invoked through the main driver,
-# there are ways via the API to get the CVC4 library to open a file for reading or
-# writing and thus leak information from an existing file, or overwrite an existing
-# file with malicious content.
-undocumented-option filesystemAccess /--no-filesystem-access bool :default true
-undocumented-alias --no-include-file = --no-filesystem-access
-
-endmodule
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index d17d5d141..0e8a9e241 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -14,24 +14,26 @@
  ** Parser state implementation.
  **/
 
-#include <iostream>
-#include <fstream>
-#include <sstream>
-#include <iterator>
+#include "parser/parser.h"
+
 #include <stdint.h>
+
 #include <cassert>
+#include <fstream>
+#include <iostream>
+#include <iterator>
+#include <sstream>
 
-#include "parser/input.h"
-#include "parser/parser.h"
-#include "parser/parser_exception.h"
-#include "expr/command.h"
+#include "base/output.h"
 #include "expr/expr.h"
 #include "expr/kind.h"
+#include "expr/resource_manager.h"
 #include "expr/type.h"
-#include "util/output.h"
-#include "util/resource_manager.h"
 #include "options/options.h"
-#include "smt/options.h"
+#include "options/smt_options.h"
+#include "parser/input.h"
+#include "parser/parser_exception.h"
+#include "smt_util/command.h"
 
 using namespace std;
 using namespace CVC4::kind;
diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp
index a2faec704..08e0232aa 100644
--- a/src/parser/parser_builder.cpp
+++ b/src/parser/parser_builder.cpp
@@ -13,20 +13,19 @@
  **
  ** A builder for parsers.
  **/
+#include "parser/parser_builder.h"
 
 #include <string>
 
-#include "parser/parser_builder.h"
+#include "expr/expr_manager.h"
+#include "options/parser_options.h"
+#include "options/smt_options.h"
 #include "parser/input.h"
 #include "parser/parser.h"
 #include "smt1/smt1.h"
 #include "smt2/smt2.h"
 #include "tptp/tptp.h"
 
-#include "expr/expr_manager.h"
-#include "parser/options.h"
-#include "smt/options.h"
-
 namespace CVC4 {
 namespace parser {
 
@@ -168,7 +167,7 @@ ParserBuilder& ParserBuilder::withOptions(const Options& options) {
       .withParseOnly(options[options::parseOnly])
       .withIncludeFile(options[options::filesystemAccess]);
   if(options.wasSetByUser(options::forceLogic)) {
-    retval = retval.withForcedLogic(options[options::forceLogic].getLogicString());
+    retval = retval.withForcedLogic(options[options::forceLogic]->getLogicString());
   }
   return retval;
 }
diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h
index 71810bf7c..fe652286b 100644
--- a/src/parser/parser_builder.h
+++ b/src/parser/parser_builder.h
@@ -21,10 +21,9 @@
 
 #include <string>
 
+#include "options/language.h"
 #include "parser/input.h"
 
-#include "util/language.h"
-
 namespace CVC4 {
 
 class ExprManager;
diff --git a/src/parser/parser_exception.h b/src/parser/parser_exception.h
index 3b211371c..de47767c9 100644
--- a/src/parser/parser_exception.h
+++ b/src/parser/parser_exception.h
@@ -23,7 +23,7 @@
 #include <string>
 #include <sstream>
 
-#include "util/exception.h"
+#include "base/exception.h"
 
 namespace CVC4 {
 namespace parser {
diff --git a/src/parser/smt1/Smt1.g b/src/parser/smt1/Smt1.g
index a885fe990..98825f1c3 100644
--- a/src/parser/smt1/Smt1.g
+++ b/src/parser/smt1/Smt1.g
@@ -63,7 +63,7 @@ options {
 
 #include <stdint.h>
 
-#include "expr/command.h"
+#include "smt_util/command.h"
 #include "parser/parser.h"
 #include "parser/antlr_tracing.h"
 
@@ -101,6 +101,9 @@ namespace CVC4 {
 
 @parser::postinclude {
 
+#include <vector>
+
+#include "base/output.h"
 #include "expr/expr.h"
 #include "expr/kind.h"
 #include "expr/type.h"
@@ -108,9 +111,7 @@ namespace CVC4 {
 #include "parser/parser.h"
 #include "parser/smt1/smt1.h"
 #include "util/integer.h"
-#include "util/output.h"
 #include "util/rational.h"
-#include <vector>
 
 using namespace CVC4;
 using namespace CVC4::parser;
@@ -573,7 +574,7 @@ annotation[CVC4::Command*& smt_command]
     annotatedFormulas[pats,pat] '}'
   | attribute[key]
     ( userValue[value]
-      { smt_command = new SetInfoCommand(key.c_str() + 1, value); }
+      { smt_command = new SetInfoCommand(key.c_str() + 1, SExpr(value)); }
     | { smt_command = new EmptyCommand(std::string("annotation: ") + key); }
     )
   ;
diff --git a/src/parser/smt1/smt1.cpp b/src/parser/smt1/smt1.cpp
index 8d827b17e..01bc8901e 100644
--- a/src/parser/smt1/smt1.cpp
+++ b/src/parser/smt1/smt1.cpp
@@ -18,7 +18,7 @@ namespace std {
 }
 
 #include "expr/type.h"
-#include "expr/command.h"
+#include "smt_util/command.h"
 #include "parser/parser.h"
 #include "parser/smt1/smt1.h"
 
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index d2409ba15..8ac1fa34c 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -75,9 +75,9 @@ using namespace CVC4::parser;
 }/* @lexer::postinclude */
 
 @parser::includes {
-#include "expr/command.h"
 #include "parser/parser.h"
 #include "parser/antlr_tracing.h"
+#include "smt_util/command.h"
 
 namespace CVC4 {
   class Expr;
@@ -102,21 +102,22 @@ namespace CVC4 {
 
 @parser::postinclude {
 
+#include <set>
+#include <sstream>
+#include <string>
+#include <vector>
+
+#include "base/output.h"
 #include "expr/expr.h"
 #include "expr/kind.h"
 #include "expr/type.h"
 #include "parser/antlr_input.h"
 #include "parser/parser.h"
 #include "parser/smt2/smt2.h"
+#include "util/floatingpoint.h"
+#include "util/hash.h"
 #include "util/integer.h"
-#include "util/output.h"
 #include "util/rational.h"
-#include "util/hash.h"
-#include "util/floatingpoint.h"
-#include <vector>
-#include <set>
-#include <string>
-#include <sstream>
 // \todo Review the need for this header
 #include "math.h"
 
@@ -995,10 +996,7 @@ smt25Command[CVC4::Command*& cmd]
     /* echo */
   | ECHO_TOK
     ( simpleSymbolicExpr[sexpr]
-      { std::stringstream ss;
-        ss << sexpr;
-        cmd = new EchoCommand(ss.str());
-      }
+      { cmd = new EchoCommand(sexpr.toString()); }
     | { cmd = new EchoCommand(); }
     )
 
@@ -1446,12 +1444,12 @@ simpleSymbolicExprNoKeyword[CVC4::SExpr& sexpr]
   | HEX_LITERAL
     { assert( AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0 );
       std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2);
-      sexpr = Integer(hexString, 16);
+      sexpr = SExpr(Integer(hexString, 16));
     }
   | BINARY_LITERAL
     { assert( AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0 );
       std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 2);
-      sexpr = Integer(binString, 2);
+      sexpr = SExpr(Integer(binString, 2));
     }
   | str[s,false]
     { sexpr = SExpr(s); }
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index d3af9143a..355b58067 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -13,14 +13,14 @@
  **
  ** Definitions of SMT2 constants.
  **/
+#include "parser/smt2/smt2.h"
+
 
 #include "expr/type.h"
-#include "expr/command.h"
+#include "parser/antlr_input.h"
 #include "parser/parser.h"
 #include "parser/smt1/smt1.h"
-#include "parser/smt2/smt2.h"
-#include "parser/antlr_input.h"
-
+#include "smt_util/command.h"
 #include "util/bitvector.h"
 
 // ANTLR defines these, which is really bad!
diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g
index 62dcc70f5..a2bad4988 100644
--- a/src/parser/tptp/Tptp.g
+++ b/src/parser/tptp/Tptp.g
@@ -83,7 +83,7 @@ using namespace CVC4::parser;
 }/* @lexer::postinclude */
 
 @parser::includes {
-#include "expr/command.h"
+#include "smt_util/command.h"
 #include "parser/parser.h"
 #include "parser/tptp/tptp.h"
 #include "parser/antlr_tracing.h"
@@ -92,6 +92,11 @@ using namespace CVC4::parser;
 
 @parser::postinclude {
 
+#include <algorithm>
+#include <iterator>
+#include <vector>
+
+#include "base/output.h"
 #include "expr/expr.h"
 #include "expr/kind.h"
 #include "expr/type.h"
@@ -99,11 +104,7 @@ using namespace CVC4::parser;
 #include "parser/parser.h"
 #include "parser/tptp/tptp.h"
 #include "util/integer.h"
-#include "util/output.h"
 #include "util/rational.h"
-#include <vector>
-#include <iterator>
-#include <algorithm>
 
 using namespace CVC4;
 using namespace CVC4::parser;
@@ -203,7 +204,7 @@ parseCommand returns [CVC4::Command* cmd = NULL]
         filename = filename.substr(0, filename.length() - 2);
       }
       CommandSequence* seq = new CommandSequence();
-      seq->addCommand(new SetInfoCommand("name", filename));
+      seq->addCommand(new SetInfoCommand("name", SExpr(filename)));
       if(PARSER_STATE->hasConjecture()) {
         seq->addCommand(new QueryCommand(MK_CONST(bool(false))));
       } else {
diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h
index 2cd8f4339..4fdbc236d 100644
--- a/src/parser/tptp/tptp.h
+++ b/src/parser/tptp/tptp.h
@@ -19,13 +19,14 @@
 #ifndef __CVC4__PARSER__TPTP_H
 #define __CVC4__PARSER__TPTP_H
 
-#include "parser/parser.h"
-#include "expr/command.h"
-#include "util/hash.h"
-#include <ext/hash_set>
 #include <cassert>
-#include "parser/options.h"
+#include <ext/hash_set>
+
+#include "options/parser_options.h"
 #include "parser/antlr_input.h"
+#include "parser/parser.h"
+#include "smt_util/command.h"
+#include "util/hash.h"
 
 namespace CVC4 {