From: Andrew Reynolds Date: Fri, 17 Aug 2018 19:18:16 +0000 (-0500) Subject: Remove miscellaneous unused code (#2333) X-Git-Tag: cvc5-1.0.0~4761 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6d65aa41a7e218469e99f476259cccb08c4c46c1;p=cvc5.git Remove miscellaneous unused code (#2333) --- diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp index ac07e13fb..ae560c5e5 100644 --- a/src/theory/quantifiers/equality_query.cpp +++ b/src/theory/quantifiers/equality_query.cpp @@ -210,79 +210,6 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative(Node a, } } -void EqualityQueryQuantifiersEngine::flattenRepresentatives( std::map< TypeNode, std::vector< Node > >& reps ) { - //make sure internal representatives currently exist - for( std::map< TypeNode, std::vector< Node > >::iterator it = reps.begin(); it != reps.end(); ++it ){ - if( it->first.isSort() ){ - for( unsigned i=0; isecond.size(); i++ ){ - Node r = getInternalRepresentative( it->second[i], Node::null(), 0 ); - } - } - } - Trace("internal-rep-flatten") << "---Flattening representatives : " << std::endl; - for( std::map< TypeNode, std::map< Node, Node > >::iterator itt = d_int_rep.begin(); itt != d_int_rep.end(); ++itt ){ - for( std::map< Node, Node >::iterator it = itt->second.begin(); it != itt->second.end(); ++it ){ - Trace("internal-rep-flatten") << itt->first << " : irep( " << it->first << " ) = " << it->second << std::endl; - } - } - //store representatives for newly created terms - std::map< Node, Node > temp_rep_map; - - bool success; - do { - success = false; - for( std::map< TypeNode, std::map< Node, Node > >::iterator itt = d_int_rep.begin(); itt != d_int_rep.end(); ++itt ){ - for( std::map< Node, Node >::iterator it = itt->second.begin(); it != itt->second.end(); ++it ){ - if( it->second.getKind()==APPLY_UF && it->second.getType().isSort() ){ - Node ni = it->second; - std::vector< Node > cc; - cc.push_back( it->second.getOperator() ); - bool changed = false; - for( unsigned j=0; jsecond.find( r )==itt->second.end() ){ - Assert( temp_rep_map.find( r )!=temp_rep_map.end() ); - r = temp_rep_map[r]; - } - if( r==ni ){ - //found sub-term as instance - Trace("internal-rep-flatten-debug") << "...Changed " << it->second << " to subterm " << ni[j] << std::endl; - itt->second[it->first] = ni[j]; - changed = false; - success = true; - break; - }else{ - Node ir = itt->second[r]; - cc.push_back( ir ); - if( ni[j]!=ir ){ - changed = true; - } - } - }else{ - changed = false; - break; - } - } - if( changed ){ - Node n = NodeManager::currentNM()->mkNode( APPLY_UF, cc ); - Trace("internal-rep-flatten-debug") << "...Changed " << it->second << " to " << n << std::endl; - success = true; - itt->second[it->first] = n; - temp_rep_map[n] = it->first; - } - } - } - } - }while( success ); - Trace("internal-rep-flatten") << "---After flattening : " << std::endl; - for( std::map< TypeNode, std::map< Node, Node > >::iterator itt = d_int_rep.begin(); itt != d_int_rep.end(); ++itt ){ - for( std::map< Node, Node >::iterator it = itt->second.begin(); it != itt->second.end(); ++it ){ - Trace("internal-rep-flatten") << itt->first << " : irep( " << it->first << " ) = " << it->second << std::endl; - } - } -} - eq::EqualityEngine* EqualityQueryQuantifiersEngine::getEngine(){ return d_qe->getActiveEqualityEngine(); } diff --git a/src/theory/quantifiers/equality_query.h b/src/theory/quantifiers/equality_query.h index a9a3cb185..8f836f9c6 100644 --- a/src/theory/quantifiers/equality_query.h +++ b/src/theory/quantifiers/equality_query.h @@ -114,8 +114,6 @@ class EqualityQueryQuantifiersEngine : public EqualityQuery Node getInstance( Node n, const std::vector< Node >& eqc, std::unordered_map& cache ); /** get score */ int getRepScore( Node n, Node f, int index, TypeNode v_tn ); - /** flatten representatives */ - void flattenRepresentatives( std::map< TypeNode, std::vector< Node > >& reps ); }; /* EqualityQueryQuantifiersEngine */ }/* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp index 6763a0ad3..81ecf9e77 100644 --- a/src/theory/quantifiers/fmf/model_engine.cpp +++ b/src/theory/quantifiers/fmf/model_engine.cpp @@ -166,11 +166,6 @@ bool ModelEngine::optOneQuantPerRound(){ int ModelEngine::checkModel(){ FirstOrderModel* fm = d_quantEngine->getModel(); - //flatten the representatives - //Trace("model-engine-debug") << "Flattening representatives...." << std::endl; - // d_quantEngine->getEqualityQuery()->flattenRepresentatives( - // fm->getRepSet()->d_type_reps ); - //for debugging, setup for (std::map >::iterator it = fm->getRepSetPtr()->d_type_reps.begin(); diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 3006a07bf..02c9aedf5 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -1870,33 +1870,6 @@ bool QuantConflictFind::areMatchDisequal( TNode n1, TNode n2 ) { //} } -//-------------------------------------------------- handling assertions / eqc - -void QuantConflictFind::assertNode( Node q ) { - /* - if( d_quantEngine->hasOwnership( q, this ) ){ - Trace("qcf-proc") << "QCF : assertQuantifier : "; - debugPrintQuant("qcf-proc", q); - Trace("qcf-proc") << std::endl; - } - */ -} - -/** new node */ -void QuantConflictFind::newEqClass( Node n ) { - -} - -/** merge */ -void QuantConflictFind::merge( Node a, Node b ) { - -} - -/** assert disequal */ -void QuantConflictFind::assertDisequal( Node a, Node b ) { - -} - //-------------------------------------------------- check function bool QuantConflictFind::needsCheck( Theory::Effort level ) { diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index e4eefe9ad..d76495b52 100644 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -236,14 +236,6 @@ public: void registerQuantifier(Node q) override; public: - /** assert quantifier */ - void assertNode(Node q) override; - /** new node */ - void newEqClass( Node n ); - /** merge */ - void merge( Node a, Node b ); - /** assert disequal */ - void assertDisequal( Node a, Node b ); /** needs check */ bool needsCheck(Theory::Effort level) override; /** reset round */ diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 37451b776..cff14e0c3 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -32,25 +32,6 @@ namespace CVC4 { namespace theory { namespace quantifiers { -bool QuantifiersRewriter::isClause( Node n ){ - if( isLiteral( n ) ){ - return true; - }else if( n.getKind()==NOT ){ - return isCube( n[0] ); - }else if( n.getKind()==OR ){ - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - if( !isClause( n[i] ) ){ - return false; - } - } - return true; - }else if( n.getKind()==IMPLIES ){ - return isCube( n[0] ) && isClause( n[1] ); - }else{ - return false; - } -} - bool QuantifiersRewriter::isLiteral( Node n ){ switch( n.getKind() ){ case NOT: @@ -73,23 +54,6 @@ bool QuantifiersRewriter::isLiteral( Node n ){ return true; } -bool QuantifiersRewriter::isCube( Node n ){ - if( isLiteral( n ) ){ - return true; - }else if( n.getKind()==NOT ){ - return isClause( n[0] ); - }else if( n.getKind()==AND ){ - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - if( !isCube( n[i] ) ){ - return false; - } - } - return true; - }else{ - return false; - } -} - void QuantifiersRewriter::addNodeToOrBuilder( Node n, NodeBuilder<>& t ){ if( n.getKind()==OR ){ for( int i=0; i<(int)n.getNumChildren(); i++ ){ diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index bd0192d9e..963e73701 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -32,9 +32,7 @@ class QuantifiersRewriter { private: static int getPurifyIdLit2( Node n, std::map< Node, int >& visited ); public: - static bool isClause( Node n ); static bool isLiteral( Node n ); - static bool isCube( Node n ); private: static bool addCheckElimChild( std::vector< Node >& children, Node c, Kind k, std::map< Node, bool >& lit_pol, bool& childrenChanged ); static void addNodeToOrBuilder( Node n, NodeBuilder<>& t ); 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& conjunctions ) { - Assert(conjunctions.size() > 0); - std::set 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::const_iterator it = all.begin(); - std::set::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 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 Elements; -typedef std::unordered_map SettermElementsMap; - -struct FlattenedNodeTag {}; -typedef expr::Attribute 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 node_set; - - node_set visited; - visited.insert(skipNode); - - std::vector toProcess; - toProcess.push_back(n); - - Kind k = n.getKind(); - typedef std::vector 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); }