From 371c0799fa38452c2186efd268c73a42c282c96e Mon Sep 17 00:00:00 2001 From: PaulMeng Date: Tue, 9 Feb 2016 14:51:44 -0600 Subject: [PATCH] - extend cvc4 frontend parser to accept relational operators (product, join, transpose, transitive closure) - added a finite relations module to collect all relational terms in EE --- src/Makefile.am | 2 + src/parser/cvc/Cvc.g | 21 ++++- src/printer/cvc/cvc_printer.cpp | 16 ++++ src/theory/sets/kinds | 15 +++ src/theory/sets/theory_sets_private.cpp | 7 +- src/theory/sets/theory_sets_private.h | 2 + src/theory/sets/theory_sets_rels.cpp | 111 +++++++++++++++++++++++ src/theory/sets/theory_sets_rels.h | 47 ++++++++++ src/theory/sets/theory_sets_type_rules.h | 74 +++++++++++++++ 9 files changed, 293 insertions(+), 2 deletions(-) create mode 100644 src/theory/sets/theory_sets_rels.cpp create mode 100644 src/theory/sets/theory_sets_rels.h diff --git a/src/Makefile.am b/src/Makefile.am index 4f2998e7a..040be7fae 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -255,6 +255,8 @@ libcvc4_la_SOURCES = \ theory/sets/theory_sets.h \ theory/sets/theory_sets_private.cpp \ theory/sets/theory_sets_private.h \ + theory/sets/theory_sets_rels.cpp \ + theory/sets/theory_sets_rels.h \ theory/sets/theory_sets_rewriter.cpp \ theory/sets/theory_sets_rewriter.h \ theory/sets/theory_sets_type_enumerator.h \ diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index d57aea93c..f3a2bbe02 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -201,6 +201,12 @@ tokens { BVSGT_TOK = 'BVSGT'; BVSLE_TOK = 'BVSLE'; BVSGE_TOK = 'BVSGE'; + + // Relations + JOIN_TOK = 'JOIN'; + TRANSPOSE_TOK = 'TRANSPOSE'; + PRODUCT_TOK = 'PRODUCT'; + TRANSCLOSURE_TOK = 'TRANSCLOSURE'; // Strings @@ -290,7 +296,11 @@ int getOperatorPrecedence(int type) { case DIV_TOK: case MOD_TOK: return 23; case PLUS_TOK: - case MINUS_TOK: return 24; + case MINUS_TOK: + case JOIN_TOK: + case TRANSPOSE_TOK: + case PRODUCT_TOK: + case TRANSCLOSURE_TOK: return 24; case LEQ_TOK: case LT_TOK: case GEQ_TOK: @@ -327,6 +337,9 @@ Kind getOperatorKind(int type, bool& negate) { case OR_TOK: return kind::OR; case XOR_TOK: return kind::XOR; case AND_TOK: return kind::AND; + + case PRODUCT_TOK: return kind::PRODUCT; + case JOIN_TOK: return kind::JOIN; // comparisonBinop case EQUAL_TOK: return kind::EQUAL; @@ -1449,6 +1462,8 @@ booleanBinop[unsigned& op] | OR_TOK | XOR_TOK | AND_TOK + | JOIN_TOK + | PRODUCT_TOK ; comparison[CVC4::Expr& f] @@ -1620,6 +1635,10 @@ bvNegTerm[CVC4::Expr& f] /* BV neg */ : BVNEG_TOK bvNegTerm[f] { f = MK_EXPR(CVC4::kind::BITVECTOR_NOT, f); } + | TRANSPOSE_TOK bvNegTerm[f] + { f = MK_EXPR(CVC4::kind::TRANSPOSE, f); } + | TRANSCLOSURE_TOK bvNegTerm[f] + { f = MK_EXPR(CVC4::kind::TRANSCLOSURE, f); } | postfixTerm[f] ; diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 25f958963..db4949c1f 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -738,6 +738,22 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo op << "IS_IN"; opType = INFIX; break; + case kind::PRODUCT: + op << "PRODUCT"; + opType = INFIX; + break; + case kind::JOIN: + op << "JOIN"; + opType = INFIX; + break; + case kind::TRANSPOSE: + op << "TRANSPOSE"; + opType = PREFIX; + break; + case kind::TRANSCLOSURE: + op << "TRANSCLOSURE"; + opType = PREFIX; + break; case kind::SINGLETON: out << "{"; toStream(out, n[0], depth, types, false); diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds index a43902b1b..6767de481 100644 --- a/src/theory/sets/kinds +++ b/src/theory/sets/kinds @@ -43,6 +43,11 @@ operator MEMBER 2 "set membership predicate; first parameter a member of operator SINGLETON 1 "the set of the single element given as a parameter" operator INSERT 2: "set obtained by inserting elements (first N-1 parameters) into a set (the last parameter)" +operator JOIN 2 "set join" +operator PRODUCT 2 "set cartesian product" +operator TRANSPOSE 1 "set transpose" +operator TRANSCLOSURE 1 "set transitive closure" + typerule UNION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule typerule INTERSECTION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule typerule SETMINUS ::CVC4::theory::sets::SetsBinaryOperatorTypeRule @@ -52,10 +57,20 @@ typerule SINGLETON ::CVC4::theory::sets::SingletonTypeRule typerule EMPTYSET ::CVC4::theory::sets::EmptySetTypeRule 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 + construle UNION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule construle INTERSECTION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule construle SETMINUS ::CVC4::theory::sets::SetsBinaryOperatorTypeRule construle SINGLETON ::CVC4::theory::sets::SingletonTypeRule 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 + endtheory diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index d0866e537..c7f34bb52 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -93,6 +93,8 @@ void TheorySetsPrivate::check(Theory::Effort level) { // and that leads to conflict (externally). if(d_conflict) { return; } Debug("sets") << "[sets] is complete = " << isComplete() << std::endl; + + d_rels->check(level); } if( (level == Theory::EFFORT_FULL || options::setsEagerLemmas() ) && !isComplete()) { @@ -1105,9 +1107,11 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external, d_modelCache(c), d_ccg_i(c), d_ccg_j(c), - d_scrutinize(NULL) + d_scrutinize(NULL), + d_rels(NULL) { d_termInfoManager = new TermInfoManager(*this, c, &d_equalityEngine); + d_rels = new TheorySetsRels(&d_equalityEngine); d_equalityEngine.addFunctionKind(kind::UNION); d_equalityEngine.addFunctionKind(kind::INTERSECTION); @@ -1125,6 +1129,7 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external, TheorySetsPrivate::~TheorySetsPrivate() { delete d_termInfoManager; + delete d_rels; if( Debug.isOn("sets-scrutinize") ) { Assert(d_scrutinize != NULL); delete d_scrutinize; diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index ad273c546..8cbc17ae3 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -25,6 +25,7 @@ #include "theory/theory.h" #include "theory/uf/equality_engine.h" #include "theory/sets/term_info.h" +#include "theory/sets/theory_sets_rels.h" namespace CVC4 { namespace theory { @@ -70,6 +71,7 @@ public: private: TheorySets& d_external; + TheorySetsRels* d_rels; class Statistics { public: diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp new file mode 100644 index 000000000..7ed0ada32 --- /dev/null +++ b/src/theory/sets/theory_sets_rels.cpp @@ -0,0 +1,111 @@ +/********************* */ +/*! \file theory_sets_rels.cpp + ** \verbatim + ** Original author: Paul Meng + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Sets theory implementation. + ** + ** Extension to Sets theory. + **/ + +#include "theory/sets/theory_sets_rels.h" + +//#include "expr/emptyset.h" +//#include "options/sets_options.h" +//#include "smt/smt_statistics_registry.h" +//#include "theory/sets/expr_patterns.h" // ONLY included here +//#include "theory/sets/scrutinize.h" +//#include "theory/sets/theory_sets.h" +//#include "theory/theory_model.h" +//#include "util/result.h" + + +using namespace std; +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace sets { + + TheorySetsRels::TheorySetsRels(eq::EqualityEngine* eq): + d_eqEngine(eq) + { + d_eqEngine->addFunctionKind(kind::PRODUCT); + d_eqEngine->addFunctionKind(kind::JOIN); + d_eqEngine->addFunctionKind(kind::TRANSPOSE); + d_eqEngine->addFunctionKind(kind::TRANSCLOSURE); + } + + TheorySetsRels::TheorySetsRels::~TheorySetsRels() {} + + void TheorySetsRels::TheorySetsRels::check(Theory::Effort level) { + + Debug("rels") << "\nStart iterating equivalence class......\n" << std::endl; + + if (!d_eqEngine->consistent()) + return; + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( d_eqEngine ); + + std::map< TypeNode, int > typ_num; + while( !eqcs_i.isFinished() ){ + TNode r = (*eqcs_i); + TypeNode tr = r.getType(); + if( typ_num.find( tr )==typ_num.end() ){ + typ_num[tr] = 0; + } + typ_num[tr]++; + bool firstTime = true; + Debug("rels") << " " << r; + Debug("rels") << " : { "; + eq::EqClassIterator eqc_i = eq::EqClassIterator( r, d_eqEngine ); + while( !eqc_i.isFinished() ){ + TNode n = (*eqc_i); + if( r!=n ){ + if( firstTime ){ + Debug("rels") << std::endl; + firstTime = false; + } + if (n.getKind() == kind::PRODUCT || + n.getKind() == kind::JOIN || + n.getKind() == kind::TRANSCLOSURE || + n.getKind() == kind::TRANSPOSE) { + Debug("rels") << " " << n << std::endl; + } + } + ++eqc_i; + } + if( !firstTime ){ Debug("rels") << " "; } + Debug("rels") << "}" << std::endl; + ++eqcs_i; + } + } +} +} +} + + + + + + + + + + + + + + + + + + + + + diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h new file mode 100644 index 000000000..d83fd59c2 --- /dev/null +++ b/src/theory/sets/theory_sets_rels.h @@ -0,0 +1,47 @@ +/********************* */ +/*! \file theory_sets_rels.h + ** \verbatim + ** Original author: Paul Meng + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Sets theory implementation. + ** + ** Extension to Sets theory. + **/ + +#ifndef SRC_THEORY_SETS_THEORY_SETS_RELS_H_ +#define SRC_THEORY_SETS_THEORY_SETS_RELS_H_ + +#include "theory/theory.h" +#include "theory/uf/equality_engine.h" + +namespace CVC4 { +namespace theory { +namespace sets { + +class TheorySetsRels { + +public: + TheorySetsRels(eq::EqualityEngine*); + + ~TheorySetsRels(); + + void check(Theory::Effort); + +private: + + eq::EqualityEngine *d_eqEngine; +}; + +}/* CVC4::theory::sets namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + + + +#endif /* SRC_THEORY_SETS_THEORY_SETS_RELS_H_ */ diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h index d0e1f18f1..3b0fabf59 100644 --- a/src/theory/sets/theory_sets_type_rules.h +++ b/src/theory/sets/theory_sets_type_rules.h @@ -164,6 +164,80 @@ struct InsertTypeRule { } };/* struct InsertTypeRule */ +struct RelBinaryOperatorTypeRule { + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + Assert(n.getKind() == kind::PRODUCT || + n.getKind() == kind::JOIN); + + TypeNode firstRelType = n[0].getType(check); + TypeNode secondRelType = n[1].getType(check); + + if(check) { + if(!firstRelType.isSet() || !secondRelType.isSet()) { + throw TypeCheckingExceptionPrivate(n, " set operator operates on non-sets"); + } + if(!firstRelType[0].isTuple() || !secondRelType[0].isTuple()) { + throw TypeCheckingExceptionPrivate(n, " set operator operates on non-relations (sets of tuples)"); + } + // JOIN is applied on two sets of tuples that are not both unary + if(n.getKind() == kind::JOIN) { + if((firstRelType[0].getNumChildren() == 1) && (secondRelType[0].getNumChildren() == 1)) { + throw TypeCheckingExceptionPrivate(n, " Join operates on two unary relations"); + } + } + } + + Assert(firstRelType == secondRelType); + return firstRelType; + } + + inline static bool computeIsConst(NodeManager* nodeManager, TNode n) { + Assert(n.getKind() == kind::JOIN || + n.getKind() == kind::PRODUCT); + return false; + } +};/* struct RelBinaryOperatorTypeRule */ + +struct RelTransposeTypeRule { + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + Assert(n.getKind() == kind::TRANSPOSE); + TypeNode setType = n[0].getType(check); + if(check && !setType.isSet()) { + throw TypeCheckingExceptionPrivate(n, "relation transpose operats on non-rel"); + } + return setType; + } + + inline static bool computeIsConst(NodeManager* nodeManager, TNode n) { + //Assert(n.getKind() == kind::TRANSCLOSURE); + return false; + } +};/* struct RelTransposeTypeRule */ + +struct RelTransClosureTypeRule { + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + 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[0].getNumChildren() != 2) { + throw TypeCheckingExceptionPrivate(n, " transitive closure operates on non-binary relations"); + } + } + return setType; + } + + inline static bool computeIsConst(NodeManager* nodeManager, TNode n) { + Assert(n.getKind() == kind::TRANSCLOSURE); + return true; + } +};/* struct RelTransClosureTypeRule */ + struct SetsProperties { inline static Cardinality computeCardinality(TypeNode type) { -- 2.30.2