From 10308c88ae5de234eb62c08380d53d4967112ccd Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 13 Apr 2021 14:30:03 -0500
Subject: Formalize more skolems (#6307)

This formalizes more skolems in preparation for moving Theory::expandDefinitions to Rewriter::expandDefinitions.

It also adds proof support for datatypes purification.
---
 src/expr/skolem_manager.cpp |  6 ++++--
 src/expr/skolem_manager.h   | 14 +++++++++-----
 2 files changed, 13 insertions(+), 7 deletions(-)

(limited to 'src/expr')

diff --git a/src/expr/skolem_manager.cpp b/src/expr/skolem_manager.cpp
index 1d66cbee2..773159b09 100644
--- a/src/expr/skolem_manager.cpp
+++ b/src/expr/skolem_manager.cpp
@@ -50,6 +50,8 @@ const char* toString(SkolemFunId id)
     case SkolemFunId::INT_DIV_BY_ZERO: return "INT_DIV_BY_ZERO";
     case SkolemFunId::MOD_BY_ZERO: return "MOD_BY_ZERO";
     case SkolemFunId::SQRT: return "SQRT";
+    case SkolemFunId::SELECTOR_WRONG: return "SELECTOR_WRONG";
+    case SkolemFunId::SEQ_NTH_OOB: return "SEQ_NTH_OOB";
     default: return "?";
   }
 }
@@ -190,8 +192,8 @@ Node SkolemManager::mkPurifySkolem(Node t,
 
 Node SkolemManager::mkSkolemFunction(SkolemFunId id, TypeNode tn, Node cacheVal)
 {
-  std::pair<SkolemFunId, Node> key(id, cacheVal);
-  std::map<std::pair<SkolemFunId, Node>, Node>::iterator it =
+  std::tuple<SkolemFunId, TypeNode, Node> key(id, tn, cacheVal);
+  std::map<std::tuple<SkolemFunId, TypeNode, Node>, Node>::iterator it =
       d_skolemFuns.find(key);
   if (it == d_skolemFuns.end())
   {
diff --git a/src/expr/skolem_manager.h b/src/expr/skolem_manager.h
index 426202b7e..dd228e598 100644
--- a/src/expr/skolem_manager.h
+++ b/src/expr/skolem_manager.h
@@ -29,14 +29,18 @@ class ProofGenerator;
 /** Skolem function identifier */
 enum class SkolemFunId
 {
-  /* an uninterpreted function f s.t. f(x) = x / 0.0 (real division) */
+  /** an uninterpreted function f s.t. f(x) = x / 0.0 (real division) */
   DIV_BY_ZERO,
-  /* an uninterpreted function f s.t. f(x) = x / 0 (integer division) */
+  /** an uninterpreted function f s.t. f(x) = x / 0 (integer division) */
   INT_DIV_BY_ZERO,
-  /* an uninterpreted function f s.t. f(x) = x mod 0 */
+  /** an uninterpreted function f s.t. f(x) = x mod 0 */
   MOD_BY_ZERO,
-  /* an uninterpreted function f s.t. f(x) = sqrt(x) */
+  /** an uninterpreted function f s.t. f(x) = sqrt(x) */
   SQRT,
+  /** a wrongly applied selector */
+  SELECTOR_WRONG,
+  /** an application of seq.nth that is out of bounds */
+  SEQ_NTH_OOB,
 };
 /** Converts a skolem function name to a string. */
 const char* toString(SkolemFunId id);
@@ -283,7 +287,7 @@ class SkolemManager
   /**
    * Cached of skolem functions for mkSkolemFunction above.
    */
-  std::map<std::pair<SkolemFunId, Node>, Node> d_skolemFuns;
+  std::map<std::tuple<SkolemFunId, TypeNode, Node>, Node> d_skolemFuns;
   /**
    * Mapping from witness terms to proof generators.
    */
-- 
cgit v1.2.3