fix #1469

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

src/qe/qe.cpp

@@ -130,8 +130,7 @@ namespace qe {
                     visited.mark(e, true);
                 }            
             }
-            for (unsigned i = 0; i < conjs.size(); ++i) {
+            for (expr* e : conjs) {
-                expr* e = conjs[i].get();
                 bool cv = contains_var.is_marked(e);
                 bool cu = contains_uf.is_marked(e);
                 if (cv && cu) {
@@ -989,11 +988,11 @@ namespace qe {
                 todo.pop_back();
                 if (st->m_children.empty() && st->fml() && 
                     st->m_vars.empty() && !st->has_var()) {
+                    TRACE("qe", st->display(tout << "appending leaf\n");); 
                     result.push_back(st->fml());
                 }
-                for (unsigned i = 0; i < st->m_children.size(); ++i) {
+                for (auto * ch : st->m_children)
-                    todo.push_back(st->m_children[i]);
+                    todo.push_back(ch);
-                }
             }
         }
 
@@ -1020,9 +1019,7 @@ namespace qe {
 
         void reset() {
             TRACE("qe",tout << "resetting\n";);
-            for (unsigned i = 0; i < m_children.size(); ++i) {
+            for (auto* ch : m_children) dealloc(ch);
-                dealloc(m_children[i]);
-            }
             m_pos.reset();
             m_neg.reset();
             m_children.reset();
@@ -1046,9 +1043,10 @@ namespace qe {
         }
 
         unsigned num_free_vars() const { return m_vars.size(); }
-        app* const* free_vars() const { return m_vars.c_ptr(); }
+        // app* const* free_vars() const { return m_vars.c_ptr(); }
+        app_ref_vector const& free_vars() const { return m_vars; }
         app*        free_var(unsigned i) const { return m_vars[i]; }
-        void        reset_free_vars() { m_vars.reset(); }
+        void        reset_free_vars() { TRACE("qe", tout << m_vars << "\n";); m_vars.reset(); }
 
         atom_set const& pos_atoms() const { return m_pos; }   
         atom_set const& neg_atoms() const { return m_neg; }    
@@ -1119,7 +1117,7 @@ namespace qe {
             st->init(fml);
             st->m_vars.append(m_vars.size(), m_vars.c_ptr());
             SASSERT(invariant());
-            TRACE("qe", tout << mk_pp(m_fml, m) << " child: " << mk_pp(fml, m) << "\n";);
+            TRACE("qe", display_node(tout); st->display_node(tout););
             return st;
         }
 
@@ -1133,7 +1131,7 @@ namespace qe {
             m_branch_index.insert(branch_id, index);
             st->m_vars.append(m_vars.size(), m_vars.c_ptr());
             SASSERT(invariant());
-            //TRACE("qe", tout << mk_pp(m_fml, m) << " child: " << mk_pp(st->fml(), m) << "\n";);
+            TRACE("qe", display_node(tout); st->display_node(tout););
             return st;
         }
 
@@ -1141,27 +1139,29 @@ namespace qe {
             display(out, "");
         }
 
-        void display(std::ostream& out, char const* indent) const {
+        void display_node(std::ostream& out, char const* indent = "") const {
-
+            out << indent << "node " << std::hex << this << std::dec << "\n";
-            out << indent << "node\n";
             if (m_var) {
-                out << indent << " var:  " << mk_ismt2_pp(m_var.get(), m) << "\n";
+                out << indent << " var:  " << m_var << "\n";
             }
-            for (unsigned i = 0; i < m_vars.size(); ++i) {
+            for (app* v : m_vars) {
-                out << indent << " free: " << mk_ismt2_pp(m_vars[i], m) << "\n";
+                out << indent << " free: " << mk_pp(v, m) << "\n";            
             }
             if (m_fml) {
-                out << indent << " fml:  " << mk_ismt2_pp(m_fml.get(), m) << "\n";
+                out << indent << " fml:  " << m_fml << "\n";
             }
             for (unsigned i = 0; i < m_def.size(); ++i) {
                 out << indent << " def:  " << m_def.var(i)->get_name() << " = " << mk_ismt2_pp(m_def.def(i), m) << "\n";
             }
             out << indent << " branches: " << m_num_branches << "\n";
+        }
 
+        void display(std::ostream& out, char const* indent) const {
+            display_node(out, indent);
             std::string new_indent(indent);
             new_indent += " ";
-            for (unsigned i = 0; i < m_children.size(); ++i) {
+            for (auto * ch : m_children) {
-                m_children[i]->display(out, new_indent.c_str());
+                ch->display(out, new_indent.c_str());
             }
         }
 
@@ -1214,6 +1214,7 @@ namespace qe {
                 out << "(push)\n";
                 pp.display_smt2(out, fml);                
                 out << "(pop)\n\n";      
+#if 0
                 DEBUG_CODE(
                     smt_params params;
                     params.m_simplify_bit2int = true;
@@ -1227,7 +1228,8 @@ namespace qe {
                         std::cout << "; Validation failed:\n";
                         std::cout << mk_pp(fml, m) << "\n";
                     }
-);
+                           );
+#endif
 
             }
             for (unsigned i = 0; i < m_children.size(); ++i) {
@@ -1486,9 +1488,7 @@ namespace qe {
                   tout << "subformula: " << mk_ismt2_pp(m_subfml, m) << "\n";
                   m_root.display(tout); 
                   m_root.display_validate(tout); 
-                  for (unsigned i = 0; i < m_free_vars.size(); ++i) tout << mk_ismt2_pp(m_free_vars[i].get(), m) << " ";
+                  tout << "free: " << m_free_vars << "\n";);
-                  tout << "\n";
-                  );
 
             free_vars.append(m_free_vars);
             if (!m_free_vars.empty() || m_solver.inconsistent()) {
@@ -1546,14 +1546,14 @@ namespace qe {
 
         app* get_var(unsigned idx) const { return m_current->free_var(idx); } 
 
-        app* const* get_vars() const { return m_current->free_vars(); }
+        app_ref_vector const& get_vars() const { return m_current->free_vars(); }
 
         contains_app& contains(unsigned idx) { return contains(get_var(idx)); }              
 
         //
         // The variable at idx is eliminated (without branching).
         // 
-        void elim_var(unsigned idx, expr* _fml, expr* def) {
+        void elim_var(unsigned idx, expr* _fml, expr* def) override {
             app* x = get_var(idx);
             expr_ref fml(_fml, m);
             TRACE("qe", tout << mk_pp(x,m) << " " << mk_pp(def, m) << "\n";);
@@ -1598,7 +1598,7 @@ namespace qe {
             add_literal(l3);
             expr_ref fml(m);
             fml = m.mk_or(m_literals.size(), m_literals.c_ptr());
-            TRACE("qe", tout << mk_ismt2_pp(fml, m) << "\n";);
+            TRACE("qe", tout << fml << "\n";);
             m_solver.assert_expr(fml);
         }            
 
@@ -1654,9 +1654,7 @@ namespace qe {
         }
 
         app* get_branch_id(app* x) {
-            app* result = 0;
+            return m_var2branch[x];
-            VERIFY (m_var2branch.find(x, result));
-            return result;
         }
 
         bool extract_partition(ptr_vector<app>& vars) {
@@ -1912,6 +1910,7 @@ namespace qe {
             }
 
             m_current->set_var(x, k);
+            TRACE("qe", tout << mk_pp(x, m) << " := " << k << "\n";);
             if (m_bv.is_bv(x)) {                
                 return;
             }
@@ -1952,7 +1951,7 @@ namespace qe {
                 vars.reset();
                 closed = closed && (r != l_undef);
             }        
-            TRACE("qe", tout << mk_pp(fml, m) << "\n";);
+            TRACE("qe", tout << fml << " free: " << m_current->free_vars() << "\n";);
             m_current->add_child(fml)->reset_free_vars();
             block_assignment(); 
         }
@@ -1961,9 +1960,7 @@ namespace qe {
         // variable queueing.
 
         contains_app& contains(app* x) {
-            contains_app* result = 0;
+            return *m_var2contains[x];
-            VERIFY(m_var2contains.find(x, result));
-            return *result;
         }
 
         bool find_min_weight(app*& x, rational& num_branches) {
@@ -2003,6 +2000,7 @@ namespace qe {
             bool solved = true;
             while (solved) {
                 expr_ref fml(m_current->fml(), m);
+                TRACE("qe", tout << fml << "\n";);
                 conj_enum conjs(m, fml);
                 solved = false;
                 for (unsigned i = 0; !solved && i < m_plugins.size(); ++i) {
@@ -2512,7 +2510,7 @@ namespace qe {
         // Access current set of variables to solve
         virtual unsigned    get_num_vars() const { return m_vars->size(); }
         virtual app*        get_var(unsigned idx) const { return (*m_vars)[idx].get(); }
-        virtual app*const*  get_vars() const { return m_vars->c_ptr(); }
+        virtual app_ref_vector const&  get_vars() const { return *m_vars; }
         virtual bool        is_var(expr* e, unsigned& idx) const { 
             for (unsigned i = 0; i < m_vars->size(); ++i) {
                 if ((*m_vars)[i].get() == e) { 
@@ -2540,6 +2538,7 @@ namespace qe {
 
         // callback to add new variable to branch.
         virtual void add_var(app* x) {
+            TRACE("qe", tout << "add var: " << mk_pp(x, m) << "\n";);
             m_vars->push_back(x);
         }
 

src/qe/qe.h

@@ -86,7 +86,7 @@ namespace qe {
         // Access current set of variables to solve
         virtual unsigned      get_num_vars() const = 0;
         virtual app*          get_var(unsigned idx) const = 0;
-        virtual app*const*    get_vars() const = 0;
+        virtual app_ref_vector const&  get_vars() const = 0;
         virtual bool          is_var(expr* e, unsigned& idx) const;
         virtual contains_app& contains(unsigned idx) = 0;
 

src/qe/qe_arith_plugin.cpp

@@ -105,6 +105,7 @@ namespace qe {
     public:
         arith_util        m_arith; // initialize before m_zero_i, etc.
         th_rewriter       simplify;
+        app_ref_vector    m_vars_added;
     private:
         arith_eq_solver   m_arith_solver;
         bv_util           m_bv;
@@ -126,6 +127,7 @@ namespace qe {
             m_ctx(ctx),
             m_arith(m),
             simplify(m),
+            m_vars_added(m),
             m_arith_solver(m),
             m_bv(m),
             m_zero_i(m_arith.mk_numeral(numeral(0), true), m),
@@ -783,6 +785,11 @@ namespace qe {
             }
         }
 
+        void add_var(app* v, bool track = true) {
+            m_ctx.add_var(v);
+            if (track) m_vars_added.push_back(v);
+        }
+
 
     private:
 
@@ -850,10 +857,11 @@ namespace qe {
                   << mk_pp(result, m) << "\n";);
         }
 
+
         void mk_big_or_symbolic(numeral up, app* x, expr* body, expr_ref& result) {
             app_ref z_bv(m);
             mk_big_or_symbolic(up, x, body, z_bv, result);
-            m_ctx.add_var(z_bv);
+            add_var(z_bv);
         }        
 
         void mk_big_or_symbolic_blast(numeral up, app* x, expr* body, expr_ref& result) {
@@ -999,9 +1007,9 @@ namespace qe {
         bool solve_linear(expr* p, expr* fml) {
             vector<numeral> values;
             unsigned num_vars = m_ctx.get_num_vars();
-            app*const* vars_ptr = m_ctx.get_vars();
+            app_ref_vector const& vars = m_ctx.get_vars();
             
-            if (!is_linear(p, num_vars, vars_ptr, values)) {
+            if (!is_linear(p, num_vars, vars.c_ptr(), values)) {
                 return false;
             }
 
@@ -1025,7 +1033,7 @@ namespace qe {
                 // it has coefficient 'm' = values[index].
                 SASSERT(values[index] >= rational(3));
                 z  = m.mk_fresh_const("x", m_arith.mk_int());
-                m_ctx.add_var(z);
+                add_var(z);
                 p1 = m_arith.mk_mul(m_arith.mk_numeral(values[index], true), z);
             }
             else {                
@@ -1475,16 +1483,18 @@ public:
         expr*    m_result;
         rational m_coeff;
         expr*    m_term;
+        ptr_vector<app> m_vars;
 
         branch_formula(): m_fml(0), m_var(0), m_branch(0), m_result(0), m_term(0) {}
         
-        branch_formula(expr* fml, app* var, unsigned b, expr* r, rational coeff, expr* term):
+        branch_formula(expr* fml, app* var, unsigned b, expr* r, rational coeff, expr* term, app_ref_vector const& vars):
             m_fml(fml),
             m_var(var),
             m_branch(b),
             m_result(r),
             m_coeff(coeff),
-            m_term(term)
+            m_term(term),
+            m_vars(vars.size(), vars.c_ptr())
         {}
         
         unsigned mk_hash() const {
@@ -1544,6 +1554,7 @@ public:
             if (get_cache(x, fml, v, result)) {
                 return;
             }
+            m_util.m_vars_added.reset();
             
             bounds_proc& bounds = get_bounds(x, fml);            
             bool is_lower = get_bound_sizes(bounds, x, t_size, e_size);            
@@ -1601,8 +1612,7 @@ public:
             expr_ref t(bounds.exprs(is_strict, is_lower)[index], m);
             rational a = bounds.coeffs(is_strict, is_lower)[index];
 
-            
+                                            
-                                
             mk_bounds(bounds, x, true,  is_eq, is_strict, is_lower, index, a, t, result);
             mk_bounds(bounds, x, false, is_eq, is_strict, is_lower, index, a, t, result);
 
@@ -1617,7 +1627,7 @@ public:
                   {
                       tout << vl << " " << mk_pp(bounds.atoms(is_strict, is_lower)[index],m) << "\n";
                       tout << mk_pp(fml, m) << "\n";
-                      tout << mk_pp(result, m) << "\n";
+                      tout << result << "\n";
                   }
                   );
         }
@@ -1637,7 +1647,7 @@ public:
 
         virtual void subst(contains_app& contains_x, rational const& vl, expr_ref& fml, expr_ref* def) {
             SASSERT(vl.is_unsigned());            
-           if (def) {
+            if (def) {
                get_def(contains_x, vl.get_unsigned(), fml, *def);
             }
             VERIFY(get_cache(contains_x.x(), fml, vl.get_unsigned(), fml));
@@ -1740,7 +1750,7 @@ public:
             x_subst x_t(m_util);
             bounds_proc& bounds = get_bounds(x, fml);    
             branch_formula bf;
-            VERIFY (m_subst.find(branch_formula(fml, x, v, 0, rational::zero(), 0), bf));
+            VERIFY (m_subst.find(branch_formula(fml, x, v, 0, rational::zero(), 0, m_util.m_vars_added), bf));
             x_t.set_term(bf.m_term);
             x_t.set_coeff(bf.m_coeff);
 
@@ -2022,16 +2032,19 @@ public:
             m_trail.push_back(fml);
             m_trail.push_back(result);
             if (term) m_trail.push_back(term);
-            m_subst.insert(branch_formula(fml, x, v, result, coeff, term));
+            m_subst.insert(branch_formula(fml, x, v, result, coeff, term, m_util.m_vars_added));
         }
         
         bool get_cache(app* x, expr* fml, unsigned v, expr_ref& result) {
             branch_formula bf;
-            if (!m_subst.find(branch_formula(fml, x, v, 0, rational::zero(), 0), bf)) {
+            if (!m_subst.find(branch_formula(fml, x, v, 0, rational::zero(), 0, m_util.m_vars_added), bf)) {
                 return false;
             }
             SASSERT(bf.m_result);
             result = bf.m_result;
+            for (app* v : bf.m_vars) {
+                m_util.add_var(v, false);
+            }            
             return true;
         }
 
@@ -2043,7 +2056,7 @@ public:
             if (!bounds.div_z(d, z_bv, z)) {
                 return;
             }
-            m_ctx.add_var(z_bv);
+            m_util.add_var(z_bv);
             
             //
             // assert 
@@ -2120,7 +2133,7 @@ public:
                 app* z1_bv = bounds.nested_div_z_bv(i);
                 app* z1 = bounds.nested_div_z(i);
 
-                m_ctx.add_var(z1_bv);
+                m_util.add_var(z1_bv);
 
                 //
                 // assert

src/qe/qe_sat_tactic.cpp

@@ -122,7 +122,7 @@ namespace qe {
             // Access current set of variables to solve
             virtual unsigned      get_num_vars() const { return m_vars.size(); }
             virtual app*          get_var(unsigned idx) const {  return m_vars[idx]; }
-            virtual app*const*    get_vars() const { return m_vars.c_ptr(); }
+            virtual app_ref_vector const& get_vars() const { return m_vars; }
             virtual bool          is_var(expr* e, unsigned& idx) const {
                 for (unsigned i = 0; i < m_vars.size(); ++i) {
                     if (e == m_vars[i]) return (idx = i, true);