From c0dcc5ff59473a45864f818cfdda037c0ee4ea12 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Sun, 8 Jul 2012 17:36:50 +0000 Subject: Bugs resolved by this commit: #314, #322, #359, #364, #365. See below for details. * Fix the "assert" name-collision bug (resolves bug #364). Our identifiers should never be named "assert", as that's a preprocessor definition in , which is often #included indirectly (so simply having a policy of not including isn't good enough---one of our dependences might include it). It was once the case that we didn't have anything named "assert", but "assert()" has now crept back in. Instead, name things "assertFoo()" or similar. Thanks to Tim for the report. To fix this, I've changed some of Dejan's circuit-propagator code from "assert()" to "assertTrue()". Ditto for Andy's explanation manager. Guys, if you prefer a different name in your code, please change it. * Fix the incorrect parsing of lets in SMT-LIBv2 parser (resolves bug #365). Inner lets now shadow outer lets (previously, they incorrectly gave an error). Additionally, while looking at this, I found that a sequential let was implemented rather than a parallel let. This is now fixed. Thanks to Liana for the report. * Remove ANTLR parser generation warnings in CVC parser (resolves bug #314). * There were a lot of Debug lines in bitvectors that had embedded toString() calls. This wasted a LOT of time in debug builds for BV benchmarks (like in "make regress"). Added if(Debug.isOn(...)) guards; much faster now. * Support for building public-facing interface documentation only (as opposed to all internals documentation). Now "make doc" does the public-facing and "make doc-internals" does documentation of everything. (Along with changes to the nightly build script---which will now build and publish both types of Doxygen documentation---this resolves bug #359). * Fix the lambda typechecking bug (resolves bug #322). Thanks to Andy for the report (a long long time ago--sorry). * The default output language for all streams is now based on the current set of Options (if there is one). This has been a constant annoyance, especially when stringstreams are used to construct output. However, it doesn't work for calls from outside the library, so it's mainly an annoyance-fixer for CVC4 library code itself. * Add some CVC4_UNUSED markers to local variables in theory_arith.cpp that are used only in assertions-enabled builds (and thus give warnings in production builds). This was briefly discussed at the meeting this week. --- src/util/hash.h | 1 + src/util/options.cpp | 2 ++ src/util/options.h | 7 +++++-- 3 files changed, 8 insertions(+), 2 deletions(-) (limited to 'src/util') diff --git a/src/util/hash.h b/src/util/hash.h index fdfbf4087..6fb20dab0 100644 --- a/src/util/hash.h +++ b/src/util/hash.h @@ -26,6 +26,7 @@ namespace __gnu_cxx {} #include +#include namespace __gnu_cxx { diff --git a/src/util/options.cpp b/src/util/options.cpp index a10aae83d..2352ae503 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -87,6 +87,7 @@ Options::Options() : strictParsing(false), lazyDefinitionExpansion(false), printWinner(false), + defaultExprDepth(0), simplificationMode(SIMPLIFICATION_MODE_BATCH), simplificationModeSetByUser(false), decisionMode(DECISION_STRATEGY_INTERNAL), @@ -951,6 +952,7 @@ throw(OptionException) { Chat.getStream() << Expr::setdepth(depth); Message.getStream() << Expr::setdepth(depth); Warning.getStream() << Expr::setdepth(depth); + defaultExprDepth = depth; } break; diff --git a/src/util/options.h b/src/util/options.h index f3ae3b64e..f423260b0 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -27,8 +27,6 @@ #include "util/exception.h" #include "util/language.h" -#include "util/lemma_output_channel.h" -#include "util/lemma_input_channel.h" #include "util/tls.h" #include "theory/theoryof_mode.h" @@ -37,6 +35,8 @@ namespace CVC4 { class ExprStream; +class LemmaInputChannel; +class LemmaOutputChannel; /** Class representing an option-parsing exception. */ class CVC4_PUBLIC OptionException : public CVC4::Exception { @@ -112,6 +112,9 @@ struct CVC4_PUBLIC Options { /** Parallel Only: Whether the winner is printed at the end or not. */ bool printWinner; + /** The default expression depth to print on ostreams. */ + int defaultExprDepth; + /** Enumeration of simplification modes (when to simplify). */ typedef enum { /** Simplify the assertions as they come in */ -- cgit v1.2.3