Add documentation for theory_bags_type_rules.h (#7642)

This PR adds documentation for theory_bags_type_rules.h, and updates the type rule for rel.join_image to ensure tuple elements in the binary relation have the same sort.

diff --git a/src/theory/bags/theory_bags_type_rules.h b/src/theory/bags/theory_bags_type_rules.h
index 3bc3b34628d4da127a4ad0df384179052f563db6..d7b8b27377782a0000268cf677d0db50fbb2edef 100644 (file)
--- a/src/theory/bags/theory_bags_type_rules.h
+++ b/src/theory/bags/theory_bags_type_rules.h
@@ -31,7 +31,7 @@ namespace bags {
 /**
  * Type rule for binary operators (bag.union_max, bag.union_disjoint,
  * bag.inter_min bag.difference_subtract, bag.difference_remove) to check
- * if the two arguments are of the same sort.
+ * if the two arguments are bags of the same sort.
  */
 struct BinaryOperatorTypeRule
 {
@@ -40,8 +40,8 @@ struct BinaryOperatorTypeRule
 }; /* struct BinaryOperatorTypeRule */
 
 /**
- * Type rule for binary operator bag.subbag to check if the two arguments have
- * the same sort.
+ * Type rule for binary operator bag.subbag to check if the two arguments are
+ * bags of the same sort.
  */
 struct SubBagTypeRule
 {
@@ -76,7 +76,7 @@ struct BagMakeTypeRule
 }; /* struct BagMakeTypeRule */
 
 /**
- * Type rule for bag.is_singleton to check the argument is of a bag.
+ * Type rule for (bag.is_singleton B) to check the argument B is a bag.
  */
 struct IsSingletonTypeRule
 {
@@ -84,7 +84,7 @@ struct IsSingletonTypeRule
 }; /* struct IsSingletonTypeRule */
 
 /**
- * Type rule for (as bag.empty (Bag ...))
+ * Type rule for (as bag.empty (Bag T)) where T is a type
  */
 struct EmptyBagTypeRule
 {
@@ -92,7 +92,7 @@ struct EmptyBagTypeRule
 }; /* struct EmptyBagTypeRule */
 
 /**
- * Type rule for (bag.card ..) to check the argument is of a bag.
+ * Type rule for (bag.card B) to check the argument B is a bag.
  */
 struct CardTypeRule
 {
@@ -100,7 +100,7 @@ struct CardTypeRule
 }; /* struct CardTypeRule */
 
 /**
- * Type rule for (bag.choose ..) to check the argument is of a bag.
+ * Type rule for (bag.choose B) to check the argument B is a bag.
  */
 struct ChooseTypeRule
 {

diff --git a/src/theory/sets/singleton_op.cpp b/src/theory/sets/singleton_op.cpp
index fb64b01cdb987ed8faf92bb9c0d149a3d2f7449c..327df69841ecd169226793e3defd79ae0f96a048 100644 (file)
--- a/src/theory/sets/singleton_op.cpp
+++ b/src/theory/sets/singleton_op.cpp
@@ -23,7 +23,7 @@ namespace cvc5 {
 
 std::ostream& operator<<(std::ostream& out, const SetSingletonOp& op)
 {
-  return out << "(singleton_op " << op.getType() << ')';
+  return out << "(SetSingletonOp " << op.getType() << ')';
 }
 
 size_t SetSingletonOpHashFunction::operator()(const SetSingletonOp& op) const

diff --git a/src/theory/sets/theory_sets_type_rules.cpp b/src/theory/sets/theory_sets_type_rules.cpp
index 8101661bd18f4570c6e5d2540e693c8e49cd27f7..a8a79d5f9bfe36c5efcc36212c07e2712c82e27f 100644 (file)
--- a/src/theory/sets/theory_sets_type_rules.cpp
+++ b/src/theory/sets/theory_sets_type_rules.cpp
@@ -131,7 +131,7 @@ TypeNode SingletonTypeRule::computeType(NodeManager* nodeManager,
     TypeNode type2 = n[0].getType(check);
     TypeNode leastCommonType = TypeNode::leastCommonTypeNode(type1, type2);
     // the type of the element should be a subtype of the type of the operator
-    // e.g. (singleton (singleton_op Real) 1) where 1 is an Int
+    // e.g. (set.singleton (SetSingletonOp Real) 1) where 1 is an Int
     if (leastCommonType.isNull() || leastCommonType != type1)
     {
       std::stringstream ss;
@@ -463,6 +463,13 @@ TypeNode JoinImageTypeRule::computeType(NodeManager* nodeManager,
     throw TypeCheckingExceptionPrivate(
         n, " JoinImage operates on a non-binary relation");
   }
+  if (tupleTypes[0] != tupleTypes[1])
+  {
+    // TODO: Investigate supporting JoinImage for general binary
+    // relationshttps://github.com/cvc5/cvc5-projects/issues/346
+    throw TypeCheckingExceptionPrivate(
+        n, " JoinImage operates on a pair of different types");
+  }
   TypeNode valType = n[1].getType(check);
   if (valType != nodeManager->integerType())
   {

diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h
index b793205c0483935d2d677d1a27ddf912ef85b68f..dc473d145a57e3ce7c60d793b4971bf3fff6995c 100644 (file)
--- a/src/theory/sets/theory_sets_type_rules.h
+++ b/src/theory/sets/theory_sets_type_rules.h
@@ -25,23 +25,38 @@ namespace cvc5 {
 namespace theory {
 namespace sets {
 
+/**
+ * Type rule for binary operators (set.union, set.inter_min, set.minus) to check
+ * if the two arguments are sets of the same sort.
+ */
 struct SetsBinaryOperatorTypeRule
 {
   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
-
   static bool computeIsConst(NodeManager* nodeManager, TNode n);
 };
 
+/**
+ * Type rule for binary operator set.subset to check if the two arguments are
+ * sets of the same sort.
+ */
 struct SubsetTypeRule
 {
   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
+/**
+ * Type rule for binary operator set.member to check the sort of the first
+ * argument matches the element sort of the given set.
+ */
 struct MemberTypeRule
 {
   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
+/**
+ * Type rule for (set.singleton (SetSingletonOp t) x) to check the sort of x
+ * matches the sort t.
+ */
 struct SingletonTypeRule
 {
   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
@@ -49,41 +64,68 @@ struct SingletonTypeRule
   static bool computeIsConst(NodeManager* nodeManager, TNode n);
 };
 
+/**
+ * Type rule for (as set.empty (Set T)) where T is a type
+ */
 struct EmptySetTypeRule
 {
   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
+/**
+ * Type rule for (bag.card A) to check the argument A is a set.
+ */
 struct CardTypeRule
 {
   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
+/**
+ * Type rule for (set.complement A) to check the argument A is a set.
+ */
 struct ComplementTypeRule
 {
   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
+/**
+ * Type rule for (as set.universe (Set T)) where T is a type
+ */
 struct UniverseSetTypeRule
 {
   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
+/**
+ * Type rule for (set.comprehension ((x1 T1) ... (xn Tn)) predicate body)
+ * that checks x1 ... xn are bound variables, predicate is a boolean term,
+ * and computes the type (Set T) where T is the type of body
+ */
 struct ComprehensionTypeRule
 {
   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
+/**
+ * Type rule for (set.choose A) to check the argument A is a set.
+ */
 struct ChooseTypeRule
 {
   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
+/**
+ * Type rule for (set.is_singleton A) to check the argument A is a set.
+ */
 struct IsSingletonTypeRule
 {
   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
+/**
+ * Type rule for (set.insert e1 ... en A) that checks the sorts of e1, ..., en
+ * match the element sort of the set A
+ */
 struct InsertTypeRule
 {
   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
@@ -98,26 +140,55 @@ struct SetMapTypeRule
   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 }; /* struct SetMapTypeRule */
 
+/**
+ * Type rule for binary operators (rel.join, rel.product) to check
+ * if the two arguments are relations (set of tuples).
+ * For arguments A of type (Set (Tuple A1 ... Am)) and B of type
+ * (Set (Tuple B1 ... Bn)):
+ * - (rel.product A B): it computes the type (Set (Tuple (A1 ... Am B1 ... Bn)).
+ * - (rel.join A B) it checks that m, n > 1 and Am = B1 and computes the type
+ *   (Set (Tuple (A1 ... Am-1 B2 ... Bn)).
+ */
 struct RelBinaryOperatorTypeRule
 {
   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
+/**
+ * Type rule for unary operator (rel.transpose A) to check that A is a relation
+ * (set of Tuples). For an argument A of type (Set (Tuple A1 ... An))
+ * it reveres A1 ... An and computes the type (Set (Tuple An ... A1)).
+ */
 struct RelTransposeTypeRule
 {
   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
+/**
+ * Type rule for unary operator (rel.tclosure A) to check that A is a binary
+ * relation of type (Set (Tuple T T)), where T is a type
+ */
 struct RelTransClosureTypeRule
 {
   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
+/**
+ * Type rule for operator (rel.join_image A c) that checks A is a binary
+ * relation of type (Set (Tuple T T)), where T is a type, and c is an integer
+ * term (in fact c should be a non-negative constant, otherwise a logic
+ * exception is thrown TheorySetsPrivate::preRegisterTerm).
+ */
 struct JoinImageTypeRule
 {
   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
+/**
+ * Type rule for unary operator (rel.iden A) to check that A is a unary relation
+ * of type (Set (Tuple T)) and computes the type (Set (Tuple T T)) for the
+ * identity
+ */
 struct RelIdenTypeRule
 {
   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);