(proof-new) Add proof support in TheoryUF (#5002)

This makes TheoryUF use a standard theory inference manager, which thus makes it proof producing when proof-new is enabled.

This additionally cleans HoExtension so that it does not keep a backwards reference to TheoryUF and instead takes its inference manager. This additionally adds two rules for higher-order that are required to make its equality engine proofs correct.

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>

diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp
index 0a45c6790f0f3518ed9ad65f68ead513e69ac6ce..bd58fc787ccb8af28f200b70d5aa9f770ef8e785 100644 (file)
--- a/src/expr/proof_rule.cpp
+++ b/src/expr/proof_rule.cpp
@@ -94,6 +94,8 @@ const char* toString(PfRule id)
     case PfRule::TRUE_ELIM: return "TRUE_ELIM";
     case PfRule::FALSE_INTRO: return "FALSE_INTRO";
     case PfRule::FALSE_ELIM: return "FALSE_ELIM";
+    case PfRule::HO_APP_ENCODE: return "HO_APP_ENCODE";
+    case PfRule::HO_CONG: return "HO_CONG";
     //================================================= Quantifiers rules
     case PfRule::WITNESS_INTRO: return "WITNESS_INTRO";
     case PfRule::EXISTS_INTRO: return "EXISTS_INTRO";

diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h
index 59c406d28ef7d20c99afe9c8c435fd0659083b21..b6b9f1ea8a31c21404611f9d343a95276d7f421d 100644 (file)
--- a/src/expr/proof_rule.h
+++ b/src/expr/proof_rule.h
@@ -520,6 +520,20 @@ enum class PfRule : uint32_t
   // ----------------------------------------
   // Conclusion: (not F)
   FALSE_ELIM,
+  // ======== HO trust
+  // Children: none
+  // Arguments: (t)
+  // ---------------------
+  // Conclusion: (= t TheoryUfRewriter::getHoApplyForApplyUf(t))
+  // For example, this rule concludes (f x y) = (HO_APPLY (HO_APPLY f x) y)
+  HO_APP_ENCODE,
+  // ======== Congruence
+  // Children: (P1:(= f g), P2:(= t1 s1), ..., Pn+1:(= tn sn))
+  // Arguments: ()
+  // ---------------------------------------------
+  // Conclusion: (= (f t1 ... tn) (g s1 ... sn))
+  // Notice that this rule is only used when the application kinds are APPLY_UF.
+  HO_CONG,
 
   //================================================= Quantifiers rules
   // ======== Witness intro

diff --git a/src/theory/uf/ho_extension.cpp b/src/theory/uf/ho_extension.cpp
index 11b872e724c8f18d29413bd22918ad770e749d50..2a57cde5e8d0c15d793ed7239e13a7aaddb9fd9f 100644 (file)
--- a/src/theory/uf/ho_extension.cpp
+++ b/src/theory/uf/ho_extension.cpp
@@ -18,7 +18,6 @@
 #include "expr/node_algorithm.h"
 #include "options/uf_options.h"
 #include "theory/theory_model.h"
-#include "theory/uf/theory_uf.h"
 #include "theory/uf/theory_uf_rewriter.h"
 
 using namespace std;
@@ -28,9 +27,9 @@ namespace CVC4 {
 namespace theory {
 namespace uf {
 
-HoExtension::HoExtension(TheoryUF& p, TheoryState& state)
-    : d_parent(p),
-      d_state(state),
+HoExtension::HoExtension(TheoryState& state, TheoryInferenceManager& im)
+    : d_state(state),
+      d_im(im),
       d_extensionality(state.getUserContext()),
       d_uf_std_skolem(state.getUserContext())
 {
@@ -108,7 +107,7 @@ unsigned HoExtension::applyExtensionality(TNode deq)
     Node lem = NodeManager::currentNM()->mkNode(OR, deq[0], conc);
     Trace("uf-ho-lemma") << "uf-ho-lemma : extensionality : " << lem
                          << std::endl;
-    d_parent.getOutputChannel().lemma(lem);
+    d_im.lemma(lem);
     return 1;
   }
   return 0;
@@ -168,7 +167,7 @@ Node HoExtension::getApplyUfForHoApply(Node node)
       Trace("uf-ho-lemma")
           << "uf-ho-lemma : Skolem definition for apply-conversion : " << lem
           << std::endl;
-      d_parent.getOutputChannel().lemma(lem);
+      d_im.lemma(lem);
       d_uf_std_skolem[f] = new_f;
     }
     else
@@ -257,7 +256,7 @@ unsigned HoExtension::checkExtensionality(TheoryModel* m)
               Node lem = nm->mkNode(OR, deq.negate(), eq);
               Trace("uf-ho") << "HoExtension: cmi extensionality lemma " << lem
                              << std::endl;
-              d_parent.getOutputChannel().lemma(lem);
+              d_im.lemma(lem);
               return 1;
             }
           }
@@ -282,10 +281,10 @@ unsigned HoExtension::applyAppCompletion(TNode n)
   Node ret = TheoryUfRewriter::getHoApplyForApplyUf(n);
   if (!ee->hasTerm(ret) || !ee->areEqual(ret, n))
   {
-    Node eq = ret.eqNode(n);
+    Node eq = n.eqNode(ret);
     Trace("uf-ho-lemma") << "uf-ho-lemma : infer, by apply-expand : " << eq
                          << std::endl;
-    ee->assertEquality(eq, true, d_true);
+    d_im.assertInternalFact(eq, true, PfRule::HO_APP_ENCODE, {}, {n});
     return 1;
   }
   Trace("uf-ho-debug") << "    ...already have " << ret << " == " << n << "."
@@ -442,7 +441,7 @@ bool HoExtension::collectModelInfoHoTerm(Node n, TheoryModel* m)
       Node eq = n.eqNode(hn);
       Trace("uf-ho") << "HoExtension: cmi app completion lemma " << eq
                      << std::endl;
-      d_parent.getOutputChannel().lemma(eq);
+      d_im.lemma(eq);
       return false;
     }
   }

