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.

diff --git a/src/expr/skolem_manager.cpp b/src/expr/skolem_manager.cpp
index 1d66cbee2809b56269cdb5d42a4fab424196e487..773159b09739c87169921888c289fba6c1c108c2 100644 (file)
--- 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 426202b7e36d180ab17becdc01383bec18bd0f78..dd228e5987331a55e07cfa4a6393d72cffee5311 100644 (file)
--- 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.
    */

diff --git a/src/theory/datatypes/infer_proof_cons.cpp b/src/theory/datatypes/infer_proof_cons.cpp
index 9d3532368645b3b22ec3db028ef7a5f82c1cb854..5ab8a563f0ba2ef18ab54fc6ce4ad0cd1b12f59a 100644 (file)
--- a/src/theory/datatypes/infer_proof_cons.cpp
+++ b/src/theory/datatypes/infer_proof_cons.cpp
@@ -222,6 +222,12 @@ void InferProofCons::convert(InferenceId infer, TNode conc, TNode exp, CDProof*
       success = true;
     }
     break;
+    case InferenceId::DATATYPES_PURIFY:
+    {
+      cdp->addStep(conc, PfRule::MACRO_SR_PRED_INTRO, {}, {});
+      success = true;
+    }
+    break;
     // inferences currently not supported
     case InferenceId::DATATYPES_LABEL_EXH:
     case InferenceId::DATATYPES_BISIMILAR:

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 60fd877318fd670f0767633924b3cce92e65b90c..01ef77172fc0645b14c170b68cab08d58442151f 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -523,9 +523,11 @@ TrustNode TheoryDatatypes::expandDefinition(Node n)
         {
           ret = sel;
         }else{
-          mkExpDefSkolem(selector, ndt, n.getType());
-          Node sk =
-              nm->mkNode(kind::APPLY_UF, d_exp_def_skolem[ndt][selector], n[0]);
+          SkolemManager* sm = nm->getSkolemManager();
+          TypeNode tnw = nm->mkFunctionType(ndt, n.getType());
+          Node f =
+              sm->mkSkolemFunction(SkolemFunId::SELECTOR_WRONG, tnw, selector);
+          Node sk = nm->mkNode(kind::APPLY_UF, f, n[0]);
           if (tst == nm->mkConst(false))
           {
             ret = sk;
@@ -835,17 +837,6 @@ void TheoryDatatypes::getPossibleCons( EqcInfo* eqc, Node n, std::vector< bool >
   }
 }
 
-void TheoryDatatypes::mkExpDefSkolem( Node sel, TypeNode dt, TypeNode rt ) {
-  if( d_exp_def_skolem[dt].find( sel )==d_exp_def_skolem[dt].end() ){
-    NodeManager* nm = NodeManager::currentNM();
-    SkolemManager* sm = nm->getSkolemManager();
-    std::stringstream ss;
-    ss << sel << "_uf";
-    d_exp_def_skolem[dt][sel] =
-        sm->mkDummySkolem(ss.str().c_str(), nm->mkFunctionType(dt, rt));
-  }
-}
-
 Node TheoryDatatypes::getTermSkolemFor( Node n ) {
   if( n.getKind()==APPLY_CONSTRUCTOR ){
     NodeMap::const_iterator it = d_term_sk.find( n );
@@ -853,8 +844,7 @@ Node TheoryDatatypes::getTermSkolemFor( Node n ) {
       NodeManager* nm = NodeManager::currentNM();
       SkolemManager* sm = nm->getSkolemManager();
       //add purification unit lemma ( k = n )
-      Node k =
-          sm->mkDummySkolem("k", n.getType(), "reference skolem for datatypes");
+      Node k = sm->mkPurifySkolem(n, "kdt");
       d_term_sk[n] = k;
       Node eq = k.eqNode( n );
       Trace("datatypes-infer") << "DtInfer : ref : " << eq << std::endl;

diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 7997b9429514dd255d134efe8de3748f5aa2ce92..5617682ef80fce52948a9db1280ce93ddd3e21d3 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -96,8 +96,6 @@ private:
   bool hasTester( Node n );
   /** get the possible constructors for n */
   void getPossibleCons( EqcInfo* eqc, Node n, std::vector< bool >& cons );
-  /** mkExpDefSkolem */
-  void mkExpDefSkolem( Node sel, TypeNode dt, TypeNode rt );
   /** skolems for terms */
   NodeMap d_term_sk;
   Node getTermSkolemFor( Node n );
@@ -153,8 +151,6 @@ private:
   context::CDList<TNode> d_functionTerms;
   /** counter for forcing assignments (ensures fairness) */
   unsigned d_dtfCounter;
-  /** expand definition skolem functions */
-  std::map< TypeNode, std::map< Node, Node > > d_exp_def_skolem;
   /** uninterpreted constant to variable map */
   std::map< Node, Node > d_uc_to_fresh_var;
 private:

diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp
index f68d7805b0888f7dbeacfc66c497cde1b14c3da5..eb2df12856a2f96710dfdee33a791040fc9ca552 100644 (file)
--- a/src/theory/strings/skolem_cache.cpp
+++ b/src/theory/strings/skolem_cache.cpp
@@ -141,15 +141,18 @@ Node SkolemCache::mkTypedSkolemCached(TypeNode tn,
 
 Node SkolemCache::mkSkolemSeqNth(TypeNode seqType, const char* c)
 {
+  // Note this method is static and does not rely on any local caching.
+  // It is used by expand definitions and by (dynamic) reductions, thus
+  // it is centrally located here.
   Assert(seqType.isSequence());
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   std::vector<TypeNode> argTypes;
   argTypes.push_back(seqType);
   argTypes.push_back(nm->integerType());
   TypeNode elemType = seqType.getSequenceElementType();
   TypeNode ufType = nm->mkFunctionType(argTypes, elemType);
-  return mkTypedSkolemCached(
-      ufType, Node::null(), Node::null(), SkolemCache::SK_NTH, c);
+  return sm->mkSkolemFunction(SkolemFunId::SEQ_NTH_OOB, ufType);
 }
 
 Node SkolemCache::mkSkolem(const char* c)

diff --git a/src/theory/strings/skolem_cache.h b/src/theory/strings/skolem_cache.h
index 1006a758c4ac3ca7f674d11c206db78f9b47b533..d64e4d5ae620c673b44a36499f570fbb9328ac84 100644 (file)
--- a/src/theory/strings/skolem_cache.h
+++ b/src/theory/strings/skolem_cache.h
@@ -164,7 +164,7 @@ class SkolemCache
    * Specific version for seq.nth, used for cases where the index is out of
    * range for sequence type seqType.
    */
-  Node mkSkolemSeqNth(TypeNode seqType, const char* c);
+  static Node mkSkolemSeqNth(TypeNode seqType, const char* c);
   /** Returns a (uncached) skolem of type string with name c */
   Node mkSkolem(const char* c);
   /** Returns true if n is a skolem allocated by this class */

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index ea0fc5ea84acda846f85ffcaf87b5088655febcf..0ed003cc7297ffa26c973578a5141f8235b26b74 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -560,7 +560,6 @@ TrustNode TheoryStrings::expandDefinition(Node node)
   if (node.getKind() == kind::SEQ_NTH)
   {
     NodeManager* nm = NodeManager::currentNM();
-    SkolemCache* sc = d_termReg.getSkolemCache();
     Node s = node[0];
     Node n = node[1];
     // seq.nth(s, n) --> ite(0 <= n < len(s), seq.nth_total(s,n), Uf(s, n))
@@ -568,7 +567,7 @@ TrustNode TheoryStrings::expandDefinition(Node node)
                            nm->mkNode(LEQ, d_zero, n),
                            nm->mkNode(LT, n, nm->mkNode(STRING_LENGTH, s)));
     Node ss = nm->mkNode(SEQ_NTH_TOTAL, s, n);
-    Node uf = sc->mkSkolemSeqNth(s.getType(), "Uf");
+    Node uf = SkolemCache::mkSkolemSeqNth(s.getType(), "Uf");
     Node u = nm->mkNode(APPLY_UF, uf, s, n);
     Node ret = nm->mkNode(ITE, cond, ss, u);
     Trace("strings-exp-def") << "...return " << ret << std::endl;

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 1fd2bb51939fd15454e1204bb4c15ce2c17ff189..5e6b27e1bf23e98c094f95bb630c5f1351d795f3 100644 (file)
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -445,7 +445,7 @@ Node StringsPreprocess::reduce(Node t,
     Node b1 = nm->mkNode(AND, b11, b12, b13);
 
     // nodes for the case where `seq.nth` is undefined.
-    Node uf = sc->mkSkolemSeqNth(s.getType(), "Uf");
+    Node uf = SkolemCache::mkSkolemSeqNth(s.getType(), "Uf");
     Node b2 = nm->mkNode(EQUAL, skt, nm->mkNode(APPLY_UF, uf, s, n));
 
     // the full ite, split on definedness of `seq.nth`