more on #3858 elim_term_ite

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

src/ast/rewriter/var_subst.h

@@ -49,6 +49,8 @@ public:
        Otherwise, (VAR 0) is stored in the first position, (VAR 1) in the second, and so on.
     */
     expr_ref operator()(expr * n, unsigned num_args, expr * const * args);
+    inline expr_ref operator()(expr * n, expr_ref_vector const& args) { return (*this)(n, args.size(), args.c_ptr()); }
+    inline expr_ref operator()(expr * n, ptr_vector<expr> const& args) { return (*this)(n, args.size(), args.c_ptr()); }
     void reset() { m_reducer.reset(); }
 };
 
@@ -90,6 +92,8 @@ class expr_free_vars {
     ptr_vector<sort> m_sorts;
     ptr_vector<expr> m_todo;
 public:
+    expr_free_vars() {}
+    expr_free_vars(expr* e) { (*this)(e); }
     void reset();
     void operator()(expr* e);
     void accumulate(expr* e);

src/muz/transforms/dl_mk_elim_term_ite.cpp

@@ -17,27 +17,32 @@ Revision History:
 
 --*/
 
-#include "muz/transforms/dl_mk_elim_term_ite.h"
-#include "tactic/core/blast_term_ite_tactic.h"
 #include "ast/ast_util.h"
 #include "ast/expr_abstract.h"
+#include "tactic/core/blast_term_ite_tactic.h"
 #include "tactic/tactic.h"
 #include "tactic/core/elim_term_ite_tactic.h"
+#include "muz/transforms/dl_mk_elim_term_ite.h"
 
 namespace {
+    /**
+     * collect uninterpreted constants that are contained in ground
+     */
     struct uninterp_const_collector {
-        app_ref_vector &m_consts;
+        app_ref_vector&         m_consts;
-        uninterp_const_collector(app_ref_vector &v) : m_consts(v) {}
+        expr_ref_vector const&  m_ground;
+        uninterp_const_collector(app_ref_vector &v, expr_ref_vector const& g) : m_consts(v), m_ground(g) {}
         void operator()(var *v) {}
         void operator()(quantifier *n) {}
         void operator()(expr *a){}
         void operator()(app *a){
-            if (is_uninterp_const(a)) {m_consts.push_back(a);};
+            if (is_uninterp_const(a) && m_ground.contains(a)) 
+                m_consts.push_back(a);
         }
     };
 
-    void collect_uninterp_consts(expr *e, app_ref_vector &v) {
+    void collect_uninterp_consts(expr *e, app_ref_vector &v, expr_ref_vector const& g) {
-        uninterp_const_collector c(v);
+        uninterp_const_collector c(v, g);
         quick_for_each_expr(c, e);
     }
 
@@ -47,9 +52,9 @@ namespace {
         term_ite_proc(ast_manager &m) : m(m) {}
         void operator()(var *v) {}
         void operator()(quantifier *n) {}
-        void operator()(expr *a){}
+        void operator()(expr *a) {
-        void operator()(app *a){
+            if (m.is_term_ite(a)) 
-            if (m.is_term_ite(a)) throw found();
+                throw found();
         }
     };
 
@@ -57,14 +62,16 @@ namespace {
         term_ite_proc f(m);
         try {
             quick_for_each_expr(f, e);
-        } catch (const term_ite_proc::found &) {
+        } 
+        catch (const term_ite_proc::found &) {
             return true;
         }
         return false;
     }
-    bool has_term_ite(expr_ref &e) { return has_term_ite(e, e.m());}
 
+    bool has_term_ite(expr_ref &e) { return has_term_ite(e, e.m());}
 }
+
 namespace datalog {
     mk_elim_term_ite::mk_elim_term_ite(context & ctx, unsigned priority) :
         rule_transformer::plugin(priority, false),
@@ -75,18 +82,23 @@ namespace datalog {
 
     mk_elim_term_ite::~mk_elim_term_ite() {}
 
+    /**
+       \brief map free variables in e to ground, fresh, constants
+       m_ground is reset on every new rule so it is safe to assume
+       that the sorts in m_ground are consistent.       
+     */
     expr_ref mk_elim_term_ite::ground(expr* e) {
-        expr_free_vars fv;
+        expr_free_vars fv(e);
-        fv(e);
+        m_ground.reserve(fv.size());
-        if (m_ground.size() < fv.size())
-            m_ground.resize(fv.size());
         for (unsigned i = 0, sz = fv.size(); i < sz; ++i) {
-            if (fv[i] && !m_ground.get(i))
+            if (!fv[i])
+                continue;
+            if (!m_ground.get(i))
                 m_ground[i] = m.mk_fresh_const("c", fv[i]);
+            SASSERT(m.get_sort(m_ground.get(i)) == fv[i]);
         }
-
         var_subst vsub(m, false);
-        return vsub(e, m_ground.size(), m_ground.c_ptr());
+        return vsub(e, m_ground);
     }
 
     bool mk_elim_term_ite::elim(rule &r, rule_set &new_rules){
@@ -96,13 +108,12 @@ namespace datalog {
         unsigned utsz = r.get_uninterpreted_tail_size();
         unsigned tsz = r.get_tail_size();
         expr_ref_vector new_conjs(m);
-        expr_ref tmp(m);
 
         for (unsigned i = utsz; i < tsz; ++i)
             new_conjs.push_back(r.get_tail(i));
         flatten_and(new_conjs);
 
-        expr_ref fml1(m), fml2(m), body(m), head(m);
+        expr_ref fml1(m), fml2(m), body(m);
 
         // blast ite
         body = mk_and(new_conjs);
@@ -127,12 +138,11 @@ namespace datalog {
             rule_ref new_rule(rm.mk(r.get_head(), tail.size(), tail.c_ptr(), nullptr, r.name(), false), rm);           
             rm.mk_rule_rewrite_proof(r, *new_rule.get());
             new_rules.add_rule(new_rule);
-            TRACE("dl_term_ite", tout << "No term-ite after blast_term_ite\n";);
+            TRACE("dl", tout << "No term-ite after blast_term_ite\n";);
             return true;
         }
 
-        TRACE("dl_term_ite",
+        TRACE("dl", tout << "Rule has term-ite after blasting, starting elimination\n";);
-              tout << "Rule has term-ite after blasting, starting elimination\n";);
         body = ground(body);
         // elim ite
         tactic_ref elim_term_ite = mk_elim_term_ite_tactic(m);
@@ -145,6 +155,7 @@ namespace datalog {
         unsigned sz = g->num_exprs();
         (*elim_term_ite)(g, result);
         if (result.size() == 1) {
+            // NSB code review: fragile test for effect
             goal_ref new_goal = result[0];
             if (new_goal->num_exprs() != sz) {
                 new_conjs.reset();
@@ -160,20 +171,20 @@ namespace datalog {
         body = mk_and(new_conjs);
         rw(body);
 
-        head = ground(r.get_head());
+        fml2 = m.mk_implies(body, ground(r.get_head()));
-
-        fml2 = m.mk_implies(body, head);
         if (has_term_ite(fml2))
             return false;
         app_ref_vector consts(m);
-        collect_uninterp_consts(fml2, consts);
+        collect_uninterp_consts(fml2, consts, m_ground);
+        
         fml2 = mk_forall(m, consts.size(), consts.c_ptr(), fml2);
         proof_ref p(m);
         rm.mk_rule(fml2, p, new_rules, r.name()); 
-        // TBD: breaks abstraction barrier: mk_rule could convert a single formula
+
+        // NSB code review: breaks abstraction barrier: mk_rule could convert a single formula
         // into multiple rules
         rm.mk_rule_rewrite_proof(r, *new_rules.last());
-        TRACE("dl_term_ite", tout << "New rule: " << fml2 << "\n";);
+        TRACE("dl", tout << "New rule: " << fml2 << "\n";);
         return true;
     }
 
@@ -188,8 +199,7 @@ namespace datalog {
         bool change = false;
         for (auto *rule : source) {
             if (m_ctx.canceled()) {
-                change = false;
+                return nullptr;
-                break;
             }
             change |= elim(*rule, *rules);
         }