/*********************                                                        */
/*! \file theory_strings.cpp
 ** \verbatim
 ** Original author: Tianyi Liang
 ** Major contributors: Tianyi Liang, Andrew Reynolds
 ** Minor contributors (to current version): none
 ** This file is part of the CVC4 prototype.
 ** Copyright (c) 2013-2013  New York University and The University of Iowa
 ** See the file COPYING in the top-level source directory for licensing
 ** information.\endverbatim
 **
 ** \brief Implementation of the theory of strings.
 **
 ** Implementation of the theory of strings.
 **/


#include "theory/strings/theory_strings.h"
#include "theory/valuation.h"
#include "expr/kind.h"
#include "theory/rewriter.h"
#include "expr/command.h"
#include "theory/model.h"
#include "smt/logic_exception.h"
#include "theory/strings/options.h"
#include "theory/strings/type_enumerator.h"
#include <cmath>

#define STR_UNROLL_INDUCTION

using namespace std;
using namespace CVC4::context;

namespace CVC4 {
namespace theory {
namespace strings {

TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe)
    : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo, qe),
    d_notify( *this ),
    d_equalityEngine(d_notify, c, "theory::strings::TheoryStrings"),
    d_conflict( c, false ),
    d_infer(c),
    d_infer_exp(c),
    d_nf_pairs(c),
    d_ind_map1(c),
    d_ind_map2(c),
    d_ind_map_exp(c),
    d_ind_map_lemma(c),
	//d_lit_to_decide_index( c, 0 ),
	//d_lit_to_decide( c ),
	d_lit_to_unroll( c )
{
    // The kinds we are treating as function application in congruence
    d_equalityEngine.addFunctionKind(kind::STRING_IN_REGEXP);
    d_equalityEngine.addFunctionKind(kind::STRING_LENGTH);
    d_equalityEngine.addFunctionKind(kind::STRING_CONCAT);

    d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) );
    d_emptyString = NodeManager::currentNM()->mkConst( ::CVC4::String("") );
    d_true = NodeManager::currentNM()->mkConst( true );
    d_false = NodeManager::currentNM()->mkConst( false );
}

TheoryStrings::~TheoryStrings() {

}

Node TheoryStrings::getRepresentative( Node t ) {
	if( d_equalityEngine.hasTerm( t ) ){
		return d_equalityEngine.getRepresentative( t );
	}else{
		return t;
	}
}

bool TheoryStrings::hasTerm( Node a ){
  return d_equalityEngine.hasTerm( a );
}

bool TheoryStrings::areEqual( Node a, Node b ){
  if( a==b ){
    return true;
  }else if( hasTerm( a ) && hasTerm( b ) ){
    return d_equalityEngine.areEqual( a, b );
  }else{
    return false;
  }
}

bool TheoryStrings::areDisequal( Node a, Node b ){
  if( hasTerm( a ) && hasTerm( b ) ){
    return d_equalityEngine.areDisequal( a, b, false );
  }else{
    return false;
  }
}

Node TheoryStrings::getLength( Node t ) {
	EqcInfo * ei = getOrMakeEqcInfo( t );
	Node length_term = ei->d_length_term;
	if( length_term.isNull()) {
		//typically shouldnt be necessary
		length_term = t;
	}
	return NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, length_term );
}

void TheoryStrings::setMasterEqualityEngine(eq::EqualityEngine* eq) {
  d_equalityEngine.setMasterEqualityEngine(eq);
}

void TheoryStrings::addSharedTerm(TNode t) {
  Debug("strings") << "TheoryStrings::addSharedTerm(): "
                     << t << " " << t.getType().isBoolean() << endl;
  d_equalityEngine.addTriggerTerm(t, THEORY_STRINGS);
  Debug("strings") << "TheoryStrings::addSharedTerm() finished" << std::endl;
}

EqualityStatus TheoryStrings::getEqualityStatus(TNode a, TNode b) {
  if( d_equalityEngine.hasTerm(a) && d_equalityEngine.hasTerm(b) ){
    if (d_equalityEngine.areEqual(a, b)) {
      // The terms are implied to be equal
      return EQUALITY_TRUE;
    }
    if (d_equalityEngine.areDisequal(a, b, false)) {
      // The terms are implied to be dis-equal
      return EQUALITY_FALSE;
    }
  }
  return EQUALITY_UNKNOWN;
}

void TheoryStrings::propagate(Effort e)
{
  // direct propagation now
}

bool TheoryStrings::propagate(TNode literal) {
  Debug("strings-propagate") << "TheoryStrings::propagate(" << literal  << ")" << std::endl;
  // If already in conflict, no more propagation
  if (d_conflict) {
    Debug("strings-propagate") << "TheoryStrings::propagate(" << literal << "): already in conflict" << std::endl;
    return false;
  }
  Trace("strings-prop") << "strPropagate " << literal << std::endl;
  // Propagate out
  bool ok = d_out->propagate(literal);
  if (!ok) {
    d_conflict = true;
  }
  return ok;
}

/** explain */
void TheoryStrings::explain(TNode literal, std::vector<TNode>& assumptions){
  Debug("strings-explain") << "Explain " << literal << std::endl;
  bool polarity = literal.getKind() != kind::NOT;
  TNode atom = polarity ? literal : literal[0];
  if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) {
    d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions);
  } else {
    d_equalityEngine.explainPredicate(atom, polarity, assumptions);
  }
}

Node TheoryStrings::explain( TNode literal ){
  std::vector< TNode > assumptions;
  explain( literal, assumptions );
  if( assumptions.empty() ){
    return d_true;
  }else if( assumptions.size()==1 ){
    return assumptions[0];
  }else{
    return NodeManager::currentNM()->mkNode( kind::AND, assumptions );
  }
}

/////////////////////////////////////////////////////////////////////////////
// MODEL GENERATION
/////////////////////////////////////////////////////////////////////////////


void TheoryStrings::collectModelInfo( TheoryModel* m, bool fullModel ) {
	Trace("strings-model") << "TheoryStrings : Collect model info, fullModel = " << fullModel << std::endl;
	Trace("strings-model") << "TheoryStrings : assertEqualityEngine." << std::endl;
	m->assertEqualityEngine( &d_equalityEngine );
    // Generate model
	std::vector< Node > nodes;
	getEquivalenceClasses( nodes );
	std::map< Node, Node > processed;
	std::vector< std::vector< Node > > col;
	std::vector< Node > lts;
	seperateByLength( nodes, col, lts );
	//step 1 : get all values for known lengths
	std::vector< Node > lts_values;
	//std::map< Node, bool > values_used;
	for( unsigned i=0; i<col.size(); i++ ){
		Trace("strings-model") << "Checking length for " << col[i][0] << " (length is " << lts[i] << ")" << std::endl;
		if( lts[i].isConst() ){
			lts_values.push_back( lts[i] );
			//values_used[ lts[i] ] = true;
		}else{
			//get value for lts[i];
			if( !lts[i].isNull() ){
				Node v = d_valuation.getModelValue(lts[i]);
				//Node v = m->getValue(lts[i]);
				Trace("strings-model") << "Model value for " << lts[i] << " is " << v << std::endl;
				lts_values.push_back( v );
				//values_used[ v ] = true;
			}else{
				Trace("strings-model-warn") << "No length for eqc " << col[i][0] << std::endl;
				Assert( false );
				lts_values.push_back( Node::null() );
			}
		}
	}
	////step 2 : assign arbitrary values for unknown lengths?
	//for( unsigned i=0; i<col.size(); i++ ){
	//	if( 
	//}
	Trace("strings-model") << "Assign to equivalence classes..." << std::endl;
	//step 3 : assign values to equivalence classes that are pure variables
	for( unsigned i=0; i<col.size(); i++ ){
		std::vector< Node > pure_eq;
		Trace("strings-model") << "The equivalence classes ";
		for( unsigned j=0; j<col[i].size(); j++ ) {
			Trace("strings-model") << col[i][j] << " ";
			//check if col[i][j] has only variables
			EqcInfo* ei = getOrMakeEqcInfo( col[i][j], false );
            Node cst = ei ? ei->d_const_term : Node::null();
			if( cst.isNull() ){
				Assert( d_normal_forms.find( col[i][j] )!=d_normal_forms.end() );
				if( d_normal_forms[col[i][j]].size()==1 ){//&& d_normal_forms[col[i][j]][0]==col[i][j] ){
					pure_eq.push_back( col[i][j] );
				}
			}else{
				processed[col[i][j]] = cst;
			}
		}
		Trace("strings-model") << "have length " << lts_values[i] << std::endl;
		
		Trace("strings-model") << "Need to assign values of length " << lts_values[i] << " to equivalence classes ";
		for( unsigned j=0; j<pure_eq.size(); j++ ){
			Trace("strings-model") << pure_eq[j] << " ";
		}
		Trace("strings-model") << std::endl;

		//use type enumerator
		StringEnumeratorLength sel(lts_values[i].getConst<Rational>().getNumerator().toUnsignedInt());
		for( unsigned j=0; j<pure_eq.size(); j++ ){
			Assert( !sel.isFinished() );
			Node c = *sel;
			while( d_equalityEngine.hasTerm( c ) ){
				++sel;
				Assert( !sel.isFinished() );
				c = *sel;
			}
			++sel;
			Trace("strings-model") << "*** Assigned constant " << c << " for " << pure_eq[j] << std::endl;
			processed[pure_eq[j]] = c;
			m->assertEquality( pure_eq[j], c, true );
		}
	}
	Trace("strings-model") << "String Model : Finished." << std::endl;
	//step 4 : assign constants to all other equivalence classes
	for( unsigned i=0; i<nodes.size(); i++ ){
		if( processed.find( nodes[i] )==processed.end() ){
			Assert( d_normal_forms.find( nodes[i] )!=d_normal_forms.end() );
			Trace("strings-model") << "Construct model for " << nodes[i] << " based on normal form ";
			for( unsigned j=0; j<d_normal_forms[nodes[i]].size(); j++ ) {
				if( j>0 ) Trace("strings-model") << " ++ ";
				Trace("strings-model") << d_normal_forms[nodes[i]][j];
				Node r = getRepresentative( d_normal_forms[nodes[i]][j] );
				if( !r.isConst() && processed.find( r )==processed.end() ){
					Trace("strings-model") << "(UNPROCESSED)";
				}
			}
			Trace("strings-model") << std::endl;
			std::vector< Node > nc;
			for( unsigned j=0; j<d_normal_forms[nodes[i]].size(); j++ ) {
				Node r = getRepresentative( d_normal_forms[nodes[i]][j] );
				Assert( r.isConst() || processed.find( r )!=processed.end() );
				nc.push_back(r.isConst() ? r : processed[r]);
			}
			Node cc = mkConcat( nc );
			Assert( cc.getKind()==kind::CONST_STRING );
			Trace("strings-model") << "*** Determined constant " << cc << " for " << nodes[i] << std::endl;
			processed[nodes[i]] = cc;
			m->assertEquality( nodes[i], cc, true );
		}
	}
}

/////////////////////////////////////////////////////////////////////////////
// MAIN SOLVER
/////////////////////////////////////////////////////////////////////////////

void TheoryStrings::preRegisterTerm(TNode n) {
  Debug("strings-prereg") << "TheoryStrings::preRegisterTerm() " << n << endl;
  //collectTerms( n );
  switch (n.getKind()) {
  case kind::EQUAL:
    d_equalityEngine.addTriggerEquality(n);
    break;
  case kind::STRING_IN_REGEXP:
    d_equalityEngine.addTriggerPredicate(n);
    break;
  default:
    if(n.getKind() == kind::VARIABLE || n.getKind()==kind::SKOLEM) {
	  if( std::find( d_length_intro_vars.begin(), d_length_intro_vars.end(), n )==d_length_intro_vars.end() ){
		  Node n_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n);
		  Node n_len_geq_zero = NodeManager::currentNM()->mkNode( kind::GEQ, n_len, d_zero);
		  Trace("strings-lemma") << "Strings: Add lemma " << n_len_geq_zero << std::endl;
		  d_out->lemma(n_len_geq_zero);
	  }
    }
    if (n.getType().isBoolean()) {
      // Get triggered for both equal and dis-equal
      d_equalityEngine.addTriggerPredicate(n);
    } else {
      // Function applications/predicates
      d_equalityEngine.addTerm(n);
    }
    break;
  }
}

void TheoryStrings::check(Effort e) {
  bool polarity;
  TNode atom;

  if( !done() && !hasTerm( d_emptyString ) ){
	 preRegisterTerm( d_emptyString );
  }

 // Trace("strings-process") << "Theory of strings, check : " << e << std::endl;
  Trace("strings-check") << "Theory of strings, check : " << e << std::endl;
  while ( !done() && !d_conflict)
  {
    // Get all the assertions
    Assertion assertion = get();
    TNode fact = assertion.assertion;

    Trace("strings-assertion") << "get assertion: " << fact << endl;

    polarity = fact.getKind() != kind::NOT;
    atom = polarity ? fact : fact[0];
    if (atom.getKind() == kind::EQUAL) {
      d_equalityEngine.assertEquality(atom, polarity, fact);
    } else {
      d_equalityEngine.assertPredicate(atom, polarity, fact);
    }
#ifdef STR_UNROLL_INDUCTION
	//check if it is a literal to unroll?
	if( d_lit_to_unroll.find( atom )!=d_lit_to_unroll.end() ){
		Trace("strings-ind") << "Strings-ind : Possibly unroll for : " << atom << ", polarity = " << polarity << std::endl;
	}
#endif
  }
  doPendingFacts();


  bool addedLemma = false;
  if( e == EFFORT_FULL && !d_conflict ) {
      eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
      while( !eqcs_i.isFinished() ){
        Node eqc = (*eqcs_i);
        //if eqc.getType is string
        if (eqc.getType().isString()) {
            //EqcInfo* ei = getOrMakeEqcInfo( eqc, true );
            //get the constant for the equivalence class
            //int c_len = ...;
            eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
            while( !eqc_i.isFinished() ){
              Node n = (*eqc_i);

              //if n is concat, and
              //if n has not instantiatied the concat..length axiom
              //then, add lemma
              if( n.getKind() == kind::STRING_CONCAT || n.getKind() == kind::CONST_STRING ){
                if( d_length_inst.find(n)==d_length_inst.end() ){
                    d_length_inst[n] = true;
                    Trace("strings-debug") << "get n: " << n << endl;
                    Node sk = NodeManager::currentNM()->mkSkolem( "lsym_$$", n.getType(), "created for concat lemma" );
					d_length_intro_vars.push_back( sk );
                    Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, sk, n );
                    eq = Rewriter::rewrite(eq);
                    Trace("strings-lemma") << "Strings: Add lemma " << eq << std::endl;
                    d_out->lemma(eq);
                    Node skl = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk );
                    Node lsum;
                    if( n.getKind() == kind::STRING_CONCAT ){
                        //add lemma
                        std::vector<Node> node_vec;
                        for( unsigned i=0; i<n.getNumChildren(); i++ ) {
                            Node lni = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[i] );
                            node_vec.push_back(lni);
                        }
                        lsum = NodeManager::currentNM()->mkNode( kind::PLUS, node_vec );
                    }else{
                        //add lemma
                        lsum = NodeManager::currentNM()->mkConst( ::CVC4::Rational( n.getConst<String>().size() ) );
                    }
                    Node ceq = NodeManager::currentNM()->mkNode( kind::EQUAL, skl, lsum );
                    ceq = Rewriter::rewrite(ceq);
                    Trace("strings-lemma") << "Strings: Add lemma " << ceq << std::endl;
                    d_out->lemma(ceq);
                    addedLemma = true;
                }
              }
              ++eqc_i;
            }
        }
        ++eqcs_i;
  }
  if( !addedLemma ){
      addedLemma = checkNormalForms();
	  Trace("strings-process") << "Done check normal forms, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
      if(!d_conflict && !addedLemma) {
          addedLemma = checkCardinality();
		  Trace("strings-process") << "Done check cardinality, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
          if( !d_conflict && !addedLemma ){
            addedLemma = checkInductiveEquations();
			Trace("strings-process") << "Done check inductive equations, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
          }
      }
  }
  }
  Trace("strings-process") << "Theory of strings, done check : " << e << std::endl;
}

TheoryStrings::EqcInfo::EqcInfo(  context::Context* c ) : d_const_term(c), d_length_term(c), d_cardinality_lem_k(c) {

}

TheoryStrings::EqcInfo * TheoryStrings::getOrMakeEqcInfo( Node eqc, bool doMake ) {
  std::map< Node, EqcInfo* >::iterator eqc_i = d_eqc_info.find( eqc );
  if( eqc_i==d_eqc_info.end() ){
    if( doMake ){
      EqcInfo* ei = new EqcInfo( getSatContext() );
      d_eqc_info[eqc] = ei;
      return ei;
    }else{
      return NULL;
    }
  }else{
    return (*eqc_i).second;
  }
}


/** Conflict when merging two constants */
void TheoryStrings::conflict(TNode a, TNode b){
  Node conflictNode;
  if (a.getKind() == kind::CONST_BOOLEAN) {
    conflictNode = explain( a.iffNode(b) );
  } else {
    conflictNode = explain( a.eqNode(b) );
  }
  Debug("strings-conflict") << "CONFLICT: Eq engine conflict : " << conflictNode << std::endl;
  d_out->conflict( conflictNode );
  d_conflict = true;
}

/** called when a new equivalance class is created */
void TheoryStrings::eqNotifyNewClass(TNode t){
  if( t.getKind() == kind::CONST_STRING ){
    EqcInfo * ei =getOrMakeEqcInfo( t, true );
    ei->d_const_term = t;
  }
  if( t.getKind() == kind::STRING_LENGTH ){
    Trace("strings-debug") << "New length eqc : " << t << std::endl;
    Node r = d_equalityEngine.getRepresentative(t[0]);
    EqcInfo * ei = getOrMakeEqcInfo( r, true );
    ei->d_length_term = t[0];
  }
}

/** called when two equivalance classes will merge */
void TheoryStrings::eqNotifyPreMerge(TNode t1, TNode t2){
    EqcInfo * e2 = getOrMakeEqcInfo(t2, false);
    if( e2 ){
        EqcInfo * e1 = getOrMakeEqcInfo( t1 );
        //add information from e2 to e1
        if( !e2->d_const_term.get().isNull() ){
            e1->d_const_term.set( e2->d_const_term );
        }
        if( !e2->d_length_term.get().isNull() ){
            e1->d_length_term.set( e2->d_length_term );
        }
        if( e2->d_cardinality_lem_k.get()>e1->d_cardinality_lem_k.get() ) {
            e1->d_cardinality_lem_k.set( e2->d_cardinality_lem_k );
        }
    }
    if( hasTerm( d_zero ) ){
        Node leqc;
        if( areEqual(d_zero, t1) ){
            leqc = t2;
        }else if( areEqual(d_zero, t2) ){
            leqc = t1;
        }
        if( !leqc.isNull() ){
            //scan equivalence class to see if we apply
            eq::EqClassIterator eqc_i = eq::EqClassIterator( leqc, &d_equalityEngine );
            while( !eqc_i.isFinished() ){
              Node n = (*eqc_i);
              if( n.getKind()==kind::STRING_LENGTH ){
                if( !hasTerm( d_emptyString ) || !areEqual(n[0], d_emptyString ) ){
                    //apply the rule length(n[0])==0 => n[0] == ""
                    Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, n[0], d_emptyString );
                    d_pending.push_back( eq );
                    Node eq_exp = NodeManager::currentNM()->mkNode( kind::EQUAL, n, d_zero );
                    d_pending_exp[eq] = eq_exp;
                    Trace("strings-infer") << "Strings : Infer " << eq << " from " << eq_exp << std::endl;
                    d_infer.push_back(eq);
                    d_infer_exp.push_back(eq_exp);
                }
              }
              ++eqc_i;
            }
        }
    }
}

