From: Andrew Reynolds Date: Wed, 23 Oct 2019 00:42:55 +0000 (-0500) Subject: Refactoring skolems for sets (#3381) X-Git-Tag: cvc5-1.0.0~3875 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0d4d9bf3f31687d9cf48b0c45ab420b06ff099f7;p=cvc5.git Refactoring skolems for sets (#3381) This refactors skolems introduced in the theory of sets. This is analogous to how skolems are treated for the theory of strings. A key change that this commit enables is to identify "variable" sets based on those that weren't introduced by the SkolemCache (instead of via a check that their kind is `VARIABLE`, which is done currently and is error prone). --- diff --git a/src/theory/sets/skolem_cache.cpp b/src/theory/sets/skolem_cache.cpp index 99e6588ca..a70e6dc51 100644 --- a/src/theory/sets/skolem_cache.cpp +++ b/src/theory/sets/skolem_cache.cpp @@ -39,6 +39,13 @@ Node SkolemCache::mkTypedSkolemCached( } return it->second; } +Node SkolemCache::mkTypedSkolemCached(TypeNode tn, + Node a, + SkolemId id, + const char* c) +{ + return mkTypedSkolemCached(tn, a, Node::null(), id, c); +} Node SkolemCache::mkTypedSkolem(TypeNode tn, const char* c) { diff --git a/src/theory/sets/skolem_cache.h b/src/theory/sets/skolem_cache.h index 74a8073d4..f1f2a82c0 100644 --- a/src/theory/sets/skolem_cache.h +++ b/src/theory/sets/skolem_cache.h @@ -43,6 +43,14 @@ class SkolemCache */ enum SkolemId { + // exists k. k = a + SK_PURIFY, + // a != b => exists k. ( k in a != k in b ) + SK_DISEQUAL, + // a in tclosure(b) => exists k1 k2. ( a.1, k1 ) in b ^ ( k2, a.2 ) in b ^ + // ( k1 = k2 V ( k1, k2 ) in tclosure(b) ) + SK_TCLOSURE_DOWN1, + SK_TCLOSURE_DOWN2, // (a,b) in join(A,B) => exists k. (a,k) in A ^ (k,b) in B // This is cached by the nodes corresponding to (a,b) and join(A,B). SK_JOIN, @@ -54,6 +62,8 @@ class SkolemCache */ Node mkTypedSkolemCached( TypeNode tn, Node a, Node b, SkolemId id, const char* c); + /** same as above, cached based on key (a,null,id) */ + Node mkTypedSkolemCached(TypeNode tn, Node a, SkolemId id, const char* c); /** Same as above, but without caching. */ Node mkTypedSkolem(TypeNode tn, const char* c); /** Returns true if n is a skolem allocated by this class */ diff --git a/src/theory/sets/solver_state.cpp b/src/theory/sets/solver_state.cpp index 76c7c3884..7756fe081 100644 --- a/src/theory/sets/solver_state.cpp +++ b/src/theory/sets/solver_state.cpp @@ -137,10 +137,10 @@ void SolverState::registerTerm(Node r, TypeNode tnn, Node n) d_nvar_sets[r].push_back(n); Trace("sets-debug2") << "Non-var-set[" << r << "] : " << n << std::endl; } - else if (nk == VARIABLE) + else if (n.isVar() && !d_skCache.isSkolem(n)) { - // it is important that we check kind VARIABLE, due to the semantics of the - // universe set. + // it is important that we check it is a variable, but not an internally + // introduced skolem, due to the semantics of the universe set. if (tnn.isSet()) { if (d_var_set.find(r) == d_var_set.end()) @@ -401,7 +401,8 @@ Node SolverState::getProxy(Node n) return (*it).second; } NodeManager* nm = NodeManager::currentNM(); - Node k = nm->mkSkolem("sp", n.getType(), "proxy for set"); + Node k = d_skCache.mkTypedSkolemCached( + n.getType(), n, SkolemCache::SK_PURIFY, "sp"); d_proxy[n] = k; d_proxy_to_term[k] = n; Node eq = k.eqNode(n); diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 472395e1b..3b52da338 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -736,44 +736,50 @@ void TheorySetsPrivate::checkDisequalities() { //disequalities Trace("sets") << "TheorySetsPrivate: check disequalities..." << std::endl; + NodeManager* nm = NodeManager::currentNM(); for(NodeBoolMap::const_iterator it=d_deq.begin(); it !=d_deq.end(); ++it) { - if( (*it).second ){ - Node deq = (*it).first; - //check if it is already satisfied - Assert( d_equalityEngine.hasTerm( deq[0] ) && d_equalityEngine.hasTerm( deq[1] ) ); - Node r1 = d_equalityEngine.getRepresentative( deq[0] ); - Node r2 = d_equalityEngine.getRepresentative( deq[1] ); - bool is_sat = d_state.isSetDisequalityEntailed(r1, r2); - /* - if( !is_sat ){ - //try to make one of them empty - for( unsigned e=0; e<2; e++ ){ - } - } - */ - Trace("sets-debug") << "Check disequality " << deq << ", is_sat = " << is_sat << std::endl; - //will process regardless of sat/processed/unprocessed - d_deq[deq] = false; - - if( !is_sat ){ - if( d_deq_processed.find( deq )==d_deq_processed.end() ){ - d_deq_processed.insert( deq ); - d_deq_processed.insert( deq[1].eqNode( deq[0] ) ); - Trace("sets") << "Process Disequality : " << deq.negate() << std::endl; - TypeNode elementType = deq[0].getType().getSetElementType(); - Node x = NodeManager::currentNM()->mkSkolem("sde_", elementType); - Node mem1 = NodeManager::currentNM()->mkNode( kind::MEMBER, x, deq[0] ); - Node mem2 = NodeManager::currentNM()->mkNode( kind::MEMBER, x, deq[1] ); - Node lem = NodeManager::currentNM()->mkNode( kind::OR, deq, NodeManager::currentNM()->mkNode( kind::EQUAL, mem1, mem2 ).negate() ); - lem = Rewriter::rewrite( lem ); - d_im.assertInference(lem, d_emp_exp, "diseq", 1); - d_im.flushPendingLemmas(); - if (d_im.hasProcessed()) - { - return; - } - } - } + if (!(*it).second) + { + // not active + continue; + } + Node deq = (*it).first; + // check if it is already satisfied + Assert(d_equalityEngine.hasTerm(deq[0]) + && d_equalityEngine.hasTerm(deq[1])); + Node r1 = d_equalityEngine.getRepresentative(deq[0]); + Node r2 = d_equalityEngine.getRepresentative(deq[1]); + bool is_sat = d_state.isSetDisequalityEntailed(r1, r2); + Trace("sets-debug") << "Check disequality " << deq + << ", is_sat = " << is_sat << std::endl; + // will process regardless of sat/processed/unprocessed + d_deq[deq] = false; + + if (is_sat) + { + // already satisfied + continue; + } + if (d_deq_processed.find(deq) != d_deq_processed.end()) + { + // already added lemma + continue; + } + d_deq_processed.insert(deq); + d_deq_processed.insert(deq[1].eqNode(deq[0])); + Trace("sets") << "Process Disequality : " << deq.negate() << std::endl; + TypeNode elementType = deq[0].getType().getSetElementType(); + Node x = d_state.getSkolemCache().mkTypedSkolemCached( + elementType, deq[0], deq[1], SkolemCache::SK_DISEQUAL, "sde"); + Node mem1 = nm->mkNode(MEMBER, x, deq[0]); + Node mem2 = nm->mkNode(MEMBER, x, deq[1]); + Node lem = nm->mkNode(OR, deq, nm->mkNode(EQUAL, mem1, mem2).negate()); + lem = Rewriter::rewrite(lem); + d_im.assertInference(lem, d_emp_exp, "diseq", 1); + d_im.flushPendingLemmas(); + if (d_im.hasProcessed()) + { + return; } } } diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp index 382cb671b..65cff2418 100644 --- a/src/theory/sets/theory_sets_rels.cpp +++ b/src/theory/sets/theory_sets_rels.cpp @@ -510,6 +510,8 @@ void TheorySetsRels::check(Theory::Effort level) << " or can be infered by TC_Graph of tc_rel[0]! " << std::endl; return; } + NodeManager* nm = NodeManager::currentNM(); + // add mem_rep to d_tcrRep_tcGraph TC_IT tc_it = d_tcr_tcGraph.find( tc_rel ); Node mem_rep_fst = getRepresentative( RelsUtils::nthElementOfTuple( mem_rep, 0 ) ); @@ -544,25 +546,45 @@ void TheorySetsRels::check(Theory::Effort level) exp_map[mem_rep_tup] = exp; d_tcr_tcGraph_exps[tc_rel] = exp_map; } - Node fst_element = RelsUtils::nthElementOfTuple( exp[0], 0 ); Node snd_element = RelsUtils::nthElementOfTuple( exp[0], 1 ); - Node sk_1 = NodeManager::currentNM()->mkSkolem("stc", fst_element.getType()); - Node sk_2 = NodeManager::currentNM()->mkSkolem("stc", snd_element.getType()); - Node mem_of_r = NodeManager::currentNM()->mkNode(kind::MEMBER, exp[0], tc_rel[0]); - Node sk_eq = NodeManager::currentNM()->mkNode(kind::EQUAL, sk_1, sk_2); + SkolemCache& sc = d_state.getSkolemCache(); + Node sk_1 = sc.mkTypedSkolemCached(fst_element.getType(), + exp[0], + tc_rel[0], + SkolemCache::SK_TCLOSURE_DOWN1, + "stc1"); + Node sk_2 = sc.mkTypedSkolemCached(fst_element.getType(), + exp[0], + tc_rel[0], + SkolemCache::SK_TCLOSURE_DOWN2, + "stc2"); + Node mem_of_r = nm->mkNode(MEMBER, exp[0], tc_rel[0]); + Node sk_eq = nm->mkNode(EQUAL, sk_1, sk_2); Node reason = exp; if( tc_rel != exp[1] ) { - reason = NodeManager::currentNM()->mkNode(kind::AND, reason, NodeManager::currentNM()->mkNode(kind::EQUAL, tc_rel, exp[1])); - } - - Node conclusion = NodeManager::currentNM()->mkNode(kind::OR, mem_of_r, - (NodeManager::currentNM()->mkNode(kind::AND, NodeManager::currentNM()->mkNode(kind::MEMBER, RelsUtils::constructPair(tc_rel, fst_element, sk_1), tc_rel[0]), - (NodeManager::currentNM()->mkNode(kind::AND, NodeManager::currentNM()->mkNode(kind::MEMBER, RelsUtils::constructPair(tc_rel, sk_2, snd_element), tc_rel[0]), - (NodeManager::currentNM()->mkNode(kind::OR, sk_eq, NodeManager::currentNM()->mkNode(kind::MEMBER, RelsUtils::constructPair(tc_rel, sk_1, sk_2), tc_rel)))))))); - - Node tc_lemma = NodeManager::currentNM()->mkNode(kind::IMPLIES, reason, conclusion ); + reason = nm->mkNode(AND, reason, nm->mkNode(EQUAL, tc_rel, exp[1])); + } + + Node conc = nm->mkNode( + OR, + mem_of_r, + nm->mkNode( + AND, + nm->mkNode(MEMBER, + RelsUtils::constructPair(tc_rel, fst_element, sk_1), + tc_rel[0]), + nm->mkNode(MEMBER, + RelsUtils::constructPair(tc_rel, sk_2, snd_element), + tc_rel[0]), + nm->mkNode(OR, + sk_eq, + nm->mkNode(MEMBER, + RelsUtils::constructPair(tc_rel, sk_1, sk_2), + tc_rel)))); + + Node tc_lemma = nm->mkNode(IMPLIES, reason, conc); d_pending.push_back(tc_lemma); } @@ -1168,17 +1190,15 @@ void TheorySetsRels::check(Theory::Effort level) } void TheorySetsRels::makeSharedTerm( Node n ) { - if(d_shared_terms.find(n) == d_shared_terms.end()) { - Trace("rels-share") << " [sets-rels] making shared term " << n - << std::endl; - Node skolem = NodeManager::currentNM()->mkSkolem( "sts", NodeManager::currentNM()->mkSetType( n.getType() ) ); - Node skEq = - skolem.eqNode(NodeManager::currentNM()->mkNode(kind::SINGLETON, n)); - // force lemma to be sent immediately - d_im.assertInference(skEq, d_trueNode, "shared-term"); - d_im.flushPendingLemmas(); - d_shared_terms.insert(n); + if (d_shared_terms.find(n) != d_shared_terms.end()) + { + return; } + Trace("rels-share") << " [sets-rels] making shared term " << n << std::endl; + // force a proxy lemma to be sent for the singleton containing n + Node ss = NodeManager::currentNM()->mkNode(SINGLETON, n); + d_state.getProxy(ss); + d_shared_terms.insert(n); } /*