From: Morgan Deters Date: Sat, 6 Oct 2012 18:53:27 +0000 (+0000) Subject: * Clean up some options documentation X-Git-Tag: cvc5-1.0.0~7732 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4e883ffc0b88256a966183ac6b87bb5767154cdf;p=cvc5.git * 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.) --- 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 Mon, 02 Nov 2009 17:54:27 -0500 +-- Morgan Deters 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("")])], - [ 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_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/printer/model_format_mode.cpp b/src/printer/model_format_mode.cpp new file mode 100644 index 000000000..df3585bcf --- /dev/null +++ b/src/printer/model_format_mode.cpp @@ -0,0 +1,39 @@ +/********************* */ +/*! \file model_format_mode.cpp + ** \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 [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "printer/model_format_mode.h" + +namespace CVC4 { + +std::ostream& operator<<(std::ostream& out, ModelFormatMode mode) { + switch(mode) { + case MODEL_FORMAT_MODE_DEFAULT: + out << "MODEL_FORMAT_MODE_DEFAULT"; + break; + case MODEL_FORMAT_MODE_TABLE: + out << "MODEL_FORMAT_MODE_TABLE"; + break; + default: + out << "ModelFormatMode:UNKNOWN![" << unsigned(mode) << "]"; + } + + return out; +} + +}/* CVC4 namespace */ diff --git a/src/printer/model_format_mode.h b/src/printer/model_format_mode.h new file mode 100644 index 000000000..bdfa5721a --- /dev/null +++ b/src/printer/model_format_mode.h @@ -0,0 +1,41 @@ +/********************* */ +/*! \file model_format_mode.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 [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__PRINTER__MODEL_FORMAT_MODE_H +#define __CVC4__PRINTER__MODEL_FORMAT_MODE_H + +#include + +namespace CVC4 { + +/** Enumeration of model_format modes (how to print models from get-model command). */ +typedef enum { + /** default mode (print expressions in the output language format) */ + MODEL_FORMAT_MODE_DEFAULT, + /** print functional values in a table format */ + MODEL_FORMAT_MODE_TABLE, +} ModelFormatMode; + +std::ostream& operator<<(std::ostream& out, ModelFormatMode mode) CVC4_PUBLIC; + +}/* CVC4 namespace */ + +#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 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/model_format_mode.cpp b/src/smt/model_format_mode.cpp deleted file mode 100644 index ffaa3df95..000000000 --- a/src/smt/model_format_mode.cpp +++ /dev/null @@ -1,39 +0,0 @@ -/********************* */ -/*! \file model_format_mode.cpp - ** \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 [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "smt/model_format_mode.h" - -namespace CVC4 { - -std::ostream& operator<<(std::ostream& out, ModelFormatMode mode) { - switch(mode) { - case MODEL_FORMAT_MODE_DEFAULT: - out << "MODEL_FORMAT_MODE_DEFAULT"; - break; - case MODEL_FORMAT_MODE_TABLE: - out << "MODEL_FORMAT_MODE_TABLE"; - break; - default: - out << "ModelFormatMode:UNKNOWN![" << unsigned(mode) << "]"; - } - - return out; -} - -}/* CVC4 namespace */ diff --git a/src/smt/model_format_mode.h b/src/smt/model_format_mode.h deleted file mode 100644 index 3c0a3569e..000000000 --- a/src/smt/model_format_mode.h +++ /dev/null @@ -1,41 +0,0 @@ -/********************* */ -/*! \file model_format_mode.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 [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "cvc4_public.h" - -#ifndef __CVC4__SMT__MODEL_FORMAT_MODE_H -#define __CVC4__SMT__MODEL_FORMAT_MODE_H - -#include - -namespace CVC4 { - -/** Enumeration of model_format modes (how to print models from get-model command). */ -typedef enum { - /** default mode (print expressions in the output language format) */ - MODEL_FORMAT_MODE_DEFAULT, - /** print functional values in a table format */ - MODEL_FORMAT_MODE_TABLE, -} ModelFormatMode; - -std::ostream& operator<<(std::ostream& out, ModelFormatMode mode) CVC4_PUBLIC; - -}/* CVC4 namespace */ - -#endif /* __CVC4__SMT__MODEL_FORMAT_H */ 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