From: Tim King <taking@cs.nyu.edu>
Date: Thu, 29 Mar 2012 19:53:20 +0000 (+0000)
Subject: Fix for bug 316. If the flag @CVC4_TLS_SUPPORTED@ is false, function pointers cannot... 
X-Git-Tag: cvc5-1.0.0~8251
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=889d34864fb2218516fd18250e4f086213f14611;p=cvc5.git

Fix for bug 316. If the flag @CVC4_TLS_SUPPORTED@ is false, function pointers cannot be directly used with the CVC4_THREADLOCAL macro. This is why there were problems on macs.
---

diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 586f37073..2b48977b6 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -33,7 +33,7 @@ using namespace CVC4::theory::bv;
 
 // CVC4_THREADLOCAL(AllRewriteRules*) TheoryBVRewriter::s_allRules = NULL;
 // CVC4_THREADLOCAL(TimerStat*) TheoryBVRewriter::d_rewriteTimer = NULL;
-CVC4_THREADLOCAL(RewriteFunction) TheoryBVRewriter::d_rewriteTable[kind::LAST_KIND]; 
+RewriteFunction TheoryBVRewriter::d_rewriteTable[kind::LAST_KIND]; 
 void TheoryBVRewriter::init() {
    // s_allRules = new AllRewriteRules;
    // d_rewriteTimer = new TimerStat("theory::bv::rewriteTimer");
diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h
index e72c1a910..7ce914477 100644
--- a/src/theory/bv/theory_bv_rewriter.h
+++ b/src/theory/bv/theory_bv_rewriter.h
@@ -35,7 +35,9 @@ typedef RewriteResponse (*RewriteFunction) (TNode);
 class TheoryBVRewriter {
   // static CVC4_THREADLOCAL(AllRewriteRules*) s_allRules;
   // static CVC4_THREADLOCAL(TimerStat*) d_rewriteTimer; 
-  static CVC4_THREADLOCAL(RewriteFunction) d_rewriteTable[kind::LAST_KIND];
+
+#warning "TODO: Double check thread safety and make sure the fix compiles on mac."
+  static RewriteFunction d_rewriteTable[kind::LAST_KIND];
 
   static RewriteResponse IdentityRewrite(TNode node);
   static RewriteResponse UndefinedRewrite(TNode node);