From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Sat, 26 Mar 2022 02:51:29 +0000 (-0500)
Subject: Throw logic exception for set.map (#8403)
X-Git-Tag: cvc5-1.0.0~160
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=aba70eb79f255582aa5c254518b3731f284ad0c4;p=cvc5.git

Throw logic exception for set.map (#8403)

Support parsing/rewriting, but not solving currently.
---

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 7a07ae996..099843e3c 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -1149,6 +1149,12 @@ void TheorySetsPrivate::preRegisterTerm(TNode node)
       }
     }
     break;
+    case kind::SET_MAP:
+    {
+        throw LogicException(
+            "set.map not currently supported by the sets theory solver");
+    }
+      break;
     default: d_equalityEngine->addTerm(node); break;
   }
 }