From 730f4cf0c5cf5af8475e338fbe28e099b14bfed5 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 24 Mar 2022 13:14:59 -0500 Subject: [PATCH] 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(...). --- src/expr/skolem_manager.cpp | 4 +++ src/expr/skolem_manager.h | 8 ++++- src/theory/arrays/skolem_cache.cpp | 42 +++---------------------- src/theory/arrays/skolem_cache.h | 7 ----- src/theory/arrays/theory_arrays.cpp | 28 +---------------- src/theory/arrays/theory_arrays.h | 4 --- src/theory/bags/solver_state.cpp | 9 ++---- src/theory/sets/theory_sets_private.cpp | 5 +-- 8 files changed, 21 insertions(+), 86 deletions(-) diff --git a/src/expr/skolem_manager.cpp b/src/expr/skolem_manager.cpp index 7df8711a9..e3288c9e4 100644 --- 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 7ca3d2dc7..c83c35aeb 100644 --- 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 7cf192b7f..efc39e55a 100644 --- 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 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(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(deq, atnIndex); -} } // namespace arrays } // namespace theory diff --git a/src/theory/arrays/skolem_cache.h b/src/theory/arrays/skolem_cache.h index 17a5c6975..f69bd6ffc 100644 --- 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 fc5535408..b64f1d1da 100644 --- 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::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& 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::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 11c838c2b..beefda7d6 100644 --- 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 d_skolemCache; - context::CDO d_skolemIndex; - std::vector d_skolemAssertions; - // The decision requests we have for the core context::CDQueue d_decisionRequests; diff --git a/src/theory/bags/solver_state.cpp b/src/theory/bags/solver_state.cpp index 3a66d5c9a..8e15a0ebc 100644 --- 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(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 c6be43d6d..fc870b6ec 100644 --- 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()); -- 2.30.2