The demodulator doesn't produce proofs so remove code path that depen…

…ds it does.
Z3Prover · Dec 4, 2022 · d218083 · d218083
1 parent 7fe6787
commit d218083
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 14 deletions.
diff --git a/src/ast/rewriter/demodulator_rewriter.cpp b/src/ast/rewriter/demodulator_rewriter.cpp
@@ -616,15 +616,8 @@ void demodulator_rewriter::reschedule_demodulators(func_decl * f, expr * lhs) {
     }
 }
 
-void demodulator_rewriter::operator()(unsigned n, expr * const * exprs, proof * const * prs, 
-                               expr_ref_vector & new_exprs, proof_ref_vector & new_prs) {
-    if (m.proofs_enabled()) {
-        TRACE("tactic", tout << "PRE_DEMODULATOR=true is not supported when proofs are enabled.";);
-        // Let us not waste time with proof production
-        new_exprs.append(n, exprs);
-        new_prs.append(n, prs);
-        return;
-    }
+void demodulator_rewriter::operator()(unsigned n, expr * const * exprs, 
+                               expr_ref_vector & new_exprs) {
 
     TRACE("demodulator", tout << "before demodulator:\n";
                          for ( unsigned i = 0 ; i < n ; i++ )

diff --git a/src/ast/rewriter/demodulator_rewriter.h b/src/ast/rewriter/demodulator_rewriter.h
@@ -197,7 +197,7 @@ class demodulator_rewriter final {
     demodulator_rewriter(ast_manager & m);
     ~demodulator_rewriter();
 
-    void operator()(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs);
+    void operator()(unsigned n, expr * const * exprs, expr_ref_vector & new_exprs);
 
     /**
       Given a demodulator (aka rewrite rule) of the form

diff --git a/src/tactic/ufbv/ufbv_rewriter_tactic.cpp b/src/tactic/ufbv/ufbv_rewriter_tactic.cpp
@@ -41,14 +41,16 @@ class demodulator_rewriter_tactic : public tactic {
     void collect_param_descrs(param_descrs & r) override {
         insert_max_memory(r);
         insert_produce_models(r);
-        insert_produce_proofs(r);
     }
 
     void operator()(goal_ref const & g, goal_ref_buffer & result) override {
         tactic_report report("ufbv-rewriter", *g);
         fail_if_unsat_core_generation("ufbv-rewriter", g);
 
-        bool produce_proofs = g->proofs_enabled();
+        if (g->proofs_enabled()) {
+            result.push_back(g.get());
+            return;
+        }
 
         demodulator_rewriter dem(m_manager);
 
@@ -61,11 +63,11 @@ class demodulator_rewriter_tactic : public tactic {
             proofs.push_back(g->pr(i));
         }
 
-        dem(forms.size(), forms.data(), proofs.data(), new_forms, new_proofs);
+        dem(forms.size(), forms.data(), new_forms);
 
         g->reset();
         for (unsigned i = 0; i < new_forms.size(); i++)
-            g->assert_expr(new_forms.get(i), produce_proofs ? new_proofs.get(i) : nullptr, nullptr);
+            g->assert_expr(new_forms.get(i), nullptr, nullptr);
 
         // CMW: Remark: The demodulator could potentially
         // remove all references to a variable.