diff options
author | PaulMeng <baolmeng@gmail.com> | 2016-03-23 09:15:17 -0500 |
---|---|---|
committer | PaulMeng <baolmeng@gmail.com> | 2016-03-23 09:15:17 -0500 |
commit | 0ef0ba5360ae6e1586269c12396e07e9aa3dfb65 (patch) | |
tree | 1240ef93a87ddaf7326e685ee3390ae2a0ea2428 /src | |
parent | 02ecbe40a286e314f3e6775b93bed3bf135c8173 (diff) |
added typing rule for transitive closure
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/sets/theory_sets_rels.cpp | 12 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_type_rules.h | 10 |
2 files changed, 12 insertions, 10 deletions
diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp index bb9f10d16..7baf5976a 100644 --- a/src/theory/sets/theory_sets_rels.cpp +++ b/src/theory/sets/theory_sets_rels.cpp @@ -83,11 +83,9 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it; } if(kind_terms.find(kind::JOIN) != kind_terms.end()) { std::vector<Node> join_terms = kind_terms[kind::JOIN]; - Trace("rels-debug") << "[sets-rels] apply join rules on join terms with size = " << join_terms.size() << std::endl; // 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++) { - Trace("rels-debug") << "[sets-rels] join term = " << join_terms[j] << std::endl; applyJoinRule(exp, join_terms[j]); } } @@ -193,7 +191,7 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it; if(polarity & d_lemma.find(exp) != d_lemma.end()) { Trace("rels-debug") << "\n[sets-rels] Apply PRODUCT-SPLIT rule on term: " << product_term - << " with explaination: " << exp << std::endl; + << " with explanation: " << exp << std::endl; std::vector<Node> r1_element; std::vector<Node> r2_element; @@ -239,7 +237,7 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it; } else { // ONLY need to explicitly compute joins if there are negative literals involving PRODUCT Trace("rels-debug") << "\n[sets-rels] Apply PRODUCT-COMPOSE rule on term: " << product_term - << " with explaination: " << exp << std::endl; + << " with explanation: " << exp << std::endl; computeRels(product_term); } } @@ -261,7 +259,7 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it; if(polarity && d_lemma.find(exp) == d_lemma.end()) { Trace("rels-debug") << "\n[sets-rels] Apply JOIN-SPLIT rule on term: " << join_term - << " with explaination: " << exp << std::endl; + << " with explanation: " << exp << std::endl; std::vector<Node> r1_element; std::vector<Node> r2_element; @@ -323,7 +321,7 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it; } else { // ONLY need to explicitly compute joins if there are negative literals involving JOIN Trace("rels-debug") << "\n[sets-rels] Apply JOIN-COMPOSE rule on term: " << join_term - << " with explaination: " << exp << std::endl; + << " with explanation: " << exp << std::endl; computeRels(join_term); } } @@ -339,7 +337,7 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it; */ void TheorySetsRels::applyTransposeRule(Node exp, Node tp_term, bool tp_occur) { Trace("rels-debug") << "\n[sets-rels] Apply transpose rule on term: " << tp_term - << " with explaination: " << exp << std::endl; + << " with explanation: " << exp << std::endl; bool polarity = exp.getKind() != kind::NOT; Node atom = polarity ? exp : exp[0]; Node reversedTuple = getRepresentative(reverseTuple(atom[0])); diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h index 0e80795ea..22127ad50 100644 --- a/src/theory/sets/theory_sets_type_rules.h +++ b/src/theory/sets/theory_sets_type_rules.h @@ -236,12 +236,16 @@ struct RelTransClosureTypeRule { Assert(n.getKind() == kind::TRANSCLOSURE); TypeNode setType = n[0].getType(check); if(check) { - if(!setType.isSet()) { - throw TypeCheckingExceptionPrivate(n, " transitive closure operates on non-rel"); + if(!setType.isSet() && !setType.getSetElementType().isTuple()) { + throw TypeCheckingExceptionPrivate(n, " transitive closure operates on non-relation"); } - if(setType[0].getNumChildren() != 2) { + std::vector<TypeNode> tupleTypes = setType[0].getTupleTypes(); + if(tupleTypes.size() != 2) { throw TypeCheckingExceptionPrivate(n, " transitive closure operates on non-binary relations"); } + if(tupleTypes[0] != tupleTypes[1]) { + throw TypeCheckingExceptionPrivate(n, " transitive closure operates on non-homogeneous binary relations"); + } } return setType; } |