/** called when two equivalance classes have merged */
void TheoryStrings::eqNotifyPostMerge(TNode t1, TNode t2) {

}

/** called when two equivalance classes are disequal */
void TheoryStrings::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {

}

void TheoryStrings::computeCareGraph(){
  Theory::computeCareGraph();
}

void TheoryStrings::doPendingFacts() {
  int i=0;
  while( !d_conflict && i<(int)d_pending.size() ){
    Node fact = d_pending[i];
    Node exp = d_pending_exp[ fact ];
      Trace("strings-pending") << "Process pending fact : " << fact << " from " << exp << std::endl;
      bool polarity = fact.getKind() != kind::NOT;
      TNode atom = polarity ? fact : fact[0];
      if (atom.getKind() == kind::EQUAL) {
		Assert( d_equalityEngine.hasTerm( atom[0] ) );
		Assert( d_equalityEngine.hasTerm( atom[1] ) );
		d_equalityEngine.assertEquality( atom, polarity, exp );
      }else{
        d_equalityEngine.assertPredicate( atom, polarity, exp );
      }
    i++;
  }
  d_pending.clear();
  d_pending_exp.clear();
}
void TheoryStrings::doPendingLemmas() {
  if( !d_conflict && !d_lemma_cache.empty() ){
	  for( unsigned i=0; i<d_lemma_cache.size(); i++ ){
		  Trace("strings-pending") << "Process pending lemma : " << d_lemma_cache[i] << std::endl;
		  d_out->lemma( d_lemma_cache[i] );
	  }
	  for( std::map< Node, bool >::iterator it = d_pending_req_phase.begin(); it != d_pending_req_phase.end(); ++it ){
		Trace("strings-pending") << "Require phase : " << it->first << ", polarity = " << it->second << std::endl;
		d_out->requirePhase( it->first, it->second );
	  }
	d_lemma_cache.clear();
	d_pending_req_phase.clear();
  }
}

