Add set.map signature to lfsc (#8860)

Fix buildbot failure

diff --git a/proofs/lfsc/signatures/theory_def.plf b/proofs/lfsc/signatures/theory_def.plf
index eb2c34991486a45e16df387d5e39fa1bfab3e7bb..df0abe39594164a8575126b2cf0bb2fae5f99ebe 100644 (file)
--- a/proofs/lfsc/signatures/theory_def.plf
+++ b/proofs/lfsc/signatures/theory_def.plf
@@ -485,6 +485,8 @@
 (define rel.join_image (# x term (# y term (apply (apply f_rel.join_image x) y))))
 (declare f_set.insert term)
 (define set.insert (# x term (# y term (apply (apply f_set.insert x) y))))
+(declare f_set.map term)
+(define set.map (# x term (# y term (apply (apply f_set.map x) y))))
 
 ;; ---- Bags
 (declare bag.empty (! s sort term))

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index aceaafe74406577b41ef900bb73cd02263cc76b8..4aae37ecfcf3440be83a5be82a0f7e3a14b8fcfa 100644 (file)
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -57,6 +57,7 @@ TheorySetsPrivate::TheorySetsPrivate(Env& env,
       d_cardSolver(new CardinalityExtension(d_env, state, im, d_treg)),
       d_rels_enabled(false),
       d_card_enabled(false),
+      d_higher_order_kinds_enabled(false),
       d_cpacb(cpacb)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
@@ -198,6 +199,7 @@ void TheorySetsPrivate::fullEffortReset()
   Assert(d_equalityEngine->consistent());
   d_fullCheckIncomplete = false;
   d_fullCheckIncompleteId = IncompleteId::UNKNOWN;
+  d_higher_order_kinds_enabled = false;
   d_card_enabled = false;
   d_rels_enabled = false;
   // reset the state object