From e8a38c548235d21c9f075cc9cdbe473fc68ef8bd Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 18 Jul 2023 19:14:45 -0700 Subject: [PATCH] build fixes Signed-off-by: Nikolaj Bjorner --- scripts/update_api.py | 3 ++- src/api/c++/z3++.h | 9 ++++++--- src/api/dotnet/OnClause.cs | 3 ++- 3 files changed, 10 insertions(+), 5 deletions(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index ad76b9be0..5f8db1932 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -426,9 +426,10 @@ def mk_dotnet(dotnet): dotnet.write(' {\n\n') for name, ret, sig in Closures: + sig = sig.replace("unsigned const*","uint[]") sig = sig.replace("void*","voidp").replace("unsigned","uint") sig = sig.replace("Z3_ast*","ref IntPtr").replace("uint*","ref uint").replace("Z3_lbool*","ref int") - ret = ret.replace("void*","voidp").replace("unsigned","uint") + ret = ret.replace("void*","voidp").replace("unsigned","uint") if "*" in sig or "*" in ret: continue dotnet.write(' [UnmanagedFunctionPointer(CallingConvention.Cdecl)]\n') diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 4e51e83dd..2f59a6ee7 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -4214,17 +4214,20 @@ namespace z3 { return expr(ctx(), r); } - typedef std::function on_clause_eh_t; + typedef std::function const& deps, expr_vector const& clause)> on_clause_eh_t; class on_clause { context& c; on_clause_eh_t m_on_clause; - static void _on_clause_eh(void* _ctx, Z3_ast _proof, Z3_ast_vector _literals) { + static void _on_clause_eh(void* _ctx, Z3_ast _proof, unsigned n, unsigned const* dep, Z3_ast_vector _literals) { on_clause* ctx = static_cast(_ctx); expr_vector lits(ctx->c, _literals); expr proof(ctx->c, _proof); - ctx->m_on_clause(proof, lits); + std::vector deps; + for (unsigned i = 0; i < n; ++i) + deps.push_back(dep[i]); + ctx->m_on_clause(proof, deps, lits); } public: on_clause(solver& s, on_clause_eh_t& on_clause_eh): c(s.ctx()) { diff --git a/src/api/dotnet/OnClause.cs b/src/api/dotnet/OnClause.cs index 686318928..05defb312 100644 --- a/src/api/dotnet/OnClause.cs +++ b/src/api/dotnet/OnClause.cs @@ -30,6 +30,7 @@ namespace Microsoft.Z3 using Z3_context = System.IntPtr; using Z3_solver = System.IntPtr; using voidp = System.IntPtr; + using uintp = System.IntPtr; using Z3_ast = System.IntPtr; using Z3_ast_vector = System.IntPtr; @@ -60,7 +61,7 @@ namespace Microsoft.Z3 Native.Z3_on_clause_eh on_clause_eh; - static void _on_clause(voidp ctx, Z3_ast _proof_hint, Z3_ast_vector _clause) + static void _on_clause(voidp ctx, Z3_ast _proof_hint, uint n, uint[] deps, Z3_ast_vector _clause) { var onc = (OnClause)GCHandle.FromIntPtr(ctx).Target; using var proof_hint = Expr.Create(onc.ctx, _proof_hint);