mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

add tactic name

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-12-07 13:37:57 -08:00
parent e3bd5badf2
commit 9f2b18cac5
73 changed files with 218 additions and 63 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/tactic/core/blast_term_ite_tactic.cpp
View file

@ -171,6 +171,8 @@ public:
dealloc(m_imp);
}
char const* name() const override { return "blast_term_ite"; }
void updt_params(params_ref const & p) override {
m_params = p;
m_imp->m_rw.m_cfg.updt_params(p);

1
src/tactic/core/cofactor_term_ite_tactic.cpp
View file

@ -51,6 +51,7 @@ public:
}
~cofactor_term_ite_tactic() override {}
char const* name() const override { return "cofactor"; }
void updt_params(params_ref const & p) override { m_params = p; m_elim_ite.updt_params(p); }
void collect_param_descrs(param_descrs & r) override { m_elim_ite.collect_param_descrs(r); }

2
src/tactic/core/collect_statistics_tactic.cpp
View file

@ -53,6 +53,8 @@ public:
~collect_statistics_tactic() override {}
char const* name() const override { return "collect_statistics"; }
tactic * translate(ast_manager & m_) override {
return alloc(collect_statistics_tactic, m_, m_params);
}

2
src/tactic/core/ctx_simplify_tactic.h
View file

@ -49,6 +49,8 @@ public:
~ctx_simplify_tactic() override;
char const* name() const override { return "ctx_simplify"; }
void updt_params(params_ref const & p) override;
static void get_param_descrs(param_descrs & r);
void collect_param_descrs(param_descrs & r) override { get_param_descrs(r); }

2
src/tactic/core/der_tactic.cpp
View file

@ -68,6 +68,8 @@ public:
~der_tactic() override {
dealloc(m_imp);
}
char const* name() const override { return "der"; }
void operator()(goal_ref const & in,
goal_ref_buffer & result) override {

2
src/tactic/core/distribute_forall_tactic.cpp
View file

@ -102,6 +102,8 @@ public:
return alloc(distribute_forall_tactic);
}
char const* name() const override { return "distribute_forall"; }
void operator()(goal_ref const & g,
goal_ref_buffer & result) override {
ast_manager & m = g->m();

1
src/tactic/core/dom_simplify_tactic.cpp
View file

@ -182,6 +182,7 @@ tactic * dom_simplify_tactic::translate(ast_manager & m) {
return alloc(dom_simplify_tactic, m, m_simplifier->translate(m), m_params);
}
void dom_simplify_tactic::operator()(goal_ref const & in, goal_ref_buffer & result) {
tactic_report report("dom-simplify", *in.get());
simplify_goal(*(in.get()));

2
src/tactic/core/dom_simplify_tactic.h
View file

@ -131,6 +131,8 @@ public:
~dom_simplify_tactic() override;
char const* dom_simplify_tactic::name() const { return "dom_simplify"; }
tactic * translate(ast_manager & m) override;
void updt_params(params_ref const & p) override {}
static void get_param_descrs(param_descrs & r) {}

2
src/tactic/core/elim_term_ite_tactic.cpp
View file

@ -136,6 +136,8 @@ public:
dealloc(m_imp);
}
char const* name() const override { return "elim_term_ite"; }
tactic * translate(ast_manager & m) override {
return alloc(elim_term_ite_tactic, m, m_params);
}

2
src/tactic/core/elim_uncnstr_tactic.cpp
View file

@ -853,6 +853,8 @@ public:
updt_params(p);
}
char const* name() const override { return "elim_uncstr"; }
tactic * translate(ast_manager & m) override {
return alloc(elim_uncnstr_tactic, m, m_params);
}

2
src/tactic/core/injectivity_tactic.cpp
View file

@ -255,6 +255,8 @@ public:
dealloc(m_map);
}
char const* name() const override { return "injectivity"; }
void updt_params(params_ref const & p) override {
m_params = p;
m_finder->updt_params(p);

2
src/tactic/core/nnf_tactic.cpp
View file

@ -49,6 +49,8 @@ public:
~nnf_tactic() override {}
char const* name() const override { return "nnf"; }
void updt_params(params_ref const & p) override { m_params = p; }
void collect_param_descrs(param_descrs & r) override { nnf::get_param_descrs(r); }

2
src/tactic/core/occf_tactic.cpp
View file

@ -196,6 +196,8 @@ public:
dealloc(m_imp);
}
char const* name() const override { return "occf"; }
void updt_params(params_ref const & p) override {}
void collect_param_descrs(param_descrs & r) override {}

2
src/tactic/core/pb_preprocess_tactic.cpp
View file

@ -107,6 +107,8 @@ public:
tactic * translate(ast_manager & m) override {
return alloc(pb_preprocess_tactic, m);
}
char const* name() const override { return "pb_preprocess"; }
void operator()(
goal_ref const & g,

2
src/tactic/core/propagate_values_tactic.cpp
View file

@ -216,6 +216,8 @@ public:
return alloc(propagate_values_tactic, m, m_params);
}
char const* name() const override { return "propagate_values"; }
void updt_params(params_ref const & p) override {
m_params = p;
m_r.updt_params(p);

102
src/tactic/core/reduce_args_tactic.cpp
View file

@ -73,6 +73,8 @@ public:
}
~reduce_args_tactic() override;
char const* name() const override { return "reduce_args"; }
void operator()(goal_ref const & g, goal_ref_buffer & result) override;
void cleanup() override;
@ -86,15 +88,14 @@ tactic * mk_reduce_args_tactic(ast_manager & m, params_ref const & p) {
struct reduce_args_tactic::imp {
expr_ref_vector m_vars;
ast_manager & m_manager;
ast_manager & m;
bv_util m_bv;
array_util m_ar;
ast_manager & m() const { return m_manager; }
imp(ast_manager & m):
m_vars(m),
m_manager(m),
m(m),
m_bv(m),
m_ar(m) {
}
@ -120,17 +121,17 @@ struct reduce_args_tactic::imp {
}
void checkpoint() {
tactic::checkpoint(m_manager);
tactic::checkpoint(m);
}
struct find_non_candidates_proc {
ast_manager & m_manager;
ast_manager & m;
bv_util & m_bv;
array_util & m_ar;
obj_hashtable<func_decl> & m_non_candidates;
find_non_candidates_proc(ast_manager & m, bv_util & bv, array_util& ar, obj_hashtable<func_decl> & non_candidates):
m_manager(m),
m(m),
m_bv(bv),
m_ar(ar),
m_non_candidates(non_candidates) {
@ -156,7 +157,7 @@ struct reduce_args_tactic::imp {
unsigned j = n->get_num_args();
while (j > 0) {
--j;
if (may_be_unique(m_manager, m_bv, n->get_arg(j)))
if (may_be_unique(m, m_bv, n->get_arg(j)))
return;
}
m_non_candidates.insert(d);
@ -172,7 +173,7 @@ struct reduce_args_tactic::imp {
for (expr* v : m_vars)
if (is_app(v))
non_candidates.insert(to_app(v)->get_decl());
find_non_candidates_proc proc(m_manager, m_bv, m_ar, non_candidates);
find_non_candidates_proc proc(m, m_bv, m_ar, non_candidates);
expr_fast_mark1 visited;
unsigned sz = g.size();
for (unsigned i = 0; i < sz; i++) {
@ -187,14 +188,14 @@ struct reduce_args_tactic::imp {
}
struct populate_decl2args_proc {
ast_manager & m_manager;
ast_manager & m;
bv_util & m_bv;
obj_hashtable<func_decl> & m_non_candidates;
obj_map<func_decl, bit_vector> & m_decl2args;
obj_map<func_decl, svector<expr*> > m_decl2base; // for args = base + offset
populate_decl2args_proc(ast_manager & m, bv_util & bv, obj_hashtable<func_decl> & nc, obj_map<func_decl, bit_vector> & d):
m_manager(m), m_bv(bv), m_non_candidates(nc), m_decl2args(d) {}
m(m), m_bv(bv), m_non_candidates(nc), m_decl2args(d) {}
void operator()(var * n) {}
void operator()(quantifier * n) {}
@ -218,7 +219,7 @@ struct reduce_args_tactic::imp {
it->m_value.reserve(j);
while (j > 0) {
--j;
it->m_value.set(j, may_be_unique(m_manager, m_bv, n->get_arg(j), base));
it->m_value.set(j, may_be_unique(m, m_bv, n->get_arg(j), base));
bases[j] = base;
}
} else {
@ -226,7 +227,7 @@ struct reduce_args_tactic::imp {
SASSERT(j == it->m_value.size());
while (j > 0) {
--j;
it->m_value.set(j, it->m_value.get(j) && may_be_unique(m_manager, m_bv, n->get_arg(j), base) && bases[j] == base);
it->m_value.set(j, it->m_value.get(j) && may_be_unique(m, m_bv, n->get_arg(j), base) && bases[j] == base);
}
}
}
@ -237,7 +238,7 @@ struct reduce_args_tactic::imp {
obj_map<func_decl, bit_vector> & decl2args) {
expr_fast_mark1 visited;
decl2args.reset();
populate_decl2args_proc proc(m_manager, m_bv, non_candidates, decl2args);
populate_decl2args_proc proc(m, m_bv, non_candidates, decl2args);
unsigned sz = g.size();
for (unsigned i = 0; i < sz; i++) {
checkpoint();
@ -246,28 +247,24 @@ struct reduce_args_tactic::imp {
// Remove all cases where the simplification is not applicable.
ptr_buffer<func_decl> bad_decls;
obj_map<func_decl, bit_vector>::iterator it = decl2args.begin();
obj_map<func_decl, bit_vector>::iterator end = decl2args.end();
for (; it != end; it++) {
for (auto const& [k, v] : decl2args) {
bool is_zero = true;
for (unsigned i = 0; i < it->m_value.size() && is_zero ; i++) {
if (it->m_value.get(i))
for (unsigned i = 0; i < v.size() && is_zero; i++) {
if (v.get(i))
is_zero = false;
}
if (is_zero)
bad_decls.push_back(it->m_key);
if (is_zero)
bad_decls.push_back(k);
}
ptr_buffer<func_decl>::iterator it2 = bad_decls.begin();
ptr_buffer<func_decl>::iterator end2 = bad_decls.end();
for (; it2 != end2; ++it2)
decl2args.erase(*it2);
for (func_decl* a : bad_decls)
decl2args.erase(a);
TRACE("reduce_args", tout << "decl2args:" << std::endl;
for (obj_map<func_decl, bit_vector>::iterator it = decl2args.begin() ; it != decl2args.end() ; it++) {
tout << it->m_key->get_name() << ": ";
for (unsigned i = 0 ; i < it->m_value.size() ; i++)
tout << (it->m_value.get(i) ? "1" : "0");
for (auto const& [k, v] : decl2args) {
tout << k->get_name() << ": ";
for (auto b : v)
tout << (b ? "1" : "0");
tout << std::endl;
});
}
@ -311,22 +308,17 @@ struct reduce_args_tactic::imp {
typedef obj_map<func_decl, arg2func *> decl2arg2func_map;
struct reduce_args_ctx {
ast_manager & m_manager;
ast_manager & m;
decl2arg2func_map m_decl2arg2funcs;
reduce_args_ctx(ast_manager & m): m_manager(m) {
reduce_args_ctx(ast_manager & m): m(m) {
}
~reduce_args_ctx() {
obj_map<func_decl, arg2func *>::iterator it = m_decl2arg2funcs.begin();
obj_map<func_decl, arg2func *>::iterator end = m_decl2arg2funcs.end();
for (; it != end; ++it) {
arg2func * map = it->m_value;
arg2func::iterator it2 = map->begin();
arg2func::iterator end2 = map->end();
for (; it2 != end2; ++it2) {
m_manager.dec_ref(it2->m_key);
m_manager.dec_ref(it2->m_value);
for (auto const& [_, map] : m_decl2arg2funcs) {
for (auto const& [k, v] : *map) {
m.dec_ref(k);
m.dec_ref(v);
}
dealloc(map);
}
@ -340,7 +332,7 @@ struct reduce_args_tactic::imp {
decl2arg2func_map & m_decl2arg2funcs;
reduce_args_rw_cfg(imp & owner, obj_map<func_decl, bit_vector> & decl2args, decl2arg2func_map & decl2arg2funcs):
m(owner.m_manager),
m(owner.m),
m_owner(owner),
m_decl2args(decl2args),
m_decl2arg2funcs(decl2arg2funcs) {
@ -396,16 +388,16 @@ struct reduce_args_tactic::imp {
reduce_args_rw_cfg m_cfg;
public:
reduce_args_rw(imp & owner, obj_map<func_decl, bit_vector> & decl2args, decl2arg2func_map & decl2arg2funcs):
rewriter_tpl<reduce_args_rw_cfg>(owner.m_manager, false, m_cfg),
rewriter_tpl<reduce_args_rw_cfg>(owner.m, false, m_cfg),
m_cfg(owner, decl2args, decl2arg2funcs) {
}
};
model_converter * mk_mc(obj_map<func_decl, bit_vector> & decl2args, decl2arg2func_map & decl2arg2funcs) {
ptr_buffer<expr> new_args;
var_ref_vector new_vars(m_manager);
var_ref_vector new_vars(m);
ptr_buffer<expr> new_eqs;
generic_model_converter * f_mc = alloc(generic_model_converter, m_manager, "reduce_args");
generic_model_converter * f_mc = alloc(generic_model_converter, m, "reduce_args");
for (auto const& kv : decl2arg2funcs) {
func_decl * f = kv.m_key;
arg2func * map = kv.m_value;
@ -415,18 +407,14 @@ struct reduce_args_tactic::imp {
new_vars.reset();
new_args.reset();
for (unsigned i = 0; i < f->get_arity(); i++) {
new_vars.push_back(m_manager.mk_var(i, f->get_domain(i)));
new_vars.push_back(m.mk_var(i, f->get_domain(i)));
if (!bv.get(i))
new_args.push_back(new_vars.back());
}
arg2func::iterator it2 = map->begin();
arg2func::iterator end2 = map->end();
for (; it2 != end2; ++it2) {
app * t = it2->m_key;
func_decl * new_def = it2->m_value;
for (auto const& [t, new_def] : *map) {
f_mc->hide(new_def);
SASSERT(new_def->get_arity() == new_args.size());
app * new_t = m_manager.mk_app(new_def, new_args.size(), new_args.data());
app * new_t = m.mk_app(new_def, new_args.size(), new_args.data());
if (def == nullptr) {
def = new_t;
}
@ -434,15 +422,15 @@ struct reduce_args_tactic::imp {
new_eqs.reset();
for (unsigned i = 0; i < f->get_arity(); i++) {
if (bv.get(i))
new_eqs.push_back(m_manager.mk_eq(new_vars.get(i), t->get_arg(i)));
new_eqs.push_back(m.mk_eq(new_vars.get(i), t->get_arg(i)));
}
SASSERT(new_eqs.size() > 0);
expr * cond;
if (new_eqs.size() == 1)
cond = new_eqs[0];
else
cond = m_manager.mk_and(new_eqs.size(), new_eqs.data());
def = m_manager.mk_ite(cond, new_t, def);
cond = m.mk_and(new_eqs.size(), new_eqs.data());
def = m.mk_ite(cond, new_t, def);
}
}
SASSERT(def);
@ -464,7 +452,7 @@ struct reduce_args_tactic::imp {
if (decl2args.empty())
return;
reduce_args_ctx ctx(m_manager);
reduce_args_ctx ctx(m);
reduce_args_rw rw(*this, decl2args, ctx.m_decl2arg2funcs);
unsigned sz = g.size();
@ -472,7 +460,7 @@ struct reduce_args_tactic::imp {
if (g.inconsistent())
break;
expr * f = g.form(i);
expr_ref new_f(m_manager);
expr_ref new_f(m);
rw(f, new_f);
g.update(i, new_f);
}
@ -499,7 +487,7 @@ void reduce_args_tactic::operator()(goal_ref const & g,
goal_ref_buffer & result) {
fail_if_unsat_core_generation("reduce-args", g);
result.reset();
if (!m_imp->m().proofs_enabled()) {
if (!m_imp->m.proofs_enabled()) {
m_imp->operator()(*(g.get()));
}
g->inc_depth();
@ -507,7 +495,7 @@ void reduce_args_tactic::operator()(goal_ref const & g,
}
void reduce_args_tactic::cleanup() {
ast_manager & m = m_imp->m();
ast_manager & m = m_imp->m;
expr_ref_vector vars = m_imp->m_vars;
m_imp->~imp();
m_imp = new (m_imp) imp(m);

2
src/tactic/core/reduce_invertible_tactic.cpp
View file

@ -47,6 +47,8 @@ public:
~reduce_invertible_tactic() override { }
char const* name() const override { return "reduce_invertible"; }
tactic * translate(ast_manager & m) override {
return alloc(reduce_invertible_tactic, m);
}

2
src/tactic/core/simplify_tactic.h
View file

@ -43,6 +43,8 @@ public:
tactic * translate(ast_manager & m) override { return alloc(simplify_tactic, m, m_params); }
char const* name() const override { return "simplify"; }
};
tactic * mk_simplify_tactic(ast_manager & m, params_ref const & p = params_ref());

2
src/tactic/core/solve_eqs_tactic.cpp
View file

@ -1089,6 +1089,8 @@ public:
dealloc(m_imp);
}
char const* name() const override { return "solve_eqs"; }
void updt_params(params_ref const & p) override {
m_params = p;
m_imp->updt_params(p);

2
src/tactic/core/special_relations_tactic.h
View file

@ -59,6 +59,8 @@ public:
tactic * translate(ast_manager & m) override { return alloc(special_relations_tactic, m, m_params); }
char const* name() const override { return "special_relations"; }
};
tactic * mk_special_relations_tactic(ast_manager & m, params_ref const & p = params_ref());

2
src/tactic/core/split_clause_tactic.cpp
View file

@ -91,6 +91,8 @@ public:
~split_clause_tactic() override {
}
char const* name() const override { return "split_clause"; }
void updt_params(params_ref const & p) override {
m_largest_clause = p.get_bool("split_largest_clause", false);
}

2
src/tactic/core/symmetry_reduce_tactic.cpp
View file

@ -37,6 +37,8 @@ public:
}
~symmetry_reduce_tactic() override;
char const* name() const override { return "symmetry_reduce"; }
void operator()(goal_ref const & g,
goal_ref_buffer & result) override;

2
src/tactic/core/tseitin_cnf_tactic.cpp
View file

@ -891,6 +891,8 @@ public:
dealloc(m_imp);
}
char const* name() const override { return "tseitin_cnf"; }
void updt_params(params_ref const & p) override {
m_params = p;
m_imp->updt_params(p);