diff --git a/src/theory/uf/ho_extension.h b/src/theory/uf/ho_extension.h
index 25cb3623b93b57c784c9a8d0f791ec2f0cf510e9..ceb8e9c125f1e839b5d2c995f49ba4485fe62500 100644 (file)
--- a/src/theory/uf/ho_extension.h
+++ b/src/theory/uf/ho_extension.h
@@ -21,6 +21,7 @@
 #include "context/cdhashset.h"
 #include "context/cdo.h"
 #include "expr/node.h"
+#include "theory/theory_inference_manager.h"
 #include "theory/theory_model.h"
 #include "theory/theory_state.h"
 
@@ -51,7 +52,7 @@ class HoExtension
   typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
 
  public:
-  HoExtension(TheoryUF& p, TheoryState& state);
+  HoExtension(TheoryState& state, TheoryInferenceManager& im);
 
   /** expand definition
    *
@@ -181,10 +182,10 @@ class HoExtension
  private:
   /** common constants */
   Node d_true;
-  /** the parent of this extension */
-  TheoryUF& d_parent;
   /** Reference to the state object */
   TheoryState& d_state;
+  /** Reference to the inference manager */
+  TheoryInferenceManager& d_im;
   /** extensionality has been applied to these disequalities */
   NodeSet d_extensionality;
 

diff --git a/src/theory/uf/proof_checker.cpp b/src/theory/uf/proof_checker.cpp
index b010b6d17c61f81de9fd84336ca00c381a2fcf54..ea95c1f24f530e5458c66ee48aebc25b7f4bd4cd 100644 (file)
--- a/src/theory/uf/proof_checker.cpp
+++ b/src/theory/uf/proof_checker.cpp
@@ -14,6 +14,8 @@
 
 #include "theory/uf/proof_checker.h"
 
+#include "theory/uf/theory_uf_rewriter.h"
+
 using namespace CVC4::kind;
 
 namespace CVC4 {
@@ -31,6 +33,8 @@ void UfProofRuleChecker::registerTo(ProofChecker* pc)
   pc->registerChecker(PfRule::TRUE_ELIM, this);
   pc->registerChecker(PfRule::FALSE_INTRO, this);
   pc->registerChecker(PfRule::FALSE_ELIM, this);
+  pc->registerChecker(PfRule::HO_CONG, this);
+  pc->registerChecker(PfRule::HO_APP_ENCODE, this);
 }
 
 Node UfProofRuleChecker::checkInternal(PfRule id,
@@ -171,6 +175,32 @@ Node UfProofRuleChecker::checkInternal(PfRule id,
     }
     return children[0][0].notNode();
   }
