Basic proof support in inference manager (#4975)

This adds basic support for asserting internal facts with proofs in the inference manager class.

The purpose of this PR is twofold:
(1) From the point of view of proofs, this PR standardizes the management of proof equality engine within inference manager. Theories no longer have to manually construct proof equality engines, and instead are recommended to create inference managers.
(2) From the point of view of the new approach to theory combination, this PR ensures standard theory callbacks (preNotifyFact / notifyFact) are used for internal facts, regardless of whether proofs are enabled.

This will simplify several of the current (unmerged) changes for proof production in theory solvers on proof-new.

Notice this PR adds the utility method NodeManager::mkAnd, which is arguably long overdue.

Also notice this code is not yet active, but will be used on proof-new after this PR is merged.

2 files changed, 3 insertions, 35 deletions

diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp
index 274a46b26..021a737c0 100644
--- a/src/theory/uf/proof_equality_engine.cpp
+++ b/src/theory/uf/proof_equality_engine.cpp
@@ -126,7 +126,7 @@ bool ProofEqEngine::assertFact(Node lit,
     d_proof.addLazyStep(lit, &d_factPg, false);
   }
   // second, assert it to the equality engine
-  Node reason = mkAnd(exp);
+  Node reason = NodeManager::currentNM()->mkAnd(exp);
   return assertFactInternal(atom, polarity, reason);
 }
 
@@ -494,11 +494,11 @@ TrustNode ProofEqEngine::ensureProofForFact(Node conc,
     // scope the proof constructed above, and connect the formula with the proof
     // minimize the assumptions
     pf = d_pnm->mkScope(pfBody, scopeAssumps, true, true);
-    exp = mkAnd(scopeAssumps);
+    exp = nm->mkAnd(scopeAssumps);
   }
   else
   {
-    exp = mkAnd(assumps);
+    exp = nm->mkAnd(assumps);
   }
   // Make the lemma or conflict node. This must exactly match the conclusion
   // of SCOPE below.
@@ -668,32 +668,6 @@ void ProofEqEngine::explainWithProof(Node lit,
   Trace("pfee-proof") << "pfee::explainWithProof: finished" << std::endl;
 }
 
-Node ProofEqEngine::mkAnd(const std::vector<Node>& a)
-{
-  if (a.empty())
-  {
-    return d_true;
-  }
-  else if (a.size() == 1)
-  {
-    return a[0];
-  }
-  return NodeManager::currentNM()->mkNode(AND, a);
-}
-
-Node ProofEqEngine::mkAnd(const std::vector<TNode>& a)
-{
-  if (a.empty())
-  {
-    return d_true;
-  }
-  else if (a.size() == 1)
-  {
-    return a[0];
-  }
-  return NodeManager::currentNM()->mkNode(AND, a);
-}
-
 ProofEqEngine::FactProofGenerator::FactProofGenerator(context::Context* c,
                                                       ProofNodeManager* pnm)
     : ProofGenerator(), d_facts(c), d_pnm(pnm)
diff --git a/src/theory/uf/proof_equality_engine.h b/src/theory/uf/proof_equality_engine.h
index b71f72c53..314353131 100644
--- a/src/theory/uf/proof_equality_engine.h
+++ b/src/theory/uf/proof_equality_engine.h
@@ -307,12 +307,6 @@ class ProofEqEngine : public EagerProofGenerator
                                const std::vector<TNode>& assumps,
                                TrustNodeKind tnk,
                                LazyCDProof* curr);
-  /**
-   * Make the conjunction of nodes in a. Returns true if a is empty, and a
-   * single literal if a has size 1.
-   */
-  Node mkAnd(const std::vector<Node>& a);
-  Node mkAnd(const std::vector<TNode>& a);
   /** Reference to the equality engine */
   eq::EqualityEngine& d_ee;
   /** The default proof generator (for simple facts) */