diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-05-05 22:23:50 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-05-05 22:23:50 +0000 |
commit | fef0f8190fc7e5f3b88b33e7574b7df1e629e80f (patch) | |
tree | dfdda739bf5008096860e19f6b9275fb2a257960 /src/util | |
parent | 90d8205a86b698c2548108ca4db124fe9c3f738a (diff) |
Merge from nonclausal-simplification-v2 branch:
* Preprocessing-time, non-clausal, Boolean simplification round to
support "quasi-non-linear rewrites" as discussed at last few meetings.
* --simplification=none is the default for now, but we'll probably
change that to --simplification=incremental. --simplification=batch
is also a possibility. See --simplification=help for details.
* RecursionBreaker<T> now uses a hash set for the seen trail.
* Fixes to TLS stuff to support that.
* Fixes to theory and SmtEngine documentation.
* Fixes to stream indentation.
* Other miscellaneous stuff.
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/Makefile.am | 2 | ||||
-rw-r--r-- | src/util/boolean_simplification.cpp | 33 | ||||
-rw-r--r-- | src/util/boolean_simplification.h | 50 | ||||
-rw-r--r-- | src/util/cache.h | 129 | ||||
-rw-r--r-- | src/util/datatype.cpp | 8 | ||||
-rw-r--r-- | src/util/datatype.h | 18 | ||||
-rw-r--r-- | src/util/options.cpp | 85 | ||||
-rw-r--r-- | src/util/options.h | 47 | ||||
-rw-r--r-- | src/util/output.cpp | 3 | ||||
-rw-r--r-- | src/util/output.h | 73 | ||||
-rw-r--r-- | src/util/recursion_breaker.h | 12 | ||||
-rw-r--r-- | src/util/tls.h.in | 55 | ||||
-rw-r--r-- | src/util/utility.h | 75 |
13 files changed, 538 insertions, 52 deletions
diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 27b9e42d2..20806464d 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -51,6 +51,8 @@ libutil_la_SOURCES = \ subrange_bound.h \ cardinality.h \ cardinality.cpp \ + cache.h \ + utility.h \ trans_closure.h \ trans_closure.cpp \ boolean_simplification.h \ diff --git a/src/util/boolean_simplification.cpp b/src/util/boolean_simplification.cpp index a154f342f..92534bfd4 100644 --- a/src/util/boolean_simplification.cpp +++ b/src/util/boolean_simplification.cpp @@ -20,7 +20,7 @@ namespace CVC4 { -void +bool BooleanSimplification::push_back_associative_commute_recursive (Node n, std::vector<Node>& buffer, Kind k, Kind notK, bool negateNode) throw(AssertionException) { @@ -28,17 +28,40 @@ BooleanSimplification::push_back_associative_commute_recursive for(; i != end; ++i){ Node child = *i; if(child.getKind() == k){ - push_back_associative_commute_recursive(child, buffer, k, notK, negateNode); + if(! push_back_associative_commute_recursive(child, buffer, k, notK, negateNode)) { + return false; + } }else if(child.getKind() == kind::NOT && child[0].getKind() == notK){ - push_back_associative_commute_recursive(child, buffer, notK, k, !negateNode); + if(! push_back_associative_commute_recursive(child[0], buffer, notK, k, !negateNode)) { + return false; + } }else{ if(negateNode){ - buffer.push_back(negate(child)); + if(child.getMetaKind() == kind::metakind::CONSTANT) { + if((k == kind::AND && child.getConst<bool>()) || + (k == kind::OR && !child.getConst<bool>())) { + buffer.clear(); + buffer.push_back(negate(child)); + return false; + } + } else { + buffer.push_back(negate(child)); + } }else{ - buffer.push_back(child); + if(child.getMetaKind() == kind::metakind::CONSTANT) { + if((k == kind::OR && child.getConst<bool>()) || + (k == kind::AND && !child.getConst<bool>())) { + buffer.clear(); + buffer.push_back(child); + return false; + } + } else { + buffer.push_back(child); + } } } } + return true; }/* BooleanSimplification::push_back_associative_commute_recursive() */ }/* CVC4 namespace */ diff --git a/src/util/boolean_simplification.h b/src/util/boolean_simplification.h index e938a2b38..c2da8af5b 100644 --- a/src/util/boolean_simplification.h +++ b/src/util/boolean_simplification.h @@ -39,9 +39,9 @@ class BooleanSimplification { BooleanSimplification() CVC4_UNUSED; BooleanSimplification(const BooleanSimplification&) CVC4_UNUSED; - static void push_back_associative_commute_recursive + static bool push_back_associative_commute_recursive (Node n, std::vector<Node>& buffer, Kind k, Kind notK, bool negateNode) - throw(AssertionException); + throw(AssertionException) CVC4_WARN_UNUSED_RESULT; public: @@ -80,6 +80,10 @@ public: removeDuplicates(buffer); + if(buffer.size() == 1) { + return buffer[0]; + } + NodeBuilder<> nb(kind::AND); nb.append(buffer); return nb; @@ -100,6 +104,11 @@ public: removeDuplicates(buffer); + Assert(buffer.size() > 0); + if(buffer.size() == 1) { + return buffer[0]; + } + NodeBuilder<> nb(kind::OR); nb.append(buffer); return nb; @@ -138,10 +147,14 @@ public: * @param k the kind to collapse (should equal the kind of node n) * @param notK the "negation" of kind k (e.g. OR's negation is AND), * or kind::UNDEFINED_KIND if none. + * @param negateChildren true if the children of the resulting node + * (that is, the elements in buffer) should all be negated; you want + * this if e.g. you're simplifying the (OR...) in (NOT (OR...)), + * intending to make the result an AND. */ static inline void push_back_associative_commute(Node n, std::vector<Node>& buffer, - Kind k, Kind notK) + Kind k, Kind notK, bool negateChildren = false) throw(AssertionException) { AssertArgument(buffer.empty(), buffer); AssertArgument(!n.isNull(), n); @@ -150,7 +163,13 @@ public: AssertArgument(n.getKind() == k, n, "expected node to have kind %s", kindToString(k).c_str()); - push_back_associative_commute_recursive(n, buffer, k, notK, false); + bool b CVC4_UNUSED = + push_back_associative_commute_recursive(n, buffer, k, notK, false); + + if(buffer.size() == 0) { + // all the TRUEs for an AND (resp FALSEs for an OR) were simplified away + buffer.push_back(NodeManager::currentNM()->mkConst(k == kind::AND ? true : false)); + } }/* push_back_associative_commute() */ /** @@ -168,6 +187,9 @@ public: base = base[0]; polarity = !polarity; } + if(n.getMetaKind() == kind::metakind::CONSTANT) { + return NodeManager::currentNM()->mkConst(!n.getConst<bool>()); + } if(polarity){ return base.notNode(); }else{ @@ -175,6 +197,26 @@ public: } } + /** + * Simplify an OR, AND, or IMPLIES. This function is the identity + * for all other kinds. + */ + inline static Node simplify(TNode n) throw(AssertionException) { + switch(n.getKind()) { + case kind::AND: + return simplifyConflict(n); + + case kind::OR: + return simplifyClause(n); + + case kind::IMPLIES: + return simplifyHornClause(n); + + default: + return n; + } + } + };/* class BooleanSimplification */ }/* CVC4 namespace */ diff --git a/src/util/cache.h b/src/util/cache.h new file mode 100644 index 000000000..08c624d99 --- /dev/null +++ b/src/util/cache.h @@ -0,0 +1,129 @@ +/********************* */ +/*! \file cache.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, 2010, 2011 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 A generic Cache<> template class for use by functions that + ** walk the Node DAG and want to cache results for sub-DAGs + ** + ** A generic Cache<> template class for use by functions that walk + ** the Node DAG and want to cache results for sub-DAGs. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__CACHE_H +#define __CVC4__CACHE_H + +#include <utility> +#include <functional> + +namespace CVC4 { + +/** + * A generic implementation of a cache for functions that walk the + * Node DAG performing a computation and want to cache some or all + * computations. + */ +template <class T, class U, class Hasher = std::hash<T> > +class Cache { + typedef std::hash_map<T, U, Hasher> Map; + Map d_map; + std::vector<T> d_current; + typename Map::iterator d_result; + + // disallow copy/assignment + Cache(const Cache&) CVC4_UNUSED; + Cache& operator=(const Cache&) CVC4_UNUSED; + +public: + + typedef T key_type; + typedef U value_type; + typedef Hasher hash_function; + + /** + * Makes it easy and error-free to use a Cache<> in a function. + */ + class Scope { + Cache& d_cache; + bool d_fired; + + public: + Scope(Cache<T, U, Hasher>& cache, const T& elt) throw(AssertionException) : + d_cache(cache), + d_fired(d_cache.computing(elt)) { + } + + ~Scope() { + if(!d_fired) { + d_cache();// pop stack + } + } + + operator bool() throw() { + return d_fired; + } + + const U& get() throw(AssertionException) { + Assert(d_fired, "nothing in cache"); + return d_cache.get(); + } + + U& operator()(U& computed) throw(AssertionException) { + Assert(!d_fired, "can only cache a computation once"); + d_fired = true; + return d_cache(computed); + } + const U& operator()(const U& computed) throw(AssertionException) { + Assert(!d_fired, "can only cache a computation once"); + d_fired = true; + return d_cache(computed); + } + };/* class Cache::Scope */ + + Cache() {} + + bool computing(const T& elt) { + d_result = d_map.find(elt); + bool found = (d_result != d_map.end()); + if(!found) { + d_current.push_back(elt); + } + return found; + } + + const U& get() { + Assert(d_result != d_map.end()); + return (*d_result).second; + } + + // cache nothing (just pop) + void operator()() { + d_current.pop_back(); + } + + U& operator()(U& result) { + d_map.insert(d_current.back(), result); + d_current.pop_back(); + return result; + } + const U& operator()(const U& result) { + d_map.insert(std::make_pair(d_current.back(), result)); + d_current.pop_back(); + return result; + } +};/* class Cache<> */ + + +}/* CVC4 namespace */ + +#endif /* __CVC4__CACHE_H */ diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp index 2a3f69fd6..ab52e7f93 100644 --- a/src/util/datatype.cpp +++ b/src/util/datatype.cpp @@ -109,7 +109,7 @@ void Datatype::addConstructor(const Constructor& c) { Cardinality Datatype::getCardinality() const throw(AssertionException) { CheckArgument(isResolved(), this, "this datatype is not yet resolved"); - RecursionBreaker<const Datatype*> breaker(__PRETTY_FUNCTION__, this); + RecursionBreaker<const Datatype*, DatatypeHashFunction> breaker(__PRETTY_FUNCTION__, this); if(breaker.isRecursion()) { return Cardinality::INTEGERS; } @@ -159,7 +159,7 @@ bool Datatype::isWellFounded() const throw(AssertionException) { return self.getAttribute(DatatypeWellFoundedAttr()); } - RecursionBreaker<const Datatype*> breaker(__PRETTY_FUNCTION__, this); + RecursionBreaker<const Datatype*, DatatypeHashFunction> breaker(__PRETTY_FUNCTION__, this); if(breaker.isRecursion()) { // This *path* is cyclic, so may not be well-founded. The // datatype itself might still be well-founded, though (we'll find @@ -518,7 +518,7 @@ bool Datatype::Constructor::isWellFounded() const throw(AssertionException) { return self.getAttribute(DatatypeWellFoundedAttr()); } - RecursionBreaker<const Datatype::Constructor*> breaker(__PRETTY_FUNCTION__, this); + RecursionBreaker<const Datatype::Constructor*, DatatypeHashFunction> breaker(__PRETTY_FUNCTION__, this); if(breaker.isRecursion()) { // This *path* is cyclic, sso may not be well-founded. The // constructor itself might still be well-founded, though (we'll @@ -563,7 +563,7 @@ Expr Datatype::Constructor::mkGroundTerm() const throw(AssertionException) { return groundTerm; } - RecursionBreaker<const Datatype::Constructor*> breaker(__PRETTY_FUNCTION__, this); + RecursionBreaker<const Datatype::Constructor*, DatatypeHashFunction> breaker(__PRETTY_FUNCTION__, this); if(breaker.isRecursion()) { // Recursive path, we should skip and go to the next constructor; // see lengthy comments in Datatype::mkGroundTerm(). diff --git a/src/util/datatype.h b/src/util/datatype.h index 75da1405f..7d9ae6f39 100644 --- a/src/util/datatype.h +++ b/src/util/datatype.h @@ -427,6 +427,24 @@ struct CVC4_PUBLIC DatatypeHashStrategy { } };/* struct DatatypeHashStrategy */ +/** + * A hash function for Datatypes. Needed to store them in hash sets + * and hash maps. + */ +struct CVC4_PUBLIC DatatypeHashFunction { + inline size_t operator()(const Datatype& dt) const { + return StringHashFunction()(dt.getName()); + } + inline size_t operator()(const Datatype* dt) const { + return StringHashFunction()(dt->getName()); + } + inline size_t operator()(const Datatype::Constructor& dtc) const { + return StringHashFunction()(dtc.getName()); + } + inline size_t operator()(const Datatype::Constructor* dtc) const { + return StringHashFunction()(dtc->getName()); + } +};/* struct DatatypeHashFunction */ // FUNCTION DECLARATIONS FOR OUTPUT STREAMS diff --git a/src/util/options.cpp b/src/util/options.cpp index 1329a443a..dbe0f6804 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -69,6 +69,8 @@ Options::Options() : memoryMap(false), strictParsing(false), lazyDefinitionExpansion(false), + simplificationMode(INCREMENTAL_MODE), + simplificationStyle(NO_SIMPLIFICATION_STYLE), interactive(false), interactiveSetByUser(false), segvNoSpin(false), @@ -83,7 +85,7 @@ Options::Options() : rewriteArithEqualities(false), arithPropagation(false), satRandomFreq(0.0), - satRandomSeed(91648253), //Minisat's default value + satRandomSeed(91648253),// Minisat's default value pivotRule(MINIMUM) { } @@ -102,10 +104,10 @@ static const string optionsDescription = "\ --no-checking disable ALL semantic checks, including type checks\n\ --no-theory-registration disable theory reg (not safe for some theories)\n\ --strict-parsing fail on non-conformant inputs (SMT2 only)\n\ - --verbose | -v increase verbosity (repeatable)\n\ - --quiet | -q decrease verbosity (repeatable)\n\ - --trace | -t tracing for something (e.g. --trace pushpop)\n\ - --debug | -d debugging for something (e.g. --debug arith), implies -t\n\ + --verbose | -v increase verbosity (may be repeated)\n\ + --quiet | -q decrease verbosity (may be repeated)\n\ + --trace | -t trace something (e.g. -t pushpop), can repeat\n\ + --debug | -d debug something (e.g. -d arith), can repeat\n\ --stats give statistics on exit\n\ --default-expr-depth=N print exprs to depth N (0 == default, -1 == no limit)\n\ --print-expr-types print types with variables when printing exprs\n\ @@ -115,8 +117,9 @@ static const string optionsDescription = "\ --produce-models support the get-value command\n\ --produce-assignments support the get-assignment command\n\ --lazy-definition-expansion expand define-fun lazily\n\ - --replay file replay decisions from file\n\ - --replay-log file log decisions and propagations to file\n\ + --simplification=MODE choose simplification mode, see --simplification=help\n\ + --replay=file replay decisions from file\n\ + --replay-log=file log decisions and propagations to file\n\ --pivot-rule=RULE change the pivot rule (see --pivot-rule help)\n\ --random-freq=P sets the frequency of random decisions in the sat solver(P=0.0 by default)\n\ --random-seed=S sets the random seed for the sat solver\n\ @@ -132,14 +135,42 @@ Languages currently supported as arguments to the -L / --lang option:\n\ smt2 | smtlib2 SMT-LIB format 2.0\n\ "; +static const string simplificationHelp = "\ +Simplification modes currently supported by the --simplification option:\n\ +\n\ +batch\n\ ++ save up all ASSERTions; run nonclausal simplification and clausal\n\ + (MiniSat) propagation for all of them only after reaching a querying command\n\ + (CHECKSAT or QUERY or predicate SUBTYPE declaration)\n\ +\n\ +incremental (default)\n\ ++ run nonclausal simplification and clausal propagation at each ASSERT\n\ + (and at CHECKSAT/QUERY/SUBTYPE)\n\ +\n\ +incremental-lazy-sat\n\ ++ run nonclausal simplification at each ASSERT, but delay clausification of\n\ + ASSERT until reaching a CHECKSAT/QUERY/SUBTYPE, then clausify them all\n\ +\n\ +You can also specify the level of aggressiveness for the simplification\n\ +(by repeating the --simplification option):\n\ +\n\ +toplevel (default)\n\ ++ apply toplevel simplifications (things known true/false at outer level\n\ + only)\n\ +\n\ +aggressive\n\ ++ do aggressive, local simplification across the entire formula\n\ +\n\ +none\n\ ++ do not perform nonclausal simplification\n\ +"; + string Options::getDescription() const { return optionsDescription; } void Options::printUsage(const std::string msg, std::ostream& out) { out << msg << optionsDescription << endl << flush; - // printf(usage + options.getDescription(), options.binary_name.c_str()); - // printf(usage, binary_name.c_str()); } void Options::printLanguageHelp(std::ostream& out) { @@ -155,7 +186,7 @@ void Options::printLanguageHelp(std::ostream& out) { * any collision. */ enum OptionValue { - SMTCOMP = 256, /* no clash with char options */ + SMTCOMP = 256, /* avoid clashing with char options */ STATS, SEGV_NOSPIN, PARSE_ONLY, @@ -168,6 +199,7 @@ enum OptionValue { PRINT_EXPR_TYPES, UF_THEORY, LAZY_DEFINITION_EXPANSION, + SIMPLIFICATION_MODE, INTERACTIVE, NO_INTERACTIVE, PRODUCE_MODELS, @@ -231,6 +263,7 @@ static struct option cmdlineOptions[] = { { "print-expr-types", no_argument , NULL, PRINT_EXPR_TYPES }, { "uf" , required_argument, NULL, UF_THEORY }, { "lazy-definition-expansion", no_argument, NULL, LAZY_DEFINITION_EXPANSION }, + { "simplification", required_argument, NULL, SIMPLIFICATION_MODE }, { "interactive", no_argument , NULL, INTERACTIVE }, { "no-interactive", no_argument , NULL, NO_INTERACTIVE }, { "produce-models", no_argument , NULL, PRODUCE_MODELS }, @@ -397,8 +430,8 @@ throw(OptionException) { uf_implementation = Options::MORGAN; } else if(!strcmp(optarg, "help")) { printf("UF implementations available:\n"); - printf("tim\n"); - printf("morgan\n"); + printf(" tim\n"); + printf(" morgan\n"); exit(1); } else { throw OptionException(string("unknown option for --uf: `") + @@ -411,6 +444,28 @@ throw(OptionException) { lazyDefinitionExpansion = true; break; + case SIMPLIFICATION_MODE: + if(!strcmp(optarg, "batch")) { + simplificationMode = BATCH_MODE; + } else if(!strcmp(optarg, "incremental")) { + simplificationMode = INCREMENTAL_MODE; + } else if(!strcmp(optarg, "incremental-lazy-sat")) { + simplificationMode = INCREMENTAL_LAZY_SAT_MODE; + } else if(!strcmp(optarg, "aggressive")) { + simplificationStyle = AGGRESSIVE_SIMPLIFICATION_STYLE; + } else if(!strcmp(optarg, "toplevel")) { + simplificationStyle = TOPLEVEL_SIMPLIFICATION_STYLE; + } else if(!strcmp(optarg, "none")) { + simplificationStyle = NO_SIMPLIFICATION_STYLE; + } else if(!strcmp(optarg, "help")) { + puts(simplificationHelp.c_str()); + exit(1); + } else { + throw OptionException(string("unknown option for --simplification: `") + + optarg + "'. Try --simplification help."); + } + break; + case INTERACTIVE: interactive = true; interactiveSetByUser = true; @@ -545,14 +600,12 @@ throw(OptionException) { printf("tls : %s\n", Configuration::isBuiltWithTlsSupport() ? "yes" : "no"); exit(0); - case '?': - throw OptionException(string("can't understand option `") + argv[optind - 1] + "'"); - case ':': throw OptionException(string("option `") + argv[optind - 1] + "' missing its required argument"); + case '?': default: - throw OptionException(string("can't understand option:") + argv[optind - 1] + "'"); + throw OptionException(string("can't understand option `") + argv[optind - 1] + "'"); } } diff --git a/src/util/options.h b/src/util/options.h index be432e5a7..d9d9c8567 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -34,7 +34,7 @@ namespace CVC4 { class ExprStream; /** Class representing an option-parsing exception. */ -class OptionException : public CVC4::Exception { +class CVC4_PUBLIC OptionException : public CVC4::Exception { public: OptionException(const std::string& s) throw() : CVC4::Exception("Error in option parsing: " + s) { @@ -104,6 +104,25 @@ struct CVC4_PUBLIC Options { /** Should we expand function definitions lazily? */ bool lazyDefinitionExpansion; + /** Enumeration of simplification modes (when to simplify). */ + typedef enum { + BATCH_MODE, + INCREMENTAL_MODE, + INCREMENTAL_LAZY_SAT_MODE + } SimplificationMode; + /** When to perform nonclausal simplifications. */ + SimplificationMode simplificationMode; + + /** Enumeration of simplification styles (how much to simplify). */ + typedef enum { + AGGRESSIVE_SIMPLIFICATION_STYLE, + TOPLEVEL_SIMPLIFICATION_STYLE, + NO_SIMPLIFICATION_STYLE + } SimplificationStyle; + + /** Style of nonclausal simplifications to perform. */ + SimplificationStyle simplificationStyle; + /** Whether we're in interactive mode or not */ bool interactive; @@ -188,6 +207,9 @@ struct CVC4_PUBLIC Options { };/* struct Options */ inline std::ostream& operator<<(std::ostream& out, + Options::UfImplementation uf) CVC4_PUBLIC; + +inline std::ostream& operator<<(std::ostream& out, Options::UfImplementation uf) { switch(uf) { case Options::TIM: @@ -203,7 +225,28 @@ inline std::ostream& operator<<(std::ostream& out, return out; } -std::ostream& operator<<(std::ostream& out, Options::ArithPivotRule rule); +inline std::ostream& operator<<(std::ostream& out, + Options::SimplificationMode mode) CVC4_PUBLIC; +inline std::ostream& operator<<(std::ostream& out, + Options::SimplificationMode mode) { + switch(mode) { + case Options::BATCH_MODE: + out << "BATCH_MODE"; + break; + case Options::INCREMENTAL_MODE: + out << "INCREMENTAL_MODE"; + break; + case Options::INCREMENTAL_LAZY_SAT_MODE: + out << "INCREMENTAL_LAZY_SAT_MODE"; + break; + default: + out << "SimplificationMode:UNKNOWN![" << unsigned(mode) << "]"; + } + + return out; +} + +std::ostream& operator<<(std::ostream& out, Options::ArithPivotRule rule) CVC4_PUBLIC; }/* CVC4 namespace */ diff --git a/src/util/output.cpp b/src/util/output.cpp index 88628481f..29de4c360 100644 --- a/src/util/output.cpp +++ b/src/util/output.cpp @@ -31,6 +31,9 @@ ostream null_os(&null_sb); NullC nullCvc4Stream CVC4_PUBLIC; +const std::string CVC4ostream::s_tab = " "; +const int CVC4ostream::s_indentIosIndex = ios_base::xalloc(); + DebugC DebugChannel CVC4_PUBLIC (&cout); WarningC WarningChannel CVC4_PUBLIC (&cerr); MessageC MessageChannel CVC4_PUBLIC (&cout); diff --git a/src/util/output.h b/src/util/output.h index b0e210c17..6d0f27f2a 100644 --- a/src/util/output.h +++ b/src/util/output.h @@ -21,6 +21,7 @@ #ifndef __CVC4__OUTPUT_H #define __CVC4__OUTPUT_H +#include <ios> #include <iostream> #include <string> #include <cstdio> @@ -59,20 +60,42 @@ extern null_streambuf null_sb; extern std::ostream null_os CVC4_PUBLIC; class CVC4_PUBLIC CVC4ostream { + static const std::string s_tab; + static const int s_indentIosIndex; + + /** The underlying ostream */ std::ostream* d_os; - // Current indentation - unsigned d_indent; + /** Are we in the first column? */ + bool d_firstColumn; - std::ostream& (*d_endl)(std::ostream&); + /** The endl manipulator (why do we need to keep this?) */ + std::ostream& (*const d_endl)(std::ostream&); public: - CVC4ostream() : d_os(NULL) {} - explicit CVC4ostream(std::ostream* os) : d_os(os), d_indent(0) { - d_endl = &std::endl; + CVC4ostream() : + d_os(NULL), + d_firstColumn(false), + d_endl(&std::endl) { + } + explicit CVC4ostream(std::ostream* os) : + d_os(os), + d_firstColumn(true), + d_endl(&std::endl) { } - void pushIndent() { d_indent ++; } - void popIndent() { if (d_indent > 0) -- d_indent; } + void pushIndent() { + if(d_os != NULL) { + ++d_os->iword(s_indentIosIndex); + } + } + void popIndent() { + if(d_os != NULL) { + long& indent = d_os->iword(s_indentIosIndex); + if(indent > 0) { + --indent; + } + } + } CVC4ostream& flush() { if(d_os != NULL) { @@ -87,6 +110,13 @@ public: template <class T> CVC4ostream& operator<<(T const& t) { if(d_os != NULL) { + if(d_firstColumn) { + d_firstColumn = false; + long indent = d_os->iword(s_indentIosIndex); + for(long i = 0; i < indent; ++ i) { + d_os = &(*d_os << s_tab); + } + } d_os = &(*d_os << t); } return *this; @@ -97,10 +127,8 @@ public: if(d_os != NULL) { d_os = &(*d_os << pf); - if (pf == d_endl) { - for (unsigned i = 0; i < d_indent; ++ i) { - d_os = &(*d_os << '\t'); - } + if(pf == d_endl) { + d_firstColumn = true; } } return *this; @@ -452,6 +480,27 @@ public: extern NullC nullCvc4Stream CVC4_PUBLIC; +/** + * Pushes an indentation level on construction, pop on destruction. + * Useful for tracing recursive functions especially, but also can be + * used for clearly separating different phases of an algorithm, + * or iterations of a loop, or... etc. + */ +class IndentedScope { + CVC4ostream d_out; +public: + inline IndentedScope(CVC4ostream out); + inline ~IndentedScope(); +};/* class IndentedScope */ + +#ifdef CVC4_DEBUG +inline IndentedScope::IndentedScope(CVC4ostream out) : d_out(out) { d_out << push; } +inline IndentedScope::~IndentedScope() { d_out << pop; } +#else /* CVC4_DEBUG */ +inline IndentedScope::IndentedScope(CVC4ostream out) {} +inline IndentedScope::~IndentedScope() {} +#endif /* CVC4_DEBUG */ + }/* CVC4 namespace */ #endif /* __CVC4__OUTPUT_H */ diff --git a/src/util/recursion_breaker.h b/src/util/recursion_breaker.h index 6f82eec5c..6573e9b64 100644 --- a/src/util/recursion_breaker.h +++ b/src/util/recursion_breaker.h @@ -79,10 +79,9 @@ namespace CVC4 { -template <class T> +template <class T, class Hasher = std::hash<T> > class RecursionBreaker { - //typedef std::hash_set<T> Set; - typedef std::set<T> Set; + typedef std::hash_set<T, Hasher> Set; typedef std::map<std::string, Set> Map; static CVC4_THREADLOCAL(Map*) s_maps; @@ -92,6 +91,7 @@ class RecursionBreaker { bool d_recursion; public: + /** Mark that item has been seen for tag. */ RecursionBreaker(std::string tag, const T& item) : d_tag(tag), d_item(item) { @@ -107,6 +107,7 @@ public: } } + /** Clean up the seen trail. */ ~RecursionBreaker() { Assert(s_maps->find(d_tag) != s_maps->end()); if(!d_recursion) { @@ -119,14 +120,15 @@ public: } } + /** Return true iff recursion has been detected. */ bool isRecursion() const throw() { return d_recursion; } };/* class RecursionBreaker<T> */ -template <class T> -CVC4_THREADLOCAL(typename RecursionBreaker<T>::Map*) RecursionBreaker<T>::s_maps; +template <class T, class Hasher> +CVC4_THREADLOCAL(typename RecursionBreaker<T, Hasher>::Map*) RecursionBreaker<T, Hasher>::s_maps; }/* CVC4 namespace */ diff --git a/src/util/tls.h.in b/src/util/tls.h.in index c2892d11c..fc0b6932b 100644 --- a/src/util/tls.h.in +++ b/src/util/tls.h.in @@ -26,13 +26,17 @@ #line 28 "@srcdir@/tls.h.in" +// A bit obnoxious: we have to take varargs to support multi-argument +// template types in the threadlocals. +// E.g. "CVC4_THREADLOCAL(hash_set<type, hasher>*)" fails otherwise, +// due to the embedded comma. #if @CVC4_TLS_SUPPORTED@ -# define CVC4_THREADLOCAL(__type) @CVC4_TLS@ __type -# define CVC4_THREADLOCAL_PUBLIC(__type) @CVC4_TLS@ CVC4_PUBLIC __type +# define CVC4_THREADLOCAL(__type...) @CVC4_TLS@ __type +# define CVC4_THREADLOCAL_PUBLIC(__type...) @CVC4_TLS@ CVC4_PUBLIC __type #else # include <pthread.h> -# define CVC4_THREADLOCAL(__type) ::CVC4::ThreadLocal< __type > -# define CVC4_THREADLOCAL_PUBLIC(__type) CVC4_PUBLIC ::CVC4::ThreadLocal< __type > +# define CVC4_THREADLOCAL(__type...) ::CVC4::ThreadLocal< __type > +# define CVC4_THREADLOCAL_PUBLIC(__type...) CVC4_PUBLIC ::CVC4::ThreadLocal< __type > namespace CVC4 { @@ -76,6 +80,49 @@ public: };/* class ThreadLocalImpl<T, true> */ template <class T> +class ThreadLocalImpl<T*, true> { + pthread_key_t d_key; + + static void cleanup(void*) { + } + +public: + ThreadLocalImpl() { + pthread_key_create(&d_key, ThreadLocalImpl::cleanup); + } + + ThreadLocalImpl(const T* t) { + pthread_key_create(&d_key, ThreadLocalImpl::cleanup); + pthread_setspecific(d_key, const_cast<void*>(reinterpret_cast<const void*>(t))); + } + + ThreadLocalImpl(const ThreadLocalImpl& tl) { + pthread_key_create(&d_key, ThreadLocalImpl::cleanup); + pthread_setspecific(d_key, const_cast<void*>(reinterpret_cast<const void*>(static_cast<const T*>(tl)))); + } + + ThreadLocalImpl& operator=(const T* t) { + pthread_setspecific(d_key, const_cast<void*>(reinterpret_cast<const void*>(t))); + return *this; + } + ThreadLocalImpl& operator=(const ThreadLocalImpl& tl) { + pthread_setspecific(d_key, const_cast<void*>(reinterpret_cast<const void*>(static_cast<const T*>(tl)))); + return *this; + } + + operator T*() const { + return static_cast<T*>(pthread_getspecific(d_key)); + } + + T operator*() { + return *static_cast<T*>(pthread_getspecific(d_key)); + } + T* operator->() { + return static_cast<T*>(pthread_getspecific(d_key)); + } +};/* class ThreadLocalImpl<T*, true> */ + +template <class T> class ThreadLocalImpl<T, false> { };/* class ThreadLocalImpl<T, false> */ diff --git a/src/util/utility.h b/src/util/utility.h new file mode 100644 index 000000000..9aa4c1158 --- /dev/null +++ b/src/util/utility.h @@ -0,0 +1,75 @@ +/********************* */ +/*! \file utility.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, 2010, 2011 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 Some standard STL-related utility functions for CVC4 + ** + ** Some standard STL-related utility functions for CVC4. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__UTILITY_H +#define __CVC4__UTILITY_H + +#include <utility> +#include <functional> + +namespace CVC4 { + + +/** + * Like std::equal_to<>, but tests equality between the first element + * of a pair and an element. + */ +template <class T, class U> +struct first_equal_to : std::binary_function<std::pair<T, U>, T, bool> { + bool operator()(const std::pair<T, U>& pr, const T& x) const { + return pr.first == x; + } +};/* struct first_equal_to<T> */ + + +/** + * Like std::equal_to<>, but tests equality between the second element + * of a pair and an element. + */ +template <class T, class U> +struct second_equal_to : std::binary_function<std::pair<T, U>, U, bool> { + bool operator()(const std::pair<T, U>& pr, const U& x) const { + return pr.second == x; + } +};/* struct first_equal_to<T> */ + + +/** + * Using std::find_if(), finds the first iterator in [first,last) + * range that satisfies predicate. If none, return last; otherwise, + * search for a second one. If there IS a second one, return last, + * otherwise return the first (and unique) iterator satisfying pred(). + */ +template <class InputIterator, class Predicate> +inline InputIterator find_if_unique(InputIterator first, InputIterator last, Predicate pred) { + InputIterator match = std::find_if(first, last, pred); + if(match == last) { + return last; + } + + InputIterator match2 = match; + match2 = std::find_if(++match2, last, pred); + return (match2 == last) ? match : last; +} + + +}/* CVC4 namespace */ + +#endif /* __CVC4__UTILITY_H */ |