summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@cs.nyu.edu>2012-12-06 18:42:43 -0500
committerFrançois Bobot <francois@bobot.eu>2012-12-07 09:28:04 +0100
commit5d0d0b56d1383f1ad4027d8e6dc739c12cacced8 (patch)
tree0e8fe5e6ea39492e716da1a450bc2f6d155ff4a5
parentbd28a94095d8aebe4eb70fedcbe0f511edd38b0b (diff)
Fix to portfolio builds
(cherry picked from commit f46ba71e78054af63b529eb3271952c55beba37e)
-rw-r--r--src/main/portfolio_util.h4
1 files changed, 4 insertions, 0 deletions
diff --git a/src/main/portfolio_util.h b/src/main/portfolio_util.h
index 80c653eca..eff8d6a7e 100644
--- a/src/main/portfolio_util.h
+++ b/src/main/portfolio_util.h
@@ -46,6 +46,8 @@ public:
cnt(0)
{}
+ ~PortfolioLemmaOutputChannel() throw() { }
+
void notifyNewLemma(Expr lemma) {
if(int(lemma.getNumChildren()) > options::sharingFilterByLength()) {
return;
@@ -84,6 +86,8 @@ public:
d_pickler(em, to, from){
}
+ ~PortfolioLemmaInputChannel() throw() { }
+
bool hasNewLemma(){
Debug("lemmaInputChannel") << d_tag << ": " << "hasNewLemma" << std::endl;
return !d_sharedChannel->empty();
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback