* Clean up some options documentation

* Remove defunct --no-theory-registration option
* Point people to Wiki tutorial
* Modernize the cut-release script
* Misc cleanup, documentation

(this commit was certified error- and warning-free by the test-and-commit script.)

24 files changed, 224 insertions, 85 deletions

diff --git a/INSTALL b/INSTALL
index e2cceb967..3008a576c 100644
--- a/INSTALL
+++ b/INSTALL
@@ -136,8 +136,8 @@ from Fedora RPMs or our Debian packages, the process should be
 completely automatic, since the libraries and headers are installed in
 a standard location.  If you download the sources yourself, you need
 to build them in a special way.  Fortunately, the
-"contrib/build-cudd-with-libtool.sh" script in the CVC4 source tree
-does exactly what you need: it patches the CUDD makefiles to use
+"contrib/build-cudd-2.4.2-with-libtool.sh" script in the CVC4 source
+tree does exactly what you need: it patches the CUDD makefiles to use
 libtool, builds the libtool libraries, then reverses the patch to
 leave the makefiles as they were.  Once you run this script on an
 unpacked CUDD 2.4.2 source distribution, then CVC4's configure script
@@ -149,9 +149,9 @@ configure script; this makes it a hard requirement rather than an
 optional add-on.
 
 The NYU-provided Debian packaging of CUDD 2.4.2 and CUDD 2.5.0 are
-here:
+here (along with the CVC4 Debian packages):
 
-  deb http://goedel.cims.nyu.edu/cvc4-builds/debian unstable/
+  deb http://cvc4.cs.nyu.edu/debian/ unstable/
 
 The Debian source package "cudd", available from the same repository,
 includes a diff of all changes made to cudd makefiles.
diff --git a/NEWS b/NEWS
index 860c27633..ad3373cf7 100644
--- a/NEWS
+++ b/NEWS
@@ -1,3 +1,3 @@
-This is a prerelease version of CVC4; distribution is restricted.
+Preparing for the first public release, CVC4 1.0.
 
--- Morgan Deters <mdeters@cs.nyu.edu>  Mon, 02 Nov 2009 17:54:27 -0500
+-- Morgan Deters <mdeters@cs.nyu.edu>  Sat, 06 Oct 2012 13:22:31 -0400
diff --git a/README b/README
index ad9c8eb7e..73865d123 100644
--- a/README
+++ b/README
@@ -21,6 +21,17 @@ predecessors.  It is written entirely in C++ and is released under a
 free software license (see the file COPYING in the source
 distribution).
 
+*** Getting started with CVC4
+
+For help installing CVC4, see the INSTALL file that comes with this
+distribution.
+
+We recommend that you visit our CVC4 tutorials online at:
+
+  http://cvc4.cs.nyu.edu/wiki/Tutorials
+
+for help getting started using CVC4.
+
 *** The History of CVC4
 
 The Cooperating Validity Checker series has a long history.  The
diff --git a/config/readline.m4 b/config/readline.m4
index 30d285b29..90785c7a0 100644
--- a/config/readline.m4
+++ b/config/readline.m4
@@ -14,11 +14,16 @@ else
   else
     AC_MSG_RESULT([yes, readline enabled by user])
   fi
+  dnl Try a bunch of combinations until something works :-/
   READLINE_LIBS=
   CVC4_TRY_READLINE_WITH([])
   CVC4_TRY_READLINE_WITH([-ltinfo])
+  CVC4_TRY_READLINE_WITH([-ltermcap])
+  CVC4_TRY_READLINE_WITH([-ltermcap -ltinfo])
   CVC4_TRY_READLINE_WITH([-lncurses -ltermcap])
   CVC4_TRY_READLINE_WITH([-lncurses -ltermcap -ltinfo])
