mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 09:35:32 +00:00
Code Activity

Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

Browse source
This commit is contained in:
Nikolaj Bjorner 2013-04-28 13:20:49 -07:00
commit e6d6c55df0
2 changed files with 8 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/muz_qe/dl_rule.cpp
View file

@ -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<rule_manager::remove_label_cfg>;
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 {
}
};

4
src/muz_qe/dl_rule.h
View file

@ -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);