自学教程：C++ ASTNodeSet类代码示例

void LetizeNode(const ASTNode& n, ASTNodeSet& PLPrintNodeSet, bool smtlib1){  const Kind kind = n.GetKind();  if (kind == SYMBOL || kind == BVCONST || kind == FALSE || kind == TRUE)    return;  const ASTVec& c = n.GetChildren();  for (ASTVec::const_iterator it = c.begin(), itend = c.end(); it != itend;       it++)  {    const ASTNode& ccc = *it;    const Kind k = ccc.GetKind();    if (k == SYMBOL || k == BVCONST || k == FALSE || k == TRUE)      continue;    if (PLPrintNodeSet.find(ccc) == PLPrintNodeSet.end())    {      // If branch: if *it is not in NodeSet then,      //      // 1. add it to NodeSet      //      // 2. Letize its childNodes      PLPrintNodeSet.insert(ccc);      LetizeNode(ccc, PLPrintNodeSet, smtlib1);    }    else    {      // 0. Else branch: Node has been seen before      //      // 1. Check if the node has a corresponding letvar in the      // 1. NodeLetVarMap.      //      // 2. if no, then create a new var and add it to the      // 2. NodeLetVarMap      if ((!smtlib1 || ccc.GetType() == BITVECTOR_TYPE) &&          NodeLetVarMap.find(ccc) == NodeLetVarMap.end())      {        // Create a new symbol. Get some name. if it conflicts with a        // declared name, too bad.        int sz = NodeLetVarMap.size();        std::ostringstream oss;        oss << "?let_k_" << sz;        ASTNode CurrentSymbol = n.GetSTPMgr()->CreateSymbol(            oss.str().c_str(), n.GetIndexWidth(), n.GetValueWidth());        /* If for some reason the variable being created here is         * already declared by the user then the printed output will         * not be a legal input to the system. too bad. I refuse to         * check for this.  [Vijay is the author of this comment.]         */        NodeLetVarMap[ccc] = CurrentSymbol;        std::pair<ASTNode, ASTNode> node_letvar_pair(CurrentSymbol, ccc);        NodeLetVarVec.push_back(node_letvar_pair);      }    }  }} // end of LetizeNode()

// Adds to the dependency graph that n0 depends on the variables in n1.// It's not the transitive closure of the dependencies. Just the variables in the expression "n1".// This is only needed as long as all the substitution rules haven't been written through.  void  SubstitutionMap::buildDepends(const ASTNode& n0, const ASTNode& n1)  {    if (n0.GetKind() != SYMBOL)      return;    if (n1.isConstant())      return;    vector<Symbols*> av;    vars.VarSeenInTerm(vars.getSymbol(n1), rhs_visited, rhs, av);    sort(av.begin(), av.end());    for (int i = 0; i < av.size(); i++)      {      if (i != 0 && av[i] == av[i - 1])        continue; // Treat it like a set of Symbol* in effect.      ASTNodeSet* sym = (vars.TermsAlreadySeenMap.find(av[i])->second);      if (rhsAlreadyAdded.find(sym) != rhsAlreadyAdded.end())        continue;      rhsAlreadyAdded.insert(sym);      //cout << loopCount++ << " ";      //cout << "initial" << rhs.size() << " Adding: " <<sym->size();      rhs.insert(sym->begin(), sym->end());      //cout << "final:" << rhs.size();      //cout << "added:" << sym << endl;      }    assert(dependsOn.find(n0) == dependsOn.end());    dependsOn.insert(make_pair(n0, vars.getSymbol(n1)));  }

void STPMgr::printVarDeclsToStream(ostream& os, ASTNodeSet& ListOfDeclaredVars){  for (ASTNodeSet::iterator i = ListOfDeclaredVars.begin(),                            iend = ListOfDeclaredVars.end();       i != iend; i++)  {    stp::ASTNode a = *i;    switch (a.GetType())    {      case stp::BITVECTOR_TYPE:        a.PL_Print(os);        os << " : BITVECTOR(" << a.GetValueWidth() << ");" << endl;        break;      case stp::ARRAY_TYPE:        a.PL_Print(os);        os << " : ARRAY "           << "BITVECTOR(" << a.GetIndexWidth() << ") OF ";        os << "BITVECTOR(" << a.GetValueWidth() << ");" << endl;        break;      case stp::BOOLEAN_TYPE:        a.PL_Print(os);        os << " : BOOLEAN;" << endl;        break;      default:        stp::FatalError("vc_printDeclsToStream: Unsupported type", a);        break;    }  }} // printVarDeclsToStream

void printVarDeclsToStream(ASTNodeSet& symbols, ostream& os){	for (ASTNodeSet::const_iterator i = symbols.begin(), iend = symbols.end(); i			!= iend; i++)	{      const BEEV::ASTNode& a = *i;      os << "(declare-fun ";      // Should be a symbol.      assert(a.GetKind()== SYMBOL);      os << "|";      a.nodeprint(os);      os << "|";		switch (a.GetType())		{      case BEEV::BITVECTOR_TYPE:    	  os << " () (";    	  os << "_ BitVec " << a.GetValueWidth() << ")";        break;      case BEEV::ARRAY_TYPE:    	  os << " () (";    	  os << "Array (_ BitVec " << a.GetIndexWidth()  << ") (_ BitVec " << a.GetValueWidth() << ") )";        break;      case BEEV::BOOLEAN_TYPE:        os << " () Bool ";        break;      default:        BEEV::FatalError("printVarDeclsToStream: Unsupported type",a);        break;      }  	  os << ")/n";    }  } //printVarDeclsToStream

ASTNodeSet * VariablesInExpression::SetofVarsSeenInTerm(Symbols* symbol, bool& destruct){	assert(symbol != NULL);	SymbolPtrToNode::iterator it = TermsAlreadySeenMap.find(symbol);	if ( it != TermsAlreadySeenMap.end())		{		destruct = false;		return it->second;		}	SymbolPtrSet visited;	ASTNodeSet *symbols = new ASTNodeSet();	vector<Symbols*> av;	VarSeenInTerm(symbol,visited,*symbols,av);	for (size_t i =0; i < av.size();i++)	{		const ASTNodeSet& sym = *TermsAlreadySeenMap.find(av[i])->second;		symbols->insert(sym.begin(), sym.end());	}	destruct = true;	//TermsAlreadySeenMap.insert(make_pair(symbol,symbols));	return symbols;}

bool containsArrayOps(const ASTNode& n, ASTNodeSet& visited){	if (visited.find(n) != visited.end())		return false;	if (n.GetType() == ARRAY_TYPE)		return true;	for (int i =0; i < n.Degree();i++)		if (containsArrayOps(n[i],visited))			return true;	visited.insert(n);	return false;}

// If n0 is replaced by n1 in the substitution map. Will it cause a loop?// i.e. will the dependency graph be an acyclic graph still.// For example, if we have x = F(y,z,w), it would make the substitutionMap loop// if there's already z = F(x).bool SubstitutionMap::loops(const ASTNode& n0, const ASTNode& n1){  if (n0.GetKind() != SYMBOL)    return false; // sometimes this function is called with constants on the                  // lhs.  if (n1.isConstant())    return false; // constants contain no variables. Can't loop.  // We are adding an edge FROM n0, so unless there is already an edge TO n0,  // there is no change it can loop. Unless adding this would add a TO and FROM  // edge.  if (rhs.find(n0) == rhs.end())  {    return vars.VarSeenInTerm(n0, n1);  }  if (n1.GetKind() == SYMBOL && dependsOn.find(n1) == dependsOn.end())    return false; // The rhs is a symbol and doesn't appear.  if (debug_substn)    cout << loopCount++ << endl;  bool destruct = true;  ASTNodeSet* dependN = vars.SetofVarsSeenInTerm(n1, destruct);  if (debug_substn)  {    cout << n0 << " "         << n1.GetNodeNum(); //<< " Expression size:" << bm->NodeSize(n1,true);    cout << "Variables in expression: " << dependN->size() << endl;  }  set<ASTNode> depend(dependN->begin(), dependN->end());  if (destruct)    delete dependN;  set<ASTNode> visited;  loops_helper(depend, visited);  bool loops = visited.find(n0) != visited.end();  if (debug_substn)    cout << "Visited:" << visited.size() << "Loops:" << loops << endl;  return (loops);}

// Builds a set of the SYMBOLS that were found under the "term". The symbols are the union of "found" and// all the sets : TermsAlreadySeen(av[0]) union ... TermsAlreadySeen(av[n])".void VariablesInExpression::VarSeenInTerm(Symbols* term, SymbolPtrSet& visited,		ASTNodeSet& found, vector<Symbols*>& av) {	if (visited.find(term) != visited.end()) {		return;	}	if (term->isLeaf()) {		found.insert(term->found);		return;	}	visited.insert(term);	SymbolPtrToNode::const_iterator it;	if ((it = TermsAlreadySeenMap.find(term)) != TermsAlreadySeenMap.end()) {		// We've previously built the set of variables below this "symbols".		// It's not added into "found" because its sometimes 70k variables		// big, and if there are no other symbols discovered it's a terrible		// waste to create a copy of the set. Instead we store (in effect)		// a pointer to the set.		av.push_back(term);		return;	}	for (vector<Symbols*>::const_iterator it = term->children.begin(), itend =			term->children.end(); it != itend; it++) {		VarSeenInTerm(*it, visited, found, av);	}	return;}//End of VarSeenInTerm

  void buildListOfSymbols(const ASTNode& n, ASTNodeSet& visited,  		ASTNodeSet& symbols)  {  	if (visited.find(n) != visited.end())  		return; // already visited.  	visited.insert(n);  	if (n.GetKind() == SYMBOL)  	{  		symbols.insert(n);  	}  	for (unsigned i = 0; i < n.GetChildren().size(); i++)  		buildListOfSymbols(n[i], visited, symbols);  }

// Check that the transformations have occurred.void ArrayTransformer::assertTransformPostConditions(const ASTNode& term,                                                     ASTNodeSet& visited){  // I haven't measure whether this is the quickest way to do it?  std::pair<ASTNodeSet::iterator, bool> p = visited.insert(term);  if (!p.second)    return;  const Kind k = term.GetKind();  // Check the array reads / writes have been removed  assert(READ != k);  assert(WRITE != k);  // There should be no nodes left of type array.  assert(0 == term.GetIndexWidth());  const ASTVec& c = term.GetChildren();  ASTVec::const_iterator it = c.begin();  const ASTVec::const_iterator itend = c.end();  for (; it != itend; it++)  {    assertTransformPostConditions(*it, visited);  }} 

// Take the transitive closure of the varsToCheck. Storing the result in// visited.void SubstitutionMap::loops_helper(const set<ASTNode>& varsToCheck,                                   set<ASTNode>& visited){  set<ASTNode>::const_iterator visitedIt = visited.begin();  set<ASTNode> toVisit;  vector<ASTNode> visitedN;  // for each variable.  for (set<ASTNode>::const_iterator varIt = varsToCheck.begin();       varIt != varsToCheck.end(); varIt++)  {    while (visitedIt != visited.end() && *visitedIt < *varIt)      visitedIt++;    if ((visitedIt != visited.end()) && *visitedIt == *varIt)      continue;    visitedN.push_back(*varIt);    DependsType::iterator it;    if ((it = dependsOn.find(*varIt)) != dependsOn.end())    {      Symbols* s = it->second;      bool destruct;      ASTNodeSet* varsSeen = vars.SetofVarsSeenInTerm(s, destruct);      toVisit.insert(varsSeen->begin(), varsSeen->end());      if (destruct)        delete varsSeen;    }  }  visited.insert(visitedN.begin(), visitedN.end());  visitedN.clear();  if (toVisit.size() != 0)    loops_helper(toVisit, visited);}

    bool    ConstantBitPropagation::checkAtFixedPoint(const ASTNode& n, ASTNodeSet & visited)    {      if (status == CONFLICT)        return true; // can't do anything.      if (visited.find(n) != visited.end())        return true;      visited.insert(n);      // get the current for the children.      vector<FixedBits> childrenFixedBits;      childrenFixedBits.reserve(n.GetChildren().size());      // get a copy of the current fixing from the cache.      for (unsigned i = 0; i < n.GetChildren().size(); i++)        {          childrenFixedBits.push_back(*getCurrentFixedBits(n[i]));        }      FixedBits current = *getCurrentFixedBits(n);      FixedBits newBits = *getUpdatedFixedBits(n);      assert(FixedBits::equals(newBits, current));      for (int i = 0; i < n.Degree(); i++)        {          if (!FixedBits::equals(*getUpdatedFixedBits(n[i]),              childrenFixedBits[i]))            {              cerr << "Not fixed point";              assert(false);            }          checkAtFixedPoint(n[i], visited);        }      return true;    }

/* Maintains a set of nodes that have already been seen. So that deeply shared * AND,OR operations are not * flattened multiple times. */void FlattenKindNoDuplicates(const Kind k, const ASTVec& children,                             ASTVec& flat_children,                             ASTNodeSet& alreadyFlattened){  const ASTVec::const_iterator ch_end = children.end();  for (ASTVec::const_iterator it = children.begin(); it != ch_end; it++)  {    const Kind ck = it->GetKind();    if (k == ck)    {      if (alreadyFlattened.find(*it) == alreadyFlattened.end())      {        alreadyFlattened.insert(*it);        FlattenKindNoDuplicates(k, it->GetChildren(), flat_children,                                alreadyFlattened);      }    }    else    {      flat_children.push_back(*it);    }  }}

void printSMTLIB1VarDeclsToStream(ASTNodeSet& symbols, ostream& os){	for (ASTNodeSet::const_iterator i = symbols.begin(), iend = symbols.end(); i			!= iend; i++)	{      const BEEV::ASTNode& a = *i;      // Should be a symbol.      assert(a.GetKind()== SYMBOL);		switch (a.GetType())		{      case BEEV::BITVECTOR_TYPE:        os << ":extrafuns (( ";        a.nodeprint(os);        os << " BitVec[" << a.GetValueWidth() << "]";        os << " ))" << endl;        break;      case BEEV::ARRAY_TYPE:        os << ":extrafuns (( ";        a.nodeprint(os);        os << " Array[" << a.GetIndexWidth();        os << ":" << a.GetValueWidth() << "] ))" << endl;        break;      case BEEV::BOOLEAN_TYPE:        os << ":extrapreds (( ";        a.nodeprint(os);        os << "))" << endl;        break;      default:        BEEV::FatalError("printVarDeclsToStream: Unsupported type",a);        break;      }    }  } //printVarDeclsToStream

  ASTNode  RemoveUnconstrained::topLevel_other(const ASTNode &n, Simplifier *simplifier)  {    if (n.GetKind() == SYMBOL)      return n; // top level is an unconstrained symbol/.    simplifier_convenient = simplifier;    ASTNodeSet noCheck; // We don't want to check some expensive nodes over and over again.    vector<MutableASTNode*> variable_array;    MutableASTNode* topMutable = MutableASTNode::build(n);    vector<MutableASTNode*> extracts;    topMutable->getDisjointExtractVariables(extracts);    if (extracts.size() > 0)      {          splitExtractOnly(extracts);      }    topMutable->getAllUnconstrainedVariables(variable_array);    for (int i =0; i < variable_array.size() ; i++)      {        // Don't make this is a reference. If the vector gets resized, it will point to        // memory that no longer contains the object.        MutableASTNode& muteNode = *variable_array[i];        const ASTNode var = muteNode.n;        assert(var.GetKind() == SYMBOL);        if (!muteNode.isUnconstrained())          continue;        MutableASTNode& muteParent = muteNode.getParent();        if (noCheck.find(muteParent.n) != noCheck.end())          {            continue;          }        vector <MutableASTNode*> mutable_children = muteParent.children;        //nb. The children might be dirty. i.e. not have substitutions written through them yet.        ASTVec children;        children.reserve(mutable_children.size());        for (int j = 0; j <mutable_children.size(); j++ )          children.push_back(mutable_children[j]->n);        const size_t numberOfChildren = children.size();        const Kind kind = muteNode.getParent().n.GetKind();        unsigned width = muteNode.getParent().n.GetValueWidth();        unsigned indexWidth = muteNode.getParent().n.GetIndexWidth();        ASTNode other;        MutableASTNode* muteOther;          if(numberOfChildren == 2)          {            if (children[0] != var)              {                other = children[0];                muteOther = mutable_children[0];              }            else              {                other = children[1];                muteOther = mutable_children[1];              }            if (kind != AND && kind != OR && kind != BVOR && kind != BVAND)              if (other == var)                continue; // Most rules don't like duplicate variables.          }        else          {            if (kind != AND && kind != OR && kind != BVOR && kind != BVAND)              {                  int found = 0;                  for (int i = 0; i < numberOfChildren; i++)                    {                      if (children[i] == var)                        found++;                   }                    if (found != 1)                      continue; // Most rules don't like duplicate variables.              }          }          /*          cout << i << " " << kind << " " << variable_array.size() <<  " " << mutable_children.size() << endl;          cout << "children[0]" << children[0] << endl;          cout << "children[1]" << children[1] << endl;          cout << muteParent.n << endl;           *///.........这里部分代码省略.........

void GDL_Print1(ostream& os, const ASTNode& n, hash_set<int>* alreadyOutput,                string (*annotate)(const ASTNode&)){  // check if this node has already been printed. If so return.  if (alreadyOutput->find(n.GetNodeNum()) != alreadyOutput->end())    return;  alreadyOutput->insert(n.GetNodeNum());  os << "node: { title:/"n" << n.GetNodeNum() << "/" label: /"";  switch (n.GetKind())  {    case SYMBOL:      n.nodeprint(os);      break;    case BITVECTOR:    case BVCONST:      outputBitVec(n, os);      break;    default:      os << _kind_names[n.GetKind()];  }  os << annotate(n);  os << "/"}" << endl;  // print the edges to each child.  const ASTVec ch = n.GetChildren();  const ASTVec::const_iterator itend = ch.end();  // If a node has the child 'TRUE' twice, we only want to output one TRUE node.  ASTNodeSet constantOutput;  int i = 0;  for (ASTVec::const_iterator it = ch.begin(); it < itend; it++)  {    std::stringstream label;    if (!isCommutative(n.GetKind()))      label << " label:/"" << i << "/"";    if (it->isConstant())    {      std::stringstream ss;      ss << n.GetNodeNum() << "_" << it->GetNodeNum();      if (constantOutput.end() == constantOutput.find(*it))      {        os << "node: { title:/"n";        os << ss.str() << "/" label: /"";        if (it->GetType() == BEEV::BOOLEAN_TYPE)          os << _kind_names[it->GetKind()];        else          outputBitVec(*it, os);        os << "/"}" << endl;        constantOutput.insert(*it);      }      os << "edge: { source:/"n" << n.GetNodeNum() << "/" target: /""         << "n" << ss.str() << "/"" << label.str() << "}" << endl;    }    else      os << "edge: { source:/"n" << n.GetNodeNum() << "/" target: /""         << "n" << it->GetNodeNum() << "/"" << label.str() << "}" << endl;    i++;  }  // print each of the children.  for (ASTVec::const_iterator it = ch.begin(); it < itend; it++)  {    if (!it->isConstant())      GDL_Print1(os, *it, alreadyOutput, annotate);  }}

  //this function looksup the "var to letexpr map" and returns the  //corresponding letexpr. if there is no letexpr, then it simply  //returns the var.  ASTNode BeevMgr::ResolveID(const ASTNode& v) {    if(v.GetKind() != SYMBOL) {      return v;    }    if(_parser_symbol_table.find(v) != _parser_symbol_table.end()) {      return v;    }    ASTNodeMap::iterator it;    if((it =_letid_expr_map.find(v)) != _letid_expr_map.end()) {      if(it->second == ASTUndefined) 	FatalError("Unresolved Identifier: ",v);      else	return it->second;    }    //this is to mark the let-var as undefined. the let var is defined    //only after the LetExprMgr has completed its work, and until then    //'v' is undefined.     //    //declared variables also get stored in this map, but there value    //is ASTUndefined. This is really a hack. I don't know how to get    //rid of this hack.    _letid_expr_map[v] = ASTUndefined;    return v;      }

  // FUNC: This function maintains a map between LET-var names and  // LET-expressions  //  //1. if the Let-var is already defined in the LET scope, then the  //1. function returns an error.  //  //2. if the Let-var is already declared variable in the input, then  //2. the function returns an error  //  //3. otherwise add the <var,letExpr> pair to the _letid_expr table.  void BeevMgr::LetExprMgr(const ASTNode& var, const ASTNode& letExpr) {    ASTNodeMap::iterator it;    if(((it = _letid_expr_map.find(var)) != _letid_expr_map.end()) &&        it->second != ASTUndefined) {            FatalError("LetExprMgr:The LET-var v has already been defined in this LET scope: v =", var);    }    if(_parser_symbol_table.find(var) != _parser_symbol_table.end()) {      FatalError("LetExprMgr:This var is already declared. cannot redeclare as a letvar: v =", var);    }    _letid_expr_map[var] = letExpr;     }

// Print in lisp formatostream& Lisp_Print(ostream& os, const ASTNode& n, int indentation){  // Clear the PrintMap  Lisp_AlreadyPrintedSet.clear();  Lisp_Print_indent(os, n, indentation);  printf("/n");  return os;}

/** Internal function to print in lisp format.  Assume newline    and indentation printed already before first line.  Recursive    calls will have newline & indent, though */ostream& Lisp_Print1(ostream& os, const ASTNode& n, int indentation){  if (!n.IsDefined())  {    os << "<undefined>";    return os;  }  Kind kind = n.GetKind();  // FIXME: figure out how to avoid symbols with same names as kinds.  //    if (kind == READ) {  //      const ASTVec &children = GetChildren();  //      children[0].LispPrint1(os, indentation);  //  os << "[" << children[1] << "]";  //    } else  if (kind == BOOLEXTRACT)  {    const ASTVec& children = n.GetChildren();    // child 0 is a symbol.  Print without the NodeNum.    os << n.GetNodeNum() << ":";    children[0].nodeprint(os, true);    os << "{";    children[1].nodeprint(os, true);    os << "}";  }  else if (kind == NOT)  {    const ASTVec& children = n.GetChildren();    os << n.GetNodeNum() << ":";    os << "(NOT ";    Lisp_Print1(os, children[0], indentation);    os << ")";  }  else if (n.Degree() == 0)  {    // Symbol or a kind with no children print as index:NAME if shared,    // even if they have been printed before.    os << n.GetNodeNum() << ":";    n.nodeprint(os, true);    // os << "(" << _int_node_ptr->_ref_count << ")";    // os << "{" << GetValueWidth() << "}";  }  else if (Lisp_AlreadyPrintedSet.find(n) != Lisp_AlreadyPrintedSet.end())  {    // print non-symbols as "[index]" if seen before.    os << "[" << n.GetNodeNum() << "]";    //         << "(" << _int_node_ptr->_ref_count << ")";  }  else  {    Lisp_AlreadyPrintedSet.insert(n);    const ASTVec& children = n.GetChildren();    os << n.GetNodeNum() << ":"       //<< "(" << _int_node_ptr->_ref_count << ")"       << "(" << kind << " ";    // os << "{" << GetValueWidth() << "}";    ASTVec::const_iterator iend = children.end();    for (ASTVec::const_iterator i = children.begin(); i != iend; i++)    {      Lisp_Print_indent(os, *i, indentation + 2);    }    os << ")";  }  return os;}