Fix proof equality engine for "no-explain" premises (#7079)

There was an inconsistency between when the equality engine would explain a literal and when we would provide a proof for it. This led to rare cases where we over zealously provided a proof for a fact that should have been an assumption in the theory lemma proof.

This corrects the issue by ensuring that no-explain premises are explicitly marked via a new helper proof generator "AssumptionProofGenerator" which always supplies (ASSUME f) as the proof for f.

This corrects some proof checking errors on string benchmarks.

8 files changed, 106 insertions, 2 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 306420a2c..4bce6f0d2 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -159,6 +159,8 @@ libcvc5_add_sources(
   printer/smt2/smt2_printer.h
   printer/tptp/tptp_printer.cpp
   printer/tptp/tptp_printer.h
+  proof/assumption_proof_generator.cpp
+  proof/assumption_proof_generator.h
   proof/buffered_proof_generator.cpp
   proof/buffered_proof_generator.h
   proof/conv_proof_generator.cpp
diff --git a/src/proof/assumption_proof_generator.cpp b/src/proof/assumption_proof_generator.cpp
new file mode 100644
index 000000000..84adb676e
--- /dev/null
+++ b/src/proof/assumption_proof_generator.cpp
@@ -0,0 +1,36 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * The assumption proof generator class.
+ */
+
+#include "proof/assumption_proof_generator.h"
+
+#include "proof/proof_node_manager.h"
+
+namespace cvc5 {
+
+AssumptionProofGenerator::AssumptionProofGenerator(ProofNodeManager* pnm)
+    : d_pnm(pnm)
+{
+}
+
+std::shared_ptr<ProofNode> AssumptionProofGenerator::getProofFor(Node f)
+{
+  return d_pnm->mkAssume(f);
+}
+std::string AssumptionProofGenerator::identify() const
+{
+  return "AssumptionProofGenerator";
+}
+
+}  // namespace cvc5
diff --git a/src/proof/assumption_proof_generator.h b/src/proof/assumption_proof_generator.h
new file mode 100644
index 000000000..218e5ffc0
--- /dev/null
+++ b/src/proof/assumption_proof_generator.h
@@ -0,0 +1,46 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * The assumption proof generator class.
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__PROOF__ASSUMPTION_PROOF_GENERATOR_H
+#define CVC5__PROOF__ASSUMPTION_PROOF_GENERATOR_H
+
+#include "proof/proof_generator.h"
+
+namespace cvc5 {
+
+class ProofNodeManager;
+
+/**
+ * A proof generator which always returns (ASSUME f) for getProofFor(f).
+ */
+class AssumptionProofGenerator : public ProofGenerator
+{
+ public:
+  AssumptionProofGenerator(ProofNodeManager* pnm);
+  /** Get the proof for formula f */
+  std::shared_ptr<ProofNode> getProofFor(Node f) override;
+  /** Identify this generator (for debugging, etc..) */
+  std::string identify() const override;
+
+ private:
+  /** The proof manager, used for allocating new ProofNode objects */
+  ProofNodeManager* d_pnm;
+};
+
+}  // namespace cvc5
+
+#endif /* CVC5__PROOF__ASSUMPTION_PROOF_GENERATOR_H */
diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp
index b4522d9df..ca8b3f740 100644
--- a/src/theory/uf/proof_equality_engine.cpp
+++ b/src/theory/uf/proof_equality_engine.cpp
@@ -36,6 +36,7 @@ ProofEqEngine::ProofEqEngine(context::Context* c,
     : EagerProofGenerator(pnm, u, "pfee::" + ee.identify()),
       d_ee(ee),
       d_factPg(c, pnm),
+      d_assumpPg(pnm),
       d_pnm(pnm),
       d_proof(pnm, nullptr, c, "pfee::LazyCDProof::" + ee.identify()),
       d_keep(c)
@@ -225,7 +226,7 @@ TrustNode ProofEqEngine::assertLemma(Node conc,
   LazyCDProof* curr;
   TrustNodeKind tnk;
   // same policy as above: for conflicts, use existing lazy proof
-  if (conc == d_false)
+  if (conc == d_false && noExplain.empty())
   {
     curr = &d_proof;
     tnk = TrustNodeKind::CONFLICT;
@@ -264,7 +265,7 @@ TrustNode ProofEqEngine::assertLemma(Node conc,
   LazyCDProof* curr;
   TrustNodeKind tnk;
   // same policy as above: for conflicts, use existing lazy proof
-  if (conc == d_false)
+  if (conc == d_false && noExplain.empty())
   {
     curr = &d_proof;
     tnk = TrustNodeKind::CONFLICT;
@@ -314,6 +315,8 @@ void ProofEqEngine::explainVecWithProof(TrustNodeKind& tnk,
       assumps.push_back(e);
       // it is not a conflict, since it may involve new literals
       tnk = TrustNodeKind::LEMMA;
+      // ensure this is an assumption
+      curr->addLazyStep(e, &d_assumpPg);
     }
   }
 }
diff --git a/src/theory/uf/proof_equality_engine.h b/src/theory/uf/proof_equality_engine.h
index 0c093d4b2..baf155dac 100644
--- a/src/theory/uf/proof_equality_engine.h
+++ b/src/theory/uf/proof_equality_engine.h
@@ -23,6 +23,7 @@
 #include "context/cdhashmap.h"
 #include "context/cdhashset.h"
 #include "expr/node.h"
+#include "proof/assumption_proof_generator.h"
 #include "proof/buffered_proof_generator.h"
 #include "proof/eager_proof_generator.h"
 #include "proof/lazy_proof.h"
@@ -278,6 +279,8 @@ class ProofEqEngine : public EagerProofGenerator
   eq::EqualityEngine& d_ee;
   /** The default proof generator (for simple facts) */
   BufferedProofGenerator d_factPg;
+  /** The no-explain proof generator */
+  AssumptionProofGenerator d_assumpPg;
   /** common nodes */
   Node d_true;
   Node d_false;
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index dca8860fd..0d8ec19dc 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2131,6 +2131,8 @@ set(regress_1_tests
   regress1/strings/idof-neg-index.smt2
   regress1/strings/idof-triv.smt2
   regress1/strings/ilc-l-nt.smt2
+  regress1/strings/instance3303-delta.smt2
+  regress1/strings/instance7075-delta.smt2
   regress1/strings/issue1105.smt2
   regress1/strings/issue1684-regex.smt2
   regress1/strings/issue2060.smt2
diff --git a/test/regress/regress1/strings/instance3303-delta.smt2 b/test/regress/regress1/strings/instance3303-delta.smt2
new file mode 100644
index 000000000..b42974774
--- /dev/null
+++ b/test/regress/regress1/strings/instance3303-delta.smt2
@@ -0,0 +1,6 @@
+(set-logic QF_S)
+(set-info :status unsat)
+(declare-const X String)
+(assert (str.in_re X (re.++ (re.range "1" "9") ((_ re.loop 0 2) (re.range "0" "9")) (str.to_re "}"))))
+(assert (not (str.in_re X (re.++ (re.union (re.range "0" "9") (re.++ (re.range "1" "9") (re.range "0" "9")) (re.++ (re.range "1" "9") (re.range "0" "9") (re.range "0" "9"))) (str.to_re "}")))))
+(check-sat)
diff --git a/test/regress/regress1/strings/instance7075-delta.smt2 b/test/regress/regress1/strings/instance7075-delta.smt2
new file mode 100644
index 000000000..54cd2cd9c
--- /dev/null
+++ b/test/regress/regress1/strings/instance7075-delta.smt2
@@ -0,0 +1,6 @@
+(set-logic QF_S)
+(set-info :status sat)
+(declare-const X String)
+(assert (not (str.in_re X (re.++ (re.range "0" "9") ((_ re.loop 1 2) (re.range "0" "9"))))))
+(assert (str.in_re X (re.union (re.++ (re.range "0" "9") ((_ re.loop 1 6) (re.range "0" "9"))) (str.to_re ""))))
+(check-sat)