Variable elimination rewrite for quantified strings (#3071)

4 files changed, 115 insertions, 13 deletions

diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 015bf9c5a..ec52bf990 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -23,6 +23,7 @@
 #include "theory/quantifiers/skolemize.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/strings/theory_strings_rewriter.h"
 
 using namespace std;
 using namespace CVC4::kind;
@@ -64,7 +65,11 @@ void QuantifiersRewriter::addNodeToOrBuilder( Node n, NodeBuilder<>& t ){
   }
 }
 
-void QuantifiersRewriter::computeArgs( std::vector< Node >& args, std::map< Node, bool >& activeMap, Node n, std::map< Node, bool >& visited ){
+void QuantifiersRewriter::computeArgs(const std::vector<Node>& args,
+                                      std::map<Node, bool>& activeMap,
+                                      Node n,
+                                      std::map<Node, bool>& visited)
+{
   if( visited.find( n )==visited.end() ){
     visited[n] = true;
     if( n.getKind()==BOUND_VARIABLE ){
@@ -83,7 +88,10 @@ void QuantifiersRewriter::computeArgs( std::vector< Node >& args, std::map< Node
   }
 }
 
-void QuantifiersRewriter::computeArgVec( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n ) {
+void QuantifiersRewriter::computeArgVec(const std::vector<Node>& args,
+                                        std::vector<Node>& activeArgs,
+                                        Node n)
+{
   Assert( activeArgs.empty() );
   std::map< Node, bool > activeMap;
   std::map< Node, bool > visited;
@@ -97,7 +105,11 @@ void QuantifiersRewriter::computeArgVec( std::vector< Node >& args, std::vector<
   }
 }
 
-void QuantifiersRewriter::computeArgVec2( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n, Node ipl ) {
+void QuantifiersRewriter::computeArgVec2(const std::vector<Node>& args,
+                                         std::vector<Node>& activeArgs,
+                                         Node n,
+                                         Node ipl)
+{
   Assert( activeArgs.empty() );
   std::map< Node, bool > activeMap;
   std::map< Node, bool > visited;
@@ -880,7 +892,7 @@ bool QuantifiersRewriter::isVarElim(Node v, Node s)
 }
 
 Node QuantifiersRewriter::getVarElimLitBv(Node lit,
-                                          std::vector<Node>& args,
+                                          const std::vector<Node>& args,
                                           Node& var)
 {
   if (Trace.isOn("quant-velim-bv"))
@@ -930,6 +942,54 @@ Node QuantifiersRewriter::getVarElimLitBv(Node lit,
   return Node::null();
 }
 
+Node QuantifiersRewriter::getVarElimLitString(Node lit,
+                                              const std::vector<Node>& args,
+                                              Node& var)
+{
+  Assert(lit.getKind() == EQUAL);
+  NodeManager* nm = NodeManager::currentNM();
+  for (unsigned i = 0; i < 2; i++)
+  {
+    if (lit[i].getKind() == STRING_CONCAT)
+    {
+      for (unsigned j = 0, nchildren = lit[i].getNumChildren(); j < nchildren;
+           j++)
+      {
+        if (std::find(args.begin(), args.end(), lit[i][j]) != args.end())
+        {
+          var = lit[i][j];
+          Node slv = lit[1 - i];
+          std::vector<Node> preL(lit[i].begin(), lit[i].begin() + j);
+          std::vector<Node> postL(lit[i].begin() + j + 1, lit[i].end());
+          Node tpre =
+              strings::TheoryStringsRewriter::mkConcat(STRING_CONCAT, preL);
+          Node tpost =
+              strings::TheoryStringsRewriter::mkConcat(STRING_CONCAT, postL);
+          Node slvL = nm->mkNode(STRING_LENGTH, slv);
+          Node tpreL = nm->mkNode(STRING_LENGTH, tpre);
+          Node tpostL = nm->mkNode(STRING_LENGTH, tpost);
+          slv = nm->mkNode(
+              STRING_SUBSTR,
+              slv,
+              tpreL,
+              nm->mkNode(MINUS, slvL, nm->mkNode(PLUS, tpreL, tpostL)));
+          // forall x. r ++ x ++ t = s => P( x )
+          //   is equivalent to
+          // r ++ s' ++ t = s => P( s' ) where
+          // s' = substr( s, |r|, |s|-(|t|+|r|) ).
+          // We apply this only if r,t,s do not contain free variables.
+          if (!expr::hasFreeVar(slv))
+          {
+            return slv;
+          }
+        }
+      }
+    }
+  }
+
+  return Node::null();
+}
+
 bool QuantifiersRewriter::getVarElimLit(Node lit,
                                         bool pol,
                                         std::vector<Node>& args,
@@ -1058,10 +1118,19 @@ bool QuantifiersRewriter::getVarElimLit(Node lit,
       }
     }
   }
-  if (lit.getKind() == EQUAL && lit[0].getType().isBitVector() && pol)
+  if (lit.getKind() == EQUAL && pol)
   {
     Node var;
-    Node slv = getVarElimLitBv(lit, args, var);
+    Node slv;
+    TypeNode tt = lit[0].getType();
+    if (tt.isBitVector())
+    {
+      slv = getVarElimLitBv(lit, args, var);
+    }
+    else if (tt.isString())
+    {
+      slv = getVarElimLitString(lit, args, var);
+    }
     if (!slv.isNull())
     {
       Assert(!var.isNull());
@@ -1069,7 +1138,7 @@ bool QuantifiersRewriter::getVarElimLit(Node lit,
           std::find(args.begin(), args.end(), var);
       Assert(ita != args.end());
       Trace("var-elim-quant")
-          << "Variable eliminate based on bit-vector inversion : " << var
+          << "Variable eliminate based on theory-specific solving : " << var
           << " -> " << slv << std::endl;
       Assert(!expr::hasSubterm(slv, var));
       Assert(slv.getType().isSubtypeOf(var.getType()));
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index 09f26b65b..f91630097 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -36,9 +36,17 @@ public:
 private:
   static bool addCheckElimChild( std::vector< Node >& children, Node c, Kind k, std::map< Node, bool >& lit_pol, bool& childrenChanged );
   static void addNodeToOrBuilder( Node n, NodeBuilder<>& t );
-  static void computeArgs( std::vector< Node >& args, std::map< Node, bool >& activeMap, Node n, std::map< Node, bool >& visited );
-  static void computeArgVec( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n );
-  static void computeArgVec2( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n, Node ipl );
+  static void computeArgs(const std::vector<Node>& args,
+                          std::map<Node, bool>& activeMap,
+                          Node n,
+                          std::map<Node, bool>& visited);
+  static void computeArgVec(const std::vector<Node>& args,
+                            std::vector<Node>& activeArgs,
+                            Node n);
+  static void computeArgVec2(const std::vector<Node>& args,
+                             std::vector<Node>& activeArgs,
+                             Node n,
+                             Node ipl);
   static Node computeProcessTerms2( Node body, bool hasPol, bool pol, std::map< Node, bool >& currCond, int nCurrCond,
                                     std::map< Node, Node >& cache, std::map< Node, Node >& icache,
                                     std::vector< Node >& new_vars, std::vector< Node >& new_conds, bool elimExtArith );
@@ -62,12 +70,22 @@ private:
                             std::vector<Node>& args,
                             std::vector<Node>& vars,
                             std::vector<Node>& subs);
-  /** variable eliminate for bit-vector literals
+  /** variable eliminate for bit-vector equalities
    *
    * If this returns a non-null value ret, then var is updated to a member of
-   * args, lit is equivalent to ( var = ret ), and var is removed from args.
+   * args, lit is equivalent to ( var = ret ).
    */
-  static Node getVarElimLitBv(Node lit, std::vector<Node>& args, Node& var);
+  static Node getVarElimLitBv(Node lit,
+                              const std::vector<Node>& args,
+                              Node& var);
+  /** variable eliminate for string equalities
+   *
+   * If this returns a non-null value ret, then var is updated to a member of
+   * args, lit is equivalent to ( var = ret ).
+   */
+  static Node getVarElimLitString(Node lit,
+                                  const std::vector<Node>& args,
+                                  Node& var);
   /** get variable elimination
    *
    * If n asserted with polarity pol entails a literal lit that corresponds
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 3c5d82fa8..f7760a504 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1352,6 +1352,7 @@ set(regress_1_tests
   regress1/quantifiers/intersection-example-onelane.proof-node22337.smt2
   regress1/quantifiers/is-even.smt2
   regress1/quantifiers/isaplanner-goal20.smt2
+  regress1/quantifiers/issue2970-string-var-elim.smt2
   regress1/quantifiers/javafe.ast.StmtVec.009.smt2
   regress1/quantifiers/lra-vts-inf.smt2
   regress1/quantifiers/mix-coeff.smt2
diff --git a/test/regress/regress1/quantifiers/issue2970-string-var-elim.smt2 b/test/regress/regress1/quantifiers/issue2970-string-var-elim.smt2
new file mode 100644
index 000000000..31a57fc8b
--- /dev/null
+++ b/test/regress/regress1/quantifiers/issue2970-string-var-elim.smt2
@@ -0,0 +1,14 @@
+(set-logic ALL)
+(set-info :status unsat)
+(declare-fun s () String)
+(declare-fun t () String)
+(assert (! 
+ (forall ((t1 String) (t2 String))
+  (=> (= (str.++ t1 t2) t) (= (= t1 s) false))
+  )
+  :named a1))
+(assert (! 
+ (not (= (str.prefixof s t) false)) :named a0))
+
+
+(check-sat)