Proper error message for non-first-class sets (#8245)

Fixes cvc5/cvc5-projects#347.

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index b465c41623ad6f71f10505e98a5faedbd64e3042..7ed9dba51be08a83aaad2ceb39dfec657dbfa262 100644 (file)
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -1247,6 +1247,11 @@ Node mkAnd(const std::vector<TNode>& conjunctions)
 
 Valuation& TheorySetsPrivate::getValuation() { return d_external.d_valuation; }
 
+bool TheorySetsPrivate::isEntailed(Node n, bool pol)
+{
+  return d_state.isEntailed(n, pol);
+}
+
 Node TheorySetsPrivate::explain(TNode literal)
 {
   Debug("sets") << "TheorySetsPrivate::explain(" << literal << ")" << std::endl;
@@ -1277,6 +1282,11 @@ void TheorySetsPrivate::preRegisterTerm(TNode node)
 {
   Debug("sets") << "TheorySetsPrivate::preRegisterTerm(" << node << ")"
                 << std::endl;
+  TypeNode tn = node.getType();
+  if (tn.isSet())
+  {
+    ensureFirstClassSetType(tn);
+  }
   switch (node.getKind())
   {
     case kind::EQUAL:
@@ -1369,6 +1379,7 @@ TrustNode TheorySetsPrivate::expandChooseOperator(
   SkolemManager* sm = nm->getSkolemManager();
   Node A = node[0];
   TypeNode setType = A.getType();
+  ensureFirstClassSetType(setType);
   TypeNode ufType = nm->mkFunctionType(setType, setType.getSetElementType());
   // a Null node is used here to get a unique skolem function per set type
   Node uf = sm->mkSkolemFunction(SkolemFunId::SETS_CHOOSE, ufType, Node());
@@ -1414,6 +1425,7 @@ TrustNode TheorySetsPrivate::expandIsSingletonOperator(const Node& node)
   }
 
   TypeNode setType = set.getType();
+  ensureFirstClassSetType(setType);
   Node boundVar = nm->mkBoundVar(setType.getSetElementType());
   Node singleton = nm->mkSingleton(setType.getSetElementType(), boundVar);
   Node equal = set.eqNode(singleton);
@@ -1425,6 +1437,18 @@ TrustNode TheorySetsPrivate::expandIsSingletonOperator(const Node& node)
   return TrustNode::mkTrustRewrite(node, exists, nullptr);
 }
 
+void TheorySetsPrivate::ensureFirstClassSetType(TypeNode tn) const
+{
+  Assert(tn.isSet());
+  if (!tn.getSetElementType().isFirstClass())
+  {
+    std::stringstream ss;
+    ss << "Cannot handle sets of non-first class types, offending set type is "
+       << tn;
+    throw LogicException(ss.str());
+  }
+}
+
 void TheorySetsPrivate::presolve() { d_state.reset(); }
 
 }  // namespace sets

diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index a2564b2de4e7ebcbbd21d12ca0c75f7c0ab3600a..c75f1a24fd0c653873b13c4c2c074b100e6b938b 100644 (file)
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -179,6 +179,9 @@ class TheorySetsPrivate : protected EnvObj
 
   /** get the valuation */
   Valuation& getValuation();
+  /** Is formula n entailed to have polarity pol in the current context? */
+  bool isEntailed(Node n, bool pol);
+
  private:
   TheorySets& d_external;
   /** The state of the sets solver at full effort */
@@ -195,17 +198,14 @@ class TheorySetsPrivate : protected EnvObj
 
   bool isCareArg( Node n, unsigned a );
 
- public:
-  /** Is formula n entailed to have polarity pol in the current context? */
-  bool isEntailed(Node n, bool pol) { return d_state.isEntailed(n, pol); }
-
- private:
-
   /** expand the definition of the choose operator */
   TrustNode expandChooseOperator(const Node& node,
                                  std::vector<SkolemLemma>& lems);
   /** expand the definition of is_singleton operator */
   TrustNode expandIsSingletonOperator(const Node& node);
+  /** ensure that the set type is over first class type, throw logic exception
+   * if not */
+  void ensureFirstClassSetType(TypeNode tn) const;
   /** subtheory solver for the theory of relations */
   std::unique_ptr<TheorySetsRels> d_rels;
   /** subtheory solver for the theory of sets with cardinality */