Deterministic variables for RE elim (#7489)

Fixes #6766.

4 files changed, 45 insertions, 4 deletions

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index c4935340f..19eab3617 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -302,7 +302,11 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const
   // formulas at preprocess time.
   //
   // We don't want to set this option when we are in logics that contain ALL.
-  if (!logic.hasEverything() && logic.isTheoryEnabled(THEORY_STRINGS))
+  //
+  // We also must enable stringExp if reElimAgg is true, since this introduces
+  // bounded quantifiers during preprocessing.
+  if ((!logic.hasEverything() && logic.isTheoryEnabled(THEORY_STRINGS))
+      || opts.strings.regExpElimAgg)
   {
     // If the user explicitly set a logic that includes strings, but is not
     // the generic "ALL" logic, then enable stringsExp.
diff --git a/src/theory/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp
index dfe006a86..b3dc309d5 100644
--- a/src/theory/strings/regexp_elim.cpp
+++ b/src/theory/strings/regexp_elim.cpp
@@ -15,6 +15,7 @@
 
 #include "theory/strings/regexp_elim.h"
 
+#include "expr/bound_var_manager.h"
 #include "options/strings_options.h"
 #include "proof/proof_node_manager.h"
 #include "theory/rewriter.h"
@@ -29,6 +30,22 @@ namespace cvc5 {
 namespace theory {
 namespace strings {
 
+/**
+ * Attributes used for constructing unique bound variables. The following
+ * attributes are used to construct (deterministic) bound variables for
+ * eliminations within eliminateConcat and eliminateStar respectively.
+ */
+struct ReElimConcatIndexAttributeId
+{
+};
+typedef expr::Attribute<ReElimConcatIndexAttributeId, Node>
+    ReElimConcatIndexAttribute;
+struct ReElimStarIndexAttributeId
+{
+};
+typedef expr::Attribute<ReElimStarIndexAttributeId, Node>
+    ReElimStarIndexAttribute;
+
 RegExpElimination::RegExpElimination(bool isAgg,
                                      ProofNodeManager* pnm,
                                      context::Context* c)
@@ -77,6 +94,7 @@ TrustNode RegExpElimination::eliminateTrusted(Node atom)
 Node RegExpElimination::eliminateConcat(Node atom, bool isAgg)
 {
   NodeManager* nm = NodeManager::currentNM();
+  BoundVarManager* bvm = nm->getBoundVarManager();
   Node x = atom[0];
   Node lenx = nm->mkNode(STRING_LENGTH, x);
   Node re = atom[1];
@@ -260,7 +278,11 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg)
           }
           // if the gap after this one is strict, we need a non-greedy find
           // thus, we add a symbolic constant
-          Node k = nm->mkBoundVar(nm->integerType());
+          Node cacheVal =
+              BoundVarManager::getCacheValue(atom, nm->mkConst(Rational(i)));
+          TypeNode intType = nm->integerType();
+          Node k =
+              bvm->mkBoundVar<ReElimConcatIndexAttribute>(cacheVal, intType);
           non_greedy_find_vars.push_back(k);
           prev_end = nm->mkNode(PLUS, prev_end, k);
         }
@@ -452,7 +474,10 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg)
       }
       else
       {
-        k = nm->mkBoundVar(nm->integerType());
+        Node cacheVal =
+            BoundVarManager::getCacheValue(atom, nm->mkConst(Rational(i)));
+        TypeNode intType = nm->integerType();
+        k = bvm->mkBoundVar<ReElimConcatIndexAttribute>(cacheVal, intType);
         Node bound =
             nm->mkNode(AND,
                        nm->mkNode(LEQ, zero, k),
@@ -509,6 +534,7 @@ Node RegExpElimination::eliminateStar(Node atom, bool isAgg)
   // only aggressive rewrites below here
 
   NodeManager* nm = NodeManager::currentNM();
+  BoundVarManager* bvm = nm->getBoundVarManager();
   Node x = atom[0];
   Node lenx = nm->mkNode(STRING_LENGTH, x);
   Node re = atom[1];
@@ -530,7 +556,8 @@ Node RegExpElimination::eliminateStar(Node atom, bool isAgg)
   }
   bool lenOnePeriod = true;
   std::vector<Node> char_constraints;
-  Node index = nm->mkBoundVar(nm->integerType());
+  TypeNode intType = nm->integerType();
+  Node index = bvm->mkBoundVar<ReElimStarIndexAttribute>(atom, intType);
   Node substr_ch =
       nm->mkNode(STRING_SUBSTR, x, index, nm->mkConst(Rational(1)));
   substr_ch = Rewriter::rewrite(substr_ch);
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 24bb43244..cb535a469 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2271,6 +2271,7 @@ set(regress_1_tests
   regress1/strings/issue6653-4-rre.smt2
   regress1/strings/issue6653-rre.smt2
   regress1/strings/issue6653-rre-small.smt2
+  regress1/strings/issue6766-re-elim-bv.smt2
   regress1/strings/issue6777-seq-nth-eval-cm.smt2
   regress1/strings/issue6913.smt2
   regress1/strings/issue6973-dup-lemma-conc.smt2
diff --git a/test/regress/regress1/strings/issue6766-re-elim-bv.smt2 b/test/regress/regress1/strings/issue6766-re-elim-bv.smt2
new file mode 100644
index 000000000..13677838b
--- /dev/null
+++ b/test/regress/regress1/strings/issue6766-re-elim-bv.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --strings-exp --re-elim --re-elim-agg
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun a () String)
+(declare-fun b () String)
+(assert
+ (str.in_re (str.++ a (ite (str.in_re (str.++ a "BA" b) (re.++ (re.* (str.to_re "A")) (str.to_re "B"))) b a))
+  (re.diff (re.* (str.to_re "A")) (str.to_re ""))))
+(check-sat)