From 10308c88ae5de234eb62c08380d53d4967112ccd Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 13 Apr 2021 14:30:03 -0500 Subject: [PATCH] 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 +++++++----- src/theory/datatypes/infer_proof_cons.cpp | 6 +++++ src/theory/datatypes/theory_datatypes.cpp | 22 +++++-------------- src/theory/datatypes/theory_datatypes.h | 4 ---- src/theory/strings/skolem_cache.cpp | 7 ++++-- src/theory/strings/skolem_cache.h | 2 +- src/theory/strings/theory_strings.cpp | 3 +-- .../strings/theory_strings_preprocess.cpp | 2 +- 9 files changed, 33 insertions(+), 33 deletions(-) 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 key(id, cacheVal); - std::map, Node>::iterator it = + std::tuple key(id, tn, cacheVal); + std::map, 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, Node> d_skolemFuns; + std::map, 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 9d3532368..5ab8a563f 100644 --- 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 60fd87731..01ef77172 100644 --- 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 7997b9429..5617682ef 100644 --- 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 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 f68d7805b..eb2df1285 100644 --- 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 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 1006a758c..d64e4d5ae 100644 --- 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 ea0fc5ea8..0ed003cc7 100644 --- 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 1fd2bb519..5e6b27e1b 100644 --- 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` -- 2.30.2