diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp index 2d7d051c5..732a89099 100644 --- a/examples/c++/example.cpp +++ b/examples/c++/example.cpp @@ -470,7 +470,7 @@ void unsat_core_example2() { // The solver s already contains p1 => F // To disable F, we add (not p1) as an additional assumption qs.push_back(!p1); - std::cout << s.check(qs.size(), &qs[0]) << "\n"; + std::cout << s.check(static_cast(qs.size()), &qs[0]) << "\n"; expr_vector core2 = s.unsat_core(); std::cout << core2 << "\n"; std::cout << "size: " << core2.size() << "\n"; @@ -1136,7 +1136,7 @@ static void parse_example() { 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); + expr_vector a = c.parse_string("(assert a)", sorts, decls); std::cout << a << "\n"; } diff --git a/examples/c/test_capi.c b/examples/c/test_capi.c index 88fdaa1cf..56b402ad5 100644 --- a/examples/c/test_capi.c +++ b/examples/c/test_capi.c @@ -2632,13 +2632,16 @@ void reference_counter_example() { */ void smt2parser_example() { Z3_context ctx; - Z3_ast fs; + Z3_ast_vector fs; printf("\nsmt2parser_example\n"); LOG_MSG("smt2parser_example"); ctx = mk_context(); fs = Z3_parse_smtlib2_string(ctx, "(declare-fun a () (_ BitVec 8)) (assert (bvuge a #x10)) (assert (bvule a #xf0))", 0, 0, 0, 0, 0, 0); - printf("formulas: %s\n", Z3_ast_to_string(ctx, fs)); + Z3_ast_vector_inc_ref(ctx, fs); + printf("formulas: %s\n", Z3_ast_vector_to_string(ctx, fs)); + Z3_ast_vector_dec_ref(ctx, fs); + Z3_del_context(ctx); } diff --git a/src/api/api_interp.cpp b/src/api/api_interp.cpp index 10aa06568..abfca9827 100644 --- a/src/api/api_interp.cpp +++ b/src/api/api_interp.cpp @@ -511,12 +511,13 @@ extern "C" { try { std::string foo(filename); if (foo.size() >= 5 && foo.substr(foo.size() - 5) == ".smt2"){ - Z3_ast assrts = Z3_parse_smtlib2_file(ctx, filename, 0, 0, 0, 0, 0, 0); - Z3_app app = Z3_to_app(ctx, assrts); - int nconjs = Z3_get_app_num_args(ctx, app); + Z3_ast_vector assrts = Z3_parse_smtlib2_file(ctx, filename, 0, 0, 0, 0, 0, 0); + Z3_ast_vector_inc_ref(ctx, assrts); + unsigned nconjs = Z3_ast_vector_size(ctx, assrts); assertions.resize(nconjs); - for (int k = 0; k < nconjs; k++) - assertions[k] = Z3_get_app_arg(ctx, app, k); + for (unsigned k = 0; k < nconjs; k++) + assertions[k] = Z3_ast_vector_get(ctx, assrts, k); + // Z3_ast_vector_dec_ref(ctx, assrts) is unsafe } else { Z3_parse_smtlib_file(ctx, filename, 0, 0, 0, 0, 0, 0); diff --git a/src/api/api_parsers.cpp b/src/api/api_parsers.cpp index 8f6eb1125..29c7fa707 100644 --- a/src/api/api_parsers.cpp +++ b/src/api/api_parsers.cpp @@ -24,6 +24,7 @@ Revision History: #include"smt2parser.h" #include"smtparser.h" #include"solver_na2as.h" +#include"api_ast_vector.h" extern "C" { @@ -252,7 +253,7 @@ extern "C" { // --------------- // Support for SMTLIB2 - Z3_ast parse_smtlib2_stream(bool exec, Z3_context c, std::istream& is, + Z3_ast_vector parse_smtlib2_stream(bool exec, Z3_context c, std::istream& is, unsigned num_sorts, Z3_symbol const sort_names[], Z3_sort const sorts[], @@ -262,6 +263,9 @@ extern "C" { Z3_TRY; cmd_context ctx(false, &(mk_c(c)->m())); ctx.set_ignore_check(true); + Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m()); + mk_c(c)->save_object(v); + for (unsigned i = 0; i < num_decls; ++i) { ctx.insert(to_symbol(decl_names[i]), to_func_decl(decls[i])); } @@ -271,16 +275,18 @@ extern "C" { } if (!parse_smt2_commands(ctx, is)) { SET_ERROR_CODE(Z3_PARSER_ERROR); - return of_ast(mk_c(c)->m().mk_true()); + return of_ast_vector(v); } ptr_vector::const_iterator it = ctx.begin_assertions(); ptr_vector::const_iterator end = ctx.end_assertions(); - unsigned size = static_cast(end - it); - return of_ast(mk_c(c)->mk_and(size, it)); + for (; it != end; ++it) { + v->m_ast_vector.push_back(*it); + } + return of_ast_vector(v); Z3_CATCH_RETURN(0); } - Z3_ast Z3_API Z3_parse_smtlib2_string(Z3_context c, Z3_string str, + Z3_ast_vector Z3_API Z3_parse_smtlib2_string(Z3_context c, Z3_string str, unsigned num_sorts, Z3_symbol const sort_names[], Z3_sort const sorts[], @@ -291,12 +297,12 @@ extern "C" { LOG_Z3_parse_smtlib2_string(c, str, num_sorts, sort_names, sorts, num_decls, decl_names, decls); std::string s(str); std::istringstream is(s); - Z3_ast r = parse_smtlib2_stream(false, c, is, num_sorts, sort_names, sorts, num_decls, decl_names, decls); + Z3_ast_vector r = parse_smtlib2_stream(false, c, is, num_sorts, sort_names, sorts, num_decls, decl_names, decls); RETURN_Z3(r); Z3_CATCH_RETURN(0); } - Z3_ast Z3_API Z3_parse_smtlib2_file(Z3_context c, Z3_string file_name, + Z3_ast_vector Z3_API Z3_parse_smtlib2_file(Z3_context c, Z3_string file_name, unsigned num_sorts, Z3_symbol const sort_names[], Z3_sort const sorts[], @@ -310,7 +316,7 @@ extern "C" { SET_ERROR_CODE(Z3_PARSER_ERROR); return 0; } - Z3_ast r = parse_smtlib2_stream(false, c, is, num_sorts, sort_names, sorts, num_decls, decl_names, decls); + Z3_ast_vector r = parse_smtlib2_stream(false, c, is, num_sorts, sort_names, sorts, num_decls, decl_names, decls); RETURN_Z3(r); Z3_CATCH_RETURN(0); } diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 9d9982523..bd03237be 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -309,11 +309,11 @@ namespace z3 { /** \brief parsing */ - expr parse_string(char const* s); - expr parse_file(char const* file); + expr_vector parse_string(char const* s); + expr_vector parse_file(char const* file); - expr parse_string(char const* s, sort_vector const& sorts, func_decl_vector const& decls); - expr parse_file(char const* s, sort_vector const& sorts, func_decl_vector const& decls); + expr_vector parse_string(char const* s, sort_vector const& sorts, func_decl_vector const& decls); + expr_vector parse_file(char const* s, sort_vector const& sorts, func_decl_vector const& decls); /** \brief Interpolation support @@ -2701,19 +2701,19 @@ namespace z3 { return expr(a.ctx(), Z3_mk_interpolant(a.ctx(), a)); } - inline expr context::parse_string(char const* s) { - Z3_ast r = Z3_parse_smtlib2_string(*this, s, 0, 0, 0, 0, 0, 0); + inline expr_vector context::parse_string(char const* s) { + Z3_ast_vector r = Z3_parse_smtlib2_string(*this, s, 0, 0, 0, 0, 0, 0); check_error(); - return expr(*this, r); + return expr_vector(*this, r); } - inline expr context::parse_file(char const* s) { - Z3_ast r = Z3_parse_smtlib2_file(*this, s, 0, 0, 0, 0, 0, 0); + inline expr_vector context::parse_file(char const* s) { + Z3_ast_vector r = Z3_parse_smtlib2_file(*this, s, 0, 0, 0, 0, 0, 0); check_error(); - return expr(*this, r); + return expr_vector(*this, r); } - inline expr context::parse_string(char const* s, sort_vector const& sorts, func_decl_vector const& decls) { + inline expr_vector context::parse_string(char const* s, sort_vector const& sorts, func_decl_vector const& decls) { array sort_names(sorts.size()); array decl_names(decls.size()); array sorts1(sorts); @@ -2724,12 +2724,12 @@ namespace z3 { for (unsigned i = 0; i < decls.size(); ++i) { decl_names[i] = decls[i].name(); } - Z3_ast r = Z3_parse_smtlib2_string(*this, s, sorts.size(), sort_names.ptr(), sorts1.ptr(), decls.size(), decl_names.ptr(), decls1.ptr()); + Z3_ast_vector r = Z3_parse_smtlib2_string(*this, s, sorts.size(), sort_names.ptr(), sorts1.ptr(), decls.size(), decl_names.ptr(), decls1.ptr()); check_error(); - return expr(*this, r); + return expr_vector(*this, r); } - inline expr context::parse_file(char const* s, sort_vector const& sorts, func_decl_vector const& decls) { + inline expr_vector context::parse_file(char const* s, sort_vector const& sorts, func_decl_vector const& decls) { array sort_names(sorts.size()); array decl_names(decls.size()); array sorts1(sorts); @@ -2740,9 +2740,9 @@ namespace z3 { 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()); + Z3_ast_vector 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); + return expr_vector(*this, r); } diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index a656be3eb..a6614a202 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -3390,7 +3390,7 @@ namespace Microsoft.Z3 /// /// /// A conjunction of assertions in the scope (up to push/pop) at the end of the string. - public BoolExpr ParseSMTLIB2String(string str, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null) + public BoolExpr[] ParseSMTLIB2String(string str, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null) { Contract.Ensures(Contract.Result() != null); @@ -3400,16 +3400,17 @@ namespace Microsoft.Z3 uint cd = AST.ArrayLength(decls); if (csn != cs || cdn != cd) throw new Z3Exception("Argument size mismatch"); - return (BoolExpr)Expr.Create(this, Native.Z3_parse_smtlib2_string(nCtx, str, + ASTVector assertions = new ASTVector(this, Native.Z3_parse_smtlib2_string(nCtx, str, AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts), AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls))); + return assertions.ToBoolExprArray(); } /// /// Parse the given file using the SMT-LIB2 parser. /// /// - public BoolExpr ParseSMTLIB2File(string fileName, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null) + public BoolExpr[] ParseSMTLIB2File(string fileName, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null) { Contract.Ensures(Contract.Result() != null); @@ -3419,9 +3420,10 @@ namespace Microsoft.Z3 uint cd = AST.ArrayLength(decls); if (csn != cs || cdn != cd) throw new Z3Exception("Argument size mismatch"); - return (BoolExpr)Expr.Create(this, Native.Z3_parse_smtlib2_file(nCtx, fileName, + ASTVector assertions = new ASTVector(this, Native.Z3_parse_smtlib2_file(nCtx, fileName, AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts), AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls))); + return assertions.ToBoolExprArray(); } #endregion diff --git a/src/api/java/Context.java b/src/api/java/Context.java index db7a08711..d9e938086 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -2621,7 +2621,7 @@ public class Context implements AutoCloseable { * @return A conjunction of assertions in the scope (up to push/pop) at the * end of the string. **/ - public BoolExpr parseSMTLIB2String(String str, Symbol[] sortNames, + public BoolExpr[] parseSMTLIB2String(String str, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls) { @@ -2633,17 +2633,18 @@ public class Context implements AutoCloseable { if (csn != cs || cdn != cd) { throw new Z3Exception("Argument size mismatch"); } - return (BoolExpr) Expr.create(this, Native.parseSmtlib2String(nCtx(), + ASTVector v = new ASTVector(this, Native.parseSmtlib2String(nCtx(), str, AST.arrayLength(sorts), Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts), AST.arrayLength(decls), Symbol.arrayToNative(declNames), AST.arrayToNative(decls))); + return v.ToBoolExprArray(); } /** * Parse the given file using the SMT-LIB2 parser. * @see #parseSMTLIB2String **/ - public BoolExpr parseSMTLIB2File(String fileName, Symbol[] sortNames, + public BoolExpr[] parseSMTLIB2File(String fileName, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls) { @@ -2653,11 +2654,12 @@ public class Context implements AutoCloseable { int cd = AST.arrayLength(decls); if (csn != cs || cdn != cd) throw new Z3Exception("Argument size mismatch"); - return (BoolExpr) Expr.create(this, Native.parseSmtlib2File(nCtx(), + ASTVector v = new ASTVector(this, Native.parseSmtlib2File(nCtx(), fileName, AST.arrayLength(sorts), Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts), AST.arrayLength(decls), Symbol.arrayToNative(declNames), AST.arrayToNative(decls))); + return v.ToBoolExprArray(); } /** diff --git a/src/api/z3_api.h b/src/api/z3_api.h index e3bd942bd..4ae7c5c22 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -5059,9 +5059,9 @@ extern "C" { It returns a formula comprising of the conjunction of assertions in the scope (up to push/pop) at the end of the string. - def_API('Z3_parse_smtlib2_string', AST, (_in(CONTEXT), _in(STRING), _in(UINT), _in_array(2, SYMBOL), _in_array(2, SORT), _in(UINT), _in_array(5, SYMBOL), _in_array(5, FUNC_DECL))) + def_API('Z3_parse_smtlib2_string', AST_VECTOR, (_in(CONTEXT), _in(STRING), _in(UINT), _in_array(2, SYMBOL), _in_array(2, SORT), _in(UINT), _in_array(5, SYMBOL), _in_array(5, FUNC_DECL))) */ - Z3_ast Z3_API Z3_parse_smtlib2_string(Z3_context c, + Z3_ast_vector Z3_API Z3_parse_smtlib2_string(Z3_context c, Z3_string str, unsigned num_sorts, Z3_symbol const sort_names[], @@ -5073,9 +5073,9 @@ extern "C" { /** \brief Similar to #Z3_parse_smtlib2_string, but reads the benchmark from a file. - def_API('Z3_parse_smtlib2_file', AST, (_in(CONTEXT), _in(STRING), _in(UINT), _in_array(2, SYMBOL), _in_array(2, SORT), _in(UINT), _in_array(5, SYMBOL), _in_array(5, FUNC_DECL))) + def_API('Z3_parse_smtlib2_file', AST_VECTOR, (_in(CONTEXT), _in(STRING), _in(UINT), _in_array(2, SYMBOL), _in_array(2, SORT), _in(UINT), _in_array(5, SYMBOL), _in_array(5, FUNC_DECL))) */ - Z3_ast Z3_API Z3_parse_smtlib2_file(Z3_context c, + Z3_ast_vector Z3_API Z3_parse_smtlib2_file(Z3_context c, Z3_string file_name, unsigned num_sorts, Z3_symbol const sort_names[], @@ -6045,7 +6045,6 @@ extern "C" { Z3_ast_vector Z3_API Z3_solver_get_lemmas(Z3_context c, Z3_solver s); - /** \brief Retrieve the model for the last #Z3_solver_check or #Z3_solver_check_assumptions @@ -6054,7 +6053,6 @@ extern "C" { def_API('Z3_solver_get_model', MODEL, (_in(CONTEXT), _in(SOLVER))) */ - Z3_model Z3_API Z3_solver_get_model(Z3_context c, Z3_solver s); /** diff --git a/src/test/smt2print_parse.cpp b/src/test/smt2print_parse.cpp index c79a80ae5..ba497d180 100644 --- a/src/test/smt2print_parse.cpp +++ b/src/test/smt2print_parse.cpp @@ -10,13 +10,21 @@ Copyright (c) 2015 Microsoft Corporation #include "z3.h" #include -void test_print(Z3_context ctx, Z3_ast a) { +void test_print(Z3_context ctx, Z3_ast_vector av) { Z3_set_ast_print_mode(ctx, Z3_PRINT_SMTLIB2_COMPLIANT); + Z3_ast* args = new Z3_ast[Z3_ast_vector_size(ctx, av)]; + for (unsigned i = 0; i < Z3_ast_vector_size(ctx, av); ++i) { + args[i] = Z3_ast_vector_get(ctx, av, i); + } + Z3_ast a = Z3_mk_and(ctx, Z3_ast_vector_size(ctx, av), args); + Z3_inc_ref(ctx, a); + delete[] args; char const* spec1 = Z3_benchmark_to_smtlib_string(ctx, "test", 0, 0, 0, 0, 0, a); + Z3_dec_ref(ctx, a); std::cout << "spec1: benchmark->string\n" << spec1 << "\n"; std::cout << "attempting to parse spec1...\n"; - Z3_ast b = + Z3_ast_vector b = Z3_parse_smtlib2_string(ctx, spec1, 0, @@ -26,15 +34,17 @@ void test_print(Z3_context ctx, Z3_ast a) { 0, 0); std::cout << "parse successful, converting ast->string\n"; - char const* spec2 = Z3_ast_to_string(ctx, b); + Z3_ast_vector_inc_ref(ctx, b); + char const* spec2 = Z3_ast_vector_to_string(ctx, b); std::cout << "spec2: string->ast->string\n" << spec2 << "\n"; + Z3_ast_vector_dec_ref(ctx, b); } void test_parseprint(char const* spec) { Z3_context ctx = Z3_mk_context(0); std::cout << "spec:\n" << spec << "\n"; - Z3_ast a = + Z3_ast_vector a = Z3_parse_smtlib2_string(ctx, spec, 0, @@ -45,11 +55,12 @@ void test_parseprint(char const* spec) { 0); std::cout << "done parsing\n"; - + Z3_ast_vector_inc_ref(ctx, a); test_print(ctx, a); std::cout << "done printing\n"; + Z3_ast_vector_dec_ref(ctx, a); Z3_del_context(ctx); }