summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/expr/expr_manager_template.cpp4
-rw-r--r--src/expr/expr_manager_template.h11
-rw-r--r--src/include/cvc4_private.h4
-rw-r--r--src/lib/replacements.h4
-rwxr-xr-xsrc/options/mkoptions256
-rw-r--r--src/smt/options3
-rw-r--r--src/util/exception.h4
-rw-r--r--src/util/statistics_registry.cpp13
8 files changed, 154 insertions, 145 deletions
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 516930bcd..be2804fd5 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -126,6 +126,10 @@ ExprManager::~ExprManager() throw() {
}
}
+StatisticsRegistry* ExprManager::getStatisticsRegistry() throw() {
+ return d_nodeManager->getStatisticsRegistry();
+}
+
const Options& ExprManager::getOptions() const {
return d_nodeManager->getOptions();
}
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 460e3f1dc..d883cd725 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -46,6 +46,7 @@ class NodeManager;
class Options;
class IntStat;
class ExprManagerMapCollection;
+class StatisticsRegistry;
namespace expr {
namespace pickle {
@@ -57,6 +58,10 @@ namespace context {
class Context;
}/* CVC4::context namespace */
+namespace stats {
+ StatisticsRegistry* getStatisticsRegistry(ExprManager*);
+}/* CVC4::stats namespace */
+
class CVC4_PUBLIC ExprManager {
private:
/** The context */
@@ -98,6 +103,12 @@ private:
/** NodeManager reaches in to get the NodeManager */
friend class NodeManager;
+ /** Statistics reach in to get the StatisticsRegistry */
+ friend ::CVC4::StatisticsRegistry* ::CVC4::stats::getStatisticsRegistry(ExprManager*);
+
+ /** Get the underlying statistics registry. */
+ StatisticsRegistry* getStatisticsRegistry() throw();
+
// undefined, private copy constructor and assignment op (disallow copy)
ExprManager(const ExprManager&) CVC4_UNDEFINED;
ExprManager& operator=(const ExprManager&) CVC4_UNDEFINED;
diff --git a/src/include/cvc4_private.h b/src/include/cvc4_private.h
index c97398e1e..e41a13979 100644
--- a/src/include/cvc4_private.h
+++ b/src/include/cvc4_private.h
@@ -25,6 +25,10 @@
# warning A private CVC4 header was included when not building the library or private unit test code.
#endif /* ! (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST) */
+#ifdef __BUILDING_STATISTICS_FOR_EXPORT
+# warning A private CVC4 header was included when building a library for export.
+#endif /* __BUILDING_STATISTICS_FOR_EXPORT */
+
#include "cvc4_public.h"
#include "cvc4autoconfig.h"
diff --git a/src/lib/replacements.h b/src/lib/replacements.h
index ee2ffc2dd..7be06818b 100644
--- a/src/lib/replacements.h
+++ b/src/lib/replacements.h
@@ -19,13 +19,13 @@
#ifndef __CVC4__LIB__REPLACEMENTS_H
#define __CVC4__LIB__REPLACEMENTS_H
-#if defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST)
+#if (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST)) && !defined(__BUILDING_STATISTICS_FOR_EXPORT)
# include "cvc4_private.h"
#else
# if defined(__BUILDING_CVC4PARSERLIB) || defined(__BUILDING_CVC4PARSERLIB_UNIT_TEST)
# include "cvc4parser_private.h"
# else
-# if defined(__BUILDING_CVC4DRIVER) || defined(__BUILDING_CVC4_SYSTEM_TEST)
+# if defined(__BUILDING_CVC4DRIVER) || defined(__BUILDING_CVC4_SYSTEM_TEST) || defined(__BUILDING_STATISTICS_FOR_EXPORT)
# include "cvc4autoconfig.h"
# else
# error Must be building libcvc4 or libcvc4parser to use replacement functions. This is because replacement function headers should never be publicly-depended upon, as they should not be installed on user machines with 'make install'.
diff --git a/src/options/mkoptions b/src/options/mkoptions
index 8e098cb95..79ef35f5b 100755
--- a/src/options/mkoptions
+++ b/src/options/mkoptions
@@ -28,6 +28,19 @@ function progress {
progress_char="`echo "$progress_char" | tr -- '-\\\\|/' '\\\\|/-'`"
}
+function NOTE {
+ printf "\r%-80s\n" "$kf:$lineno: note: $@"
+}
+
+function WARN {
+ printf "\r%-80s\n" "$kf:$lineno: warning: $@"
+}
+
+function ERR {
+ printf "\r%-80s\n" "$kf:$lineno: error: $@"
+ exit 1
+}
+
declare -a templates
declare -a outputs
@@ -115,9 +128,7 @@ function module {
seen_module=true
if [ $# -lt 3 -o -z "$1" -o -z "$2" -o -z "$3" ]; then
- echo >&2
- echo "$kf:$lineno: error: \"module\" directive requires exactly three arguments" >&2
- exit 1
+ ERR "\"module\" directive requires exactly three arguments"
fi
module_id="$1"; shift
@@ -152,9 +163,7 @@ function endmodule {
check_doc
seen_endmodule=true
if [ $# -ne 0 ]; then
- echo >&2
- echo "$kf:$lineno: error: endmodule takes no arguments" >&2
- exit 1
+ ERR "endmodule takes no arguments"
fi
}
@@ -233,16 +242,12 @@ function handle_option {
while [ $i -lt $type_pos ]; do
if expr "${args[$i]}" : '--' &>/dev/null || expr "${args[$i]}" : '/--' &>/dev/null; then
if [ -n "$long_option" -o -n "$long_option_alternate" ]; then
- echo >&2
- echo "$kf:$lineno: error: malformed option line for \`$internal': unexpected \`${args[$i]}'" >&2
- exit 1
+ ERR "malformed option line for \`$internal': unexpected \`${args[$i]}'"
fi
long_option="$(echo "${args[$i]}" | sed 's,/.*,,')"
if [ -n "$long_option" ]; then
if ! expr "$long_option" : '--.' &>/dev/null; then
- echo >&2
- echo "$kf:$option: bad long option \`$long_option': expected something like \`--foo'" >&2
- exit 1
+ ERR "bad long option \`$long_option': expected something like \`--foo'"
fi
long_option="$(echo "$long_option" | sed 's,^--,,')"
fi
@@ -251,25 +256,19 @@ function handle_option {
long_option_alternate_set=set
if [ -n "$long_option_alternate" ]; then
if ! expr "$long_option_alternate" : '--.' &>/dev/null; then
- echo >&2
- echo "$kf:$option: bad alternate long option \`$long_option_alternate': expected something like \`--foo'" >&2
- exit 1
+ ERR "bad alternate long option \`$long_option_alternate': expected something like \`--foo'"
fi
long_option_alternate="$(echo "$long_option_alternate" | sed 's,^--,,')"
fi
fi
elif expr "${args[$i]}" : '-' &>/dev/null || expr "${args[$i]}" : '/-' &>/dev/null; then
if [ -n "$short_option" -o -n "$short_option_alternate" -o -n "$long_option" -o -n "$long_option_alternate" ]; then
- echo >&2
- echo "$kf:$lineno: error: malformed option line for \`$internal': unexpected \`${args[$i]}'" >&2
- exit 1
+ ERR "malformed option line for \`$internal': unexpected \`${args[$i]}'"
fi
short_option="$(echo "${args[$i]}" | sed 's,/.*,,')"
if [ -n "$short_option" ]; then
if ! expr "$short_option" : '-.$' &>/dev/null; then
- echo >&2
- echo "$kf:$option: bad short option \`$short_option': expected something like \`-x'" >&2
- exit 1
+ ERR "bad short option \`$short_option': expected something like \`-x'"
fi
short_option="$(echo "$short_option" | sed 's,^-,,')"
fi
@@ -277,18 +276,14 @@ function handle_option {
short_option_alternate="$(echo "${args[$i]}" | sed 's,[^/]*/,,')"
if expr "$short_option_alternate" : - &>/dev/null; then
if ! expr "$short_option_alternate" : '-.$' &>/dev/null; then
- echo >&2
- echo "$kf:$option: bad alternate short option \`$short_option_alternate': expected something like \`-x'" >&2
- exit 1
+ ERR "bad alternate short option \`$short_option_alternate': expected something like \`-x'"
fi
short_option_alternate="$(echo "$short_option_alternate" | sed 's,^-,,')"
fi
fi
else
if [ -n "$smtname" -o -n "$short_option" -o -n "$short_option_alternate" -o -n "$long_option" -o -n "$long_option_alternate" ]; then
- echo >&2
- echo "$kf:$lineno: error: malformed option line for \`$internal': unexpected \`${args[$i]}'" >&2
- exit 1
+ ERR "malformed option line for \`$internal': unexpected \`${args[$i]}'"
fi
smtname="${args[$i]}"
fi
@@ -297,13 +292,9 @@ function handle_option {
fi
if [ "$type" = void -a "$internal" != - ]; then
- echo >&2
- echo "$kf:$lineno: error: $internal cannot be void-typed; use \`-' as the name if its to be void" >&2
- exit 1
+ ERR "$internal cannot be void-typed; use \`-' as the name if its to be void"
elif [ "$type" != void -a "$internal" = - ]; then
- echo >&2
- echo "$kf:$lineno: error: cannot use an unnamed option if its type is not void" >&2
- exit 1
+ ERR "cannot use an unnamed option if its type is not void"
fi
if [ "$type" = bool -a -n "$long_option$short_option" -a "$category" != UNDOCUMENTED ]; then
@@ -315,61 +306,45 @@ function handle_option {
long_option_alternate="no-$(echo "$long_option" | sed 's,^--,,')"
fi
if [ "$type" != bool -a -n "$short_option_alternate" ]; then
- echo >&2
- echo "$kf:$lineno: error: cannot use alternate short option -$short_option_alternate for \`$internal' because it's not of bool type" >&2
- exit 1
+ ERR "cannot use alternate short option -$short_option_alternate for \`$internal' because it's not of bool type"
elif [ "$type" != bool -a -n "$long_option_alternate" ]; then
- echo >&2
- echo "$kf:$lineno: error: cannot use alternate long option --$long_option_alternate for \`$internal' because it's not of bool type" >&2
- exit 1
+ ERR "cannot use alternate long option --$long_option_alternate for \`$internal' because it's not of bool type"
fi
# check for duplicates
if [ "$internal" != - ]; then
if echo " $all_declared_internal_options " | grep -q " $internal "; then
- echo >&2
- echo "$kf:$lineno: error: internal option name \`$internal' previously declared" >&2
- exit 1
+ ERR "internal option name \`$internal' previously declared"
fi
all_declared_internal_options="$all_declared_internal_options $internal"
fi
if [ -n "$long_option" ]; then
if echo " $all_declared_long_options " | grep -q " $long_option "; then
- echo >&2
- echo "$kf:$lineno: error: long option name \`--$long_option' previously declared" >&2
- exit 1
+ ERR "long option name \`--$long_option' previously declared"
fi
all_declared_long_options="$all_declared_long_options $long_option"
fi
if [ -n "$long_option_alternate" ]; then
if echo " $all_declared_long_options " | grep -q " $long_option_alternate "; then
- echo >&2
- echo "$kf:$lineno: error: long option name \`--$long_option_alternate' previously declared" >&2
- exit 1
+ ERR "long option name \`--$long_option_alternate' previously declared"
fi
all_declared_long_options="$all_declared_long_options $long_option_alternate"
fi
if [ -n "$short_option" ]; then
if echo " $all_declared_short_options " | grep -q " $short_option "; then
- echo >&2
- echo "$kf:$lineno: error: short option name \`-$short_option' previously declared" >&2
- exit 1
+ ERR "short option name \`-$short_option' previously declared"
fi
all_declared_short_options="$all_declared_short_options $short_option"
fi
if [ -n "$short_option_alternate" ]; then
if echo " $all_declared_short_options " | grep -q " $short_option_alternate "; then
- echo >&2
- echo "$kf:$lineno: error: short option name \`-$short_option_alternate' previously declared" >&2
- exit 1
+ ERR "short option name \`-$short_option_alternate' previously declared"
fi
all_declared_short_options="$all_declared_short_options $short_option_alternate"
fi
if [ -n "$smtname" ]; then
if echo " $all_declared_smt_options " | grep -q " $smtname "; then
- echo >&2
- echo "$kf:$lineno: error: SMT option name \`$smtname' previously declared" >&2
- exit 1
+ ERR "SMT option name \`$smtname' previously declared"
fi
all_declared_smt_options="$all_declared_smt_options $smtname"
fi
@@ -386,9 +361,7 @@ function handle_option {
:handler)
let ++i
if [ -n "$handlers" ]; then
- echo >&2
- echo "$kf:$lineno: error: cannot specify more than one handler; maybe you want a :handler and a :predicate" >&2
- exit 1
+ ERR "cannot specify more than one handler; maybe you want a :handler and a :predicate"
fi
handlers="${args[$i]}"
;;
@@ -434,9 +407,7 @@ function handle_option {
readOnly=true
;;
*)
- echo >&2
- echo "$kf:$lineno: error in option \`$internal': bad attribute \`$attribute'" >&2
- exit 1
+ ERR "error in option \`$internal': bad attribute \`$attribute'"
esac
let ++i
done
@@ -558,9 +529,7 @@ template <> bool Options::wasSetByUser(options::${internal}__option_t) const { r
if [ "$type" = bool ] && [ -n "$cases" -o -n "$cases_alternate" -o -n "$smtname" ]; then
run_handlers=
if [ -n "$handlers" ]; then
- echo >&2
- echo "$kf:$lineno: error: bool-valued options cannot have handlers" >&2
- exit 1
+ ERR "bool-valued options cannot have handlers"
fi
if [ -n "$predicates" ]; then
for predicate in $predicates; do
@@ -620,9 +589,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
elif [ -n "$expect_arg" ]; then
run_handlers=
if [ -n "$predicates" ]; then
- echo >&2
- echo "$kf:$lineno: error: void-valued options cannot have predicates" >&2
- exit 1
+ ERR "void-valued options cannot have predicates"
fi
if [ -n "$handlers" ]; then
for handler in $handlers; do
@@ -639,9 +606,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
else
run_handlers=
if [ -n "$predicates" ]; then
- echo >&2
- echo "$kf:$lineno: error: void-valued options cannot have predicates" >&2
- exit 1
+ ERR "void-valued options cannot have predicates"
fi
if [ -n "$handlers" ]; then
for handler in $handlers; do
@@ -665,9 +630,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
break;
"
else
- echo >&2
- echo "$kf:$lineno: internal error: expected BOOL-typed option in alternate handler" >&2
- exit 1
+ ERR "internal error: expected BOOL-typed option in alternate handler"
fi
fi
@@ -823,33 +786,23 @@ function handle_alias {
expect_doc_alternate=false
if [ $# -lt 3 ]; then
- echo >&2
- echo "$kf:$lineno: error: malformed \"alias\" command; expected more arguments" >&2
- exit 1
+ ERR "malformed \"alias\" command; expected more arguments"
fi
if [ "$1" = '=' ]; then
- echo >&2
- echo "$kf:$lineno: error: malformed \"alias\" command; expected option name" >&2
- exit 1
+ ERR "malformed \"alias\" command; expected option name"
fi
option="$1"
shift
if [ "$1" != '=' ]; then
- echo >&2
- echo "$kf:$lineno: error: malformed \"alias\" command; expected \`='" >&2
- exit 1
+ ERR "malformed \"alias\" command; expected \`='"
fi
shift
if [ $# -eq 0 ]; then
- echo >&2
- echo "$kf:$lineno: error: malformed \"alias\" command; expected more arguments" >&2
- exit 1
+ ERR "malformed \"alias\" command; expected more arguments"
fi
cases=
if ! expr "$option" : - &>/dev/null; then
- echo >&2
- echo "$kf:$lineno: error: alias for SMT options not yet supported" >&2
- exit 1
+ ERR "alias for SMT options not yet supported"
fi
if expr "$option" : -- &>/dev/null; then
if expr "$option" : '.*=' &>/dev/null; then
@@ -870,9 +823,7 @@ function handle_alias {
else
if ! expr "$option" : '-.$' &>/dev/null; then
if ! expr "$option" : '-.=' &>/dev/null; then
- echo >&2
- echo "$kf:$lineno: error: expected short option specification, got \`$option'" >&2
- exit 1
+ ERR "expected short option specification, got \`$option'"
fi
expect_arg=:
arg="$(echo "$option" | sed 's,[^=]*=,,')"
@@ -923,8 +874,7 @@ function warning {
check_module_seen
check_doc
- echo >&2
- echo "$kf:$lineno: warning: $@" >&2
+ WARN "$*"
}
function doc {
@@ -938,6 +888,53 @@ function doc {
if [ -n "$smtname" ]; then
expect_doc_alternate=true
else
+ if [ "$internal" != - ]; then
+ if ! $alternate_options_already_documented; then
+ if [ "$short_option_alternate" ]; then
+ if [ "$long_option_alternate" ]; then
+ altopt="s -$short_option_alternate and --$long_option_alternate, each of"
+ else
+ altopt=" -$short_option_alternate,"
+ fi
+ else
+ altopt=" --$long_option_alternate,"
+ fi
+ if [ -z "$default_value" ]; then
+ typedefault="($type)"
+ else
+ typedefault="($type, default = $default_value)"
+ fi
+ mansmtdoc="$@"
+ if [ "$category" = EXPERT ]; then
+ mansmtdoc="$mansmtdoc (EXPERTS only)"
+ fi
+ if [ "$category" = COMMON ]; then
+ common_manpage_internals_documentation="${common_manpage_internals_documentation}
+.TP
+.B \"$internal\"
+$typedefault
+.br
+.B \"This internal Boolean flag is undocumented; however, its alternate option$altopt which reverses the sense of the option, is documented thusly:\"
+$mansmtdoc"
+ else
+ remaining_manpage_internals_documentation="${remaining_manpage_internals_documentation}
+.TP
+.B \"$internal\"
+$typedefault
+.br
+.B \"This internal Boolean flag is undocumented; however, its alternate option$altopt which reverses the sense of the option, is documented thusly:\"
+$mansmtdoc"
+ fi
+ else
+ if [ "$category" = COMMON ]; then
+ common_manpage_internals_documentation="${common_manpage_internals_documentation}
+$@"
+ else
+ remaining_manpage_internals_documentation="${remaining_manpage_internals_documentation}
+$@"
+ fi
+ fi
+ fi
doc-alternate "$@"
return
fi
@@ -1084,15 +1081,11 @@ function doc-alternate {
expect_doc_alternate=false
if $expect_doc; then
- echo >&2
- echo "$kf:$lineno: error: must provide documentation before alternate documentation" >&2
- exit 1
+ ERR "must provide documentation before alternate documentation"
fi
if [ -z "$short_option_alternate" -a -z "$long_option_alternate" ]; then
- echo >&2
- echo "$kf:$lineno: cannot document an alternative for option \`$internal'; one does not exist" >&2
- exit 1
+ ERR "cannot document an alternative for option \`$internal'; one does not exist"
fi
if [ "$category" = UNDOCUMENTED ]; then
@@ -1170,17 +1163,13 @@ $@"
function check_doc {
if $expect_doc; then
if [ "$internal" != - ]; then
- echo >&2
- echo "$kf:$lineno: warning: $internal is lacking documentation" >&2
+ WARN "$internal is lacking documentation"
elif [ -n "$long_option" ]; then
- echo >&2
- echo "$kf:$lineno: warning: option --$long_option is lacking documentation" >&2
+ WARN "option --$long_option is lacking documentation"
elif [ -n "$short_option" ]; then
- echo >&2
- echo "$kf:$lineno: warning: option -$short_option is lacking documentation" >&2
+ WARN "option -$short_option is lacking documentation"
elif [ -n "$smtname" ]; then
- echo >&2
- echo "$kf:$lineno: warning: SMT option $smtname is lacking documentation" >&2
+ WARN "SMT option $smtname is lacking documentation"
fi
expect_doc=false
elif ! $seen_doc; then
@@ -1209,22 +1198,17 @@ $typedefault
fi
if $expect_doc_alternate; then
- echo >&2
- echo "$kf:$lineno: warning: $internal is lacking documentation for the alternative option(s): $short_option_alternate $long_option_alternate" >&2
+ WARN "$internal is lacking documentation for the alternative option(s): $short_option_alternate $long_option_alternate"
expect_doc_alternate=false
fi
}
function check_module_seen {
if $seen_endmodule; then
- echo >&2
- echo "$kf:$lineno: error: command after \"endmodule\" declaration (endmodule has to be last)" >&2
- exit 1
+ ERR "command after \"endmodule\" declaration (endmodule has to be last)"
fi
if ! $seen_module; then
- echo >&2
- echo "$kf:$lineno: error: no \"module\" declaration found (it has to be first)" >&2
- exit 1
+ ERR "no \"module\" declaration found (it has to be first)"
fi
}
@@ -1280,10 +1264,11 @@ function output_module {
error="$(grep '.*\${[^}]*}.*' "$output.working" | head -n 1)"
if [ -n "$error" ]; then
error="$(echo "$error" | sed 's,.*\${\([^}]*\)}.*,\1,')"
- echo "$template:0: error: undefined replacement \${$error}" >&2
rm -f "$output.working"
rm -f "$output.sed"
- exit 1
+ kf="$template"
+ lineno=0
+ ERR "undefined replacement \${$error}"
fi
(
@@ -1372,29 +1357,22 @@ while [ $# -gt 0 ]; do
elif expr "$line" : '\.[ ]*$' &>/dev/null; then
doc ""
elif expr "$line" : '\.' &>/dev/null; then
- echo >&2
- echo "$kf:$lineno: error: malformed line during processing of option \`$internal': continuation lines should not have content" >&2
- exit 1
+ ERR "malformed line during processing of option \`$internal': continuation lines should not have content"
elif expr "$line" : '/.*' &>/dev/null; then
doc-alternate "$(echo "$line" | sed 's,^/,,')"
else
line="$(echo "$line" | sed 's,\([<>&()!?*]\),\\\1,g')"
+ progress "$kf" $count $total
if ! eval "$line"; then
- echo >&2
- echo "$kf:$lineno: error was due to evaluation of this line" >&2
- exit 1
+ ERR "error was due to evaluation of this line"
fi
fi
done < "$kf"
if ! $seen_module; then
- echo >&2
- echo "$kf: error: no module content found in file!" >&2
- exit 1
+ ERR "no module content found in file!"
fi
if ! $seen_endmodule; then
- echo >&2
- echo "$kf:$lineno: error: no \"endmodule\" declaration found (it is required at the end)" >&2
- exit 1
+ ERR "no \"endmodule\" declaration found (it is required at the end)"
fi
output_module "$options_h_template" "$outdir/$(basename "$kf").h"
@@ -1403,11 +1381,14 @@ done
## final outputs
+regenerated=false
i=0; while [ $i -lt ${#templates[@]} ]; do
template="${templates[$i]}"
output="${outputs[$i]}"
+progress "$output" $count $total
+
let ++i
filename="$(basename "$output")"
@@ -1518,10 +1499,17 @@ cat "$output.working"
rm -f "$output.working"
rm -f "$output.sed"
-diff -q "$output" "$output.tmp" &>/dev/null || (mv -f "$output.tmp" "$output" && printf "\rregenerated %-68s\n" "$output")
+if diff -q "$output" "$output.tmp" &>/dev/null; then
+ regenerated=false
+else
+ mv -f "$output.tmp" "$output"
+ printf "\rregenerated %-68s\n" "$output"
+ regenerated=true
+fi
rm -f "$output.tmp"
-progress "$output" $count $total
done
-echo
+if ! $regenerated; then
+ printf "\r%-80s\r" ""
+fi
diff --git a/src/smt/options b/src/smt/options
index f82867b68..24c8b5e43 100644
--- a/src/smt/options
+++ b/src/smt/options
@@ -81,7 +81,4 @@ option lemmaInputChannel LemmaInputChannel* :default NULL :include "util/lemma_i
option lemmaOutputChannel LemmaOutputChannel* :default NULL :include "util/lemma_output_channel.h"
The output channel to receive notfication events for new lemmas
-option optionWithOnlyAlternate /--optionWithOnlyAlternate bool
- option with only an alternate
-
endmodule
diff --git a/src/util/exception.h b/src/util/exception.h
index 89e42b6d1..4241fb1f1 100644
--- a/src/util/exception.h
+++ b/src/util/exception.h
@@ -130,9 +130,9 @@ inline std::ostream& operator<<(std::ostream& os, const Exception& e) throw() {
}/* CVC4 namespace */
-#if defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST)
+#if (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST)) && !defined(__BUILDING_STATISTICS_FOR_EXPORT)
# include "util/Assert.h"
-#endif /* __BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST */
+#endif /* (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST) && !__BUILDING_STATISTICS_FOR_EXPORT */
namespace CVC4 {
diff --git a/src/util/statistics_registry.cpp b/src/util/statistics_registry.cpp
index 48e1355ec..6194145a8 100644
--- a/src/util/statistics_registry.cpp
+++ b/src/util/statistics_registry.cpp
@@ -18,13 +18,14 @@
**/
#include "util/statistics_registry.h"
-#include "expr/node_manager.h"
-#include "expr/expr_manager_scope.h"
#include "expr/expr_manager.h"
#include "lib/clock_gettime.h"
-#include "smt/smt_engine_scope.h"
#include "smt/smt_engine.h"
+#ifndef __BUILDING_STATISTICS_FOR_EXPORT
+# include "smt/smt_engine_scope.h"
+#endif /* ! __BUILDING_STATISTICS_FOR_EXPORT */
+
#ifdef CVC4_STATISTICS_ON
# define __CVC4_USE_STATISTICS true
#else
@@ -42,6 +43,10 @@ inline StatisticsRegistry* getStatisticsRegistry(SmtEngine* smt) {
return smt->d_statisticsRegistry;
}
+inline StatisticsRegistry* getStatisticsRegistry(ExprManager* em) {
+ return em->getStatisticsRegistry();
+}
+
}/* CVC4::stats namespace */
#ifndef __BUILDING_STATISTICS_FOR_EXPORT
@@ -117,7 +122,7 @@ void TimerStat::stop() {
}/* TimerStat::stop() */
RegisterStatistic::RegisterStatistic(ExprManager& em, Stat* stat) :
- d_reg(NodeManager::fromExprManager(&em)->getStatisticsRegistry()),
+ d_reg(stats::getStatisticsRegistry(&em)),
d_stat(stat) {
d_reg->registerStat_(d_stat);
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback