From b5c40e30ef20461600c21945d462331c8765d8a0 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 1 Nov 2015 12:12:41 -0800
Subject: [PATCH] feat(library/app_builder): add set_context

---
 src/library/app_builder.cpp | 4 ++++
 src/library/app_builder.h   | 7 +++++++
 2 files changed, 11 insertions(+)

diff --git a/src/library/app_builder.cpp b/src/library/app_builder.cpp
index 845e0bf7f..869b8c94e 100644
--- a/src/library/app_builder.cpp
+++ b/src/library/app_builder.cpp
@@ -226,4 +226,8 @@ optional<expr> app_builder::mk_app(name const & c, unsigned nargs, expr const *
 optional<expr> app_builder::mk_app(name const & c, unsigned mask_sz, bool const * mask, expr const * args) {
     return m_ptr->mk_app(c, mask_sz, mask, args);
 }
+
+void app_builder::set_context(list<expr> const & ctx) {
+    m_ptr->m_ctx->set_context(ctx);
+}
 }
diff --git a/src/library/app_builder.h b/src/library/app_builder.h
index e3aada5de..995bc89a3 100644
--- a/src/library/app_builder.h
+++ b/src/library/app_builder.h
@@ -62,5 +62,12 @@ public:
     }
 
     optional<expr> mk_app(name const & c, unsigned mask_sz, bool const * mask, expr const * args);
+
+    /** \brief Set the local context. This method is relevant when we want to expose local class instances
+        to the app_builder.
+
+        \remark When the constructor app_builder(std::unique_ptr<tmp_type_context> && ctx) is used
+        the initialization can be performed outside. */
+    void set_context(list<expr> const & ctx);
 };
 }