diff options
Diffstat (limited to 'src/theory/sets')
-rw-r--r-- | src/theory/sets/theory_sets_rels.cpp | 35 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_rels.h | 1 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_rewriter.cpp | 101 |
3 files changed, 1 insertions, 136 deletions
diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp index 29cd492c7..ebfa6f8bb 100644 --- a/src/theory/sets/theory_sets_rels.cpp +++ b/src/theory/sets/theory_sets_rels.cpp @@ -1670,41 +1670,6 @@ typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFuncti } } - - Node TheorySetsRels::mkAnd( std::vector<TNode>& conjunctions ) { - Assert(conjunctions.size() > 0); - std::set<TNode> all; - - for (unsigned i = 0; i < conjunctions.size(); ++i) { - TNode t = conjunctions[i]; - if (t.getKind() == kind::AND) { - for(TNode::iterator child_it = t.begin(); - child_it != t.end(); ++child_it) { - Assert((*child_it).getKind() != kind::AND); - all.insert(*child_it); - } - } - else { - all.insert(t); - } - } - Assert(all.size() > 0); - if (all.size() == 1) { - // All the same, or just one - return conjunctions[0]; - } - - NodeBuilder<> conjunction(kind::AND); - std::set<TNode>::const_iterator it = all.begin(); - std::set<TNode>::const_iterator it_end = all.end(); - while (it != it_end) { - conjunction << *it; - ++ it; - } - - return conjunction; - }/* mkAnd() */ - void TheorySetsRels::printNodeMap(const char* fst, const char* snd, const NodeMap& map) diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h index a95948bc7..161b5195e 100644 --- a/src/theory/sets/theory_sets_rels.h +++ b/src/theory/sets/theory_sets_rels.h @@ -185,7 +185,6 @@ private: bool areEqual( Node a, Node b ); Node getRepresentative( Node t ); bool exists( std::vector<Node>&, Node ); - Node mkAnd( std::vector< TNode >& assumptions ); inline void addToMembershipDB( Node, Node, Node ); static void printNodeMap(const char* fst, const char* snd, diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp index 17f001a55..a3f1f9893 100644 --- a/src/theory/sets/theory_sets_rewriter.cpp +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -25,104 +25,6 @@ namespace CVC4 { namespace theory { namespace sets { -typedef std::set<TNode> Elements; -typedef std::unordered_map<TNode, Elements, TNodeHashFunction> SettermElementsMap; - -struct FlattenedNodeTag {}; -typedef expr::Attribute<FlattenedNodeTag, bool> flattened; - - -/** - * flattenNode looks for children of same kind, and if found merges - * them into the parent. - * - * It simultaneously handles a couple of other optimizations: - * - trivialNode - if found during exploration, return that node itself - * (like in case of OR, if "true" is found, makes sense to replace - * whole formula with "true") - * - skipNode - as name suggests, skip them - * (like in case of OR, you may want to skip any "false" nodes found) - * - * Use a null node if you want to ignore any of the optimizations. - */ -RewriteResponse flattenNode(TNode n, TNode trivialNode, TNode skipNode) -{ - if(n.hasAttribute(flattened()) && n.getAttribute(flattened())) { - return RewriteResponse(REWRITE_DONE, n); - } - - typedef std::unordered_set<TNode, TNodeHashFunction> node_set; - - node_set visited; - visited.insert(skipNode); - - std::vector<TNode> toProcess; - toProcess.push_back(n); - - Kind k = n.getKind(); - typedef std::vector<TNode> ChildList; - ChildList childList; //TNode should be fine, since 'n' is still there - - Debug("sets-rewrite-flatten") << "[sets-rewrite-flatten] " << n << std::endl; - for (unsigned i = 0; i < toProcess.size(); ++ i) { - TNode current = toProcess[i]; - Debug("sets-rewrite-flatten") << "[sets-rewrite-flatten] > Processing " << current << std::endl; - for(unsigned j = 0, j_end = current.getNumChildren(); j < j_end; ++ j) { - TNode child = current[j]; - if(visited.find(child) != visited.end()) { - continue; - } else if(child == trivialNode) { - return RewriteResponse(REWRITE_DONE, trivialNode); - } else { - visited.insert(child); - if(child.getKind() == k) { - toProcess.push_back(child); - } else { - childList.push_back(child); - } - } - } - } - if (childList.size() == 0) return RewriteResponse(REWRITE_DONE, skipNode); - if (childList.size() == 1) return RewriteResponse(REWRITE_AGAIN, childList[0]); - - sort(childList.begin(), childList.end()); - - /* Make sure we are under number of children possible in a node */ - NodeManager* nodeManager = NodeManager::currentNM(); - static const unsigned MAX_CHILDREN = (1u << __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN ) - 1; - AlwaysAssert(childList.size() < MAX_CHILDREN, "do not support formulas this big"); - - ChildList::iterator cur = childList.begin(), en = childList.end(); - Node ret = (*cur); - ++cur; - while( cur != en ) { - ret = nodeManager->mkNode(k, ret, *cur); - ret.setAttribute(flattened(), true); - ++cur; - } - Trace("sets-postrewrite") << "flatten Sets::postRewrite returning " << ret << std::endl; - if(ret != n) { - return RewriteResponse(REWRITE_AGAIN, ret); // again for constants - } else { - return RewriteResponse(REWRITE_DONE, ret); - } - // if (childList.size() < MAX_CHILDREN) { - // Node retNode = nodeManager->mkNode(k, childList); - // return RewriteResponse(REWRITE_DONE, retNode); - // } else { - // Assert(childList.size() < size_t(MAX_CHILDREN) * size_t(MAX_CHILDREN) ); - // NodeBuilder<> nb(k); - // ChildList::iterator cur = childList.begin(), next, en = childList.end(); - // while( cur != en ) { - // next = min(cur + MAX_CHILDREN, en); - // nb << (nodeManager->mkNode(k, ChildList(cur, next) )); - // cur = next; - // } - // return RewriteResponse(REWRITE_DONE, nb.constructNode()); - // } -} - bool checkConstantMembership(TNode elementTerm, TNode setTerm) { if(setTerm.getKind() == kind::EMPTYSET) { @@ -543,9 +445,8 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { default: break; - }//switch(node.getKind()) + } - // This default implementation return RewriteResponse(REWRITE_DONE, node); } |