mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity

build fixes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-07-18 19:14:45 -07:00
parent 3d8f75b3d8
commit e8a38c5482
3 changed files with 10 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
scripts/update_api.py
View file

@ -426,6 +426,7 @@ def mk_dotnet(dotnet):
dotnet.write(' {\n\n') dotnet.write(' {\n\n')
for name, ret, sig in Closures: for name, ret, sig in Closures:
sig = sig.replace("unsigned const*","uint[]")
sig = sig.replace("void*","voidp").replace("unsigned","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") 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")

9
src/api/c++/z3++.h
View file

@ -4214,17 +4214,20 @@ namespace z3 {
return expr(ctx(), r); return expr(ctx(), r);
} }
typedef std::function<void(expr const& proof, expr_vector const& clause)> on_clause_eh_t; typedef std::function<void(expr const& proof, std::vector<unsigned> const& deps, expr_vector const& clause)> on_clause_eh_t;
class on_clause { class on_clause {
context& c; context& c;
on_clause_eh_t m_on_clause; 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<on_clause*>(_ctx); on_clause* ctx = static_cast<on_clause*>(_ctx);
expr_vector lits(ctx->c, _literals); expr_vector lits(ctx->c, _literals);
expr proof(ctx->c, _proof); expr proof(ctx->c, _proof);
ctx->m_on_clause(proof, lits); std::vector<unsigned> deps;
for (unsigned i = 0; i < n; ++i)
deps.push_back(dep[i]);
ctx->m_on_clause(proof, deps, lits);
} }
public: public:
on_clause(solver& s, on_clause_eh_t& on_clause_eh): c(s.ctx()) { on_clause(solver& s, on_clause_eh_t& on_clause_eh): c(s.ctx()) {

3
src/api/dotnet/OnClause.cs
View file

@ -30,6 +30,7 @@ namespace Microsoft.Z3
using Z3_context = System.IntPtr; using Z3_context = System.IntPtr;
using Z3_solver = System.IntPtr; using Z3_solver = System.IntPtr;
using voidp = System.IntPtr; using voidp = System.IntPtr;
using uintp = System.IntPtr;
using Z3_ast = System.IntPtr; using Z3_ast = System.IntPtr;
using Z3_ast_vector = System.IntPtr; using Z3_ast_vector = System.IntPtr;
@ -60,7 +61,7 @@ namespace Microsoft.Z3
Native.Z3_on_clause_eh on_clause_eh; 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; var onc = (OnClause)GCHandle.FromIntPtr(ctx).Target;
using var proof_hint = Expr.Create(onc.ctx, _proof_hint); using var proof_hint = Expr.Create(onc.ctx, _proof_hint);