[proof-new] Registering proof checkers uniformly from the SMT solver (#6275)

Each theory has its own proof checker, responsible for checking the rules pertaining to that theory. The main proof checker uses these specialized checkers. Previously the main proof checker (of the proof node manager used across the SMT solver) was connected to these theory proof checkers during initialization of the theory. This commit adds an interface to the theories for retrieving its proof checker (analogous to how one retrieves the rewriter of a theory) which is used by a new method in the theory engine to register a theory proof checker to a given proof checker according to a theory id.

This is in preparation for the new unsat cores based on proofs.

2 files changed, 55 insertions, 23 deletions

diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index ab9b1b08d..6085c034d 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -87,6 +87,8 @@ void TheorySep::declareSepHeap(TypeNode locT, TypeNode dataT)
 
 TheoryRewriter* TheorySep::getTheoryRewriter() { return &d_rewriter; }
 
+ProofRuleChecker* TheorySep::getProofChecker() { return nullptr; }
+
 bool TheorySep::needsEqualityEngine(EeSetupInfo& esi)
 {
   esi.d_notify = &d_notify;
@@ -174,7 +176,7 @@ void TheorySep::computeCareGraph() {
 
 void TheorySep::postProcessModel( TheoryModel* m ){
   Trace("sep-model") << "Printing model for TheorySep..." << std::endl;
-  
+
   std::vector< Node > sep_children;
   Node m_neq;
   Node m_heap;
@@ -963,9 +965,15 @@ void TheorySep::ppNotifyAssertions(const std::vector<Node>& assertions) {
 }
 
 //return cardinality
-int TheorySep::processAssertion( Node n, std::map< int, std::map< Node, int > >& visited, 
-                                 std::map< int, std::map< Node, std::vector< Node > > >& references, std::map< int, std::map< Node, bool > >& references_strict,
-                                 bool pol, bool hasPol, bool underSpatial ) {
+int TheorySep::processAssertion(
+    Node n,
+    std::map<int, std::map<Node, int> >& visited,
+    std::map<int, std::map<Node, std::vector<Node> > >& references,
+    std::map<int, std::map<Node, bool> >& references_strict,
+    bool pol,
+    bool hasPol,
+    bool underSpatial)
+{
   int index = hasPol ? ( pol ? 1 : -1 ) : 0;
   int card = 0;
   std::map< Node, int >::iterator it = visited[index].find( n );
@@ -975,7 +983,7 @@ int TheorySep::processAssertion( Node n, std::map< int, std::map< Node, int > >&
       registerRefDataTypesAtom(n);
       if( hasPol && pol ){
         references[index][n].clear();
-        references_strict[index][n] = true; 
+        references_strict[index][n] = true;
       }else{
         card = 1;
       }
@@ -993,7 +1001,7 @@ int TheorySep::processAssertion( Node n, std::map< int, std::map< Node, int > >&
         references[index][n].push_back( n[0] );
       }
       if( hasPol && pol ){
-        references_strict[index][n] = true; 
+        references_strict[index][n] = true;
       }else{
         card = 1;
       }
@@ -1055,7 +1063,7 @@ int TheorySep::processAssertion( Node n, std::map< int, std::map< Node, int > >&
   }else{
     card = it->second;
   }
-  
+
   if( !underSpatial && ( !references[index][n].empty() || card>0 ) ){
     TypeNode tn = getReferenceType( n );
     Assert(!tn.isNull());
@@ -1157,7 +1165,7 @@ void TheorySep::initializeBounds() {
       Trace("sep-bound")  << "Initialize bounds for " << tn << "..." << std::endl;
       unsigned n_emp = 0;
       if( d_bound_kind[tn] != bound_invalid ){
-        n_emp = d_card_max[tn];  
+        n_emp = d_card_max[tn];
       }else if( d_type_references[tn].empty() ){
         //must include at least one constant TODO: remove?
         n_emp = 1;
@@ -1213,12 +1221,13 @@ Node TheorySep::getBaseLabel( TypeNode tn ) {
       }
     }else{
       //break symmetries TODO
-    
+
       d_type_references_all[tn].insert( d_type_references_all[tn].end(), d_type_references_card[tn].begin(), d_type_references_card[tn].end() );
     }
     //Assert( !d_type_references_all[tn].empty() );
-    
-    if( d_bound_kind[tn]!=bound_invalid ){      
+
+    if (d_bound_kind[tn] != bound_invalid)
+    {
       //construct bound
       d_reference_bound_max[tn] = mkUnion( tn, d_type_references_all[tn] );
       Trace("sep-bound") << "overall bound for " << d_base_label[tn] << " : " << d_reference_bound_max[tn] << std::endl;
@@ -1247,7 +1256,7 @@ Node TheorySep::getBaseLabel( TypeNode tn ) {
         }
       }
     }
-    
+
     //assert that nil ref is not in base label
     Node nr = getNilRef( tn );
     Node nrlem = NodeManager::currentNM()->mkNode( kind::MEMBER, nr, n_lbl ).negate();
@@ -1344,8 +1353,16 @@ Node TheorySep::applyLabel( Node n, Node lbl, std::map< Node, Node >& visited )
   }
 }
 
-Node TheorySep::instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std::map< Node, Node >& visited, std::map< Node, Node >& pto_model, 
-                                  TypeNode rtn, std::map< Node, bool >& active_lbl, unsigned ind ) {
+Node TheorySep::instantiateLabel(Node n,
+                                 Node o_lbl,
+                                 Node lbl,
+                                 Node lbl_v,
+                                 std::map<Node, Node>& visited,
+                                 std::map<Node, Node>& pto_model,
+                                 TypeNode rtn,
+                                 std::map<Node, bool>& active_lbl,
+                                 unsigned ind)
+{
   Trace("sep-inst-debug") << "Instantiate label " << n << " " << lbl << " " << lbl_v << std::endl;
   if( options::sepMinimalRefine() && lbl!=o_lbl && active_lbl.find( lbl )!=active_lbl.end() ){
     Trace("sep-inst") << "...do not instantiate " << o_lbl << " since it has an active sublabel " << lbl << std::endl;
@@ -1420,7 +1437,8 @@ Node TheorySep::instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std:
             for( unsigned i=0; i<children.size(); i++ ){
               std::vector< Node > tchildren;
               Node mval = mvals[i];
-              tchildren.push_back( NodeManager::currentNM()->mkNode( kind::SUBSET, mval, lbl ) );            
+              tchildren.push_back(
+                  NodeManager::currentNM()->mkNode(kind::SUBSET, mval, lbl));
               tchildren.push_back( children[i] );
               std::vector< Node > rem_children;
               for( unsigned j=0; j<children.size(); j++ ){
@@ -1442,7 +1460,7 @@ Node TheorySep::instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std:
           Node sub_lbl_0 = d_label_map[n][lbl][0];
           Node lbl_mval_0 = d_label_model[sub_lbl_0].getValue( rtn );
           wchildren.push_back( NodeManager::currentNM()->mkNode( kind::INTERSECTION, lbl_mval_0, lbl ).eqNode( empSet ).negate() );
-          
+
           //return the lemma
           wchildren.push_back( children[0].negate() );
           wchildren.push_back( children[1] );
diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h
index d52a3bca5..7d658352d 100644
--- a/src/theory/sep/theory_sep.h
+++ b/src/theory/sep/theory_sep.h
@@ -56,7 +56,7 @@ class TheorySep : public Theory {
 
   /** True node for predicates = false */
   Node d_false;
-  
+
   //whether bounds have been initialized
   bool d_bounds_init;
 
@@ -68,9 +68,14 @@ class TheorySep : public Theory {
 
   Node mkAnd( std::vector< TNode >& assumptions );
 
-  int processAssertion( Node n, std::map< int, std::map< Node, int > >& visited, 
-                        std::map< int, std::map< Node, std::vector< Node > > >& references, std::map< int, std::map< Node, bool > >& references_strict,
-                        bool pol, bool hasPol, bool underSpatial );
+  int processAssertion(
+      Node n,
+      std::map<int, std::map<Node, int> >& visited,
+      std::map<int, std::map<Node, std::vector<Node> > >& references,
+      std::map<int, std::map<Node, bool> >& references_strict,
+      bool pol,
+      bool hasPol,
+      bool underSpatial);
 
  public:
   TheorySep(context::Context* c,
@@ -93,6 +98,8 @@ class TheorySep : public Theory {
   //--------------------------------- initialization
   /** get the official theory rewriter of this theory */
   TheoryRewriter* getTheoryRewriter() override;
+  /** get the proof checker of this theory */
+  ProofRuleChecker* getProofChecker() override;
   /**
    * Returns true if we need an equality engine. If so, we initialize the
    * information regarding how it should be setup. For details, see the
@@ -258,7 +265,7 @@ class TheorySep : public Theory {
     bound_invalid,
   };
   std::map< TypeNode, unsigned > d_bound_kind;
-  
+
   std::map< TypeNode, std::vector< Node > > d_type_references_card;
   std::map< Node, unsigned > d_type_ref_card_id;
   std::map< TypeNode, std::vector< Node > > d_type_references_all;
@@ -328,8 +335,15 @@ class TheorySep : public Theory {
   void addPto( HeapAssertInfo * ei, Node ei_n, Node p, bool polarity );
   void mergePto( Node p1, Node p2 );
   void computeLabelModel( Node lbl );
-  Node instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std::map< Node, Node >& visited, std::map< Node, Node >& pto_model, 
-                         TypeNode rtn, std::map< Node, bool >& active_lbl, unsigned ind = 0 );
+  Node instantiateLabel(Node n,
+                        Node o_lbl,
+                        Node lbl,
+                        Node lbl_v,
+                        std::map<Node, Node>& visited,
+                        std::map<Node, Node>& pto_model,
+                        TypeNode rtn,
+                        std::map<Node, bool>& active_lbl,
+                        unsigned ind = 0);
   void setInactiveAssertionRec( Node fact, std::map< Node, std::vector< Node > >& lbl_to_assertions, std::map< Node, bool >& assert_active );
 
   Node mkUnion( TypeNode tn, std::vector< Node >& locs );