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

Whitespace

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2017-08-24 18:33:21 +01:00
parent ed4477c9e4
commit 227e6801c2
1 changed files with 22 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

44
src/tactic/ufbv/macro_finder_tactic.cpp
View file

@ -26,24 +26,24 @@ Notes:
#include "tactic/extension_model_converter.h" #include "tactic/extension_model_converter.h"
#include "tactic/ufbv/macro_finder_tactic.h" #include "tactic/ufbv/macro_finder_tactic.h"
class macro_finder_tactic : public tactic { class macro_finder_tactic : public tactic {
struct imp { struct imp {
ast_manager & m_manager; ast_manager & m_manager;
bool m_elim_and; bool m_elim_and;
imp(ast_manager & m, params_ref const & p) : imp(ast_manager & m, params_ref const & p) :
m_manager(m), m_manager(m),
m_elim_and(false) { m_elim_and(false) {
updt_params(p); updt_params(p);
} }
ast_manager & m() const { return m_manager; } ast_manager & m() const { return m_manager; }
void operator()(goal_ref const & g, void operator()(goal_ref const & g,
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) {
SASSERT(g->is_well_sorted()); SASSERT(g->is_well_sorted());
@ -63,20 +63,20 @@ class macro_finder_tactic : public tactic {
bv_simplifier_params bv_params; bv_simplifier_params bv_params;
bv_simplifier_plugin * bvsimp = alloc(bv_simplifier_plugin, m_manager, *bsimp, bv_params); bv_simplifier_plugin * bvsimp = alloc(bv_simplifier_plugin, m_manager, *bsimp, bv_params);
simp.register_plugin(bvsimp); simp.register_plugin(bvsimp);
macro_manager mm(m_manager, simp); macro_manager mm(m_manager, simp);
macro_finder mf(m_manager, mm); macro_finder mf(m_manager, mm);
expr_ref_vector forms(m_manager), new_forms(m_manager); expr_ref_vector forms(m_manager), new_forms(m_manager);
proof_ref_vector proofs(m_manager), new_proofs(m_manager); proof_ref_vector proofs(m_manager), new_proofs(m_manager);
unsigned size = g->size(); unsigned size = g->size();
for (unsigned idx = 0; idx < size; idx++) { for (unsigned idx = 0; idx < size; idx++) {
forms.push_back(g->form(idx)); forms.push_back(g->form(idx));
proofs.push_back(g->pr(idx)); proofs.push_back(g->pr(idx));
} }
mf(forms.size(), forms.c_ptr(), proofs.c_ptr(), new_forms, new_proofs); mf(forms.size(), forms.c_ptr(), proofs.c_ptr(), new_forms, new_proofs);
g->reset(); g->reset();
for (unsigned i = 0; i < new_forms.size(); i++) for (unsigned i = 0; i < new_forms.size(); i++)
g->assert_expr(new_forms.get(i), produce_proofs ? new_proofs.get(i) : 0, 0); g->assert_expr(new_forms.get(i), produce_proofs ? new_proofs.get(i) : 0, 0);
@ -89,7 +89,7 @@ class macro_finder_tactic : public tactic {
evmc->insert(f, f_interp); evmc->insert(f, f_interp);
} }
mc = evmc; mc = evmc;
g->inc_depth(); g->inc_depth();
result.push_back(g.get()); result.push_back(g.get());
TRACE("macro-finder", g->display(tout);); TRACE("macro-finder", g->display(tout););
@ -102,7 +102,7 @@ class macro_finder_tactic : public tactic {
}; };
imp * m_imp; imp * m_imp;
params_ref m_params; params_ref m_params;
public: public:
macro_finder_tactic(ast_manager & m, params_ref const & p): macro_finder_tactic(ast_manager & m, params_ref const & p):
m_params(p) { m_params(p) {
@ -112,7 +112,7 @@ public:
virtual tactic * translate(ast_manager & m) { virtual tactic * translate(ast_manager & m) {
return alloc(macro_finder_tactic, m, m_params); return alloc(macro_finder_tactic, m, m_params);
} }
virtual ~macro_finder_tactic() { virtual ~macro_finder_tactic() {
dealloc(m_imp); dealloc(m_imp);
} }
@ -128,19 +128,19 @@ public:
insert_produce_proofs(r); insert_produce_proofs(r);
r.insert("elim_and", CPK_BOOL, "(default: false) eliminate conjunctions during (internal) calls to the simplifier."); r.insert("elim_and", CPK_BOOL, "(default: false) eliminate conjunctions during (internal) calls to the simplifier.");
} }
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);
} }