Fixes for dt ipc

ajreynol · Jan 15, 2025 · d5b770c · d5b770c
1 parent c27f5d6
commit d5b770c
Show file tree

Hide file tree

Showing 2 changed files with 64 additions and 8 deletions.
diff --git a/src/theory/datatypes/infer_proof_cons.cpp b/src/theory/datatypes/infer_proof_cons.cpp
@@ -144,7 +144,8 @@ void InferProofCons::convert(InferenceId infer, TNode conc, TNode exp, CDProof*
         if (n >= 0)
         {
           Node eq = tst.eqNode(conc);
-          cdp->addTheoryRewriteStep(eq, ProofRewriteRule::DT_INST);
+          // ensure the theory rewrite below is correct
+          tryRewriteRule(tst, conc, ProofRewriteRule::DT_INST, cdp);
           cdp->addStep(conc, ProofRule::EQ_RESOLVE, {tst, eq}, {});
           success = true;
         }
@@ -191,7 +192,7 @@ void InferProofCons::convert(InferenceId infer, TNode conc, TNode exp, CDProof*
         Node seq = sl.eqNode(sr);
         cdp->addStep(seq, ProofRule::CONG, {exp}, {asn, sop});
         Node sceq = sr.eqNode(concEq[1]);
-        cdp->addTheoryRewriteStep(sceq, ProofRewriteRule::DT_COLLAPSE_SELECTOR);
+        tryRewriteRule(sr, concEq[1], ProofRewriteRule::DT_COLLAPSE_SELECTOR, cdp);
         cdp->addStep(sl.eqNode(concEq[1]), ProofRule::TRANS, {seq, sceq}, {});
         if (conc.getKind() != Kind::EQUAL)
         {
@@ -264,13 +265,30 @@ void InferProofCons::convert(InferenceId infer, TNode conc, TNode exp, CDProof*
     break;
     case InferenceId::DATATYPES_LABEL_EXH:
     {
+      // partition to substitution / testers
+      std::vector<Node> expvs;
+      std::vector<Node> expvt;
+      std::map<Node, Node> tmap;
+      for (const Node& e : expv)
+      {
+        if (e.getKind() == Kind::NOT && e[0].getKind() == Kind::APPLY_TESTER)
+        {
+          expvt.push_back(e);
+          tmap[e[0].getOperator()] = e;
+        }
+        else if (e.getKind()==Kind::EQUAL)
+        {
+          expvs.push_back(e);
+        }
+      }
+
       // Exhausted labels. For example, this proves ~is-cons(x) => is-nil(x)
       // We prove this by:
       // ------------------------ DT_SPLIT
       // is-cons(x) or is-nil(x)            ~is-cons(x)
       // ---------------------------------------------- CHAIN_RESOLUTION
       // is-nil(x)
-      Node tst = expv[0];
+      Node tst = expvt[0];
       Assert(tst.getKind() == Kind::NOT
              && tst[0].getKind() == Kind::APPLY_TESTER);
       Node t = tst[0][0];
@@ -286,16 +304,34 @@ void InferProofCons::convert(InferenceId infer, TNode conc, TNode exp, CDProof*
         premises.push_back(sconc);
         std::vector<Node> pols;
         std::vector<Node> lits;
-        for (const Node& e : expv)
+        std::map<Node, Node>::iterator itt;
+        for (const Node& e : sconc)
         {
-          if (e.getKind() != Kind::NOT || e[0].getKind() != Kind::APPLY_TESTER)
+          Node en = e.notNode();
+          premises.push_back(en);
+          pols.emplace_back(truen);
+          lits.emplace_back(e);
+          // must ensure we have a proof of en
+          Assert (e.getKind()==Kind::APPLY_TESTER);
+          bool successLit = false;
+          itt = tmap.find(e.getOperator());
+          if (itt!=tmap.end())
+          {
+            if (itt->second==en)
+            {
+              successLit = true;
+            }
+            else
+            {
+              // otherwise maybe equal modulo rewriting?
+              Trace("dt-ipc") << "exh-label: " << itt->second << " vs " << en << ", substitution " << expvs << std::endl;
+            }
+          }
+          if (!successLit)
           {
             curr = Node::null();
             break;
           }
-          premises.push_back(e);
-          pols.emplace_back(truen);
-          lits.emplace_back(e[0]);
         }
         if (!curr.isNull())
         {
@@ -379,6 +415,20 @@ void InferProofCons::convert(InferenceId infer, TNode conc, TNode exp, CDProof*
   }
 }
 
+void InferProofCons::tryRewriteRule(TNode a, TNode b, ProofRewriteRule r, CDProof* cdp)
+{
+  Node eq = a.eqNode(b);
+  Node ar = d_env.getRewriter()->rewriteViaRule(r, a);
+  if (ar==b)
+  {
+    cdp->addTheoryRewriteStep(eq, r);
+  }
+  else
+  {
+    cdp->addTrustedStep(eq, TrustId::THEORY_INFERENCE_DATATYPES, {}, {});
+  }
+}
+
 void InferProofCons::addDtUnif(CDProof* cdp,
                                const Node& conc,
                                const Node& exp,

diff --git a/src/theory/datatypes/infer_proof_cons.h b/src/theory/datatypes/infer_proof_cons.h
@@ -18,6 +18,7 @@
 #ifndef CVC5__THEORY__DATATYPES__INFER_PROOF_CONS_H
 #define CVC5__THEORY__DATATYPES__INFER_PROOF_CONS_H
 
+#include "proof/proof.h"
 #include "context/cdhashmap.h"
 #include "expr/node.h"
 #include "proof/proof_generator.h"
@@ -83,6 +84,11 @@ class InferProofCons : protected EnvObj, public ProofGenerator
    * information is stored in cdp.
    */
   void convert(InferenceId infer, TNode conc, TNode exp, CDProof* cdp);
+  /**
+   * Add a step a=b to cdp using ProofRewriteRule rule r if possible, or a
+   * trust step otherwise.
+   */
+  void tryRewriteRule(TNode a, TNode b, ProofRewriteRule r, CDProof* cdp);
   /**
    * Adds a step concluding t_i = s_i from C(t_1 ... t_n) = C(s_1 ... s_n),
    * where i is stored in the node narg.