Fix type rule for relations join image (#6349)

The join image type rule restricted that an argument was a constant. This is a logic restriction that should not be a part of the type checker.

This is required for not throwing type checking exceptions during proof conversion to LFSC.

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index eea90da413601beda90015be03a796d71ea2193d..034af284808ec7f8579a72be043729d265fd1c92 100644 (file)
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -16,6 +16,7 @@
 #include "theory/sets/theory_sets_private.h"
 
 #include <algorithm>
+#include <climits>
 
 #include "expr/emptyset.h"
 #include "expr/node_algorithm.h"
@@ -1279,6 +1280,27 @@ void TheorySetsPrivate::preRegisterTerm(TNode node)
       d_equalityEngine->addTriggerPredicate(node);
     }
     break;
+    case kind::JOIN_IMAGE:
+    {
+      // these are logic exceptions, not type checking exceptions
+      if (node[1].getKind() != kind::CONST_RATIONAL)
+      {
+        throw LogicException(
+            "JoinImage cardinality constraint must be a constant");
+      }
+      cvc5::Rational r(INT_MAX);
+      if (node[1].getConst<Rational>() > r)
+      {
+        throw LogicException(
+            "JoinImage Exceeded INT_MAX in cardinality constraint");
+      }
+      if (node[1].getConst<Rational>().getNumerator().getSignedInt() < 0)
+      {
+        throw LogicException(
+            "JoinImage cardinality constraint must be non-negative");
+      }
+    }
+    break;
     default: d_equalityEngine->addTerm(node); break;
   }
 }

diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h
index ca89728d605f4f30e7388caeed625088bcce4350..94e18dc64bdf6990993d8de7c24cc2eb7caf7651 100644 (file)
--- a/src/theory/sets/theory_sets_type_rules.h
+++ b/src/theory/sets/theory_sets_type_rules.h
@@ -385,19 +385,6 @@ struct JoinImageTypeRule {
       throw TypeCheckingExceptionPrivate(
           n, " JoinImage cardinality constraint must be integer");
     }
-    if (n[1].getKind() != kind::CONST_RATIONAL) {
-      throw TypeCheckingExceptionPrivate(
-          n, " JoinImage cardinality constraint must be a constant");
-    }
-    cvc5::Rational r(INT_MAX);
-    if (n[1].getConst<Rational>() > r) {
-      throw TypeCheckingExceptionPrivate(
-          n, " JoinImage Exceeded INT_MAX in cardinality constraint");
-    }
-    if (n[1].getConst<Rational>().getNumerator().getSignedInt() < 0) {
-      throw TypeCheckingExceptionPrivate(
-          n, " JoinImage cardinality constraint must be non-negative");
-    }
     std::vector<TypeNode> newTupleTypes;
     newTupleTypes.push_back(tupleTypes[0]);
     return nodeManager->mkSetType(nodeManager->mkTupleType(newTupleTypes));