diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-04-23 05:15:56 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-04-23 05:15:56 +0000 |
commit | 57b8c4c8581d2d3ffcf3d3a1bb228271cb4d074a (patch) | |
tree | 1c1781cc83118e4bbd2ad6939b16734c30a69f1a /src/util/boolean_simplification.h | |
parent | 673d0e86b91094a58433c3ca71591fb0a0c60f84 (diff) |
* reviewed BooleanSimplification, added documentation & unit test
* work around a lexer ambiguity in CVC grammar
* add support for tracing antlr parser/lexer
* add parsing support for more language features
* initial parameterized types parsing work to support Andy's work
Diffstat (limited to 'src/util/boolean_simplification.h')
-rw-r--r-- | src/util/boolean_simplification.h | 140 |
1 files changed, 104 insertions, 36 deletions
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){ |