merged

src/muz_qe/pdr_util.cpp

@@ -1129,7 +1129,11 @@ namespace pdr {
             if (a.is_numeral(lhs) || a.is_numeral(rhs)) {
                 return test_ineq(e);
             }
-            return test_term(lhs) && test_term(rhs);
+            return 
+                test_term(lhs) && 
+                test_term(rhs) &&
+                !a.is_mul(lhs) &&
+                !a.is_mul(rhs);
         }
 
         bool test_term(expr* e) const {

src/muz_qe/proof_utils.cpp

@@ -312,9 +312,10 @@ public:
 };
 
 void proof_utils::reduce_hypotheses(proof_ref& pr) {
-    class reduce_hypotheses reduce(pr.get_manager());
+    ast_manager& m = pr.get_manager();
+    class reduce_hypotheses reduce(m);
     reduce(pr);
-    SASSERT(is_closed(pr.get_manager(), pr));
+    CTRACE("proof_utils", !is_closed(m, pr), tout << mk_pp(pr, m) << "\n";);
 }
 
 class proof_is_closed {

src/muz_qe/qe_lite.cpp

@@ -2104,10 +2104,56 @@ namespace fm {
 } // namespace fm
 
 class qe_lite::impl {
+public:
+    struct elim_cfg : public default_rewriter_cfg {
+        impl& m_imp;
+        ast_manager& m;
+    public:
+        elim_cfg(impl& i): m_imp(i), m(i.m) {}
+        
+        bool reduce_quantifier(quantifier * q, 
+                               expr * new_body, 
+                               expr * const * new_patterns, 
+                               expr * const * new_no_patterns,
+                               expr_ref & result,
+                               proof_ref & result_pr) {
+            result = new_body;
+            if (is_forall(q)) {
+                result = m.mk_not(result);
+            }
+            uint_set indices;
+            for (unsigned i = 0; i < q->get_num_decls(); ++i) {
+                indices.insert(i);
+            }
+            m_imp(indices, true, result);          
+            if (is_forall(q)) {
+                result = m.mk_not(result);
+            }
+            result = m.update_quantifier(
+                q, 
+                q->get_num_patterns(), new_patterns, 
+                q->get_num_no_patterns(), new_no_patterns, result);
+            m_imp.m_rewriter(result);
+            return true;
+        }
+    };
+
+    class elim_star : public rewriter_tpl<elim_cfg> {
+        elim_cfg m_cfg;
+    public:
+        elim_star(impl& i): 
+            rewriter_tpl<elim_cfg>(i.m, false, m_cfg),
+            m_cfg(i)
+        {}
+    };
+
+private:
     ast_manager& m;
     eq::der      m_der;
     fm::fm       m_fm;
     ar::der      m_array_der;
+    elim_star    m_elim_star;
+    th_rewriter  m_rewriter;
 
     bool has_unique_non_ground(expr_ref_vector const& fmls, unsigned& index) {
         index = fmls.size();
@@ -2126,7 +2172,13 @@ class qe_lite::impl {
     }
 
 public:
-    impl(ast_manager& m): m(m), m_der(m), m_fm(m), m_array_der(m) {}
+    impl(ast_manager& m): 
+        m(m), 
+        m_der(m), 
+        m_fm(m), 
+        m_array_der(m), 
+        m_elim_star(*this), 
+        m_rewriter(m) {}
     
     void operator()(app_ref_vector& vars, expr_ref& fml) {
         if (vars.empty()) {
@@ -2168,19 +2220,9 @@ public:
     }    
 
     void operator()(expr_ref& fml, proof_ref& pr) {
-        if (is_exists(fml)) {
+        expr_ref tmp(m);
-            quantifier* q = to_quantifier(fml);
+        m_elim_star(fml, tmp, pr);
-            expr_ref body(m);
+        fml = tmp;
-            body = q->get_expr();
-            uint_set indices;
-            for (unsigned i = 0; i < q->get_num_decls(); ++i) {
-                indices.insert(i);
-            }
-            (*this)(indices, true, body);
-            fml = m.update_quantifier(q, body);
-            th_rewriter rewriter(m);
-            rewriter(fml);
-        }
     }
 
     void operator()(uint_set const& index_set, bool index_of_bound, expr_ref& fml) {
@@ -2227,6 +2269,8 @@ public:
         m_der.set_cancel(f);
         m_array_der.set_cancel(f);
         m_fm.set_cancel(f);
+        m_elim_star.set_cancel(f);
+        m_rewriter.set_cancel(f);
     }
 
 };
@@ -2383,3 +2427,5 @@ public:
 tactic * mk_qe_lite_tactic(ast_manager & m, params_ref const & p) {
     return alloc(qe_lite_tactic, m, p);
 }
+
+template class rewriter_tpl<qe_lite::impl::elim_cfg>;