From 5d9820f3e2d4c49389536092a90aca1be720555d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 7 Oct 2016 12:57:07 -0700
Subject: [PATCH] add example of parsing with external declarations

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 examples/c++/example.cpp | 12 ++++++++++++
 src/api/c++/z3++.h       | 17 +++++++++++++++--
 2 files changed, 27 insertions(+), 2 deletions(-)

diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp
index a1240543f..2d7d051c5 100644
--- a/examples/c++/example.cpp
+++ b/examples/c++/example.cpp
@@ -1129,6 +1129,17 @@ void consequence_example() {
     std::cout << consequences << "\n";
 }
 
+static void parse_example() {
+    std::cout << "parse example\n";
+    context c;
+    sort_vector sorts(c);
+    func_decl_vector decls(c);
+    sort B = c.bool_sort();
+    decls.push_back(c.function("a", 0, 0, B));
+    expr a = c.parse_string("(assert a)", sorts, decls);
+    std::cout << a << "\n";
+}
+
 int main() {
 
     try {
@@ -1173,6 +1184,7 @@ int main() {
         param_descrs_example(); std::cout << "\n";
         sudoku_example(); std::cout << "\n";
         consequence_example(); std::cout << "\n";
+        parse_example(); std::cout << "\n";
         std::cout << "done\n";
     }
     catch (exception & ex) {
diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index e72acf3d6..b03e38b7e 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -2460,7 +2460,6 @@ namespace z3 {
         return expr(re.ctx(), r);
     }
 
-
     inline expr interpolant(expr const& a) {
         return expr(a.ctx(), Z3_mk_interpolant(a.ctx(), a));
     }
@@ -2493,7 +2492,21 @@ namespace z3 {
         return expr(*this, r);
     }
 
-    // inline expr context::parse_file(char const* s, sort_vector const& sorts, func_decl_vector const& decls);
+    inline expr context::parse_file(char const* s, sort_vector const& sorts, func_decl_vector const& decls) {
+        array<Z3_symbol> sort_names(sorts.size());
+        array<Z3_symbol> decl_names(decls.size());
+        array<Z3_sort>   sorts1(sorts);
+        array<Z3_func_decl> decls1(decls);
+        for (unsigned i = 0; i < sorts.size(); ++i) {
+            sort_names[i] = sorts[i].name();
+        }
+        for (unsigned i = 0; i < decls.size(); ++i) {
+            decl_names[i] = decls[i].name();
+        }
+        Z3_ast r = Z3_parse_smtlib2_file(*this, s, sorts.size(), sort_names.ptr(), sorts1.ptr(), decls.size(), decl_names.ptr(), decls1.ptr());
+        check_error();
+        return expr(*this, r);
+    }
 
 
     inline check_result context::compute_interpolant(expr const& pat, params const& p, expr_vector& i, model& m) {