From: Paul Meng Date: Fri, 23 Sep 2016 22:43:05 +0000 (-0500) Subject: fixed a few bugs X-Git-Tag: cvc5-1.0.0~6030 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d9720be47f1e8e5550c82a740b7dfeb920f4e08a;p=cvc5.git fixed a few bugs --- diff --git a/src/theory/sets/rels_utils.h b/src/theory/sets/rels_utils.h index 3b9820360..df14bf53b 100644 --- a/src/theory/sets/rels_utils.h +++ b/src/theory/sets/rels_utils.h @@ -63,8 +63,9 @@ public: } static Node nthElementOfTuple( Node tuple, int n_th ) { - if(tuple.isConst() || (!tuple.isVar() && !tuple.isConst())) + if( tuple.getKind() == kind::APPLY_CONSTRUCTOR ) { return tuple[n_th]; + } Datatype dt = tuple.getType().getDatatype(); return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, dt[0][n_th].getSelector(), tuple); } @@ -92,4 +93,4 @@ public: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif \ No newline at end of file +#endif diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp index a1e6951cd..5b75c7810 100644 --- a/src/theory/sets/theory_sets_rels.cpp +++ b/src/theory/sets/theory_sets_rels.cpp @@ -56,60 +56,57 @@ int TheorySetsRels::EqcInfo::counter = 0; while(m_it != d_membership_constraints_cache.end()) { Node rel_rep = m_it->first; - // No relational terms found with rel_rep as its representative - // But TRANSPOSE(rel_rep) may occur in the context - if(d_terms_cache.find(rel_rep) == d_terms_cache.end()) { - Node tp_rel = NodeManager::currentNM()->mkNode(kind::TRANSPOSE, rel_rep); - Node tp_rel_rep = getRepresentative(tp_rel); - - if(d_terms_cache.find(tp_rel_rep) != d_terms_cache.end()) { - for(unsigned int i = 0; i < m_it->second.size(); i++) { - // Lazily apply transpose-occur rule. - // Need to eagerly apply if we don't send facts as lemmas - applyTransposeRule(d_membership_exp_cache[rel_rep][i], tp_rel_rep, true); + 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 + // transposed terms that are equal to the right hand side of exp + for(unsigned int j = 0; j < tp_terms.size(); j++) { + applyTransposeRule( exp, tp_terms[j] ); } } - } else { - 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 - // transposed terms that are equal to the right hand side of exp - for(unsigned int j = 0; j < tp_terms.size(); j++) { - applyTransposeRule(exp, tp_terms[j]); - } + if( kind_terms.find(kind::JOIN) != kind_terms.end() ) { + std::vector join_terms = kind_terms[kind::JOIN]; + // exp is a membership term and join_terms contains all + // terms involving "join" operator that are in the same + // equivalence class with the right hand side of exp + for(unsigned int j = 0; j < join_terms.size(); j++) { + applyJoinRule( exp, join_terms[j] ); } - if(kind_terms.find(kind::JOIN) != kind_terms.end()) { - std::vector join_terms = kind_terms[kind::JOIN]; - // exp is a membership term and join_terms contains all - // terms involving "join" operator that are in the same - // equivalence class with the right hand side of exp - for(unsigned int j = 0; j < join_terms.size(); j++) { - applyJoinRule(exp, join_terms[j]); - } + } + if( kind_terms.find(kind::PRODUCT) != kind_terms.end() ) { + std::vector product_terms = kind_terms[kind::PRODUCT]; + for(unsigned int j = 0; j < product_terms.size(); j++) { + applyProductRule( exp, product_terms[j] ); } - if(kind_terms.find(kind::PRODUCT) != kind_terms.end()) { - std::vector product_terms = kind_terms[kind::PRODUCT]; - for(unsigned int j = 0; j < product_terms.size(); j++) { - applyProductRule(exp, product_terms[j]); - } + } + if( kind_terms.find(kind::TCLOSURE) != kind_terms.end() ) { + std::vector tc_terms = kind_terms[kind::TCLOSURE]; + for(unsigned int j = 0; j < tc_terms.size(); j++) { + applyTCRule( exp, tc_terms[j] ); } - if(kind_terms.find(kind::TCLOSURE) != kind_terms.end()) { - std::vector tc_terms = kind_terms[kind::TCLOSURE]; - for(unsigned int j = 0; j < tc_terms.size(); j++) { - applyTCRule(exp, tc_terms[j]); - } + } + + MEM_IT tp_it = d_arg_rep_tp_terms.find( rel_rep ); + + if( tp_it != d_arg_rep_tp_terms.end() ) { + std::vector< Node >::iterator tp_ts_it = tp_it->second.begin(); + + while( tp_ts_it != tp_it->second.end() ) { + applyTransposeRule( exp, *tp_ts_it, (*tp_ts_it)[0] == rel_rep?Node::null():explain(EQUAL((*tp_ts_it)[0], rel_rep)), true ); + ++tp_ts_it; } + ++tp_it; } } m_it++; } TERM_IT t_it = d_terms_cache.begin(); - while(t_it != d_terms_cache.end()) { + while( t_it != d_terms_cache.end() ) { if(d_membership_constraints_cache.find(t_it->first) == d_membership_constraints_cache.end()) { Trace("rels-debug") << "[sets-rels-ee] A term that does not have membership constraints: " << t_it->first << std::endl; KIND_TERM_IT k_t_it = t_it->second.begin(); @@ -168,7 +165,6 @@ int TheorySetsRels::EqcInfo::counter = 0; 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(); - addToMap(d_membership_exp_cache, rel_rep, reason); if( is_true_eq ) { // add tup_rep to membership database @@ -185,6 +181,19 @@ int TheorySetsRels::EqcInfo::counter = 0; std::map > rel_terms; TERM_IT terms_it = d_terms_cache.find(eqc_rep); + if( eqc_node.getKind() == kind::TRANSPOSE ) { + Node eqc_node0_rep = getRepresentative( eqc_node[0] ); + MEM_IT mem_it = d_arg_rep_tp_terms.find( eqc_node0_rep ); + + if( mem_it != d_arg_rep_tp_terms.end() ) { + mem_it->second.push_back( eqc_node ); + } else { + std::vector< Node > tp_terms; + tp_terms.push_back( eqc_node ); + d_arg_rep_tp_terms[eqc_node0_rep] = tp_terms; + } + } + if( terms_it == d_terms_cache.end() ) { terms.push_back(eqc_node); rel_terms[eqc_node.getKind()] = terms; @@ -546,8 +555,8 @@ int TheorySetsRels::EqcInfo::counter = 0; * ----------------------------------------------- * [NOT] (X = Y) */ - void TheorySetsRels::applyTransposeRule(Node exp, Node tp_term, bool tp_occur) { - Trace("rels-debug") << "\n[sets-rels] *********** Applying TRANSPOSE rule " << std::endl; + void TheorySetsRels::applyTransposeRule(Node exp, Node tp_term, Node more_reason, bool tp_occur) { + Trace("rels-debug") << "\n[sets-rels] *********** Applying TRANSPOSE rule on term " << tp_term << std::endl; bool polarity = exp.getKind() != kind::NOT; Node atom = polarity ? exp : exp[0]; @@ -558,7 +567,7 @@ int TheorySetsRels::EqcInfo::counter = 0; << " with explanation: " << exp << std::endl; Node fact = polarity ? MEMBER(reversedTuple, tp_term) : MEMBER(reversedTuple, tp_term).negate(); - sendInfer(fact, exp, "transpose-occur"); + sendInfer(fact, more_reason == Node::null()?exp:AND(exp, more_reason), "transpose-occur"); return; } @@ -838,7 +847,7 @@ int TheorySetsRels::EqcInfo::counter = 0; doTCLemmas(); } - + d_arg_rep_tp_terms.clear(); d_tc_membership_db.clear(); d_rel_nodes.clear(); d_pending_facts.clear(); @@ -1176,18 +1185,26 @@ int TheorySetsRels::EqcInfo::counter = 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; + Trace("rels-debug") << "Reduce tuple var: " << n[0] << " to concrete one " << " node = " << n << std::endl; std::vector tuple_elements; tuple_elements.push_back(Node::fromExpr((n[0].getType().getDatatype())[0].getConstructor())); - + Trace("rels-debug") << "Reduce tuple var: " << n[0] << " to concrete one ****** 0" << std::endl; for(unsigned int i = 0; i < n[0].getType().getTupleLength(); i++) { + Trace("rels-debug") << "Reduce tuple var: " << n[0] << " to concrete one ****** 1" << std::endl; Node element = RelsUtils::nthElementOfTuple(n[0], i); + Trace("rels-debug") << "Reduce tuple var: " << n[0] << " to concrete one ****** 2" << std::endl; makeSharedTerm(element); + Trace("rels-debug") << "Reduce tuple var: " << n[0] << " to concrete one ****** 3" << std::endl; tuple_elements.push_back(element); + Trace("rels-debug") << "Reduce tuple var: " << n[0] << " to concrete one ****** 4" << std::endl; } + Trace("rels-debug") << "Reduce tuple var: " << n[0] << " to concrete one ****** 5" << std::endl; Node tuple_reduct = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, tuple_elements); + Trace("rels-debug") << "Reduce tuple var: " << n[0] << " to concrete one ****** 6" << std::endl; tuple_reduct = MEMBER(tuple_reduct, n[1]); + Trace("rels-debug") << "Reduce tuple var: " << n[0] << " to concrete one ****** 7" << std::endl; Node tuple_reduction_lemma = NodeManager::currentNM()->mkNode(kind::IFF, n, tuple_reduct); + Trace("rels-debug") << "Reduce tuple var: " << n[0] << " to concrete one ****** 8" << std::endl; sendLemma(tuple_reduction_lemma, d_trueNode, "tuple-reduction"); d_symbolic_tuples.insert(n); } diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h index f756930c4..7877cdde5 100644 --- a/src/theory/sets/theory_sets_rels.h +++ b/src/theory/sets/theory_sets_rels.h @@ -147,6 +147,9 @@ private: /** Mapping between a relation representative and its equivalent relations involving relational operators */ std::map< Node, std::map > > d_terms_cache; + /** Mapping between relation and its member representatives */ + std::map< Node, std::vector > d_arg_rep_tp_terms; + /** Mapping between TC(r) and one explanation when building TC graph*/ std::map< Node, Node > d_membership_tc_exp_cache; @@ -193,7 +196,7 @@ private: void applyProductRule( Node, Node ); void composeTupleMemForRel( Node ); void assertMembership( Node fact, Node reason, bool polarity ); - void applyTransposeRule( Node, Node, bool tp_occur_rule = false ); + void applyTransposeRule( Node, Node, Node more_reason = Node::null(), bool tp_occur_rule = false ); diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h index a709eff09..89d481746 100644 --- a/src/theory/sets/theory_sets_type_rules.h +++ b/src/theory/sets/theory_sets_type_rules.h @@ -189,8 +189,6 @@ struct RelBinaryOperatorTypeRule { Assert(n.getKind() == kind::PRODUCT || n.getKind() == kind::JOIN); - - TypeNode firstRelType = n[0].getType(check); TypeNode secondRelType = n[1].getType(check); TypeNode resultType = firstRelType;