Refactor strings extended functions inferences (#2480)

This refactors the extended function inference step of TheoryStrings. It also generalizes a data member (d_pol) so that we track extended functions that are equal to constants for any type.

This is in preparation for working on solving equations and further inferences in this style.

2 files changed, 245 insertions, 114 deletions

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 4b73e496e..1acb5ec95 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -397,7 +397,12 @@ int TheoryStrings::getReduction( int effort, Node n, Node& nr ) {
   Assert( d_extf_info_tmp.find( n )!=d_extf_info_tmp.end() );
   if( d_extf_info_tmp[n].d_model_active ){
     int r_effort = -1;
-    int pol = d_extf_info_tmp[n].d_pol;
+    // polarity : 1 true, -1 false, 0 neither
+    int pol = 0;
+    if (n.getType().isBoolean() && !d_extf_info_tmp[n].d_const.isNull())
+    {
+      pol = d_extf_info_tmp[n].d_const.getConst<bool>() ? 1 : -1;
+    }
     if( n.getKind()==kind::STRING_STRCTN ){
       if( pol==1 ){
         r_effort = 1;
@@ -1505,22 +1510,23 @@ void TheoryStrings::checkExtfEval( int effort ) {
     Node n = terms[i];
     Node sn = sterms[i];
     //setup information about extf
-    d_extf_info_tmp[n].init();
-    std::map< Node, ExtfInfoTmp >::iterator itit = d_extf_info_tmp.find( n );
-    if( n.getType().isBoolean() ){
-      if( areEqual( n, d_true ) ){
-        itit->second.d_pol = 1;
-      }else if( areEqual( n, d_false ) ){
-        itit->second.d_pol = -1;
-      }
+    ExtfInfoTmp& einfo = d_extf_info_tmp[n];
+    Node r = getRepresentative(n);
+    std::map<Node, Node>::iterator itcit = d_eqc_to_const.find(r);
+    if (itcit != d_eqc_to_const.end())
+    {
+      einfo.d_const = itcit->second;
     }
-    Trace("strings-extf-debug") << "Check extf " << n << " == " << sn << ", pol = " << itit->second.d_pol << ", effort=" << effort << "..." << std::endl;
+    Trace("strings-extf-debug") << "Check extf " << n << " == " << sn
+                                << ", constant = " << einfo.d_const
+                                << ", effort=" << effort << "..." << std::endl;
     //do the inference
     Node to_reduce;
     if( n!=sn ){
-      itit->second.d_exp.insert( itit->second.d_exp.end(), exp[i].begin(), exp[i].end() );
+      einfo.d_exp.insert(einfo.d_exp.end(), exp[i].begin(), exp[i].end());
       // inference is rewriting the substituted node
       Node nrc = Rewriter::rewrite( sn );
+      Kind nrck = nrc.getKind();
       //if rewrites to a constant, then do the inference and mark as reduced
       if( nrc.isConst() ){
         if( effort<3 ){
@@ -1565,13 +1571,13 @@ void TheoryStrings::checkExtfEval( int effort ) {
               }else{
                 conc = nrs.eqNode( nrc );
               }
-              itit->second.d_exp.clear();
+              einfo.d_exp.clear();
             }
           }else{
             if( !areEqual( n, nrc ) ){
               if( n.getType().isBoolean() ){
                 if( areEqual( n, nrc==d_true ? d_false : d_true )  ){
-                  itit->second.d_exp.push_back( nrc==d_true ? n.negate() : n );
+                  einfo.d_exp.push_back(nrc == d_true ? n.negate() : n);
                   conc = d_false;
                 }else{
                   conc = nrc==d_true ? n : n.negate();
@@ -1583,7 +1589,8 @@ void TheoryStrings::checkExtfEval( int effort ) {
           }
           if( !conc.isNull() ){
             Trace("strings-extf") << "  resolve extf : " << sn << " -> " << nrc << std::endl;
-            sendInference( itit->second.d_exp, conc, effort==0 ? "EXTF" : "EXTF-N", true );
+            sendInference(
+                einfo.d_exp, conc, effort == 0 ? "EXTF" : "EXTF-N", true);
             if( d_conflict ){
               Trace("strings-extf-debug") << "  conflict, return." << std::endl;
               return;
@@ -1593,18 +1600,25 @@ void TheoryStrings::checkExtfEval( int effort ) {
           //check if it is already equal, if so, mark as reduced. Otherwise, do nothing.
           if( areEqual( n, nrc ) ){ 
             Trace("strings-extf") << "  resolved extf, since satisfied by model: " << n << std::endl;
-            itit->second.d_model_active = false;
+            einfo.d_model_active = false;
           }
         }
       //if it reduces to a conjunction, infer each and reduce
-      }else if( ( nrc.getKind()==kind::OR && itit->second.d_pol==-1 ) || ( nrc.getKind()==kind::AND && itit->second.d_pol==1 ) ){
+      }
+      else if ((nrck == OR && einfo.d_const == d_false)
+               || (nrck == AND && einfo.d_const == d_true))
+      {
         Assert( effort<3 );
         getExtTheory()->markReduced( n );
-        itit->second.d_exp.push_back( itit->second.d_pol==-1 ? n.negate() : n );
+        einfo.d_exp.push_back(einfo.d_const == d_false ? n.negate() : n);
         Trace("strings-extf-debug") << "  decomposable..." << std::endl;
-        Trace("strings-extf") << "  resolve extf : " << sn << " -> " << nrc << ", pol = " << itit->second.d_pol << std::endl;
-        for( unsigned i=0; i<nrc.getNumChildren(); i++ ){
-          sendInference( itit->second.d_exp, itit->second.d_pol==-1 ? nrc[i].negate() : nrc[i], effort==0 ? "EXTF_d" : "EXTF_d-N" );
+        Trace("strings-extf") << "  resolve extf : " << sn << " -> " << nrc
+                              << ", const = " << einfo.d_const << std::endl;
+        for (const Node& nrcc : nrc)
+        {
+          sendInference(einfo.d_exp,
+                        einfo.d_const == d_false ? nrcc.negate() : nrcc,
+                        effort == 0 ? "EXTF_d" : "EXTF_d-N");
         }
       }else{
         to_reduce = nrc;
@@ -1618,18 +1632,20 @@ void TheoryStrings::checkExtfEval( int effort ) {
       if( effort==1 ){
         Trace("strings-extf") << "  cannot rewrite extf : " << to_reduce << std::endl;
       }
-      checkExtfInference( n, to_reduce, itit->second, effort );
+      checkExtfInference(n, to_reduce, einfo, effort);
       if( Trace.isOn("strings-extf-list") ){
         Trace("strings-extf-list") << "  * " << to_reduce;
-        if( itit->second.d_pol!=0 ){
-          Trace("strings-extf-list") << ", pol = " << itit->second.d_pol;
+        if (!einfo.d_const.isNull())
+        {
+          Trace("strings-extf-list") << ", const = " << einfo.d_const;
         }
         if( n!=to_reduce ){
           Trace("strings-extf-list") << ", from " << n;
         }
         Trace("strings-extf-list") << std::endl;
-      }  
-      if( getExtTheory()->isActive( n ) && itit->second.d_model_active ){
+      }
+      if (getExtTheory()->isActive(n) && einfo.d_model_active)
+      {
         has_nreduce = true;
       }
     }
@@ -1638,81 +1654,144 @@ void TheoryStrings::checkExtfEval( int effort ) {
 }
 
 void TheoryStrings::checkExtfInference( Node n, Node nr, ExtfInfoTmp& in, int effort ){
-  //make additional inferences that do not contribute to the reduction of n, but may help show a refutation
-  if( in.d_pol!=0 ){
-    //add original to explanation
-    in.d_exp.push_back( in.d_pol==1 ? n : n.negate() );
-    
-    //d_extf_infer_cache stores whether we have made the inferences associated with a node n, 
-    // this may need to be generalized if multiple inferences apply
-        
-    if( nr.getKind()==kind::STRING_STRCTN ){
-      if( ( in.d_pol==1 && nr[1].getKind()==kind::STRING_CONCAT ) || ( in.d_pol==-1 && nr[0].getKind()==kind::STRING_CONCAT ) ){
-        if( d_extf_infer_cache.find( nr )==d_extf_infer_cache.end() ){
-          d_extf_infer_cache.insert( nr );
-
-          //one argument does (not) contain each of the components of the other argument
-          int index = in.d_pol==1 ? 1 : 0;
-          std::vector< Node > children;
-          children.push_back( nr[0] );
-          children.push_back( nr[1] );
-          //Node exp_n = mkAnd( exp );
-          for( unsigned i=0; i<nr[index].getNumChildren(); i++ ){
-            children[index] = nr[index][i];
-            Node conc = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, children );
-            conc = Rewriter::rewrite(in.d_pol == 1 ? conc : conc.negate());
-            // check if it already (does not) hold
-            if (hasTerm(conc))
+  if (in.d_const.isNull())
+  {
+    return;
+  }
+  NodeManager* nm = NodeManager::currentNM();
+
+  Node exp = n.eqNode(in.d_const);
+  exp = Rewriter::rewrite(exp);
+
+  // add original to explanation
+  in.d_exp.push_back(exp);
+
+  // d_extf_infer_cache stores whether we have made the inferences associated
+  // with a node n,
+  // this may need to be generalized if multiple inferences apply
+
+  if (nr.getKind() == STRING_STRCTN)
+  {
+    Assert(in.d_const.isConst());
+    bool pol = in.d_const.getConst<bool>();
+    if ((pol && nr[1].getKind() == STRING_CONCAT)
+        || (!pol && nr[0].getKind() == STRING_CONCAT))
+    {
+      // If str.contains( x, str.++( y1, ..., yn ) ),
+      //   we may infer str.contains( x, y1 ), ..., str.contains( x, yn )
+      // The following recognizes two situations related to the above reasoning:
+      // (1) If ~str.contains( x, yi ) holds for some i, we are in conflict,
+      // (2) If str.contains( x, yj ) already holds for some j, then the term
+      // str.contains( x, yj ) is irrelevant since it is satisfied by all models
+      // for str.contains( x, str.++( y1, ..., yn ) ).
+
+      // Notice that the dual of the above reasoning also holds, i.e.
+      // If ~str.contains( str.++( x1, ..., xn ), y ),
+      //   we may infer ~str.contains( x1, y ), ..., ~str.contains( xn, y )
+      // This is also handled here.
+      if (d_extf_infer_cache.find(nr) == d_extf_infer_cache.end())
+      {
+        d_extf_infer_cache.insert(nr);
+
+        int index = pol ? 1 : 0;
+        std::vector<Node> children;
+        children.push_back(nr[0]);
+        children.push_back(nr[1]);
+        for (const Node& nrc : nr[index])
+        {
+          children[index] = nrc;
+          Node conc = nm->mkNode(STRING_STRCTN, children);
+          conc = Rewriter::rewrite(pol ? conc : conc.negate());
+          // check if it already (does not) hold
+          if (hasTerm(conc))
+          {
+            if (areEqual(conc, d_false))
             {
-              if (areEqual(conc, d_false))
-              {
-                // should be a conflict
-                sendInference(in.d_exp, conc, "CTN_Decompose");
-              }
-              else if (getExtTheory()->hasFunctionKind(conc.getKind()))
-              {
-                // can mark as reduced, since model for n => model for conc
-                getExtTheory()->markReduced(conc);
-              }
+              // we are in conflict
+              sendInference(in.d_exp, conc, "CTN_Decompose");
+            }
+            else if (getExtTheory()->hasFunctionKind(conc.getKind()))
+            {
+              // can mark as reduced, since model for n implies model for conc
+              getExtTheory()->markReduced(conc);
             }
           }
-          
         }
-      }else{
-        //store this (reduced) assertion
-        //Assert( effort==0 || nr[0]==getRepresentative( nr[0] ) );
-        bool pol = in.d_pol==1;
-        if( std::find( d_extf_info_tmp[nr[0]].d_ctn[pol].begin(), d_extf_info_tmp[nr[0]].d_ctn[pol].end(), nr[1] )==d_extf_info_tmp[nr[0]].d_ctn[pol].end() ){
-          Trace("strings-extf-debug") << "  store contains info : " << nr[0] << " " << pol << " " << nr[1] << std::endl;
-          d_extf_info_tmp[nr[0]].d_ctn[pol].push_back( nr[1] );
-          d_extf_info_tmp[nr[0]].d_ctn_from[pol].push_back( n );
-          //transitive closure for contains
-          bool opol = !pol;
-          for( unsigned i=0; i<d_extf_info_tmp[nr[0]].d_ctn[opol].size(); i++ ){
-            Node onr = d_extf_info_tmp[nr[0]].d_ctn[opol][i];
-            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_c;
-              exp_c.insert( exp_c.end(), in.d_exp.begin(), in.d_exp.end() );
-              Node ofrom = d_extf_info_tmp[nr[0]].d_ctn_from[opol][i];
-              Assert( d_extf_info_tmp.find( ofrom )!=d_extf_info_tmp.end() );
-              exp_c.insert( exp_c.end(), d_extf_info_tmp[ofrom].d_exp.begin(), d_extf_info_tmp[ofrom].d_exp.end() );
-              sendInference( exp_c, conc, "CTN_Trans" );
-            }
+      }
+    }
+    else
+    {
+      if (std::find(d_extf_info_tmp[nr[0]].d_ctn[pol].begin(),
+                    d_extf_info_tmp[nr[0]].d_ctn[pol].end(),
+                    nr[1])
+          == d_extf_info_tmp[nr[0]].d_ctn[pol].end())
+      {
+        Trace("strings-extf-debug") << "  store contains info : " << nr[0]
+                                    << " " << pol << " " << nr[1] << std::endl;
+        // Store s (does not) contains t, since nr = (~)contains( s, t ) holds.
+        d_extf_info_tmp[nr[0]].d_ctn[pol].push_back(nr[1]);
+        d_extf_info_tmp[nr[0]].d_ctn_from[pol].push_back(n);
+        // Do transistive closure on contains, e.g.
+        // if contains( s, t ) and ~contains( s, r ), then ~contains( t, r ).
+
+        // The following infers new (negative) contains based on the above
+        // reasoning, provided that ~contains( t, r ) does not
+        // already hold in the current context. We test this by checking that
+        // contains( t, r ) is not already asserted false in the current
+        // context. We also handle the case where contains( t, r ) is equivalent
+        // to t = r, in which case we check that t != r does not already hold
+        // in the current context.
+
+        // Notice that form of the above inference is enough to find
+        // conflicts purely due to contains predicates. For example, if we
+        // have only positive occurrences of contains, then no conflicts due to
+        // contains predicates are possible and this schema does nothing. For
+        // example, note that contains( s, t ) and contains( t, r ) implies
+        // contains( s, r ), which we could but choose not to infer. Instead,
+        // we prefer being lazy: only if ~contains( s, r ) appears later do we
+        // infer ~contains( t, r ), which suffices to show a conflict.
+        bool opol = !pol;
+        for (unsigned i = 0, size = d_extf_info_tmp[nr[0]].d_ctn[opol].size();
+             i < size;
+             i++)
+        {
+          Node onr = d_extf_info_tmp[nr[0]].d_ctn[opol][i];
+          Node conc =
+              nm->mkNode(STRING_STRCTN, pol ? nr[1] : onr, pol ? onr : nr[1]);
+          conc = Rewriter::rewrite(conc);
+          bool do_infer = false;
+          if (conc.getKind() == 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_c;
+            exp_c.insert(exp_c.end(), in.d_exp.begin(), in.d_exp.end());
+            Node ofrom = d_extf_info_tmp[nr[0]].d_ctn_from[opol][i];
+            Assert(d_extf_info_tmp.find(ofrom) != d_extf_info_tmp.end());
+            exp_c.insert(exp_c.end(),
+                         d_extf_info_tmp[ofrom].d_exp.begin(),
+                         d_extf_info_tmp[ofrom].d_exp.end());
+            sendInference(exp_c, conc, "CTN_Trans");
           }
-        }else{
-          Trace("strings-extf-debug") << "  redundant." << std::endl;
-          getExtTheory()->markReduced( n );
         }
       }
+      else
+      {
+        // If we already know that s (does not) contain t, then n is redundant.
+        // For example, if str.contains( x, y ), str.contains( z, y ), and x=z
+        // are asserted in the current context, then str.contains( z, y ) is
+        // satisfied by all models of str.contains( x, y ) ^ x=z and thus can
+        // be ignored.
+        Trace("strings-extf-debug") << "  redundant." << std::endl;
+        getExtTheory()->markReduced(n);
+      }
     }
   }
 }
@@ -4503,8 +4582,9 @@ void TheoryStrings::checkMemberships() {
   for (unsigned i = 0; i < mems.size(); i++) {
     Node n = mems[i];
     Assert( d_extf_info_tmp.find( n )!=d_extf_info_tmp.end() );
-    if( d_extf_info_tmp[n].d_pol==1 || d_extf_info_tmp[n].d_pol==-1 ){
-      bool pol = d_extf_info_tmp[n].d_pol==1;
+    if (!d_extf_info_tmp[n].d_const.isNull())
+    {
+      bool pol = d_extf_info_tmp[n].d_const.getConst<bool>();
       Trace("strings-process-debug") << "  add membership : " << n << ", pol = " << pol << std::endl;
       addMembership( pol ? n : n.negate() );
     }else{
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 73906d029..2fd7b3525 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -289,6 +289,25 @@ private:
   NodeList d_ee_disequalities;
 private:
   NodeSet d_congruent;
+  /**
+   * The following three vectors are used for tracking constants that each
+   * equivalence class is entailed to be equal to.
+   * - The map d_eqc_to_const maps (representatives) r of equivalence classes to
+   * the constant that that equivalence class is entailed to be equal to,
+   * - The term d_eqc_to_const_base[r] is the term in the equivalence class r
+   * that is entailed to be equal to the constant d_eqc_to_const[r],
+   * - The term d_eqc_to_const_exp[r] is the explanation of why
+   * d_eqc_to_const_base[r] is equal to d_eqc_to_const[r].
+   *
+   * For example, consider the equivalence class { r, x++"a"++y, x++z }, and
+   * assume x = "" and y = "bb" in the current context. We have that
+   *   d_eqc_to_const[r] = "abb",
+   *   d_eqc_to_const_base[r] = x++"a"++y
+   *   d_eqc_to_const_exp[r] = ( x = "" AND y = "bb" )
+   *
+   * This information is computed during checkInit and is used during various
+   * inference schemas for deriving inferences.
+   */
   std::map< Node, Node > d_eqc_to_const;
   std::map< Node, Node > d_eqc_to_const_base;
   std::map< Node, Node > d_eqc_to_const_exp;
@@ -375,24 +394,6 @@ private:
     //all variables in this term
     std::vector< Node > d_vars;
   };
-  // non-static information about extf
-  class ExtfInfoTmp {
-  public:
-    void init(){
-      d_pol = 0;
-      d_model_active = true;
-    }
-    // list of terms that something (does not) contain and their explanation
-    std::map< bool, std::vector< Node > > d_ctn;
-    std::map< bool, std::vector< Node > > d_ctn_from;
-    //polarity
-    int d_pol;
-    //explanation
-    std::vector< Node > d_exp;
-    //false if it is reduced in the model
-    bool d_model_active;
-  };
-  std::map< Node, ExtfInfoTmp > d_extf_info_tmp;
 
  private:
   /** Length status, used for the registerLength function below */
@@ -441,9 +442,59 @@ private:
   SkolemCache d_sk_cache;
 
   void checkConstantEquivalenceClasses( TermIndex* ti, std::vector< Node >& vecc );
-  void checkExtfInference( Node n, Node nr, ExtfInfoTmp& in, int effort );
   Node getSymbolicDefinition( Node n, std::vector< Node >& exp );
 
+  //--------------------------for checkExtfEval
+  /**
+   * Non-static information about an extended function t. This information is
+   * constructed and used during the check extended function evaluation
+   * inference schema.
+   *
+   * In the following, we refer to the "context-dependent simplified form"
+   * of a term t to be the result of rewriting t * sigma, where sigma is a
+   * derivable substitution in the current context. For example, the
+   * context-depdendent simplified form of contains( x++y, "a" ) given
+   * sigma = { x -> "" } is contains(y,"a").
+   */
+  class ExtfInfoTmp
+  {
+   public:
+    ExtfInfoTmp() : d_model_active(true) {}
+    /**
+     * If s is in d_ctn[true] (resp. d_ctn[false]), then contains( t, s )
+     * (resp. ~contains( t, s )) holds in the current context. The vector
+     * d_ctn_from is the explanation for why this holds. For example,
+     * if d_ctn[false][i] is "A", then d_ctn_from[false][i] might be
+     * t = x ++ y AND x = "" AND y = "B".
+     */
+    std::map<bool, std::vector<Node> > d_ctn;
+    std::map<bool, std::vector<Node> > d_ctn_from;
+    /**
+     * The constant that t is entailed to be equal to, or null if none exist.
+     */
+    Node d_const;
+    /**
+     * The explanation for why t is equal to its context-dependent simplified
+     * form.
+     */
+    std::vector<Node> d_exp;
+    /** This flag is false if t is reduced in the model. */
+    bool d_model_active;
+  };
+  /** map extended functions to the above information */
+  std::map<Node, ExtfInfoTmp> d_extf_info_tmp;
+  /** check extended function inferences
+   *
+   * This function makes additional inferences for n that do not contribute
+   * to its reduction, but may help show a refutation.
+   *
+   * This function is called when the context-depdendent simplified form of
+   * n is nr. The argument "in" is the information object for n. The argument
+   * "effort" has the same meaning as the effort argument of checkExtfEval.
+   */
+  void checkExtfInference(Node n, Node nr, ExtfInfoTmp& in, int effort);
+  //--------------------------end for checkExtfEval
+
   //--------------------------for checkFlatForm
   /**
    * This checks whether there are flat form inferences between eqc[start] and