(proof-new) Fix missing connection in trust substitution proofs (#6685)

This PR fixes a missing connection in trust substitution proofs, which was the cause of open proofs when solved equalities from ppAssert were not justified by proofs.

Also distinguishes TRUST_SUBS_EQ from TRUST_SUBS_MAP for clarity.

11 files changed, 31 insertions, 14 deletions

diff --git a/src/proof/proof_rule.cpp b/src/proof/proof_rule.cpp
index 0cefe1209..676fa6a63 100644
--- a/src/proof/proof_rule.cpp
+++ b/src/proof/proof_rule.cpp
@@ -46,6 +46,7 @@ const char* toString(PfRule id)
     case PfRule::TRUST_REWRITE: return "TRUST_REWRITE";
     case PfRule::TRUST_SUBS: return "TRUST_SUBS";
     case PfRule::TRUST_SUBS_MAP: return "TRUST_SUBS_MAP";
+    case PfRule::TRUST_SUBS_EQ: return "TRUST_SUBS_EQ";
     //================================================= Boolean rules
     case PfRule::RESOLUTION: return "RESOLUTION";
     case PfRule::CHAIN_RESOLUTION: return "CHAIN_RESOLUTION";
diff --git a/src/proof/proof_rule.h b/src/proof/proof_rule.h
index 107285cc3..a42b30773 100644
--- a/src/proof/proof_rule.h
+++ b/src/proof/proof_rule.h
@@ -219,11 +219,13 @@ enum class PfRule : uint32_t
   THEORY_REWRITE,
   // The remaining rules in this section have the signature of a "trusted rule":
   //
-  // Children: none
+  // Children: ?
   // Arguments: (F)
   // ---------------------------------------------------------------
   // Conclusion: F
   //
+  // Unless stated below, the expected children vector of the rule is empty.
+  //
   // where F is an equality of the form t = t' where t was replaced by t'
   // based on some preprocessing pass, or otherwise F was added as a new
   // assertion by some preprocessing pass.
@@ -248,8 +250,13 @@ enum class PfRule : uint32_t
   // could not be replayed during proof postprocessing.
   TRUST_SUBS,
   // where F is an equality (= t t') that holds by a form of substitution that
-  // could not be determined by the TrustSubstitutionMap.
+  // could not be determined by the TrustSubstitutionMap. This inference may
+  // contain possibly multiple children corresponding to the formulas used to
+  // derive the substitution.
   TRUST_SUBS_MAP,
+  // where F is a solved equality of the form (= x t) derived as the solved
+  // form of F', where F' is given as a child.
+  TRUST_SUBS_EQ,
   // ========= SAT Refutation for assumption-based unsat cores
   // Children: (P1, ..., Pn)
   // Arguments: none
diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp
index 7ec0525c9..dae3922e6 100644
--- a/src/theory/builtin/proof_checker.cpp
+++ b/src/theory/builtin/proof_checker.cpp
@@ -52,6 +52,7 @@ void BuiltinProofRuleChecker::registerTo(ProofChecker* pc)
   pc->registerTrustedChecker(PfRule::TRUST_REWRITE, this, 1);
   pc->registerTrustedChecker(PfRule::TRUST_SUBS, this, 1);
   pc->registerTrustedChecker(PfRule::TRUST_SUBS_MAP, this, 1);
+  pc->registerTrustedChecker(PfRule::TRUST_SUBS_EQ, this, 3);
 }
 
 Node BuiltinProofRuleChecker::applySubstitutionRewrite(
@@ -399,7 +400,7 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id,
            || id == PfRule::THEORY_EXPAND_DEF || id == PfRule::WITNESS_AXIOM
            || id == PfRule::THEORY_LEMMA || id == PfRule::THEORY_REWRITE
            || id == PfRule::TRUST_REWRITE || id == PfRule::TRUST_SUBS
-           || id == PfRule::TRUST_SUBS_MAP)
+           || id == PfRule::TRUST_SUBS_MAP || id == PfRule::TRUST_SUBS_EQ)
   {
     // "trusted" rules
     Assert(!args.empty());
diff --git a/src/theory/theory.h b/src/theory/theory.h
index d71348ce3..378305c75 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -675,8 +675,8 @@ class Theory {
    * add the solved substitutions to the map, if any. The method should return
    * true if the literal can be safely removed from the input problem.
    *
-   * Note that tin has trude node kind LEMMA. Its proof generator should be
-   * take into account when adding a substitution to outSubstitutions when
+   * Note that tin has trust node kind LEMMA. Its proof generator should be
+   * taken into account when adding a substitution to outSubstitutions when
    * proofs are enabled.
    */
   virtual PPAssertStatus ppAssert(TrustNode tin,
diff --git a/src/theory/trust_substitutions.cpp b/src/theory/trust_substitutions.cpp
index 7a2fb19bd..7934231b9 100644
--- a/src/theory/trust_substitutions.cpp
+++ b/src/theory/trust_substitutions.cpp
@@ -115,11 +115,10 @@ ProofGenerator* TrustSubstitutionMap::addSubstitutionSolved(TNode x,
   // Try to transform tn.getProven() to (= x t) here, if necessary
   if (!d_tspb->applyPredTransform(proven, eq, {}))
   {
-    // failed to rewrite, it is critical for unsat cores that proven is a
-    // premise here, since the conclusion depends on it
-    addSubstitution(x, t, PfRule::TRUST_SUBS_MAP, {proven}, {eq});
-    Trace("trust-subs") << "...failed to rewrite" << std::endl;
-    return nullptr;
+    // failed to rewrite, we add a trust step which assumes eq is provable
+    // from proven, and proceed as normal.
+    Trace("trust-subs") << "...failed to rewrite " << proven << std::endl;
+    d_tspb->addStep(PfRule::TRUST_SUBS_EQ, {proven}, {eq}, eq);
   }
   Trace("trust-subs") << "...successful rewrite" << std::endl;
   solvePg->addSteps(*d_tspb.get());
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index b5a45e8d5..0cb64510c 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -806,6 +806,7 @@ set(regress_0_tests
   regress0/printer/tuples_and_records.cvc
   regress0/proofs/issue277-circuit-propagator.smt2
   regress0/proofs/scope.smt2
+  regress0/proofs/trust-subs-eq-open.smt2
   regress0/push-pop/boolean/fuzz_12.smt2
   regress0/push-pop/boolean/fuzz_13.smt2
   regress0/push-pop/boolean/fuzz_14.smt2
diff --git a/test/regress/regress0/bv/core/bitvec1.smtv1.smt2 b/test/regress/regress0/bv/core/bitvec1.smtv1.smt2
index 78dd44d66..63273b899 100644
--- a/test/regress/regress0/bv/core/bitvec1.smtv1.smt2
+++ b/test/regress/regress0/bv/core/bitvec1.smtv1.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE:  --no-check-proofs
+; COMMAND-LINE:
 ; EXPECT: unsat
 (set-option :incremental false)
 (set-info :source "Hand-crafted bit-vector benchmarks.  Some are from the SVC benchmark suite.
diff --git a/test/regress/regress0/bv/core/bitvec3.smtv1.smt2 b/test/regress/regress0/bv/core/bitvec3.smtv1.smt2
index b149c0570..79af1ce94 100644
--- a/test/regress/regress0/bv/core/bitvec3.smtv1.smt2
+++ b/test/regress/regress0/bv/core/bitvec3.smtv1.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE:  --no-check-proofs
+; COMMAND-LINE:
 ; EXPECT: unsat
 (set-option :incremental false)
 (set-info :source "Hand-crafted bit-vector benchmarks.  Some are from the SVC benchmark suite.
diff --git a/test/regress/regress0/bv/core/constant_core.smt2 b/test/regress/regress0/bv/core/constant_core.smt2
index f9d2e022d..e433e58e2 100644
--- a/test/regress/regress0/bv/core/constant_core.smt2
+++ b/test/regress/regress0/bv/core/constant_core.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE:  --no-check-proofs
+; COMMAND-LINE:
 ; EXPECT: unsat
 (set-logic QF_BV)
 (set-info :smt-lib-version 2.6)
diff --git a/test/regress/regress0/cores/issue3455.smt2 b/test/regress/regress0/cores/issue3455.smt2
index ec72daa32..7050e8c7d 100644
--- a/test/regress/regress0/cores/issue3455.smt2
+++ b/test/regress/regress0/cores/issue3455.smt2
@@ -13,4 +13,4 @@
 (assert (<= x0 (- 13)))
 (check-sat)
 (check-sat)
-(check-sat)
\ No newline at end of file
+(check-sat)
diff --git a/test/regress/regress0/proofs/trust-subs-eq-open.smt2 b/test/regress/regress0/proofs/trust-subs-eq-open.smt2
new file mode 100644
index 000000000..5f6bd9ef9
--- /dev/null
+++ b/test/regress/regress0/proofs/trust-subs-eq-open.smt2
@@ -0,0 +1,8 @@
+(set-logic ALL)
+(set-info :status unsat)
+(declare-fun c () (_ BitVec 3))
+(check-sat-assuming (
+(and 
+(= (_ bv0 1) ((_ extract 1 1) c)) 
+(= (_ bv1 1) ((_ extract 0 0) c)) 
+(not (= (_ bv1 2) ((_ extract 1 0) c))))))