diff options
author | PaulMeng <baolmeng@gmail.com> | 2016-04-15 11:40:40 -0500 |
---|---|---|
committer | PaulMeng <baolmeng@gmail.com> | 2016-04-15 11:40:40 -0500 |
commit | 7f09980d2bed5effd511d5f690d968f3cc048363 (patch) | |
tree | 61481c16efe95c30f5a4e68009612191e8f7f49b /src/theory | |
parent | 4a17519a49f49633fa0145a55b1b45346f2b86fc (diff) |
change transitive closure operator name to TCLOUSRE
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/sets/kinds | 6 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_private.cpp | 2 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_rels.cpp | 22 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_rewriter.cpp | 6 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_type_rules.h | 4 |
5 files changed, 19 insertions, 21 deletions
diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds index 6767de481..efd00093a 100644 --- a/src/theory/sets/kinds +++ b/src/theory/sets/kinds @@ -46,7 +46,7 @@ operator INSERT 2: "set obtained by inserting elements (first N-1 paramet operator JOIN 2 "set join" operator PRODUCT 2 "set cartesian product" operator TRANSPOSE 1 "set transpose" -operator TRANSCLOSURE 1 "set transitive closure" +operator TCLOSURE 1 "set transitive closure" typerule UNION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule typerule INTERSECTION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule @@ -60,7 +60,7 @@ typerule INSERT ::CVC4::theory::sets::InsertTypeRule typerule JOIN ::CVC4::theory::sets::RelBinaryOperatorTypeRule typerule PRODUCT ::CVC4::theory::sets::RelBinaryOperatorTypeRule typerule TRANSPOSE ::CVC4::theory::sets::RelTransposeTypeRule -typerule TRANSCLOSURE ::CVC4::theory::sets::RelTransClosureTypeRule +typerule TCLOSURE ::CVC4::theory::sets::RelTransClosureTypeRule construle UNION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule construle INTERSECTION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule @@ -71,6 +71,6 @@ construle INSERT ::CVC4::theory::sets::InsertTypeRule construle JOIN ::CVC4::theory::sets::RelBinaryOperatorTypeRule construle PRODUCT ::CVC4::theory::sets::RelBinaryOperatorTypeRule construle TRANSPOSE ::CVC4::theory::sets::RelTransposeTypeRule -construle TRANSCLOSURE ::CVC4::theory::sets::RelTransClosureTypeRule +construle TCLOSURE ::CVC4::theory::sets::RelTransClosureTypeRule endtheory diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index db4f4bf26..434202a53 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -782,7 +782,7 @@ bool TheorySetsPrivate::checkModel(const SettermElementsMap& settermElementsMap, Trace("rels-debug") << " ***** Done with check model for JOIN operator" << std::endl; break; } - case kind::TRANSCLOSURE: + case kind::TCLOSURE: break; default: Unhandled(); diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp index eae9a4e8f..a1a799f4b 100644 --- a/src/theory/sets/theory_sets_rels.cpp +++ b/src/theory/sets/theory_sets_rels.cpp @@ -67,8 +67,6 @@ typedef std::map< Node, std::hash_set< Node, NodeHashFunction > >::iterator TC_P 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++) { -// Node exp = tp_rel == tp_rel_rep ? d_membership_exp_cache[rel_rep][i] -// : AND(d_membership_exp_cache[rel_rep][i], EQUAL(tp_rel, tp_rel_rep)); // 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); @@ -100,8 +98,8 @@ typedef std::map< Node, std::hash_set< Node, NodeHashFunction > >::iterator TC_P applyProductRule(exp, product_terms[j]); } } - if(kind_terms.find(kind::TRANSCLOSURE) != kind_terms.end()) { - std::vector<Node> tc_terms = kind_terms[kind::TRANSCLOSURE]; + if(kind_terms.find(kind::TCLOSURE) != kind_terms.end()) { + std::vector<Node> tc_terms = kind_terms[kind::TCLOSURE]; for(unsigned int j = 0; j < tc_terms.size(); j++) { applyTCRule(exp, tc_terms[j]); } @@ -153,7 +151,7 @@ typedef std::map< Node, std::hash_set< Node, NodeHashFunction > >::iterator TC_P if( n.getKind() == kind::TRANSPOSE || n.getKind() == kind::JOIN || n.getKind() == kind::PRODUCT || - n.getKind() == kind::TRANSCLOSURE ) { + n.getKind() == kind::TCLOSURE ) { std::map<kind::Kind_t, std::vector<Node> > rel_terms; std::vector<Node> terms; // No r record is found @@ -190,15 +188,15 @@ typedef std::map< Node, std::hash_set< Node, NodeHashFunction > >::iterator TC_P /* * * - * transitive closure rule 1: y = (TRANSCLOSURE x) + * transitive closure rule 1: y = (TCLOSURE x) * --------------------------------------------- * y = x | x.x | x.x.x | ... (| is union) * * * - * transitive closure rule 2: TRANSCLOSURE(x) + * transitive closure rule 2: TCLOSURE(x) * ----------------------------------------------------------- - * x <= TRANSCLOSURE(x) && (x JOIN x) <= TRANSCLOSURE(x) .... + * x <= TCLOSURE(x) && (x JOIN x) <= TCLOSURE(x) .... * * TC(x) = TC(y) => x = y ? * @@ -984,7 +982,7 @@ typedef std::map< Node, std::hash_set< Node, NodeHashFunction > >::iterator TC_P // tc_terms are transitive closure of rels and are modulo equal to tc_rep Node TheorySetsRels::findMemExp(Node tc_rep, Node tuple) { Trace("rels-exp") << "TheorySetsRels::findMemExp ( tc_rep = " << tc_rep << ", tuple = " << tuple << ")" << std::endl; - std::vector<Node> tc_terms = d_terms_cache.find(tc_rep)->second[kind::TRANSCLOSURE]; + std::vector<Node> tc_terms = d_terms_cache.find(tc_rep)->second[kind::TCLOSURE]; Assert(tc_terms.size() > 0); for(unsigned int i = 0; i < tc_terms.size(); i++) { Node tc_term = tc_terms[i]; @@ -1054,7 +1052,7 @@ typedef std::map< Node, std::hash_set< Node, NodeHashFunction > >::iterator TC_P return Node::null(); } - Node TheorySetsRels::nthElementOfTuple( Node tuple, int n_th ) { + Node TheorySetsRels::nthElementOfTuple( Node tuple, int n_th ) { if(tuple.isConst() || (!tuple.isVar() && !tuple.isConst())) return tuple[n_th]; Datatype dt = tuple.getType().getDatatype(); @@ -1159,7 +1157,7 @@ typedef std::map< Node, std::hash_set< Node, NodeHashFunction > >::iterator TC_P d_eqEngine->addFunctionKind(kind::PRODUCT); d_eqEngine->addFunctionKind(kind::JOIN); d_eqEngine->addFunctionKind(kind::TRANSPOSE); - d_eqEngine->addFunctionKind(kind::TRANSCLOSURE); + d_eqEngine->addFunctionKind(kind::TCLOSURE); } TheorySetsRels::~TheorySetsRels() {} @@ -1188,7 +1186,7 @@ typedef std::map< Node, std::hash_set< Node, NodeHashFunction > >::iterator TC_P Node TupleTrie::existsTerm( std::vector< Node >& reps, int argIndex ) { if( argIndex==(int)reps.size() ){ - if( d_data.empty() ){ + if( d_data.empty() ){ return Node::null(); }else{ return d_data.begin()->first; diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp index 61ec07e9d..4c22f588d 100644 --- a/src/theory/sets/theory_sets_rewriter.cpp +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -296,14 +296,14 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { break; } - case kind::TRANSCLOSURE: { + case kind::TCLOSURE: { if(node[0].getKind() == kind::EMPTYSET) { return RewriteResponse(REWRITE_DONE, nm->mkConst(EmptySet(nm->toType(node.getType())))); } else if (node[0].isConst()) { - } else if(node[0].getKind() == kind::TRANSCLOSURE) { + } else if(node[0].getKind() == kind::TCLOSURE) { return RewriteResponse(REWRITE_AGAIN, node[0]); - } else if(node[0].getKind() != kind::TRANSCLOSURE) { + } else if(node[0].getKind() != kind::TCLOSURE) { Trace("sets-postrewrite") << "Sets::postRewrite returning " << node << std::endl; return RewriteResponse(REWRITE_DONE, node); } diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h index 22127ad50..fdcb094fc 100644 --- a/src/theory/sets/theory_sets_type_rules.h +++ b/src/theory/sets/theory_sets_type_rules.h @@ -233,7 +233,7 @@ struct RelTransposeTypeRule { struct RelTransClosureTypeRule { inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate, AssertionException) { - Assert(n.getKind() == kind::TRANSCLOSURE); + Assert(n.getKind() == kind::TCLOSURE); TypeNode setType = n[0].getType(check); if(check) { if(!setType.isSet() && !setType.getSetElementType().isTuple()) { @@ -251,7 +251,7 @@ struct RelTransClosureTypeRule { } inline static bool computeIsConst(NodeManager* nodeManager, TNode n) { - Assert(n.getKind() == kind::TRANSCLOSURE); + Assert(n.getKind() == kind::TCLOSURE); return false; } };/* struct RelTransClosureTypeRule */ |