From: mudathirmahgoub <mudathirmahgoub@gmail.com>
Date: Tue, 7 Jun 2022 03:37:32 +0000 (-0500)
Subject: Add set.map signature to lfsc (#8860)
X-Git-Tag: cvc5-1.0.1~63
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d2f8c855f290f10545fc21444773c5506786a42b;p=cvc5.git

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 eb2c34991..df0abe395 100644
--- 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 aceaafe74..4aae37ecf 100644
--- 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