From bf27090641772dc701db6a118f1f65d167bca421 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 26 Oct 2012 15:54:02 +0100 Subject: [PATCH] Bugfixes in UFBV-related tactics. Signed-off-by: Christoph M. Wintersteiger --- src/tactic/ufbv/macro_finder_tactic.cpp | 9 +++------ src/tactic/ufbv/quasi_macros_tactic.cpp | 9 +++------ src/tactic/ufbv/ufbv_rewriter_tactic.cpp | 9 +++------ 3 files changed, 9 insertions(+), 18 deletions(-) diff --git a/src/tactic/ufbv/macro_finder_tactic.cpp b/src/tactic/ufbv/macro_finder_tactic.cpp index c58c04f14..11e58ee69 100644 --- a/src/tactic/ufbv/macro_finder_tactic.cpp +++ b/src/tactic/ufbv/macro_finder_tactic.cpp @@ -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(); diff --git a/src/tactic/ufbv/quasi_macros_tactic.cpp b/src/tactic/ufbv/quasi_macros_tactic.cpp index 6356adfbe..8d8c7cae0 100644 --- a/src/tactic/ufbv/quasi_macros_tactic.cpp +++ b/src/tactic/ufbv/quasi_macros_tactic.cpp @@ -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(); diff --git a/src/tactic/ufbv/ufbv_rewriter_tactic.cpp b/src/tactic/ufbv/ufbv_rewriter_tactic.cpp index b9c0b5f7c..010ffab28 100644 --- a/src/tactic/ufbv/ufbv_rewriter_tactic.cpp +++ b/src/tactic/ufbv/ufbv_rewriter_tactic.cpp @@ -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.