summaryrefslogtreecommitdiff
path: root/src/theory/sets
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/sets')
-rw-r--r--src/theory/sets/theory_sets_rels.cpp35
-rw-r--r--src/theory/sets/theory_sets_rels.h1
-rw-r--r--src/theory/sets/theory_sets_rewriter.cpp101
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);
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback