diff options
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/Assert.h | 18 | ||||
-rw-r--r-- | src/util/Makefile.am | 4 | ||||
-rw-r--r-- | src/util/boolean_simplification.cpp | 45 | ||||
-rw-r--r-- | src/util/boolean_simplification.h | 140 | ||||
-rw-r--r-- | src/util/output.h | 4 | ||||
-rw-r--r-- | src/util/subrange_bound.h | 94 |
6 files changed, 257 insertions, 48 deletions
diff --git a/src/util/Assert.h b/src/util/Assert.h index ec942e00b..0ff89bedf 100644 --- a/src/util/Assert.h +++ b/src/util/Assert.h @@ -250,8 +250,8 @@ void debugAssertionFailed(const AssertionException& thisException, if(EXPECT_FALSE( ! (cond) )) { \ /* save the last assertion failure */ \ const char* lastException = s_debugLastException; \ - AssertionException exception(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \ - debugAssertionFailed(exception, lastException); \ + CVC4::AssertionException exception(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \ + CVC4::debugAssertionFailed(exception, lastException); \ } \ } while(0) @@ -261,27 +261,27 @@ void debugAssertionFailed(const AssertionException& thisException, # define AlwaysAssert(cond, msg...) \ do { \ if(EXPECT_FALSE( ! (cond) )) { \ - throw AssertionException(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \ + throw CVC4::AssertionException(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \ } \ } while(0) #endif /* CVC4_DEBUG */ #define Unreachable(msg...) \ - throw UnreachableCodeException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) + throw CVC4::UnreachableCodeException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) #define Unhandled(msg...) \ - throw UnhandledCaseException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) + throw CVC4::UnhandledCaseException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) #define Unimplemented(msg...) \ - throw UnimplementedOperationException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) + throw CVC4::UnimplementedOperationException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) #define InternalError(msg...) \ - throw InternalErrorException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) + throw CVC4::InternalErrorException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) #define IllegalArgument(arg, msg...) \ - throw IllegalArgumentException(#arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) + throw CVC4::IllegalArgumentException(#arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) #define CheckArgument(cond, arg, msg...) \ AlwaysAssertArgument(cond, arg, ## msg) #define AlwaysAssertArgument(cond, arg, msg...) \ do { \ if(EXPECT_FALSE( ! (cond) )) { \ - throw IllegalArgumentException(#cond, #arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \ + throw CVC4::IllegalArgumentException(#cond, #arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \ } \ } while(0) diff --git a/src/util/Makefile.am b/src/util/Makefile.am index aaf9ca03b..e76858d80 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -46,9 +46,11 @@ libutil_la_SOURCES = \ dynamic_array.h \ language.h \ triple.h \ + subrange_bound.h \ trans_closure.h \ trans_closure.cpp \ - boolean_simplification.h + boolean_simplification.h \ + boolean_simplification.cpp libutil_la_LIBADD = \ @builddir@/libutilcudd.la diff --git a/src/util/boolean_simplification.cpp b/src/util/boolean_simplification.cpp new file mode 100644 index 000000000..a154f342f --- /dev/null +++ b/src/util/boolean_simplification.cpp @@ -0,0 +1,45 @@ +/********************* */ +/*! \file boolean_simplification.cpp + ** \verbatim + ** Original author: taking + ** 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 Simple routines for Boolean simplification + ** + ** Simple, commonly-used routines for Boolean simplification. + **/ + +#include "util/boolean_simplification.h" + +namespace CVC4 { + +void +BooleanSimplification::push_back_associative_commute_recursive + (Node n, std::vector<Node>& buffer, Kind k, Kind notK, bool negateNode) + throw(AssertionException) { + Node::iterator i = n.begin(), end = n.end(); + for(; i != end; ++i){ + Node child = *i; + if(child.getKind() == k){ + push_back_associative_commute_recursive(child, buffer, k, notK, negateNode); + }else if(child.getKind() == kind::NOT && child[0].getKind() == notK){ + push_back_associative_commute_recursive(child, buffer, notK, k, !negateNode); + }else{ + if(negateNode){ + buffer.push_back(negate(child)); + }else{ + buffer.push_back(child); + } + } + } +}/* BooleanSimplification::push_back_associative_commute_recursive() */ + +}/* CVC4 namespace */ + diff --git a/src/util/boolean_simplification.h b/src/util/boolean_simplification.h index 95d5fb435..e938a2b38 100644 --- a/src/util/boolean_simplification.h +++ b/src/util/boolean_simplification.h @@ -11,10 +11,9 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief [[ Add one-line brief description here ]] + ** \brief Simple routines for Boolean simplification ** - ** [[ Add lengthier description here ]] - ** \todo document this file + ** Simple, commonly-used routines for Boolean simplification. **/ #include "cvc4_private.h" @@ -22,30 +21,62 @@ #ifndef __CVC4__BOOLEAN_SIMPLIFICATION_H #define __CVC4__BOOLEAN_SIMPLIFICATION_H -#include "expr/node.h" -#include "util/Assert.h" #include <vector> +#include <algorithm> +#include "expr/node.h" +#include "util/Assert.h" namespace CVC4 { +/** + * A class to contain a number of useful functions for simple + * simplification of nodes. One never uses it as an object (and + * it cannot be constructed). It is used as a namespace. + */ class BooleanSimplification { + // cannot construct one of these + BooleanSimplification() CVC4_UNUSED; + BooleanSimplification(const BooleanSimplification&) CVC4_UNUSED; + + static void push_back_associative_commute_recursive + (Node n, std::vector<Node>& buffer, Kind k, Kind notK, bool negateNode) + throw(AssertionException); + public: + /** + * The threshold for removing duplicates. (See removeDuplicates().) + */ static const uint32_t DUPLICATE_REMOVAL_THRESHOLD = 10; - static void removeDuplicates(std::vector<Node>& buffer){ - if(buffer.size() < DUPLICATE_REMOVAL_THRESHOLD){ + /** + * Remove duplicate nodes from a vector, modifying it in-place. + * If the vector has size >= DUPLICATE_REMOVAL_THRESHOLD, this + * function is a no-op. + */ + static void removeDuplicates(std::vector<Node>& buffer) + throw(AssertionException) { + if(buffer.size() < DUPLICATE_REMOVAL_THRESHOLD) { std::sort(buffer.begin(), buffer.end()); - std::vector<Node>::iterator new_end = std::unique(buffer.begin(), buffer.end()); + std::vector<Node>::iterator new_end = + std::unique(buffer.begin(), buffer.end()); buffer.erase(new_end, buffer.end()); } } - static Node simplifyConflict(Node andNode){ - Assert(andNode.getKind() == kind::AND); + /** + * Takes a node with kind AND, collapses all AND and (NOT OR)-kinded + * children of it (as far as possible---see + * push_back_associative_commute()), removes duplicates, and returns + * the resulting Node. + */ + static Node simplifyConflict(Node andNode) throw(AssertionException) { + AssertArgument(!andNode.isNull(), andNode); + AssertArgument(andNode.getKind() == kind::AND, andNode); + std::vector<Node> buffer; - push_back_associative_commute(andNode, buffer, kind::AND, kind::OR, false); + push_back_associative_commute(andNode, buffer, kind::AND, kind::OR); removeDuplicates(buffer); @@ -54,10 +85,18 @@ public: return nb; } - static Node simplifyClause(Node orNode){ - Assert(orNode.getKind() == kind::OR); + /** + * Takes a node with kind OR, collapses all OR and (NOT AND)-kinded + * children of it (as far as possible---see + * push_back_associative_commute()), removes duplicates, and returns + * the resulting Node. + */ + static Node simplifyClause(Node orNode) throw(AssertionException) { + AssertArgument(!orNode.isNull(), orNode); + AssertArgument(orNode.getKind() == kind::OR, orNode); + std::vector<Node> buffer; - push_back_associative_commute(orNode, buffer, kind::OR, kind::AND, false); + push_back_associative_commute(orNode, buffer, kind::OR, kind::AND); removeDuplicates(buffer); @@ -66,34 +105,63 @@ public: return nb; } - static Node simplifyHornClause(Node implication){ - Assert(implication.getKind() == kind::IMPLIES); + /** + * Takes a node with kind IMPLIES, converts it to an OR, then + * simplifies the result with simplifyClause(). + * + * The input doesn't actually have to be Horn, it seems, but that's + * the common case(?), hence the name. + */ + static Node simplifyHornClause(Node implication) throw(AssertionException) { + AssertArgument(implication.getKind() == kind::IMPLIES, implication); + TNode left = implication[0]; TNode right = implication[1]; - Node notLeft = NodeBuilder<1>(kind::NOT)<<left; - Node clause = NodeBuilder<2>(kind::OR)<< notLeft << right; + + Node notLeft = negate(left); + Node clause = NodeBuilder<2>(kind::OR) << notLeft << right; + return simplifyClause(clause); } - static void push_back_associative_commute(Node n, std::vector<Node>& buffer, Kind k, Kind notK, bool negateNode){ - Node::iterator i = n.begin(), end = n.end(); - for(; i != end; ++i){ - Node child = *i; - if(child.getKind() == k){ - push_back_associative_commute(child, buffer, k, notK, negateNode); - }else if(child.getKind() == kind::NOT && child[0].getKind() == notK){ - push_back_associative_commute(child, buffer, notK, k, !negateNode); - }else{ - if(negateNode){ - buffer.push_back(negate(child)); - }else{ - buffer.push_back(child); - } - } - } - } + /** + * Aids in reforming a node. Takes a node of (N-ary) kind k and + * copies its children into an output vector, collapsing its k-kinded + * children into it. Also collapses negations of notK. For example: + * + * push_back_associative_commute( [OR [OR a b] [OR b c d] [NOT [AND e f]]], + * buffer, kind::OR, kind::AND ) + * yields a "buffer" vector of [a b b c d e f] + * + * @param n the node to operate upon + * @param buffer the output vector (must be empty on entry) + * @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. + */ + static inline void + push_back_associative_commute(Node n, std::vector<Node>& buffer, + Kind k, Kind notK) + throw(AssertionException) { + AssertArgument(buffer.empty(), buffer); + AssertArgument(!n.isNull(), n); + AssertArgument(k != kind::UNDEFINED_KIND && k != kind::NULL_EXPR, k); + AssertArgument(notK != kind::NULL_EXPR, notK); + 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); + }/* push_back_associative_commute() */ + + /** + * Negates a node, doing all the double-negation elimination + * that's possible. + * + * @param n the node to negate (cannot be the null node) + */ + static Node negate(TNode n) throw(AssertionException) { + AssertArgument(!n.isNull(), n); - static Node negate(TNode n){ bool polarity = true; TNode base = n; while(base.getKind() == kind::NOT){ diff --git a/src/util/output.h b/src/util/output.h index 0b1c86afd..d3eb3a831 100644 --- a/src/util/output.h +++ b/src/util/output.h @@ -273,7 +273,7 @@ public: /** The debug output singleton */ extern DebugC DebugChannel CVC4_PUBLIC; #ifdef CVC4_DEBUG -# define Debug DebugChannel +# define Debug CVC4::DebugChannel #else /* CVC4_DEBUG */ # define Debug CVC4::__cvc4_true() ? CVC4::debugNullCvc4Stream : CVC4::DebugChannel #endif /* CVC4_DEBUG */ @@ -290,7 +290,7 @@ extern ChatC Chat CVC4_PUBLIC; /** The trace output singleton */ extern TraceC TraceChannel CVC4_PUBLIC; #ifdef CVC4_TRACING -# define Trace TraceChannel +# define Trace CVC4::TraceChannel #else /* CVC4_TRACING */ # define Trace CVC4::__cvc4_true() ? CVC4::debugNullCvc4Stream : CVC4::TraceChannel #endif /* CVC4_TRACING */ diff --git a/src/util/subrange_bound.h b/src/util/subrange_bound.h new file mode 100644 index 000000000..fc6a259b4 --- /dev/null +++ b/src/util/subrange_bound.h @@ -0,0 +1,94 @@ +/********************* */ +/*! \file subrange_bound.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 Representation of subrange bounds + ** + ** Simple class to represent a subrange bound, either infinite + ** (no bound) or finite (an arbitrary precision integer). + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__SUBRANGE_BOUND_H +#define __CVC4__SUBRANGE_BOUND_H + +#include "util/integer.h" +#include "util/Assert.h" + +namespace CVC4 { + +/** + * Representation of a subrange bound. A bound can either exist and be + * a finite arbitrary-precision integer, or not exist (and thus be + * an infinite bound). For example, the CVC language subrange [-5.._] + * has a lower bound of -5 and an infinite upper bound. + */ +class SubrangeBound { + bool d_nobound; + Integer d_bound; + +public: + + /** Construct an infinite SubrangeBound. */ + SubrangeBound() throw() : + d_nobound(true), + d_bound() { + } + + /** Construct a finite SubrangeBound. */ + SubrangeBound(const Integer& i) throw() : + d_nobound(false), + d_bound(i) { + } + + ~SubrangeBound() throw() { + } + + /** Get the finite SubrangeBound, failing an assertion if infinite. */ + Integer getBound() const throw(IllegalArgumentException) { + CheckArgument(!d_nobound, this, "SubrangeBound is infinite"); + return d_bound; + } + + /** Returns true iff this is a finite SubrangeBound. */ + bool hasBound() const throw() { + return !d_nobound; + } + + /** Test two SubrangeBounds for equality. */ + bool operator==(const SubrangeBound& b) const throw() { + return hasBound() == b.hasBound() && + (!hasBound() || getBound() == b.getBound()); + } + + /** Test two SubrangeBounds for disequality. */ + bool operator!=(const SubrangeBound& b) const throw() { + return !(*this == b); + } + +};/* class SubrangeBound */ + +inline std::ostream& +operator<<(std::ostream& out, const SubrangeBound& bound) throw() { + if(bound.hasBound()) { + out << bound.getBound(); + } else { + out << '_'; + } + + return out; +} + +}/* CVC4 namespace */ + +#endif /* __CVC4__SUBRANGE_BOUND_H */ |