updates for #2151 #2152

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/ast/normal_forms/defined_names.cpp

@@ -159,11 +159,11 @@ void defined_names::impl::bound_vars(sort_ref_buffer const & sorts, buffer<symbo
         expr * patterns[1] = { m.mk_pattern(name) };
         quantifier_ref q(m);
         q = m.mk_forall(sorts.size(),
-                                sorts.c_ptr(),
-                                names.c_ptr(),
-                                def_conjunct,
-                                1, qid, symbol::null,
-                                1, patterns);
+                        sorts.c_ptr(),
+                        names.c_ptr(),
+                        def_conjunct,
+                        1, qid, symbol::null,
+                        1, patterns);
         TRACE("mk_definition_bug", tout << "before elim_unused_vars:\n" << mk_ismt2_pp(q, m) << "\n";);
         result = elim_unused_vars(m, q, params_ref());
         TRACE("mk_definition_bug", tout << "after elim_unused_vars:\n" << result << "\n";);

src/ast/rewriter/array_rewriter.h

@@ -45,6 +45,7 @@ public:
     }
     ast_manager & m() const { return m_util.get_manager(); }
     family_id get_fid() const { return m_util.get_family_id(); }
+    array_util& util() { return m_util; }
 
     void set_expand_select_store(bool f) { m_expand_select_store = f; }
     void set_expand_select_ite(bool f) { m_expand_select_ite = f; }

src/ast/rewriter/rewriter.h

@@ -300,7 +300,7 @@ protected:
     void process_var(var * v);
 
     template<bool ProofGen>
-    void process_const(app * t);
+    bool process_const(app * t);
 
     template<bool ProofGen>
     bool visit(expr * t, unsigned max_depth);

src/ast/rewriter/rewriter_def.h

@@ -80,27 +80,42 @@ void rewriter_tpl<Config>::process_var(var * v) {
 
 template<typename Config>
 template<bool ProofGen>
-void rewriter_tpl<Config>::process_const(app * t) {
+bool rewriter_tpl<Config>::process_const(app * t0) {
+    app_ref t(t0, m());
+    bool rounds = 0;
+ retry:
     SASSERT(t->get_num_args() == 0);
     br_status st = m_cfg.reduce_app(t->get_decl(), 0, nullptr, m_r, m_pr);
     SASSERT(st != BR_DONE || m().get_sort(m_r) == m().get_sort(t));
-    SASSERT(st == BR_FAILED || st == BR_DONE);
-    if (st == BR_DONE) {
+    switch (st) {
+    case BR_FAILED:
+        if (rounds == 0) {
+            result_stack().push_back(t);
+            if (ProofGen)
+                result_pr_stack().push_back(nullptr); // implicit reflexivity
+            return true;
+        }
+        m_r = t;
+        // fall through
+    case BR_DONE:
         result_stack().push_back(m_r.get());
         if (ProofGen) {
             if (m_pr)
                 result_pr_stack().push_back(m_pr);
             else
-                result_pr_stack().push_back(m().mk_rewrite(t, m_r));
+                result_pr_stack().push_back(m().mk_rewrite(t0, m_r));
             m_pr = nullptr;
         }
         m_r = nullptr;
-        set_new_child_flag(t);
-    }
-    else {
-        result_stack().push_back(t);
-        if (ProofGen)
-            result_pr_stack().push_back(nullptr); // implicit reflexivity
+        set_new_child_flag(t0);
+        return true;
+    default: 
+        if (is_app(m_r) && to_app(m_r)->get_num_args() == 0) {
+            t = to_app(m_r);
+            rounds++;
+            goto retry;
+        }
+        return false;
     }
 }
 
@@ -115,6 +130,7 @@ void rewriter_tpl<Config>::process_const(app * t) {
 template<typename Config>
 template<bool ProofGen>
 bool rewriter_tpl<Config>::visit(expr * t, unsigned max_depth) {
+ // retry:
     TRACE("rewriter_visit", tout << "visiting\n" << mk_ismt2_pp(t, m()) << "\n";);
     expr *  new_t = nullptr;
     proof * new_t_pr = nullptr;
@@ -164,15 +180,14 @@ bool rewriter_tpl<Config>::visit(expr * t, unsigned max_depth) {
     switch (t->get_kind()) {
     case AST_APP:
         if (to_app(t)->get_num_args() == 0) {
-            process_const<ProofGen>(to_app(t));
-            return true;
-        }
-        else {
-            if (max_depth != RW_UNBOUNDED_DEPTH)
-                max_depth--;
-            push_frame(t, c, max_depth);
-            return false;
+            if (process_const<ProofGen>(to_app(t))) 
+                return true; 
+            t = m_r;
         }
+        if (max_depth != RW_UNBOUNDED_DEPTH)
+            max_depth--;
+        push_frame(t, c, max_depth);
+        return false;        
     case AST_VAR:
         process_var<ProofGen>(to_var(t));
         return true;
@@ -224,7 +239,7 @@ bool rewriter_tpl<Config>::constant_fold(app * t, frame & fr) {
 template<typename Config>
 template<bool ProofGen>
 void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
-    SASSERT(t->get_num_args() > 0);
+    // SASSERT(t->get_num_args() > 0);
     SASSERT(!frame_stack().empty());
     switch (fr.m_state) {
     case PROCESS_CHILDREN: {

src/ast/rewriter/th_rewriter.cpp

@@ -661,6 +661,13 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
                 p1 = m().mk_pull_quant(old_q, q1);
             }
         }
+        else if (
+                 old_q->get_kind() == lambda_k &&
+                 is_ground(new_body)) {
+            result = m_ar_rw.util().mk_const_array(old_q->get_sort(), new_body);
+            result_pr = nullptr;
+            return true;
+        }
         else {
             ptr_buffer<expr> new_patterns_buf;
             ptr_buffer<expr> new_no_patterns_buf;
@@ -677,10 +684,10 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
             TRACE("reduce_quantifier", tout << mk_ismt2_pp(old_q, m()) << "\n----->\n" << mk_ismt2_pp(q1, m()) << "\n";);
             SASSERT(is_well_sorted(m(), q1));
         }
-
         SASSERT(m().get_sort(old_q) == m().get_sort(q1));
         result = elim_unused_vars(m(), q1, params_ref());
 
+
         TRACE("reduce_quantifier", tout << "after elim_unused_vars:\n" << result << "\n";);
 
         result_pr = nullptr;