void TheoryStrings::getNormalForms(Node &eqc, std::vector< Node > & visited, std::vector< Node > & nf,
    std::vector< std::vector< Node > > &normal_forms,  std::vector< std::vector< Node > > &normal_forms_exp, std::vector< Node > &normal_form_src) {
    // EqcItr
    eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
    while( !eqc_i.isFinished() ) {
        Node n = (*eqc_i);
        Trace("strings-process") << "Process term " << n << std::endl;
        if( n.getKind() == kind::CONST_STRING || n.getKind() == kind::STRING_CONCAT ) {
            std::vector<Node> nf_n;
            std::vector<Node> nf_exp_n;
            if( n.getKind() == kind::CONST_STRING  ){
                if( n!=d_emptyString ) {
                    nf_n.push_back( n );
                }
            } else if( n.getKind() == kind::STRING_CONCAT ) {
                for( unsigned i=0; i<n.getNumChildren(); i++ ) {
                    Node nr = d_equalityEngine.getRepresentative( n[i] );
                    std::vector< Node > nf_temp;
                    std::vector< Node > nf_exp_temp;
                    Trace("strings-process") << "Normalizing subterm " << n[i] << " = "  << nr << std::endl;
                    normalizeEquivalenceClass( nr, visited, nf_temp, nf_exp_temp );
                    if( d_conflict || !d_pending.empty() || !d_lemma_cache.empty() ) {
                        return;
                    }
                    if( nf.size()!=1 || nf[0]!=d_emptyString ) {
                        for( unsigned r=0; r<nf_temp.size(); r++ ) {
                            Assert( nf_temp[r].getKind()!=kind::STRING_CONCAT );
                        }
                        nf_n.insert( nf_n.end(), nf_temp.begin(), nf_temp.end() );
                    }
                    nf_exp_n.insert( nf_exp_n.end(), nf_exp_temp.begin(), nf_exp_temp.end() );
                    if( nr!=n[i] ) {
                        nf_exp_n.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, n[i], nr ) );
                    }
                }
            }
            normal_forms.push_back(nf_n);
            normal_forms_exp.push_back(nf_exp_n);
            normal_form_src.push_back(n);
        }
        /* should we add these?
        else {
            //var/sk?
            std::vector<Node> nf_n;
            std::vector<Node> nf_exp_n;
            nf_n.push_back(n);
            normal_forms.push_back(nf_n);
            normal_forms_exp.push_back(nf_exp_n);
            normal_form_src.push_back(n);
        }*/
        ++eqc_i;
    }

    // Test the result
    if( !normal_forms.empty() ) {
        Trace("strings-solve") << "--- Normal forms for equivlance class " << eqc << " : " << std::endl;
        for( unsigned i=0; i<normal_forms.size(); i++ ) {
            Trace("strings-solve") << "#" << i << " (from " << normal_form_src[i] << ") : ";
            for( unsigned j=0; j<normal_forms[i].size(); j++ ) {
                if(j>0) Trace("strings-solve") << ", ";
                Trace("strings-solve") << normal_forms[i][j];
            }
            Trace("strings-solve") << std::endl;
            Trace("strings-solve") << "   Explanation is : ";
            if(normal_forms_exp[i].size() == 0) {
                Trace("strings-solve") << "NONE";
            } else {
                for( unsigned j=0; j<normal_forms_exp[i].size(); j++ ) {
                    if(j>0) Trace("strings-solve") << " AND ";
                    Trace("strings-solve") << normal_forms_exp[i][j];
                }
            }
            Trace("strings-solve") << std::endl;
        }
    }
}
//nf_exp is conjunction
void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & visited, std::vector< Node > & nf, std::vector< Node > & nf_exp ) {
    Trace("strings-process") << "Process equivalence class " << eqc << std::endl;
    if( std::find( visited.begin(), visited.end(), eqc )!=visited.end() ){
        //nf.push_back( eqc );
        if( eqc.getKind()==kind::STRING_CONCAT ){
            for( unsigned i=0; i<eqc.getNumChildren(); i++ ){
				if( !d_equalityEngine.hasTerm(d_emptyString) || !d_equalityEngine.areEqual( eqc[i], d_emptyString ) ){
					nf.push_back( eqc[i] );
				}
            }
        }else if( !d_equalityEngine.hasTerm(d_emptyString) || !d_equalityEngine.areEqual( eqc, d_emptyString ) ){
            nf.push_back( eqc );
        }
        Trace("strings-process") << "Return process equivalence class " << eqc << " : already visited." << std::endl;
    } else if (d_equalityEngine.hasTerm(d_emptyString) && d_equalityEngine.areEqual( eqc, d_emptyString )){
        //do nothing
        Trace("strings-process") << "Return process equivalence class " << eqc << " : empty." << std::endl;
		d_normal_forms[eqc].clear();
		d_normal_forms_exp[eqc].clear();
    } else {
        visited.push_back( eqc );
        if(d_normal_forms.find(eqc)==d_normal_forms.end() ){
            //phi => t = s1 * ... * sn
            // normal form for each non-variable term in this eqc (s1...sn)
            std::vector< std::vector< Node > > normal_forms;
            // explanation for each normal form (phi)
            std::vector< std::vector< Node > > normal_forms_exp;
            // record terms for each normal form (t)
            std::vector< Node > normal_form_src;
            //Get Normal Forms
            getNormalForms(eqc, visited, nf, normal_forms, normal_forms_exp, normal_form_src);
            if( d_conflict || !d_pending.empty() || !d_lemma_cache.empty() ) {
                return;
            }

            unsigned i = 0;
            //unify each normal form > 0 with normal_forms[0]
            for( unsigned j=1; j<normal_forms.size(); j++ ) {

                Trace("strings-solve") << "Process normal form #0 against #" << j << "..." << std::endl;
                if( isNormalFormPair( normal_form_src[i], normal_form_src[j] ) ){
                    Trace("strings-solve") << "Already normalized (in cache)." << std::endl;
                }else{
                    Trace("strings-solve") << "Not in cache." << std::endl;
                    //the current explanation for why the prefix is equal
                    std::vector< Node > curr_exp;
                    curr_exp.insert(curr_exp.end(), normal_forms_exp[i].begin(), normal_forms_exp[i].end() );
                    curr_exp.insert(curr_exp.end(), normal_forms_exp[j].begin(), normal_forms_exp[j].end() );
                    curr_exp.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, normal_form_src[i], normal_form_src[j] ) );
                    //ensure that normal_forms[i] and normal_forms[j] are the same modulo equality
                    unsigned index_i = 0;
                    unsigned index_j = 0;
                    bool success;
                    do
                    {
                        success = false;
                        //if we are at the end
                        if(index_i==normal_forms[i].size() || index_j==normal_forms[j].size() ) {
                            if( index_i==normal_forms[i].size() && index_j==normal_forms[j].size() ){
                                //we're done
                                addNormalFormPair( normal_form_src[i], normal_form_src[j] );
                            }else{
                                //the remainder must be empty
                                unsigned k = index_i==normal_forms[i].size() ? j : i;
                                unsigned index_k = index_i==normal_forms[i].size() ? index_j : index_i;
                                while(!d_conflict && index_k<normal_forms[k].size()) {
                                    //can infer that this string must be empty
                                    Node eq_exp;
                                    if( curr_exp.empty() ) {
                                        eq_exp = d_true;
                                    } else if( curr_exp.size() == 1 ) {
                                        eq_exp = curr_exp[0];
                                    } else {
                                        eq_exp = NodeManager::currentNM()->mkNode( kind::AND, curr_exp );
                                    }
                                    Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, d_emptyString, normal_forms[k][index_k] );
                                    Trace("strings-lemma") << "Strings : Infer " << eq << " from " << eq_exp << std::endl;
									Assert( !d_equalityEngine.areEqual( d_emptyString, normal_forms[k][index_k] ) );
                                    d_pending.push_back( eq );
                                    d_pending_exp[eq] = eq_exp;
                                    d_infer.push_back(eq);
                                    d_infer_exp.push_back(eq_exp);
                                    index_k++;
                                }
                            }
                        }else {
                            Trace("strings-solve-debug") << "Process " << normal_forms[i][index_i] << " ... " << normal_forms[j][index_j] << std::endl;
                            if(areEqual(normal_forms[i][index_i],normal_forms[j][index_j])){
                                Trace("strings-solve-debug") << "Case 1 : strings are equal" << std::endl;
                                //terms are equal, continue
                                if( normal_forms[i][index_i]!=normal_forms[j][index_j] ){
                                    Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL,normal_forms[i][index_i],
                                                                                                     normal_forms[j][index_j]);
                                    Trace("strings-solve-debug") << "Add to explanation : " << eq << std::endl;
                                    curr_exp.push_back(eq);
                                }
                                index_j++;
                                index_i++;
                                success = true;
                            }else{
								Node length_term_i = getLength( normal_forms[i][index_i] );
								Node length_term_j = getLength( normal_forms[j][index_j] );
                                //check if length(normal_forms[i][index]) == length(normal_forms[j][index])
                                if( areEqual(length_term_i, length_term_j)  ){
                                    Trace("strings-solve-debug") << "Case 2 : string lengths are equal" << std::endl;
                                    //length terms are equal, merge equivalence classes if not already done so
                                    Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[i][index_i], normal_forms[j][index_j] );
                                    std::vector< Node > temp_exp;
                                    temp_exp.insert(temp_exp.end(), curr_exp.begin(), curr_exp.end() );
                                    temp_exp.push_back(NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_j ));
                                    Node eq_exp = temp_exp.empty() ? d_true :
                                                    temp_exp.size() == 1 ? temp_exp[0] : NodeManager::currentNM()->mkNode( kind::AND, temp_exp );
                                    Trace("strings-lemma") << "Strings : Infer " << eq << " from " << eq_exp << std::endl;
                                    //d_equalityEngine.assertEquality( eq, true, eq_exp );
                                    d_pending.push_back( eq );
                                    d_pending_exp[eq] = eq_exp;
                                    d_infer.push_back(eq);
                                    d_infer_exp.push_back(eq_exp);
                                    return;
								}else if( ( normal_forms[i][index_i].getKind()!=kind::CONST_STRING && index_i==normal_forms[i].size()-1 ) || 
										  ( normal_forms[j][index_j].getKind()!=kind::CONST_STRING && index_j==normal_forms[j].size()-1 ) ){
									Trace("strings-solve-debug") << "Case 3 : at endpoint" << std::endl;
                                    Node conc;
                                    std::vector< Node > antec;
									antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
                                    std::vector< Node > antec_new_lits;
									std::vector< Node > eqn;
									for( unsigned r=0; r<2; r++ ){
										int index_k = r==0 ? index_i : index_j;
										int k = r==0 ? i : j;
										std::vector< Node > eqnc;
										for( unsigned index_l=index_k; index_l<normal_forms[k].size(); index_l++ ){
											eqnc.push_back( normal_forms[k][index_l] );
										}
										eqn.push_back( mkConcat( eqnc ) );
									}
									conc = eqn[0].eqNode( eqn[1] );
									Node ant = mkExplain( antec, antec_new_lits );
									sendLemma( ant, conc, "Endpoint" );
									return;
								}else{
                                    Trace("strings-solve-debug") << "Case 4 : must compare strings" << std::endl;
                                    Node conc;
                                    std::vector< Node > antec;
                                    std::vector< Node > antec_new_lits;
                                    //check for loops
                                    //Trace("strings-loop") << "Check for loops i,j = " << (index_i+1) << "/" << normal_forms[i].size() << " " << (index_j+1) << "/" << normal_forms[j].size() << std::endl;
                                    int has_loop[2] = { -1, -1 };
                                    for( unsigned r=0; r<2; r++ ){
                                        int index = (r==0 ? index_i : index_j);
                                        int other_index = (r==0 ? index_j : index_i );
                                        int n_index = (r==0 ? i : j);
                                        int other_n_index = (r==0 ? j : i);
                                        if( normal_forms[other_n_index][other_index].getKind() != kind::CONST_STRING ) {
                                            for( unsigned lp = index+1; lp<normal_forms[n_index].size(); lp++ ){
                                                if( normal_forms[n_index][lp]==normal_forms[other_n_index][other_index] ){
                                                    has_loop[r] = lp;
                                                    break;
                                                }
                                            }
                                        }
                                    }
                                    if( has_loop[0]!=-1 || has_loop[1]!=-1 ){
                                        int loop_n_index = has_loop[0]!=-1 ? i : j;
                                        int other_n_index = has_loop[0]!=-1 ? j : i;
                                        int loop_index = has_loop[0]!=-1 ? has_loop[0] : has_loop[1];
                                        int index = has_loop[0]!=-1 ? index_i : index_j;
                                        int other_index = has_loop[0]!=-1 ? index_j : index_i;
                                        Trace("strings-loop") << "Detected possible loop for " << normal_forms[loop_n_index][loop_index];
                                        Trace("strings-loop") << " ... " << normal_forms[other_n_index][other_index] << std::endl;

                                        //we have x * s1 * .... * sm = t1 * ... * tn * x * r1 * ... * rp
                                        //check if
                                        //t1 * ... * tn = n[loop_n_index][index]....n[loop_n_index][loop_index-1] = y * z
                                        // and
                                        //s1 * ... * sk = n[other_n_index][other_index+1].....n[other_n_index][k+1] = z * y
                                        // for some y,z,k

										Trace("strings-loop") << "Must add lemma." << std::endl;
										//need to break
										Node sk_y= NodeManager::currentNM()->mkSkolem( "ysym_$$", normal_forms[i][index_i].getType(), "created for loop detection split" );
										Node sk_z= NodeManager::currentNM()->mkSkolem( "zsym_$$", normal_forms[i][index_i].getType(), "created for loop detection split" );

										antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
										//require that x is non-empty
										Node x_empty = normal_forms[loop_n_index][loop_index].eqNode( d_emptyString );
										x_empty = Rewriter::rewrite( x_empty );
										//if( d_equalityEngine.hasTerm( d_emptyString ) && d_equalityEngine.areDisequal( normal_forms[loop_n_index][loop_index], d_emptyString, true ) ){
										//	antec.push_back( x_empty.negate() );
										//}else{
										antec_new_lits.push_back( x_empty.negate() );
										//}
										d_pending_req_phase[ x_empty ] = true;


										//t1 * ... * tn = y * z
										std::vector< Node > c1c;
										//n[loop_n_index][index]....n[loop_n_index][loop_lindex-1]
										for( int r=index; r<=loop_index-1; r++ ) {
											c1c.push_back( normal_forms[loop_n_index][r] );
										}
										Node conc1 = mkConcat( c1c );
										conc1 = NodeManager::currentNM()->mkNode( kind::EQUAL, conc1,
														NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk_y, sk_z ) );
										std::vector< Node > c2c;
										//s1 * ... * sk = n[other_n_index][other_index+1].....n[other_n_index][k+1]
										for( int r=other_index+1; r < (int)normal_forms[other_n_index].size(); r++ ) {
											c2c.push_back( normal_forms[other_n_index][r] );
										}
										Node left2 = mkConcat( c2c );
										std::vector< Node > c3c;
										c3c.push_back( sk_z );
										c3c.push_back( sk_y );
										//r1 * ... * rk = n[loop_n_index][loop_index+1]....n[loop_n_index][loop_index-1]
										for( int r=loop_index+1; r < (int)normal_forms[loop_n_index].size(); r++ ) {
											c3c.push_back( normal_forms[loop_n_index][r] );
										}
										Node conc2 = NodeManager::currentNM()->mkNode( kind::EQUAL, left2,
														mkConcat( c3c ) );
										
										Node sk_y_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_y );
										//Node sk_z_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_z );
										//Node len_y_eq_zero = NodeManager::currentNM()->mkNode( kind::EQUAL, sk_y_len, d_zero);
										//Node len_z_eq_zero = NodeManager::currentNM()->mkNode( kind::EQUAL, sk_z_len, d_zero);
										//Node len_y_eq_zero = NodeManager::currentNM()->mkNode( kind::EQUAL, sk_y, d_emptyString);
										//Node zz_imp_yz = NodeManager::currentNM()->mkNode( kind::IMPLIES, len_z_eq_zero, len_y_eq_zero);
										
										//Node z_neq_empty = NodeManager::currentNM()->mkNode( kind::EQUAL, sk_z, d_emptyString).negate();
										//Node len_x_gt_len_y = NodeManager::currentNM()->mkNode( kind::GT, 
										//						NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, normal_forms[other_n_index][other_index]),
										//						sk_y_len );
										Node ant = mkExplain( antec, antec_new_lits );
										conc = NodeManager::currentNM()->mkNode( kind::AND, conc1, conc2 );//, x_eq_y_rest );// , z_neq_empty //, len_x_gt_len_y

										//Node x_eq_empty = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[other_n_index][other_index], d_emptyString);
										//conc = NodeManager::currentNM()->mkNode( kind::OR, x_eq_empty, conc );

										//we will be done
										addNormalFormPair( normal_form_src[i], normal_form_src[j] );
										sendLemma( ant, conc, "Loop" );
										addInductiveEquation( normal_forms[other_n_index][other_index], sk_y, sk_z, ant, "Loop Induction" );
										return;
                                    }else{
                                        Trace("strings-solve-debug") << "No loops detected." << std::endl;
                                        if( normal_forms[i][index_i].getKind() == kind::CONST_STRING ||
                                            normal_forms[j][index_j].getKind() == kind::CONST_STRING) {
											unsigned const_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? i : j;
											unsigned const_index_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? index_i : index_j;
											unsigned nconst_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? j : i;
											unsigned nconst_index_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? index_j : index_i;
                                            Node const_str = normal_forms[const_k][const_index_k];
                                            Node other_str = normal_forms[nconst_k][nconst_index_k];
                                            if( other_str.getKind() == kind::CONST_STRING ) {
                                                unsigned len_short = const_str.getConst<String>().size() <= other_str.getConst<String>().size() ? const_str.getConst<String>().size() : other_str.getConst<String>().size();
                                                if( const_str.getConst<String>().strncmp(other_str.getConst<String>(), len_short) ) {
                                                    //same prefix
                                                    //k is the index of the string that is shorter
                                                    int k = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? i : j;
                                                    int index_k = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? index_i : index_j;
                                                    int l = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? j : i;
                                                    int index_l = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? index_j : index_i;
                                                    Node remainderStr = NodeManager::currentNM()->mkConst( normal_forms[l][index_l].getConst<String>().substr(len_short) );
                                                    Trace("strings-solve-debug-test") << "Break normal form of " << normal_forms[l][index_l] << " into " << normal_forms[k][index_k] << ", " << remainderStr << std::endl;
                                                    normal_forms[l].insert( normal_forms[l].begin()+index_l + 1, remainderStr );
                                                    normal_forms[l][index_l] = normal_forms[k][index_k];
                                                    success = true;
                                                } else {
                                                    //curr_exp is conflict
                                                    antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
													Node ant = mkExplain( antec, antec_new_lits );
													sendLemma( ant, conc, "Conflict" );
													return;
                                                }
                                            } else {
                                                Assert( other_str.getKind()!=kind::STRING_CONCAT );
                                                antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
												Node firstChar = const_str.getConst<String>().size() == 1 ? const_str :
													NodeManager::currentNM()->mkConst( const_str.getConst<String>().substr(0, 1) );
												//split the string
												Node sk = NodeManager::currentNM()->mkSkolem( "ssym_$$", normal_forms[i][index_i].getType(), "created for split" );

												Node eq1 = NodeManager::currentNM()->mkNode( kind::EQUAL, other_str, d_emptyString );
												Node eq2_m = NodeManager::currentNM()->mkNode( kind::EQUAL, other_str,
															NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, firstChar, sk ) );
												Node eq2 = eq2_m;//NodeManager::currentNM()->mkNode( kind::AND, eq2_m, sk_len_geq_zero );
												conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 );
                                                Trace("strings-solve-debug") << "Break normal form constant/variable " << std::endl;

												Node ant = mkExplain( antec, antec_new_lits );
												sendLemma( ant, conc, "Constant Split" );
												return;
                                            }
                                        }else{
                                            antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );

											Node ldeq = NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_j ).negate();
											if( d_equalityEngine.areDisequal( length_term_i, length_term_j, true ) ){
												antec.push_back( ldeq );
											}else{
												antec_new_lits.push_back(ldeq);
											}
											Node sk = NodeManager::currentNM()->mkSkolem( "ssym_$$", normal_forms[i][index_i].getType(), "created for split" );
											Node eq1 = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[i][index_i],
														NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, normal_forms[j][index_j], sk ) );
											Node eq2 = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[j][index_j],
														NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, normal_forms[i][index_i], sk ) );
											conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 );
											// |sk| > 0
											//Node sk_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk );
											//Node sk_gt_zero = NodeManager::currentNM()->mkNode( kind::GT, sk_len, d_zero);
											Node sk_gt_zero = NodeManager::currentNM()->mkNode( kind::EQUAL, sk, d_emptyString).negate();
											Trace("strings-lemma") << "Strings lemma : " << sk_gt_zero << std::endl;
											//d_out->lemma(sk_gt_zero);
											d_lemma_cache.push_back( sk_gt_zero );

											Node ant = mkExplain( antec, antec_new_lits );
											sendLemma( ant, conc, "Split" );
											return;
                                        }
                                    }
                                }
                            }
                        }
                    }while(success);
                }
            }

            //construct the normal form
            if( normal_forms.empty() ){
                Trace("strings-solve-debug2") << "construct the normal form" << std::endl;
                nf.push_back( eqc );
            } else {
                Trace("strings-solve-debug2") << "just take the first normal form" << std::endl;
                //just take the first normal form
                nf.insert( nf.end(), normal_forms[0].begin(), normal_forms[0].end() );
                nf_exp.insert( nf_exp.end(), normal_forms_exp[0].begin(), normal_forms_exp[0].end() );
                if( eqc!=normal_form_src[0] ){
                    nf_exp.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, eqc, normal_form_src[0] ) );
                }
                Trace("strings-solve-debug2") << "just take the first normal form ... done" << std::endl;
            }
            //if( visited.empty() ){
                //TODO : cache?
            //}
            d_normal_forms[eqc].insert( d_normal_forms[eqc].end(), nf.begin(), nf.end() );
            d_normal_forms_exp[eqc].insert( d_normal_forms_exp[eqc].end(), nf_exp.begin(), nf_exp.end() );
            Trace("strings-process") << "Return process equivalence class " << eqc << " : returned." << std::endl;
        }else{
            Trace("strings-process") << "Return process equivalence class " << eqc << " : already computed." << std::endl;
            nf.insert( nf.end(), d_normal_forms[eqc].begin(), d_normal_forms[eqc].end() );
            nf_exp.insert( nf_exp.end(), d_normal_forms_exp[eqc].begin(), d_normal_forms_exp[eqc].end() );
        }
        visited.pop_back();
    }
}

