void StatisicsPropertyintegration::setup()
{
    m_char_type = new TypeNode("char_type");

    m_char_property = new StatisticsProperty;
    m_char_property->setFlags(flag_class);
    m_char_type->addProperty("char_prop", m_char_property);

    m_char1 = new Entity("1", 1);
    m_char1->setType(m_char_type);
    m_char_property->install(m_char1, "char_prop");
    m_char_property->apply(m_char1);

    m_char2 = new Entity("2", 2);
    m_char2->setType(m_char_type);
    m_char_property->install(m_char2, "char_prop");
    m_char_property->apply(m_char2);
}

bool TermEnumeration::isClosedEnumerableType(TypeNode tn)
{
  std::unordered_map<TypeNode, bool, TypeNodeHashFunction>::iterator it =
      d_typ_closed_enum.find(tn);
  if (it == d_typ_closed_enum.end())
  {
    d_typ_closed_enum[tn] = true;
    bool ret = true;
    if (tn.isArray() || tn.isSort() || tn.isCodatatype() || tn.isFunction())
    {
      ret = false;
    }
    else if (tn.isSet())
    {
      ret = isClosedEnumerableType(tn.getSetElementType());
    }
    else if (tn.isDatatype())
    {
      const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
      for (unsigned i = 0; i < dt.getNumConstructors(); i++)
      {
        for (unsigned j = 0; j < dt[i].getNumArgs(); j++)
        {
          TypeNode ctn = TypeNode::fromType(dt[i][j].getRangeType());
          if (tn != ctn && !isClosedEnumerableType(ctn))
          {
            ret = false;
            break;
          }
        }
        if (!ret)
        {
          break;
        }
      }
    }
    
    // other parametric sorts go here
    
    d_typ_closed_enum[tn] = ret;
    return ret;
  }
  else
  {
    return it->second;
  }
}

Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){
   Node ret;
   if( i<d_terms[tn].size() ){
     ret = d_terms[tn][i];
   }else{
     Debug("dt-enum-debug") << "get term enum " << tn << " " << i << std::endl;
     std::map< TypeNode, unsigned >::iterator it = d_te_index.find( tn );
     unsigned tei;
     if( it==d_te_index.end() ){
       //initialize child enumerator for type
       tei = d_children.size();
       d_te_index[tn] = tei;
       if( tn.isDatatype() && d_has_debruijn ){
         //must indicate that this is a child enumerator (do not normalize constants for it)
         DatatypesEnumerator * dte = new DatatypesEnumerator( tn, true );
         d_children.push_back( TypeEnumerator( dte ) );
       }else{
         d_children.push_back( TypeEnumerator( tn ) );
       }
       d_terms[tn].push_back( *d_children[tei] );
     }else{
       tei = it->second;
     }
     //enumerate terms until index is reached
     while( i>=d_terms[tn].size() ){
       ++d_children[tei];
       if( d_children[tei].isFinished() ){
         Debug("dt-enum-debug") << "...fail term enum " << tn << " " << i << std::endl;
         return Node::null();
       }
       d_terms[tn].push_back( *d_children[tei] );
     }
     Debug("dt-enum-debug") << "...return term enum " << tn << " " << i << " : " << d_terms[tn][i] << std::endl;
     ret = d_terms[tn][i];
   }
   return ret;
 }

