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

 ASTNode STPMgr::CreateSimpXor(const ASTNode& form1, const ASTNode& form2) {   ASTVec children;   children.push_back(form1);   children.push_back(form2);   return CreateSimpXor(children); }

bool PropagateEqualities::searchTerm(const ASTNode& lhs, const ASTNode& rhs){  const unsigned width = lhs.GetValueWidth();  if (lhs == rhs)    return true;  if (lhs.GetKind() == SYMBOL)    return simp->UpdateSubstitutionMap(lhs, rhs); // checks whether it's been                                                  // solved for, or if the RHS                                                  // contains the LHS.  if (lhs.GetKind() == BVUMINUS)    return searchTerm(lhs[0], nf->CreateTerm(BVUMINUS, width, rhs));  if (lhs.GetKind() == BVNEG)    return searchTerm(lhs[0], nf->CreateTerm(BVNEG, width, rhs));  if (lhs.GetKind() == BVXOR || lhs.GetKind() == BVPLUS)    for (size_t i = 0; i < lhs.Degree(); i++)    {      ASTVec others;      for (size_t j = 0; j < lhs.Degree(); j++)        if (j != i)          others.push_back(lhs[j]);      ASTNode new_rhs;      if (lhs.GetKind() == BVXOR)      {        others.push_back(rhs);        assert(others.size() > 1);        new_rhs = nf->CreateTerm(lhs.GetKind(), width, others);      }      else if (lhs.GetKind() == BVPLUS)      {        if (others.size() > 1)          new_rhs = nf->CreateTerm(BVPLUS, width, others);        else          new_rhs = others[0];        new_rhs = nf->CreateTerm(BVUMINUS, width, new_rhs);        new_rhs = nf->CreateTerm(BVPLUS, width, new_rhs, rhs);      }      else        FatalError("sdafasfsdf2q3234423");      bool result = searchTerm(lhs[i], new_rhs);      if (result)        return true;    }  if (lhs.Degree() == 2 && lhs.GetKind() == BVMULT && lhs[0].isConstant() &&      simp->BVConstIsOdd(lhs[0]))    return searchTerm(lhs[1],                      nf->CreateTerm(BVMULT, width,                                     simp->MultiplicativeInverse(lhs[0]), rhs));  return false;}

  // Does some simple caching of prior results.  void  Cpp_interface::checkSat(const ASTVec & assertionsSMT2)  {    if (ignoreCheckSatRequest)      return;    bm.GetRunTimes()->stop(RunTimes::Parsing);    checkInvariant();    assert(assertionsSMT2.size() == cache.size());    Entry& last_run = cache.back();    if ((last_run.node_number != assertionsSMT2.back().GetNodeNum()) && (last_run.result == SOLVER_SATISFIABLE))      {        // extra asserts might have been added to it,        // flipping from sat to unsat. But never from unsat to sat.        last_run.result =  SOLVER_UNDECIDED;      }    // We might have run this query before, or it might already be shown to be unsat. If it was sat,    // we've stored the result (but not the model), so we can shortcut and return what we know.    if (!((last_run.result == SOLVER_SATISFIABLE) || last_run.result == SOLVER_UNSATISFIABLE))        {          resetSolver();          ASTNode query;          if (assertionsSMT2.size() > 1)            query = nf->CreateNode(AND, assertionsSMT2);          else if (assertionsSMT2.size() == 1)            query = assertionsSMT2[0];          else            query = bm.ASTTrue;          SOLVER_RETURN_TYPE last_result = GlobalSTP->TopLevelSTP(query, bm.ASTFalse);          // Store away the answer. Might be timeout, or error though..          last_run = Entry(last_result);          last_run.node_number = assertionsSMT2.back().GetNodeNum();          // It's satisfiable, so everything beneath it is satisfiable too.          if (last_result == SOLVER_SATISFIABLE)            {              for (int i = 0; i < cache.size(); i++)                {                  assert(cache[i].result != SOLVER_UNSATISFIABLE);                  cache[i].result = SOLVER_SATISFIABLE;                }            }        }    if (bm.UserFlags.quick_statistics_flag)      {        bm.GetRunTimes()->print();      }    (GlobalSTP->tosat)->PrintOutput(last_run.result);    bm.GetRunTimes()->start(RunTimes::Parsing);  }

 ASTNode STPMgr::CreateSimpAndOr(bool IsAnd,                                  const ASTNode& form1, const ASTNode& form2) {   ASTVec children;   children.push_back(form1);   children.push_back(form2);   return CreateSimpAndOr(IsAnd, children); }

 ASTNode STPMgr::CreateSimpForm(Kind kind, const ASTNode& child0) {   ASTVec children;   //child_stack.clear();      // could just reset top pointer.   children.push_back(child0);   //child_stack.push_back(child0);   return CreateSimpForm(kind, children);   //return CreateSimpForm(kind, child_stack); }

  void checkChildrenAreBV(const ASTVec& v, const ASTNode&n) {	for (ASTVec::const_iterator it = v.begin(), itend = v.end(); it != itend; it++)		if (BITVECTOR_TYPE != it->GetType()) {			cerr << "The type is: " << it->GetType() << endl;			FatalError(					"BVTypeCheck:ChildNodes of bitvector-terms must be bitvectors/n",					n);		}}

ASTNode NodeFactory::CreateNode(Kind kind, const ASTNode& child0,                                const ASTVec & back_children){    ASTVec front_children;    front_children.reserve(1 + back_children.size());    front_children.push_back(child0);    front_children.insert(front_children.end(), back_children.begin(),                          back_children.end());    return CreateNode(kind, front_children);}

void STPMgr::printAssertsToStream(ostream& os){  ASTVec v = GetAsserts();  for (ASTVec::iterator i = v.begin(), iend = v.end(); i != iend; i++)  {    ASTNode q = *i;    os << "ASSERT( ";    q.PL_Print(os, this);    os << ");" << endl;  }}

 void STPMgr::printAssertsToStream(ostream &os, int simplify_print) {   ASTVec v = GetAsserts();   for(ASTVec::iterator i=v.begin(),iend=v.end();i!=iend;i++) {     //Begin_RemoveWrites = true; ASTNode q = (simplify_print == 1) ?     //SimplifyFormula_TopLevel(*i,false) : *i; q = (simplify_print     //== 1) ? SimplifyFormula_TopLevel(q,false) : q;     ASTNode q = *i;     //Begin_RemoveWrites = false;     os << "ASSERT( ";     q.PL_Print(os);     os << ");" << endl;   } }

ASTNode NodeFactory::CreateArrayTerm(Kind kind, unsigned int index, unsigned int width,                                     const ASTNode& child0, const ASTNode& child1, const ASTNode& child2,                                     const ASTVec &children){    ASTVec child;    child.reserve(children.size() + 3);    child.push_back(child0);    child.push_back(child1);    child.push_back(child2);    child.insert(child.end(), children.begin(), children.end());    return CreateArrayTerm(kind, index, width, child);}

 void FlattenKind(const Kind k, const ASTVec &children, ASTVec & flat_children) {   ASTVec::const_iterator ch_end = children.end();   for (ASTVec::const_iterator it = children.begin(); it != ch_end; it++)     {       Kind ck = it->GetKind();       if (k == ck)         {           FlattenKind(k,it->GetChildren(), flat_children);         }       else         {           flat_children.push_back(*it);         }     } }

  void print_STPInput_Back(const ASTNode& query) {	  // Determine the symbols in the query and asserts.	  ASTNodeSet visited;	  ASTNodeSet symbols;	  buildListOfSymbols(query,  visited, symbols);      ASTVec v = (BEEV::GlobalSTP->bm)->GetAsserts();      for(ASTVec::iterator i=v.begin(),iend=v.end();i!=iend;i++)    	buildListOfSymbols(*i,  visited, symbols);	(BEEV::GlobalSTP->bm)->printVarDeclsToStream(cout, symbols);    (BEEV::GlobalSTP->bm)->printAssertsToStream(cout,0);    cout << "QUERY(";    query.PL_Print(cout);    cout << ");/n";  } //end of print_STPInput_Back()

bool PropagateEqualities::searchXOR(const ASTNode& lhs, const ASTNode& rhs){  Kind k = lhs.GetKind();  if (lhs == rhs)    return true;  if (k == SYMBOL)    return simp->UpdateSubstitutionMap(        lhs, rhs); // checks whether it's been solved for or loops.  if (k == NOT)    return searchXOR(lhs[0], nf->CreateNode(NOT, rhs));  bool result = false;  if (k == XOR)    for (size_t i = 0; i < lhs.Degree(); i++)    {      ASTVec others;      for (size_t j = 0; j < lhs.Degree(); j++)        if (j != i)          others.push_back(lhs[j]);      others.push_back(rhs);      assert(others.size() > 1);      ASTNode new_rhs = nf->CreateNode(XOR, others);      result = searchXOR(lhs[i], new_rhs);      if (result)        return result;    }  if (k == EQ && lhs[0].GetValueWidth() == 1)  {    bool result =        searchTerm(lhs[0], nf->CreateTerm(ITE, 1, rhs, lhs[1],                                          nf->CreateTerm(BVNEG, 1, lhs[1])));    if (!result)      result =          searchTerm(lhs[1], nf->CreateTerm(ITE, 1, rhs, lhs[0],                                            nf->CreateTerm(BVNEG, 1, lhs[0])));  }  return result;}

  void Dot_Print1(ostream &os, const ASTNode n, hash_set<int> *alreadyOutput)  {    // check if this node has already been printed. If so return.    if (alreadyOutput->find(n.GetNodeNum()) != alreadyOutput->end())      return;    alreadyOutput->insert(n.GetNodeNum());    os << "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 << "/"];" << endl;    // print the edges to each child.    ASTVec ch = n.GetChildren();    ASTVec::iterator itend = ch.end();    int i = 0;    for (ASTVec::iterator it = ch.begin(); it < itend; it++)      {        os << "n" << n.GetNodeNum()            << " -> " << "n"            << it->GetNodeNum()            << "[label=" << i++            << "];" << endl;      }    // print each of the children.    for (ASTVec::iterator it = ch.begin(); it < itend; it++)      {        Dot_Print1(os, *it, alreadyOutput);      }  }

/* 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);    }  }}

  // Flatten (k ... (k ci cj) ...) to (k ... ci cj ...)  // This is local to this file.  ASTVec FlattenKind(Kind k, const ASTVec &children)  {    ASTVec flat_children;    ASTVec::const_iterator ch_end = children.end();    for (ASTVec::const_iterator it = children.begin(); it != ch_end; it++)      {        Kind ck = it->GetKind();        const ASTVec &gchildren = it->GetChildren();        if (k == ck)          {            // append grandchildren to children            flat_children.insert(flat_children.end(),                                 gchildren.begin(), gchildren.end());          }        else          {            flat_children.push_back(*it);          }      }    return flat_children;  }

  /* The most complicated handling is for EXTRACTS. If a variable has parents that * are all extracts and each of those extracts is disjoint (i.e. reads different bits) * Then each of the extracts are replaced by a fresh variable. This is the only case * where a variable with multiple distinct parents is replaced by a fresh variable. * + We perform this check upfront, so will miss any extra cases the the unconstrained *   variable elimination introduces. * + It's all or nothing. So even if there's an extract of [0:2] [1:2] and [3:5], we wont *   replace the [3:5] (even though it could be). */  void  RemoveUnconstrained::splitExtractOnly(vector<MutableASTNode*> extracts)  {    assert(extracts.size() >0);    // Going to be rebuilt later anyway, so discard.    vector<MutableASTNode*> variables;    for (int i =0; i <extracts.size(); i++)      {        ASTNode& var = extracts[i]->n;        assert(var.GetKind() == SYMBOL);        const int size = var.GetValueWidth();        std::vector<ASTNode> toVar(size);        // Create a mutable copy that we can iterate over.        vector <MutableASTNode*> mut;        mut.insert(mut.end(), extracts[i]->parents.begin(), extracts[i]->parents.end());        for (vector<MutableASTNode*>::iterator it = mut.begin(); it != mut.end(); it++)          {            ASTNode parent_node = (*it)->n;            assert(((**it)).children[0] == extracts[i]);            assert(!parent_node.IsNull());            assert(parent_node.GetKind() == BVEXTRACT);            int lb = parent_node[2].GetUnsignedConst();            // Replace each parent with a fresh.            toVar[lb] = replaceParentWithFresh(**it,variables);          }      ASTVec concatVec;      int empty =0;      for (int j=0; j < size;j++)      {          if (toVar[j].IsNull())            {              empty++;              continue;            }          if (empty > 0)            {              concatVec.push_back(bm.CreateFreshVariable(0, empty, "extract_unc"));              empty = 0;            }          concatVec.push_back(toVar[j]);          //cout << toVar[j];          assert(toVar[j].GetValueWidth() > 0);          j+=toVar[j].GetValueWidth()-1;        }      if (empty> 0)        {          concatVec.push_back(bm.CreateFreshVariable(0, empty, "extract_unc"));        }    ASTNode concat = concatVec[0];    for (int i=1; i < concatVec.size();i++)      {          assert(!concat.IsNull());          concat = bm.CreateTerm(BVCONCAT, concat.GetValueWidth() + concatVec[i].GetValueWidth(),concatVec[i], concat);      }    replace(var,concat);        }  }

  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;           *///.........这里部分代码省略.........

ASTNode ArrayTransformer::TransformTerm(const ASTNode& term){  assert(TransformMap != NULL);  const Kind k = term.GetKind();  if (!is_Term_kind(k))    FatalError("TransformTerm: Illegal kind: You have input a nonterm:", term,               k);  ASTNodeMap::const_iterator iter;  if ((iter = TransformMap->find(term)) != TransformMap->end())    return iter->second;  ASTNode result;  switch (k)  {    case SYMBOL:    case BVCONST:    {      result = term;      break;    }    case WRITE:      FatalError("TransformTerm: this kind is not supported", term);      break;    case READ:      result = TransformArrayRead(term);      break;    case ITE:    {      ASTNode cond = term[0];      ASTNode thn = term[1];      ASTNode els = term[2];      cond = TransformFormula(cond);      if (ASTTrue == cond)        result = TransformTerm(thn);      else if (ASTFalse == cond)        result = TransformTerm(els);      else      {        thn = TransformTerm(thn);        els = TransformTerm(els);        if (bm->UserFlags.optimize_flag)          result = simp->CreateSimplifiedTermITE(cond, thn, els);        else          result = nf->CreateTerm(ITE, thn.GetValueWidth(), cond, thn, els);      }      assert(result.GetIndexWidth() == term.GetIndexWidth());      break;    }    default:    {      const ASTVec& c = term.GetChildren();      ASTVec::const_iterator it = c.begin();      ASTVec::const_iterator itend = c.end();      const unsigned width = term.GetValueWidth();      const unsigned indexwidth = term.GetIndexWidth();      ASTVec o;      o.reserve(c.size());      for (; it != itend; it++)      {        o.push_back(TransformTerm(*it));      }      if (c != o)      {        result = nf->CreateArrayTerm(k, indexwidth, width, o);      }      else        result = term;    }    break;  }  if (term.Degree() > 0)    (*TransformMap)[term] = result;  if (term.GetValueWidth() != result.GetValueWidth())    FatalError("TransformTerm: "               "result and input terms are of different length",               result);  if (term.GetIndexWidth() != result.GetIndexWidth())  {    std::cerr << "TransformTerm: input term is : " << term << std::endl;    FatalError("TransformTerm: "               "result & input terms have different index length",               result);  }  return result;} 

int main(int argc, char** argv){    extern int smt2parse();    extern int smt2lex_destroy(void);    extern FILE* smt2in;    STPMgr stp;    STPMgr* mgr = &stp;    Cpp_interface interface(*mgr, mgr->defaultNodeFactory);    interface.startup();    interface.ignoreCheckSat();    stp::GlobalParserInterface = &interface;    Simplifier* simp = new Simplifier(mgr);    ArrayTransformer* at = new ArrayTransformer(mgr, simp);    AbsRefine_CounterExample* abs = new AbsRefine_CounterExample(mgr, simp, at);    ToSATAIG* tosat = new ToSATAIG(mgr, at);    GlobalSTP = new STP(mgr, simp, at, tosat, abs);    srand(time(NULL));    stp::GlobalParserBM = &stp;    stp.UserFlags.disableSimplifications();    stp.UserFlags.bitConstantProp_flag = true;    // Parse SMTLIB2-----------------------------------------    mgr->GetRunTimes()->start(RunTimes::Parsing);    if (argc > 1)    {        smt2in = fopen(argv[1], "r");        smt2parse();    }    else    {        smt2in = NULL; // from stdin.        smt2parse();    }    smt2lex_destroy();    //-----------------------------------------------------    ASTNode n;    ASTVec v = interface.GetAsserts();    if (v.size() > 1)        n = interface.CreateNode(AND, v);    else        n = v[0];    // Apply cbitp ----------------------------------------    simplifier::constantBitP::ConstantBitPropagation cb(        simp, mgr->defaultNodeFactory, n);    if (cb.isUnsatisfiable())        n = mgr->ASTFalse;    else        n = cb.topLevelBothWays(n, true, true);    if (simp->hasUnappliedSubstitutions())    {        n = simp->applySubstitutionMap(n);        simp->haveAppliedSubstitutionMap();    }    // Print back out.    printer::SMTLIB2_PrintBack(cout, n);    cout << "(check-sat)/n";    cout << "(exit)/n";    return 0;}

  //UserGuided abstraction refinement  SOLVER_RETURN_TYPE  STP::  UserGuided_AbsRefine(SATSolver& NewSolver,		       const ASTNode& original_input)  {    ASTVec v = bm->GetAsserts_WithKey(0);    if(v.empty())      {	FatalError("UserGuided_AbsRefine: Something is seriously wrong."/		   "The input set is empty");      }    ASTNode sureAddInput =       (v.size() == 1) ? v[0] : bm->CreateNode(AND, v);     SOLVER_RETURN_TYPE res = SOLVER_UNDECIDED;    res = TopLevelSTPAux(NewSolver, sureAddInput, original_input);    if(SOLVER_UNDECIDED != res)      {	return res;      }        //Do refinement here    if(AND != original_input.GetKind())      {	FatalError("UserGuided_AbsRefine: The input must be an AND");      }    ASTVec RefineFormulasVec;    ASTVec RemainingFormulasVec;    ASTNode asttrue = bm->CreateNode(TRUE);    ASTNode astfalse = bm->CreateNode(FALSE);    for(int count=0; count < bm->UserFlags.num_absrefine; count++)      {	RemainingFormulasVec.clear();	RemainingFormulasVec.push_back(asttrue);	RefineFormulasVec.clear();		RefineFormulasVec.push_back(asttrue);	ASTVec InputKids = original_input.GetChildren();	for(ASTVec::iterator it = InputKids.begin(), itend = InputKids.end();	    it!=itend;it++)	  {	    Ctr_Example->ClearComputeFormulaMap();	    if(astfalse == Ctr_Example->ComputeFormulaUsingModel(*it))	      {		RefineFormulasVec.push_back(*it);	      }	    else	      {		RemainingFormulasVec.push_back(*it);	      }	  }	ASTNode RefineFormulas =	  (RefineFormulasVec.size() == 1) ?	  RefineFormulasVec[0] : bm->CreateNode(AND, RefineFormulasVec);	res = TopLevelSTPAux(NewSolver, RefineFormulas, original_input);	if(SOLVER_UNDECIDED != res)	  {	    return res;	  }      }    ASTNode RemainingFormulas =       (RemainingFormulasVec.size() == 1) ?      RemainingFormulasVec[0] : bm->CreateNode(AND, RemainingFormulasVec);    res = TopLevelSTPAux(NewSolver, RemainingFormulas, original_input);        if(SOLVER_UNDECIDED != res)      {	return res;      }        FatalError("TopLevelSTPAux: reached the end without proper conclusion:"	       "either a divide by zero in the input or a bug in STP");        return SOLVER_ERROR;  } //End of UserGuided_AbsRefine()

  // FIXME:  How do I know whether ITE is a formula or not?  ASTNode STPMgr::CreateSimpFormITE(const ASTNode& child0,                                     const ASTNode& child1,                                     const ASTNode& child2)  {    ASTNode retval;    if (_trace_simpbool)      {        cout << "========" << endl              << "CreateSimpFormITE "              << child0 << child1 << child2 << endl;      }    if (ASTTrue == child0)      {        retval = child1;      }    else if (ASTFalse == child0)      {        retval = child2;      }    else if (child1 == child2)      {        retval = child1;      }    // ITE(x, TRUE, y ) == x OR y    else if (ASTTrue == child1)      {        retval = CreateSimpAndOr(0, child0, child2);      }    // ITE(x, FALSE, y ) == (!x AND y)    else if (ASTFalse == child1)      {        retval = CreateSimpAndOr(1, CreateSimpNot(child0), child2);      }    // ITE(x, y, TRUE ) == (!x OR y)    else if (ASTTrue == child2)      {        retval = CreateSimpAndOr(0, CreateSimpNot(child0), child1);      }    // ITE(x, y, FALSE ) == (x AND y)    else if (ASTFalse == child2)      {        retval = CreateSimpAndOr(1, child0, child1);      }    else      {	ASTNode left  = CreateNode(AND, child0, child1);	ASTNode right = CreateNode(AND, CreateNode(NOT,child0), child2);	ASTVec c;	c.push_back(left);	c.push_back(right);        retval = CreateSimpXor(c);      }    if (_trace_simpbool)      {        cout << "returns " << retval << endl;      }    return retval;  }

  // Constant children are accumulated in "accumconst".  ASTNode STPMgr::CreateSimpXor(ASTVec &children)  {    if (_trace_simpbool)      {        cout << "========" << endl << "CreateSimpXor ";        lpvec(children);        cout << endl;      }    ASTVec flat_children; // empty vector    ASTVec::const_iterator it_end = children.end();    if (UserFlags.xor_flatten_flag)      {        flat_children = FlattenKind(XOR, children);      }    else      {        flat_children = children;      }    // sort so that identical nodes occur in sequential runs, followed by    // their negations.    SortByExprNum(flat_children);    ASTNode retval;    // This is the C Boolean value of all constant args seen.  It is initially    // 0.  TRUE children cause it to change value.    bool accumconst = 0;    ASTVec new_children;    it_end = flat_children.end();    ASTVec::iterator next_it;    for (ASTVec::iterator it = flat_children.begin(); it != it_end; it++)      {        next_it = it + 1;        bool nextexists = (next_it < it_end);        if (ASTTrue == *it)          {            accumconst = !accumconst;          }        else if (ASTFalse == *it)          {            // Ignore it          }        else if (nextexists && (*next_it == *it))          {            // x XOR x = FALSE.  Skip current, write "false" into next_it            // so that it gets tossed, too.            *next_it = ASTFalse;          }        else if (nextexists && (next_it->GetKind() == NOT)                  && ((*next_it)[0] == *it))          {            // x XOR NOT x = TRUE.  Skip current, write "true" into next_it            // so that it gets tossed, too.            *next_it = ASTTrue;          }        else if (NOT == it->GetKind())          {            // If child is (NOT alpha), we can flip accumconst and use alpha.            // This is ok because (NOT alpha) == TRUE XOR alpha            accumconst = !accumconst;            // CreateSimpNot just takes child of not.            new_children.push_back(CreateSimpNot(*it));          }        else          {            new_children.push_back(*it);          }      }    // Children should be non-constant.    if (new_children.size() < 2)      {        if (0 == new_children.size())          {            // XOR(TRUE, FALSE) -- accumconst will be 1.            if (accumconst)              {                retval = ASTTrue;              }            else              {                retval = ASTFalse;              }          }        else          {            // there is just one child            // XOR(x, TRUE) -- accumconst will be 1.            if (accumconst)              {                retval = CreateSimpNot(new_children[0]);              }//.........这里部分代码省略.........

 void SortByArith(ASTVec& v) {   sort(v.begin(), v.end(), arithless); }

 void SortByExprNum(ASTVec& v) {   sort(v.begin(), v.end(), exprless); }

int main(int argc, char** argv){    // Register the error handler    vc_error_hdlr = errorHandler;#if  !defined(__MINGW32__) && !defined(__MINGW64__) && !defined( _MSC_VER)    // Grab some memory from the OS upfront to reduce system time when    // individual hash tables are being allocated    if (sbrk(INITIAL_MEMORY_PREALLOCATION_SIZE) == ((void*) - 1)) {        FatalError("Initial allocation of memory failed.");    }#endif /* !defined(__MINGW32__) && !defined(__MINGW64__) && !defined( _MSC_VER) */    bm = new STPMgr();    toClose = NULL;    auto_ptr<SimplifyingNodeFactory> simplifyingNF( new SimplifyingNodeFactory(*bm->hashingNodeFactory, *bm));    bm->defaultNodeFactory = simplifyingNF.get();    // The simplified keeps a pointer to whatever is set as the default node factory.    Simplifier* simp  = new Simplifier(bm);    auto_ptr<Simplifier> simpCleaner(simp);    ArrayTransformer* arrayTransformer = new ArrayTransformer(bm, simp);    auto_ptr<ArrayTransformer> atClearner(arrayTransformer);    ToSAT* tosat = new ToSAT(bm);    auto_ptr<ToSAT> tosatCleaner(tosat);    AbsRefine_CounterExample* Ctr_Example = new AbsRefine_CounterExample(bm, simp, arrayTransformer);    auto_ptr<AbsRefine_CounterExample> ctrCleaner(Ctr_Example);    create_options();    int ret = parse_options(argc, argv);    if (ret != 0) {        return ret;    }    GlobalSTP = new STP(bm, simp, arrayTransformer, tosat, Ctr_Example);    // If we're not reading the file from stdin.    if (!infile.empty()) {        read_file();    }    //want to print the output always from the commandline.    bm->UserFlags.print_output_flag = true;    ASTVec* AssertsQuery = new ASTVec;    bm->GetRunTimes()->start(RunTimes::Parsing);    parse_file(AssertsQuery);    bm->GetRunTimes()->stop(RunTimes::Parsing);    /*  The SMTLIB2 has a command language. The parser calls all the functions,     *  so when we get to here the parser has already called "exit". i.e. if the     *  language is smt2 then all the work has already been done, and all we need     *  to do is cleanup...     *    */    if (!bm->UserFlags.smtlib2_parser_flag) {        if (((ASTVec*) AssertsQuery)->empty()) {            FatalError("Input is Empty. Please enter some asserts and query/n");        }        if (((ASTVec*) AssertsQuery)->size() != 2) {            FatalError("Input must contain a query/n");        }        ASTNode asserts = (*(ASTVec*) AssertsQuery)[0];        ASTNode query = (*(ASTVec*) AssertsQuery)[1];        if (onePrintBack) {            print_back(query, asserts);            return 0;        }        SOLVER_RETURN_TYPE ret = GlobalSTP->TopLevelSTP(asserts, query);        if (bm->UserFlags.quick_statistics_flag) {            bm->GetRunTimes()->print();        }        (GlobalSTP->tosat)->PrintOutput(ret);        asserts = ASTNode();        query = ASTNode();    }    //Without cleanup    if (bm->UserFlags.isSet("fast-exit", "1")) {        exit(0);    }    //Propery tidy up    AssertsQuery->clear();    delete AssertsQuery;    _empty_ASTVec.clear();    simpCleaner.release();    atClearner.release();//.........这里部分代码省略.........

// This doesn't rewrite changes through properly so needs to have a substitution// applied to its output.ASTNode PropagateEqualities::propagate(const ASTNode& a, ArrayTransformer* at){  ASTNode output;  // if the variable has been solved for, then simply return it  if (simp->InsideSubstitutionMap(a, output))    return output;  if (!alreadyVisited.insert(a.GetNodeNum()).second)  {    return a;  }  output = a;  // traverse a and populate the SubstitutionMap  const Kind k = a.GetKind();  if (SYMBOL == k && BOOLEAN_TYPE == a.GetType())  {    bool updated = simp->UpdateSubstitutionMap(a, ASTTrue);    output = updated ? ASTTrue : a;  }  else if (NOT == k)  {    bool updated = searchXOR(a[0], ASTFalse);    output = updated ? ASTTrue : a;  }  else if (IFF == k || EQ == k)  {    const ASTVec& c = a.GetChildren();    if (c[0] == c[1])      return ASTTrue;    bool updated = simp->UpdateSubstitutionMap(c[0], c[1]);    if (updated)    {      // fill the arrayname readindices vector if e0 is a      // READ(Arr,index) and index is a BVCONST      int to;      if ((to = TermOrder(c[0], c[1])) == 1 && c[0].GetKind() == READ)        at->FillUp_ArrReadIndex_Vec(c[0], c[1]);      else if (to == -1 && c[1].GetKind() == READ)        at->FillUp_ArrReadIndex_Vec(c[1], c[0]);    }    if (!updated)      updated = searchTerm(c[0], c[1]);    if (!updated)      updated = searchTerm(c[1], c[0]);    output = updated ? ASTTrue : a;  }  else if (XOR == k)  {    bool updated = searchXOR(a, ASTTrue);    output = updated ? ASTTrue : a;    if (updated)      return output;// The below block should be subsumed by the searchXOR function which// generalises it.// So the below block should never do anything..#ifndef NDEBUG    if (a.Degree() != 2)      return output;    int to = TermOrder(a[0], a[1]);    if (0 == to)    {      if (a[0].GetKind() == NOT && a[0][0].GetKind() == EQ &&          a[0][0][0].GetValueWidth() == 1 && a[0][0][1].GetKind() == SYMBOL)      {        // (XOR (NOT(= (1 v)))  ... )        const ASTNode& symbol = a[0][0][1];        const ASTNode newN = nf->CreateTerm(            ITE, 1, a[1], a[0][0][0], nf->CreateTerm(BVNEG, 1, a[0][0][0]));        if (simp->UpdateSolverMap(symbol, newN))        {          assert(false);          output = ASTTrue;        }      }      else if (a[1].GetKind() == NOT && a[1][0].GetKind() == EQ &&               a[1][0][0].GetValueWidth() == 1 &&               a[1][0][1].GetKind() == SYMBOL)      {        const ASTNode& symbol = a[1][0][1];        const ASTNode newN = nf->CreateTerm(            ITE, 1, a[0], a[1][0][0], nf->CreateTerm(BVNEG, 1, a[1][0][0]));        if (simp->UpdateSolverMap(symbol, newN))        {          assert(false);          output = ASTTrue;//.........这里部分代码省略.........

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);  }}