From 891e283a2bde4055dfed88c1ad2a2bdb2a98a150 Mon Sep 17 00:00:00 2001 From: Paul Meng Date: Tue, 28 Mar 2017 23:08:52 -0500 Subject: [PATCH] Refactor the standard effort of relational solver --- src/theory/sets/theory_sets_rels.cpp | 663 +++++++++---------------- src/theory/sets/theory_sets_rels.h | 53 +- test/regress/regress0/rels/Makefile.am | 4 +- 3 files changed, 254 insertions(+), 466 deletions(-) diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp index b5b7c90b4..0c5c7a6a2 100644 --- a/src/theory/sets/theory_sets_rels.cpp +++ b/src/theory/sets/theory_sets_rels.cpp @@ -31,8 +31,6 @@ typedef std::map< Node, std::hash_set< Node, NodeHashFunction > >::iterator typedef std::map< Node, std::map< kind::Kind_t, std::vector< Node > > >::iterator TERM_IT; typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction > > >::iterator TC_IT; -int TheorySetsRels::EqcInfo::counter = 0; - void TheorySetsRels::check(Theory::Effort level) { Trace("rels") << "\n[sets-rels] ******************************* Start the relational solver, effort = " << level << " *******************************\n" << std::endl; if(Theory::fullEffort(level)) { @@ -147,8 +145,9 @@ int TheorySetsRels::EqcInfo::counter = 0; if( getRepresentative(eqc_rep) == getRepresentative(d_trueNode) || getRepresentative(eqc_rep) == getRepresentative(d_falseNode) ) { + // collect membership info - if( eqc_node.getKind() == kind::MEMBER && eqc_node[1].getType().getSetElementType().isTuple() ) { + if( eqc_node.getKind() == kind::MEMBER && eqc_node[1].getType().getSetElementType().isTuple()) { Node tup_rep = getRepresentative( eqc_node[0] ); Node rel_rep = getRepresentative( eqc_node[1] ); @@ -216,17 +215,17 @@ int TheorySetsRels::EqcInfo::counter = 0; */ /* + * TCLOSURE TCLOSURE(x) = x | x.x | x.x.x | ... (| is union) * - * - * transitive closure rule 1: y = (TCLOSURE x) - * --------------------------------------------- - * y = x | x.x | x.x.x | ... (| is union) + * TCLOSURE-UP I: (a, b) IS_IN x TCLOSURE(x) in T + * --------------------------------------------- + * (a, b) IS_IN TCLOSURE(x) * * * - * transitive closure rule 2: TCLOSURE(x) - * ----------------------------------------------------------- - * x <= TCLOSURE(x) && (x JOIN x) <= TCLOSURE(x) .... + * TCLOSURE-UP II : (a, b) IS_IN TCLOSURE(x) (b, c) IS_IN TCLOSURE(x) + * ----------------------------------------------------------- + * (a, c) IS_IN TCLOSURE(x) * */ void TheorySetsRels::applyTCRule( Node mem_rep, Node tc_rel, Node tc_rel_rep, Node exp ) { @@ -491,7 +490,7 @@ int TheorySetsRels::EqcInfo::counter = 0; Node fact_2 = NodeManager::currentNM()->mkNode(kind::MEMBER, mem2, pt_rel[1]); if( pt_rel != exp[1] ) { - reason = NodeManager::currentNM()->mkNode(kind::AND, exp, explain(NodeManager::currentNM()->mkNode(kind::EQUAL, pt_rel, exp[1]))); + reason = NodeManager::currentNM()->mkNode(kind::AND, exp, NodeManager::currentNM()->mkNode(kind::EQUAL, pt_rel, exp[1])); } sendInfer( fact_1, reason, "product-split" ); sendInfer( fact_2, reason, "product-split" ); @@ -569,18 +568,14 @@ int TheorySetsRels::EqcInfo::counter = 0; } /* - * transpose-occur rule: [NOT] (a, b) IS_IN X (TRANSPOSE X) occurs - * ------------------------------------------------------- - * [NOT] (b, a) IS_IN (TRANSPOSE X) + * transpose-occur rule: (a, b) IS_IN X (TRANSPOSE X) in T + * --------------------------------------- + * (b, a) IS_IN (TRANSPOSE X) * - * transpose-reverse rule: [NOT] (a, b) IS_IN (TRANSPOSE X) - * ------------------------------------------------ - * [NOT] (b, a) IS_IN X + * transpose-reverse rule: (a, b) IS_IN (TRANSPOSE X) + * --------------------------------------- + * (b, a) IS_IN X * - * Not implemented yet! - * transpose-equal rule: [NOT] (TRANSPOSE X) = (TRANSPOSE Y) - * ----------------------------------------------- - * [NOT] (X = Y) */ void TheorySetsRels::applyTransposeRule( std::vector tp_terms ) { if( tp_terms.size() < 1) { @@ -809,9 +804,6 @@ int TheorySetsRels::EqcInfo::counter = 0; doTCLemmas(); Trace("rels-debug") << "[Theory::Rels] **************** Done with doPendingLemmas !" << std::endl; d_tuple_reps.clear(); -// d_id_node.clear(); -// d_node_id.clear(); - d_tuple_reps.clear(); d_rReps_memberReps_exp_cache.clear(); d_terms_cache.clear(); d_lemmas_out.clear(); @@ -824,9 +816,12 @@ int TheorySetsRels::EqcInfo::counter = 0; d_tcr_tcGraph.clear(); d_tc_lemmas_last.clear(); } + + bool TheorySetsRels::isRelationKind( Kind k ) { return k == kind::TRANSPOSE || k == kind::PRODUCT || k == kind::JOIN || k == kind::TCLOSURE; } + void TheorySetsRels::doTCLemmas() { Trace("rels-debug") << "[Theory::Rels] **************** Start doTCLemmas !" << std::endl; std::map< Node, std::vector< Node > >::iterator tc_lemma_it = d_tc_lemmas_last.begin(); @@ -1003,7 +998,6 @@ int TheorySetsRels::EqcInfo::counter = 0; eq::EqualityEngine* eq, context::CDO* conflict, TheorySets& d_set ): - d_vec_size(c), d_eqEngine(eq), d_conflict(conflict), d_sets_theory(d_set), @@ -1090,403 +1084,273 @@ int TheorySetsRels::EqcInfo::counter = 0; } } - Node TheorySetsRels::explain( Node literal ){ - //use lazy explanations - return literal; - } - TheorySetsRels::EqcInfo::EqcInfo( context::Context* c ) : - d_mem(c), d_mem_exp(c), d_in(c), d_out(c), - d_tp(c), d_pt(c), d_join(c), d_tc(c) {} - - // Create an integer id for tuple element - int TheorySetsRels::getOrMakeElementRepId(EqcInfo* ei, Node e_rep) { - Trace("rels-std") << "[sets-rels] getOrMakeElementRepId:" << " e_rep = " << e_rep << std::endl; - std::map< Node, int >::iterator nid_it = d_node_id.find(e_rep); - - if( nid_it == d_node_id.end() ) { - if( d_eqEngine->hasTerm(e_rep) ) { - // it is possible that e's rep changes at this moment, thus we need to know the previous rep id of eqc of e - eq::EqClassIterator rep_eqc_i = eq::EqClassIterator( e_rep, d_eqEngine ); - while( !rep_eqc_i.isFinished() ) { - std::map< Node, int >::iterator id_it = d_node_id.find(*rep_eqc_i); - - if( id_it != d_node_id.end() ) { - d_id_node[id_it->second] = e_rep; - d_node_id[e_rep] = id_it->second; - return id_it->second; - } - rep_eqc_i++; - } - } - d_id_node[ei->counter] = e_rep; - d_node_id[e_rep] = ei->counter; - ei->counter++; - return ei->counter-1; - } - Trace("rels-std") << "[sets-rels] finish getOrMakeElementRepId:" << " e_rep = " << e_rep << std::endl; - return nid_it->second; - } - - bool TheorySetsRels::insertIntoIdList(IdList& idList, int mem) { - IdList::const_iterator idListIt = idList.begin(); - while(idListIt != idList.end()) { - if(*idListIt == mem) { - return false; - } - idListIt++; - } - idList.push_back(mem); - return true; - } - - void TheorySetsRels::addTCMemAndSendInfer( EqcInfo* tc_ei, Node membership, Node exp, bool fromRel ) { - Trace("rels-std") << "[sets-rels] addTCMemAndSendInfer:" << " membership = " << membership << " from a relation? " << fromRel<< std::endl; - - Node fst = RelsUtils::nthElementOfTuple(membership[0], 0); - Node snd = RelsUtils::nthElementOfTuple(membership[0], 1); - Node fst_rep = getRepresentative(fst); - Node snd_rep = getRepresentative(snd); - Node mem_rep = RelsUtils::constructPair(membership[1], fst_rep, snd_rep); - - if(tc_ei->d_mem.find(mem_rep) != tc_ei->d_mem.end()) { - return; - } - - int fst_rep_id = getOrMakeElementRepId( tc_ei, fst_rep ); - int snd_rep_id = getOrMakeElementRepId( tc_ei, snd_rep ); - - std::hash_set in_reachable; - std::hash_set out_reachable; - collectReachableNodes(tc_ei->d_id_inIds, fst_rep_id, in_reachable); - collectReachableNodes(tc_ei->d_id_outIds, snd_rep_id, out_reachable); - - // If fst_rep is inserted into in_lst successfully, - // save rep pair's exp and send out TC inference lemmas. - // Otherwise, mem's rep is already in the TC and return. - if( addId(tc_ei->d_id_inIds, snd_rep_id, fst_rep_id) ) { - Node reason = exp == Node::null() ? explain(membership) : exp; - if(!fromRel && tc_ei->d_tc.get() != membership[1]) { - reason = NodeManager::currentNM()->mkNode(kind::AND,reason, explain(NodeManager::currentNM()->mkNode(kind::EQUAL,tc_ei->d_tc.get(), membership[1]))); - } - if(fst != fst_rep) { - reason = NodeManager::currentNM()->mkNode(kind::AND,reason, explain(NodeManager::currentNM()->mkNode(kind::EQUAL,fst, fst_rep))); - } - if(snd != snd_rep) { - reason = NodeManager::currentNM()->mkNode(kind::AND,reason, explain(NodeManager::currentNM()->mkNode(kind::EQUAL,snd, snd_rep))); - } - tc_ei->d_mem_exp[mem_rep] = reason; - Trace("rels-std") << "Added member " << mem_rep << " for " << tc_ei->d_tc.get()<< " with reason = " << reason << std::endl; - tc_ei->d_mem.insert(mem_rep); - Trace("rels-std") << "Added in membership arrow for " << snd_rep << " from: " << fst_rep << std::endl; - } else { - // Nothing inserted into the eqc - return; - } - Trace("rels-std") << "Add out membership arrow for " << fst_rep << " to : " << snd_rep << std::endl; - addId(tc_ei->d_id_inIds, fst_rep_id, snd_rep_id); - sendTCInference(tc_ei, in_reachable, out_reachable, mem_rep, fst_rep, snd_rep, fst_rep_id, snd_rep_id); - } - - Node TheorySetsRels::explainTCMem(EqcInfo* ei, Node pair, Node fst, Node snd) { - Trace("rels-tc") << "explainTCMem ############ pair = " << pair << std::endl; - if(ei->d_mem_exp.find(pair) != ei->d_mem_exp.end()) { - return (*ei->d_mem_exp.find(pair)).second; - } - NodeMap::iterator mem_exp_it = ei->d_mem_exp.begin(); - - while(mem_exp_it != ei->d_mem_exp.end()) { - Node tuple = (*mem_exp_it).first; - Node fst_e = RelsUtils::nthElementOfTuple(tuple, 0); - Node snd_e = RelsUtils::nthElementOfTuple(tuple, 1); - Node reason = (*mem_exp_it).second; + d_mem(c), d_mem_exp(c), d_tp(c), d_pt(c), d_tc(c), d_rel_tc(c) {} - if(areEqual(fst, fst_e) && areEqual(snd, snd_e)) { - if( fst != fst_e) { - reason = NodeManager::currentNM()->mkNode(kind::AND, reason, explain( NodeManager::currentNM()->mkNode(kind::EQUAL, fst, fst_e)) ); - } - if( snd != snd_e) { - reason = NodeManager::currentNM()->mkNode(kind::AND, reason, explain( NodeManager::currentNM()->mkNode(kind::EQUAL, snd, snd_e)) ); - } - return reason; - } - ++mem_exp_it; - } - if(!ei->d_tc.get().isNull()) { - Node rel_rep = getRepresentative(ei->d_tc.get()[0]); - EqcInfo* rel_ei = getOrMakeEqcInfo(rel_rep); - if(rel_ei != NULL) { - NodeMap::iterator rel_mem_exp_it = rel_ei->d_mem_exp.begin(); - while(rel_mem_exp_it != rel_ei->d_mem_exp.end()) { - Node exp = rel_rep == ei->d_tc.get()[0] ? d_trueNode : explain(NodeManager::currentNM()->mkNode(kind::EQUAL,rel_rep, ei->d_tc.get()[0])); - Node tuple = (*rel_mem_exp_it).first; - Node fst_e = RelsUtils::nthElementOfTuple(tuple, 0); - Node snd_e = RelsUtils::nthElementOfTuple(tuple, 1); - - if(areEqual(fst, fst_e) && areEqual(snd, snd_e)) { - if( fst != fst_e) { - exp = NodeManager::currentNM()->mkNode(kind::AND, exp, explain( NodeManager::currentNM()->mkNode(kind::EQUAL, fst, fst_e)) ); - } - if( snd != snd_e) { - exp = NodeManager::currentNM()->mkNode(kind::AND, exp, explain( NodeManager::currentNM()->mkNode(kind::EQUAL, snd, snd_e)) ); + void TheorySetsRels::eqNotifyNewClass( Node n ) { + Trace("rels-std") << "[sets-rels] eqNotifyNewClass:" << " t = " << n << std::endl; + if(n.getKind() == kind::TRANSPOSE || n.getKind() == kind::PRODUCT || n.getKind() == kind::TCLOSURE) { + getOrMakeEqcInfo( n, true ); + if( n.getKind() == kind::TCLOSURE ) { + Node relRep_of_tc = getRepresentative( n[0] ); + EqcInfo* rel_ei = getOrMakeEqcInfo( relRep_of_tc, true ); + + if( rel_ei->d_rel_tc.get().isNull() ) { + rel_ei->d_rel_tc = n; + Node exp = relRep_of_tc == n[0] ? d_trueNode : NodeManager::currentNM()->mkNode( kind::EQUAL, relRep_of_tc, n[0] ); + for( NodeSet::const_iterator mem_it = rel_ei->d_mem.begin(); mem_it != rel_ei->d_mem.end(); mem_it++ ) { + Node mem_exp = (*rel_ei->d_mem_exp.find(*mem_it)).second; + exp = NodeManager::currentNM()->mkNode( kind::AND, exp, mem_exp); + if( mem_exp[1] != relRep_of_tc ) { + exp = NodeManager::currentNM()->mkNode( kind::AND, exp, NodeManager::currentNM()->mkNode(kind::EQUAL, relRep_of_tc, mem_exp[1] ) ); } - return NodeManager::currentNM()->mkNode(kind::AND, exp, (*rel_mem_exp_it).second); + sendMergeInfer( NodeManager::currentNM()->mkNode(kind::MEMBER, mem_exp[0], n), exp, "TCLOSURE-UP I" ); } - ++rel_mem_exp_it; } } } - Trace("rels-tc") << "End explainTCMem ############ pair = " << pair << std::endl; - return Node::null(); - } - - void TheorySetsRels::sendTCInference(EqcInfo* tc_ei, std::hash_set in_reachable, std::hash_set out_reachable, Node mem_rep, Node fst_rep, Node snd_rep, int id1, int id2) { - Trace("rels-std") << "Start making TC inference after adding a member " << mem_rep << " to " << tc_ei->d_tc.get() << std::endl; - - Node exp = explainTCMem(tc_ei, mem_rep, fst_rep, snd_rep); - Assert(!exp.isNull()); - sendMergeInfer(NodeManager::currentNM()->mkNode(kind::MEMBER, mem_rep, tc_ei->d_tc.get()), exp, "TC-Infer"); - std::hash_set::iterator in_reachable_it = in_reachable.begin(); - - while(in_reachable_it != in_reachable.end()) { - Node in_node = d_id_node[*in_reachable_it]; - Node in_pair = RelsUtils::constructPair(tc_ei->d_tc.get(), in_node, fst_rep); - Node new_pair = RelsUtils::constructPair(tc_ei->d_tc.get(), in_node, snd_rep); - Node tc_exp = explainTCMem(tc_ei, in_pair, in_node, fst_rep); - Node reason = tc_exp.isNull() ? exp : NodeManager::currentNM()->mkNode(kind::AND,tc_exp, exp); - - tc_ei->d_mem_exp[new_pair] = reason; - tc_ei->d_mem.insert(new_pair); - sendMergeInfer(NodeManager::currentNM()->mkNode(kind::MEMBER, new_pair, tc_ei->d_tc.get()), reason, "TC-Infer"); - in_reachable_it++; - } - - std::hash_set::iterator out_reachable_it = out_reachable.begin(); - while(out_reachable_it != out_reachable.end()) { - Node out_node = d_id_node[*out_reachable_it]; - Node out_pair = RelsUtils::constructPair(tc_ei->d_tc.get(), snd_rep, out_node); - Node reason = explainTCMem(tc_ei, out_pair, snd_rep, out_node); - Assert(reason != Node::null()); - - std::hash_set::iterator in_reachable_it = in_reachable.begin(); - - while(in_reachable_it != in_reachable.end()) { - Node in_node = d_id_node[*in_reachable_it]; - Node in_pair = RelsUtils::constructPair(tc_ei->d_tc.get(), in_node, snd_rep); - Node new_pair = RelsUtils::constructPair(tc_ei->d_tc.get(), in_node, out_node); - Node in_pair_exp = explainTCMem(tc_ei, in_pair, in_node, snd_rep); - - Assert(in_pair_exp != Node::null()); - reason = NodeManager::currentNM()->mkNode(kind::AND,reason, in_pair_exp); - tc_ei->d_mem_exp[new_pair] = reason; - tc_ei->d_mem.insert(new_pair); - sendMergeInfer(NodeManager::currentNM()->mkNode(kind::MEMBER, new_pair, tc_ei->d_tc.get()), reason, "TC-Infer"); - in_reachable_it++; - } - out_reachable_it++; - } - } - - void TheorySetsRels::collectReachableNodes(std::map< int, std::vector< int > >& id_map, int start_id, std::hash_set< int >& reachable_set, bool firstRound) { - Trace("rels-std") << "**** Collecting reachable nodes for node with id " << start_id << std::endl; - if(reachable_set.find(start_id) != reachable_set.end()) { - return; - } - if(!firstRound) { - reachable_set.insert(start_id); - } - - std::vector< int > id_list = getIdList(id_map, start_id); - std::vector< int >::iterator id_list_it = id_list.begin(); - - while( id_list_it != id_list.end() ) { - collectReachableNodes( id_map, *id_list_it, reachable_set, false ); - id_list_it++; - } - } - - void TheorySetsRels::eqNotifyNewClass( Node n ) { - Trace("rels-std") << "[sets-rels] eqNotifyNewClass:" << " t = " << n << std::endl; - if(isRel(n) && (n.getKind() == kind::TRANSPOSE || - n.getKind() == kind::PRODUCT || - n.getKind() == kind::JOIN || - n.getKind() == kind::TCLOSURE)) { - getOrMakeEqcInfo( n, true ); - } } // Merge t2 into t1, t1 will be the rep of the new eqc void TheorySetsRels::eqNotifyPostMerge( Node t1, Node t2 ) { - Trace("rels-std") << "[sets-rels] eqNotifyPostMerge:" << " t1 = " << t1 << " t2 = " << t2 << std::endl; - - // Merge membership constraint with "true" or "false" eqc - if( (t1 == d_trueNode || t1 == d_falseNode) && t2.getKind() == kind::MEMBER && t2[0].getType().isTuple() ) { + Trace("rels-std") << "[sets-rels-std] eqNotifyPostMerge:" << " t1 = " << t1 << " t2 = " << t2 << std::endl; + + // Merge membership constraint with "true" eqc + if( t1 == d_trueNode && t2.getKind() == kind::MEMBER && t2[0].getType().isTuple() ) { + Node mem_rep = getRepresentative( t2[0] ); + Node t2_1rep = getRepresentative( t2[1] ); + EqcInfo* ei = getOrMakeEqcInfo( t2_1rep, true ); + if(ei->d_mem.contains(mem_rep)) { + return; + } + Node exp = t2; - Assert(t1 == d_trueNode || t1 == d_falseNode); - bool polarity = t1 == d_trueNode; - Node t2_1rep = getRepresentative(t2[1]); - EqcInfo* ei = getOrMakeEqcInfo( t2_1rep, true ); + ei->d_mem.insert( mem_rep ); + ei->d_mem_exp.insert( mem_rep, exp ); - if( polarity ) { - ei->d_mem.insert(t2[0]); - ei->d_mem_exp[t2[0]] = explain(t2); - } // Process a membership constraint that a tuple is a member of transpose of rel if( !ei->d_tp.get().isNull() ) { - Node exp = polarity ? explain(t2) : explain(t2.negate()); - if(ei->d_tp.get() != t2[1]) { - exp = NodeManager::currentNM()->mkNode(kind::AND, explain(NodeManager::currentNM()->mkNode(kind::EQUAL, ei->d_tp.get(), t2[1]) ), exp ); + if( ei->d_tp.get() != t2[1] ) { + exp = NodeManager::currentNM()->mkNode(kind::AND, NodeManager::currentNM()->mkNode(kind::EQUAL, ei->d_tp.get(), t2[1]), t2 ); } - sendInferTranspose( polarity, t2[0], ei->d_tp.get(), exp, true ); + sendInferTranspose( t2[0], ei->d_tp.get(), exp ); } // Process a membership constraint that a tuple is a member of product of rel if( !ei->d_pt.get().isNull() ) { - Node exp = polarity ? explain(t2) : explain(t2.negate()); - if(ei->d_pt.get() != t2[1]) { - exp = NodeManager::currentNM()->mkNode(kind::AND, explain(NodeManager::currentNM()->mkNode(kind::EQUAL, ei->d_pt.get(), t2[1]) ), exp ); + if( ei->d_pt.get() != t2[1] ) { + exp = NodeManager::currentNM()->mkNode(kind::AND, NodeManager::currentNM()->mkNode(kind::EQUAL, ei->d_pt.get(), t2[1]), t2 ); } - sendInferProduct( polarity, t2[0], ei->d_pt.get(), exp ); + sendInferProduct( t2[0], ei->d_pt.get(), exp ); + } + + if( !ei->d_rel_tc.get().isNull() ) { + if( ei->d_rel_tc.get()[0] != t2[1] ) { + exp = NodeManager::currentNM()->mkNode(kind::AND, NodeManager::currentNM()->mkNode(kind::EQUAL, ei->d_rel_tc.get()[0], t2[1]), t2 ); + } + sendMergeInfer(NodeManager::currentNM()->mkNode(kind::MEMBER, t2[0], ei->d_rel_tc.get()), exp, "TCLOSURE-UP I"); } // Process a membership constraint that a tuple is a member of transitive closure of rel - if( polarity && !ei->d_tc.get().isNull() ) { - addTCMemAndSendInfer( ei, t2, Node::null() ); + if( !ei->d_tc.get().isNull() ) { + sendInferTClosure( t2, ei ); } // Merge two relation eqcs } else if( t1.getType().isSet() && t2.getType().isSet() && t1.getType().getSetElementType().isTuple() ) { - mergeTransposeEqcs(t1, t2); - mergeProductEqcs(t1, t2); - mergeTCEqcs(t1, t2); - } + EqcInfo* t1_ei = getOrMakeEqcInfo( t1 ); + EqcInfo* t2_ei = getOrMakeEqcInfo( t2 ); - Trace("rels-std") << "[sets-rels] done with eqNotifyPostMerge:" << " t1 = " << t1 << " t2 = " << t2 << std::endl; - } - - void TheorySetsRels::mergeTCEqcs(Node t1, Node t2) { - Trace("rels-std") << "[sets-rels] Merge TC eqcs t1 = " << t1 << " and t2 = " << t2 << std::endl; - - EqcInfo* t1_ei = getOrMakeEqcInfo(t1); - EqcInfo* t2_ei = getOrMakeEqcInfo(t2); - - if(t1_ei != NULL && t2_ei != NULL) { - if(!t1_ei->d_tc.get().isNull()) { - NodeSet::const_iterator mem_it = t2_ei->d_mem.begin(); - while(mem_it != t2_ei->d_mem.end()) { - addTCMemAndSendInfer(t1_ei, NodeManager::currentNM()->mkNode(kind::MEMBER,*mem_it, t1_ei->d_tc.get()), (*t2_ei->d_mem_exp.find(*mem_it)).second); - mem_it++; + if( t1_ei != NULL && t2_ei != NULL ) { + if( !t1_ei->d_tp.get().isNull() && !t2_ei->d_tp.get().isNull() ) { + sendInferTranspose(t1_ei->d_tp.get(), t2_ei->d_tp.get(), NodeManager::currentNM()->mkNode(kind::EQUAL, t1_ei->d_tp.get(), t2_ei->d_tp.get() ) ); } - } else if(!t2_ei->d_tc.get().isNull()) { - t1_ei->d_tc.set(t2_ei->d_tc); - NodeSet::const_iterator t1_mem_it = t1_ei->d_mem.begin(); - - while(t1_mem_it != t1_ei->d_mem.end()) { - NodeMap::const_iterator reason_it = t1_ei->d_mem_exp.find(*t1_mem_it); - Assert(reason_it != t1_ei->d_mem_exp.end()); - addTCMemAndSendInfer(t1_ei, NodeManager::currentNM()->mkNode(kind::MEMBER,*t1_mem_it, t1_ei->d_tc.get()), (*reason_it).second); - t1_mem_it++; - } - - NodeSet::const_iterator t2_mem_it = t2_ei->d_mem.begin(); - - while(t2_mem_it != t2_ei->d_mem.end()) { - addTCMemAndSendInfer(t1_ei, NodeManager::currentNM()->mkNode(kind::MEMBER,*t2_mem_it, t2_ei->d_tc.get()), (*t2_ei->d_mem_exp.find(*t2_mem_it)).second); - t2_mem_it++; + std::vector< Node > t2_new_mems; + std::vector< Node > t2_new_exps; + NodeSet::const_iterator t2_mem_it = t2_ei->d_mem.begin(); + NodeSet::const_iterator t1_mem_it = t1_ei->d_mem.begin(); + + for( ; t2_mem_it != t2_ei->d_mem.end(); t2_mem_it++ ) { + if( !t1_ei->d_mem.contains( *t2_mem_it ) ) { + Node t2_mem_exp = (*t2_ei->d_mem_exp.find(*t2_mem_it)).second; + + if( t2_ei->d_tp.get().isNull() && !t1_ei->d_tp.get().isNull() ) { + Node reason = t1_ei->d_tp.get() == (t2_mem_exp)[1] + ? (t2_mem_exp) : NodeManager::currentNM()->mkNode(kind::AND, t2_mem_exp, NodeManager::currentNM()->mkNode(kind::EQUAL, (t2_mem_exp)[1], t1_ei->d_tp.get())); + sendInferTranspose( t2_mem_exp[0], t1_ei->d_tp.get(), reason ); + } + if( t2_ei->d_pt.get().isNull() && !t1_ei->d_pt.get().isNull() ) { + Node reason = t1_ei->d_pt.get() == (t2_mem_exp)[1] + ? (t2_mem_exp) : NodeManager::currentNM()->mkNode(kind::AND, t2_mem_exp, NodeManager::currentNM()->mkNode(kind::EQUAL, (t2_mem_exp)[1], t1_ei->d_pt.get())); + sendInferProduct( t2_mem_exp[0], t1_ei->d_pt.get(), reason ); + } + if( t2_ei->d_tc.get().isNull() && !t1_ei->d_tc.get().isNull() ) { + sendInferTClosure( t2_mem_exp, t1_ei ); + } + if( t2_ei->d_rel_tc.get().isNull() && !t1_ei->d_rel_tc.get().isNull() ) { + Node reason = t1_ei->d_rel_tc.get()[0] == t2_mem_exp[1] ? + t2_mem_exp : NodeManager::currentNM()->mkNode(kind::AND, NodeManager::currentNM()->mkNode(kind::EQUAL, t1_ei->d_rel_tc.get()[0], t2_mem_exp[1]), t2_mem_exp ); + sendMergeInfer(NodeManager::currentNM()->mkNode(kind::MEMBER, t2_mem_exp[0], t1_ei->d_rel_tc.get()), reason, "TCLOSURE-UP I"); + } + t2_new_mems.push_back( *t2_mem_it ); + t2_new_exps.push_back( t2_mem_exp ); + } } - } - } - Trace("rels-std") << "[sets-rels] Done with merging TC eqcs t1 = " << t1 << " and t2 = " << t2 << std::endl; - } - - - - - void TheorySetsRels::mergeProductEqcs(Node t1, Node t2) { - Trace("rels-std") << "[sets-rels] Merge PRODUCT eqcs t1 = " << t1 << " and t2 = " << t2 << std::endl; - EqcInfo* t1_ei = getOrMakeEqcInfo(t1); - EqcInfo* t2_ei = getOrMakeEqcInfo(t2); - - if(t1_ei != NULL && t2_ei != NULL) { - // Apply Product rule on (non)members of t2 and t1->pt - if(!t1_ei->d_pt.get().isNull()) { - for(NodeSet::key_iterator itr = t2_ei->d_mem.key_begin(); itr != t2_ei->d_mem.key_end(); itr++) { - if(!t1_ei->d_mem.contains(*itr)) { - sendInferProduct( true, *itr, t1_ei->d_pt.get(), NodeManager::currentNM()->mkNode(kind::AND,explain(NodeManager::currentNM()->mkNode(kind::EQUAL,t1_ei->d_pt.get(), t2)), explain(NodeManager::currentNM()->mkNode(kind::MEMBER,*itr, t2))) ); + for( ; t1_mem_it != t1_ei->d_mem.end(); t1_mem_it++ ) { + if( !t2_ei->d_mem.contains( *t1_mem_it ) ) { + Node t1_mem_exp = (*t1_ei->d_mem_exp.find(*t1_mem_it)).second; + if( t1_ei->d_tp.get().isNull() && !t2_ei->d_tp.get().isNull() ) { + Node reason = t2_ei->d_tp.get() == (t1_mem_exp)[1] + ? (t1_mem_exp) : NodeManager::currentNM()->mkNode(kind::AND, t1_mem_exp, NodeManager::currentNM()->mkNode(kind::EQUAL, (t1_mem_exp)[1], t2_ei->d_tp.get())); + sendInferTranspose( (t1_mem_exp)[0], t2_ei->d_tp.get(), reason ); + } + if( t1_ei->d_pt.get().isNull() && !t2_ei->d_pt.get().isNull() ) { + Node reason = t2_ei->d_pt.get() == (t1_mem_exp)[1] + ? (t1_mem_exp) : NodeManager::currentNM()->mkNode(kind::AND, t1_mem_exp, NodeManager::currentNM()->mkNode(kind::EQUAL, (t1_mem_exp)[1], t2_ei->d_pt.get())); + sendInferProduct( (t1_mem_exp)[0], t2_ei->d_pt.get(), reason ); + } + if( t1_ei->d_tc.get().isNull() && !t2_ei->d_tc.get().isNull() ) { + sendInferTClosure(t1_mem_exp, t2_ei ); + } + if( t1_ei->d_rel_tc.get().isNull() && !t2_ei->d_rel_tc.get().isNull() ) { + Node reason = t2_ei->d_rel_tc.get()[0] == t1_mem_exp[1] ? + t1_mem_exp : NodeManager::currentNM()->mkNode(kind::AND, NodeManager::currentNM()->mkNode(kind::EQUAL, t2_ei->d_rel_tc.get()[0], t1_mem_exp[1]), t1_mem_exp ); + sendMergeInfer(NodeManager::currentNM()->mkNode(kind::MEMBER, t1_mem_exp[0], t2_ei->d_rel_tc.get()), reason, "TCLOSURE-UP I"); + } } } - } else if(!t2_ei->d_pt.get().isNull()) { - t1_ei->d_pt.set(t2_ei->d_pt); - for(NodeSet::key_iterator itr = t1_ei->d_mem.key_begin(); itr != t1_ei->d_mem.key_end(); itr++) { - if(!t2_ei->d_mem.contains(*itr)) { - sendInferProduct( true, *itr, t2_ei->d_pt.get(), NodeManager::currentNM()->mkNode(kind::AND,explain(NodeManager::currentNM()->mkNode(kind::EQUAL,t1, t2_ei->d_pt.get())), explain(NodeManager::currentNM()->mkNode(kind::MEMBER,*itr, t1))) ); + std::vector< Node >::iterator t2_new_mem_it = t2_new_mems.begin(); + std::vector< Node >::iterator t2_new_exp_it = t2_new_exps.begin(); + for( ; t2_new_mem_it != t2_new_mems.end(); t2_new_mem_it++, t2_new_exp_it++ ) { + t1_ei->d_mem.insert( *t2_new_mem_it ); + t1_ei->d_mem_exp.insert( *t2_new_mem_it, *t2_new_exp_it ); + } + if( t1_ei->d_tp.get().isNull() && !t2_ei->d_tp.get().isNull() ) { + t1_ei->d_tp.set(t2_ei->d_tp.get()); + } + if( t1_ei->d_pt.get().isNull() && !t2_ei->d_pt.get().isNull() ) { + t1_ei->d_pt.set(t2_ei->d_pt.get()); + } + if( t1_ei->d_tc.get().isNull() && !t2_ei->d_tc.get().isNull() ) { + t1_ei->d_tc.set(t2_ei->d_tc.get()); + } + if( t1_ei->d_rel_tc.get().isNull() && !t2_ei->d_rel_tc.get().isNull() ) { + t1_ei->d_rel_tc.set(t2_ei->d_rel_tc.get()); + } + } else if( t1_ei != NULL ) { + if( (t2.getKind() == kind::TRANSPOSE && t1_ei->d_tp.get().isNull()) || + (t2.getKind() == kind::PRODUCT && t1_ei->d_pt.get().isNull()) || + (t2.getKind() == kind::TCLOSURE && t1_ei->d_tc.get().isNull()) ) { + NodeSet::const_iterator t1_mem_it = t1_ei->d_mem.begin(); + + if( t2.getKind() == kind::TRANSPOSE ) { + t1_ei->d_tp = t2; + } else if( t2.getKind() == kind::PRODUCT ) { + t1_ei->d_pt = t2; + } else if( t2.getKind() == kind::TCLOSURE ) { + t1_ei->d_tc = t2; + } + for( ; t1_mem_it != t1_ei->d_mem.end(); t1_mem_it++ ) { + Node t1_exp = (*t1_ei->d_mem_exp.find(*t1_mem_it)).second; + if( t2.getKind() == kind::TRANSPOSE ) { + Node reason = t2 == t1_exp[1] + ? (t1_exp) : NodeManager::currentNM()->mkNode(kind::AND, (t1_exp), NodeManager::currentNM()->mkNode(kind::EQUAL, (t1_exp)[1], t2)); + sendInferTranspose( (t1_exp)[0], t2, reason ); + } else if( t2.getKind() == kind::PRODUCT ) { + Node reason = t2 == (t1_exp)[1] + ? (t1_exp) : NodeManager::currentNM()->mkNode(kind::AND, (t1_exp), NodeManager::currentNM()->mkNode(kind::EQUAL, (t1_exp)[1], t2)); + sendInferProduct( (t1_exp)[0], t2, reason ); + } else if( t2.getKind() == kind::TCLOSURE ) { + sendInferTClosure( t1_exp, t1_ei ); + } } } - } - // t1 was created already and t2 was not - } else if(t1_ei != NULL) { - if(t1_ei->d_pt.get().isNull() && t2.getKind() == kind::PRODUCT) { - t1_ei->d_pt.set( t2 ); - } - } else if(t2_ei != NULL){ - t1_ei = getOrMakeEqcInfo(t1, true); - if(t1_ei->d_pt.get().isNull() && !t2_ei->d_pt.get().isNull()) { - t1_ei->d_pt.set(t2_ei->d_pt); - for(NodeSet::key_iterator itr = t2_ei->d_mem.key_begin(); itr != t2_ei->d_mem.key_end(); itr++) { - t1_ei->d_mem.insert(*itr); - t1_ei->d_mem_exp.insert(*itr, t2_ei->d_mem_exp[*itr]); + } else if( t2_ei != NULL ) { + EqcInfo* new_t1_ei = getOrMakeEqcInfo( t1, true ); + if( new_t1_ei->d_tp.get().isNull() && !t2_ei->d_tp.get().isNull() ) { + new_t1_ei->d_tp.set(t2_ei->d_tp.get()); + } + if( new_t1_ei->d_pt.get().isNull() && !t2_ei->d_pt.get().isNull() ) { + new_t1_ei->d_pt.set(t2_ei->d_pt.get()); + } + if( new_t1_ei->d_tc.get().isNull() && !t2_ei->d_tc.get().isNull() ) { + new_t1_ei->d_tc.set(t2_ei->d_tc.get()); + } + if( new_t1_ei->d_rel_tc.get().isNull() && !t2_ei->d_rel_tc.get().isNull() ) { + new_t1_ei->d_rel_tc.set(t2_ei->d_rel_tc.get()); + } + if( (t1.getKind() == kind::TRANSPOSE && t2_ei->d_tp.get().isNull()) || + (t1.getKind() == kind::PRODUCT && t2_ei->d_pt.get().isNull()) || + (t1.getKind() == kind::TCLOSURE && t2_ei->d_tc.get().isNull()) ) { + NodeSet::const_iterator t2_mem_it = t2_ei->d_mem.begin(); + + for( ; t2_mem_it != t2_ei->d_mem.end(); t2_mem_it++ ) { + Node t2_exp = (*t1_ei->d_mem_exp.find(*t2_mem_it)).second; + + if( t1.getKind() == kind::TRANSPOSE ) { + Node reason = t1 == (t2_exp)[1] + ? (t2_exp) : NodeManager::currentNM()->mkNode(kind::AND, (t2_exp), NodeManager::currentNM()->mkNode(kind::EQUAL, (t2_exp)[1], t1)); + sendInferTranspose( (t2_exp)[0], t1, reason ); + } else if( t1.getKind() == kind::PRODUCT ) { + Node reason = t1 == (t2_exp)[1] + ? (t2_exp) : NodeManager::currentNM()->mkNode(kind::AND, (t2_exp), NodeManager::currentNM()->mkNode(kind::EQUAL, (t2_exp)[1], t1)); + sendInferProduct( (t2_exp)[0], t1, reason ); + } else if( t1.getKind() == kind::TCLOSURE ) { + sendInferTClosure( t2_exp, new_t1_ei ); + } + } } } } - } - void TheorySetsRels::mergeTransposeEqcs( Node t1, Node t2 ) { - Trace("rels-std") << "[sets-rels] Merge TRANSPOSE eqcs t1 = " << t1 << " and t2 = " << t2 << std::endl; - EqcInfo* t1_ei = getOrMakeEqcInfo( t1 ); - EqcInfo* t2_ei = getOrMakeEqcInfo( t2 ); + Trace("rels-std") << "[sets-rels] done with eqNotifyPostMerge:" << " t1 = " << t1 << " t2 = " << t2 << std::endl; + } - if( t1_ei != NULL && t2_ei != NULL ) { - Trace("rels-std") << "[sets-rels] 0 Merge TRANSPOSE eqcs t1 = " << t1 << " and t2 = " << t2 << std::endl; - // TP(t1) = TP(t2) -> t1 = t2; - if( !t1_ei->d_tp.get().isNull() && !t2_ei->d_tp.get().isNull() ) { - sendInferTranspose( true, t1_ei->d_tp.get(), t2_ei->d_tp.get(), explain(NodeManager::currentNM()->mkNode(kind::EQUAL,t1, t2)) ); + void TheorySetsRels::sendInferTClosure( Node new_mem_exp, EqcInfo* ei ) { + NodeSet::const_iterator mem_it = ei->d_mem.begin(); + Node mem_rep = getRepresentative( new_mem_exp[0] ); + Node new_mem_rel = new_mem_exp[1]; + Node new_mem_fst = RelsUtils::nthElementOfTuple( new_mem_exp[0], 0 ); + Node new_mem_snd = RelsUtils::nthElementOfTuple( new_mem_exp[0], 1 ); + for( ; mem_it != ei->d_mem.end(); mem_it++ ) { + if( *mem_it == mem_rep ) { + continue; } - // Apply transpose rule on (non)members of t2 and t1->tp - if( !t1_ei->d_tp.get().isNull() ) { - for( NodeSet::key_iterator itr = t2_ei->d_mem.key_begin(); itr != t2_ei->d_mem.key_end(); itr++ ) { - if( !t1_ei->d_mem.contains( *itr ) ) { - sendInferTranspose( true, *itr, t1_ei->d_tp.get(), NodeManager::currentNM()->mkNode(kind::AND, explain(NodeManager::currentNM()->mkNode(kind::EQUAL,t1_ei->d_tp.get(), t2)), explain(NodeManager::currentNM()->mkNode(kind::MEMBER,*itr, t2))) ); - } + Node d_mem_exp = (*ei->d_mem_exp.find(*mem_it)).second; + Node d_mem_fst = RelsUtils::nthElementOfTuple( d_mem_exp[0], 0 ); + Node d_mem_snd = RelsUtils::nthElementOfTuple( d_mem_exp[0], 1 ); + Node d_mem_rel = d_mem_exp[1]; + if( areEqual( new_mem_fst, d_mem_snd) ) { + Node reason = NodeManager::currentNM()->mkNode( kind::AND, new_mem_exp, d_mem_exp ); + reason = NodeManager::currentNM()->mkNode( kind::AND, reason, NodeManager::currentNM()->mkNode(kind::EQUAL, new_mem_fst, d_mem_snd ) ); + if( new_mem_rel != ei->d_tc.get() ) { + reason = NodeManager::currentNM()->mkNode( kind::AND, reason, NodeManager::currentNM()->mkNode(kind::EQUAL, new_mem_rel, ei->d_tc.get() ) ); } - // Apply transpose rule on members of t1 and t2->tp - } else if( !t2_ei->d_tp.get().isNull() ) { - t1_ei->d_tp.set( t2_ei->d_tp ); - for( NodeSet::key_iterator itr = t1_ei->d_mem.key_begin(); itr != t1_ei->d_mem.key_end(); itr++ ) { - if( !t2_ei->d_mem.contains(*itr) ) { - sendInferTranspose( true, *itr, t2_ei->d_tp.get(), NodeManager::currentNM()->mkNode(kind::AND, explain(NodeManager::currentNM()->mkNode(kind::EQUAL,t1, t2_ei->d_tp.get())), explain(NodeManager::currentNM()->mkNode(kind::MEMBER,*itr, t1))) ); - } + if( d_mem_rel != ei->d_tc.get() ) { + reason = NodeManager::currentNM()->mkNode( kind::AND, reason, NodeManager::currentNM()->mkNode(kind::EQUAL, d_mem_rel, ei->d_tc.get() ) ); } + Node new_membership = NodeManager::currentNM()->mkNode( kind::MEMBER, RelsUtils::constructPair( d_mem_rel, d_mem_fst, new_mem_snd ), ei->d_tc.get() ); + sendMergeInfer( new_membership, reason, "TCLOSURE-UP II" ); } - // t1 was created already and t2 was not - } else if(t1_ei != NULL) { - if( t1_ei->d_tp.get().isNull() && t2.getKind() == kind::TRANSPOSE ) { - t1_ei->d_tp.set( t2 ); - } - } else if( t2_ei != NULL ){ - t1_ei = getOrMakeEqcInfo( t1, true ); - if( t1_ei->d_tp.get().isNull() && !t2_ei->d_tp.get().isNull() ) { - t1_ei->d_tp.set( t2_ei->d_tp ); - for( NodeSet::key_iterator itr = t2_ei->d_mem.key_begin(); itr != t2_ei->d_mem.key_end(); itr++ ) { - t1_ei->d_mem.insert( *itr ); - t1_ei->d_mem_exp.insert( *itr, t2_ei->d_mem_exp[*itr] ); + if( areEqual( new_mem_snd, d_mem_fst ) ) { + Node reason = NodeManager::currentNM()->mkNode( kind::AND, new_mem_exp, d_mem_exp ); + reason = NodeManager::currentNM()->mkNode( kind::AND, reason, NodeManager::currentNM()->mkNode(kind::EQUAL, new_mem_snd, d_mem_fst ) ); + if( new_mem_rel != ei->d_tc.get() ) { + reason = NodeManager::currentNM()->mkNode( kind::AND, reason, NodeManager::currentNM()->mkNode(kind::EQUAL, new_mem_rel, ei->d_tc.get() ) ); } + if( d_mem_rel != ei->d_tc.get() ) { + reason = NodeManager::currentNM()->mkNode( kind::AND, reason, NodeManager::currentNM()->mkNode(kind::EQUAL, d_mem_rel, ei->d_tc.get() ) ); + } + Node new_membership = NodeManager::currentNM()->mkNode( kind::MEMBER, RelsUtils::constructPair( d_mem_rel, new_mem_fst, d_mem_snd ), ei->d_tc.get() ); + sendMergeInfer( new_membership, reason, "TCLOSURE-UP II" ); } } } + void TheorySetsRels::doPendingMerge() { for( NodeList::const_iterator itr = d_pending_merge.begin(); itr != d_pending_merge.end(); itr++ ) { if( !holds(*itr) ) { if( d_lemmas_produced.find(*itr)==d_lemmas_produced.end() ) { - Trace("rels-lemma") << "[std-sets-rels-lemma] Send out a merge fact as lemma: " + Trace("rels-std-lemma") << "[std-sets-rels-lemma] Send out a merge fact as lemma: " << *itr << std::endl; d_sets_theory.d_out->lemma( *itr ); d_lemmas_produced.insert(*itr); @@ -1495,41 +1359,31 @@ int TheorySetsRels::EqcInfo::counter = 0; } } - void TheorySetsRels::sendInferTranspose( bool polarity, Node t1, Node t2, Node exp, bool reverseOnly ) { + // t1 and t2 can be both relations + // or t1 is a tuple, t2 is a transposed relation + void TheorySetsRels::sendInferTranspose( Node t1, Node t2, Node exp ) { Assert( t2.getKind() == kind::TRANSPOSE ); - if( !polarity ) { - return; - } - if( polarity && isRel(t1) && isRel(t2) ) { + + if( isRel(t1) && isRel(t2) ) { Assert(t1.getKind() == kind::TRANSPOSE); sendMergeInfer(NodeManager::currentNM()->mkNode(kind::EQUAL, t1[0], t2[0]), exp, "Transpose-Equal"); return; } - - if( reverseOnly ) { - sendMergeInfer( NodeManager::currentNM()->mkNode(kind::MEMBER, RelsUtils::reverseTuple(t1), t2[0]), exp, "Transpose-Rule" ); - } else { - sendMergeInfer(NodeManager::currentNM()->mkNode(kind::MEMBER, t1, t2), exp, "Transpose-Rule"); - sendMergeInfer(NodeManager::currentNM()->mkNode(kind::MEMBER, RelsUtils::reverseTuple(t1), t2[0]), exp, "Transpose-Rule"); - } + sendMergeInfer(NodeManager::currentNM()->mkNode(kind::MEMBER, RelsUtils::reverseTuple(t1), t2[0]), exp, "Transpose-Rule"); } void TheorySetsRels::sendMergeInfer( Node fact, Node reason, const char * c ) { if( !holds( fact ) ) { Node lemma = NodeManager::currentNM()->mkNode( kind::IMPLIES, reason, fact); d_pending_merge.push_back(lemma); - Trace("std-rels") << "[std-rels-lemma] Generate a lemma by applying " << c + Trace("rels-std") << "[std-rels-lemma] Generate a lemma by applying " << c << ": " << lemma << std::endl; } } - void TheorySetsRels::sendInferProduct( bool polarity, Node member, Node pt_rel, Node exp ) { + void TheorySetsRels::sendInferProduct( Node member, Node pt_rel, Node exp ) { Assert( pt_rel.getKind() == kind::PRODUCT ); - if(!polarity) { - return; - } - std::vector r1_element; std::vector r2_element; Node r1 = pt_rel[0]; @@ -1573,8 +1427,6 @@ int TheorySetsRels::EqcInfo::counter = 0; ei->d_pt = n; } else if( n.getKind() == kind::TCLOSURE ) { ei->d_tc = n; - } else if( n.getKind() == kind::JOIN ) { - ei->d_join = n; } return ei; }else{ @@ -1628,35 +1480,6 @@ int TheorySetsRels::EqcInfo::counter = 0; } } - bool TheorySetsRels::addId( std::map< int, std::vector< int > >& id_map, int key, int id ) { - int n_data = d_vec_size[key]; - int len = n_data < (int)id_map[key].size() ? n_data : id_map[key].size(); - - for( int i = 0; i < len; i++ ) { - if( id_map[key][i] == id) { - return false; - } - } - if( n_data < (int)id_map[key].size() ) { - id_map[key][n_data] = id; - } else { - id_map[key].push_back( id ); - } - d_vec_size[key] = n_data+1; - return true; - } - - std::vector< int > TheorySetsRels::getIdList( std::map< int, std::vector< int > >& id_map, int key ) { - std::vector< int > id_list; - int n_data = d_vec_size[key]; - int len = n_data < (int)id_map[key].size() ? n_data : id_map[key].size(); - - for( int i = 0; i < len; i++ ) { - id_list.push_back(id_map[key][i]); - } - return id_list; - } - } } } diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h index 65a1c4164..fed808de4 100644 --- a/src/theory/sets/theory_sets_rels.h +++ b/src/theory/sets/theory_sets_rels.h @@ -79,43 +79,19 @@ private: public: EqcInfo( context::Context* c ); ~EqcInfo(){} - static int counter; NodeSet d_mem; NodeMap d_mem_exp; - NodeListMap d_in; - NodeListMap d_out; context::CDO< Node > d_tp; context::CDO< Node > d_pt; - context::CDO< Node > d_join; context::CDO< Node > d_tc; - /** mapping from an element rep id to a list of rep ids that pointed by */ - /** Context dependent map Int -> IntList */ - std::map< int, std::vector< int > > d_id_inIds; - /** mapping from an element rep id to a list of rep ids that point to */ - /** Context dependent map Int -> IntList */ - std::map< int, std::vector< int > > d_id_outIds; + context::CDO< Node > d_rel_tc; }; private: - /** Context */ - context::CDHashMap< int, int > d_vec_size; - - /** Mapping between integer id and tuple element rep */ - std::map< int, Node > d_id_node; - - /** Mapping between tuple element rep and integer id*/ - std::map< Node, int > d_node_id; /** has eqc info */ bool hasEqcInfo( TNode n ) { return d_eqc_info.find( n )!=d_eqc_info.end(); } - bool addId( std::map< int, std::vector< int > >& id_map, int key, int id ); - std::vector< int > getIdList( std::map< int, std::vector< int > >& id_map, int key ); - - void collectReachableNodes( std::map< int, std::vector< int > >&, int, std::hash_set& , bool first_round = true); - - -private: eq::EqualityEngine *d_eqEngine; context::CDO *d_conflict; TheorySets& d_sets_theory; @@ -179,30 +155,22 @@ private: std::map< Node, EqcInfo* > d_eqc_info; public: + /** Standard effort notifications */ void eqNotifyNewClass(Node t); void eqNotifyPostMerge(Node t1, Node t2); private: + /** Methods used in standard effort */ void doPendingMerge(); - Node findTCMemExp(EqcInfo*, Node); - void buildTCAndExp(Node, EqcInfo*); - void mergeTCEqcs(Node t1, Node t2); - void mergeTCEqcExp(EqcInfo*, EqcInfo*); - void mergeProductEqcs(Node t1, Node t2); - int getOrMakeElementRepId(EqcInfo*, Node); - void mergeTransposeEqcs(Node t1, Node t2); - Node explainTCMem(EqcInfo*, Node, Node, Node); - void sendInferProduct(bool, Node, Node, Node); + void sendInferProduct(Node member, Node pt_rel, Node exp); + void sendInferTranspose(Node t1, Node t2, Node exp ); + void sendInferTClosure( Node mem_rep, EqcInfo* ei ); + void sendMergeInfer( Node fact, Node reason, const char * c ); EqcInfo* getOrMakeEqcInfo( Node n, bool doMake = false ); - void sendInferTranspose(bool, Node, Node, Node, bool reverseOnly = false); - void addTCMemAndSendInfer(EqcInfo* tc_ei, Node mem, Node exp, bool fromRel = false); - void sendTCInference(EqcInfo* tc_ei, std::hash_set in_reachable, std::hash_set out_reachable, Node mem_rep, Node fst_rep, Node snd_rep, int id1, int id2); - - + /** Methods used in full effort */ void check(); - Node explain(Node); void collectRelsInfo(); void applyTransposeRule( std::vector tp_terms ); void applyTransposeRule( Node rel, Node rel_rep, Node exp ); @@ -227,10 +195,9 @@ private: void addSharedTerm( TNode n ); void sendInfer( Node fact, Node exp, const char * c ); void sendLemma( Node fact, Node reason, const char * c ); - void sendMergeInfer( Node fact, Node reason, const char * c ); void doTCLemmas(); - // Helper functions + /** Helper functions */ bool holds( Node ); bool hasTerm( Node a ); void makeSharedTerm( Node ); @@ -248,8 +215,6 @@ private: void addToMap( std::map< Node, std::vector >&, Node, Node ); bool safelyAddToMap( std::map< Node, std::vector >&, Node, Node ); bool isRel( Node n ) {return n.getType().isSet() && n.getType().getSetElementType().isTuple();} - - }; diff --git a/test/regress/regress0/rels/Makefile.am b/test/regress/regress0/rels/Makefile.am index 50f979fbd..06658e988 100644 --- a/test/regress/regress0/rels/Makefile.am +++ b/test/regress/regress0/rels/Makefile.am @@ -99,10 +99,10 @@ TESTS = \ rel_tc_5_1.cvc \ rel_tp_join_1.cvc \ rel_transpose_0.cvc \ - set-strat.cvc + set-strat.cvc \ + rel_tc_8.cvc # unsolved : garbage_collect.cvc -# dump-unsat-core crash : rel_tc_8.cvc EXTRA_DIST = $(TESTS) -- 2.30.2