TypeNode* TypeNameNode::getTypeNode(TemplateArguments* templateArguments)
{
	//assert(0 == templateArguments || templateArguments->m_classTypeNode->isTemplateClassInstance());
	assert(0 != m_startTypeNode);
	TypeNode* result = 0;
	if (0 == m_typeNode)// under template parameter
	{
		assert(templateArguments && m_startTypeNode 
			&& (m_startTypeNode->isTemplateParameter() || m_startTypeNode->isTypedef()) );
		if (templateArguments->m_classTypeNode->isClass())
		{
			return 0;
		}
		TypeNode* actualStartTypeNode = m_startTypeNode->getActualTypeNode(templateArguments);
		assert(actualStartTypeNode);
		std::vector<ScopeNameNode*> scopeNameNodes;
		m_scopeNameList->collectIdentifyNodes(scopeNameNodes);
		if (scopeNameNodes.size() == 1)
		{
			result = actualStartTypeNode;
		}
		else
		{
			scopeNameNodes.erase(scopeNameNodes.begin());
			TypeNode* initialTypeTreeNode = 0;
			TypeNode* finalTypeTreeNode = 0;
			if (g_typeTree.findNodeByScopeNames(initialTypeTreeNode, finalTypeTreeNode,
				scopeNameNodes, actualStartTypeNode, templateArguments))
			{
				assert(finalTypeTreeNode);
				result = finalTypeTreeNode;
			}
		}
	}
	else if (m_typeNode->isTemplateParameter())
	{
		assert(templateArguments);
		result = templateArguments->findTypeNode(m_scopeNameList->m_scopeName->m_name->m_str);
	}
	else if (m_typeNode->isTemplateClass())
	{
		assert(templateArguments);
		if (m_scopeNameList->m_scopeName->isTemplateForm())
		{
			result = g_typeTree.findNodeByScopeName(m_scopeNameList->m_scopeName, m_typeNode->m_enclosing, templateArguments);
		}
		else
		{
			assert(m_scopeNameList->m_scopeName->m_name->m_str == templateArguments->m_className);
			result = templateArguments->m_classTypeNode;
		}
	}
	else if (m_typeNode->isUnderTemplateClass())
	{
		assert(templateArguments);
		if (m_startTypeNode->isUnderTemplateClass())
		{
			std::vector<TypeNode*> typeNodes;
			TypeNode* typeNode = m_typeNode;
			while (typeNode)
			{
				if (typeNode->isTemplateClass())
				{
					break;
				}
				typeNodes.push_back(typeNode);
				typeNode = typeNode->m_enclosing;
			}
			assert(typeNode->isTemplateClass() && typeNode->m_name == templateArguments->m_className);
			typeNode = templateArguments->m_classTypeNode;
			auto it = typeNodes.rbegin();
			auto end = typeNodes.rend();
			for (; it != end; ++it)
			{
				TypeNode* tempTypeNode = *it;
				typeNode = typeNode->getChildNode(tempTypeNode->m_name);
				assert(typeNode);
			}
			if (typeNode->isTypedef())
			{
				TypeNode* actualTypeNode = typeNode->getActualTypeNode(templateArguments);
				if (actualTypeNode->isTemplateParameter())
				{
					typeNode = templateArguments->findTypeNode(actualTypeNode->m_name);
					assert(0 != typeNode);
				}
			}
			result = typeNode;
		}
		else
		{
			std::vector<ScopeNameNode*> scopeNameNodes;
			m_scopeNameList->collectIdentifyNodes(scopeNameNodes);
			TypeNode* initialTypeTreeNode = 0;
			TypeNode* finalTypeTreeNode = 0;
			if (m_startTypeNode->isTemplateClass() && !scopeNameNodes[0]->isTemplateForm())
			{
				assert(m_startTypeNode->m_name == templateArguments->m_className);
				scopeNameNodes.erase(scopeNameNodes.begin());
				if (g_typeTree.findNodeByScopeNames(initialTypeTreeNode, finalTypeTreeNode,
//.........这里部分代码省略.........

TypeCategory TemplateParameterTypeNode::getTypeCategory(TemplateArguments* templateArguments)
{
	TypeNode* actualTypeNode = templateArguments->findTypeNode(m_name);
	return actualTypeNode->getTypeCategory(templateArguments);

}

void TypeNodeProvider::value(Atlas::Message::Element& value, const TypeNode& type) const
{
    if (m_attribute_name == "name") {
        value = type.name();
    }
}

Node DtInstantiator::solve_dt(Node v, Node a, Node b, Node sa, Node sb)
{
  Trace("cegqi-arith-debug2") << "Solve dt : " << v << " " << a << " " << b
                              << " " << sa << " " << sb << std::endl;
  Node ret;
  if (!a.isNull() && a == v)
  {
    ret = sb;
  }
  else if (!b.isNull() && b == v)
  {
    ret = sa;
  }
  else if (!a.isNull() && a.getKind() == APPLY_CONSTRUCTOR)
  {
    if (!b.isNull() && b.getKind() == APPLY_CONSTRUCTOR)
    {
      if (a.getOperator() == b.getOperator())
      {
        for (unsigned i = 0, nchild = a.getNumChildren(); i < nchild; i++)
        {
          Node s = solve_dt(v, a[i], b[i], sa[i], sb[i]);
          if (!s.isNull())
          {
            return s;
          }
        }
      }
    }
    else
    {
      NodeManager* nm = NodeManager::currentNM();
      unsigned cindex = Datatype::indexOf(a.getOperator().toExpr());
      TypeNode tn = a.getType();
      const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
      for (unsigned i = 0, nchild = a.getNumChildren(); i < nchild; i++)
      {
        Node nn = nm->mkNode(
            APPLY_SELECTOR_TOTAL,
            Node::fromExpr(dt[cindex].getSelectorInternal(tn.toType(), i)),
            sb);
        Node s = solve_dt(v, a[i], Node::null(), sa[i], nn);
        if (!s.isNull())
        {
          return s;
        }
      }
    }
  }
  else if (!b.isNull() && b.getKind() == APPLY_CONSTRUCTOR)
  {
    // flip sides
    return solve_dt(v, b, a, sb, sa);
  }
  if (!ret.isNull())
  {
    // ensure does not contain v
    if (expr::hasSubterm(ret, v))
    {
      ret = Node::null();
    }
  }
  return ret;
}

    void setup()
    {
        m_inheritance = new Inheritance();
//Set up testing environment for Type/Soft properties
        m_b1 = new TestEntity("1", 1);
        add_entity(m_b1);

        m_thingType = new TypeNode("thing");
        types["thing"] = m_thingType;

        m_barrelType = new TypeNode("barrel");
        m_barrelType->setParent(m_thingType);
        types["barrel"] = m_barrelType;
        m_b1->setType(m_barrelType);
        m_b1->setProperty("mass", new SoftProperty(Element(30)));
        m_b1->setProperty("burn_speed", new SoftProperty(Element(0.3)));
        m_b1->setProperty("isVisible", new SoftProperty(Element(true)));

        m_b2 = new Entity("2", 2);
        add_entity(m_b2);
        m_b2->setProperty("mass", new SoftProperty(Element(20)));
        m_b2->setProperty("burn_speed", new SoftProperty(0.25));
        m_b2->setType(m_barrelType);
        m_b2->setProperty("isVisible", new SoftProperty(Element(false)));

        m_b3 = new Entity("3", 3);
        add_entity(m_b3);
        m_b3->setProperty("mass", new SoftProperty(Element(25)));
        m_b3->setProperty("burn_speed", new SoftProperty(Element(0.25)));
        m_b3->setType(m_barrelType);

        m_boulderType = new TypeNode("boulder");
        types["boulder"] = m_boulderType;
        m_bl1 = new Entity("4", 4);
        add_entity(m_bl1);
        m_bl1->setProperty("mass", new SoftProperty(Element(25)));
        m_bl1->setType(m_boulderType);

        SoftProperty* prop1 = new SoftProperty();
        prop1->set(std::vector<Element>{25.0, 20.0});
        m_bl1->setProperty("float_list", prop1);

        SoftProperty* list_prop2 = new SoftProperty();
        list_prop2->set(std::vector<Element>{"foo", "bar"});
        m_bl1->setProperty("string_list", list_prop2);

// Create an entity-related memory map
        Atlas::Message::MapType entity_memory_map{{"disposition", 25}};

        m_memory.emplace("1", entity_memory_map);

//b1 contains bl1 which contains b3
        m_b1_container = new LocatedEntitySet;
        m_b1_container->insert(m_bl1);
        m_bl1->m_location.m_parent = m_b1;
        m_b1->m_contains = m_b1_container;
        m_b1->test_setDomain(new TestDomain(*m_b1));

        m_bl1_container = new LocatedEntitySet;
        m_bl1_container->insert(m_b3);
        m_b3->m_location.m_parent = m_bl1;

        m_bl1->m_contains = m_bl1_container;

//Set up testing environment for Outfit property
        m_glovesType = new TypeNode("gloves");
        types["gloves"] = m_glovesType;
        m_bootsType = new TypeNode("boots");
        m_characterType = new TypeNode("character");
        types["character"] = m_characterType;
        TypeNode* m_clothType = new TypeNode("cloth");
        types["cloth"] = m_clothType;
        TypeNode* m_leatherType = new TypeNode("leather");

        m_glovesEntity = new Entity("5", 5);
        add_entity(m_glovesEntity);
        m_glovesEntity->setType(m_glovesType);
        m_glovesEntity->setProperty("color", new SoftProperty("brown"));
        m_glovesEntity->setProperty("mass", new SoftProperty(5));
        //Mark it with a "reach" so we can use it in the "can_reach ... with" tests
        auto reachProp = new Property<double>();
        reachProp->data() = 10.0f;
        m_glovesEntity->setProperty("reach", reachProp);

        m_bootsEntity = new Entity("6", 6);
        add_entity(m_bootsEntity);
        m_bootsEntity->setType(m_bootsType);
        m_bootsEntity->setProperty("color", new SoftProperty("black"));
        m_bootsEntity->setProperty("mass", new SoftProperty(10));


        m_cloth = new Entity("8", 8);
        add_entity(m_cloth);
        m_cloth->setType(m_clothType);
        m_cloth->setProperty("color", new SoftProperty("green"));

        m_leather = new Entity("9", 9);
        add_entity(m_leather);
        m_leather->setType(m_leatherType);
        m_leather->setProperty("color", new SoftProperty("pink"));
//.........这里部分代码省略.........

PreprocessingPassResult SygusAbduct::applyInternal(
    AssertionPipeline* assertionsToPreprocess)
{
  NodeManager* nm = NodeManager::currentNM();
  Trace("sygus-abduct") << "Run sygus abduct..." << std::endl;

  Trace("sygus-abduct-debug") << "Collect symbols..." << std::endl;
  std::unordered_set<Node, NodeHashFunction> symset;
  std::vector<Node>& asserts = assertionsToPreprocess->ref();
  // do we have any assumptions, e.g. via check-sat-assuming?
  bool usingAssumptions = (assertionsToPreprocess->getNumAssumptions() > 0);
  // The following is our set of "axioms". We construct this set only when the
  // usingAssumptions (above) is true. In this case, our input formula is
  // partitioned into Fa ^ Fc as described in the header of this class, where:
  // - The conjunction of assertions marked as assumptions are the negated
  // conjecture Fc, and
  // - The conjunction of all other assertions are the axioms Fa.
  std::vector<Node> axioms;
  for (size_t i = 0, size = asserts.size(); i < size; i++)
  {
    expr::getSymbols(asserts[i], symset);
    // if we are not an assumption, add it to the set of axioms
    if (usingAssumptions && i < assertionsToPreprocess->getAssumptionsStart())
    {
      axioms.push_back(asserts[i]);
    }
  }
  Trace("sygus-abduct-debug")
      << "...finish, got " << symset.size() << " symbols." << std::endl;

  Trace("sygus-abduct-debug") << "Setup symbols..." << std::endl;
  std::vector<Node> syms;
  std::vector<Node> vars;
  std::vector<Node> varlist;
  std::vector<TypeNode> varlistTypes;
  for (const Node& s : symset)
  {
    TypeNode tn = s.getType();
    if (tn.isFirstClass())
    {
      std::stringstream ss;
      ss << s;
      Node var = nm->mkBoundVar(tn);
      syms.push_back(s);
      vars.push_back(var);
      Node vlv = nm->mkBoundVar(ss.str(), tn);
      varlist.push_back(vlv);
      varlistTypes.push_back(tn);
    }
  }
  Trace("sygus-abduct-debug") << "...finish" << std::endl;

  Trace("sygus-abduct-debug") << "Make abduction predicate..." << std::endl;
  // make the abduction predicate to synthesize
  TypeNode abdType = varlistTypes.empty() ? nm->booleanType()
                                          : nm->mkPredicateType(varlistTypes);
  Node abd = nm->mkBoundVar("A", abdType);
  Trace("sygus-abduct-debug") << "...finish" << std::endl;

  Trace("sygus-abduct-debug") << "Make abduction predicate app..." << std::endl;
  std::vector<Node> achildren;
  achildren.push_back(abd);
  achildren.insert(achildren.end(), vars.begin(), vars.end());
  Node abdApp = vars.empty() ? abd : nm->mkNode(APPLY_UF, achildren);
  Trace("sygus-abduct-debug") << "...finish" << std::endl;

  Trace("sygus-abduct-debug") << "Set attributes..." << std::endl;
  // set the sygus bound variable list
  Node abvl = nm->mkNode(BOUND_VAR_LIST, varlist);
  abd.setAttribute(theory::SygusSynthFunVarListAttribute(), abvl);
  Trace("sygus-abduct-debug") << "...finish" << std::endl;

  Trace("sygus-abduct-debug") << "Make conjecture body..." << std::endl;
  Node input = asserts.size() == 1 ? asserts[0] : nm->mkNode(AND, asserts);
  input = input.substitute(syms.begin(), syms.end(), vars.begin(), vars.end());
  // A(x) => ~input( x )
  input = nm->mkNode(OR, abdApp.negate(), input.negate());
  Trace("sygus-abduct-debug") << "...finish" << std::endl;

  Trace("sygus-abduct-debug") << "Make conjecture..." << std::endl;
  Node res = input.negate();
  if (!vars.empty())
  {
    Node bvl = nm->mkNode(BOUND_VAR_LIST, vars);
    // exists x. ~( A( x ) => ~input( x ) )
    res = nm->mkNode(EXISTS, bvl, res);
  }
  // sygus attribute
  Node sygusVar = nm->mkSkolem("sygus", nm->booleanType());
  theory::SygusAttribute ca;
  sygusVar.setAttribute(ca, true);
  Node instAttr = nm->mkNode(INST_ATTRIBUTE, sygusVar);
  std::vector<Node> iplc;
  iplc.push_back(instAttr);
  if (!axioms.empty())
  {
    Node aconj = axioms.size() == 1 ? axioms[0] : nm->mkNode(AND, axioms);
    aconj =
        aconj.substitute(syms.begin(), syms.end(), vars.begin(), vars.end());
    Trace("sygus-abduct") << "---> Assumptions: " << aconj << std::endl;
//.........这里部分代码省略.........

bool TypeTree::checkTypeNameNode(TypeNode*& initialTypeTreeNode, TypeNode*& finalTypeTreeNode,
	ScopeNameListNode* scopeNameListNode, TypeNode* enclosingTypeTreeNode, TemplateArguments* templateArguments)
{
	assert(0 == templateArguments || templateArguments->m_classTypeNode->isTemplateClass());
	initialTypeTreeNode = 0;
	finalTypeTreeNode = 0;
	std::vector<ScopeNameNode*> scopeNameNodes;
	scopeNameListNode->collectIdentifyNodes(scopeNameNodes);
	assert(!scopeNameNodes.empty());

	if (0 != templateArguments && !scopeNameListNode->isGlobal())
	{
		ScopeNameNode* scopeNameNode = scopeNameNodes.front();
		if (!scopeNameNode->isTemplateForm())
		{
			if (scopeNameNode->m_name->m_str == templateArguments->m_className)
			{
				initialTypeTreeNode = templateArguments->m_classTypeNode;
				if (1 == scopeNameNodes.size())
				{
					//finalTypeTreeNode->isTemplateClass()
					finalTypeTreeNode = initialTypeTreeNode; 
					return true;
				}
				else
				{
					//0 == finalTypeTreeNode || finalTypeTreeNode->isUnderTemplateClass()
					scopeNameNodes.erase(scopeNameNodes.begin());
					TypeNode* tmpTypeNode = 0;
					return findNodeByScopeNames(tmpTypeNode, finalTypeTreeNode, scopeNameNodes, initialTypeTreeNode, 0);
				}
			}
			initialTypeTreeNode = templateArguments->findTypeNode(scopeNameNode->m_name->m_str);
			if(initialTypeTreeNode)
			{
				if (1 == scopeNameNodes.size())
				{
					//finalTypeTreeNode->isTemplateParameter()
					finalTypeTreeNode = initialTypeTreeNode;
				}
				else
				{
					finalTypeTreeNode = 0;
				}
				return true;
			}
		}
	}
	if (scopeNameListNode->isGlobal())
	{
		return findNodeByScopeNames(initialTypeTreeNode, finalTypeTreeNode, scopeNameNodes, getRootNamespaceTypeNode(), templateArguments);
	}

	TypeNode* enclosing = enclosingTypeTreeNode;
	while (enclosing)
	{
		if(findNodeByScopeNames(initialTypeTreeNode, finalTypeTreeNode, scopeNameNodes, enclosing, templateArguments))
		{
			return true;
		}		
		enclosing = enclosing->getEnclosing();
	}

	initialTypeTreeNode = 0;
	finalTypeTreeNode = 0;
	bool result = false;
	auto it = m_allNamespaces.begin();
	auto end = m_allNamespaces.end();
	for (; it != end; ++it)
	{
		TypeNode* tempInitialTypeTreeNode = 0;
		TypeNode* tempFinalTypeTreeNode = 0;
		if(findNodeByScopeNames(tempInitialTypeTreeNode, tempFinalTypeTreeNode, scopeNameNodes, *it, templateArguments))
		{
			if (result)
			{
				char buf[512];
				std::string str;
				scopeNameListNode->getString(str);
				sprintf_s(buf, "\'%s\' : ambiguous type name could be %s(%d, %d) or %s(%d, %d)",
					str.c_str(),
					finalTypeTreeNode->m_sourceFile->m_fileName.c_str(), 
					finalTypeTreeNode->m_identifyNode->m_lineNo, 
					finalTypeTreeNode->m_identifyNode->m_columnNo,
					tempFinalTypeTreeNode->m_sourceFile->m_fileName.c_str(), 
					tempFinalTypeTreeNode->m_identifyNode->m_lineNo,
					tempFinalTypeTreeNode->m_identifyNode->m_columnNo);
				ErrorList_AddItem_CurrentFile(scopeNameNodes.back()->m_name->m_lineNo,
					scopeNameNodes.back()->m_name->m_columnNo, semantic_error_ambiguous_type_name, buf);
				return false;
			}
			else
			{
				initialTypeTreeNode = tempInitialTypeTreeNode;
				finalTypeTreeNode = tempFinalTypeTreeNode;
				result = true;
			}
		}
	}
	if (!result)
//.........这里部分代码省略.........

void SortInference::simplify( std::vector< Node >& assertions, bool doSortInference, bool doMonotonicyInference ){
  if( doSortInference ){
    Trace("sort-inference-proc") << "Calculating sort inference..." << std::endl;
    NodeManager* nm = NodeManager::currentNM();
    //process all assertions
    std::map< Node, int > visited;
    for( unsigned i=0; i<assertions.size(); i++ ){
      Trace("sort-inference-debug") << "Process " << assertions[i] << std::endl;
      std::map< Node, Node > var_bound;
      process( assertions[i], var_bound, visited );
    }
    Trace("sort-inference-proc") << "...done" << std::endl;
    for( std::map< Node, int >::iterator it = d_op_return_types.begin(); it != d_op_return_types.end(); ++it ){
      Trace("sort-inference") << it->first << " : ";
      TypeNode retTn = it->first.getType();
      if( !d_op_arg_types[ it->first ].empty() ){
        Trace("sort-inference") << "( ";
        for( size_t i=0; i<d_op_arg_types[ it->first ].size(); i++ ){
          recordSubsort( retTn[i], d_op_arg_types[ it->first ][i] );
          printSort( "sort-inference", d_op_arg_types[ it->first ][i] );
          Trace("sort-inference") << " ";
        }
        Trace("sort-inference") << ") -> ";
        retTn = retTn[(int)retTn.getNumChildren()-1];
      }
      recordSubsort( retTn, it->second );
      printSort( "sort-inference", it->second );
      Trace("sort-inference") << std::endl;
    }
    for( std::map< Node, std::map< Node, int > >::iterator it = d_var_types.begin(); it != d_var_types.end(); ++it ){
      Trace("sort-inference") << "Quantified formula : " << it->first << " : " << std::endl;
      for( unsigned i=0; i<it->first[0].getNumChildren(); i++ ){
        recordSubsort( it->first[0][i].getType(), it->second[it->first[0][i]] );
        printSort( "sort-inference", it->second[it->first[0][i]] );
        Trace("sort-inference") << std::endl;
      }
      Trace("sort-inference") << std::endl;
    }

    bool rewritten = false;
    // determine monotonicity of sorts
    Trace("sort-inference-proc") << "Calculating monotonicty for subsorts..."
                                 << std::endl;
    std::map<Node, std::map<int, bool> > visitedm;
    for (const Node& a : assertions)
    {
      Trace("sort-inference-debug") << "Process monotonicity for " << a
                                    << std::endl;
      std::map<Node, Node> var_bound;
      processMonotonic(a, true, true, var_bound, visitedm);
    }
    Trace("sort-inference-proc") << "...done" << std::endl;

    Trace("sort-inference") << "We have " << d_sub_sorts.size()
                            << " sub-sorts : " << std::endl;
    for (unsigned i = 0, size = d_sub_sorts.size(); i < size; i++)
    {
      printSort("sort-inference", d_sub_sorts[i]);
      if (d_type_types.find(d_sub_sorts[i]) != d_type_types.end())
      {
        Trace("sort-inference") << " is interpreted." << std::endl;
      }
      else if (d_non_monotonic_sorts.find(d_sub_sorts[i])
               == d_non_monotonic_sorts.end())
      {
        Trace("sort-inference") << " is monotonic." << std::endl;
      }
      else
      {
        Trace("sort-inference") << " is not monotonic." << std::endl;
      }
    }

    // simplify all assertions by introducing new symbols wherever necessary
    Trace("sort-inference-proc") << "Perform simplification..." << std::endl;
    std::map<Node, std::map<TypeNode, Node> > visited2;
    for (unsigned i = 0, size = assertions.size(); i < size; i++)
    {
      Node prev = assertions[i];
      std::map<Node, Node> var_bound;
      Trace("sort-inference-debug") << "Simplify " << prev << std::endl;
      TypeNode tnn;
      Node curr = simplifyNode(assertions[i], var_bound, tnn, visited2);
      Trace("sort-inference-debug") << "Done." << std::endl;
      if (curr != assertions[i])
      {
        Trace("sort-inference-debug") << "Rewrite " << curr << std::endl;
        curr = theory::Rewriter::rewrite(curr);
        rewritten = true;
        Trace("sort-inference-rewrite") << assertions << std::endl;
        Trace("sort-inference-rewrite") << " --> " << curr << std::endl;
        PROOF(ProofManager::currentPM()->addDependence(curr, assertions[i]););
        assertions[i] = curr;
      }
    }

void SharedTermsVisitor::visit(TNode current, TNode parent) {

  Debug("register") << "SharedTermsVisitor::visit(" << current << "," << parent << ")" << std::endl;
  if (Debug.isOn("register::internal")) {
    Debug("register::internal") << toString() << std::endl;
  }

  // Get the theories of the terms
  TheoryId currentTheoryId = Theory::theoryOf(current);
  TheoryId parentTheoryId  = Theory::theoryOf(parent);

#if 0
  bool useType = current != parent && currentTheoryId != parentTheoryId;
#else
  // Should we use the theory of the type
  bool useType = false;
  TheoryId typeTheoryId = THEORY_LAST;

  if (current != parent) {
    if (currentTheoryId != parentTheoryId) {
      // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers
      TypeNode type = current.getType();
      useType = true;
      typeTheoryId = Theory::theoryOf(type);
    } else {
      TypeNode type = current.getType();
      typeTheoryId = Theory::theoryOf(type);
      if (typeTheoryId != currentTheoryId) {
        if (options::finiteModelFind() && type.isSort()) {
          // We're looking for finite models
          useType = true;
        } else {
          Cardinality card = type.getCardinality();
          if (card.isFinite()) {
            useType = true;
          }
        }
      }
    }
  }
#endif

  Theory::Set visitedTheories = d_visited[current];
  Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): previously registered with " << Theory::setToString(visitedTheories) << std::endl;
  if (!Theory::setContains(currentTheoryId, visitedTheories)) {
    visitedTheories = Theory::setInsert(currentTheoryId, visitedTheories);
    Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): adding " << currentTheoryId << std::endl;
  }
  if (!Theory::setContains(parentTheoryId, visitedTheories)) {
    visitedTheories = Theory::setInsert(parentTheoryId, visitedTheories);
    Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): adding " << parentTheoryId << std::endl;
  }
  if (useType) {
    //////TheoryId typeTheoryId = Theory::theoryOf(current.getType());
    if (!Theory::setContains(typeTheoryId, visitedTheories)) {
      visitedTheories = Theory::setInsert(typeTheoryId, visitedTheories);
      Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): adding " << typeTheoryId << std::endl;
    }
  }
  Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): now registered with " << Theory::setToString(visitedTheories) << std::endl;

  // Record the new theories that we visited
  d_visited[current] = visitedTheories;

  // If there is more than two theories and a new one has been added notify the shared terms database
  if (Theory::setDifference(visitedTheories, Theory::setInsert(currentTheoryId))) {
    d_sharedTerms.addSharedTerm(d_atom, current, visitedTheories);
  }

  Assert(d_visited.find(current) != d_visited.end());
  Assert(alreadyVisited(current, parent));
}

void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
{
  TheoryModel* tm = (TheoryModel*)m;

  // buildModel with fullModel = true should only be called once in any context
  Assert(!tm->d_modelBuilt);
  tm->d_modelBuilt = fullModel;

  // Reset model
  tm->reset();

  // Collect model info from the theories
  Trace("model-builder") << "TheoryEngineModelBuilder: Collect model info..." << std::endl;
  d_te->collectModelInfo(tm, fullModel);

  // Loop through all terms and make sure that assignable sub-terms are in the equality engine
  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &tm->d_equalityEngine );
  {
    NodeSet cache;
    for ( ; !eqcs_i.isFinished(); ++eqcs_i) {
      eq::EqClassIterator eqc_i = eq::EqClassIterator((*eqcs_i), &tm->d_equalityEngine);
      for ( ; !eqc_i.isFinished(); ++eqc_i) {
        checkTerms(*eqc_i, tm, cache);
      }
    }
  }

  Trace("model-builder") << "Collect representatives..." << std::endl;

  // Process all terms in the equality engine, store representatives for each EC
  std::map< Node, Node > assertedReps, constantReps;
  TypeSet typeConstSet, typeRepSet, typeNoRepSet;
  std::set< TypeNode > allTypes;
  eqcs_i = eq::EqClassesIterator(&tm->d_equalityEngine);
  for ( ; !eqcs_i.isFinished(); ++eqcs_i) {

    // eqc is the equivalence class representative
    Node eqc = (*eqcs_i);
    Trace("model-builder") << "Processing EC: " << eqc << endl;
    Assert(tm->d_equalityEngine.getRepresentative(eqc) == eqc);
    TypeNode eqct = eqc.getType();
    Assert(assertedReps.find(eqc) == assertedReps.end());
    Assert(constantReps.find(eqc) == constantReps.end());

    // Loop through terms in this EC
    Node rep, const_rep;
    eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, &tm->d_equalityEngine);
    for ( ; !eqc_i.isFinished(); ++eqc_i) {
      Node n = *eqc_i;
      Trace("model-builder") << "  Processing Term: " << n << endl;
      // Record as rep if this node was specified as a representative
      if (tm->d_reps.find(n) != tm->d_reps.end()){
        Assert(rep.isNull());
        rep = tm->d_reps[n];
        Assert(!rep.isNull() );
        Trace("model-builder") << "  Rep( " << eqc << " ) = " << rep << std::endl;
      }
      // Record as const_rep if this node is constant
      if (n.isConst()) {
        Assert(const_rep.isNull());
        const_rep = n;
        Trace("model-builder") << "  ConstRep( " << eqc << " ) = " << const_rep << std::endl;
      }
      //model-specific processing of the term
      tm->addTerm(n);
    }

    // Assign representative for this EC
    if (!const_rep.isNull()) {
      // Theories should not specify a rep if there is already a constant in the EC
      Assert(rep.isNull() || rep == const_rep);
      constantReps[eqc] = const_rep;
      typeConstSet.add(eqct.getBaseType(), const_rep);
    }
    else if (!rep.isNull()) {
      assertedReps[eqc] = rep;
      typeRepSet.add(eqct.getBaseType(), eqc);
      allTypes.insert(eqct);
    }
    else {
      typeNoRepSet.add(eqct, eqc);
      allTypes.insert(eqct);
    }
  }

  // Need to ensure that each EC has a constant representative.

  Trace("model-builder") << "Processing EC's..." << std::endl;

  TypeSet::iterator it;
  set<TypeNode>::iterator type_it;
  set<Node>::iterator i, i2;
  bool changed, unassignedAssignable, assignOne = false;
  set<TypeNode> evaluableSet;

  // Double-fixed-point loop
  // Outer loop handles a special corner case (see code at end of loop for details)
  for (;;) {

    // Inner fixed-point loop: we are trying to learn constant values for every EC.  Each time through this loop, we process all of the
//.........这里部分代码省略.........

void PrintEquelleASTVisitor::visit(TypeNode& node)
{
    std::cout << SymbolTable::equelleString(node.type());
}

Node RemoveITE::run(TNode node, std::vector<Node>& output,
                    IteSkolemMap& iteSkolemMap) {
  // Current node
  Debug("ite") << "removeITEs(" << node << ")" << endl;

  // The result may be cached already
  NodeManager *nodeManager = NodeManager::currentNM();
  ITECache::iterator i = d_iteCache.find(node);
  if(i != d_iteCache.end()) {
    Node cachedRewrite = (*i).second;
    Debug("ite") << "removeITEs: in-cache: " << cachedRewrite << endl;
    return cachedRewrite.isNull() ? Node(node) : cachedRewrite;
  }

  // If an ITE replace it
  if(node.getKind() == kind::ITE) {
    TypeNode nodeType = node.getType();
    if(!nodeType.isBoolean()) {
      // Make the skolem to represent the ITE
      Node skolem = nodeManager->mkSkolem("termITE_$$", nodeType, "a variable introduced due to term-level ITE removal");

      // The new assertion
      Node newAssertion =
        nodeManager->mkNode(kind::ITE, node[0], skolem.eqNode(node[1]),
                            skolem.eqNode(node[2]));
      Debug("ite") << "removeITEs(" << node << ") => " << newAssertion << endl;

      // Attach the skolem
      d_iteCache[node] = skolem;

      // Remove ITEs from the new assertion, rewrite it and push it to the output
      newAssertion = run(newAssertion, output, iteSkolemMap);
      iteSkolemMap[skolem] = output.size();
      output.push_back(newAssertion);

      // The representation is now the skolem
      return skolem;
    }
  }

  // If not an ITE, go deep
  if( node.getKind() != kind::FORALL &&
      node.getKind() != kind::EXISTS &&
      node.getKind() != kind::REWRITE_RULE ) {
    vector<Node> newChildren;
    bool somethingChanged = false;
    if(node.getMetaKind() == kind::metakind::PARAMETERIZED) {
      newChildren.push_back(node.getOperator());
    }
    // Remove the ITEs from the children
    for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) {
      Node newChild = run(*it, output, iteSkolemMap);
      somethingChanged |= (newChild != *it);
      newChildren.push_back(newChild);
    }

    // If changes, we rewrite
    if(somethingChanged) {
      Node cachedRewrite = nodeManager->mkNode(node.getKind(), newChildren);
      d_iteCache[node] = cachedRewrite;
      return cachedRewrite;
    } else {
      d_iteCache[node] = Node::null();
      return node;
    }
  } else {
    d_iteCache[node] = Node::null();
    return node;
  }
}

TypeNode exportTypeInternal(TypeNode n, NodeManager* from, NodeManager* to, ExprManagerMapCollection& vmap) {
  Debug("export") << "type: " << n << " " << n.getId() << std::endl;
  if(theory::kindToTheoryId(n.getKind()) == theory::THEORY_DATATYPES) {
    throw ExportUnsupportedException
      ("export of types belonging to theory of DATATYPES kinds unsupported");
  }
  if(n.getMetaKind() == kind::metakind::PARAMETERIZED &&
     n.getKind() != kind::SORT_TYPE) {
    throw ExportUnsupportedException
      ("export of PARAMETERIZED-kinded types (other than SORT_KIND) not supported");
  }
  if(n.getKind() == kind::TYPE_CONSTANT) {
    return to->mkTypeConst(n.getConst<TypeConstant>());
  } else if(n.getKind() == kind::BITVECTOR_TYPE) {
    return to->mkBitVectorType(n.getConst<BitVectorSize>());
  } else if(n.getKind() == kind::SUBRANGE_TYPE) {
    return to->mkSubrangeType(n.getSubrangeBounds());
  }
  Type from_t = from->toType(n);
  Type& to_t = vmap.d_typeMap[from_t];
  if(! to_t.isNull()) {
    Debug("export") << "+ mapped `" << from_t << "' to `" << to_t << "'" << std::endl;
    return *Type::getTypeNode(to_t);
  }
  NodeBuilder<> children(to, n.getKind());
  if(n.getKind() == kind::SORT_TYPE) {
    Debug("export") << "type: operator: " << n.getOperator() << std::endl;
    // make a new sort tag in target node manager
    Node sortTag = NodeBuilder<0>(to, kind::SORT_TAG);
    children << sortTag;
  }
  for(TypeNode::iterator i = n.begin(), i_end = n.end(); i != i_end; ++i) {
    Debug("export") << "type: child: " << *i << std::endl;
    children << exportTypeInternal(*i, from, to, vmap);
  }
  TypeNode out = children.constructTypeNode();// FIXME thread safety
  to_t = to->toType(out);
  return out;
}/* exportTypeInternal() */

TypeNode NodeManager::getDatatypeForTupleRecord(TypeNode t) {
  Assert(t.isTuple() || t.isRecord());

  //AJR: not sure why .getBaseType() was used in two cases below,
  //     disabling this, which is necessary to fix bug 605/667,
  //     which involves records of INT which were mapped to records of REAL below.
  TypeNode tOrig = t;
  if(t.isTuple()) {
    vector<TypeNode> v;
    bool changed = false;
    for(size_t i = 0; i < t.getNumChildren(); ++i) {
      TypeNode tn = t[i];
      TypeNode base;
      if(tn.isTuple() || tn.isRecord()) {
        base = getDatatypeForTupleRecord(tn);
      } else {
        base = tn;//.getBaseType();
      }
      changed = changed || (tn != base);
      v.push_back(base);
    }
    if(changed) {
      t = mkTupleType(v);
    }
  } else {
    const Record& r = t.getRecord();
    std::vector< std::pair<std::string, Type> > v;
    bool changed = false;
    const Record::FieldVector& fields = r.getFields();
    for(Record::FieldVector::const_iterator i = fields.begin(); i != fields.end(); ++i) {
      Type tn = (*i).second;
      Type base;
      if(tn.isTuple() || tn.isRecord()) {