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
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.
-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
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
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)])
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
[], [$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
#
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
$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 ||
./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
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
.\" 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
.\" 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
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);
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 {
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 {
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 \
cvc/cvc_printer.h \
cvc/cvc_printer.cpp
-EXTRA_DIST =
+EXTRA_DIST = \
+ options_handlers.h
--- /dev/null
+/********************* */
+/*! \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 */
--- /dev/null
+/********************* */
+/*! \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 <iostream>
+
+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 */
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
--- /dev/null
+/********************* */
+/*! \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 */
#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 {
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;
}
*/
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,
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
+++ /dev/null
-/********************* */
-/*! \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 */
+++ /dev/null
-/********************* */
-/*! \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 <iostream>
-
-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 */
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
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.
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
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*
+ 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());
}
}
-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) {
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.
# 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
#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"
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
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
projects / cvc5.git / commitdiff