Options merge. This commit:

1. changes the way options are declared (see http://church.cims.nyu.edu/wiki/Options)
2. moves module-specific options enumerations (SimplificationMode, DecisionMode, ArithUnateLemmaMode, etc.) to their own header files, also they are no longer inside the Options:: class namespace.
3. includes many SMT-LIBv2 compliance fixes, especially to (set-option..) and (get-option..)

The biggest syntactical changes (outside of adding new options) you'll notice are in accessing and setting options:

* to access an option, write (e.g.) options::unconstrainedSimp() instead of Options::current()->unconstrainedSimp.
* to determine if an option value was set by the user, check (e.g.) options::unconstrainedSimp.wasSetByUser().
* ensure that you have the option available (you have to #include the right module's options.h file, e.g. #include "theory/uf/options.h" for UF options)
*** this point is important.  If you access an option and it tells you the option doesn't exist, you aren't #including the appropriate options.h header file ***

Note that if you want an option to be directly set (i.e., other than via command-line parsing or SmtEngine::setOption()), you need to mark the option :read-write in its options file (otherwise it's read-only), and you then write (e.g.) options::unconstrainedSimp.set(true).

Adding new options is incredibly simple for primitive types (int, unsigned, bool, string, double).  For option settings that you need to turn into a member of an enumerated type, you write a custom "handler" for the option---this is no additional work than it was before, and there are many examples to copy from (a good one is stringToSimplificationMode() in src/smt/options_handlers.h).

Benefits of the new options system include:

1. changes to options declarations don't require a full-source rebuild (you only have to rebuild those sources that depend on the set of options that changed).
2. lots of sanity checks (that the same option isn't declared twice, that option values are in range for their type, that all options are documented properly, etc.)
3. consistency: Boolean-valued option --foo gets a --no-foo automatically, documentation is generated consistently, the option-parsing matches the documented option name, etc.
4. setting options programmatically via SmtEngine::setOption() is enabled, and behaves the same as command-line equivalents (including checking the value is in range, etc.)
5. the notion of options being "set by the user" is now primitive; you can use (e.g.) options::unconstrainedSimp.wasSetByUser() instead of having to use (and maintain) a separate Boolean option for the purpose

I've taken lots of care not to break anything.  Hopefully, I've succeeded in that.

9 files changed, 88 insertions, 79 deletions

diff --git a/src/parser/cvc/Makefile.am b/src/parser/cvc/Makefile.am
index 15a572745..e5666b702 100644
--- a/src/parser/cvc/Makefile.am
+++ b/src/parser/cvc/Makefile.am
@@ -15,14 +15,14 @@ ANTLR_OPTS =
 noinst_LTLIBRARIES = libparsercvc.la
 
 ANTLR_TOKEN_STUFF = \
-	@srcdir@/generated/Cvc.tokens
+	generated/Cvc.tokens
 ANTLR_LEXER_STUFF = \
-    @srcdir@/generated/CvcLexer.h \
-    @srcdir@/generated/CvcLexer.c \
+    generated/CvcLexer.h \
+    generated/CvcLexer.c \
     $(ANTLR_TOKEN_STUFF)
 ANTLR_PARSER_STUFF = \
-    @srcdir@/generated/CvcParser.h \
-    @srcdir@/generated/CvcParser.c
+    generated/CvcParser.h \
+    generated/CvcParser.c
 ANTLR_STUFF = \
     $(ANTLR_LEXER_STUFF) \
     $(ANTLR_PARSER_STUFF)
@@ -33,29 +33,27 @@ libparsercvc_la_SOURCES = \
     cvc_input.cpp \
     $(ANTLR_STUFF)
 
-BUILT_SOURCES = $(ANTLR_STUFF) @srcdir@/stamp-generated
+BUILT_SOURCES = $(ANTLR_STUFF) stamp-generated
 
-EXTRA_DIST = \
-	@srcdir@/stamp-generated \
-	README
+EXTRA_DIST = README
 
 MAINTAINERCLEANFILES = $(ANTLR_STUFF)
 maintainer-clean-local:
-	-$(AM_V_at)rmdir @srcdir@/generated
-	-$(AM_V_at)rm -f @srcdir@/stamp-generated
+	-$(AM_V_at)rmdir generated
+	-$(AM_V_at)rm -f stamp-generated
 
-@srcdir@/stamp-generated:
-	$(AM_V_at)mkdir -p @srcdir@/generated
-	$(AM_V_at)touch @srcdir@/stamp-generated
+stamp-generated:
+	$(AM_V_at)mkdir -p generated
+	$(AM_V_at)touch stamp-generated
 
 # antlr doesn't overwrite output files, it just leaves them.  So we have to delete them first.
-@srcdir@/generated/CvcLexer.h: Cvc.g @srcdir@/stamp-generated
+generated/CvcLexer.h: Cvc.g stamp-generated
 	-$(AM_V_at)rm -f $(ANTLR_STUFF)
 	@if test -z "$(ANTLR)"; then echo "ERROR: antlr parser generator cannot be found, cannot generate the parser" >&2; exit 1; fi
-	$(AM_V_GEN)$(ANTLR) $(ANTLR_OPTS) -fo "@srcdir@/generated" "@srcdir@/Cvc.g"
+	$(AM_V_GEN)$(ANTLR) $(ANTLR_OPTS) -fo "generated" "@srcdir@/Cvc.g"
 
 # These don't actually depend on CvcLexer.h, but if we're doing parallel
 # make and the lexer needs to be rebuilt, we have to keep the rules
 # from running in parallel (since the token files will be deleted &
 # recreated)
-@srcdir@/generated/CvcLexer.c @srcdir@/generated/CvcParser.h @srcdir@/generated/CvcParser.c $(ANTLR_TOKEN_STUFF): @srcdir@/generated/CvcLexer.h
+generated/CvcLexer.c generated/CvcParser.h generated/CvcParser.c $(ANTLR_TOKEN_STUFF): generated/CvcLexer.h
diff --git a/src/parser/options b/src/parser/options
new file mode 100644
index 000000000..beae09823
--- /dev/null
+++ b/src/parser/options
@@ -0,0 +1,17 @@
+#
+# 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
+
+endmodule
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 2265355f0..44148a7f1 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -29,7 +29,7 @@
 #include "expr/kind.h"
 #include "expr/type.h"
 #include "util/output.h"
-#include "util/options.h"
+#include "options/options.h"
 #include "util/Assert.h"
 #include "parser/cvc/cvc_input.h"
 #include "parser/smt/smt_input.h"
diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp
index d9b7cf341..bd71f71e7 100644
--- a/src/parser/parser_builder.cpp
+++ b/src/parser/parser_builder.cpp
@@ -26,7 +26,7 @@
 #include "tptp/tptp.h"
 
 #include "expr/expr_manager.h"
-#include "util/options.h"
+#include "parser/options.h"
 
 namespace CVC4 {
 namespace parser {
@@ -146,11 +146,11 @@ ParserBuilder& ParserBuilder::withParseOnly(bool flag) {
 
 ParserBuilder& ParserBuilder::withOptions(const Options& options) {
   return
-    withInputLanguage(options.inputLanguage)
-      .withMmap(options.memoryMap)
-      .withChecks(options.semanticChecks)
-      .withStrictMode(options.strictParsing)
-      .withParseOnly(options.parseOnly);
+    withInputLanguage(options[options::inputLanguage])
+      .withMmap(options[options::memoryMap])
+      .withChecks(options[options::semanticChecks])
+      .withStrictMode(options[options::strictParsing])
+      .withParseOnly(options[options::parseOnly]);
   }
 
 ParserBuilder& ParserBuilder::withStrictMode(bool flag) {
diff --git a/src/parser/smt/Makefile.am b/src/parser/smt/Makefile.am
index 975a90b72..a74a6909c 100644
--- a/src/parser/smt/Makefile.am
+++ b/src/parser/smt/Makefile.am
@@ -15,14 +15,14 @@ ANTLR_OPTS =
 noinst_LTLIBRARIES = libparsersmt.la
 
 ANTLR_TOKEN_STUFF = \
-	@srcdir@/generated/Smt.tokens
+	generated/Smt.tokens
 ANTLR_LEXER_STUFF = \
-	@srcdir@/generated/SmtLexer.h \
-	@srcdir@/generated/SmtLexer.c \
+	generated/SmtLexer.h \
+	generated/SmtLexer.c \
 	$(ANTLR_TOKEN_STUFF)
 ANTLR_PARSER_STUFF = \
-	@srcdir@/generated/SmtParser.h \
-	@srcdir@/generated/SmtParser.c
+	generated/SmtParser.h \
+	generated/SmtParser.c
 ANTLR_STUFF = \
 	$(ANTLR_LEXER_STUFF) \
 	$(ANTLR_PARSER_STUFF)
@@ -35,27 +35,25 @@ libparsersmt_la_SOURCES = \
 	smt_input.cpp \
 	$(ANTLR_STUFF)
 
-BUILT_SOURCES = $(ANTLR_STUFF) @srcdir@/stamp-generated
-
-EXTRA_DIST = @srcdir@/stamp-generated
+BUILT_SOURCES = $(ANTLR_STUFF) stamp-generated
 
 MAINTAINERCLEANFILES = $(ANTLR_STUFF)
 maintainer-clean-local:
-	-$(AM_V_at)rmdir @srcdir@/generated
-	-$(AM_V_at)rm -f @srcdir@/stamp-generated
+	-$(AM_V_at)rmdir generated
+	-$(AM_V_at)rm -f stamp-generated
 
-@srcdir@/stamp-generated:
-	$(AM_V_at)mkdir -p @srcdir@/generated
-	$(AM_V_at)touch @srcdir@/stamp-generated
+stamp-generated:
+	$(AM_V_at)mkdir -p generated
+	$(AM_V_at)touch stamp-generated
 
 # antlr doesn't overwrite output files, it just leaves them.  So we have to delete them first.
-@srcdir@/generated/SmtLexer.h: Smt.g @srcdir@/stamp-generated
+generated/SmtLexer.h: Smt.g stamp-generated
 	-$(AM_V_at)rm -f $(ANTLR_STUFF)
 	@if test -z "$(ANTLR)"; then echo "ERROR: antlr parser generator cannot be found, cannot generate the parser" >&2; exit 1; fi
-	$(AM_V_GEN)$(ANTLR) $(ANTLR_OPTS) -fo "@srcdir@/generated" "@srcdir@/Smt.g"
+	$(AM_V_GEN)$(ANTLR) $(ANTLR_OPTS) -fo "generated" "@srcdir@/Smt.g"
 
 # These don't actually depend on SmtLexer.h, but if we're doing parallel
 # make and the lexer needs to be rebuilt, we have to keep the rules
 # from running in parallel (since the token files will be deleted &
 # recreated)
-@srcdir@/generated/SmtLexer.c @srcdir@/generated/SmtParser.h @srcdir@/generated/SmtParser.c $(ANTLR_TOKEN_STUFF): @srcdir@/generated/SmtLexer.h
+generated/SmtLexer.c generated/SmtParser.h generated/SmtParser.c $(ANTLR_TOKEN_STUFF): generated/SmtLexer.h
diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g
index 429adee0a..f9c38385f 100644
--- a/src/parser/smt/Smt.g
+++ b/src/parser/smt/Smt.g
@@ -565,7 +565,7 @@ annotation[CVC4::Command*& smt_command]
         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);
         value.erase(std::find_if(value.rbegin(), value.rend(), std::not1(std::ptr_fun<int, int>(std::isspace))).base(), value.end());
-        smt_command = new SetInfoCommand(key, value); }
+        smt_command = new SetInfoCommand(key.c_str() + 1, value); }
     )?
     { if(smt_command == NULL) {
         smt_command = new EmptyCommand(std::string("annotation: ") + key);
diff --git a/src/parser/smt2/Makefile.am b/src/parser/smt2/Makefile.am
index 75ceec43a..8f7bf433c 100644
--- a/src/parser/smt2/Makefile.am
+++ b/src/parser/smt2/Makefile.am
@@ -15,14 +15,14 @@ ANTLR_OPTS =
 noinst_LTLIBRARIES = libparsersmt2.la
 
 ANTLR_TOKEN_STUFF = \
-	@srcdir@/generated/Smt2.tokens
+	generated/Smt2.tokens
 ANTLR_LEXER_STUFF = \
-	@srcdir@/generated/Smt2Lexer.h \
-	@srcdir@/generated/Smt2Lexer.c \
+	generated/Smt2Lexer.h \
+	generated/Smt2Lexer.c \
 	$(ANTLR_TOKEN_STUFF)
 ANTLR_PARSER_STUFF = \
-	@srcdir@/generated/Smt2Parser.h \
-	@srcdir@/generated/Smt2Parser.c
+	generated/Smt2Parser.h \
+	generated/Smt2Parser.c
 ANTLR_STUFF = \
 	$(ANTLR_LEXER_STUFF) \
 	$(ANTLR_PARSER_STUFF)
@@ -35,27 +35,25 @@ libparsersmt2_la_SOURCES = \
 	smt2_input.cpp \
 	$(ANTLR_STUFF)
 
-BUILT_SOURCES = $(ANTLR_STUFF) @srcdir@/stamp-generated
-
-EXTRA_DIST = @srcdir@/stamp-generated
+BUILT_SOURCES = $(ANTLR_STUFF) stamp-generated
 
 MAINTAINERCLEANFILES = $(ANTLR_STUFF)
 maintainer-clean-local:
-	-$(AM_V_at)rmdir @srcdir@/generated
-	-$(AM_V_at)rm -f @srcdir@/stamp-generated
+	-$(AM_V_at)rmdir generated
+	-$(AM_V_at)rm -f stamp-generated
 
-@srcdir@/stamp-generated:
-	$(AM_V_at)mkdir -p @srcdir@/generated
-	$(AM_V_at)touch @srcdir@/stamp-generated
+stamp-generated:
+	$(AM_V_at)mkdir -p generated
+	$(AM_V_at)touch stamp-generated
 
 # antlr doesn't overwrite output files, it just leaves them.  So we have to delete them first.
-@srcdir@/generated/Smt2Lexer.h: Smt2.g @srcdir@/stamp-generated
+generated/Smt2Lexer.h: Smt2.g stamp-generated
 	-$(AM_V_at)rm -f $(ANTLR_STUFF)
 	@if test -z "$(ANTLR)"; then echo "ERROR: antlr parser generator cannot be found, cannot generate the parser" >&2; exit 1; fi
-	$(AM_V_GEN)$(ANTLR) $(ANTLR_OPTS) -fo "@srcdir@/generated" "@srcdir@/Smt2.g"
+	$(AM_V_GEN)$(ANTLR) $(ANTLR_OPTS) -fo "generated" "@srcdir@/Smt2.g"
 
 # These don't actually depend on SmtLexer.h, but if we're doing parallel
 # make and the lexer needs to be rebuilt, we have to keep the rules
 # from running in parallel (since the token files will be deleted &
 # recreated)
-@srcdir@/generated/Smt2Lexer.c @srcdir@/generated/Smt2Parser.h @srcdir@/generated/Smt2Parser.c $(ANTLR_TOKEN_STUFF): @srcdir@/generated/Smt2Lexer.h
+generated/Smt2Lexer.c generated/Smt2Parser.h generated/Smt2Parser.c $(ANTLR_TOKEN_STUFF): generated/Smt2Lexer.h
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 93d596264..dd0ccb0ad 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -183,19 +183,19 @@ command returns [CVC4::Command* cmd = NULL]
       $cmd = new SetBenchmarkLogicCommand(name); }
   | SET_INFO_TOK KEYWORD symbolicExpr[sexpr]
     { name = AntlrInput::tokenText($KEYWORD);
-      PARSER_STATE->setInfo(name,sexpr);
-      cmd = new SetInfoCommand(name,sexpr); }
+      PARSER_STATE->setInfo(name.c_str() + 1, sexpr);
+      cmd = new SetInfoCommand(name.c_str() + 1, sexpr); }
   | /* get-info */
     GET_INFO_TOK KEYWORD
-    { cmd = new GetInfoCommand(AntlrInput::tokenText($KEYWORD)); }
+    { cmd = new GetInfoCommand(AntlrInput::tokenText($KEYWORD).c_str() + 1); }
   | /* set-option */
     SET_OPTION_TOK KEYWORD symbolicExpr[sexpr]
     { name = AntlrInput::tokenText($KEYWORD);
-      PARSER_STATE->setOption(name,sexpr);
-      cmd = new SetOptionCommand(name,sexpr); }
+      PARSER_STATE->setOption(name.c_str() + 1, sexpr);
+      cmd = new SetOptionCommand(name.c_str() + 1, sexpr); }
   | /* get-option */
     GET_OPTION_TOK KEYWORD
-    { cmd = new GetOptionCommand(AntlrInput::tokenText($KEYWORD)); }
+    { cmd = new GetOptionCommand(AntlrInput::tokenText($KEYWORD).c_str() + 1); }
   | /* sort declaration */
     DECLARE_SORT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     symbol[name,CHECK_UNDECLARED,SYM_SORT]
diff --git a/src/parser/tptp/Makefile.am b/src/parser/tptp/Makefile.am
index 4ec1717e9..3113a523c 100644
--- a/src/parser/tptp/Makefile.am
+++ b/src/parser/tptp/Makefile.am
@@ -15,14 +15,14 @@ ANTLR_OPTS =
 noinst_LTLIBRARIES = libparsertptp.la
 
 ANTLR_TOKEN_STUFF = \
-	@srcdir@/generated/Tptp.tokens
+	generated/Tptp.tokens
 ANTLR_LEXER_STUFF = \
-	@srcdir@/generated/TptpLexer.h \
-	@srcdir@/generated/TptpLexer.c \
+	generated/TptpLexer.h \
+	generated/TptpLexer.c \
 	$(ANTLR_TOKEN_STUFF)
 ANTLR_PARSER_STUFF = \
-	@srcdir@/generated/TptpParser.h \
-	@srcdir@/generated/TptpParser.c
+	generated/TptpParser.h \
+	generated/TptpParser.c
 ANTLR_STUFF = \
 	$(ANTLR_LEXER_STUFF) \
 	$(ANTLR_PARSER_STUFF)
@@ -35,27 +35,25 @@ libparsertptp_la_SOURCES = \
 	tptp_input.cpp \
 	$(ANTLR_STUFF)
 
-BUILT_SOURCES = $(ANTLR_STUFF) @srcdir@/stamp-generated
-
-EXTRA_DIST = @srcdir@/stamp-generated
+BUILT_SOURCES = $(ANTLR_STUFF) stamp-generated
 
 MAINTAINERCLEANFILES = $(ANTLR_STUFF)
 maintainer-clean-local:
-	-$(AM_V_at)rmdir @srcdir@/generated
-	-$(AM_V_at)rm -f @srcdir@/stamp-generated
+	-$(AM_V_at)rmdir generated
+	-$(AM_V_at)rm -f stamp-generated
 
-@srcdir@/stamp-generated:
-	$(AM_V_at)mkdir -p @srcdir@/generated
-	$(AM_V_at)touch @srcdir@/stamp-generated
+stamp-generated:
+	$(AM_V_at)mkdir -p generated
+	$(AM_V_at)touch stamp-generated
 
 # antlr doesn't overwrite output files, it just leaves them.  So we have to delete them first.
-@srcdir@/generated/TptpLexer.h: Tptp.g @srcdir@/stamp-generated
+generated/TptpLexer.h: Tptp.g stamp-generated
 	-$(AM_V_at)rm -f $(ANTLR_STUFF)
 	@if test -z "$(ANTLR)"; then echo "ERROR: antlr parser generator cannot be found, cannot generate the parser" >&2; exit 1; fi
-	$(AM_V_GEN)$(ANTLR) $(ANTLR_OPTS) -fo "@srcdir@/generated" "@srcdir@/Tptp.g"
+	$(AM_V_GEN)$(ANTLR) $(ANTLR_OPTS) -fo "generated" "@srcdir@/Tptp.g"
 
 # These don't actually depend on TptpLexer.h, but if we're doing parallel
 # make and the lexer needs to be rebuilt, we have to keep the rules
 # from running in parallel (since the token files will be deleted &
 # recreated)
-@srcdir@/generated/TptpLexer.c @srcdir@/generated/TptpParser.h @srcdir@/generated/TptpParser.c $(ANTLR_TOKEN_STUFF): @srcdir@/generated/TptpLexer.h
+generated/TptpLexer.c generated/TptpParser.h generated/TptpParser.c $(ANTLR_TOKEN_STUFF): generated/TptpLexer.h