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

fix #3957

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-14 06:46:10 -07:00
parent d7d6877031
commit f564c325d3
1 changed files with 55 additions and 52 deletions
Download patch file Download diff file Expand all files Collapse all files

107
src/tactic/tactical.cpp
View file

@ -792,11 +792,6 @@ class repeat_tactical : public unary_tactical {
void operator()(unsigned depth, void operator()(unsigned depth,
goal_ref const & in, goal_ref const & in,
goal_ref_buffer& result) { goal_ref_buffer& result) {
// TODO: implement a non-recursive version.
if (depth > m_max_depth) {
result.push_back(in.get());
return;
}
bool models_enabled = in->models_enabled(); bool models_enabled = in->models_enabled();
bool proofs_enabled = in->proofs_enabled(); bool proofs_enabled = in->proofs_enabled();
@ -804,64 +799,72 @@ class repeat_tactical : public unary_tactical {
ast_manager & m = in->m(); ast_manager & m = in->m();
goal_ref_buffer r1; goal_ref_buffer r1;
result.reset(); goal_ref g = in;
unsigned r1_size = 0;
result.reset();
try_goal:
r1.reset();
if (depth > m_max_depth) {
result.push_back(g.get());
return;
}
{ {
goal orig_in(in->m(), proofs_enabled, models_enabled, cores_enabled); goal orig_in(g->m(), proofs_enabled, models_enabled, cores_enabled);
orig_in.copy_from(*(in.get())); orig_in.copy_from(*(g.get()));
m_t->operator()(in, r1); m_t->operator()(g, r1);
if (r1.size() == 1 && is_equal(orig_in, *(r1[0]))) { if (r1.size() == 1 && is_equal(orig_in, *(r1[0]))) {
result.push_back(r1[0]); result.push_back(r1[0]);
return; return;
} }
} }
unsigned r1_size = r1.size(); r1_size = r1.size();
SASSERT(r1_size > 0); SASSERT(r1_size > 0);
if (r1_size == 1) { if (r1_size == 1) {
if (r1[0]->is_decided()) { if (r1[0]->is_decided()) {
result.push_back(r1[0]); result.push_back(r1[0]);
return; return;
} }
goal_ref r1_0 = r1[0]; g = r1[0];
operator()(depth+1, r1_0, result); depth++;
} goto try_goal;
else { }
goal_ref_buffer r2;
for (unsigned i = 0; i < r1_size; i++) { goal_ref_buffer r2;
goal_ref g = r1[i]; for (unsigned i = 0; i < r1_size; i++) {
r2.reset(); goal_ref g = r1[i];
operator()(depth+1, g, r2); r2.reset();
if (is_decided(r2)) { operator()(depth + 1, g, r2);
SASSERT(r2.size() == 1); if (is_decided(r2)) {
if (is_decided_sat(r2)) { SASSERT(r2.size() == 1);
// found solution... if (is_decided_sat(r2)) {
result.push_back(r2[0]); // found solution...
return; result.push_back(r2[0]);
} return;
else { }
SASSERT(is_decided_unsat(r2)); else {
} SASSERT(is_decided_unsat(r2));
} }
else { }
result.append(r2.size(), r2.c_ptr()); else {
} result.append(r2.size(), r2.c_ptr());
} }
}
if (result.empty()) {
// all subgoals were shown to be unsat. if (result.empty()) {
// create an decided_unsat goal with the proof // all subgoals were shown to be unsat.
in->reset_all(); // create an decided_unsat goal with the proof
proof_ref pr(m); g->reset_all();
expr_dependency_ref core(m); proof_ref pr(m);
if (proofs_enabled) { expr_dependency_ref core(m);
apply(m, in->pc(), pr); if (proofs_enabled) {
} apply(m, g->pc(), pr);
if (cores_enabled && in->dc()) { }
core = (*in->dc())(); if (cores_enabled && g->dc()) {
} core = (*g->dc())();
in->assert_expr(m.mk_false(), pr, core); }
result.push_back(in.get()); g->assert_expr(m.mk_false(), pr, core);
} result.push_back(g.get());
} }
} }
public: public: