diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-10-06 18:53:27 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-10-06 18:53:27 +0000 |
commit | 4e883ffc0b88256a966183ac6b87bb5767154cdf (patch) | |
tree | a193f12035e4417834ef08312f50739ae0b39a87 /src | |
parent | 99cad5495be99efae434177d1537d4cfac35581c (diff) |
* 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.)
Diffstat (limited to 'src')
-rw-r--r-- | src/main/driver_unified.cpp | 5 | ||||
-rwxr-xr-x | src/options/mkoptions | 31 | ||||
-rw-r--r-- | src/printer/Makefile.am | 5 | ||||
-rw-r--r-- | src/printer/model_format_mode.cpp (renamed from src/smt/model_format_mode.cpp) | 2 | ||||
-rw-r--r-- | src/printer/model_format_mode.h (renamed from src/smt/model_format_mode.h) | 6 | ||||
-rw-r--r-- | src/printer/options | 3 | ||||
-rw-r--r-- | src/printer/options_handlers.h | 56 | ||||
-rw-r--r-- | src/prop/theory_proxy.cpp | 3 | ||||
-rw-r--r-- | src/prop/theory_proxy.h | 6 | ||||
-rw-r--r-- | src/smt/Makefile.am | 4 | ||||
-rw-r--r-- | src/smt/options | 19 | ||||
-rw-r--r-- | src/smt/options_handlers.h | 24 | ||||
-rw-r--r-- | src/theory/arith/options | 3 | ||||
-rw-r--r-- | src/theory/datatypes/options | 2 | ||||
-rw-r--r-- | src/theory/model.cpp | 1 | ||||
-rw-r--r-- | src/theory/options | 3 | ||||
-rw-r--r-- | src/theory/uf/options | 3 |
17 files changed, 121 insertions, 55 deletions
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 |