bool TheoryStrings::normalizeDisequality( Node ni, Node nj ) {
	//Assert( areDisequal( ni, nj ) );
	if( d_normal_forms[ni].size()>1 || d_normal_forms[nj].size()>1 ){
		unsigned index = 0;
		while( index<d_normal_forms[ni].size() ){
			Node i = d_normal_forms[ni][index];
			Node j = d_normal_forms[nj][index];
			Trace("strings-solve-debug")  << "...Processing " << i << " " << j << std::endl;
			if( !areEqual( i, j ) ){
				Node li = getLength( i );
				Node lj = getLength( j );
				if( !areEqual(li, lj) ){
					Trace("strings-solve") << "Case 2 : add lemma " << std::endl;
					//must add lemma
					std::vector< Node > antec;
					std::vector< Node > antec_new_lits;
					antec.insert( antec.end(), d_normal_forms_exp[ni].begin(), d_normal_forms_exp[ni].end() );
					antec.insert( antec.end(), d_normal_forms_exp[nj].begin(), d_normal_forms_exp[nj].end() );
					antec.push_back( ni.eqNode( nj ).negate() );
					antec_new_lits.push_back( li.eqNode( lj ) );
					std::vector< Node > conc;
					Node sk1 = NodeManager::currentNM()->mkSkolem( "w1sym_$$", ni.getType(), "created for disequality normalization" );
					Node sk2 = NodeManager::currentNM()->mkSkolem( "w2sym_$$", ni.getType(), "created for disequality normalization" );
					Node sk3 = NodeManager::currentNM()->mkSkolem( "w3sym_$$", ni.getType(), "created for disequality normalization" );
					Node sk4 = NodeManager::currentNM()->mkSkolem( "w4sym_$$", ni.getType(), "created for disequality normalization" );
					Node sk5 = NodeManager::currentNM()->mkSkolem( "w5sym_$$", ni.getType(), "created for disequality normalization" );
					Node w1w2w3 = NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk2, sk3 );
					Node w1w4w5 = NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk4, sk5 );
					Node s_eq_w1w2w3 = NodeManager::currentNM()->mkNode( kind::EQUAL, ni, w1w2w3 );
					conc.push_back( s_eq_w1w2w3 );
					Node t_eq_w1w4w5 = NodeManager::currentNM()->mkNode( kind::EQUAL, nj, w1w4w5 );
					conc.push_back( t_eq_w1w4w5 );
					Node w2_neq_w4 = sk2.eqNode( sk4 ).negate();
					conc.push_back( w2_neq_w4 );
					Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational( 1 ) );
					Node w2_len_one = NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2), one);
					conc.push_back( w2_len_one );
					Node w4_len_one = NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk4), one);
					conc.push_back( w4_len_one );

					//Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2),
					//													     NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk4) );
					//conc.push_back( eq );
					sendLemma( mkExplain( antec, antec_new_lits ), NodeManager::currentNM()->mkNode( kind::AND, conc ), "Disequality Normalize" );
					return true;
				}else if( areDisequal( i, j ) ){
					Trace("strings-solve") << "Case 1 : found equal length disequal sub strings " << i << " " << j << std::endl;
					//we are done
					return false;
				}
			}
			index++;
		}
		Assert( false );
	}
	return false;
}

