mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 09:34:08 +00:00
Code Activity

Bugfixes in UFBV-related tactics.

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2012-10-26 15:54:02 +01:00
parent 6c2ef9e70c
commit bf27090641
3 changed files with 9 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -80,12 +80,9 @@ class macro_finder_tactic : public tactic {
mf(forms.size(), forms.c_ptr(), proofs.c_ptr(), new_forms, new_proofs);
unsigned i = 0;
for (; i < g->size(); i++)
g->update(i, new_forms.get(i), produce_proofs ? new_proofs.get(i) : 0, 0);
for (; i < new_forms.size(); i++)
g->assert_expr(new_forms.get(i), new_proofs.get(i), 0);
g->reset();
for (unsigned i = 0; i < new_forms.size(); i++)
g->assert_expr(new_forms.get(i), produce_proofs ? new_proofs.get(i) : 0, 0);
extension_model_converter * evmc = alloc(extension_model_converter, mm.get_manager());
unsigned num = mm.get_num_macros();

9
src/tactic/ufbv/quasi_macros_tactic.cpp
View file

@ -91,12 +91,9 @@ class quasi_macros_tactic : public tactic {
proofs.swap(new_proofs);
}
unsigned i = 0;
for (; i < g->size(); i++)
g->update(i, new_forms.get(i), produce_proofs ? new_proofs.get(i) : 0, 0);
for (; i < new_forms.size(); i++)
g->assert_expr(new_forms.get(i), new_proofs.get(i), 0);
g->reset();
for (unsigned i = 0; i < new_forms.size(); i++)
g->assert_expr(new_forms.get(i), produce_proofs ? new_proofs.get(i) : 0, 0);
extension_model_converter * evmc = alloc(extension_model_converter, mm.get_manager());
unsigned num = mm.get_num_macros();

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

@ -66,12 +66,9 @@ class ufbv_rewriter_tactic : public tactic {
dem(forms.size(), forms.c_ptr(), proofs.c_ptr(), new_forms, new_proofs);
unsigned i = 0;
for (; i < g->size(); i++)
g->update(i, new_forms.get(i), produce_proofs ? new_proofs.get(i) : 0, g->dep(i));
for (; i < new_forms.size(); i++)
g->assert_expr(new_forms.get(i), new_proofs.get(i), 0);
g->reset();
for (unsigned i = 0; i < new_forms.size(); i++)
g->assert_expr(new_forms.get(i), produce_proofs ? new_proofs.get(i) : 0, 0);
mc = 0; // CMW: Remark: The demodulator could potentially remove all references to a variable.