- 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

9 files changed, 293 insertions, 2 deletions

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) {