add destructive equality resolution to the main simplifier.

Z3Prover · Feb 19, 2023 · cb81473 · cb81473
1 parent c0f80f9
commit cb81473
Show file tree

Hide file tree

Showing 2 changed files with 15 additions and 2 deletions.
diff --git a/src/ast/rewriter/der.cpp b/src/ast/rewriter/der.cpp
@@ -197,9 +197,10 @@ void der::reduce1(quantifier * q, expr_ref & r, proof_ref & pr) {
 
         m_pos2var.reserve(num_args, -1);
 
-        // Find all disequalities
+        // Find all equalities/disequalities
         for (unsigned i = 0; i < num_args; i++) {
-            is_eq = is_forall(q) ? is_var_diseq(literals.get(i), num_decls, v, t) : is_var_eq(literals.get(i), num_decls, v, t);
+            expr* arg = literals.get(i);
+            is_eq = is_forall(q) ? is_var_diseq(arg, num_decls, v, t) : is_var_eq(arg, num_decls, v, t);
             if (is_eq) {
                 unsigned idx = v->get_idx();
                 if (m_map.get(idx, nullptr) == nullptr) {

diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp
@@ -31,6 +31,7 @@ Module Name:
 #include "ast/rewriter/seq_rewriter.h"
 #include "ast/rewriter/rewriter_def.h"
 #include "ast/rewriter/var_subst.h"
+#include "ast/rewriter/der.h"
 #include "ast/rewriter/expr_safe_replace.h"
 #include "ast/expr_substitution.h"
 #include "ast/ast_smt2_pp.h"
@@ -54,6 +55,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
     recfun_rewriter     m_rec_rw;
     arith_util          m_a_util;
     bv_util             m_bv_util;
+    der                 m_der;
     expr_safe_replace   m_rep;
     expr_ref_vector     m_pinned;
       // substitution support
@@ -819,6 +821,15 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
             result_pr = m().mk_transitivity(p1, p2);
         }
 
+        if (is_quantifier(result)) {
+            proof_ref p2(m());
+            expr_ref r(m());
+            m_der(to_quantifier(result), r, p2);
+            if (m().proofs_enabled() && result.get() != r.get()) 
+                result_pr = m().mk_transitivity(result_pr, p2);
+            result = r;
+        }
+
         TRACE("reduce_quantifier", tout << "after elim_unused_vars:\n" << result << " " << result_pr << "\n" ;);
 
         SASSERT(old_q->get_sort() == result->get_sort());
@@ -839,6 +850,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
         m_rec_rw(m),
         m_a_util(m),
         m_bv_util(m),
+        m_der(m),
         m_rep(m),
         m_pinned(m),
         m_used_dependencies(m) {