Standardize more instances of skolems (#8351)

This is work towards limiting our usage of witness terms for skolems.

It standardizes witnessing of disequalities for sets, bags, and arrays in the appropriate way that uses mkSkolemFunction(...) instead of mkSkolem(...).

diff --git a/src/expr/skolem_manager.cpp b/src/expr/skolem_manager.cpp
index 7df8711a918645386ce467b175cb1b252cd9f4b0..e3288c9e4087cf969da94567fc651736d6e202ab 100644 (file)
--- a/src/expr/skolem_manager.cpp
+++ b/src/expr/skolem_manager.cpp
@@ -52,6 +52,7 @@ const char* toString(SkolemFunId id)
 {
   switch (id)
   {
+    case SkolemFunId::ARRAY_DEQ_DIFF: return "ARRAY_DEQ_DIFF";
     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";
@@ -89,6 +90,9 @@ const char* toString(SkolemFunId id)
     case SkolemFunId::BAGS_MAP_PREIMAGE_SIZE: return "BAGS_MAP_PREIMAGE_SIZE";
     case SkolemFunId::BAGS_MAP_PREIMAGE_INDEX: return "BAGS_MAP_PREIMAGE_INDEX";
     case SkolemFunId::BAGS_MAP_SUM: return "BAGS_MAP_SUM";
+    case SkolemFunId::BAG_DEQ_DIFF: return "BAG_DEQ_DIFF";
+    case SkolemFunId::SETS_CHOOSE: return "SETS_CHOOSE";
+    case SkolemFunId::SETS_DEQ_DIFF: return "SETS_DEQ_DIFF";
     case SkolemFunId::HO_TYPE_MATCH_PRED: return "HO_TYPE_MATCH_PRED";
     default: return "?";
   }

diff --git a/src/expr/skolem_manager.h b/src/expr/skolem_manager.h
index 7ca3d2dc765db5ee4c57a089d0ab9b5704ebae3a..c83c35aebbd81174d0a8125d7fa40468444472cf 100644 (file)
--- a/src/expr/skolem_manager.h
+++ b/src/expr/skolem_manager.h
@@ -30,6 +30,8 @@ class ProofGenerator;
 enum class SkolemFunId
 {
   NONE,
+  /** array diff to witness (not (= A B)) */
+  ARRAY_DEQ_DIFF,
   /** 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) */
@@ -167,6 +169,8 @@ enum class SkolemFunId
    * sum(i) = sum (i-1) + (bag.count (uf i) A)
    */
   BAGS_MAP_SUM,
+  /** bag diff to witness (not (= A B)) */
+  BAG_DEQ_DIFF,
   /** An interpreted function for bag.choose operator:
    * (choose A) is expanded as
    * (witness ((x elementType))
@@ -178,8 +182,10 @@ enum class SkolemFunId
    * of A
    */
   SETS_CHOOSE,
+  /** set diff to witness (not (= A B)) */
+  SETS_DEQ_DIFF,
   /** Higher-order type match predicate, see HoTermDb */
-  HO_TYPE_MATCH_PRED,
+  HO_TYPE_MATCH_PRED
 };
 /** Converts a skolem function name to a string. */
 const char* toString(SkolemFunId id);

diff --git a/src/theory/arrays/skolem_cache.cpp b/src/theory/arrays/skolem_cache.cpp
index 7cf192b7f9435c2e3c85cf4f9061fea516b55e8c..efc39e55a10ab12292747ff6fb7ef56a27da7e9b 100644 (file)
--- a/src/theory/arrays/skolem_cache.cpp
+++ b/src/theory/arrays/skolem_cache.cpp
@@ -26,15 +26,6 @@ namespace cvc5 {
 namespace theory {
 namespace arrays {
 
-/**
- * A bound variable corresponding to an index for witnessing the satisfiability
- * of array disequalities.
- */
-struct ExtIndexVarAttributeId
-{
-};
-typedef expr::Attribute<ExtIndexVarAttributeId, Node> ExtIndexVarAttribute;
-
 /**
  * A bound variable corresponding to the index used in the eqrange expansion.
  */
@@ -53,25 +44,10 @@ Node SkolemCache::getExtIndexSkolem(Node deq)
   Assert(a.getType().isArray());
   Assert(b.getType() == a.getType());
 
-  NodeManager* nm = NodeManager::currentNM();
-
-  // get the reference index, which notice is deterministic for a, b in the
-  // lifetime of the node manager
-  Node x = getExtIndexVar(deq);
-
-  // make the axiom for x
-  Node as = nm->mkNode(SELECT, a, x);
-  Node bs = nm->mkNode(SELECT, b, x);
-  Node deqIndex = as.eqNode(bs).notNode();
-  Node axiom = nm->mkNode(IMPLIES, deq, deqIndex);
-
-  // make the skolem that witnesses the above axiom
-  SkolemManager* sm = nm->getSkolemManager();
-  return sm->mkSkolem(
-      x,
-      axiom,
-      "array_ext_index",
-      "an extensional lemma index variable from the theory of arrays");
+  // make the skolem, which is deterministic for a,b.
+  SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
+  return sm->mkSkolemFunction(
+      SkolemFunId::ARRAY_DEQ_DIFF, a.getType().getArrayIndexType(), {a, b});
 }
 
 Node SkolemCache::getEqRangeVar(TNode eqr)
@@ -81,16 +57,6 @@ Node SkolemCache::getEqRangeVar(TNode eqr)
   return bvm->mkBoundVar<EqRangeVarAttribute>(eqr, eqr[2].getType());
 }
 
-Node SkolemCache::getExtIndexVar(Node deq)
-{
-  Node a = deq[0][0];
-  TypeNode atn = a.getType();
-  Assert(atn.isArray());
-  Assert(atn == deq[0][1].getType());
-  TypeNode atnIndex = atn.getArrayIndexType();
-  BoundVarManager* bvm = NodeManager::currentNM()->getBoundVarManager();
-  return bvm->mkBoundVar<ExtIndexVarAttribute>(deq, atnIndex);
-}
 
 }  // namespace arrays
 }  // namespace theory

diff --git a/src/theory/arrays/skolem_cache.h b/src/theory/arrays/skolem_cache.h
index 17a5c6975b3f537c8e9bac1d3293d681a832c491..f69bd6ffc75f82eac0dbbe07b4e5cb3483d78e39 100644 (file)
--- a/src/theory/arrays/skolem_cache.h
+++ b/src/theory/arrays/skolem_cache.h
@@ -49,13 +49,6 @@ class SkolemCache
    * variable over the lifetime of `eqr`.
    */
   static Node getEqRangeVar(TNode eqr);
-
- private:
-  /**
-   * Get the bound variable x of the witness term above for disequality deq
-   * between arrays.
-   */
-  static Node getExtIndexVar(Node deq);
 };
 
 }  // namespace arrays

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index fc55354085311461903f5dc6566523c09dae6a3b..b64f1d1da5ed86e0f59adffe87c396728553b5ae 100644 (file)
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -99,7 +99,6 @@ TheoryArrays::TheoryArrays(Env& env,
       d_constReadsList(context()),
       d_constReadsContext(new context::Context()),
       d_contextPopper(context(), d_constReadsContext),
-      d_skolemIndex(context(), 0),
       d_decisionRequests(context()),
       d_permRef(context()),
       d_modelConstraints(context()),
@@ -1126,19 +1125,6 @@ bool TheoryArrays::collectModelValues(TheoryModel* m,
 
     // Build the STORE_ALL term with the default value
     rep = nm->mkConst(ArrayStoreAll(nrep.getType(), rep));
-    /*
-  }
-  else {
-    std::unordered_map<Node, Node>::iterator it = d_skolemCache.find(n);
-    if (it == d_skolemCache.end()) {
-      rep = nm->mkSkolem("array_collect_model_var", n.getType(), "base model
-  variable for array collectModelInfo"); d_skolemCache[n] = rep;
-    }
-    else {
-      rep = (*it).second;
-    }
-  }
-*/
 
     // For each read, require that the rep stores the right value
     vector<Node>& reads = selects[nrep];
@@ -1184,19 +1170,7 @@ void TheoryArrays::presolve()
 
 Node TheoryArrays::getSkolem(TNode ref)
 {
-  // the call to SkolemCache::getExtIndexSkolem should be deterministic, but use
-  // cache anyways for now
-  Node skolem;
-  std::unordered_map<Node, Node>::iterator it = d_skolemCache.find(ref);
-  if (it == d_skolemCache.end()) {
-    Assert(ref.getKind() == kind::NOT && ref[0].getKind() == kind::EQUAL);
-    // make the skolem using the skolem cache utility
-    skolem = SkolemCache::getExtIndexSkolem(ref);
-    d_skolemCache[ref] = skolem;
-  }
-  else {
-    skolem = (*it).second;
-  }
+  Node skolem = SkolemCache::getExtIndexSkolem(ref);
 
   Trace("pf::array") << "Pregistering a Skolem" << std::endl;
   preRegisterTermInternal(skolem);

diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 11c838c2bc7dbc66899a52256e3347d50848e0d1..beefda7d631b666efbfa158edd9f6e6353c8ca3d 100644 (file)
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -409,10 +409,6 @@ class TheoryArrays : public Theory {
   };/* class ContextPopper */
   ContextPopper d_contextPopper;
 
-  std::unordered_map<Node, Node> d_skolemCache;
-  context::CDO<unsigned> d_skolemIndex;
-  std::vector<Node> d_skolemAssertions;
-
   // The decision requests we have for the core
   context::CDQueue<Node> d_decisionRequests;
 

diff --git a/src/theory/bags/solver_state.cpp b/src/theory/bags/solver_state.cpp
index 3a66d5c9a51b702b75eed41f7b8e95b96feac314..8e15a0ebc6e568c77701a7ab2c79145495d26691 100644 (file)
--- a/src/theory/bags/solver_state.cpp
+++ b/src/theory/bags/solver_state.cpp
@@ -117,14 +117,9 @@ void SolverState::collectDisequalBagTerms()
       if (d_deq.find(equal) == d_deq.end())
       {
         TypeNode elementType = A.getType().getBagElementType();
-        BoundVarManager* bvm = d_nm->getBoundVarManager();
-        Node element = bvm->mkBoundVar<BagsDeqAttribute>(equal, elementType);
         SkolemManager* sm = d_nm->getSkolemManager();
-        Node skolem =
-            sm->mkSkolem(element,
-                         n,
-                         "bag_disequal",
-                         "an extensional lemma for disequality of two bags");
+        Node skolem = sm->mkSkolemFunction(
+            SkolemFunId::BAG_DEQ_DIFF, elementType, {A, B});
         d_deq[equal] = skolem;
       }
     }

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index c6be43d6d8c8aa0e1fce6a1d5df3e52263317f01..fc870b6ec0e108f56d7f3ea1ff849e80b3a1f7fd 100644 (file)
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -681,6 +681,7 @@ void TheorySetsPrivate::checkDisequalities()
   // disequalities
   Trace("sets") << "TheorySetsPrivate: check disequalities..." << std::endl;
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   for (NodeBoolMap::const_iterator it = d_deq.begin(); it != d_deq.end(); ++it)
   {
     if (!(*it).second)
@@ -714,8 +715,8 @@ void TheorySetsPrivate::checkDisequalities()
     d_termProcessed.insert(deq[1].eqNode(deq[0]));
     Trace("sets") << "Process Disequality : " << deq.negate() << std::endl;
     TypeNode elementType = deq[0].getType().getSetElementType();
-    Node x = d_skCache.mkTypedSkolemCached(
-        elementType, deq[0], deq[1], SkolemCache::SK_DISEQUAL, "sde");
+    Node x = sm->mkSkolemFunction(
+        SkolemFunId::SETS_DEQ_DIFF, elementType, {deq[0], deq[1]});
     Node mem1 = nm->mkNode(SET_MEMBER, x, deq[0]);
     Node mem2 = nm->mkNode(SET_MEMBER, x, deq[1]);
     Node lem = nm->mkNode(OR, deq, nm->mkNode(EQUAL, mem1, mem2).negate());