How to use pble - Githubissues

ahumenberger / Z3.jl

Julia interface to Z3

MIT License

57 stars 7 forks source link

How to use pble #25

Closed MFaisalZaki closed 7 months ago

MFaisalZaki commented 11 months ago

I'm trying to assign weights to Boolean variables through z3.if(var, 1.0, 0.0) or using z3.PbLe([(var,1)], 1), but there is no clear way on how to invoke this in Julia; it works fine with the python wrapper. Any help?

remysucre commented 7 months ago

pble(ExprVector(ctx, [y]), [Int32(1)], 1)

In general you can refer to the C++ API doc since Z3.jl just wraps around that.