From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Tue, 1 Mar 2016 22:29:14 +0000 (-0600)
Subject: Shorter explanations for strings based on tracking which parts of normal forms are... 
X-Git-Tag: cvc5-1.0.0~6049^2~110
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=811834a6aeab1e055b0417eaf988fc682e74e65a;p=cvc5.git

Shorter explanations for strings based on tracking which parts of normal forms are dependent upon which equalities. Add anti-skolemization module to quantifiers. Disable rewriting of non-clashing equalities between same constructors.
---

diff --git a/src/Makefile.am b/src/Makefile.am
index 703f82614..aa12c7e03 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -353,6 +353,8 @@ libcvc4_la_SOURCES = \
 	theory/quantifiers/ceg_instantiator.cpp \
 	theory/quantifiers/quant_split.h \
 	theory/quantifiers/quant_split.cpp \
+	theory/quantifiers/anti_skolem.h \
+	theory/quantifiers/anti_skolem.cpp \
 	theory/arith/theory_arith_type_rules.h \
 	theory/arith/type_enumerator.h \
 	theory/arith/arithvar.h \
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index 58367f2e2..e3f4e94f2 100644
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -285,6 +285,8 @@ option macrosQuantMode --macros-quant-mode=MODE CVC4::theory::quantifiers::Macro
  mode for quantifiers macro expansion
 option quantDynamicSplit --quant-dsplit-mode=MODE CVC4::theory::quantifiers::QuantDSplitMode :read-write :default CVC4::theory::quantifiers::QUANT_DSPLIT_MODE_DEFAULT :include "options/quantifiers_modes.h" :handler stringToQuantDSplitMode
  mode for dynamic quantifiers splitting
+option quantAntiSkolem --quant-anti-skolem bool :read-write :default false
+ perform anti-skolemization for quantified formulas
 
 ### recursive function options
 
diff --git a/src/options/strings_options b/src/options/strings_options
index dee379878..5c991a1bb 100644
--- a/src/options/strings_options
+++ b/src/options/strings_options
@@ -63,6 +63,8 @@ option stringInferAsLemmas strings-infer-as-lemmas --strings-infer-as-lemmas boo
  always send lemmas out instead of making internal inferences
 option stringRExplainLemmas strings-rexplain-lemmas --strings-rexplain-lemmas bool :default true
  regression explanations for string lemmas
+option stringMinPrefixExplain strings-min-prefix-explain --strings-min-prefix-explain bool :default true
+ minimize explanations for prefix of normal forms in strings
 
 
 endmodule
diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index ffec86477..f1639cc96 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -208,9 +208,9 @@ public:
         if( checkClash(in[0], in[1], rew) ){
           Trace("datatypes-rewrite") << "Rewrite clashing equality " << in << " to false" << std::endl;
           return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(false));
-        }else if( rew.size()==1 && rew[0]!=in ){
-          Trace("datatypes-rewrite") << "Rewrite equality " << in << " to " << rew[0] << std::endl;
-          return RewriteResponse(REWRITE_AGAIN_FULL, rew[0] );
+        //}else if( rew.size()==1 && rew[0]!=in ){
+        //  Trace("datatypes-rewrite") << "Rewrite equality " << in << " to " << rew[0] << std::endl;
+        //  return RewriteResponse(REWRITE_AGAIN_FULL, rew[0] );
         }else if( in[1]<in[0] ){
           Node ins = NodeManager::currentNM()->mkNode(in.getKind(), in[1], in[0]);
           Trace("datatypes-rewrite") << "Swap equality " << in << " to " << ins << std::endl;
diff --git a/src/theory/quantifiers/anti_skolem.cpp b/src/theory/quantifiers/anti_skolem.cpp
new file mode 100644
index 000000000..47b4d95d1
--- /dev/null
+++ b/src/theory/quantifiers/anti_skolem.cpp
@@ -0,0 +1,269 @@
+/*********************                                                        */
+/*! \file anti_skolem.cpp
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  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 anti-skolemization
+ **          ( forall x. P[ f( x ) ] ^ forall x. Q[ f( x ) ]  ) => forall x. exists y. ( P[ y ] ^ Q[ y ] )
+ **/
+
+#include "theory/quantifiers/anti_skolem.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/first_order_model.h"
+#include "options/quantifiers_options.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+
+
+struct sortTypeOrder {
+  TermDb* d_tdb;
+  bool operator() (TypeNode i, TypeNode j) {
+    return d_tdb->getIdForType( i )<d_tdb->getIdForType( j );
+  }
+};
+
+void QuantAntiSkolem::SkQuantTypeCache::add( std::vector< TypeNode >& typs, Node q, unsigned index ) {
+  if( index==typs.size() ){
+    Assert( std::find( d_quants.begin(), d_quants.end(), q )==d_quants.end() );
+    d_quants.push_back( q );
+  }else{
+    d_children[typs[index]].add( typs, q, index+1 );
+  }
+}
+
+void QuantAntiSkolem::SkQuantTypeCache::sendLemmas( QuantAntiSkolem * ask ) {
+  for( std::map< TypeNode, SkQuantTypeCache >::iterator it = d_children.begin(); it != d_children.end(); ++it ){
+    it->second.sendLemmas( ask );
+  }
+  if( !d_quants.empty() ){
+    ask->sendAntiSkolemizeLemma( d_quants );
+  }
+}
+
+bool QuantAntiSkolem::CDSkQuantCache::add( context::Context* c, std::vector< Node >& quants, unsigned index ) {
+  if( index==quants.size() ){
+    if( !d_valid.get() ){
+      d_valid.set( true );
+      return true;
+    }else{
+      return false;
+    }
+  }else{
+    Node n = quants[index];
+    std::map< Node, CDSkQuantCache* >::iterator it = d_data.find( n );
+    CDSkQuantCache* skc;
+    if( it==d_data.end() ){
+      skc = new CDSkQuantCache( c );
+      d_data[n] = skc;
+    }else{
+      skc = it->second;
+    }
+    return skc->add( c, quants, index+1 );
+  }
+}
+
+QuantAntiSkolem::QuantAntiSkolem( QuantifiersEngine * qe ) : QuantifiersModule( qe ){
+  d_sqc = new CDSkQuantCache( qe->getUserContext() );
+}
+
+/* Call during quantifier engine's check */
+void QuantAntiSkolem::check( Theory::Effort e, unsigned quant_e ) {
+  if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){
+    d_sqtc.clear();
+    for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+      Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
+      if( d_quant_processed.find( q )==d_quant_processed.end() ){
+        d_quant_processed[q] = true;
+        Trace("anti-sk") << "Process quantified formula : " << q << std::endl;
+        bool success = false;
+        if( d_quant_sip[q].init( q[1] ) ){
+          Trace("anti-sk") << "- Partitioned to single invocation parts : " << std::endl;
+          d_quant_sip[q].debugPrint( "anti-sk" );
+          //check if it is single invocation
+          if( d_quant_sip[q].isPurelySingleInvocation() ){
+            //for now, only do purely single invocation
+            success = true;
+          }
+        }else{
+          Trace("anti-sk") << "- Failed to initialize." << std::endl;
+        }
+        if( success ){
+          //sort the argument variables
+          d_ask_types[q].insert( d_ask_types[q].end(), d_quant_sip[q].d_arg_types.begin(), d_quant_sip[q].d_arg_types.end() );
+          std::map< TypeNode, std::vector< unsigned > > indices;
+          for( unsigned j=0; j<d_ask_types[q].size(); j++ ){
+            indices[d_ask_types[q][j]].push_back( j );
+          }
+          sortTypeOrder sto;
+          sto.d_tdb = d_quantEngine->getTermDatabase();
+          std::sort( d_ask_types[q].begin(), d_ask_types[q].end(), sto );
+          //increment j on inner loop
+          for( unsigned j=0; j<d_ask_types[q].size();  ){
+            TypeNode curr = d_ask_types[q][j];
+            for( unsigned k=0; k<indices[curr].size(); k++ ){
+              Assert( d_ask_types[q][j]==curr );
+              d_ask_types_index[q].push_back( indices[curr][k] );
+              j++;
+            }
+          }
+          Assert( d_ask_types_index[q].size()==d_ask_types[q].size() );
+        }else{
+          d_quant_sip.erase( q );
+        }
+      }
+      //now, activate the quantified formula
+      std::map< Node, std::vector< TypeNode > >::iterator it = d_ask_types.find( q );
+      if( it!=d_ask_types.end() ){
+        d_sqtc.add( it->second, q );        
+      }
+    }
+    Trace("anti-sk-debug") << "Process lemmas..." << std::endl;
+    //send out lemmas for each anti-skolemizable group of quantified formulas
+    d_sqtc.sendLemmas( this );
+    Trace("anti-sk-debug") << "...Finished process lemmas" << std::endl;
+  }
+}
+
+bool QuantAntiSkolem::sendAntiSkolemizeLemma( std::vector< Node >& quants, bool pconnected ) {
+  Assert( !quants.empty() );
+  std::sort( quants.begin(), quants.end() );
+  if( d_sqc->add( d_quantEngine->getUserContext(), quants ) ){
+    //partition into connected components
+    if( pconnected && quants.size()>1 ){
+      Trace("anti-sk-debug") << "Partition into connected components..." << std::endl;
+      int eqc_count = 0;
+      std::map< Node, int > func_to_eqc;
+      std::map< int, std::vector< Node > > eqc_to_func;
+      std::map< int, std::vector< Node > > eqc_to_quant;
+      for( unsigned i=0; i<quants.size(); i++ ){
+        Node q = quants[i];
+        std::vector< int > eqcs;
+        for( std::map< Node, bool >::iterator it = d_quant_sip[q].d_funcs.begin(); it != d_quant_sip[q].d_funcs.end(); ++it ){
+          Node f = it->first;
+          std::map< Node, int >::iterator itf = func_to_eqc.find( f );
+          if( itf == func_to_eqc.end() ){
+            if( eqcs.empty() ){
+              func_to_eqc[f] = eqc_count;
+              eqc_to_func[eqc_count].push_back( f );
+              eqc_count++;
+            }else{
+              func_to_eqc[f] = eqcs[0];
+              eqc_to_func[eqcs[0]].push_back( f );
+            }
+          }
+          if( std::find( eqcs.begin(), eqcs.end(), func_to_eqc[f] )==eqcs.end() ){
+            eqcs.push_back( func_to_eqc[f] );
+          }
+        }
+        Assert( !eqcs.empty() );
+        //merge equivalence classes
+        int id = eqcs[0];
+        eqc_to_quant[id].push_back( q );
+        for( unsigned j=1; j<eqcs.size(); j++ ){
+          int id2 = eqcs[j];
+          std::map< int, std::vector< Node > >::iterator itef = eqc_to_func.find( id2 );
+          if( itef!=eqc_to_func.end() ){
+            for( unsigned k=0; k<itef->second.size(); k++ ){
+              func_to_eqc[itef->second[k]] = id;
+              eqc_to_func[id].push_back( itef->second[k] );
+            }
+            eqc_to_func.erase( id2 );
+          }
+          itef = eqc_to_quant.find( id2 );
+          if( itef!=eqc_to_quant.end() ){
+            eqc_to_quant[id].insert( eqc_to_quant[id].end(), itef->second.begin(), itef->second.end() );
+            eqc_to_quant.erase( id2 );
+          }
+        }
+      }
+      if( eqc_to_quant.size()>1 ){
+        bool addedLemma = false;
+        for( std::map< int, std::vector< Node > >::iterator it = eqc_to_quant.begin(); it != eqc_to_quant.end(); ++it ){
+          Assert( it->second.size()<quants.size() );
+          bool ret = sendAntiSkolemizeLemma( it->second, false );
+          addedLemma = addedLemma || ret;
+        }
+        return addedLemma;
+      }
+    }    
+    
+    Trace("anti-sk") << "Anti-skolemize group : " << std::endl;
+    for( unsigned i=0; i<quants.size(); i++ ){
+      Trace("anti-sk") << "   " << quants[i] << std::endl;
+    }
+
+    std::vector< Node > outer_vars;
+    std::vector< Node > inner_vars;
+    Node q = quants[0];
+    for( unsigned i=0; i<d_ask_types[q].size(); i++ ){
+      Node v = NodeManager::currentNM()->mkBoundVar( d_ask_types[q][i] );
+      Trace("anti-sk-debug") << "Outer var " << i << " : " << v << std::endl;
+      outer_vars.push_back( v );
+    }
+
+    std::map< Node, Node > func_to_var;
+    std::vector< Node > conj;
+    for( unsigned i=0; i<quants.size(); i++ ){
+      Node q = quants[i];
+      Trace("anti-sk-debug") << "Process " << q << std::endl;
+      std::vector< Node > subs_lhs;
+      std::vector< Node > subs_rhs;
+      //get outer variable substitution
+      Assert( d_ask_types_index[q].size()==d_ask_types[q].size() );
+      for( unsigned j=0; j<d_ask_types_index[q].size(); j++ ){
+        Trace("anti-sk-debug") << " o_subs : " << d_quant_sip[q].d_si_vars[d_ask_types_index[q][j]] << " -> " << outer_vars[j] << std::endl;
+        subs_lhs.push_back( d_quant_sip[q].d_si_vars[d_ask_types_index[q][j]] );
+        subs_rhs.push_back( outer_vars[j] );
+      }
+      //get function substitution
+      for( std::map< Node, bool >::iterator it = d_quant_sip[q].d_funcs.begin(); it != d_quant_sip[q].d_funcs.end(); ++it ){
+        Node f = it->first;
+        Node fv = d_quant_sip[q].d_func_fo_var[it->first];
+        if( func_to_var.find( f )==func_to_var.end() ){
+          Node v = NodeManager::currentNM()->mkBoundVar( fv.getType() );
+          Trace("anti-sk-debug") << "Inner var for " << f << " : " << v << std::endl;
+          inner_vars.push_back( v );
+          func_to_var[f] = v;
+        }
+        subs_lhs.push_back( fv );
+        subs_rhs.push_back( func_to_var[f] );
+        Trace("anti-sk-debug") << " i_subs : " << fv << " -> " << func_to_var[f] << std::endl;
+      }
+      Node c = d_quant_sip[q].getSingleInvocation();
+      if( !subs_lhs.empty() ){
+        c = c.substitute( subs_lhs.begin(), subs_lhs.end(), subs_rhs.begin(), subs_rhs.end() );
+      }
+      conj.push_back( c );
+    }
+    Node body = conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( kind::AND, conj );
+    if( !inner_vars.empty() ){
+      Node bvl = NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, inner_vars );
+      body = NodeManager::currentNM()->mkNode( kind::EXISTS, bvl, body );
+    }
+    if( !outer_vars.empty() ){
+      Node bvl = NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, outer_vars );
+      body = NodeManager::currentNM()->mkNode( kind::FORALL, bvl, body );
+    }
+    Trace("anti-sk") << "Produced : " << body << std::endl;
+    quants.push_back( body.negate() );
+    Node lem = NodeManager::currentNM()->mkNode( kind::AND, quants ).negate();
+    Trace("anti-sk-lemma") << "Anti-skolemize lemma : " << lem << std::endl;
+    quants.pop_back();
+    return d_quantEngine->addLemma( lem ); 
+  }else{
+    return false;
+  }
+}
+
diff --git a/src/theory/quantifiers/anti_skolem.h b/src/theory/quantifiers/anti_skolem.h
new file mode 100644
index 000000000..cf24e2751
--- /dev/null
+++ b/src/theory/quantifiers/anti_skolem.h
@@ -0,0 +1,75 @@
+/*********************                                                        */
+/*! \file anti_skolem.h
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief dynamic quantifiers splitting
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANT_ANTI_SKOLEM_H
+#define __CVC4__THEORY__QUANT_ANTI_SKOLEM_H
+
+#include "theory/quantifiers_engine.h"
+#include "context/cdo.h"
+#include "theory/quantifiers/ce_guided_single_inv.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class QuantAntiSkolem : public QuantifiersModule {
+  typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
+private:
+  std::map< Node, bool > d_quant_processed;
+  std::map< Node, SingleInvocationPartition > d_quant_sip;
+  std::map< Node, std::vector< TypeNode > > d_ask_types;
+  std::map< Node, std::vector< unsigned > > d_ask_types_index;
+  
+  class SkQuantTypeCache {
+  public:
+    std::map< TypeNode, SkQuantTypeCache > d_children;
+    std::vector< Node > d_quants;
+    void add( std::vector< TypeNode >& typs, Node q, unsigned index = 0 );
+    void clear() { 
+      d_children.clear();
+      d_quants.clear(); 
+    }
+    void sendLemmas( QuantAntiSkolem * ask );
+  }; 
+  SkQuantTypeCache d_sqtc;
+  
+  class CDSkQuantCache {
+  public:
+    CDSkQuantCache( context::Context* c ) : d_valid( c, false ){}
+    std::map< Node, CDSkQuantCache* > d_data;
+    context::CDO< bool > d_valid;
+    bool add( context::Context* c, std::vector< Node >& quants, unsigned index = 0 );
+  };
+  CDSkQuantCache * d_sqc;
+public:
+  bool sendAntiSkolemizeLemma( std::vector< Node >& quants, bool pconnected = true );
+public:
+  QuantAntiSkolem( QuantifiersEngine * qe );
+
+  /* Call during quantifier engine's check */
+  void check( Theory::Effort e, unsigned quant_e );
+  /* Called for new quantifiers */
+  void registerQuantifier( Node q ) {}
+  void assertNode( Node n ) {}
+  /** Identify this module (for debugging, dynamic configuration, etc..) */
+  std::string identify() const { return "QuantAntiSkolem"; }
+};
+
+}
+}
+}
+
+#endif
diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index 7ef23077f..80585a33d 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -149,8 +149,7 @@ void CegConjectureSingleInv::initialize( Node q ) {
   bool singleInvocation = true;
   if( type_valid==0 ){
     //process the single invocation-ness of the property
-    d_sip->init( types );
-    d_sip->process( qq );
+    d_sip->init( types, qq );
     Trace("cegqi-si") << "- Partitioned to single invocation parts : " << std::endl;
     d_sip->debugPrint( "cegqi-si" );
     //map from program to bound variables
@@ -839,7 +838,41 @@ void CegConjectureSingleInv::preregisterConjecture( Node q ) {
   d_orig_conjecture = q;
 }
 
-void SingleInvocationPartition::init( std::vector< TypeNode >& typs ){
+bool SingleInvocationPartition::init( Node n ) {
+  //first, get types of arguments for functions
+  std::vector< TypeNode > typs;
+  std::map< Node, bool > visited;
+  if( inferArgTypes( n, typs, visited ) ){
+    return init( typs, n );  
+  }else{
+    return false;
+  }
+}
+
+bool SingleInvocationPartition::inferArgTypes( Node n, std::vector< TypeNode >& typs, std::map< Node, bool >& visited ) {
+  if( visited.find( n )==visited.end() ){
+    visited[n] = true;
+    if( n.getKind()!=FORALL ){
+    //if( TermDb::hasBoundVarAttr( n ) ){
+      if( n.getKind()==APPLY_UF ){
+        for( unsigned i=0; i<n.getNumChildren(); i++ ){
+          typs.push_back( n[i].getType() );
+        }
+        return true;
+      }else{
+        for( unsigned i=0; i<n.getNumChildren(); i++ ){
+          if( inferArgTypes( n[i], typs, visited ) ){
+            return true;
+          }
+        }
+      }
+    //}
+    }
+  }
+  return false;
+}
+
+bool SingleInvocationPartition::init( std::vector< TypeNode >& typs, Node n ){
   Assert( d_arg_types.empty() );
   Assert( d_si_vars.empty() );
   d_arg_types.insert( d_arg_types.end(), typs.begin(), typs.end() );
@@ -849,6 +882,8 @@ void SingleInvocationPartition::init( std::vector< TypeNode >& typs ){
     Node si_v = NodeManager::currentNM()->mkBoundVar( ss.str(), d_arg_types[j] );
     d_si_vars.push_back( si_v );
   }
+  process( n );
+  return true;
 }
 
 
@@ -984,43 +1019,45 @@ bool SingleInvocationPartition::processConjunct( Node n, std::map< Node, bool >&
     return true;
   }else{
     bool ret = true;
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      if( !processConjunct( n[i], visited, args, terms, subs ) ){
-        ret = false;
+    //if( TermDb::hasBoundVarAttr( n ) ){
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        if( !processConjunct( n[i], visited, args, terms, subs ) ){
+          ret = false;
+        }
       }
-    }
-    if( ret ){
-      if( n.getKind()==APPLY_UF ){
-        if( std::find( terms.begin(), terms.end(), n )==terms.end() ){
-          Node f = n.getOperator();
-          //check if it matches the type requirement
-          if( isAntiSkolemizableType( f ) ){
-            if( args.empty() ){
-              //record arguments
-              for( unsigned i=0; i<n.getNumChildren(); i++ ){
-                args.push_back( n[i] );
-              }
-            }else{
-              //arguments must be the same as those already recorded
-              for( unsigned i=0; i<n.getNumChildren(); i++ ){
-                if( args[i]!=n[i] ){
-                  Trace("si-prt-debug") << "...bad invocation : " << n << " at arg " << i << "." << std::endl;
-                  ret = false;
-                  break;
+      if( ret ){
+        if( n.getKind()==APPLY_UF ){
+          if( std::find( terms.begin(), terms.end(), n )==terms.end() ){
+            Node f = n.getOperator();
+            //check if it matches the type requirement
+            if( isAntiSkolemizableType( f ) ){
+              if( args.empty() ){
+                //record arguments
+                for( unsigned i=0; i<n.getNumChildren(); i++ ){
+                  args.push_back( n[i] );
+                }
+              }else{
+                //arguments must be the same as those already recorded
+                for( unsigned i=0; i<n.getNumChildren(); i++ ){
+                  if( args[i]!=n[i] ){
+                    Trace("si-prt-debug") << "...bad invocation : " << n << " at arg " << i << "." << std::endl;
+                    ret = false;
+                    break;
+                  }
                 }
               }
+              if( ret ){
+                terms.push_back( n );
+                subs.push_back( d_func_inv[f] );
+              }
+            }else{
+              Trace("si-prt-debug") << "... " << f << " is a bad operator." << std::endl;
+              ret = false;
             }
-            if( ret ){
-              terms.push_back( n );
-              subs.push_back( d_func_inv[f] );
-            }
-          }else{
-            Trace("si-prt-debug") << "... " << f << " is a bad operator." << std::endl;
-            ret = false;
           }
         }
       }
-    }
+    //}
     visited[n] = ret;
     return ret;
   }
@@ -1037,6 +1074,7 @@ bool SingleInvocationPartition::isAntiSkolemizableType( Node f ) {
       ret = true;
       std::vector< Node > children;
       children.push_back( f );
+      //TODO: permutations of arguments
       for( unsigned i=0; i<d_arg_types.size(); i++ ){
         children.push_back( d_si_vars[i] );
         if( tn[i]!=d_arg_types[i] ){
diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h
index c414a51bd..fe48a0dc3 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/ce_guided_single_inv.h
@@ -153,18 +153,19 @@ public:
 class SingleInvocationPartition
 {
 private:
+  bool inferArgTypes( Node n, std::vector< TypeNode >& typs, std::map< Node, bool >& visited );
+  void process( Node n );
   bool collectConjuncts( Node n, bool pol, std::vector< Node >& conj );
   bool processConjunct( Node n, std::map< Node, bool >& visited, std::vector< Node >& args,
                         std::vector< Node >& terms, std::vector< Node >& subs );
   Node getSpecificationInst( Node n, std::map< Node, Node >& lam, std::map< Node, Node >& visited );
   void extractInvariant2( Node n, Node& func, int& pol, std::vector< Node >& disjuncts, bool hasPol, std::map< Node, bool >& visited );
 public:
-  void init( std::vector< TypeNode >& typs );
-  //inputs
-  void process( Node n );
-  std::vector< TypeNode > d_arg_types;
+  bool init( Node n );
+  bool init( std::vector< TypeNode >& typs, Node n );
 
   //outputs (everything is with bound var)
+  std::vector< TypeNode > d_arg_types;
   std::map< Node, bool > d_funcs;
   std::map< Node, Node > d_func_inv;
   std::map< Node, Node > d_inv_to_func;
@@ -187,6 +188,8 @@ public:
 
   void extractInvariant( Node n, Node& func, int& pol, std::vector< Node >& disjuncts );
 
+  bool isPurelySingleInvocation() { return d_conjuncts[1].empty(); }
+
   void debugPrint( const char * c );
 };
 
diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp
index 1ae1c3c5f..bff429e7c 100644
--- a/src/theory/quantifiers/quant_split.cpp
+++ b/src/theory/quantifiers/quant_split.cpp
@@ -9,7 +9,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief Implementation of local theory ext utilities
+ ** \brief Implementation of dynamic quantifiers splitting
  **/
 
 #include "theory/quantifiers/quant_split.h"
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 9568966d6..7cda713a1 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -40,6 +40,7 @@
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/trigger.h"
 #include "theory/quantifiers/quant_split.h"
+#include "theory/quantifiers/anti_skolem.h"
 #include "theory/theory_engine.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/uf/theory_uf.h"
@@ -123,6 +124,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext*
   d_inst_engine = NULL;
   d_i_cbqi = NULL;
   d_qsplit = NULL;
+  d_anti_skolem = NULL;
   d_model_engine = NULL;
   d_bint = NULL;
   d_rr_engine = NULL;
@@ -164,6 +166,7 @@ QuantifiersEngine::~QuantifiersEngine(){
   delete d_fs;
   delete d_i_cbqi;
   delete d_qsplit;
+  delete d_anti_skolem;
 }
 
 EqualityQueryQuantifiersEngine* QuantifiersEngine::getEqualityQuery() {
@@ -245,6 +248,10 @@ void QuantifiersEngine::finishInit(){
     d_qsplit = new quantifiers::QuantDSplit( this, c );
     d_modules.push_back( d_qsplit );
   }
+  if( options::quantAntiSkolem() ){
+    d_anti_skolem = new quantifiers::QuantAntiSkolem( this );
+    d_modules.push_back( d_anti_skolem );
+  }
   if( options::quantAlphaEquiv() ){
     d_alpha_equiv = new quantifiers::AlphaEquivalence( this );
   }
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index b9ce2063a..92296ebac 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -101,6 +101,7 @@ namespace quantifiers {
   class InstStrategyCbqi;
   class InstStrategyCegqi;
   class QuantDSplit;
+  class QuantAntiSkolem;
 }/* CVC4::theory::quantifiers */
 
 namespace inst {
@@ -162,6 +163,8 @@ private:
   quantifiers::InstStrategyCbqi * d_i_cbqi;
   /** quantifiers splitting */
   quantifiers::QuantDSplit * d_qsplit;
+  /** quantifiers anti-skolemization */
+  quantifiers::QuantAntiSkolem * d_anti_skolem;
 public: //effort levels
   enum {
     QEFFORT_CONFLICT,
@@ -260,6 +263,8 @@ public:  //modules
   quantifiers::InstStrategyCbqi * getInstStrategyCbqi() { return d_i_cbqi; }
   /** get quantifiers splitting */
   quantifiers::QuantDSplit * getQuantDSplit() { return d_qsplit; }
+  /** get quantifiers anti-skolemization */
+  quantifiers::QuantAntiSkolem * getQuantAntiSkolem() { return d_anti_skolem; }
 private:
   /** owner of quantified formulas */
   std::map< Node, QuantifiersModule * > d_owner;
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index dd498a2d2..d8a46f0ed 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -1705,14 +1705,16 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & n
       std::vector< std::vector< Node > > normal_forms;
       // explanation for each normal form (phi)
       std::vector< std::vector< Node > > normal_forms_exp;
+      // dependency information 
+      std::vector< std::map< Node, std::map< bool, int > > > normal_forms_exp_depend;
       // record terms for each normal form (t)
       std::vector< Node > normal_form_src;
       //Get Normal Forms
-      result = getNormalForms(eqc, nf, normal_forms, normal_forms_exp, normal_form_src);
+      result = getNormalForms(eqc, normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend);
       if( hasProcessed() ){
-          return true;
+        return true;
       }else if( result ){
-        if( processNEqc(normal_forms, normal_forms_exp, normal_form_src) ){
+        if( processNEqc(normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend) ){
           return true;
         }
       }
@@ -1720,18 +1722,33 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & n
       if( normal_forms.empty() ){
         Trace("strings-solve-debug2") << "construct the normal form" << std::endl;
         getConcatVec( eqc, nf );
+        d_normal_forms_base[eqc] = 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( eqc.eqNode( normal_form_src[0] ) );
+        int nf_index = 0;
+        //nf.insert( nf.end(), normal_forms[nf_index].begin(), normal_forms[nf_index].end() );
+        //nf_exp.insert( nf_exp.end(), normal_forms_exp[nf_index].begin(), normal_forms_exp[nf_index].end() );
+        //Trace("strings-solve-debug2") << "take normal form ... done" << std::endl;
+        //d_normal_forms_base[eqc] = normal_form_src[nf_index];
+        ///*
+        std::vector< Node >::iterator itn = std::find( normal_form_src.begin(), normal_form_src.end(), eqc );
+        if( itn!=normal_form_src.end() ){
+          nf_index = itn - normal_form_src.begin();
+          Trace("strings-solve-debug2") << "take normal form " << nf_index << std::endl;
+          Assert( normal_form_src[nf_index]==eqc );
+        }else{
+          //just take the first normal form
+          Trace("strings-solve-debug2") << "take the first normal form" << std::endl;
         }
-        Trace("strings-solve-debug2") << "just take the first normal form ... done" << std::endl;
+        nf.insert( nf.end(), normal_forms[nf_index].begin(), normal_forms[nf_index].end() );
+        nf_exp.insert( nf_exp.end(), normal_forms_exp[nf_index].begin(), normal_forms_exp[nf_index].end() );
+        //if( eqc!=normal_form_src[nf_index] ){
+        //  nf_exp.push_back( eqc.eqNode( normal_form_src[nf_index] ) );
+        //}
+        Trace("strings-solve-debug2") << "take normal form ... done" << std::endl;
+        d_normal_forms_base[eqc] = normal_form_src[nf_index];
+        //*/
       }
 
-      d_normal_forms_base[eqc] = normal_form_src.empty() ? eqc : normal_form_src[0];
       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-debug") << "Return process equivalence class " << eqc << " : returned, size = " << nf.size() << std::endl;
@@ -1745,9 +1762,8 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & n
   }
 }
 
-bool TheoryStrings::getNormalForms( Node &eqc, 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) {
+bool TheoryStrings::getNormalForms( Node &eqc, std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src,
+                                    std::vector< std::vector< Node > > &normal_forms_exp, std::vector< std::map< Node, std::map< bool, int > > >& normal_forms_exp_depend ) {
   Trace("strings-process-debug") << "Get normal forms " << eqc << std::endl;
   eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
   while( !eqc_i.isFinished() ){
@@ -1755,8 +1771,9 @@ bool TheoryStrings::getNormalForms( Node &eqc, std::vector< Node > & nf,
     if( d_congruent.find( n )==d_congruent.end() ){
       if( n.getKind() == kind::CONST_STRING || n.getKind() == kind::STRING_CONCAT ){
         Trace("strings-process-debug") << "Get Normal Form : Process term " << n << " in eqc " << eqc << std::endl;
-        std::vector<Node> nf_n;
-        std::vector<Node> nf_exp_n;
+        std::vector< Node > nf_n;
+        std::vector< Node > nf_exp_n;
+        std::map< Node, std::map< bool, int > > nf_exp_depend_n;
         if( n.getKind()==kind::CONST_STRING ){
           if( n!=d_emptyString ) {
             nf_n.push_back( n );
@@ -1764,33 +1781,55 @@ bool TheoryStrings::getNormalForms( Node &eqc, std::vector< Node > & nf,
         }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-debug") << "Normalizing subterm " << n[i] << " = "  << nr << std::endl;
             Assert( d_normal_forms.find( nr )!=d_normal_forms.end() );
-            nf_temp.insert( nf_temp.end(), d_normal_forms[nr].begin(), d_normal_forms[nr].end() );
-            nf_exp_temp.insert( nf_exp_temp.end(), d_normal_forms_exp[nr].begin(), d_normal_forms_exp[nr].end() );
+            unsigned orig_size = nf_n.size();
+            unsigned add_size = d_normal_forms[nr].size();
             //if not the empty string, add to current normal form
-            if( nf.size()!=1 || nf[0]!=d_emptyString ){
-              for( unsigned r=0; r<nf_temp.size(); r++ ) {
+            if( !d_normal_forms[nr].empty() ){
+              for( unsigned r=0; r<d_normal_forms[nr].size(); r++ ) {
                 if( Trace.isOn("strings-error") ) {
-                  if( nf_temp[r].getKind()==kind::STRING_CONCAT ){
+                  if( d_normal_forms[nr][r].getKind()==kind::STRING_CONCAT ){
                     Trace("strings-error") << "Strings::Error: From eqc = " << eqc << ", " << n << " index " << i << ", bad normal form : ";
-                    for( unsigned rr=0; rr<nf_temp.size(); rr++ ) {
-                      Trace("strings-error") << nf_temp[rr] << " ";
+                    for( unsigned rr=0; rr<d_normal_forms[nr].size(); rr++ ) {
+                      Trace("strings-error") << d_normal_forms[nr][rr] << " ";
                     }
                     Trace("strings-error") << std::endl;
                   }
                 }
-                Assert( nf_temp[r].getKind()!=kind::STRING_CONCAT );
+                Assert( d_normal_forms[nr][r].getKind()!=kind::STRING_CONCAT );
+              }
+              nf_n.insert( nf_n.end(), d_normal_forms[nr].begin(), d_normal_forms[nr].end() );
+            }
+
+            for( unsigned j=0; j<d_normal_forms_exp[nr].size(); j++ ){
+              Node exp = d_normal_forms_exp[nr][j];
+              nf_exp_n.push_back( exp );
+              //track depends
+              for( unsigned k=0; k<2; k++ ){
+                int prev_dep = d_normal_forms_exp_depend[nr][exp][k==1];
+                if( k==0 ){
+                  nf_exp_depend_n[exp][false] = orig_size + prev_dep;
+                }else if( k==1 ){
+                  //store forward index (restored to reverse index below)
+                  nf_exp_depend_n[exp][true] = orig_size + ( add_size - prev_dep );
+                }
               }
-              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( n[i].eqNode( nr ) );
+              Node eq = n[i].eqNode( nr );
+              nf_exp_n.push_back( eq );
+              //track depends
+              nf_exp_depend_n[eq][false] = orig_size;
+              nf_exp_depend_n[eq][true] = orig_size + add_size;
             }
           }
+          //convert forward indices to reverse indices
+          int total_size = nf_n.size();
+          for( std::map< Node, std::map< bool, int > >::iterator it = nf_exp_depend_n.begin(); it != nf_exp_depend_n.end(); ++it ){
+            it->second[true] = total_size - it->second[true];
+            Assert( it->second[true]>=0 );
+          }
         }
         //if not equal to self
         if( nf_n.size()>1 || ( nf_n.size()==1 && nf_n[0].getKind()==kind::CONST_STRING ) ){
@@ -1805,8 +1844,9 @@ bool TheoryStrings::getNormalForms( Node &eqc, std::vector< Node > & nf,
             }
           }
           normal_forms.push_back(nf_n);
-          normal_forms_exp.push_back(nf_exp_n);
           normal_form_src.push_back(n);
+          normal_forms_exp.push_back(nf_exp_n);
+          normal_forms_exp_depend.push_back(nf_exp_depend_n);
         }else{
           //this was redundant: combination of self + empty string(s)
           Node nn = nf_n.size()==0 ? d_emptyString : nf_n[0];
@@ -1850,72 +1890,92 @@ bool TheoryStrings::getNormalForms( Node &eqc, std::vector< Node > & nf,
             }
             Trace("strings-solve") << normal_forms_exp[i][j];
           }
+          Trace("strings-solve") << std::endl;
+          Trace("strings-solve") << "WITH DEPENDENCIES : " << std::endl;
+          for( unsigned j=0; j<normal_forms_exp[i].size(); j++ ) {
+            Trace("strings-solve") << "   " << normal_forms_exp[i][j] << " -> ";
+            Trace("strings-solve") << normal_forms_exp_depend[i][normal_forms_exp[i][j]][false] << ",";
+            Trace("strings-solve") << normal_forms_exp_depend[i][normal_forms_exp[i][j]][true] << std::endl;
+          }
         }
         Trace("strings-solve") << std::endl;
+        
       }
     } else {
-      //std::vector< Node > nf;
-      //nf.push_back( eqc );
-      //normal_forms.push_back(nf);
-      //std::vector< Node > nf_exp_def;
-      //normal_forms_exp.push_back(nf_exp_def);
-      //normal_form_src.push_back(eqc);
       Trace("strings-solve") << "--- Single normal form for equivalence class " << eqc << std::endl;
     }
   }
   return true;
 }
 
+void TheoryStrings::getExplanationVectorForPrefix( std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src,
+                                                   std::vector< std::vector< Node > > &normal_forms_exp, std::vector< std::map< Node, std::map< bool, int > > >& normal_forms_exp_depend,
+                                                   unsigned i, unsigned j, int index, bool isRev, std::vector< Node >& curr_exp ) {
+  if( index==-1 || !options::stringMinPrefixExplain() ){
+    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() );
+  }else{
+    Trace("strings-explain-prefix") << "Get explanation for prefix " << index << " of normal forms " << i << " and " << j << ", reverse = " << isRev << std::endl;
+    for( unsigned r=0; r<2; r++ ){
+      int tindex = r==0 ? i : j;
+      for( unsigned k=0; k<normal_forms_exp[tindex].size(); k++ ){
+        Node exp = normal_forms_exp[tindex][k];
+        int dep = normal_forms_exp_depend[tindex][exp][isRev];
+        if( dep<=index ){
+          curr_exp.push_back( exp );
+          Trace("strings-explain-prefix-debug") << "  include : " << exp << std::endl;
+        }else{
+          Trace("strings-explain-prefix-debug") << "  exclude : " << exp << std::endl;
+        }
+      }
+    }
+    Trace("strings-explain-prefix") << "Included " << curr_exp.size() << " / " << ( normal_forms_exp[i].size() + normal_forms_exp[j].size() ) << std::endl;
+  }
+  if( normal_form_src[i]!=normal_form_src[j] ){
+    curr_exp.push_back( normal_form_src[i].eqNode( normal_form_src[j] ) );
+  }
+}
 
-bool TheoryStrings::processNEqc( std::vector< std::vector< Node > > &normal_forms, std::vector< std::vector< Node > > &normal_forms_exp,
-                                 std::vector< Node > &normal_form_src) {
+bool TheoryStrings::processNEqc( std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src,
+                                 std::vector< std::vector< Node > > &normal_forms_exp, std::vector< std::map< Node, std::map< bool, int > > >& normal_forms_exp_depend ) {
   bool flag_lb = false;
   std::vector< Node > c_lb_exp;
-  int c_i, c_j, c_loop_n_index, c_other_n_index, c_loop_index, c_index, c_other_index;
+  int c_i, c_j, c_loop_n_index, c_other_n_index, c_loop_index, c_index;
   for(unsigned i=0; i<normal_forms.size()-1; i++) {
     //unify each normalform[j] with normal_forms[i]
     for(unsigned j=i+1; j<normal_forms.size(); j++ ) {
       Trace("strings-solve") << "Strings: Process normal form #" << i << " against #" << j << "..." << std::endl;
       if( isNormalFormPair( normal_form_src[i], normal_form_src[j] ) ) {
         Trace("strings-solve") << "Strings: Already cached." << std::endl;
-      } else {
-        //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() );
-        if( normal_form_src[i]!=normal_form_src[j] ){
-          curr_exp.push_back( normal_form_src[i].eqNode( normal_form_src[j] ) );
-        }
-
+      }else{
         //process the reverse direction first (check for easy conflicts and inferences)
-        if( processReverseNEq( normal_forms, normal_form_src, curr_exp, i, j ) ){
+        if( processReverseNEq( normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend, i, j ) ){
           return true;
         }
 
         //ensure that normal_forms[i] and normal_forms[j] are the same modulo equality
-        unsigned index_i = 0;
-        unsigned index_j = 0;
+        unsigned index = 0;
         bool success;
         do{
           //simple check
-          if( processSimpleNEq( normal_forms, normal_form_src, curr_exp, i, j, index_i, index_j, false ) ){
+          if( processSimpleNEq( normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend, i, j, index, false ) ){
             //added a lemma, return
             return true;
           }
 
           success = false;
           //if we are at the end
-          if(index_i==normal_forms[i].size() || index_j==normal_forms[j].size() ) {
-            Assert( index_i==normal_forms[i].size() && index_j==normal_forms[j].size() );
+          if(index==normal_forms[i].size() || index==normal_forms[j].size() ) {
+            Assert( index==normal_forms[i].size() && index==normal_forms[j].size() );
             //we're done
             //addNormalFormPair( normal_form_src[i], normal_form_src[j] );
           } else {
             std::vector< Node > lexp;
-            Node length_term_i = getLength( normal_forms[i][index_i], lexp );
-            Node length_term_j = getLength( normal_forms[j][index_j], lexp );
+            Node length_term_i = getLength( normal_forms[i][index], lexp );
+            Node length_term_j = getLength( normal_forms[j][index], lexp );
             //check  length(normal_forms[i][index]) == length(normal_forms[j][index])
             if( !areDisequal(length_term_i, length_term_j) && !areEqual(length_term_i, length_term_j) &&
-                normal_forms[i][index_i].getKind()!=kind::CONST_STRING && normal_forms[j][index_j].getKind()!=kind::CONST_STRING ) {
+                normal_forms[i][index].getKind()!=kind::CONST_STRING && normal_forms[j][index].getKind()!=kind::CONST_STRING ) {
               //length terms are equal, merge equivalence classes if not already done so
               Node length_eq = NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_j );
               Trace("strings-solve-debug") << "Non-simple Case 1 : string lengths neither equal nor disequal" << std::endl;
@@ -1928,23 +1988,21 @@ bool TheoryStrings::processNEqc( std::vector< std::vector< Node > > &normal_form
               Trace("strings-solve-debug") << "Non-simple Case 2 : must compare strings" << std::endl;
               int loop_in_i = -1;
               int loop_in_j = -1;
-              if( detectLoop(normal_forms, i, j, index_i, index_j, loop_in_i, loop_in_j) ){
+              if( detectLoop(normal_forms, i, j, index, loop_in_i, loop_in_j) ){
                 if( !flag_lb ){
                   c_i = i;
                   c_j = j;
                   c_loop_n_index = loop_in_i!=-1 ? i : j;
                   c_other_n_index = loop_in_i!=-1 ? j : i;
                   c_loop_index = loop_in_i!=-1 ? loop_in_i : loop_in_j;
-                  c_index = loop_in_i!=-1 ? index_i : index_j;
-                  c_other_index = loop_in_i!=-1 ? index_j : index_i;
-
-                  c_lb_exp = curr_exp;
+                  c_index = index;
+                  
+                  getExplanationVectorForPrefix( normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend, i, j, -1, false, c_lb_exp );
 
                   if(options::stringLB() == 0) {
                     flag_lb = true;
                   } else {
-                    if(processLoop(c_lb_exp, normal_forms, normal_form_src,
-                      c_i, c_j, c_loop_n_index, c_other_n_index, c_loop_index, c_index, c_other_index)) {
+                    if(processLoop(c_lb_exp, normal_forms, normal_form_src, c_i, c_j, c_loop_n_index, c_other_n_index, c_loop_index, c_index)) {
                       return true;
                     }
                   }
@@ -1953,26 +2011,24 @@ bool TheoryStrings::processNEqc( std::vector< std::vector< Node > > &normal_form
                 Node conc;
                 std::vector< Node > antec;
                 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( normal_forms[i][index].getKind() == kind::CONST_STRING || normal_forms[j][index].getKind() == kind::CONST_STRING) {
+                  unsigned const_k = normal_forms[i][index].getKind() == kind::CONST_STRING ? i : j;
+                  unsigned nconst_k = normal_forms[i][index].getKind() == kind::CONST_STRING ? j : i;
+                  Node const_str = normal_forms[const_k][index];
+                  Node other_str = normal_forms[nconst_k][index];
                   Assert( other_str.getKind()!=kind::CONST_STRING, "Other string is not constant." );
                   Assert( other_str.getKind()!=kind::STRING_CONCAT, "Other string is not CONCAT." );
                   if( !d_equalityEngine.areDisequal(other_str, d_emptyString, true) ) {
                     sendSplit( other_str, d_emptyString, "Len-Split(CST)" );
                   } else {
                     Assert(areDisequal(other_str, d_emptyString), "CST Split on empty Var");
-                    antec.insert( antec.end(), curr_exp.begin(), curr_exp.end() );
+                    getExplanationVectorForPrefix( normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend, i, j, index, false, antec );
                     Node xnz = other_str.eqNode(d_emptyString).negate();
                     antec.push_back( xnz );
                     Node conc;
-                    if( normal_forms[nconst_k].size() > nconst_index_k + 1 && normal_forms[nconst_k][nconst_index_k + 1].isConst() ) {
+                    if( normal_forms[nconst_k].size() > index + 1 && normal_forms[nconst_k][index + 1].isConst() ) {
                       CVC4::String stra = const_str.getConst<String>();
-                      CVC4::String strb = normal_forms[nconst_k][nconst_index_k + 1].getConst<String>();
+                      CVC4::String strb = normal_forms[nconst_k][index + 1].getConst<String>();
                       CVC4::String stra1 = stra.substr(1);
                       size_t p = stra.size() - stra1.overlap(strb);
                       size_t p2 = stra1.find(strb);
@@ -1996,7 +2052,7 @@ bool TheoryStrings::processNEqc( std::vector< std::vector< Node > > &normal_form
                   return true;
                 } else {
                   std::vector< Node > antec_new_lits;
-                  antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
+                  getExplanationVectorForPrefix( normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend, i, j, index, false, antec );
 
                   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 ) ){
@@ -2007,7 +2063,7 @@ bool TheoryStrings::processNEqc( std::vector< std::vector< Node > > &normal_form
 
                   //x!=e /\ y!=e
                   for(unsigned xory=0; xory<2; xory++) {
-                    Node x = xory==0 ? normal_forms[i][index_i] : normal_forms[j][index_j];
+                    Node x = xory==0 ? normal_forms[i][index] : normal_forms[j][index];
                     Node xgtz = x.eqNode( d_emptyString ).negate();
                     if( d_equalityEngine.areDisequal( x, d_emptyString, true ) ) {
                       antec.push_back( xgtz );
@@ -2015,9 +2071,9 @@ bool TheoryStrings::processNEqc( std::vector< std::vector< Node > > &normal_form
                       antec_new_lits.push_back( xgtz );
                     }
                   }
-                  Node sk = mkSkolemCached( normal_forms[i][index_i], normal_forms[j][index_j], sk_id_v_spt, "v_spt", 1 );
-                  Node eq1 = normal_forms[i][index_i].eqNode( mkConcat(normal_forms[j][index_j], sk) );
-                  Node eq2 = normal_forms[j][index_j].eqNode( mkConcat(normal_forms[i][index_i], sk) );
+                  Node sk = mkSkolemCached( normal_forms[i][index], normal_forms[j][index], sk_id_v_spt, "v_spt", 1 );
+                  Node eq1 = normal_forms[i][index].eqNode( mkConcat(normal_forms[j][index], sk) );
+                  Node eq2 = normal_forms[j][index].eqNode( mkConcat(normal_forms[i][index], sk) );
                   if( options::stringCheckEntailLen() ){
                     //check entailment
                     for( unsigned e=0; e<2; e++ ){
@@ -2054,8 +2110,7 @@ bool TheoryStrings::processNEqc( std::vector< std::vector< Node > > &normal_form
     }
   }
   if(flag_lb) {
-    if(processLoop(c_lb_exp, normal_forms, normal_form_src,
-      c_i, c_j, c_loop_n_index, c_other_n_index, c_loop_index, c_index, c_other_index)) {
+    if(processLoop(c_lb_exp, normal_forms, normal_form_src, c_i, c_j, c_loop_n_index, c_other_n_index, c_loop_index, c_index)) {
       return true;
     }
   }
@@ -2064,16 +2119,14 @@ bool TheoryStrings::processNEqc( std::vector< std::vector< Node > > &normal_form
 }
 
 bool TheoryStrings::processReverseNEq( std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src,
-                                       std::vector< Node > &curr_exp, unsigned i, unsigned j ) {
+                                       std::vector< std::vector< Node > > &normal_forms_exp, std::vector< std::map< Node, std::map< bool, int > > >& normal_forms_exp_depend,
+                                       unsigned i, unsigned j ) {
   //reverse normal form of i, j
   std::reverse( normal_forms[i].begin(), normal_forms[i].end() );
   std::reverse( normal_forms[j].begin(), normal_forms[j].end() );
 
-  std::vector< Node > t_curr_exp;
-  t_curr_exp.insert( t_curr_exp.begin(), curr_exp.begin(), curr_exp.end() );
-  unsigned index_i = 0;
-  unsigned index_j = 0;
-  bool ret = processSimpleNEq( normal_forms, normal_form_src, t_curr_exp, i, j, index_i, index_j, true );
+  unsigned index = 0;
+  bool ret = processSimpleNEq( normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend, i, j, index, true );
 
   //reverse normal form of i, j
   std::reverse( normal_forms[i].begin(), normal_forms[i].end() );
@@ -2082,20 +2135,23 @@ bool TheoryStrings::processReverseNEq( std::vector< std::vector< Node > > &norma
   return ret;
 }
 
-bool TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src, std::vector< Node > &curr_exp,
-                                      unsigned i, unsigned j, unsigned& index_i, unsigned& index_j, bool isRev ) {
+bool TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src, 
+                                      std::vector< std::vector< Node > > &normal_forms_exp, std::vector< std::map< Node, std::map< bool, int > > >& normal_forms_exp_depend,
+                                      unsigned i, unsigned j, unsigned& index, bool isRev ) {
   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() ) {
+    if(index==normal_forms[i].size() || index==normal_forms[j].size() ) {
+      if( index==normal_forms[i].size() && index==normal_forms[j].size() ) {
         //we're done
       } 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;
+        unsigned k = index==normal_forms[i].size() ? j : i;
+        unsigned index_k = index;
         //Node eq_exp = mkAnd( curr_exp );
+        std::vector< Node > curr_exp;
+        getExplanationVectorForPrefix( normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend, i, j, -1, isRev, curr_exp );
         while(!d_conflict && index_k<normal_forms[k].size()) {
           //can infer that this string must be empty
           Node eq = normal_forms[k][index_k].eqNode( d_emptyString );
@@ -2107,41 +2163,37 @@ bool TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal
         return true;
       }
     }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") << "Process " << normal_forms[i][index] << " ... " << normal_forms[j][index] << std::endl;
+      if( normal_forms[i][index]==normal_forms[j][index] ){
         Trace("strings-solve-debug") << "Simple Case 1 : strings are equal" << std::endl;
-        //terms are equal, continue
-        if( normal_forms[i][index_i]!=normal_forms[j][index_j] ){
-          Node eq = normal_forms[i][index_i].eqNode(normal_forms[j][index_j]);
-          Trace("strings-solve-debug") << "Add to explanation : " << eq << std::endl;
-          curr_exp.push_back(eq);
-        }
-        index_j++;
-        index_i++;
+        index++;
         success = true;
-      } else {
+      }else{
+        Assert( !areEqual(normal_forms[i][index], normal_forms[j][index]) );
         std::vector< Node > temp_exp;
-        Node length_term_i = getLength( normal_forms[i][index_i], temp_exp );
-        Node length_term_j = getLength( normal_forms[j][index_j], temp_exp );
+        Node length_term_i = getLength( normal_forms[i][index], temp_exp );
+        Node length_term_j = getLength( normal_forms[j][index], temp_exp );
         //check  length(normal_forms[i][index]) == length(normal_forms[j][index])
         if( areEqual( length_term_i, length_term_j ) ){
           Trace("strings-solve-debug") << "Simple Case 2 : string lengths are equal" << std::endl;
-          Node eq = normal_forms[i][index_i].eqNode( normal_forms[j][index_j] );
+          Node eq = normal_forms[i][index].eqNode( normal_forms[j][index] );
           //eq = Rewriter::rewrite( eq );
           Node length_eq = length_term_i.eqNode( length_term_j );
-          temp_exp.insert(temp_exp.end(), curr_exp.begin(), curr_exp.end() );
+          //temp_exp.insert(temp_exp.end(), curr_exp.begin(), curr_exp.end() );
+          getExplanationVectorForPrefix( normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend, i, j, index, isRev, temp_exp );
           temp_exp.push_back(length_eq);
           sendInference( temp_exp, eq, "LengthEq" );
           return true;
-        }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 ) ){
+        }else if( ( normal_forms[i][index].getKind()!=kind::CONST_STRING && index==normal_forms[i].size()-1 ) ||
+                  ( normal_forms[j][index].getKind()!=kind::CONST_STRING && index==normal_forms[j].size()-1 ) ){
           Trace("strings-solve-debug") << "Simple Case 3 : at endpoint" << std::endl;
           Node conc;
           std::vector< Node > antec;
-          antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
+          //antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
+          getExplanationVectorForPrefix( normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend, i, j, -1, isRev, antec );
           std::vector< Node > eqn;
           for( unsigned r=0; r<2; r++ ) {
-            int index_k = r==0 ? index_i : index_j;
+            int index_k = index;
             int k = r==0 ? i : j;
             std::vector< Node > eqnc;
             for( unsigned index_l=index_k; index_l<normal_forms[k].size(); index_l++ ) {
@@ -2158,12 +2210,12 @@ bool TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal
             sendInference( antec, conc, "ENDPOINT", true );
             return true;
           }else{
-            index_i = normal_forms[i].size();
-            index_j = normal_forms[j].size();
+            Assert( normal_forms[i].size()==normal_forms[j].size() );
+            index = normal_forms[i].size();
           }
-        } else if(normal_forms[i][index_i].isConst() && normal_forms[j][index_j].isConst()) {
-          Node const_str = normal_forms[i][index_i];
-          Node other_str = normal_forms[j][index_j];
+        } else if( normal_forms[i][index].isConst() && normal_forms[j][index].isConst() ){
+          Node const_str = normal_forms[i][index];
+          Node other_str = normal_forms[j][index];
           Trace("strings-solve-debug") << "Simple Case 3 : Const Split : " << const_str << " vs " << other_str << std::endl;
           unsigned len_short = const_str.getConst<String>().size() <= other_str.getConst<String>().size() ? const_str.getConst<String>().size() : other_str.getConst<String>().size();
           bool isSameFix = isRev ? const_str.getConst<String>().rstrncmp(other_str.getConst<String>(), len_short): const_str.getConst<String>().strncmp(other_str.getConst<String>(), len_short);
@@ -2171,27 +2223,25 @@ bool TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal
             //same prefix/suffix
             //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;
             if(isRev) {
-              int new_len = normal_forms[l][index_l].getConst<String>().size() - len_short;
-              Node remainderStr = NodeManager::currentNM()->mkConst( normal_forms[l][index_l].getConst<String>().substr(0, new_len) );
-              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 );
+              int new_len = normal_forms[l][index].getConst<String>().size() - len_short;
+              Node remainderStr = NodeManager::currentNM()->mkConst( normal_forms[l][index].getConst<String>().substr(0, new_len) );
+              Trace("strings-solve-debug-test") << "Break normal form of " << normal_forms[l][index] << " into " << normal_forms[k][index] << ", " << remainderStr << std::endl;
+              normal_forms[l].insert( normal_forms[l].begin()+index + 1, remainderStr );
             } else {
-              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 );
+              Node remainderStr = NodeManager::currentNM()->mkConst(normal_forms[l][index].getConst<String>().substr(len_short));
+              Trace("strings-solve-debug-test") << "Break normal form of " << normal_forms[l][index] << " into " << normal_forms[k][index] << ", " << remainderStr << std::endl;
+              normal_forms[l].insert( normal_forms[l].begin()+index + 1, remainderStr );
             }
-            normal_forms[l][index_l] = normal_forms[k][index_k];
-            index_i++;
-            index_j++;
+            normal_forms[l][index] = normal_forms[k][index];
+            index++;
             success = true;
           } else {
             std::vector< Node > antec;
             //curr_exp is conflict
-            antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
+            //antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
+            getExplanationVectorForPrefix( normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend, i, j, index, isRev, antec );
             sendInference( antec, d_false, "Const Conflict", true );
             return true;
           }
@@ -2202,18 +2252,15 @@ bool TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal
   return false;
 }
 
-bool TheoryStrings::detectLoop( std::vector< std::vector< Node > > &normal_forms, int i, int j,
-                                int index_i, int index_j, int &loop_in_i, int &loop_in_j) {
+bool TheoryStrings::detectLoop( std::vector< std::vector< Node > > &normal_forms, int i, int j, int index, int &loop_in_i, int &loop_in_j) {
   int has_loop[2] = { -1, -1 };
   if( options::stringLB() != 2 ) {
     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 ) {
+      if( normal_forms[other_n_index][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] ){
+          if( normal_forms[n_index][lp]==normal_forms[other_n_index][index] ){
             has_loop[r] = lp;
             break;
           }
@@ -2232,14 +2279,14 @@ bool TheoryStrings::detectLoop( std::vector< std::vector< Node > > &normal_forms
 
 //xs(zy)=t(yz)xr
 bool TheoryStrings::processLoop( std::vector< Node > &antec, std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src,
-                                 int i, int j, int loop_n_index, int other_n_index, int loop_index, int index, int other_index) {
+                                 int i, int j, int loop_n_index, int other_n_index, int loop_index, int index) {
   if( options::stringAbortLoop() ){
     Message() << "Looping word equation encountered." << std::endl;
     exit( 1 );
   }else{
     Node conc;
     Trace("strings-loop") << "Detected possible loop for " << normal_forms[loop_n_index][loop_index] << std::endl;
-    Trace("strings-loop") << " ... (X)= " << normal_forms[other_n_index][other_index] << std::endl;
+    Trace("strings-loop") << " ... (X)= " << normal_forms[other_n_index][index] << std::endl;
 
     Trace("strings-loop") << " ... T(Y.Z)= ";
     std::vector< Node > vec_t;
@@ -2252,8 +2299,8 @@ bool TheoryStrings::processLoop( std::vector< Node > &antec, std::vector< std::v
     Trace("strings-loop") << " (" << t_yz << ")" << std::endl;
     Trace("strings-loop") << " ... S(Z.Y)= ";
     std::vector< Node > vec_s;
-    for(int lp=other_index+1; lp<(int)normal_forms[other_n_index].size(); ++lp) {
-      if(lp != other_index+1) Trace("strings-loop") << " ++ ";
+    for(int lp=index+1; lp<(int)normal_forms[other_n_index].size(); ++lp) {
+      if(lp != index+1) Trace("strings-loop") << " ++ ";
       Trace("strings-loop") << normal_forms[other_n_index][lp];
       vec_s.push_back( normal_forms[other_n_index][lp] );
     }
@@ -2314,10 +2361,10 @@ bool TheoryStrings::processLoop( std::vector< Node > &antec, std::vector< std::v
           s_zy.getConst<String>().isRepeated()
           ) {
           Node rep_c = NodeManager::currentNM()->mkConst( s_zy.getConst<String>().substr(0, 1) );
-          Trace("strings-loop") << "Special case (X)=" << normal_forms[other_n_index][other_index] << " " << std::endl;
+          Trace("strings-loop") << "Special case (X)=" << normal_forms[other_n_index][index] << " " << std::endl;
           Trace("strings-loop") << "... (C)=" << rep_c << " " << std::endl;
           //special case
-          str_in_re = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, normal_forms[other_n_index][other_index],
+          str_in_re = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, normal_forms[other_n_index][index],
                   NodeManager::currentNM()->mkNode( kind::REGEXP_STAR,
                   NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, rep_c ) ) );
           conc = str_in_re;
@@ -2343,7 +2390,7 @@ bool TheoryStrings::processLoop( std::vector< Node > &antec, std::vector< std::v
             if(cc == d_false) {
               continue;
             }
-            Node conc2 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, normal_forms[other_n_index][other_index],
+            Node conc2 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, normal_forms[other_n_index][index],
                     NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT,
                       NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, y),
                       NodeManager::currentNM()->mkNode(kind::REGEXP_STAR,
@@ -2365,7 +2412,7 @@ bool TheoryStrings::processLoop( std::vector< Node > &antec, std::vector< std::v
           vec_r.insert(vec_r.begin(), sk_y);
           vec_r.insert(vec_r.begin(), sk_z);
           Node conc2 = s_zy.eqNode( mkConcat( vec_r ) );
-          Node conc3 = normal_forms[other_n_index][other_index].eqNode( mkConcat( sk_y, sk_w ) );
+          Node conc3 = normal_forms[other_n_index][index].eqNode( mkConcat( sk_y, sk_w ) );
           Node restr = r == d_emptyString ? s_zy : mkConcat( sk_z, sk_y );
           str_in_re = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, sk_w,
                   NodeManager::currentNM()->mkNode( kind::REGEXP_STAR,
@@ -2692,6 +2739,15 @@ void TheoryStrings::registerTerm( Node n, int effort ) {
 void TheoryStrings::sendInference( std::vector< Node >& exp, std::vector< Node >& exp_n, Node eq, const char * c, bool asLemma ) {
   eq = eq.isNull() ? d_false : Rewriter::rewrite( eq );
   if( eq!=d_true ){
+    if( Trace.isOn("strings-infer-debug") ){
+      Trace("strings-infer-debug") << "infer : " << eq << " from: " << std::endl;
+      for( unsigned i=0; i<exp.size(); i++ ){
+        Trace("strings-infer-debug")  << "  " << exp[i] << std::endl;
+      }
+      for( unsigned i=0; i<exp_n.size(); i++ ){
+        Trace("strings-infer-debug")  << "  N:" << exp_n[i] << std::endl;
+      }
+    }
     bool doSendLemma = ( asLemma || eq==d_false || eq.getKind()==kind::OR || options::stringInferAsLemmas() );
     if( doSendLemma ){  
       Node eq_exp;
@@ -2743,7 +2799,6 @@ void TheoryStrings::sendLemma( Node ant, Node conc, const char * c ) {
 }
 
 void TheoryStrings::sendInfer( Node eq_exp, Node eq, const char * c ) {
-  Trace("strings-infer-debug") << "infer : " << eq << " from " << eq_exp << std::endl;
   if( options::stringInferSym() ){
     std::vector< Node > vars;
     std::vector< Node > subs;
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 63098552d..5a67f3f63 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -158,6 +158,7 @@ private:
   std::map< Node, Node > d_normal_forms_base;
   std::map< Node, std::vector< Node > > d_normal_forms;
   std::map< Node, std::vector< Node > > d_normal_forms_exp;
+  std::map< Node, std::map< Node, std::map< bool, int > > > d_normal_forms_exp_depend;
   //map of pairs of terms that have the same normal form
   NodeListMap d_nf_pairs;
   void addNormalFormPair( Node n1, Node n2 );
@@ -236,7 +237,6 @@ private:
   NodeNodeMap d_proxy_var;
   NodeNodeMap d_proxy_var_to_length;
 private:
-
   //initial check
   void checkInit();
   void checkConstantEquivalenceClasses( TermIndex* ti, std::vector< Node >& vecc );
@@ -254,30 +254,31 @@ private:
   //normal forms check
   void checkNormalForms();
   bool normalizeEquivalenceClass( Node n, std::vector< Node > & nf, std::vector< Node > & nf_exp );
-  bool getNormalForms( Node &eqc, 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);
+  bool getNormalForms( Node &eqc, std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src,
+                       std::vector< std::vector< Node > > &normal_forms_exp, std::vector< std::map< Node, std::map< bool, int > > >& normal_forms_exp_depend);
   bool detectLoop(std::vector< std::vector< Node > > &normal_forms,
-        int i, int j, int index_i, int index_j,
-        int &loop_in_i, int &loop_in_j);
+        int i, int j, int index, int &loop_in_i, int &loop_in_j);
   bool processLoop(std::vector< Node > &antec,
         std::vector< std::vector< Node > > &normal_forms,
         std::vector< Node > &normal_form_src,
         int i, int j, int loop_n_index, int other_n_index,
-        int loop_index, int index, int other_index);
-  bool processNEqc(std::vector< std::vector< Node > > &normal_forms,
-        std::vector< std::vector< Node > > &normal_forms_exp,
-        std::vector< Node > &normal_form_src);
-  bool processReverseNEq(std::vector< std::vector< Node > > &normal_forms,
-        std::vector< Node > &normal_form_src, std::vector< Node > &curr_exp, unsigned i, unsigned j );
-  bool processSimpleNEq( std::vector< std::vector< Node > > &normal_forms,
-        std::vector< Node > &normal_form_src, std::vector< Node > &curr_exp, unsigned i, unsigned j,
-        unsigned& index_i, unsigned& index_j, bool isRev );
+        int loop_index, int index);
+  bool processNEqc( std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src,
+                    std::vector< std::vector< Node > > &normal_forms_exp, std::vector< std::map< Node, std::map< bool, int > > >& normal_forms_exp_depend );
+  bool processReverseNEq( std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src, 
+                          std::vector< std::vector< Node > > &normal_forms_exp, std::vector< std::map< Node, std::map< bool, int > > >& normal_forms_exp_depend, 
+                          unsigned i, unsigned j );
+  bool processSimpleNEq( std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src, 
+                         std::vector< std::vector< Node > > &normal_forms_exp, std::vector< std::map< Node, std::map< bool, int > > >& normal_forms_exp_depend, 
+                         unsigned i, unsigned j, unsigned& index, bool isRev );
   bool processDeq( Node n1, Node n2 );
   int processReverseDeq( std::vector< Node >& nfi, std::vector< Node >& nfj, Node ni, Node nj );
   int processSimpleDeq( std::vector< Node >& nfi, std::vector< Node >& nfj, Node ni, Node nj, unsigned& index, bool isRev );
   void checkDeqNF();
+  
+  void getExplanationVectorForPrefix( std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src,
+                                      std::vector< std::vector< Node > > &normal_forms_exp, std::vector< std::map< Node, std::map< bool, int > > >& normal_forms_exp_depend,
+                                      unsigned i, unsigned j, int index, bool isRev, std::vector< Node >& curr_exp );
 
   //check for extended functions
   void checkExtendedFuncs();
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 0eff9bd5d..2ce86852e 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -631,7 +631,9 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
       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());
+        //AJR: I believe this assertion is too strict, 
+        // e.g. datatypes may assert representative for two constructor terms that are not in the care graph and are merged during collectModelInfo.
+        //Assert(rep.isNull());
         rep = tm->d_reps[n];
         Assert(!rep.isNull() );
         Trace("model-builder") << "  Rep( " << eqc << " ) = " << rep << std::endl;
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index 02eaeeb47..eff6995e0 100644
--- a/test/regress/regress0/quantifiers/Makefile.am
+++ b/test/regress/regress0/quantifiers/Makefile.am
@@ -74,7 +74,8 @@ TESTS =	\
   macro-subtype-param.smt2 \
   macros-real-arg.smt2 \
   subtype-param-unk.smt2 \
-  subtype-param.smt2
+  subtype-param.smt2 \
+  anti-sk-simp.smt2
 
 
 # regression can be solved with --finite-model-find --fmf-inst-engine
diff --git a/test/regress/regress0/quantifiers/anti-sk-simp.smt2 b/test/regress/regress0/quantifiers/anti-sk-simp.smt2
new file mode 100755
index 000000000..ba4f9cbb9
--- /dev/null
+++ b/test/regress/regress0/quantifiers/anti-sk-simp.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --quant-anti-skolem
+; EXPECT: unsat
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+(declare-fun f (Int) Int)
+(declare-fun a () Int)
+(declare-fun b () Int)
+(assert (forall ((X Int)) (< X (f X))))
+(assert (forall ((X Int)) (> (+ a b) (f X))))
+(check-sat)