+  if (id == PfRule::HO_CONG)
+  {
+    Assert(children.size() > 0);
+    std::vector<Node> lchildren;
+    std::vector<Node> rchildren;
+    for (size_t i = 0, nchild = children.size(); i < nchild; ++i)
+    {
+      Node eqp = children[i];
+      if (eqp.getKind() != EQUAL)
+      {
+        return Node::null();
+      }
+      lchildren.push_back(eqp[0]);
+      rchildren.push_back(eqp[1]);
+    }
+    NodeManager* nm = NodeManager::currentNM();
+    Node l = nm->mkNode(kind::APPLY_UF, lchildren);
+    Node r = nm->mkNode(kind::APPLY_UF, rchildren);
+    return l.eqNode(r);
+  }
+  else if (id == PfRule::HO_APP_ENCODE)
+  {
+    Assert(args.size() == 1);
+    Node ret = TheoryUfRewriter::getHoApplyForApplyUf(args[0]);
+    return args[0].eqNode(ret);
+  }
   // no rule
   return Node::null();
 }

diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 3d90637e2da20bd686c9fe356ca929fca8c77193..a58834891cd5de2b5bcc2b48b8b5928ee5885b5d 100644 (file)
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -53,7 +53,8 @@ TheoryUF::TheoryUF(context::Context* c,
       d_ho(nullptr),
       d_functionsTerms(c),
       d_symb(u, instanceName),
-      d_state(c, u, valuation)
+      d_state(c, u, valuation),
+      d_im(*this, d_state, pnm)
 {
   d_true = NodeManager::currentNM()->mkConst( true );
 
@@ -62,8 +63,9 @@ TheoryUF::TheoryUF(context::Context* c,
   {
     d_ufProofChecker.registerTo(pc);
   }
-  // indicate we are using the default theory state object
+  // indicate we are using the default theory state and inference managers
   d_theoryState = &d_state;
+  d_inferManager = &d_im;
 }
 
 TheoryUF::~TheoryUF() {
@@ -96,7 +98,7 @@ void TheoryUF::finishInit() {
   if (options::ufHo())
   {
     d_equalityEngine->addFunctionKind(kind::HO_APPLY);
-    d_ho.reset(new HoExtension(*this, d_state));
+    d_ho.reset(new HoExtension(d_state, d_im));
   }
 }
 
@@ -304,12 +306,7 @@ void TheoryUF::explain(TNode literal, Node& exp)
   exp = mkAnd(assumptions);
 }
 
-TrustNode TheoryUF::explain(TNode literal)
-{
-  Node explanation;
-  explain(literal, explanation);
-  return TrustNode::mkTrustPropExp(literal, explanation, nullptr);
-}
+TrustNode TheoryUF::explain(TNode literal) { return d_im.explainLit(literal); }
 
 bool TheoryUF::collectModelValues(TheoryModel* m, const std::set<Node>& termSet)
 {
@@ -338,7 +335,8 @@ void TheoryUF::presolve() {
         i != newClauses.end();
         ++i) {
       Debug("uf") << "uf: generating a lemma: " << *i << std::endl;
-      d_out->lemma(*i);
+      // no proof generator provided
+      d_im.lemma(*i);
     }
   }
   if( d_thss ){
@@ -652,10 +650,10 @@ void TheoryUF::computeCareGraph() {
 
 void TheoryUF::conflict(TNode a, TNode b)
 {
-  Node conf;
-  explain(a.eqNode(b), conf);
-  d_out->conflict(conf);
-  d_state.notifyInConflict();
+  // call the inference manager, which will construct the conflict (possibly
+  // with proofs from the underlying proof equality engine), and notify the
+  // state object.
+  d_im.conflictEqConstantMerge(a, b);
 }
 
 void TheoryUF::eqNotifyNewClass(TNode t) {

diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 41f2ba9d5046e2b946e64ef4ce67803db94ba8aa..4a836948374c9385fa4d14d2895744f0393c3916 100644 (file)
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -26,6 +26,7 @@
 #include "theory/theory.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/uf/proof_checker.h"
+#include "theory/uf/proof_equality_engine.h"
 #include "theory/uf/symmetry_breaker.h"
 #include "theory/uf/theory_uf_rewriter.h"
 
@@ -205,6 +206,8 @@ private:
   UfProofRuleChecker d_ufProofChecker;
   /** A (default) theory state object */
   TheoryState d_state;
+  /** A (default) inference manager */
+  TheoryInferenceManager d_im;
 };/* class TheoryUF */
 
 }/* CVC4::theory::uf namespace */

diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h
index e651edb51ac8d3ae59091056a30f04aaf8b71504..5d301cf9ecbf9f75ecbe86738ad7f516a9ee77b9 100644 (file)
--- a/src/theory/uf/theory_uf_rewriter.h
+++ b/src/theory/uf/theory_uf_rewriter.h
@@ -22,6 +22,7 @@
 
 #include "expr/node_algorithm.h"
 #include "options/uf_options.h"
+#include "theory/rewriter.h"
 #include "theory/substitutions.h"
 #include "theory/theory_rewriter.h"