From 59309adbc716027a19a5077b62fadb2f3fddbf18 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Wed, 4 Jan 2012 06:14:29 +0000 Subject: [PATCH] Improvement. Replace difficulty and printing implementations with one that uses an iterator. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1465 e59a4935-1847-0410-ae03-e826735625c1 --- src/AST/ASTInternal.h | 4 +- src/AST/ASTNode.cpp | 14 +++- src/AST/ASTNode.h | 3 + src/STPManager/DifficultyScore.h | 135 +++++++++++++++---------------- src/STPManager/NodeIterator.h | 93 +++++++++++++++++++++ src/STPManager/STP.cpp | 2 +- src/STPManager/STPManager.cpp | 48 ++++------- src/STPManager/STPManager.h | 43 ++++++++-- 8 files changed, 225 insertions(+), 117 deletions(-) create mode 100644 src/STPManager/NodeIterator.h diff --git a/src/AST/ASTInternal.h b/src/AST/ASTInternal.h index e4bfb63..56e2149 100644 --- a/src/AST/ASTInternal.h +++ b/src/AST/ASTInternal.h @@ -55,6 +55,8 @@ namespace BEEV * Protected Data * ****************************************************************/ + mutable uint8_t iteration; + //reference counting for garbage collection unsigned int _ref_count; @@ -128,7 +130,7 @@ namespace BEEV ASTInternal(int nodenum = 0) : _ref_count(0), _kind(UNDEFINED), _node_num(nodenum), - _index_width(0), _value_width(0) + _index_width(0), _value_width(0), iteration(0) { } diff --git a/src/AST/ASTNode.cpp b/src/AST/ASTNode.cpp index c5bc09c..0a268f5 100644 --- a/src/AST/ASTNode.cpp +++ b/src/AST/ASTNode.cpp @@ -15,7 +15,19 @@ ********************************************************************/ namespace BEEV { - // Constructor; + uint8_t ASTNode::getIteration() const + { + return _int_node_ptr->iteration; + } + + void ASTNode::setIteration(uint8_t v) const + { + _int_node_ptr->iteration = v; + } + + + + // Constructor; // // creates a new pointer, increments refcount of pointed-to object. ASTNode::ASTNode(ASTInternal *in) : diff --git a/src/AST/ASTNode.h b/src/AST/ASTNode.h index 84bca7e..60ef09a 100644 --- a/src/AST/ASTNode.h +++ b/src/AST/ASTNode.h @@ -73,6 +73,9 @@ namespace BEEV * Public Member Functions * ****************************************************************/ + uint8_t getIteration() const; + void setIteration(uint8_t v) const; + // Default constructor. ASTNode() :_int_node_ptr(NULL) {}; diff --git a/src/STPManager/DifficultyScore.h b/src/STPManager/DifficultyScore.h index 5392a8e..b647b56 100644 --- a/src/STPManager/DifficultyScore.h +++ b/src/STPManager/DifficultyScore.h @@ -4,88 +4,79 @@ #include "../AST/AST.h" #include "../AST/AST.h" #include "../AST/ASTKind.h" +#include +#include "../STPManager/NodeIterator.h" // estimate how difficult that input is to solve based on some simple rules. namespace BEEV { -struct DifficultyScore -{ -private: - // maps from nodeNumber to the previously calculated difficulty score.. - map cache; - - static bool isLikeDivision(const Kind& k) - { - return k == BVMULT || k == BVDIV || k == BVMOD || k == SBVDIV || k == SBVREM || k == SBVMOD; - } - - int visit(const ASTNode& b, ASTNodeSet& visited) - { - if (b.isAtom()) - return 0; - - ASTNodeSet::iterator it; - - if ((it = visited.find(b)) != visited.end()) - return 0; // already included. - - visited.insert(b); - - const Kind k =b.GetKind(); - - // These scores are approximately the number of AIG nodes created when - // no input values are known. - int score= 0; - if (k == BVMULT) - score = (5 * b.GetValueWidth() * b.GetValueWidth() ); - else if (k == BVMOD) - score = (15 * b.GetValueWidth() * b.GetValueWidth() ); - else if (isLikeDivision(k)) - score = (20 * b.GetValueWidth() * b.GetValueWidth() ); - else if (k == BVCONCAT || k == BVEXTRACT || k == NOT) - {} // no harder. - else if (k == EQ || k == BVGE || k == BVGT|| k == BVSGE || k == BVSGT ) - { - // without getting the width of the child it'd always be 2. - score = std::max(b[0].GetValueWidth(),1u) * (b.Degree()); - } - else if (k == BVSUB) - { + struct DifficultyScore + { + private: + int + eval(const ASTNode& b) + { + const Kind k = b.GetKind(); + + // These scores are approximately the number of AIG nodes created when + // no input values are known. + int score = 0; + if (k == BVMULT) + score = (5 * b.GetValueWidth() * b.GetValueWidth()); + else if (k == BVMOD) + score = (15 * b.GetValueWidth() * b.GetValueWidth()); + else if (isLikeDivision(k)) + score = (20 * b.GetValueWidth() * b.GetValueWidth()); + else if (k == BVCONCAT || k == BVEXTRACT || k == NOT) + { + } // no harder. + else if (k == EQ || k == BVGE || k == BVGT || k == BVSGE || k == BVSGT) + { + // without getting the width of the child it'd always be 2. + score = std::max(b[0].GetValueWidth(), 1u) * (b.Degree()); + } + else if (k == BVSUB) + { // We convert subtract to a + (-b), we want the difficulty scores to be same. - score = std::max(b[0].GetValueWidth(),1u) * 3; - } - else - { - score = std::max(b.GetValueWidth(),1u) * (b.Degree()); - } + score = std::max(b[0].GetValueWidth(), 1u) * 3; + } + else + { + score = std::max(b.GetValueWidth(), 1u) * (b.Degree()); + } + return score; + } + + static bool + isLikeDivision(const Kind& k) + { + return k == BVMULT || k == BVDIV || k == BVMOD || k == SBVDIV || k == SBVREM || k == SBVMOD; + } + + // maps from nodeNumber to the previously calculated difficulty score.. + map cache; - const ASTVec& c = b.GetChildren(); - ASTVec::const_iterator itC = c.begin(); - ASTVec::const_iterator itendC = c.end(); - for (; itC != itendC; itC++) - { - score += visit(*itC, visited); - } + public: - return score; - } + int + score(const ASTNode& top) + { + if (cache.find(top.GetNodeNum()) != cache.end()) + return cache.find(top.GetNodeNum())->second; -public: - int score(const ASTNode& top) - { - if (cache.find(top.GetNodeNum()) != cache.end()) - return cache.find(top.GetNodeNum())->second; + NonAtomIterator ni(top, top.GetSTPMgr()->ASTUndefined, *top.GetSTPMgr()); + ASTNode current; + int result = 0; + while ((current = ni.next()) != ni.end()) + result += eval(current); - ASTNodeSet visited; - int result = visit(top,visited); - cache.insert(make_pair(top.GetNodeNum(), result)); - return result; - } -}; -}; + cache.insert(make_pair(top.GetNodeNum(), result)); + return result; + } + }; +} +; #endif /* DIFFICULTYSCORE_H_ */ - - diff --git a/src/STPManager/NodeIterator.h b/src/STPManager/NodeIterator.h new file mode 100644 index 0000000..78f4a2e --- /dev/null +++ b/src/STPManager/NodeIterator.h @@ -0,0 +1,93 @@ +#ifndef NODEITERATOR_H_ +#define NODEITERATOR_H_ + +#include + +namespace BEEV +{ + // Returns each node once, then returns the sentinal. + // NB if the sentinel is contained in the node that's passed, then it'll be wrong. + class NodeIterator + { + stack toVisit; + + const ASTNode& sentinal; + uint8_t iteration; + + NodeIterator( const NodeIterator& other ); // non copyable + NodeIterator& operator=( const NodeIterator& ); // non copyable + + public: + NodeIterator(const ASTNode &n, const ASTNode &_sentinal, STPMgr& stp) : + sentinal(_sentinal), iteration(stp.getNextIteration()) + { + toVisit.push(n); + } + + ASTNode + next() + { + ASTNode result = sentinal; + + while (true) + { + if (toVisit.empty()) + return sentinal; + + result = toVisit.top(); + toVisit.pop(); + + if (!ok(result)) + continue; // Not OK to investigate. + + if (result.getIteration() != iteration) + break; // not visited, DONE! + } + + if (result == sentinal) + return result; + + result.setIteration(iteration); + + const ASTVec& c = result.GetChildren(); + ASTVec::const_iterator itC = c.begin(); + ASTVec::const_iterator itendC = c.end(); + for (; itC != itendC; itC++) + { + if (itC->getIteration() == iteration) + continue; // already examined. + toVisit.push(*itC); + } + return result; + } + + ASTNode + end() + { + return sentinal; + } + + virtual bool + ok(const ASTNode n) + { + return true; + } + }; + + // Iterator that omits return atoms. + class NonAtomIterator : public NodeIterator + { + virtual bool + ok(const ASTNode& n) + { + return !n.isAtom(); + } + + public: + NonAtomIterator(const ASTNode &n, const ASTNode &uf, STPMgr& stp) : + NodeIterator(n, uf, stp) + { + } + }; +}; +#endif /* NODEITERATOR_H_ */ diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp index 9eec152..9c71222 100644 --- a/src/STPManager/STP.cpp +++ b/src/STPManager/STP.cpp @@ -200,7 +200,7 @@ namespace BEEV { DifficultyScore difficulty; if (bm->UserFlags.stats_flag) - cerr << "Difficulty Initially:" << difficulty.score(original_input) << endl; + cerr << "Difficulty Initially:" << difficulty.score(original_input) << endl; // A heap object so I can easily control its lifetime. BVSolver* bvSolver = new BVSolver(bm, simp); diff --git a/src/STPManager/STPManager.cpp b/src/STPManager/STPManager.cpp index 750f542..e47541a 100644 --- a/src/STPManager/STPManager.cpp +++ b/src/STPManager/STPManager.cpp @@ -1,6 +1,6 @@ // -*- c++ -*- /******************************************************************** - * AUTHORS: Vijay Ganesh + * AUTHORS: Vijay Ganesh, Trevor Hansen * * BEGIN DATE: November, 2005 * @@ -15,6 +15,7 @@ #include #include "../STPManager/STPManager.h" #include "../printer/SMTLIBPrinter.h" +#include "NodeIterator.h" namespace BEEV { @@ -613,44 +614,23 @@ namespace BEEV if (!UserFlags.stats_flag) return; - StatInfoSet.clear(); - //print node size: - - cout << "[" << GetRunTimes()->getDifference() << "]" << "Printing: " << c; + cout << "[" << GetRunTimes()->getDifference() << "]" << c; if (UserFlags.print_nodes_flag) - { - //a.PL_Print(cout,0); - //cout << endl; cout << a << endl; - } - cout << "Node size is: "; - cout << NodeSize(a) << endl; + + cout << "Node size is: " << NodeSize(a) << endl; } - unsigned int STPMgr::NodeSize(const ASTNode& a, bool clearStatInfo) + unsigned int STPMgr::NodeSize(const ASTNode& a) { - if (clearStatInfo) - StatInfoSet.clear(); - - ASTNodeSet::iterator it; - if ((it = StatInfoSet.find(a)) != StatInfoSet.end()) - //has already been counted - return 0; - - //record that you have seen this node already - StatInfoSet.insert(a); - // cout << "Number of bytes per Node is: "; - // cout << sizeof(*(a._int_node_ptr)) << endl; - - //leaf node has a size of 1 - if (a.Degree() == 0) - return 1; - - unsigned newn = 1; - const ASTVec& c = a.GetChildren(); - for (ASTVec::const_iterator it = c.begin(), itend = c.end(); it != itend; it++) - newn += NodeSize(*it); - return newn; + unsigned int result = 0; + NodeIterator ni(a, ASTUndefined, *this); + ASTNode current; + while ((current = ni.next()) != ni.end()) + { + result++; + } + return result; } bool STPMgr::VarSeenInTerm(const ASTNode& var, const ASTNode& term) diff --git a/src/STPManager/STPManager.h b/src/STPManager/STPManager.h index 83f6b0b..5c3a8b4 100644 --- a/src/STPManager/STPManager.h +++ b/src/STPManager/STPManager.h @@ -79,6 +79,37 @@ namespace BEEV //frequently used nodes ASTNode ASTFalse, ASTTrue, ASTUndefined; + + uint8_t last_iteration; + + // No nodes should already have the iteration number that is returned from here. + // This never returns zero. + uint8_t getNextIteration() + { + if (last_iteration == 255) + { + resetIteration(); + last_iteration = 0; + } + + uint8_t result = ++last_iteration; + assert(result != 0); + return result; + } + + // Detauls the iteration count back to zero. + void resetIteration() + { + for (ASTInteriorSet::iterator it =_interior_unique_table.begin(); it != _interior_unique_table.end(); it++ ) + {(*it)->iteration = 0;} + + for (ASTSymbolSet ::iterator it =_symbol_unique_table.begin(); it != _symbol_unique_table.end(); it++ ) + {(*it)->iteration = 0;} + + for (ASTBVConstSet:: iterator it =_bvconst_unique_table.begin(); it != _bvconst_unique_table.end(); it++ ) + {(*it)->iteration = 0;} + } + private: // Stack of Logical Context. each entry in the stack is a logical @@ -92,9 +123,6 @@ namespace BEEV // Memo table that tracks terms already seen ASTNodeMap TermsAlreadySeenMap; - //Map for computing ASTNode stats - ASTNodeSet StatInfoSet; - // The query for the current logical context. ASTNode _current_query; @@ -186,7 +214,9 @@ namespace BEEV _interior_unique_table(), UserFlags(), _symbol_count(0), - CNFFileNameCounter(0) + CNFFileNameCounter(0), + last_iteration(0) + { _max_node_num = 0; Begin_RemoveWrites = false; @@ -230,9 +260,7 @@ namespace BEEV return _max_node_num; } - //reports node size. Second arg is "clearstatinfo", whatever that - //is. - unsigned int NodeSize(const ASTNode& a, bool t = false); + unsigned int NodeSize(const ASTNode& a); /**************************************************************** * Simplifying create formula functions * @@ -436,7 +464,6 @@ namespace BEEV NodeLetVarMap1.clear(); PLPrintNodeSet.clear(); AlreadyPrintedSet.clear(); - StatInfoSet.clear(); TermsAlreadySeenMap.clear(); NodeLetVarVec.clear(); ListOfDeclaredVars.clear(); -- 2.47.3