From: PaulMeng Date: Fri, 15 Apr 2016 16:40:40 +0000 (-0500) Subject: change transitive closure operator name to TCLOUSRE X-Git-Tag: cvc5-1.0.0~6059 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7f09980d2bed5effd511d5f690d968f3cc048363;p=cvc5.git change transitive closure operator name to TCLOUSRE --- diff --git a/.vscode/settings.json b/.vscode/settings.json new file mode 100644 index 000000000..44d6fcbbf --- /dev/null +++ b/.vscode/settings.json @@ -0,0 +1,4 @@ +// Place your settings in this file to overwrite default and user settings. +{ + "editor.fontSize": 18 +} \ No newline at end of file diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 27182cb6d..967503074 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -208,7 +208,7 @@ tokens { JOIN_TOK = 'JOIN'; TRANSPOSE_TOK = 'TRANSPOSE'; PRODUCT_TOK = 'PRODUCT'; - TRANSCLOSURE_TOK = 'TRANSCLOSURE'; + TRANSCLOSURE_TOK = 'TCLOSURE'; // Strings @@ -1649,7 +1649,7 @@ bvNegTerm[CVC4::Expr& f] | TRANSPOSE_TOK bvNegTerm[f] { f = MK_EXPR(CVC4::kind::TRANSPOSE, f); } | TRANSCLOSURE_TOK bvNegTerm[f] - { f = MK_EXPR(CVC4::kind::TRANSCLOSURE, f); } + { f = MK_EXPR(CVC4::kind::TCLOSURE, f); } | TUPLE_TOK LPAREN bvNegTerm[f] RPAREN { std::vector types; std::vector args; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 530e9da8b..ff22dd9c7 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -225,7 +225,7 @@ void Smt2::addTheory(Theory theory) { addOperator(kind::SUBSET, "subset"); addOperator(kind::MEMBER, "member"); addOperator(kind::TRANSPOSE, "transpose"); - addOperator(kind::TRANSCLOSURE, "transclosure"); + addOperator(kind::TCLOSURE, "tclosure"); addOperator(kind::JOIN, "join"); addOperator(kind::PRODUCT, "product"); addOperator(kind::SINGLETON, "singleton"); diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 58835d4e6..9de790d7b 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -780,8 +780,8 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo op << "TRANSPOSE"; opType = PREFIX; break; - case kind::TRANSCLOSURE: - op << "TRANSCLOSURE"; + case kind::TCLOSURE: + op << "TCLOSURE"; opType = PREFIX; break; case kind::SINGLETON: diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index d37f4ae99..7c501ffec 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -505,7 +505,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::SUBSET: case kind::MEMBER: case kind::SET_TYPE: - case kind::TRANSCLOSURE: + case kind::TCLOSURE: case kind::TRANSPOSE: case kind::JOIN: case kind::PRODUCT: @@ -786,7 +786,7 @@ static string smtKindString(Kind k) throw() { case kind::SET_TYPE: return "Set"; case kind::SINGLETON: return "singleton"; case kind::INSERT: return "insert"; - case kind::TRANSCLOSURE: return "transclosure"; + case kind::TCLOSURE: return "tclosure"; case kind::TRANSPOSE: return "transpose"; case kind::PRODUCT: return "product"; case kind::JOIN: return "join"; 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 tc_terms = kind_terms[kind::TRANSCLOSURE]; + 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]); } @@ -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 > rel_terms; std::vector 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 tc_terms = d_terms_cache.find(tc_rep)->second[kind::TRANSCLOSURE]; + std::vector 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 */