From 4471d929f7c2b6b9409e37eec638cdb2b8afe98f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 28 Apr 2013 13:20:31 -0700 Subject: [PATCH] fix linking error in debug mode Signed-off-by: Nikolaj Bjorner --- src/muz_qe/dl_rule.cpp | 7 ++++++- src/muz_qe/dl_rule.h | 4 ++-- 2 files changed, 8 insertions(+), 3 deletions(-) diff --git a/src/muz_qe/dl_rule.cpp b/src/muz_qe/dl_rule.cpp index 1bbb1f342..db8189c64 100644 --- a/src/muz_qe/dl_rule.cpp +++ b/src/muz_qe/dl_rule.cpp @@ -72,6 +72,8 @@ namespace datalog { } } + rule_manager::remove_label_cfg::~remove_label_cfg() {} + br_status rule_manager::remove_label_cfg::reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { @@ -83,6 +85,9 @@ namespace datalog { return BR_FAILED; } + template class rewriter_tpl; + + void rule_manager::remove_labels(expr_ref& fml, proof_ref& pr) { expr_ref tmp(m); m_rwr(fml, tmp); @@ -1113,6 +1118,6 @@ namespace datalog { } - + }; diff --git a/src/muz_qe/dl_rule.h b/src/muz_qe/dl_rule.h index 6335c506f..77bf9ac74 100644 --- a/src/muz_qe/dl_rule.h +++ b/src/muz_qe/dl_rule.h @@ -53,8 +53,8 @@ namespace datalog { class remove_label_cfg : public default_rewriter_cfg { family_id m_label_fid; public: - remove_label_cfg(ast_manager& m): m_label_fid(m.get_label_family_id()) {} - virtual ~remove_label_cfg() {} + remove_label_cfg(ast_manager& m): m_label_fid(m.get_label_family_id()) {} + virtual ~remove_label_cfg(); br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr);