From edffdf857cf0c396c1a2885316b8bd09dc7b9c22 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 21 Nov 2017 16:07:10 -0800
Subject: [PATCH] use expr-vectors

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/ast_smt2_pp.cpp                        |  6 ++----
 src/model/model_pp.cpp                         |  6 ++----
 src/tactic/generic_model_converter.cpp         | 18 ++++++++++++++++--
 src/tactic/portfolio/bounded_int2bv_solver.cpp |  8 ++++----
 4 files changed, 24 insertions(+), 14 deletions(-)

diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp
index bb5359c19..f6169a851 100644
--- a/src/ast/ast_smt2_pp.cpp
+++ b/src/ast/ast_smt2_pp.cpp
@@ -1031,10 +1031,8 @@ class smt2_printer {
 
     void reset_expr2alias_stack() {
         SASSERT(!m_expr2alias_stack.empty());
-        ptr_vector<expr2alias>::iterator it  = m_expr2alias_stack.begin();
-        ptr_vector<expr2alias>::iterator end = m_expr2alias_stack.end();
-        for (; it != end; ++it)
-            (*it)->reset();
+        for (expr2alias * e : m_expr2alias_stack) 
+            e->reset();
         m_expr2alias = m_expr2alias_stack[0];
     }
 
diff --git a/src/model/model_pp.cpp b/src/model/model_pp.cpp
index 2f9b114bb..08d63803b 100644
--- a/src/model/model_pp.cpp
+++ b/src/model/model_pp.cpp
@@ -31,10 +31,8 @@ static void display_uninterp_sorts(std::ostream & out, model_core const & md) {
         sort * s = md.get_uninterpreted_sort(i);
         out << "(define-sort " << mk_pp(s, m); 
         ptr_vector<expr> const & univ  = md.get_universe(s);
-        ptr_vector<expr>::const_iterator it  = univ.begin();
-        ptr_vector<expr>::const_iterator end = univ.end();
-        for (; it != end; ++it) {
-            out << " " << mk_ismt2_pp(*it, m);
+        for (expr* e : univ) {
+            out << " " << mk_ismt2_pp(e, m);
         }
         out << ")\n";
     }
diff --git a/src/tactic/generic_model_converter.cpp b/src/tactic/generic_model_converter.cpp
index 19caa62ac..ae75028b0 100644
--- a/src/tactic/generic_model_converter.cpp
+++ b/src/tactic/generic_model_converter.cpp
@@ -19,6 +19,7 @@ Notes:
 --*/
 #include "ast/ast_pp.h"
 #include "ast/for_each_expr.h"
+#include "ast/ast_util.h"
 #include "tactic/generic_model_converter.h"
 #include "model/model_v2_pp.h"
 #include "model/model_evaluator.h"
@@ -101,19 +102,32 @@ struct min_app_idx_proc {
 void generic_model_converter::operator()(expr_ref& fml) {
     min_app_idx_proc min_proc(m_first_idx);
     for_each_expr(min_proc, fml);
+    expr_ref_vector fmls(m);
+    fmls.push_back(fml);
     unsigned min_idx = min_proc.m_min;
     for (unsigned i = m_add_entries.size(); i-- > min_idx;) {
         entry const& e = m_add_entries[i];
         unsigned arity = e.m_f->get_arity();
         if (arity == 0) {
-            fml = m.mk_and(fml, m.mk_eq(m.mk_const(e.m_f), e.m_def));
+            fmls.push_back(m.mk_eq(m.mk_const(e.m_f), e.m_def));
         }
         else {
-            NOT_IMPLEMENTED_YET();
+            expr_ref_vector args(m);
+            sort_ref_vector sorts(m);
+            svector<symbol> names;
+            for (unsigned i = 0; i < arity; ++i) {
+                sorts.push_back(e.m_f->get_domain(i));
+                names.push_back(symbol(i));
+                args.push_back(m.mk_var(i, sorts.back()));
+            }
+            expr_ref lhs(m.mk_app(e.m_f, arity, args.c_ptr()), m);
+            expr_ref body(m.mk_eq(lhs, e.m_def), m);
+            fmls.push_back(m.mk_forall(arity, sorts.c_ptr(), names.c_ptr(), body));
         }
         if (m_first_idx[e.m_f] == i) {
             m_first_idx.remove(e.m_f);
         }
         m_add_entries.pop_back();
     }
+    fml = mk_and(fmls);
 }
diff --git a/src/tactic/portfolio/bounded_int2bv_solver.cpp b/src/tactic/portfolio/bounded_int2bv_solver.cpp
index 7a8a0930c..a2f4cabe4 100644
--- a/src/tactic/portfolio/bounded_int2bv_solver.cpp
+++ b/src/tactic/portfolio/bounded_int2bv_solver.cpp
@@ -304,8 +304,8 @@ private:
     void flush_assertions() const {
         if (m_assertions.empty()) return;
         bound_manager& bm = *m_bounds.back();
-        for (unsigned i = 0; i < m_assertions.size(); ++i) {
-            bm(m_assertions[i].get());
+        for (expr* a : m_assertions) {
+            bm(a);
         }
         TRACE("int2bv", bm.display(tout););
         expr_safe_replace sub(m);
@@ -316,8 +316,8 @@ private:
             m_solver->assert_expr(m_assertions);
         }
         else {
-            for (unsigned i = 0; i < m_assertions.size(); ++i) {
-                sub(m_assertions[i].get(), fml1);
+            for (expr* a : m_assertions) {
+                sub(a, fml1);
                 m_rewriter(fml1, fml2, proof);
                 if (m.canceled()) {
                     m_rewriter.reset();