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.

4 files changed, 122 insertions, 60 deletions

diff --git a/src/expr/skolem_manager.cpp b/src/expr/skolem_manager.cpp
index 31c0b55cd..a823d5b60 100644
--- a/src/expr/skolem_manager.cpp
+++ b/src/expr/skolem_manager.cpp
@@ -14,6 +14,8 @@
 
 #include "expr/skolem_manager.h"
 
+#include <sstream>
+
 #include "expr/attribute.h"
 #include "expr/bound_var_manager.h"
 #include "expr/node_algorithm.h"
@@ -39,6 +41,24 @@ struct OriginalFormAttributeId
 };
 typedef expr::Attribute<OriginalFormAttributeId, Node> OriginalFormAttribute;
 
+const char* toString(SkolemFunId id)
+{
+  switch (id)
+  {
+    case SkolemFunId::DIV_BY_ZERO: return "DIV_BY_ZERO";
+    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";
+    default: return "?";
+  }
+}
+
+std::ostream& operator<<(std::ostream& out, SkolemFunId id)
+{
+  out << toString(id);
+  return out;
+}
+
 Node SkolemManager::mkSkolem(Node v,
                              Node pred,
                              const std::string& prefix,
@@ -167,6 +187,23 @@ Node SkolemManager::mkPurifySkolem(Node t,
   return k;
 }
 
+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 =
+      d_skolemFuns.find(key);
+  if (it == d_skolemFuns.end())
+  {
+    NodeManager* nm = NodeManager::currentNM();
+    std::stringstream ss;
+    ss << "SKOLEM_FUN_" << id;
+    Node k = nm->mkSkolem(ss.str(), tn, "an internal skolem function");
+    d_skolemFuns[key] = k;
+    return k;
+  }
+  return it->second;
+}
+
 Node SkolemManager::mkBooleanTermVariable(Node t)
 {
   return mkPurifySkolem(t, "", "", NodeManager::SKOLEM_BOOL_TERM_VAR);
diff --git a/src/expr/skolem_manager.h b/src/expr/skolem_manager.h
index 9955c0e15..1295b2249 100644
--- a/src/expr/skolem_manager.h
+++ b/src/expr/skolem_manager.h
@@ -25,6 +25,23 @@ namespace cvc5 {
 
 class ProofGenerator;
 
+/** Skolem function identifier */
+enum class SkolemFunId
+{
+  /* 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,
+};
+/** Converts a skolem function name to a string. */
+const char* toString(SkolemFunId id);
+/** Writes a skolem function name to a stream. */
+std::ostream& operator<<(std::ostream& out, SkolemFunId id);
+
 /**
  * A manager for skolems that can be used in proofs. This is designed to be
  * a trusted interface to NodeManager::mkSkolem, where one
@@ -56,6 +73,9 @@ class ProofGenerator;
  * Furthermore, note that original form and witness form may share skolems
  * in the rare case that a witness term is purified. This is currently only the
  * case for algorithms that introduce witness, e.g. BV/set instantiation.
+ *
+ * Additionally, we consider a third class of skolems (mkSkolemFunction) which
+ * are for convenience associated with an identifier, and not a witness term.
  */
 class SkolemManager
 {
@@ -176,6 +196,38 @@ class SkolemManager
                       const std::string& comment = "",
                       int flags = NodeManager::SKOLEM_DEFAULT);
   /**
+   * Make skolem function. This method should be used for creating fixed
+   * skolem functions of the forms described in SkolemFunId. The user of this
+   * method is responsible for providing a proper type for the identifier that
+   * matches the description of id. Skolem functions are useful for modelling
+   * the behavior of partial functions, or for theory-specific inferences that
+   * introduce fresh variables.
+   *
+   * A skolem function is not given a formal semantics in terms of a witness
+   * term, nor is it a purification skolem, thus it does not fall into the two
+   * categories of skolems above. This method is motivated by convenience, as
+   * the user of this method does not require constructing canonical variables
+   * for witness terms.
+   *
+   * The returned skolem is an ordinary skolem variable that can be used
+   * e.g. in APPLY_UF terms when tn is a function type.
+   *
+   * Notice that we do not insist that tn is a function type. A user of this
+   * method may construct a canonical (first-order) skolem using this method
+   * as well.
+   *
+   * @param id The identifier of the skolem function
+   * @param tn The type of the returned skolem function
+   * @param cacheVal A cache value. The returned skolem function will be
+   * unique to the pair (id, cacheVal). This value is required, for instance,
+   * for skolem functions that are in fact families of skolem functions,
+   * e.g. the wrongly applied case of selectors.
+   * @return The skolem function.
+   */
+  Node mkSkolemFunction(SkolemFunId id,
+                        TypeNode tn,
+                        Node cacheVal = Node::null());
+  /**
    * Make Boolean term variable for term t. This is a special case of
    * mkPurifySkolem above, where the returned term has kind
    * BOOLEAN_TERM_VARIABLE.
@@ -206,6 +258,10 @@ class SkolemManager
 
  private:
   /**
+   * Cached of skolem functions for mkSkolemFunction above.
+   */
+  std::map<std::pair<SkolemFunId, Node>, Node> d_skolemFuns;
+  /**
    * Mapping from witness terms to proof generators.
    */
   std::map<Node, ProofGenerator*> d_gens;
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