Fix potential for cycles in trust substitutions (#7687)

This ensures we use only the prefix of substitutions for the *first* time a formula is proven in a substitution map.

This avoids the possibility for cycles in proof generators during non-clausal simplification, where we may reprove a formula F later at a point where later substitutions depend on F.

4 files changed, 26 insertions, 3 deletions

diff --git a/src/theory/trust_substitutions.cpp b/src/theory/trust_substitutions.cpp
index 7934231b9..c73265095 100644
--- a/src/theory/trust_substitutions.cpp
+++ b/src/theory/trust_substitutions.cpp
@@ -162,8 +162,12 @@ TrustNode TrustSubstitutionMap::applyTrusted(Node n, bool doRewrite)
     return TrustNode::mkTrustRewrite(n, ns, nullptr);
   }
   Node eq = n.eqNode(ns);
-  // remember the index
-  d_eqtIndex[eq] = d_tsubs.size();
+  // If we haven't already stored an index, remember the index. Otherwise, a
+  // (possibly shorter) prefix of the substitution already suffices to show eq
+  if (d_eqtIndex.find(eq) == d_eqtIndex.end())
+  {
+    d_eqtIndex[eq] = d_tsubs.size();
+  }
   // this class will provide a proof if asked
   return TrustNode::mkTrustRewrite(n, ns, this);
 }
@@ -194,11 +198,16 @@ std::shared_ptr<ProofNode> TrustSubstitutionMap::getProofFor(Node eq)
   {
     return d_subsPg->getProofFor(eq);
   }
+  Trace("trust-subs-pf") << "getProofFor " << eq << std::endl;
+  AlwaysAssert(d_proving.find(eq) == d_proving.end())
+      << "Repeat getProofFor in TrustSubstitutionMap " << eq;
+  d_proving.insert(eq);
   NodeUIntMap::iterator it = d_eqtIndex.find(eq);
   Assert(it != d_eqtIndex.end());
   Trace("trust-subs-pf") << "TrustSubstitutionMap::getProofFor, # assumptions= "
                          << it->second << std::endl;
   Node cs = getSubstitution(it->second);
+  Trace("trust-subs-pf") << "getProofFor substitution is " << cs << std::endl;
   Assert(eq != cs);
   std::vector<Node> pfChildren;
   if (!cs.isConst())
@@ -252,7 +261,9 @@ std::shared_ptr<ProofNode> TrustSubstitutionMap::getProofFor(Node eq)
   d_applyPg->addSteps(*d_tspb.get());
   d_tspb->clear();
   Trace("trust-subs-pf") << "...finish, make proof" << std::endl;
-  return d_applyPg->getProofFor(eq);
+  std::shared_ptr<ProofNode> ret = d_applyPg->getProofFor(eq);
+  d_proving.erase(eq);
+  return ret;
 }
 
 std::string TrustSubstitutionMap::identify() const { return d_name; }
diff --git a/src/theory/trust_substitutions.h b/src/theory/trust_substitutions.h
index 2a6997d1d..cc08c870d 100644
--- a/src/theory/trust_substitutions.h
+++ b/src/theory/trust_substitutions.h
@@ -143,6 +143,8 @@ class TrustSubstitutionMap : public ProofGenerator
    * two substitutions but not the third when asked to prove this equality.
    */
   NodeUIntMap d_eqtIndex;
+  /** Debugging, catches potential for infinite loops */
+  std::unordered_set<Node> d_proving;
 };
 
 }  // namespace theory
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index e11149df0..2ed3ddb8b 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1847,6 +1847,7 @@ set(regress_1_tests
   regress1/proofs/qgu-fuzz-arrays-1-dd-te-auto.smt2
   regress1/proofs/quant-alpha-eq.smt2
   regress1/proofs/sat-trivial-cycle.smt2
+  regress1/proofs/str-ovf-dd.smt2
   regress1/proofs/unsat-cores-proofs.smt2
   regress1/push-pop/arith_lra_01.smt2
   regress1/push-pop/arith_lra_02.smt2
diff --git a/test/regress/regress1/proofs/str-ovf-dd.smt2 b/test/regress/regress1/proofs/str-ovf-dd.smt2
new file mode 100644
index 000000000..85a879052
--- /dev/null
+++ b/test/regress/regress1/proofs/str-ovf-dd.smt2
@@ -0,0 +1,9 @@
+(set-logic ALL)
+(set-info :status unsat)
+(declare-const x Bool)
+(declare-const a String)
+(declare-const a4 String)
+(assert (= a4 "-"))
+(assert (str.in_re (str.++ a4 a a4) re.allchar))
+(assert (= x (str.in_re a re.allchar)))
+(check-sat)