summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@cs.nyu.edu>2012-12-06 18:42:43 -0500
committerMorgan Deters <mdeters@cs.nyu.edu>2012-12-06 18:42:43 -0500
commitf46ba71e78054af63b529eb3271952c55beba37e (patch)
tree2f07a1f9fe44e088c3a9edaa8d7a45212fc83245 /src
parentf056522a587d1b080224992355be070b73d97a3b (diff)
Fix to portfolio builds
Diffstat (limited to 'src')
-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