mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-18 11:58:31 +00:00
Code Activity

fix #3584

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-30 16:50:53 -07:00
parent 7f8738dd85
commit 330b3cc8d6
3 changed files with 22 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -231,16 +231,15 @@ private:
bool merge_colors(app_map const& colors1, app_map& colors2) { bool merge_colors(app_map const& colors1, app_map& colors2) {
pair_map recolor; pair_map recolor;
unsigned num_colors = 0, v1 = 0, v2 = 0, w = 0, old_max = 0; unsigned num_colors = 0, v1 = 0, v2 = 0, w = 0, old_max = 0;
app_map::iterator it = colors2.begin(), end = colors2.end(); for (auto & kv : colors2) {
for (; it != end; ++it) { app* a = kv.m_key;
app* a = it->m_key; v1 = kv.m_value;
v1 = it->m_value;
VERIFY(colors1.find(a, v2)); VERIFY(colors1.find(a, v2));
if (recolor.find(u_pair(v1, v2), w)) { if (recolor.find(u_pair(v1, v2), w)) {
it->m_value = w; kv.m_value = w;
} }
else { else {
it->m_value = num_colors; kv.m_value = num_colors;
recolor.insert(u_pair(v1, v2), num_colors++); recolor.insert(u_pair(v1, v2), num_colors++);
} }
if (v1 > old_max) old_max = v1; if (v1 > old_max) old_max = v1;
@ -267,7 +266,8 @@ private:
} }
m_app2sortid.insert(n, id); m_app2sortid.insert(n, id);
} }
void operator()(quantifier * n) {} void operator()(quantifier * n) {
}
void operator()(var * n) {} void operator()(var * n) {}
}; };
@ -278,10 +278,9 @@ private:
} }
void compute_inv_app(app_map const& map, inv_app_map& inv_map) { void compute_inv_app(app_map const& map, inv_app_map& inv_map) {
app_map::iterator it = map.begin(), end = map.end(); for (auto & kv : map) {
for (; it != end; ++it) { app* t = kv.m_key;
app* t = it->m_key; unsigned n = kv.m_value;
unsigned n = it->m_value;
if (is_uninterpreted(t)) { if (is_uninterpreted(t)) {
inv_app_map::entry* e = inv_map.insert_if_not_there2(n, ptr_vector<app>()); inv_app_map::entry* e = inv_map.insert_if_not_there2(n, ptr_vector<app>());
e->get_data().m_value.push_back(t); e->get_data().m_value.push_back(t);
@ -635,6 +634,7 @@ void symmetry_reduce_tactic::operator()(goal_ref const & g,
goal_ref_buffer & result) { goal_ref_buffer & result) {
fail_if_proof_generation("symmetry_reduce", g); fail_if_proof_generation("symmetry_reduce", g);
fail_if_unsat_core_generation("symmetry_reduce", g); fail_if_unsat_core_generation("symmetry_reduce", g);
fail_if_has_quantifiers("symmetry_reduce", g);
result.reset(); result.reset();
(*m_imp)(*(g.get())); (*m_imp)(*(g.get()));
g->inc_depth(); g->inc_depth();

10
src/tactic/tactic.cpp
View file

@ -236,3 +236,13 @@ void fail_if_model_generation(char const * tactic_name, goal_ref const & in) {
throw tactic_exception(std::move(msg)); throw tactic_exception(std::move(msg));
} }
} }
void fail_if_has_quantifiers(char const* tactic_name, goal_ref const& g) {
for (unsigned i = 0; i < g->size(); ++i)
if (has_quantifiers(g->form(i))) {
std::string msg = tactic_name;
msg += " does not apply to quantified goals";
throw tactic_exception(std::move(msg));
}
}

1
src/tactic/tactic.h
View file

@ -125,5 +125,6 @@ lbool check_sat(tactic & t, goal_ref & g, model_ref & md, labels_vec & labels, p
void fail_if_proof_generation(char const * tactic_name, goal_ref const & in); void fail_if_proof_generation(char const * tactic_name, goal_ref const & in);
void fail_if_unsat_core_generation(char const * tactic_name, goal_ref const & in); void fail_if_unsat_core_generation(char const * tactic_name, goal_ref const & in);
void fail_if_model_generation(char const * tactic_name, goal_ref const & in); void fail_if_model_generation(char const * tactic_name, goal_ref const & in);
void fail_if_has_quantifiers(char const* tactic_name, goal_ref const& in);
#endif #endif