+  CVC4_TRY_READLINE_WITH([-lcurses -ltermcap])
+  CVC4_TRY_READLINE_WITH([-lcurses -ltermcap -ltinfo])
   if test -z "$READLINE_LIBS"; then
     if test "$with_readline" != check; then
       AC_MSG_FAILURE([cannot find libreadline! (or can't get it to work)])
@@ -27,24 +32,26 @@ else
   else
     # make sure it works in static builds, too
     if test "$enable_static_binary" = yes; then
+      READLINE_LIBS=
       AC_MSG_CHECKING([whether statically-linked readline is functional])
-      AC_LANG_PUSH([C++])
-      cvc4_save_LIBS="$LIBS"
-      cvc4_save_LDFLAGS="$LDFLAGS"
-      LDFLAGS="-static $LDFLAGS"
-      LIBS="$READLINE_LIBS $LIBS"
-      AC_LINK_IFELSE([AC_LANG_PROGRAM([#include <readline/readline.h>],
-                                      [readline("")])],
-        [ AC_MSG_RESULT([yes, it works])
-          with_readline=yes ],
-        [ AC_MSG_RESULT([no])
-          if test "$with_readline" != check; then
-            AC_MSG_FAILURE([readline installation incompatible with static-binary])
-          fi
-          with_readline=no ])
-      LIBS="$cvc4_save_LIBS"
-      LDFLAGS="$cvc4_save_LDFLAGS"
-      AC_LANG_POP([C++])
+      CVC4_TRY_STATIC_READLINE_WITH([])
+      CVC4_TRY_STATIC_READLINE_WITH([-ltinfo])
+      CVC4_TRY_STATIC_READLINE_WITH([-ltermcap])
+      CVC4_TRY_STATIC_READLINE_WITH([-ltermcap -ltinfo])
+      CVC4_TRY_STATIC_READLINE_WITH([-lncurses -ltermcap])
+      CVC4_TRY_STATIC_READLINE_WITH([-lncurses -ltermcap -ltinfo])
+      CVC4_TRY_STATIC_READLINE_WITH([-lcurses -ltermcap])
+      CVC4_TRY_STATIC_READLINE_WITH([-lcurses -ltermcap -ltinfo])
+      if test -n "$READLINE_LIBS"; then
+        AC_MSG_RESULT([yes, it works])
+        with_readline=yes
+      else
+        AC_MSG_RESULT([no])
+        if test "$with_readline" != check; then
+          AC_MSG_FAILURE([readline installation appears incompatible with static-binary])
+        fi
+        with_readline=no
+      fi
     else
       with_readline=yes
     fi
@@ -70,3 +77,23 @@ if test -z "$READLINE_LIBS"; then
                [], [$1])
 fi
 ])# CVC4_TRY_READLINE_WITH
+
+# CVC4_TRY_STATIC_READLINE_WITH(LIBS)
+# -----------------------------------
+# Try AC_CHECK_LIB(readline) with the given linking libraries
+AC_DEFUN([CVC4_TRY_STATIC_READLINE_WITH], [
+if test -z "$READLINE_LIBS"; then
+  AC_LANG_PUSH([C++])
+  cvc4_save_LIBS="$LIBS"
+  cvc4_save_LDFLAGS="$LDFLAGS"
+  LDFLAGS="-static $LDFLAGS"
+  LIBS="-lreadline $1"
+  AC_LINK_IFELSE([AC_LANG_PROGRAM([#include <readline/readline.h>],
+                                  [readline("")])],
+    [READLINE_LIBS="-lreadline $1"],
+    [])
+  LIBS="$cvc4_save_LIBS"
+  LDFLAGS="$cvc4_save_LDFLAGS"
+  AC_LANG_POP([C++])
+fi
+])# CVC4_TRY_STATIC_READLINE_WITH
diff --git a/contrib/cut-release b/contrib/cut-release
index ec5ee9c87..97bc31bb1 100755
--- a/contrib/cut-release
+++ b/contrib/cut-release
@@ -4,7 +4,11 @@
 #
 
 function isthatright {
-  echo -n "Does that look right? [y/n] "
+  if [ -z "$1" ]; then
+    echo -n "Does that look right? [y/n] "
+  else
+    echo -n "$1? [y/n] "
+  fi
   while read yn; do
     if [ "$yn" = y -o "$yn" = Y -o "$yn" = yes -o "$yn" = YES -o "$yn" = Yes ]; then
       break
@@ -111,6 +115,20 @@ if [ -n "$suspect_files" ]; then
   $dryrun || exit 1
 fi
 
+echo "Checking NEWS file for recent updates..."
+if [ -n "$(svn status -q NEWS)" ]; then
+  echo "+ It's locally modified."
+else
+  echo -n "+ "
+  svn info NEWS | grep '^Last Changed Date: '
+  echo
+  echo "You should probably make sure to put some notes in the NEWS file"
+  echo "for this release, indicating the most important changes from the"
+  echo "last release."
+  echo
+  isthatright "Continue without updating NEWS"
+fi
+
 echo "Adjusting version info lines in configure.ac..."
 if ! grep '^m4_define(_CVC4_MAJOR,  *[0-9][0-9]* *)' configure.ac &>/dev/null ||
    ! grep '^m4_define(_CVC4_MINOR,  *[0-9][0-9]* *)' configure.ac &>/dev/null ||
@@ -152,11 +170,11 @@ if ! $SHELL -c '\
 	./autogen.sh || echo "autoconf failed; does library_versions have something to match $version?"; \
 	mkdir "release-$version"; \
 	cd "release-$version"; \
-	../configure production-cln-staticbinary --disable-shared --enable-unit-testing --with-gmp --without-cudd --with-readline --with-portfolio; \
+	../configure production-cln-staticbinary --disable-shared --enable-unit-testing --without-cudd --with-readline --with-portfolio; \
 	make dist "$@"; \
 	tar xf "cvc4-$version.tar.gz"; \
 	cd "cvc4-$version"; \
-	./configure production-cln-staticbinary --disable-shared --enable-unit-testing --with-gmp --without-cudd --with-readline --with-portfolio; \
+	./configure production-cln-staticbinary --disable-shared --enable-unit-testing --without-cudd --with-readline --with-portfolio; \
 	make check "$@"; \
 	make distcheck "$@"; \
 '; then
@@ -211,5 +229,22 @@ echo "About to run: svn copy -m \"Cutting release $version.\" \"$root\" \"https:
 isthatright
 $dryrun || svn copy -m "Cutting release $version." "$root" "https://subversive.cims.nyu.edu/cvc4/cvc4/tags/releases/$version"
 
+echo
+if [ "$(svn info | grep '^URL: https://subversive.cims.nyu.edu/cvc4/cvc4/trunk$')" ]; then
+  if [ "$release" = 0 ]; then
+    echo "About to run: svn copy -m \"Branching release $version for bugfixes.\" \"https://subversive.cims.nyu.edu/cvc4/cvc4/tags/releases/$version\" \"https://subversive.cims.nyu.edu/cvc4/cvc4/branches/releases/$version.x\""
+    isthatright
+    $dryrun || svn copy -m "Branching release $version for bugfixes." "https://subversive.cims.nyu.edu/cvc4/cvc4/tags/releases/$version" "https://subversive.cims.nyu.edu/cvc4/cvc4/branches/releases/$version.x"
+  else
+    echo "Not branching, because this is a minor release (i.e., not a \"dot-oh\""
+    echo "release), so I'm guessing you have a devel repository outside of trunk"
+    echo "somewhere?  You can still make a branch manually, of course."
+  fi
+else
+  echo "Not branching, because it appears there already is a branch"
+  echo "to work with for version $version ..?  (You're not on trunk.)"
+  echo "You can still make a branch manually, of course."
+fi
+
 trap '' EXIT
 
diff --git a/doc/SmtEngine.3cvc_template.in b/doc/SmtEngine.3cvc_template.in
index 99b0451f6..835bef585 100644
--- a/doc/SmtEngine.3cvc_template.in
+++ b/doc/SmtEngine.3cvc_template.in
@@ -1,7 +1,7 @@
 .\" Process this file with
-.\" groff -man -Tascii SmtEngine.3cvc4
+.\" groff -man -Tascii SmtEngine.3cvc
 .\"
-.TH SMTENGINE 3cvc4 "@MAN_DATE@" "CVC4 release @VERSION@" "CVC4 Library Interfaces"
+.TH SMTENGINE 3cvc "@MAN_DATE@" "CVC4 release @VERSION@" "CVC4 Library Interfaces"
 .SH NAME
 SmtEngine \- the primary interface to CVC4's theorem-proving capabilities
 .SH DESCRIPTION
diff --git a/doc/options.3cvc_template.in b/doc/options.3cvc_template.in
index 8ee39b761..86f2ff976 100644
--- a/doc/options.3cvc_template.in
+++ b/doc/options.3cvc_template.in
@@ -1,7 +1,7 @@
 .\" Process this file with
-.\" groff -man -Tascii options.3cvc4
+.\" groff -man -Tascii options.3cvc
 .\"
-.TH OPTIONS 3cvc4 "@MAN_DATE@" "CVC4 release @VERSION@" "CVC4 Internals Documentation"
+.TH OPTIONS 3cvc "@MAN_DATE@" "CVC4 release @VERSION@" "CVC4 Internals Documentation"
 .SH NAME
 options \- the options infrastructure
 
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 8f8e19f81..d2adf97c4 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -313,6 +313,11 @@ int runCvc4(int argc, char* argv[], Options& opts) {
       pExecutor->flushStatistics(*opts[options::err]);
     }
 
+    // make sure to flush replay output log before early-exit
+    if( opts[options::replayLog] != NULL ) {
+      *opts[options::replayLog] << flush;
+    }
+
 #ifdef CVC4_DEBUG
     if(opts[options::earlyExit] && opts.wasSetByUser(options::earlyExit)) {
       _exit(returnValue);
diff --git a/src/options/mkoptions b/src/options/mkoptions
index 48050ef7e..9ef05c1b2 100755
--- a/src/options/mkoptions
+++ b/src/options/mkoptions
@@ -142,20 +142,31 @@ function module {
   CVC4_OPTIONS__${module_id}__FOR_OPTION_HOLDER"
   module_optionholder_spec="#define CVC4_OPTIONS__${module_id}__FOR_OPTION_HOLDER"
 
+  previous_remaining_documentation="${remaining_documentation}"
   remaining_documentation="${remaining_documentation}\\n\\n\"
 #line $lineno \"$kf\"
-\"$module_name options:"
+\"From the $module_name module:"
+  remaining_documentation_at_start_of_module="${remaining_documentation}"
+
+  previous_remaining_manpage_documentation="${remaining_manpage_documentation}"
   remaining_manpage_documentation="${remaining_manpage_documentation}
 .SH `echo "$module_name" | tr a-z A-Z` OPTIONS
 "
+  remaining_manpage_documentation_at_start_of_module="${remaining_manpage_documentation}"
+
+  previous_remaining_manpage_smt_documentation="${remaining_manpage_smt_documentation}"
   remaining_manpage_smt_documentation="${remaining_manpage_smt_documentation}
 .TP
 .I \"`echo "$module_name" | tr a-z A-Z` OPTIONS\"
 "
+  remaining_manpage_smt_documentation_at_start_of_module="${remaining_manpage_smt_documentation}"
+
+  previous_remaining_manpage_internals_documentation="${remaining_manpage_internals_documentation}"
   remaining_manpage_internals_documentation="${remaining_manpage_internals_documentation}
 .TP
 .I \"`echo "$module_name" | tr a-z A-Z` OPTIONS\"
 "
+  remaining_manpage_internals_documentation_at_start_of_module="${remaining_manpage_internals_documentation}"
 }
 
 function endmodule {
@@ -166,6 +177,24 @@ function endmodule {
   if [ $# -ne 0 ]; then
     ERR "endmodule takes no arguments"
   fi
+
+  # check, and if no documented options, remove the headers
+
+  if [ "$remaining_documentation" = "$remaining_documentation_at_start_of_module" ]; then
+    remaining_documentation="$previous_remaining_documentation"
+  fi
+
+  if [ "$remaining_manpage_documentation" = "$remaining_manpage_documentation_at_start_of_module" ]; then
+    remaining_manpage_documentation="$previous_remaining_manpage_documentation"
+  fi
+
+  if [ "$remaining_manpage_smt_documentation" = "$remaining_manpage_smt_documentation_at_start_of_module" ]; then
+    remaining_manpage_smt_documentation="$previous_remaining_manpage_smt_documentation"
+  fi
+
+  if [ "$remaining_manpage_internals_documentation" = "$remaining_manpage_internals_documentation_at_start_of_module" ]; then
+    remaining_manpage_internals_documentation="$previous_remaining_manpage_internals_documentation"
+  fi
 }
 
 function common-option {
diff --git a/src/printer/Makefile.am b/src/printer/Makefile.am
index bb94d75de..21997d2dc 100644
--- a/src/printer/Makefile.am
+++ b/src/printer/Makefile.am
@@ -10,6 +10,8 @@ libprinter_la_SOURCES = \
 	printer.cpp \
 	dagification_visitor.h \
 	dagification_visitor.cpp \
+	model_format_mode.h \
+	model_format_mode.cpp \
 	ast/ast_printer.h \
 	ast/ast_printer.cpp \
 	smt1/smt1_printer.h \
@@ -19,4 +21,5 @@ libprinter_la_SOURCES = \
 	cvc/cvc_printer.h \
 	cvc/cvc_printer.cpp
 
-EXTRA_DIST =
+EXTRA_DIST = \
+	options_handlers.h
diff --git a/src/smt/model_format_mode.cpp b/src/printer/model_format_mode.cpp
index ffaa3df95..df3585bcf 100644
--- a/src/smt/model_format_mode.cpp
+++ b/src/printer/model_format_mode.cpp
@@ -17,7 +17,7 @@
  ** \todo document this file
  **/
 
-#include "smt/model_format_mode.h"
+#include "printer/model_format_mode.h"
 
 namespace CVC4 {
 
diff --git a/src/smt/model_format_mode.h b/src/printer/model_format_mode.h
index 3c0a3569e..bdfa5721a 100644
--- a/src/smt/model_format_mode.h
+++ b/src/printer/model_format_mode.h
@@ -19,8 +19,8 @@
 
 #include "cvc4_public.h"
 
-#ifndef __CVC4__SMT__MODEL_FORMAT_MODE_H
-#define __CVC4__SMT__MODEL_FORMAT_MODE_H
+#ifndef __CVC4__PRINTER__MODEL_FORMAT_MODE_H
+#define __CVC4__PRINTER__MODEL_FORMAT_MODE_H
 
 #include <iostream>
 
@@ -38,4 +38,4 @@ std::ostream& operator<<(std::ostream& out, ModelFormatMode mode) CVC4_PUBLIC;
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4__SMT__MODEL_FORMAT_H */
+#endif /* __CVC4__PRINTER__MODEL_FORMAT_H */
diff --git a/src/printer/options b/src/printer/options
index d95c7457d..7e1b67986 100644
--- a/src/printer/options
+++ b/src/printer/options
@@ -5,4 +5,7 @@
 
 module PRINTER "printer/options.h" Printing
 
+option modelFormatMode --model-format=MODE ModelFormatMode :handler CVC4::printer::stringToModelFormatMode :default MODEL_FORMAT_MODE_DEFAULT :read-write :include "printer/model_format_mode.h" :handler-include "printer/options_handlers.h"
+ print format mode for models, see --model-format=help
+
 endmodule
diff --git a/src/printer/options_handlers.h b/src/printer/options_handlers.h
new file mode 100644
index 000000000..dea5a383c
--- /dev/null
+++ b/src/printer/options_handlers.h
@@ -0,0 +1,56 @@
+/*********************                                                        */
+/*! \file options_handlers.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Custom handlers and predicates for printer options
+ **
+ ** Custom handlers and predicates for printer options.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PRINTER__OPTIONS_HANDLERS_H
+#define __CVC4__PRINTER__OPTIONS_HANDLERS_H
+
+#include "printer/model_format_mode.h"
+
+namespace CVC4 {
+namespace printer {
+
+static const std::string modelFormatHelp = "\
+Model format modes currently supported by the --model-format option:\n\
+\n\
+default \n\
++ Print model as expressions in the output language format.\n\
+\n\
+table\n\
++ Print functional expressions over finite domains in a table format.\n\
+";
+
+inline ModelFormatMode stringToModelFormatMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
+  if(optarg == "default") {
+    return MODEL_FORMAT_MODE_DEFAULT;
+  } else if(optarg == "table") {
+    return MODEL_FORMAT_MODE_TABLE;
+  } else if(optarg == "help") {
+    puts(modelFormatHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --model-format: `") +
+                          optarg + "'.  Try --model-format help.");
+  }
+}
+
+}/* CVC4::printer namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__PRINTER__OPTIONS_HANDLERS_H */
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 9ed2202fe..1434cf6c7 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -28,6 +28,7 @@
 #include "decision/options.h"
 #include "util/lemma_input_channel.h"
 #include "util/lemma_output_channel.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace prop {
@@ -170,11 +171,11 @@ SatLiteral TheoryProxy::getNextReplayDecision() {
     Expr e = options::replayStream()->nextExpr();
     if(!e.isNull()) { // we get null node when out of decisions to replay
       // convert & return
+      ++d_replayedDecisions;
       return d_cnfStream->getLiteral(e);
     }
   }
 #endif /* CVC4_REPLAY */
-  //FIXME!
   return undefSatLiteral;
 }
 
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index 96332217e..5fa133122 100644
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -71,6 +71,12 @@ class TheoryProxy {
    */
   std::hash_set<Node, NodeHashFunction> d_shared;
 
+  /**
+   * Statistic: the number of replayed decisions (via --replay).
+   */
+  KEEP_STATISTIC(IntStat, d_replayedDecisions,
+                 "prop::theoryproxy::replayedDecisions", 0);
+
 public:
   TheoryProxy(PropEngine* propEngine,
               TheoryEngine* theoryEngine,
diff --git a/src/smt/Makefile.am b/src/smt/Makefile.am
index 8aa3e1630..6f5b8fe76 100644
--- a/src/smt/Makefile.am
+++ b/src/smt/Makefile.am
@@ -14,9 +14,7 @@ libsmt_la_SOURCES = \
 	command_list.h \
 	modal_exception.h \
 	simplification_mode.h \
-	simplification_mode.cpp \
-	model_format_mode.h \
-	model_format_mode.cpp
+	simplification_mode.cpp
 
 nodist_libsmt_la_SOURCES = \
 	smt_options.cpp
diff --git a/src/smt/options b/src/smt/options
index 24c8b5e43..5be462195 100644
--- a/src/smt/options
+++ b/src/smt/options
@@ -15,9 +15,8 @@ option simplificationMode simplification-mode --simplification=MODE Simplificati
 alias --no-simplification = --simplification=none
  turn off all simplification (same as --simplification=none)
 
-option doStaticLearning static-learning /--no-static-learning bool :default true
+option doStaticLearning static-learning --static-learning bool :default true
  use static learning (on by default)
-/turn off static learning (e.g. diamond-breaking)
 
 option expandDefinitions expand-definitions bool :default false
  always expand symbol definitions in output
@@ -25,15 +24,13 @@ common-option produceModels produce-models -m --produce-models bool :default fal
  support the get-value and get-model commands
 option checkModels check-models --check-models bool :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
  after SAT/INVALID, double-check that the generated model satisfies all user assertions
-common-option proof produce-proofs --proof bool :default false :predicate CVC4::smt::proofEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
+option proof produce-proofs --proof bool :default false :predicate CVC4::smt::proofEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
  turn on proof generation
 # this is just a placeholder for later; it doesn't show up in command-line options listings
-common-option unsatCores produce-unsat-cores bool :predicate CVC4::smt::unsatCoresEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
+undocumented-option unsatCores produce-unsat-cores --produce-unsat-cores bool :predicate CVC4::smt::unsatCoresEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
  turn on unsat core generation (NOT YET SUPPORTED)
-common-option produceAssignments produce-assignments --produce-assignments bool :default false :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
+option produceAssignments produce-assignments --produce-assignments bool :default false :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
  support the get-assignment command
-option modelFormatMode --model-format=MODE ModelFormatMode :handler CVC4::smt::stringToModelFormatMode :default MODEL_FORMAT_MODE_DEFAULT :read-write :include "smt/model_format_mode.h" :handler-include "smt/options_handlers.h"
- print format mode for models, see --model-format=help
 
 # This could go in src/main/options, but by SMT-LIBv2 spec, "interactive"
 # is a mode in which the assertion list must be kept.  So it belongs here.
@@ -42,15 +39,12 @@ common-option interactive interactive-mode --interactive bool :read-write
 
 option doITESimp --ite-simp bool :read-write
  turn on ite simplification (Kim (and Somenzi) et al., SAT 2009)
-/turn off ite simplification (Kim (and Somenzi) et al., SAT 2009)
 
 option unconstrainedSimp --unconstrained-simp bool :default false :read-write
  turn on unconstrained simplification (see Bruttomesso/Brummayer PhD thesis)
-/turn off unconstrained simplification (see Bruttomesso/Brummayer PhD thesis)
 
 option repeatSimp --repeat-simp bool :read-write
  make multiple passes with nonclausal simplifier
-/do not make multiple passes with nonclausal simplifier
 
 common-option incrementalSolving incremental -i --incremental bool
  enable incremental solving
@@ -69,9 +63,10 @@ common-option cumulativeResourceLimit --rlimit=N "unsigned long"
 common-option perCallResourceLimit --rlimit-per=N "unsigned long"
  enable resource limiting per query
 
-option replayFilename --replay=FILE std::string :handler CVC4::smt::checkReplayFilename :handler-include "smt/options_handlers.h"
+# --replay is currently broken; don't document it for 1.0
+undocumented-option replayFilename --replay=FILE std::string :handler CVC4::smt::checkReplayFilename :handler-include "smt/options_handlers.h"
  replay decisions from file
-option replayLog --replay-log=FILE std::ostream* :handler CVC4::smt::checkReplayLogFilename :handler-include "smt/options_handlers.h"
+undocumented-option replayLog --replay-log=FILE std::ostream* :handler CVC4::smt::checkReplayLogFilename :handler-include "smt/options_handlers.h"
  log decisions and propagations to file
 option replayStream ExprStream*
 
diff --git a/src/smt/options_handlers.h b/src/smt/options_handlers.h
index 2af826d24..43d53ee4c 100644
--- a/src/smt/options_handlers.h
+++ b/src/smt/options_handlers.h
@@ -154,16 +154,6 @@ none\n\
 + do not perform nonclausal simplification\n\
 ";
 
-static const std::string modelFormatHelp = "\
-Model format modes currently supported by the --model-format option:\n\
-\n\
-default \n\
-+ Print model as expressions in the output language format.\n\
-\n\
-table\n\
-+ Print functional expressions over finite domains in a table format.\n\
-";
-
 inline void dumpMode(std::string option, std::string optarg, SmtEngine* smt) {
 #ifdef CVC4_DUMPING
   char* optargPtr = strdup(optarg.c_str());
@@ -271,20 +261,6 @@ inline SimplificationMode stringToSimplificationMode(std::string option, std::st
   }
 }
 
-inline ModelFormatMode stringToModelFormatMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
-  if(optarg == "default") {
-    return MODEL_FORMAT_MODE_DEFAULT;
-  } else if(optarg == "table") {
-    return MODEL_FORMAT_MODE_TABLE;
-  } else if(optarg == "help") {
-    puts(modelFormatHelp.c_str());
-    exit(1);
-  } else {
-    throw OptionException(std::string("unknown option for --model-format: `") +
-                          optarg + "'.  Try --model-format help.");
-  }
-}
-
 // ensure we haven't started search yet
 inline void beforeSearch(std::string option, bool value, SmtEngine* smt) throw(ModalException) {
   if(smt != NULL && smt->d_fullyInited) {
diff --git a/src/theory/arith/options b/src/theory/arith/options
index 8b45a6da2..38cf07251 100644
--- a/src/theory/arith/options
+++ b/src/theory/arith/options
@@ -43,8 +43,7 @@ option arithPropagateMaxLength --prop-row-length=N uint16_t :default 16
  sets the maximum row length to be used in propagation
 
 option arithDioSolver /--disable-dio-solver bool :default true
- use Linear Diophantine Equation solver (Griggio, JSAT 2012)
-/turns off Linear Diophantine Equation solver (Griggio, JSAT 2012)
+ turns off Linear Diophantine Equation solver (Griggio, JSAT 2012)
 
 # Whether to split (= x y) into (and (<= x y) (>= x y)) in
 # arithmetic preprocessing.
diff --git a/src/theory/datatypes/options b/src/theory/datatypes/options
index ab627000e..45849858a 100644
--- a/src/theory/datatypes/options
+++ b/src/theory/datatypes/options
@@ -9,7 +9,7 @@ module DATATYPES "theory/datatypes/options.h" Datatypes theory
 # then we do not rewrite such a selector term to an arbitrary ground term.  
 # For example, by default cvc4 considers cdr( nil ) = nil.  If this option is set, then
 # cdr( nil ) has no set value.
-option dtRewriteErrorSel /--disable-dt-rewrite-error-sel bool :default true
+expert-option dtRewriteErrorSel /--disable-dt-rewrite-error-sel bool :default true
  disable rewriting incorrectly applied selectors to arbitrary ground term
  
 endmodule
diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index a4cbd720b..6a7d2ecef 100644
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -18,7 +18,6 @@
 #include "theory/quantifiers_engine.h"
 #include "theory/theory_engine.h"
 #include "theory/type_enumerator.h"
-#include "smt/model_format_mode.h"
 #include "smt/options.h"
 #include "theory/uf/theory_uf_model.h"
 
diff --git a/src/theory/options b/src/theory/options
index 40d26472f..5a523f0fa 100644
--- a/src/theory/options
+++ b/src/theory/options
@@ -5,9 +5,6 @@
 
 module THEORY "theory/options.h" Theory layer
 
-expert-option theoryRegistration /--no-theory-registration bool :default true
- disable theory reg (not safe for some theories)
-
 expert-option theoryOfMode --theoryof-mode=MODE CVC4::theory::TheoryOfMode :handler CVC4::theory::stringToTheoryOfMode :handler-include "theory/options_handlers.h" :default CVC4::theory::THEORY_OF_TYPE_BASED :include "theory/theoryof_mode.h"
  mode for theoryof
 
diff --git a/src/theory/uf/options b/src/theory/uf/options
index f199f6c1b..0799ba4d5 100644
--- a/src/theory/uf/options
+++ b/src/theory/uf/options
@@ -5,9 +5,8 @@
 
 module UF "theory/uf/options.h" Uninterpreted functions theory
 
-option ufSymmetryBreaker uf-symmetry-breaker --enable-symmetry-breaker/--disable-symmetry-breaker bool :read-write :default true
+option ufSymmetryBreaker uf-symmetry-breaker --symmetry-breaker bool :read-write :default true
  use UF symmetry breaker (Deharbe et al., CADE 2011)
-/turns off UF symmetry breaker (Deharbe et al., CADE 2011)
 
 option ufssRegions /--disable-uf-ss-regions bool :default true
  disable region-based method for discovering cliques and splits in uf strong solver