Add interface for skolem functions in SkolemManager (#6256)

This PR introduces the notion of a "skolem function" to SkolemManager, which is implemented as a simple cache of canonical skolem functions/variables.

This is a prerequisite for two things:
(1) Making progress on the LFSC proof conversion, which currently is cumbersome for skolems corresponding to regular expression unfolding.
(2) Cleaning up singletons. Having the ability make canonical skolem functions in skolem manager will enable Theory::expandDefinitions to move to TheoryRewriter::expandDefinitions. This will then enable removal of calls to SmtEngine::expandDefinitions.

This PR also makes arithmetic make use of this functionality already.

The next steps will be to clean up all raw uses of NodeManager::mkSkolem, especially for other theories that manually track allocated skolem functions.

2 files changed, 29 insertions, 60 deletions

diff --git a/src/theory/arith/operator_elim.cpp b/src/theory/arith/operator_elim.cpp
index 600724f33..85db55f3f 100644
--- a/src/theory/arith/operator_elim.cpp
+++ b/src/theory/arith/operator_elim.cpp
@@ -18,7 +18,6 @@
 
 #include "expr/attribute.h"
 #include "expr/bound_var_manager.h"
-#include "expr/skolem_manager.h"
 #include "expr/term_conversion_proof_generator.h"
 #include "options/arith_options.h"
 #include "smt/logic_exception.h"
@@ -265,7 +264,7 @@ Node OperatorElim::eliminateOperators(Node node,
       if (!den.isConst() || den.getConst<Rational>().sgn() == 0)
       {
         checkNonLinearLogic(node);
-        Node divByZeroNum = getArithSkolemApp(num, ArithSkolemId::DIV_BY_ZERO);
+        Node divByZeroNum = getArithSkolemApp(num, SkolemFunId::DIV_BY_ZERO);
         Node denEq0 = nm->mkNode(EQUAL, den, nm->mkConst(Rational(0)));
         ret = nm->mkNode(ITE, denEq0, divByZeroNum, ret);
       }
@@ -283,7 +282,7 @@ Node OperatorElim::eliminateOperators(Node node,
       {
         checkNonLinearLogic(node);
         Node intDivByZeroNum =
-            getArithSkolemApp(num, ArithSkolemId::INT_DIV_BY_ZERO);
+            getArithSkolemApp(num, SkolemFunId::INT_DIV_BY_ZERO);
         Node denEq0 = nm->mkNode(EQUAL, den, nm->mkConst(Rational(0)));
         ret = nm->mkNode(ITE, denEq0, intDivByZeroNum, ret);
       }
@@ -300,7 +299,7 @@ Node OperatorElim::eliminateOperators(Node node,
       if (!den.isConst() || den.getConst<Rational>().sgn() == 0)
       {
         checkNonLinearLogic(node);
-        Node modZeroNum = getArithSkolemApp(num, ArithSkolemId::MOD_BY_ZERO);
+        Node modZeroNum = getArithSkolemApp(num, SkolemFunId::MOD_BY_ZERO);
         Node denEq0 = nm->mkNode(EQUAL, den, nm->mkConst(Rational(0)));
         ret = nm->mkNode(ITE, denEq0, modZeroNum, ret);
       }
@@ -336,7 +335,7 @@ Node OperatorElim::eliminateOperators(Node node,
       Node lem;
       if (k == SQRT)
       {
-        Node skolemApp = getArithSkolemApp(node[0], ArithSkolemId::SQRT);
+        Node skolemApp = getArithSkolemApp(node[0], SkolemFunId::SQRT);
         Node uf = skolemApp.eqNode(var);
         Node nonNeg =
             nm->mkNode(AND, nm->mkNode(MULT, var, var).eqNode(node[0]), uf);
@@ -407,64 +406,44 @@ Node OperatorElim::eliminateOperators(Node node,
 
 Node OperatorElim::getAxiomFor(Node n) { return Node::null(); }
 
-Node OperatorElim::getArithSkolem(ArithSkolemId asi)
+Node OperatorElim::getArithSkolem(SkolemFunId id)
 {
-  std::map<ArithSkolemId, Node>::iterator it = d_arith_skolem.find(asi);
-  if (it == d_arith_skolem.end())
+  std::map<SkolemFunId, Node>::iterator it = d_arithSkolem.find(id);
+  if (it == d_arithSkolem.end())
   {
     NodeManager* nm = NodeManager::currentNM();
-
     TypeNode tn;
-    std::string name;
-    std::string desc;
-    switch (asi)
+    if (id == SkolemFunId::DIV_BY_ZERO || id == SkolemFunId::SQRT)
     {
-      case ArithSkolemId::DIV_BY_ZERO:
-        tn = nm->realType();
-        name = std::string("divByZero");
-        desc = std::string("partial real division");
-        break;
-      case ArithSkolemId::INT_DIV_BY_ZERO:
-        tn = nm->integerType();
-        name = std::string("intDivByZero");
-        desc = std::string("partial int division");
-        break;
-      case ArithSkolemId::MOD_BY_ZERO:
-        tn = nm->integerType();
-        name = std::string("modZero");
-        desc = std::string("partial modulus");
-        break;
-      case ArithSkolemId::SQRT:
-        tn = nm->realType();
-        name = std::string("sqrtUf");
-        desc = std::string("partial sqrt");
-        break;
-      default: Unhandled();
+      tn = nm->realType();
+    }
+    else
+    {
+      tn = nm->integerType();
     }
-
     Node skolem;
+    SkolemManager* sm = nm->getSkolemManager();
     if (options::arithNoPartialFun())
     {
-      // partial function: division
-      skolem = nm->mkSkolem(name, tn, desc, NodeManager::SKOLEM_EXACT_NAME);
+      // partial function: division, where we treat the skolem function as
+      // a constant
+      skolem = sm->mkSkolemFunction(id, tn);
     }
     else
     {
       // partial function: division
-      skolem = nm->mkSkolem(name,
-                            nm->mkFunctionType(tn, tn),
-                            desc,
-                            NodeManager::SKOLEM_EXACT_NAME);
+      skolem = sm->mkSkolemFunction(id, nm->mkFunctionType(tn, tn));
     }
-    d_arith_skolem[asi] = skolem;
+    // cache it
+    d_arithSkolem[id] = skolem;
     return skolem;
   }
   return it->second;
 }
 
-Node OperatorElim::getArithSkolemApp(Node n, ArithSkolemId asi)
+Node OperatorElim::getArithSkolemApp(Node n, SkolemFunId id)
 {
-  Node skolem = getArithSkolem(asi);
+  Node skolem = getArithSkolem(id);
   if (!options::arithNoPartialFun())
   {
     skolem = NodeManager::currentNM()->mkNode(APPLY_UF, skolem, n);
diff --git a/src/theory/arith/operator_elim.h b/src/theory/arith/operator_elim.h
index 1b2f7190e..ec29bcf49 100644
--- a/src/theory/arith/operator_elim.h
+++ b/src/theory/arith/operator_elim.h
@@ -17,6 +17,7 @@
 #include <map>
 
 #include "expr/node.h"
+#include "expr/skolem_manager.h"
 #include "theory/eager_proof_generator.h"
 #include "theory/logic_info.h"
 #include "theory/skolem_lemma.h"
@@ -59,20 +60,6 @@ class OperatorElim : public EagerProofGenerator
  private:
   /** Logic info of the owner of this class */
   const LogicInfo& d_info;
-
-  /** Arithmetic skolem identifier */
-  enum class ArithSkolemId
-  {
-    /* 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) */
-    INT_DIV_BY_ZERO,
-    /* an uninterpreted function f s.t. f(x) = x mod 0 */
-    MOD_BY_ZERO,
-    /* an uninterpreted function f s.t. f(x) = sqrt(x) */
-    SQRT,
-  };
-
   /**
    * Function symbols used to implement:
    * (1) Uninterpreted division-by-zero semantics.  Needed to deal with partial
@@ -85,8 +72,11 @@ class OperatorElim : public EagerProofGenerator
    * If the option arithNoPartialFun() is enabled, then the range of this map
    * stores Skolem constants instead of Skolem functions, meaning that the
    * function-ness of e.g. division by zero is ignored.
+   *
+   * Note that this cache is used only for performance reasons. Conceptually,
+   * these skolem functions actually live in SkolemManager.
    */
-  std::map<ArithSkolemId, Node> d_arith_skolem;
+  std::map<SkolemFunId, Node> d_arithSkolem;
   /**
    * Eliminate operators in term n. If n has top symbol that is not a core
    * one (including division, int division, mod, to_int, is_int, syntactic sugar
@@ -113,7 +103,7 @@ class OperatorElim : public EagerProofGenerator
    * Returns the Skolem in the above map for the given id, creating it if it
    * does not already exist.
    */
-  Node getArithSkolem(ArithSkolemId asi);
+  Node getArithSkolem(SkolemFunId asi);
   /**
    * Make the witness term, which creates a witness term based on the skolem
    * manager with this class as a proof generator.
@@ -131,7 +121,7 @@ class OperatorElim : public EagerProofGenerator
    * If the option arithNoPartialFun is enabled, this returns f, where f is
    * the Skolem constant for the identifier asi.
    */
-  Node getArithSkolemApp(Node n, ArithSkolemId asi);
+  Node getArithSkolemApp(Node n, SkolemFunId asi);
 
   /**
    * Called when a non-linear term n is given to this class. Throw an exception