mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-04 13:21:22 +00:00
Code Activity

Made ufbv-rewriter tactic public

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-01-28 11:14:01 +00:00
parent 4dba5270ad
commit 5f0ea74e89
2 changed files with 12 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/tactic/ufbv/ufbv_rewriter_tactic.cpp
View file

@ -75,7 +75,7 @@ class ufbv_rewriter_tactic : public tactic {
void updt_params(params_ref const & p) { void updt_params(params_ref const & p) {
} }
}; };
imp * m_imp; imp * m_imp;
params_ref m_params; params_ref m_params;
@ -88,7 +88,7 @@ public:
virtual tactic * translate(ast_manager & m) { virtual tactic * translate(ast_manager & m) {
return alloc(ufbv_rewriter_tactic, m, m_params); return alloc(ufbv_rewriter_tactic, m, m_params);
} }
virtual ~ufbv_rewriter_tactic() { virtual ~ufbv_rewriter_tactic() {
dealloc(m_imp); dealloc(m_imp);
} }
@ -103,19 +103,19 @@ public:
insert_produce_models(r); insert_produce_models(r);
insert_produce_proofs(r); insert_produce_proofs(r);
} }
virtual void operator()(goal_ref const & in, virtual void operator()(goal_ref const & in,
goal_ref_buffer & result, goal_ref_buffer & result,
model_converter_ref & mc, model_converter_ref & mc,
proof_converter_ref & pc, proof_converter_ref & pc,
expr_dependency_ref & core) { expr_dependency_ref & core) {
(*m_imp)(in, result, mc, pc, core); (*m_imp)(in, result, mc, pc, core);
} }
virtual void cleanup() { virtual void cleanup() {
ast_manager & m = m_imp->m(); ast_manager & m = m_imp->m();
imp * d = alloc(imp, m, m_params); imp * d = alloc(imp, m, m_params);
std::swap(d, m_imp); std::swap(d, m_imp);
dealloc(d); dealloc(d);
} }

4
src/tactic/ufbv/ufbv_rewriter_tactic.h
View file

@ -25,4 +25,8 @@ class tactic;
tactic * mk_ufbv_rewriter_tactic(ast_manager & m, params_ref const & p = params_ref()); tactic * mk_ufbv_rewriter_tactic(ast_manager & m, params_ref const & p = params_ref());
/*
ADD_TACTIC("ufbv-rewriter", "Applies UFBV-specific rewriting rules, mainly demodulation.", "mk_quasi_macros_tactic(m, p)")
*/
#endif #endif