Formalize shared selectors as skolem functions (#6591)

This is work towards properly printing shared selectors in external proofs.

diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp
index 9e09c06e6c3ba858fefb99579c13ad458fa68624..52c15a08d8645ca6f8edce77b89584c30a01c152 100644 (file)
--- a/src/expr/dtype.cpp
+++ b/src/expr/dtype.cpp
@@ -100,7 +100,8 @@ const DType& DType::datatypeOf(Node item)
   {
     case CONSTRUCTOR_TYPE: return t[t.getNumChildren() - 1].getDType();
     case SELECTOR_TYPE:
-    case TESTER_TYPE: return t[0].getDType();
+    case TESTER_TYPE:
+    case UPDATER_TYPE: return t[0].getDType();
     default:
       Unhandled() << "arg must be a datatype constructor, selector, or tester";
   }
@@ -864,10 +865,12 @@ Node DType::getSharedSelector(TypeNode dtt, TypeNode t, size_t index) const
   std::stringstream ss;
   ss << "sel_" << index;
   SkolemManager* sm = nm->getSkolemManager();
-  s = sm->mkDummySkolem(ss.str(),
-                        nm->mkSelectorType(dtt, t),
-                        "is a shared selector",
-                        NodeManager::SKOLEM_NO_NOTIFY);
+  TypeNode stype = nm->mkSelectorType(dtt, t);
+  Node nindex = nm->mkConst(Rational(index));
+  s = sm->mkSkolemFunction(SkolemFunId::SHARED_SELECTOR,
+                           stype,
+                           nindex,
+                           NodeManager::SKOLEM_NO_NOTIFY);
   d_sharedSel[dtt][t][index] = s;
   Trace("dt-shared-sel") << "Made " << s << " of type " << dtt << " -> " << t
                          << std::endl;

diff --git a/src/expr/skolem_manager.cpp b/src/expr/skolem_manager.cpp
index bb29f84ee2fde8c2a52943888f71440b1631b695..4004bf6fef6e4962baefc79064965c40212db7af 100644 (file)
--- a/src/expr/skolem_manager.cpp
+++ b/src/expr/skolem_manager.cpp
@@ -51,6 +51,7 @@ const char* toString(SkolemFunId id)
     case SkolemFunId::MOD_BY_ZERO: return "MOD_BY_ZERO";
     case SkolemFunId::SQRT: return "SQRT";
     case SkolemFunId::SELECTOR_WRONG: return "SELECTOR_WRONG";
+    case SkolemFunId::SHARED_SELECTOR: return "SHARED_SELECTOR";
     case SkolemFunId::SEQ_NTH_OOB: return "SEQ_NTH_OOB";
     default: return "?";
   }
@@ -190,7 +191,10 @@ Node SkolemManager::mkPurifySkolem(Node t,
   return k;
 }
 
-Node SkolemManager::mkSkolemFunction(SkolemFunId id, TypeNode tn, Node cacheVal)
+Node SkolemManager::mkSkolemFunction(SkolemFunId id,
+                                     TypeNode tn,
+                                     Node cacheVal,
+                                     int flags)
 {
   std::tuple<SkolemFunId, TypeNode, Node> key(id, tn, cacheVal);
   std::map<std::tuple<SkolemFunId, TypeNode, Node>, Node>::iterator it =
@@ -200,7 +204,7 @@ Node SkolemManager::mkSkolemFunction(SkolemFunId id, TypeNode tn, Node cacheVal)
     NodeManager* nm = NodeManager::currentNM();
     std::stringstream ss;
     ss << "SKOLEM_FUN_" << id;
-    Node k = nm->mkSkolem(ss.str(), tn, "an internal skolem function");
+    Node k = nm->mkSkolem(ss.str(), tn, "an internal skolem function", flags);
     d_skolemFuns[key] = k;
     return k;
   }

diff --git a/src/expr/skolem_manager.h b/src/expr/skolem_manager.h
index a6709373cc1f543427cc35bcda01372d67dcbb15..d6215394167e1f619f645e50ba03f21c3872f12c 100644 (file)
--- a/src/expr/skolem_manager.h
+++ b/src/expr/skolem_manager.h
@@ -39,6 +39,8 @@ enum class SkolemFunId
   SQRT,
   /** a wrongly applied selector */
   SELECTOR_WRONG,
+  /** a shared selector */
+  SHARED_SELECTOR,
   /** an application of seq.nth that is out of bounds */
   SEQ_NTH_OOB,
 };
@@ -231,7 +233,8 @@ class SkolemManager
    */
   Node mkSkolemFunction(SkolemFunId id,
                         TypeNode tn,
-                        Node cacheVal = Node::null());
+                        Node cacheVal = Node::null(),
+                        int flags = NodeManager::SKOLEM_DEFAULT);
   /**
    * Create a skolem constant with the given name, type, and comment. This
    * should only be used if the definition of the skolem does not matter.