void TheoryStrings::addNormalFormPair( Node n1, Node n2 ) {
  if( !isNormalFormPair( n1, n2 ) ){
        NodeList* lst;
        NodeListMap::iterator nf_i = d_nf_pairs.find( n1 );
        if( nf_i == d_nf_pairs.end() ){
          if( d_nf_pairs.find( n2 )!=d_nf_pairs.end() ){
            addNormalFormPair( n2, n1 );
            return;
          }
          lst = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false,
                                                                ContextMemoryAllocator<TNode>(getSatContext()->getCMM()) );
          d_nf_pairs.insertDataFromContextMemory( n1, lst );
		  Trace("strings-nf") << "Create cache for " << n1 << std::endl;
        }else{
          lst = (*nf_i).second;
        }
		Trace("strings-nf") << "Add normal form pair : " << n1 << " " << n2 << std::endl;
        lst->push_back( n2 );
		Assert( isNormalFormPair( n1, n2 ) );
    }else{
		Trace("strings-nf-debug") << "Already a normal form pair " << n1 << " " << n2 << std::endl;
	}

}
bool TheoryStrings::isNormalFormPair( Node n1, Node n2 ) {
    //TODO: modulo equality?
    return isNormalFormPair2( n1, n2 ) || isNormalFormPair2( n2, n1 );
}
bool TheoryStrings::isNormalFormPair2( Node n1, Node n2 ) {
    //Trace("strings-debug") << "is normal form pair. " << n1 << " " << n2 << std::endl;
  NodeList* lst;
  NodeListMap::iterator nf_i = d_nf_pairs.find( n1 );
  if( nf_i != d_nf_pairs.end() ){
    lst = (*nf_i).second;
    for( NodeList::const_iterator i = lst->begin(); i != lst->end(); ++i ) {
        Node n = *i;
        if( n==n2 ){
            return true;
        }
    }
  }
  return false;
}

bool TheoryStrings::addInductiveEquation( Node x, Node y, Node z, Node exp, const char * c ) {
    Trace("strings-solve-debug") << "add inductive equation for " << x << " = (" << y << " " << z << ")* " << y << std::endl;
#ifdef STR_UNROLL_INDUCTION
	Node w = NodeManager::currentNM()->mkSkolem( "wsym_$$", x.getType(), "created for induction" );
	Node x_eq_y_w = NodeManager::currentNM()->mkNode( kind::EQUAL, x, 
							NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, y, w ) );
	Node lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, x_eq_y_w );
	Trace("strings-lemma") << "Strings " << c << " lemma : " << lem << std::endl;
	d_lemma_cache.push_back( lem );

	//add initial induction
	Node lit1 = w.eqNode( d_emptyString );
	lit1 = Rewriter::rewrite( lit1 );
	Node wp = NodeManager::currentNM()->mkSkolem( "wpsym_$$", x.getType(), "created for induction" );
	Node lit2 = w.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, z, y, wp ) );
	lit2 = Rewriter::rewrite( lit2 );
	Node split_lem = NodeManager::currentNM()->mkNode( kind::OR, lit1, lit2 );
	Trace("strings-ind") << "Strings : Lemma " << c << " for unrolling " << split_lem << std::endl;
	Trace("strings-lemma") << "Strings : Lemma " << c << " for unrolling " << split_lem << std::endl;
	d_lemma_cache.push_back( split_lem );

	//d_lit_to_decide.push_back( lit1 );
	d_lit_to_unroll[lit2] = true;
	d_pending_req_phase[lit1] = true;
	d_pending_req_phase[lit2] = false;

	x = w;
	std::vector< Node > skc;
	skc.push_back( y );
	skc.push_back( z );
	y = d_emptyString;
	z = mkConcat( skc );
#endif

    NodeListMap::iterator itr_x_y = d_ind_map1.find(x);
    NodeList* lst1;
    NodeList* lst2;
    NodeList* lste;
    NodeList* lstl;
    if( itr_x_y == d_ind_map1.end() ) {
        // add x->y
        lst1 = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false,
                                                                ContextMemoryAllocator<TNode>(getSatContext()->getCMM()) );
        d_ind_map1.insertDataFromContextMemory( x, lst1 );
        // add x->z
        lst2 = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false,
                                                                ContextMemoryAllocator<TNode>(getSatContext()->getCMM()) );
        d_ind_map2.insertDataFromContextMemory( x, lst2 );
        // add x->exp
        lste = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false,
                                                                ContextMemoryAllocator<TNode>(getSatContext()->getCMM()) );
        d_ind_map_exp.insertDataFromContextMemory( x, lste );
        // add x->hasLemma false
        lstl = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false,
                                                                ContextMemoryAllocator<TNode>(getSatContext()->getCMM()) );
        d_ind_map_lemma.insertDataFromContextMemory( x, lstl );
    } else {
        //TODO: x in (yz)*y (exp) vs  x in (y1 z1)*y1 (exp1)
        lst1 = (*itr_x_y).second;
        lst2 = (*d_ind_map2.find(x)).second;
        lste = (*d_ind_map_exp.find(x)).second;
        lstl = (*d_ind_map_lemma.find(x)).second;
        Trace("strings-solve-debug") << "Already in maps " << x << " = (" << lst1 << " " << lst2 << ")* " << lst1 << std::endl;
        Trace("strings-solve-debug") << "... with exp = " << lste << std::endl;
    }
    lst1->push_back( y );
    lst2->push_back( z );
    lste->push_back( exp );
#ifdef STR_UNROLL_INDUCTION
	return true;
#else
	return false;
#endif
}

void TheoryStrings::sendLemma( Node ant, Node conc, const char * c ) {
	if( conc.isNull() ){
		d_out->conflict(ant);
		Trace("strings-conflict") << "CONFLICT : Strings conflict : " << ant << std::endl;
		d_conflict = true;
	}else{
		Node lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, ant, conc );
		Trace("strings-lemma") << "Strings " << c << " lemma : " << lem << std::endl;
		d_lemma_cache.push_back( lem );
	}
}

void TheoryStrings::sendSplit( Node a, Node b, const char * c ) {
	Node eq = a.eqNode( b );
	eq = Rewriter::rewrite( eq );
	Node neq = NodeManager::currentNM()->mkNode( kind::NOT, eq );
	Node lemma_or = NodeManager::currentNM()->mkNode( kind::OR, eq, neq );
	Trace("strings-lemma") << "Strings " << c << " split lemma : " << lemma_or << std::endl;
	d_lemma_cache.push_back(lemma_or);
	d_pending_req_phase[eq] = true;
}

Node TheoryStrings::mkConcat( std::vector< Node >& c ) {
    Node cc = c.size()>1 ? NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, c ) : ( c.size()==1 ? c[0] : d_emptyString );
	return Rewriter::rewrite( cc );
}

Node TheoryStrings::mkExplain( std::vector< Node >& a, std::vector< Node >& an ) {
    std::vector< TNode > antec_exp;
    for( unsigned i=0; i<a.size(); i++ ){
        Trace("strings-solve-debug") << "Ask for explanation of " << a[i] << std::endl;
        //assert
        if(a[i].getKind() == kind::EQUAL) {
            //assert( hasTerm(a[i][0]) );
            //assert( hasTerm(a[i][1]) );
            Assert( areEqual(a[i][0], a[i][1]) );
        } else if( a[i].getKind()==kind::NOT && a[i][0].getKind()==kind::EQUAL ){
            Assert( hasTerm(a[i][0][0]) );
            Assert( hasTerm(a[i][0][1]) );
            Assert( d_equalityEngine.areDisequal(a[i][0][0], a[i][0][1], true) );
        }
		unsigned ps = antec_exp.size();
        explain(a[i], antec_exp);
        Trace("strings-solve-debug") << "Done, explanation was : " << std::endl;
		for( unsigned j=ps; j<antec_exp.size(); j++ ){
			Trace("strings-solve-debug") << "  " << antec_exp[j] << std::endl;
		}
		Trace("strings-solve-debug") << std::endl;
    }
    for( unsigned i=0; i<an.size(); i++ ){
		Trace("strings-solve-debug") << "Add to explanation (new literal) " << an[i] << std::endl;
        antec_exp.push_back(an[i]);
    }
    Node ant;
    if( antec_exp.empty() ) {
        ant = d_true;
    } else if( antec_exp.size()==1 ) {
        ant = antec_exp[0];
    } else {
        ant = NodeManager::currentNM()->mkNode( kind::AND, antec_exp );
    }
	ant = Rewriter::rewrite( ant );
    return ant;
}

bool TheoryStrings::checkNormalForms() {
    Trace("strings-process") << "Normalize equivalence classes...." << std::endl;
	eq::EqClassesIterator eqcs2_i = eq::EqClassesIterator( &d_equalityEngine );
	for( unsigned t=0; t<2; t++ ){
		Trace("strings-eqc") << (t==0 ? "STRINGS:" : "OTHER:") << std::endl;
		while( !eqcs2_i.isFinished() ){
		Node eqc = (*eqcs2_i);
		bool print = (t==0 && eqc.getType().isString() ) || (t==1 && !eqc.getType().isString() );
		if (print) {
			eq::EqClassIterator eqc2_i = eq::EqClassIterator( eqc, &d_equalityEngine );
			Trace("strings-eqc") << "Eqc( " << eqc << " ) : ";
			while( !eqc2_i.isFinished() ) {
				if( (*eqc2_i)!=eqc ){
					Trace("strings-eqc") << (*eqc2_i) << " ";
				}
				++eqc2_i;
			}
			Trace("strings-eqc") << std::endl;
		}
		++eqcs2_i;
		}
		Trace("strings-eqc") << std::endl;
	}
	Trace("strings-eqc") << std::endl;
	for( NodeListMap::const_iterator it = d_nf_pairs.begin(); it != d_nf_pairs.end(); ++it ){
		NodeList* lst = (*it).second;
		NodeList::const_iterator it2 = lst->begin();
		Trace("strings-nf") << (*it).first << " has been unified with ";
		while( it2!=lst->end() ){
			Trace("strings-nf") << (*it2);
			++it2;
		}
		Trace("strings-nf") << std::endl;
	}
	Trace("strings-nf") << std::endl;
	Trace("strings-nf") << "Current inductive equations : " << std::endl;
	for( NodeListMap::const_iterator it = d_ind_map1.begin(); it != d_ind_map1.end(); ++it ){
        Node x = (*it).first;
        NodeList* lst1 = (*it).second;
        NodeList* lst2 = (*d_ind_map2.find(x)).second;
        NodeList::const_iterator i1 = lst1->begin();
        NodeList::const_iterator i2 = lst2->begin();
        while( i1!=lst1->end() ){
            Node y = *i1;
            Node z = *i2;
			Trace("strings-nf") << "Inductive equation : " << x << " = ( " << y << " ++ " << z << " ) * " << y << std::endl;
            ++i1;
            ++i2;
        }
    }

  bool addedFact;
  do {
	Trace("strings-process") << "Check Normal Forms........next round" << std::endl;
    //calculate normal forms for each equivalence class, possibly adding splitting lemmas
    d_normal_forms.clear();
    d_normal_forms_exp.clear();
    std::map< Node, Node > nf_to_eqc;
    std::map< Node, Node > eqc_to_exp;
    d_lemma_cache.clear();
	d_pending_req_phase.clear();
	//get equivalence classes
	std::vector< Node > eqcs;
	getEquivalenceClasses( eqcs );
	for( unsigned i=0; i<eqcs.size(); i++ ){
		Node eqc = eqcs[i];
		Trace("strings-process") << "- Verify normal forms are the same for " << eqc << std::endl;
		std::vector< Node > visited;
		std::vector< Node > nf;
		std::vector< Node > nf_exp;
		normalizeEquivalenceClass(eqc, visited, nf, nf_exp);
		if( d_conflict ){
			return true;
		}else if ( d_pending.empty() && d_lemma_cache.empty() ){
			Node nf_term;
			if( nf.size()==0 ){
				nf_term = d_emptyString;
			}else if( nf.size()==1 ) {
				nf_term = nf[0];
			} else {
				nf_term = NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, nf );
			}
			nf_term = Rewriter::rewrite( nf_term );
			Trace("strings-debug") << "Make nf_term_exp..." << std::endl;
			Node nf_term_exp = nf_exp.empty() ? d_true :
								nf_exp.size()==1 ? nf_exp[0] : NodeManager::currentNM()->mkNode( kind::AND, nf_exp );
			if( nf_to_eqc.find(nf_term)!=nf_to_eqc.end() ){
				//Trace("strings-debug") << "Merge because of normal form : " << eqc << " and " << nf_to_eqc[nf_term] << " both have normal form " << nf_term << std::endl;
				//two equivalence classes have same normal form, merge
				Node eq_exp = NodeManager::currentNM()->mkNode( kind::AND, nf_term_exp, eqc_to_exp[nf_to_eqc[nf_term]] );
				Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, eqc, nf_to_eqc[nf_term] );
				Trace("strings-lemma") << "Strings (by normal forms) : Infer " << eq << " from " << eq_exp << std::endl;
				//d_equalityEngine.assertEquality( eq, true, eq_exp );
				d_pending.push_back( eq );
				d_pending_exp[eq] = eq_exp;
				d_infer.push_back(eq);
				d_infer_exp.push_back(eq_exp);
			}else{
				nf_to_eqc[nf_term] = eqc;
				eqc_to_exp[eqc] = nf_term_exp;
			}
		}
		Trace("strings-process") << "Done verifying normal forms are the same for " << eqc << std::endl;
	}

	  Trace("strings-nf-debug") << "**** Normal forms are : " << std::endl;
	  for( std::map< Node, Node >::iterator it = nf_to_eqc.begin(); it != nf_to_eqc.end(); ++it ){
		Trace("strings-nf-debug") << "  normal_form(" << it->second << ") = " << it->first << std::endl;
	  }
	  Trace("strings-nf-debug") << std::endl;
      addedFact = !d_pending.empty();
      doPendingFacts();
  } while ( !d_conflict && d_lemma_cache.empty() && addedFact );


  //process disequalities between equivalence classes
  if( !d_conflict && d_lemma_cache.empty() ){
	  std::vector< Node > eqcs;
	  getEquivalenceClasses( eqcs );
	  std::vector< std::vector< Node > > cols;
	  std::vector< Node > lts;
	  seperateByLength( eqcs, cols, lts );
	  for( unsigned i=0; i<cols.size(); i++ ){
	    if( cols[i].size()>1 && d_lemma_cache.empty() ){
			Trace("strings-solve") << "- Verify disequalities are processed for ";
			printConcat( d_normal_forms[cols[i][0]], "strings-solve" );
			Trace("strings-solve")  << "..." << std::endl;
			//must ensure that normal forms are disequal
			for( unsigned j=1; j<cols[i].size(); j++ ){
				if( !d_equalityEngine.areDisequal( cols[i][0], cols[i][j], false ) ){
					sendSplit( cols[i][0], cols[i][j], "Disequality Normalization" );
					break;
				}else{
					Trace("strings-solve") << "  against ";
					printConcat( d_normal_forms[cols[i][j]], "strings-solve" );
					Trace("strings-solve")  << "..." << std::endl;
					if( normalizeDisequality( cols[i][0], cols[i][j] ) ){
						break;
					}
				}
			}
		}
	  }
  }

  //flush pending lemmas
  if( !d_conflict && !d_lemma_cache.empty() ){
	doPendingLemmas();
	return true;
  }else{
	return false;
  }
}

bool TheoryStrings::checkCardinality() {
  int cardinality = options::stringCharCardinality();
  Trace("strings-solve-debug2") << "get cardinality: " << cardinality << endl;

  std::vector< Node > eqcs;
  getEquivalenceClasses( eqcs );

  std::vector< std::vector< Node > > cols;
  std::vector< Node > lts;
  seperateByLength( eqcs, cols, lts );

  for( unsigned i = 0; i<cols.size(); ++i ){
    Node lr = lts[i];
    Trace("string-cardinality") << "Number of strings with length equal to " << lr << " is " << cols[i].size() << std::endl;
    // size > c^k
    double k = std::log( cols[i].size() ) / log((double) cardinality);
    unsigned int int_k = (unsigned int)k;
    Node k_node = NodeManager::currentNM()->mkConst( ::CVC4::Rational( int_k ) );
    //double c_k = pow ( (double)cardinality, (double)lr );
    if( cols[i].size() > 1 ) {
        bool allDisequal = true;
        for( std::vector< Node >::iterator itr1 = cols[i].begin();
              itr1 != cols[i].end(); ++itr1) {
            for( std::vector< Node >::iterator itr2 = itr1 + 1;
                  itr2 != cols[i].end(); ++itr2) {
                if(!d_equalityEngine.areDisequal( *itr1, *itr2, false )) {
                    allDisequal = false;
                    // add split lemma
					sendSplit( *itr1, *itr2, "Cardinality" );
					doPendingLemmas();
					return true;
                }
            }
        }
        if(allDisequal) {
            EqcInfo* ei = getOrMakeEqcInfo( lr, true );
            Trace("string-cardinality") << "Previous cardinality used for " << lr << " is " << ((int)ei->d_cardinality_lem_k.get()-1) << std::endl;
            if( int_k+1 > ei->d_cardinality_lem_k.get() ){
                //add cardinality lemma
                Node dist = NodeManager::currentNM()->mkNode( kind::DISTINCT, cols[i] );
                std::vector< Node > vec_node;
                vec_node.push_back( dist );
                for( std::vector< Node >::iterator itr1 = cols[i].begin();
                      itr1 != cols[i].end(); ++itr1) {
                    Node len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, *itr1 );
                    if( len!=lr ){
                      Node len_eq_lr = NodeManager::currentNM()->mkNode( kind::EQUAL, lr, len );
                      vec_node.push_back( len_eq_lr );
                    }
                }
                Node antc = NodeManager::currentNM()->mkNode( kind::AND, vec_node );
                Node len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, cols[i][0] );
                Node cons = NodeManager::currentNM()->mkNode( kind::GT, len, k_node );
				/*
				sendLemma( antc, cons, "Cardinality" );
				ei->d_cardinality_lem_k.set( int_k+1 );
				if( !d_lemma_cache.empty() ){
					doPendingLemmas();
					return true;
				}
				*/
                Node lemma = NodeManager::currentNM()->mkNode( kind::IMPLIES, antc, cons );
				lemma = Rewriter::rewrite( lemma );
				ei->d_cardinality_lem_k.set( int_k+1 );
				if( lemma!=d_true ){
					Trace("strings-lemma") << "Strings cardinality lemma : " << lemma << std::endl;
					d_out->lemma(lemma);
					return true;
				}
            }
        }
    }
  }
  return false;
}

int TheoryStrings::gcd ( int a, int b ) {
  int c;
  while ( a != 0 ) {
     c = a; a = b%a;  b = c;
  }
  return b;
}

bool TheoryStrings::checkInductiveEquations() {
    bool hasEq = false;
	if(d_ind_map1.size() != 0){
		Trace("strings-ind")  << "We are sat, with these inductive equations : " << std::endl;
		for( NodeListMap::const_iterator it = d_ind_map1.begin(); it != d_ind_map1.end(); ++it ){
			Node x = (*it).first;
			Trace("strings-ind-debug") << "Check eq for " << x << std::endl;
			NodeList* lst1 = (*it).second;
			NodeList* lst2 = (*d_ind_map2.find(x)).second;
			NodeList* lste = (*d_ind_map_exp.find(x)).second;
			//NodeList* lstl = (*d_ind_map_lemma.find(x)).second;
			NodeList::const_iterator i1 = lst1->begin();
			NodeList::const_iterator i2 = lst2->begin();
			NodeList::const_iterator ie = lste->begin();
			//NodeList::const_iterator il = lstl->begin();
			while( i1!=lst1->end() ){
				Node y = *i1;
				Node z = *i2;
				//Trace("strings-ind-debug") << "Check y=" << y << " , z=" << z << std::endl;
				//if( il==lstl->end() ) {
					std::vector< Node > nf_y, nf_z, exp_y, exp_z;
					
					//getFinalNormalForm( y, nf_y, exp_y);
					//getFinalNormalForm( z, nf_z, exp_z);
					//std::vector< Node > vec_empty;
					//Node nexp_y = mkExplain( exp_y, vec_empty );
					//Trace("strings-ind-debug") << "Check nexp_y=" << nexp_y << std::endl;
					//Node nexp_z = mkExplain( exp_z, vec_empty );

					//Node exp = *ie;
					//Trace("strings-ind-debug") << "Check exp=" << exp << std::endl;

					//exp = NodeManager::currentNM()->mkNode( kind::AND, exp, nexp_y, nexp_z );
					//exp = Rewriter::rewrite( exp );

					Trace("strings-ind") << "Inductive equation : " << x << " = ( " << y << " ++ " << z << " )* " << y << std::endl;
					/*
					for( std::vector< Node >::const_iterator itr = nf_y.begin(); itr != nf_y.end(); ++itr) {
						Trace("strings-ind") << (*itr) << " ";
					}
					Trace("strings-ind") << " ++ ";
					for( std::vector< Node >::const_iterator itr = nf_z.begin(); itr != nf_z.end(); ++itr) {
						Trace("strings-ind") << (*itr) << " ";
					}
					Trace("strings-ind") << " )* ";
					for( std::vector< Node >::const_iterator itr = nf_y.begin(); itr != nf_y.end(); ++itr) {
						Trace("strings-ind") << (*itr) << " ";
					}
					Trace("strings-ind") << std::endl;
					*/
					/*
					Trace("strings-ind") << "Explanation is : " << exp << std::endl;
					std::vector< Node > nf_yz;
					nf_yz.insert( nf_yz.end(), nf_y.begin(), nf_y.end() );
					nf_yz.insert( nf_yz.end(), nf_z.begin(), nf_z.end() );
					std::vector< std::vector< Node > > cols;
					std::vector< Node > lts;
					seperateByLength( nf_yz, cols, lts );
					Trace("strings-ind") << "This can be grouped into collections : " << std::endl;
					for( unsigned j=0; j<cols.size(); j++ ){
						Trace("strings-ind") << "  : ";
						for( unsigned k=0; k<cols[j].size(); k++ ){
							Trace("strings-ind") << cols[j][k] << " ";
						}
						Trace("strings-ind") << std::endl;
					}
					Trace("strings-ind") << std::endl;
					
					Trace("strings-ind") << "Add length lemma..." << std::endl;
					std::vector< int > co;
					co.push_back(0);
					for(unsigned int k=0; k<lts.size(); ++k) {
						if(lts[k].isConst() && lts[k].getType().isInteger()) {
							int len = lts[k].getConst<Rational>().getNumerator().toUnsignedInt();
							co[0] += cols[k].size() * len;
						} else {
							co.push_back( cols[k].size() );
						}
					}
					int g_co = co[0];
					for(unsigned k=1; k<co.size(); ++k) {
						g_co = gcd(g_co, co[k]);
					}
					Node lemma_len;
					// both constants
					Node len_x = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, x );
					Node sk = NodeManager::currentNM()->mkSkolem( "argsym_$$", NodeManager::currentNM()->integerType(), "created for length inductive lemma" );
					Node g_co_node = NodeManager::currentNM()->mkConst( CVC4::Rational(g_co) );
					Node sk_m_gcd = NodeManager::currentNM()->mkNode( kind::MULT, g_co_node, sk );
					Node len_y = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, y );
					Node sk_m_g_p_y =    NodeManager::currentNM()->mkNode( kind::PLUS, sk_m_gcd, len_y );
					lemma_len =     NodeManager::currentNM()->mkNode( kind::EQUAL, sk_m_g_p_y, len_x );
					//Node sk_geq_zero = NodeManager::currentNM()->mkNode( kind::GEQ, sk, d_zero );
					//lemma_len = NodeManager::currentNM()->mkNode( kind::AND, lemma_len, sk_geq_zero );
					lemma_len =     NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, lemma_len );
					Trace("strings-lemma") << "Strings: Add lemma " << lemma_len << std::endl;
					d_out->lemma(lemma_len);
					lstl->push_back( d_true );
					return true;*/
				//}
				++i1;
				++i2;
				++ie;
				//++il;
				if( !d_equalityEngine.hasTerm( d_emptyString ) || !d_equalityEngine.areEqual( y, d_emptyString ) || !d_equalityEngine.areEqual( x, d_emptyString ) ){
					hasEq = true;
				}
			}
		}
	}
    if( hasEq ){
		Trace("strings-ind") << "It is incomplete." << std::endl;
        d_out->setIncomplete();
    }else{
		Trace("strings-ind") << "We can answer SAT." << std::endl;
	}
  return false;
}

void TheoryStrings::getEquivalenceClasses( std::vector< Node >& eqcs ) {
    eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
    while( !eqcs_i.isFinished() ) {
        Node eqc = (*eqcs_i);
        //if eqc.getType is string
        if (eqc.getType().isString()) {
			eqcs.push_back( eqc );
        }
        ++eqcs_i;
    }
}

void TheoryStrings::getFinalNormalForm( Node n, std::vector< Node >& nf, std::vector< Node >& exp ) {
	if( n!=d_emptyString ){
		if( n.getKind()==kind::STRING_CONCAT ){
			for( unsigned i=0; i<n.getNumChildren(); i++ ){
				getFinalNormalForm( n[i], nf, exp );
			}
		}else{
			Trace("strings-debug") << "Get final normal form " << n << std::endl;
			Assert( d_equalityEngine.hasTerm( n ) );
			Node nr = d_equalityEngine.getRepresentative( n );
			EqcInfo *eqc_n = getOrMakeEqcInfo( nr, false );
			Node nc = eqc_n ? eqc_n->d_const_term.get() : Node::null();
			if( !nc.isNull() ){
				nf.push_back( nc );
				if( n!=nc ){
					exp.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, n, nc ) );
				}
			}else{
				Assert( d_normal_forms.find( nr )!=d_normal_forms.end() );
				if( d_normal_forms[nr][0]==nr ){
					Assert( d_normal_forms[nr].size()==1 );
					nf.push_back( nr );
					if( n!=nr ){
						exp.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, n, nr ) );
					}
				}else{
					for( unsigned i=0; i<d_normal_forms[nr].size(); i++ ){
						Assert( d_normal_forms[nr][i]!=nr );
						getFinalNormalForm( d_normal_forms[nr][i], nf, exp );
					}
					exp.insert( exp.end(), d_normal_forms_exp[nr].begin(), d_normal_forms_exp[nr].end() );
				}
			}
			Trace("strings-ind-nf") << "The final normal form of " << n << " is " << nf << std::endl;
		}
	}
}

void TheoryStrings::seperateByLength( std::vector< Node >& n, std::vector< std::vector< Node > >& cols,
											 std::vector< Node >& lts ) {
  unsigned leqc_counter = 0;
  std::map< Node, unsigned > eqc_to_leqc;
  std::map< unsigned, Node > leqc_to_eqc;
  std::map< unsigned, std::vector< Node > > eqc_to_strings;
  for( unsigned i=0; i<n.size(); i++ ){
	Node eqc = n[i];
	Assert( d_equalityEngine.getRepresentative(eqc)==eqc );
	EqcInfo* ei = getOrMakeEqcInfo( eqc, false );
	Node lt = ei ? ei->d_length_term : Node::null();
	if( !lt.isNull() ){
	  lt = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, lt );
	  Node r = d_equalityEngine.getRepresentative( lt );
	  if( eqc_to_leqc.find( r )==eqc_to_leqc.end() ){
		eqc_to_leqc[r] = leqc_counter;
		leqc_to_eqc[leqc_counter] = r;
		leqc_counter++;
	  }
	  eqc_to_strings[ eqc_to_leqc[r] ].push_back( eqc );
	}else{
	  eqc_to_strings[leqc_counter].push_back( eqc );
	  leqc_counter++;
	}
  }
  for( std::map< unsigned, std::vector< Node > >::iterator it = eqc_to_strings.begin(); it != eqc_to_strings.end(); ++it ){
	std::vector< Node > vec;
	vec.insert( vec.end(), it->second.begin(), it->second.end() );
	lts.push_back( leqc_to_eqc[it->first] );
	cols.push_back( vec );
  }
}

void TheoryStrings::printConcat( std::vector< Node >& n, const char * c ) {
	for( unsigned i=0; i<n.size(); i++ ){
		if( i>0 ) Trace(c) << " ++ ";
		Trace(c) << n[i];
	}
}

/*
Node TheoryStrings::getNextDecisionRequest() {
	if( d_lit_to_decide_index.get()<d_lit_to_decide.size() ){
		Node l = d_lit_to_decide[d_lit_to_decide_index.get()];
		d_lit_to_decide_index.set( d_lit_to_decide_index.get() + 1 );
		Trace("strings-ind") << "Strings-ind : decide on " << l << std::endl;
		return l;
	}else{
		return Node::null();
	}
}
*/
}/* CVC4::theory::strings namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */