summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/main/driver_unified.cpp5
-rwxr-xr-xsrc/options/mkoptions31
-rw-r--r--src/printer/Makefile.am5
-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/options3
-rw-r--r--src/printer/options_handlers.h56
-rw-r--r--src/prop/theory_proxy.cpp3
-rw-r--r--src/prop/theory_proxy.h6
-rw-r--r--src/smt/Makefile.am4
-rw-r--r--src/smt/options19
-rw-r--r--src/smt/options_handlers.h24
-rw-r--r--src/theory/arith/options3
-rw-r--r--src/theory/datatypes/options2
-rw-r--r--src/theory/model.cpp1
-rw-r--r--src/theory/options3
-rw-r--r--src/theory/uf/options3
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback