From 3a5a31758573032abedad3298699106eead63d87 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Sat, 24 Oct 2015 11:41:22 +0200
Subject: [PATCH] Fixes related to string contains.

---
 src/theory/strings/theory_strings.cpp         | 28 +++++++++++++------
 .../strings/theory_strings_rewriter.cpp       |  6 ++--
 2 files changed, 23 insertions(+), 11 deletions(-)

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index ea48d8805..630b2ae65 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -73,8 +73,8 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu
   d_congruent(c),
   d_proxy_var(u),
   d_proxy_var_to_length(u),
-  d_neg_ctn_eqlen(u),
-  d_neg_ctn_ulen(u),
+  d_neg_ctn_eqlen(c),
+  d_neg_ctn_ulen(c),
   d_neg_ctn_cached(u),
   d_ext_func_terms(c),
   d_regexp_memberships(c),
@@ -1219,13 +1219,23 @@ void TheoryStrings::checkExtfInference( Node n, Node nr, int effort ){
           bool opol = !pol;
           for( unsigned i=0; i<d_extf_info[nr[0]].d_ctn[opol].size(); i++ ){
             Node onr = d_extf_info[nr[0]].d_ctn[opol][i];
-            Node conc = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, pol ? nr[1] : onr, pol ? onr : nr[1] ).negate();
-            std::vector< Node > exp;
-            exp.insert( exp.end(), d_extf_exp[n].begin(), d_extf_exp[n].end() );
-            Node ofrom = d_extf_info[nr[0]].d_ctn_from[opol][i];
-            Assert( d_extf_exp.find( ofrom )!=d_extf_exp.end() );
-            exp.insert( exp.end(), d_extf_exp[ofrom].begin(), d_extf_exp[ofrom].end() );
-            sendInfer( mkAnd( exp ), conc, "CTN_Trans" );
+            Node conc = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, pol ? nr[1] : onr, pol ? onr : nr[1] );
+            conc = Rewriter::rewrite( conc );
+            bool do_infer = false;
+            if( conc.getKind()==kind::EQUAL ){
+              do_infer = !areDisequal( conc[0], conc[1] );
+            }else{
+              do_infer = !areEqual( conc, d_false );
+            }
+            if( do_infer ){
+              conc = conc.negate();
+              std::vector< Node > exp;
+              exp.insert( exp.end(), d_extf_exp[n].begin(), d_extf_exp[n].end() );
+              Node ofrom = d_extf_info[nr[0]].d_ctn_from[opol][i];
+              Assert( d_extf_exp.find( ofrom )!=d_extf_exp.end() );
+              exp.insert( exp.end(), d_extf_exp[ofrom].begin(), d_extf_exp[ofrom].end() );
+              sendInfer( mkAnd( exp ), conc, "CTN_Trans" );
+            }
           }
         }else{
           Trace("strings-extf-debug") << "  redundant." << std::endl;
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 6d84ace90..e0e295d40 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -1499,10 +1499,12 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) {
       }
     }
   }else if( node[0].isConst() ){
-    if( node[1].getKind()==kind::STRING_CONCAT ){
+    CVC4::String t = node[0].getConst<String>();
+    if( t.size()==0 ){
+      return NodeManager::currentNM()->mkNode( kind::EQUAL, node[0], node[1] );
+    }else if( node[1].getKind()==kind::STRING_CONCAT ){
       //must find constant components in order
       size_t pos = 0;
-      CVC4::String t = node[0].getConst<String>();
       for(unsigned i=0; i<node[1].getNumChildren(); i++) {
         if( node[1][i].isConst() ){
           CVC4::String s = node[1][i].getConst<String>();
-- 
2.30.2