summaryrefslogtreecommitdiff
path: root/src/util
diff options
context:
space:
mode:
Diffstat (limited to 'src/util')
-rw-r--r--src/util/Makefile.am2
-rw-r--r--src/util/ite_removal.cpp57
-rw-r--r--src/util/ite_removal.h29
-rw-r--r--src/util/nary_builder.cpp183
-rw-r--r--src/util/nary_builder.h38
5 files changed, 292 insertions, 17 deletions
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 156288600..5647a2057 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -76,6 +76,8 @@ libutil_la_SOURCES = \
boolean_simplification.cpp \
ite_removal.h \
ite_removal.cpp \
+ nary_builder.h \
+ nary_builder.cpp \
node_visitor.h \
chain.h \
index.h \
diff --git a/src/util/ite_removal.cpp b/src/util/ite_removal.cpp
index 7d4948251..5231e05c2 100644
--- a/src/util/ite_removal.cpp
+++ b/src/util/ite_removal.cpp
@@ -17,15 +17,37 @@
#include <vector>
#include "util/ite_removal.h"
-#include "theory/rewriter.h"
#include "expr/command.h"
#include "theory/quantifiers/options.h"
+#include "theory/ite_utilities.h"
using namespace CVC4;
using namespace std;
namespace CVC4 {
+RemoveITE::RemoveITE(context::UserContext* u)
+ : d_iteCache(u)
+{
+ d_containsVisitor = new theory::ContainsTermITEVistor();
+}
+
+RemoveITE::~RemoveITE(){
+ delete d_containsVisitor;
+}
+
+void RemoveITE::garbageCollect(){
+ d_containsVisitor->garbageCollect();
+}
+
+theory::ContainsTermITEVistor* RemoveITE::getContainsVisitor(){
+ return d_containsVisitor;
+}
+
+size_t RemoveITE::collectedCacheSizes() const{
+ return d_containsVisitor->cache_size() + d_iteCache.size();
+}
+
void RemoveITE::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap)
{
for (unsigned i = 0, i_end = output.size(); i < i_end; ++ i) {
@@ -38,18 +60,28 @@ void RemoveITE::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap)
}
}
+bool RemoveITE::containsTermITE(TNode e){
+ return d_containsVisitor->containsTermITE(e);
+}
+
Node RemoveITE::run(TNode node, std::vector<Node>& output,
- IteSkolemMap& iteSkolemMap, std::vector<Node>& quantVar) {
+ IteSkolemMap& iteSkolemMap,
+ std::vector<Node>& quantVar) {
// Current node
Debug("ite") << "removeITEs(" << node << ")" << endl;
+ if(node.isVar() || node.isConst() ||
+ (options::biasedITERemoval() && !containsTermITE(node))){
+ return Node(node);
+ }
+
// The result may be cached already
NodeManager *nodeManager = NodeManager::currentNM();
- ITECache::iterator i = d_iteCache.find(node);
+ ITECache::const_iterator i = d_iteCache.find(node);
if(i != d_iteCache.end()) {
- Node cachedRewrite = (*i).second;
- Debug("ite") << "removeITEs: in-cache: " << cachedRewrite << endl;
- return cachedRewrite.isNull() ? Node(node) : cachedRewrite;
+ Node cached = (*i).second;
+ Debug("ite") << "removeITEs: in-cache: " << cached << endl;
+ return cached.isNull() ? Node(node) : cached;
}
// If an ITE replace it
@@ -81,7 +113,7 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output,
Debug("ite") << "removeITEs(" << node << ") => " << newAssertion << endl;
// Attach the skolem
- d_iteCache[node] = skolem;
+ d_iteCache.insert(node, skolem);
// Remove ITEs from the new assertion, rewrite it and push it to the output
newAssertion = run(newAssertion, output, iteSkolemMap, quantVar);
@@ -127,17 +159,18 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output,
// If changes, we rewrite
if(somethingChanged) {
- Node cachedRewrite = nodeManager->mkNode(node.getKind(), newChildren);
- d_iteCache[node] = cachedRewrite;
- return cachedRewrite;
+ Node cached = nodeManager->mkNode(node.getKind(), newChildren);
+ d_iteCache.insert(node, cached);
+ return cached;
} else {
- d_iteCache[node] = Node::null();
+ d_iteCache.insert(node, Node::null());
return node;
}
} else {
- d_iteCache[node] = Node::null();
+ d_iteCache.insert(node, Node::null());
return node;
}
}
+
}/* CVC4 namespace */
diff --git a/src/util/ite_removal.h b/src/util/ite_removal.h
index 03197be89..9d79687f4 100644
--- a/src/util/ite_removal.h
+++ b/src/util/ite_removal.h
@@ -22,21 +22,25 @@
#include "expr/node.h"
#include "util/dump.h"
#include "context/context.h"
-#include "context/cdhashmap.h"
+#include "context/cdinsert_hashmap.h"
namespace CVC4 {
+namespace theory {
+class ContainsTermITEVistor;
+}
+
typedef std::hash_map<Node, unsigned, NodeHashFunction> IteSkolemMap;
class RemoveITE {
- typedef context::CDHashMap<Node, Node, NodeHashFunction> ITECache;
+ typedef context::CDInsertHashMap<Node, Node, NodeHashFunction> ITECache;
ITECache d_iteCache;
+
public:
- RemoveITE(context::UserContext* u) :
- d_iteCache(u) {
- }
+ RemoveITE(context::UserContext* u);
+ ~RemoveITE();
/**
* Removes the ITE nodes by introducing skolem variables. All
@@ -57,6 +61,21 @@ public:
Node run(TNode node, std::vector<Node>& additionalAssertions,
IteSkolemMap& iteSkolemMap, std::vector<Node>& quantVar);
+ /** Returns true if e contains a term ite.*/
+ bool containsTermITE(TNode e);
+
+ /** Returns the collected size of the caches.*/
+ size_t collectedCacheSizes() const;
+
+ /** Garbage collects non-context dependent data-structures.*/
+ void garbageCollect();
+
+ /** Return the RemoveITE's containsVisitor.*/
+ theory::ContainsTermITEVistor* getContainsVisitor();
+
+private:
+ theory::ContainsTermITEVistor* d_containsVisitor;
+
};/* class RemoveTTE */
}/* CVC4 namespace */
diff --git a/src/util/nary_builder.cpp b/src/util/nary_builder.cpp
new file mode 100644
index 000000000..004dd3382
--- /dev/null
+++ b/src/util/nary_builder.cpp
@@ -0,0 +1,183 @@
+
+#include "util/nary_builder.h"
+#include "expr/metakind.h"
+using namespace std;
+
+namespace CVC4 {
+namespace util {
+
+Node NaryBuilder::mkAssoc(Kind kind, const std::vector<Node>& children){
+ if(children.size() == 0){
+ return zeroArity(kind);
+ }else if(children.size() == 1){
+ return children[0];
+ }else{
+ const unsigned int max = kind::metakind::getUpperBoundForKind(kind);
+ const unsigned int min = kind::metakind::getLowerBoundForKind(kind);
+
+ Assert(min <= children.size());
+
+ unsigned int numChildren = children.size();
+ NodeManager* nm = NodeManager::currentNM();
+ if( numChildren <= max ) {
+ return nm->mkNode(kind,children);
+ }
+
+ typedef std::vector<Node>::const_iterator const_iterator;
+ const_iterator it = children.begin() ;
+ const_iterator end = children.end() ;
+
+ /* The new top-level children and the children of each sub node */
+ std::vector<Node> newChildren;
+ std::vector<Node> subChildren;
+
+ while( it != end && numChildren > max ) {
+ /* Grab the next max children and make a node for them. */
+ for(const_iterator next = it + max; it != next; ++it, --numChildren ) {
+ subChildren.push_back(*it);
+ }
+ Node subNode = nm->mkNode(kind,subChildren);
+ newChildren.push_back(subNode);
+ subChildren.clear();
+ }
+
+ /* If there's children left, "top off" the Expr. */
+ if(numChildren > 0) {
+ /* If the leftovers are too few, just copy them into newChildren;
+ * otherwise make a new sub-node */
+ if(numChildren < min) {
+ for(; it != end; ++it) {
+ newChildren.push_back(*it);
+ }
+ } else {
+ for(; it != end; ++it) {
+ subChildren.push_back(*it);
+ }
+ Node subNode = nm->mkNode(kind, subChildren);
+ newChildren.push_back(subNode);
+ }
+ }
+
+ /* It's inconceivable we could have enough children for this to fail
+ * (more than 2^32, in most cases?). */
+ AlwaysAssert( newChildren.size() <= max,
+ "Too many new children in mkAssociative" );
+
+ /* It would be really weird if this happened (it would require
+ * min > 2, for one thing), but let's make sure. */
+ AlwaysAssert( newChildren.size() >= min,
+ "Too few new children in mkAssociative" );
+
+ return nm->mkNode(kind,newChildren);
+ }
+}
+
+Node NaryBuilder::zeroArity(Kind k){
+ using namespace kind;
+ NodeManager* nm = NodeManager::currentNM();
+ switch(k){
+ case AND:
+ return nm->mkConst(true);
+ case OR:
+ return nm->mkConst(false);
+ case PLUS:
+ return nm->mkConst(Rational(0));
+ case MULT:
+ return nm->mkConst(Rational(1));
+ default:
+ return Node::null();
+ }
+}
+
+
+RePairAssocCommutativeOperators::RePairAssocCommutativeOperators()
+ : d_cache()
+{}
+RePairAssocCommutativeOperators::~RePairAssocCommutativeOperators(){}
+size_t RePairAssocCommutativeOperators::size() const{ return d_cache.size(); }
+void RePairAssocCommutativeOperators::clear(){ d_cache.clear(); }
+
+bool RePairAssocCommutativeOperators::isAssociateCommutative(Kind k){
+ using namespace kind;
+ switch(k){
+ case BITVECTOR_CONCAT:
+ case BITVECTOR_AND:
+ case BITVECTOR_OR:
+ case BITVECTOR_XOR:
+ case BITVECTOR_MULT:
+ case BITVECTOR_PLUS:
+ case DISTINCT:
+ case PLUS:
+ case MULT:
+ case AND:
+ case OR:
+ return true;
+ default:
+ return false;
+ }
+}
+
+Node RePairAssocCommutativeOperators::rePairAssocCommutativeOperators(TNode n){
+ if(d_cache.find(n) != d_cache.end()){
+ return d_cache[n];
+ }
+ Node result =
+ isAssociateCommutative(n.getKind()) ?
+ case_assoccomm(n) : case_other(n);
+
+ d_cache[n] = result;
+ return result;
+}
+
+Node RePairAssocCommutativeOperators::case_assoccomm(TNode n){
+ Kind k = n.getKind();
+ Assert(isAssociateCommutative(k));
+ Assert(n.getMetaKind() != kind::metakind::PARAMETERIZED);
+ unsigned N = n.getNumChildren();
+ Assert(N >= 2);
+
+
+ Node last = rePairAssocCommutativeOperators( n[N-1]);
+ Node nextToLast = rePairAssocCommutativeOperators(n[N-2]);
+
+ NodeManager* nm = NodeManager::currentNM();
+ Node last2 = nm->mkNode(k, nextToLast, last);
+
+ if(N <= 2){
+ return last2;
+ } else{
+ Assert(N > 2);
+ Node prevRound = last2;
+ for(unsigned prevPos = N-2; prevPos > 0; --prevPos){
+ unsigned currPos = prevPos-1;
+ Node curr = rePairAssocCommutativeOperators(n[currPos]);
+ Node round = nm->mkNode(k, curr, prevRound);
+ prevRound = round;
+ }
+ return prevRound;
+ }
+}
+
+Node RePairAssocCommutativeOperators::case_other(TNode n){
+ if(n.isConst() || n.isVar()){
+ return n;
+ }
+
+ NodeBuilder<> nb(n.getKind());
+
+ if(n.getMetaKind() == kind::metakind::PARAMETERIZED) {
+ nb << n.getOperator();
+ }
+
+ // Remove the ITEs from the children
+ for(TNode::const_iterator i = n.begin(), end = n.end(); i != end; ++i) {
+ Node newChild = rePairAssocCommutativeOperators(*i);
+ nb << newChild;
+ }
+
+ Node result = (Node)nb;
+ return result;
+}
+
+}/* util namespace */
+}/* CVC4 namespace */
diff --git a/src/util/nary_builder.h b/src/util/nary_builder.h
new file mode 100644
index 000000000..ceaa44e77
--- /dev/null
+++ b/src/util/nary_builder.h
@@ -0,0 +1,38 @@
+
+#include "cvc4_private.h"
+
+#pragma once
+
+#include <vector>
+#include "expr/node.h"
+
+namespace CVC4{
+namespace util {
+
+class NaryBuilder {
+public:
+ static Node mkAssoc(Kind k, const std::vector<Node>& children);
+ static Node zeroArity(Kind k);
+};/* class NaryBuilder */
+
+class RePairAssocCommutativeOperators {
+public:
+ RePairAssocCommutativeOperators();
+ ~RePairAssocCommutativeOperators();
+
+ Node rePairAssocCommutativeOperators(TNode n);
+
+ static bool isAssociateCommutative(Kind k);
+
+ size_t size() const;
+ void clear();
+private:
+ Node case_assoccomm(TNode n);
+ Node case_other(TNode n);
+
+ typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
+ NodeMap d_cache;
+};/* class RePairAssocCommutativeOperators */
+
+}/* util namespace */
+}/* CVC4 namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback