bool EqualitySolver::NotifyClass::eqNotifyTriggerEquality(TNode equality, bool value) {
  BVDebug("bitvector::equality") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl;
  if (value) {
    return d_solver.storePropagation(equality);
  } else {
    return d_solver.storePropagation(equality.notNode());
  }
}

Node AbstractionModule::substituteArguments(TNode signature, TNode apply, unsigned& index, TNodeTNodeMap& seen) {
  if (seen.find(signature) != seen.end()) {
    return seen[signature]; 
  }
  
  if (signature.getKind() == kind::SKOLEM) {
    // return corresponding argument and increment counter
    seen[signature] = apply[index];
    return apply[index++]; 
  }

  if (signature.getNumChildren() == 0) {
    Assert (signature.getKind() != kind::VARIABLE &&
            signature.getKind() != kind::SKOLEM); 
    seen[signature] = signature;
    return signature; 
  }
  
  NodeBuilder<> builder(signature.getKind());
  if (signature.getMetaKind() == kind::metakind::PARAMETERIZED) {
    builder << signature.getOperator();
  }
  
  for (unsigned i = 0; i < signature.getNumChildren(); ++i) {
    Node child = substituteArguments(signature[i], apply, index, seen);
    builder << child; 
  }

  Node result = builder; 
  seen[signature]= result;

  return result;
}

bool CoreSolver::decomposeFact(TNode fact) {
  Debug("bv-slicer") << "CoreSolver::decomposeFact fact=" << fact << endl;
  // FIXME: are this the right things to assert?
  // assert decompositions since the equality engine does not know the semantics of
  // concat:
  //   a == a_1 concat ... concat a_k
  //   b == b_1 concat ... concat b_k
  TNode eq = fact.getKind() == kind::NOT? fact[0] : fact;

  TNode a = eq[0];
  TNode b = eq[1];
  Node new_a = getBaseDecomposition(a);
  Node new_b = getBaseDecomposition(b);

  Assert (utils::getSize(new_a) == utils::getSize(new_b) &&
          utils::getSize(new_a) == utils::getSize(a));

  NodeManager* nm = NodeManager::currentNM();
  Node a_eq_new_a = nm->mkNode(kind::EQUAL, a, new_a);
  Node b_eq_new_b = nm->mkNode(kind::EQUAL, b, new_b);

  bool ok = true;
  ok = assertFactToEqualityEngine(a_eq_new_a, utils::mkTrue());
  if (!ok) return false;
  ok = assertFactToEqualityEngine(b_eq_new_b, utils::mkTrue());
  if (!ok) return false;
  ok = assertFactToEqualityEngine(fact, fact);
  if (!ok) return false;

  if (fact.getKind() == kind::EQUAL) {
    // assert the individual equalities as well
    //    a_i == b_i
    if (new_a.getKind() == kind::BITVECTOR_CONCAT &&
        new_b.getKind() == kind::BITVECTOR_CONCAT) {

      Assert (new_a.getNumChildren() == new_b.getNumChildren());
      for (unsigned i = 0; i < new_a.getNumChildren(); ++i) {
        Node eq_i = nm->mkNode(kind::EQUAL, new_a[i], new_b[i]);
        ok = assertFactToEqualityEngine(eq_i, fact);
        if (!ok) return false;
      }
    }
  }
  return true;
}

bool InequalitySolver::isInequalityOnly(TNode node) {
    if (d_ineqOnlyCache.find(node) != d_ineqOnlyCache.end()) {
        return d_ineqOnlyCache[node];
    }

    if (node.getKind() == kind::NOT) {
        node = node[0];
    }

    if (node.getKind() != kind::EQUAL &&
            node.getKind() != kind::BITVECTOR_ULT &&
            node.getKind() != kind::BITVECTOR_ULE &&
            node.getKind() != kind::CONST_BITVECTOR &&
            node.getKind() != kind::SELECT &&
            node.getKind() != kind::STORE &&
            node.getMetaKind() != kind::metakind::VARIABLE) {
        return false;
    }
    bool res = true;
    for (unsigned i = 0; i < node.getNumChildren(); ++i) {
        res = res && isInequalityOnly(node[i]);
    }
    d_ineqOnlyCache[node] = res;
    return res;
}

void TDecisionTree::TNode::CopyNode(const TNode& Node) {
	CleanUp();

	CutFtrN = Node.CutFtrN;
	CutFtrVal = Node.CutFtrVal;
	NExamples = Node.NExamples;
	ClassHist = Node.ClassHist;
	FtrHist = Node.FtrHist;

	if (Node.HasLeft()) {
		Left = new TNode(Tree);
		Left->CopyNode(*Node.Left);
	}
	if (Node.HasRight()) {
		Right = new TNode(Tree);
		Right->CopyNode(*Node.Right);
	}
}

void Relevancy::setJustified(TNode n)
{
  Debug("decision") << " marking [" << n.getId() << "]"<< n << "as justified" << std::endl;
  d_justified.insert(n);
  if(options::decisionComputeRelevancy()) {
    d_relevancy[n] = d_maxRelevancy[n];
    updateRelevancy(n);
  }
}

void InequalitySolver::preRegister(TNode node) {
  Kind kind = node.getKind(); 
  if (kind == kind::EQUAL ||
      kind == kind::BITVECTOR_ULE ||
      kind == kind::BITVECTOR_ULT) {
    d_ineqTerms.insert(node[0]);
    d_ineqTerms.insert(node[1]);
  }
}

void TheoryQuantifiers::preRegisterTerm(TNode n) {
  Debug("quantifiers-prereg") << "TheoryQuantifiers::preRegisterTerm() " << n << endl;
  if( n.getKind()==FORALL ){
    if( !options::cbqi() || options::recurseCbqi() || !TermUtil::hasInstConstAttr(n) ){
      getQuantifiersEngine()->registerQuantifier( n );
      Debug("quantifiers-prereg") << "TheoryQuantifiers::preRegisterTerm() done " << n << endl;
    }
  }
}

Node TheoryBuiltinRewriter::blastChain(TNode in) {

  Assert(in.getKind() == kind::CHAIN);

  Kind chainedOp = in.getOperator().getConst<Chain>().getOperator();

  if(in.getNumChildren() == 2) {
    // if this is the case exactly 1 pair will be generated so the
    // AND is not required
    return NodeManager::currentNM()->mkNode(chainedOp, in[0], in[1]);
  } else {
    NodeBuilder<> conj(kind::AND);
    for(TNode::iterator i = in.begin(), j = i + 1; j != in.end(); ++i, ++j) {
      conj << NodeManager::currentNM()->mkNode(chainedOp, *i, *j);
    }
    return conj;
  }
}

vector<string> QueryEvaluator::getSymbolsUsedBy(TNode * node) {
	vector<string> results;

	int size = node->getNumChildren();
	for (int i=0; i<size; i++) {
		TNode * child = node->getChildAtIndex(i);
		if (child->getType()==QuerySymbol) {
			results.push_back(child->getValue());
		}
		vector<string> sub_results = getSymbolsUsedBy(child);
		for (size_t j=0; j<sub_results.size(); j++) {
			if (find(results.begin(), results.end(), sub_results[j])==results.end())
				results.push_back(sub_results[j]);
		}
 	}

	return results;
}

bool AbstractionModule::isConjunctionOfAtomsRec(TNode node, TNodeSet& seen) {
  if (seen.find(node)!= seen.end())
    return true;
  
  if (!node.getType().isBitVector()) {
    return (node.getKind() == kind::AND || utils::isBVPredicate(node));
  }

  if (node.getNumChildren() == 0)
    return true;

  for (unsigned i = 0; i < node.getNumChildren(); ++i) {
    if (!isConjunctionOfAtomsRec(node[i], seen))
      return false;
  }
  seen.insert(node);
  return true;
}

bool SharedTermsDatabase::isKnown(TNode literal) const {
  bool polarity = literal.getKind() != kind::NOT;
  TNode equality = polarity ? literal : literal[0];
  if (polarity) {
    return d_equalityEngine.areEqual(equality[0], equality[1]);
  } else {
    return d_equalityEngine.areDisequal(equality[0], equality[1], false);
  }
}

/**
* return value as the model suggested. The history state must be historified
* or the history's level should be 0. when level == 0 but idx != 0, the
* history is a psuedo unigram state used for this model to combine another
* bigram cache language model
*/
double
CThreadSlm::rawTransfer(TState history, unsigned int wid, TState& result)
{
    unsigned int lvl = history.getLevel();
    unsigned int pos = history.getIdx();

    double cost = (m_UseLogPr)?0.0:1.0;

    // NON_Word id must be dealed with special, let it transfer to root
    // without any cost
    if (ID_NOT_WORD == wid) {
        result = 0;
        return cost;
    }

    while (true) {
        //for psuedo cache model unigram state
        TNode* pn = ((TNode *)m_Levels[lvl]) + ((lvl)?pos:0);

        unsigned int t = (pn+1)->ch();

        if (lvl < m_N-1) {
            TNode* pBase =(TNode*)m_Levels[lvl+1];
            unsigned int idx = find_id(pBase, pn->ch(), t, wid);
            if (idx != t) {
                result.setIdx(idx);
                result.setLevel(lvl+1);
                double pr = m_prTable[pBase[idx].pr()];
                return (m_UseLogPr)?(cost+pr):(cost*pr);
            }

        } else {
            TLeaf* pBase =(TLeaf*)m_Levels[lvl+1];
            unsigned int idx = find_id(pBase, pn->ch(), t, wid);
            if (idx != t) {
                result.setIdx(idx);
                result.setLevel(lvl+1);
                double pr = m_prTable[pBase[idx].pr()];
                return (m_UseLogPr)?(cost+pr):(cost*pr);
            }

        }

        if (m_UseLogPr)
            cost += m_bowTable[pn->bow()];
        else
            cost *= m_bowTable[pn->bow()];
        if (lvl == 0)
            break;
        lvl = pn->bol();
        pos = pn->bon();
    }
    result.setLevel(0);
    result.setIdx(0);
    if (m_UseLogPr)
        return cost + m_prTable[((TNode *)m_Levels[0])->pr()];
    else
        return cost * m_prTable[((TNode *)m_Levels[0])->pr()];
}

Node TheoryUF::ppRewrite(TNode node) {

  if (node.getKind() != kind::APPLY_UF) {
    return node;
  }

  // perform the callbacks requested by TheoryUF::registerPpRewrite()
  RegisterPpRewrites::iterator c = d_registeredPpRewrites.find(node.getOperator());
  if (c == d_registeredPpRewrites.end()) {
    return node;
  } else {
    Node res = c->second->ppRewrite(node);
    if (res != node) {
      return ppRewrite(res);
    } else {
      return res;
    }
  }
}

bool BvToBoolPreprocessor::isConvertibleBvTerm(TNode node) {
  if (!node.getType().isBitVector() ||
      node.getType().getBitVectorSize() != 1)
    return false;

  Kind kind = node.getKind();
  
  if (kind == kind::CONST_BITVECTOR ||
      kind == kind::ITE ||
      kind == kind::BITVECTOR_AND ||
      kind == kind::BITVECTOR_OR ||
      kind == kind::BITVECTOR_NOT ||
      kind == kind::BITVECTOR_XOR ||
      kind == kind::BITVECTOR_COMP) {
    return true; 
  }

  return false; 
}

bool BvToBoolPreprocessor::isConvertibleBvAtom(TNode node) {
  Kind kind = node.getKind();
  return (kind == kind::EQUAL &&
          node[0].getType().isBitVector() &&
          node[0].getType().getBitVectorSize() == 1 &&
          node[1].getType().isBitVector() &&
          node[1].getType().getBitVectorSize() == 1 &&
          node[0].getKind() != kind::BITVECTOR_EXTRACT &&
          node[1].getKind() != kind::BITVECTOR_EXTRACT); 
}

// static
RewriteResponse TheorySetsRewriter::preRewrite(TNode node) {
  NodeManager* nm = NodeManager::currentNM();

  // do nothing
  if(node.getKind() == kind::EQUAL && node[0] == node[1])
    return RewriteResponse(REWRITE_DONE, nm->mkConst(true));
  // Further optimization, if constants but differing ones

  return RewriteResponse(REWRITE_DONE, node);
}

void EqualitySolver::preRegister(TNode node) {
  if (!d_useEqualityEngine)
    return;

  if (node.getKind() == kind::EQUAL) {
      d_equalityEngine.addTriggerEquality(node);
  } else {
    d_equalityEngine.addTerm(node);
  }
}

bool BVQuickCheck::addAssertion(TNode assertion) {
  Assert (assertion.getType().isBoolean());
  d_bitblaster->bbAtom(assertion);
  // assert to sat solver and run bcp to detect easy conflicts
  bool ok = d_bitblaster->assertToSat(assertion, true);
  if (!ok) {
    setConflict();
  }
  return ok;
}

void ExtractSkolemizer::storeExtract(TNode var, unsigned high, unsigned low) {
  Assert (var.getMetaKind() == kind::metakind::VARIABLE);
  if (d_varToExtract.find(var) == d_varToExtract.end()) {
    d_varToExtract[var] = ExtractList(utils::getSize(var));
  }
  VarExtractMap::iterator it = d_varToExtract.find(var);
  ExtractList& el = it->second;
  Extract e(high, low);
  el.addExtract(e);
}