* Protected Data *
****************************************************************/
+ mutable uint8_t iteration;
+
//reference counting for garbage collection
unsigned int _ref_count;
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)
{
}
********************************************************************/
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) :
* Public Member Functions *
****************************************************************/
+ uint8_t getIteration() const;
+ void setIteration(uint8_t v) const;
+
// Default constructor.
ASTNode() :_int_node_ptr(NULL) {};
#include "../AST/AST.h"
#include "../AST/AST.h"
#include "../AST/ASTKind.h"
+#include <list>
+#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<int, int> 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<int, int> 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_ */
-
-
--- /dev/null
+#ifndef NODEITERATOR_H_
+#define NODEITERATOR_H_
+
+#include <stack>
+
+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<ASTNode> 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_ */
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);
// -*- c++ -*-
/********************************************************************
- * AUTHORS: Vijay Ganesh
+ * AUTHORS: Vijay Ganesh, Trevor Hansen
*
* BEGIN DATE: November, 2005
*
#include <cmath>
#include "../STPManager/STPManager.h"
#include "../printer/SMTLIBPrinter.h"
+#include "NodeIterator.h"
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)
//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
// 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;
_interior_unique_table(),
UserFlags(),
_symbol_count(0),
- CNFFileNameCounter(0)
+ CNFFileNameCounter(0),
+ last_iteration(0)
+
{
_max_node_num = 0;
Begin_RemoveWrites = false;
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 *
NodeLetVarMap1.clear();
PLPrintNodeSet.clear();
AlreadyPrintedSet.clear();
- StatInfoSet.clear();
TermsAlreadySeenMap.clear();
NodeLetVarVec.clear();
ListOfDeclaredVars.clear();
projects / francis / stp.git / commitdiff