From: Paul Meng <212461047> Date: Sat, 23 Jul 2016 20:35:51 +0000 (-0400) Subject: refactored code X-Git-Tag: cvc5-1.0.0~6045 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=509274ae2bc7ae9e41a803d94fce289316b8558e;p=cvc5.git refactored code --- diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp index 4278b50c0..92b13774e 100644 --- a/src/theory/sets/theory_sets_rels.cpp +++ b/src/theory/sets/theory_sets_rels.cpp @@ -15,13 +15,11 @@ **/ #include "theory/sets/theory_sets_rels.h" - #include "expr/datatype.h" #include "theory/sets/expr_patterns.h" #include "theory/sets/theory_sets_private.h" #include "theory/sets/theory_sets.h" - using namespace std; using namespace CVC4::expr::pattern; @@ -29,15 +27,14 @@ namespace CVC4 { namespace theory { namespace sets { -typedef std::map >::iterator MEM_IT; +typedef std::map< Node, std::vector< Node > >::iterator MEM_IT; +typedef std::map< kind::Kind_t, std::vector< Node > >::iterator KIND_TERM_IT; typedef std::map< Node, std::hash_set< Node, NodeHashFunction > >::iterator TC_PAIR_IT; -typedef std::map > >::iterator TERM_IT; -typedef std::map > >::iterator TC_IT; +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; - - // do a test void TheorySetsRels::check(Theory::Effort level) { Trace("rels") << "\n[sets-rels] ******************************* Start the relational solver *******************************\n" << std::endl; if(Theory::fullEffort(level)) { @@ -55,6 +52,7 @@ int TheorySetsRels::EqcInfo::counter = 0; void TheorySetsRels::check() { MEM_IT m_it = d_membership_constraints_cache.begin(); + while(m_it != d_membership_constraints_cache.end()) { Node rel_rep = m_it->first; @@ -75,6 +73,7 @@ int TheorySetsRels::EqcInfo::counter = 0; for(unsigned int i = 0; i < m_it->second.size(); i++) { Node exp = d_membership_exp_cache[rel_rep][i]; std::map > kind_terms = d_terms_cache[rel_rep]; + if(kind_terms.find(kind::TRANSPOSE) != kind_terms.end()) { std::vector tp_terms = kind_terms[kind::TRANSPOSE]; // exp is a membership term and tp_terms contains all @@ -111,69 +110,73 @@ int TheorySetsRels::EqcInfo::counter = 0; } /* - * Polulate the relational terms data structure + * Populate relational terms data structure */ void TheorySetsRels::collectRelsInfo() { - Trace("rels-debug") << "[sets-rels] Start collecting relational terms..." << std::endl; + Trace("rels") << "[sets-rels] Start collecting relational terms..." << std::endl; eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( d_eqEngine ); while( !eqcs_i.isFinished() ){ - Node r = (*eqcs_i); - eq::EqClassIterator eqc_i = eq::EqClassIterator( r, d_eqEngine ); - Trace("rels-ee") << "[sets-rels-ee] term representative: " << r << std::endl; + Node eqc_rep = (*eqcs_i); + eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc_rep, d_eqEngine ); + + Trace("rels-ee") << "[sets-rels-ee] term representative: " << eqc_rep << std::endl; + while( !eqc_i.isFinished() ){ - Node n = (*eqc_i); - Trace("rels-ee") << " term : " << n << std::endl; + Node eqc_node = (*eqc_i); + + Trace("rels-ee") << " term : " << eqc_node << std::endl; - if(getRepresentative(r) == getRepresentative(d_trueNode) || - getRepresentative(r) == getRepresentative(d_falseNode)) { + if(getRepresentative(eqc_rep) == getRepresentative(d_trueNode) || + getRepresentative(eqc_rep) == getRepresentative(d_falseNode)) { // collect membership info - if(n.getKind() == kind::MEMBER && n[1].getType().getSetElementType().isTuple()) { - Node tup_rep = getRepresentative(n[0]); - Node rel_rep = getRepresentative(n[1]); - // Todo: check n[0] or n[0]'s rep is a var?? - if(n[0].isVar()){ - reduceTupleVar(n); + 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]); + + if(eqc_node[0].isVar()){ + reduceTupleVar(eqc_node); } else { - if(safeAddToMap(d_membership_constraints_cache, rel_rep, tup_rep)) { - bool true_eq = areEqual(r, d_trueNode); - Node reason = true_eq ? n : n.negate(); - addToMap(d_membership_exp_cache, rel_rep, reason); + if( safelyAddToMap(d_membership_constraints_cache, rel_rep, tup_rep) ) { + bool is_true_eq = areEqual(eqc_rep, d_trueNode); + Node reason = is_true_eq ? eqc_node : eqc_node.negate(); - if(true_eq) { + addToMap(d_membership_exp_cache, rel_rep, reason); + if( is_true_eq ) { + // add tup_rep to membership database + // and store mapping between tuple and tuple's elements representatives addToMembershipDB(rel_rep, tup_rep, reason); } } } } // collect relational terms info - } else if( r.getType().isSet() && r.getType().getSetElementType().isTuple() ) { - if( n.getKind() == kind::TRANSPOSE || - n.getKind() == kind::JOIN || - n.getKind() == kind::PRODUCT || - n.getKind() == kind::TCLOSURE ) { - std::map > rel_terms; + } else if( eqc_rep.getType().isSet() && eqc_rep.getType().getSetElementType().isTuple() ) { + if( eqc_node.getKind() == kind::TRANSPOSE || eqc_node.getKind() == kind::JOIN || + eqc_node.getKind() == kind::PRODUCT || eqc_node.getKind() == kind::TCLOSURE ) { std::vector terms; - // No r record is found - if( d_terms_cache.find(r) == d_terms_cache.end() ) { - terms.push_back(n); - rel_terms[n.getKind()] = terms; - d_terms_cache[r] = rel_terms; + std::map > rel_terms; + TERM_IT terms_it = d_terms_cache.find(eqc_rep); + + if( terms_it == d_terms_cache.end() ) { + terms.push_back(eqc_node); + rel_terms[eqc_node.getKind()] = terms; + d_terms_cache[eqc_rep] = rel_terms; } else { - // No n's kind record is found - if( d_terms_cache[r].find(n.getKind()) == d_terms_cache[r].end() ) { - terms.push_back(n); - d_terms_cache[r][n.getKind()] = terms; + KIND_TERM_IT kind_term_it = terms_it->second.find(eqc_node.getKind()); + + if( kind_term_it == terms_it->second.end() ) { + terms.push_back(eqc_node); + d_terms_cache[eqc_rep][eqc_node.getKind()] = terms; } else { - d_terms_cache[r][n.getKind()].push_back(n); + kind_term_it->second.push_back(eqc_node); } } } // need to add all tuple elements as shared terms - } else if(n.getType().isTuple() && !n.isConst() && !n.isVar()) { - for(unsigned int i = 0; i < n.getType().getTupleLength(); i++) { - Node element = RelsUtils::nthElementOfTuple(n, i); - + } else if(eqc_node.getType().isTuple() && !eqc_node.isConst() && !eqc_node.isVar()) { + for(unsigned int i = 0; i < eqc_node.getType().getTupleLength(); i++) { + Node element = RelsUtils::nthElementOfTuple(eqc_node, i); if(!element.isConst()) { makeSharedTerm(element); } @@ -258,56 +261,6 @@ int TheorySetsRels::EqcInfo::counter = 0; } } //todo: need to construct a tc_graph if transitive closure is used in the context - -// Node atom = polarity ? exp : exp[0]; -// Node tup_rep = getRepresentative(atom[0]); -// Node tc_rep = getRepresentative(tc_term); -// Node tc_r_rep = getRepresentative(tc_term[0]); -// -// // build the TC graph for tc_rep if it was not created before -// if( d_rel_nodes.find(tc_rep) == d_rel_nodes.end() ) { -// Trace("rels-debug") << "[sets-rels] Start building the TC graph!" << std::endl; -// buildTCGraph(tc_r_rep, tc_rep, tc_term); -// d_rel_nodes.insert(tc_rep); -// } - - // insert tup_rep in the tc_graph if it is not in the graph already -// TC_IT tc_graph_it = d_membership_tc_cache.find(tc_rep); -// -// if( polarity ) { -// Node fst_rep = getRepresentative(RelsUtils::nthElementOfTuple(tup_rep, 0)); -// Node snd_rep = getRepresentative(RelsUtils::nthElementOfTuple(tup_rep, 1)); -// -// if( tc_graph_it != d_membership_tc_cache.end() ) { -// TC_PAIR_IT pair_set_it = tc_graph_it->second.find(fst_rep); -// -// if( pair_set_it != tc_graph_it->second.end() ) { -// pair_set_it->second.insert(snd_rep); -// } else { -// std::hash_set< Node, NodeHashFunction > pair_set; -// pair_set.insert(snd_rep); -// tc_graph_it->second[fst_rep] = pair_set; -// } -// -// Node reason = getReason(tc_rep, tc_term, tc_r_rep, tc_term[0]); -// std::map< Node, Node >::iterator exp_it = d_membership_tc_exp_cache.find(tc_rep); -// -// if(!reason.isNull() && exp_it->second != reason) { -// d_membership_tc_exp_cache[tc_rep] = Rewriter::rewrite(AND(exp_it->second, reason)); -// } -// } else { -// std::map< Node, std::hash_set< Node, NodeHashFunction > > pair_set; -// std::hash_set< Node, NodeHashFunction > snd_set; -// -// snd_set.insert(snd_rep); -// pair_set[fst_rep] = snd_set; -// d_membership_tc_cache[tc_rep] = pair_set; -// Node reason = getReason(tc_rep, tc_term, tc_r_rep, tc_term[0]); -// -// if(!reason.isNull()) { -// d_membership_tc_exp_cache[tc_rep] = reason; -// } -// } // // check if tup_rep already exists in TC graph for conflict // } else { // if( tc_graph_it != d_membership_tc_cache.end() ) { @@ -530,7 +483,7 @@ int TheorySetsRels::EqcInfo::counter = 0; * ------------------------------------------------ * [NOT] (b, a) IS_IN X * - * + * Not implemented! * transpose-equal rule: [NOT] (TRANSPOSE X) = (TRANSPOSE Y) * ----------------------------------------------- * [NOT] (X = Y) @@ -914,7 +867,7 @@ int TheorySetsRels::EqcInfo::counter = 0; } } - bool TheorySetsRels::isTCReachable(Node start, Node dest, std::hash_set& hasSeen, + void TheorySetsRels::isTCReachable(Node start, Node dest, std::hash_set& hasSeen, std::map< Node, std::hash_set< Node, NodeHashFunction > >& tc_graph, bool& isReachable) { if(hasSeen.find(start) == hasSeen.end()) { hasSeen.insert(start); @@ -925,6 +878,7 @@ int TheorySetsRels::EqcInfo::counter = 0; if(pair_set_it != tc_graph.end()) { if(pair_set_it->second.find(dest) != pair_set_it->second.end()) { isReachable = isReachable || true; + return; } else { std::hash_set< Node, NodeHashFunction >::iterator set_it = pair_set_it->second.begin(); @@ -937,7 +891,6 @@ int TheorySetsRels::EqcInfo::counter = 0; } } } - isReachable = isReachable || false; } void TheorySetsRels::sendSplit(Node a, Node b, const char * c) { @@ -1048,7 +1001,10 @@ int TheorySetsRels::EqcInfo::counter = 0; return false; } - bool TheorySetsRels::safeAddToMap(std::map< Node, std::vector >& map, Node rel_rep, Node member) { + /* + * Make sure duplicate members are not added in map + */ + bool TheorySetsRels::safelyAddToMap(std::map< Node, std::vector >& map, Node rel_rep, Node member) { std::map< Node, std::vector< Node > >::iterator mem_it = map.find(rel_rep); if(mem_it == map.end()) { std::vector members; @@ -1210,6 +1166,10 @@ int TheorySetsRels::EqcInfo::counter = 0; return false; } + /* + * For each tuple n, we store a mapping between n and a list of its elements representatives + * in d_tuple_reps. This would later be used for applying JOIN operator. + */ void TheorySetsRels::computeTupleReps( Node n ) { if( d_tuple_reps.find( n ) == d_tuple_reps.end() ){ for( unsigned i = 0; i < n.getType().getTupleLength(); i++ ){ @@ -1230,6 +1190,10 @@ int TheorySetsRels::EqcInfo::counter = 0; return NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, Node::fromExpr(dt[0].getConstructor()), a, b); } + /* + * Node n[0] is a tuple variable, reduce n[0] to a concrete representation, + * which is (e1, ..., en) where e1, ... ,en are concrete elements of tuple n[0]. + */ void TheorySetsRels::reduceTupleVar(Node n) { if(d_symbolic_tuples.find(n) == d_symbolic_tuples.end()) { Trace("rels-debug") << "Reduce tuple var: " << n[0] << " to concrete one " << std::endl; @@ -1505,8 +1469,6 @@ int TheorySetsRels::EqcInfo::counter = 0; 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; - - NodeMap::iterator map_it = tc_ei->d_mem_exp.begin(); Node exp = explainTCMem(tc_ei, mem_rep, fst_rep, snd_rep); Assert(!exp.isNull()); Node tc_lemma = NodeManager::currentNM()->mkNode(kind::IMPLIES, exp, MEMBER(mem_rep, tc_ei->d_tc.get())); diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h index 40ded2772..056ef9858 100644 --- a/src/theory/sets/theory_sets_rels.h +++ b/src/theory/sets/theory_sets_rels.h @@ -123,15 +123,27 @@ private: std::hash_set< Node, NodeHashFunction > d_rel_nodes; std::map< Node, std::vector > d_tuple_reps; std::map< Node, TupleTrie > d_membership_trie; + + /** Symbolic tuple variables that has been reduced to concrete ones */ std::hash_set< Node, NodeHashFunction > d_symbolic_tuples; + + /** Mapping between relation and its (non)members representatives */ std::map< Node, std::vector > d_membership_constraints_cache; + + /** Mapping between relation and its (non)members' explanation */ std::map< Node, std::vector > d_membership_exp_cache; + + /** Mapping between relation and its member representatives */ std::map< Node, std::vector > d_membership_db; + + /** Mapping between relation and its members' explanation */ std::map< Node, std::vector > d_membership_exp_db; - std::map< Node, Node > d_membership_tc_exp_cache; - std::map< Node, std::hash_set > d_tc_membership_db; + /** Mapping between a relation and its equivalent relations involving relational operators */ std::map< Node, std::map > > d_terms_cache; + + std::map< Node, Node > d_membership_tc_exp_cache; + std::map< Node, std::hash_set > d_tc_membership_db; std::map< Node, std::map< Node, std::hash_set > > d_membership_tc_cache; /** information necessary for equivalence classes */ @@ -175,7 +187,7 @@ private: void inferTC( Node, std::map< Node, std::hash_set< Node, NodeHashFunction > >& ); void inferTC( Node, Node, std::map< Node, std::hash_set< Node, NodeHashFunction > >&, Node, Node, std::hash_set< Node, NodeHashFunction >&); - bool isTCReachable(Node fst, Node snd, std::hash_set& hasSeen, + void isTCReachable(Node fst, Node snd, std::hash_set& hasSeen, std::map< Node, std::hash_set< Node, NodeHashFunction > >& tc_graph, bool&); Node explain(Node); @@ -194,7 +206,7 @@ private: inline Node getReason(Node tc_rep, Node tc_term, Node tc_r_rep, Node tc_r); inline Node constructPair(Node tc_rep, Node a, Node b); Node findMemExp(Node r, Node pair); - bool safeAddToMap( std::map< Node, std::vector >&, Node, Node ); + bool safelyAddToMap( std::map< Node, std::vector >&, Node, Node ); void addToMap( std::map< Node, std::vector >&, Node, Node ); bool hasMember( Node, Node ); Node getRepresentative( Node t );