mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-04 18:59:02 +00:00
Code Activity

Add pseudo-Boolean/cardinality constraints to Go and OCaml APIs (#9182)

Browse source 
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/64ff2e48-47b1-4195-b154-ac38095dbbfb

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
Copilot 2026-03-31 13:44:52 -07:00 • committed by GitHub
parent 31425b07ca
commit 56eeb5b52c
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 115 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

94
src/api/go/z3.go
View file

@ -414,6 +414,100 @@ func (c *Context) MkDistinct(exprs ...*Expr) *Expr {
return newExpr(c, C.Z3_mk_distinct(c.ptr, C.uint(len(exprs)), &cExprs[0]))
}
// Pseudo-Boolean / cardinality constraints
// MkAtMost encodes p1 + p2 + ... + pn <= k.
func (c *Context) MkAtMost(args []*Expr, k uint) *Expr {
cArgs := make([]C.Z3_ast, len(args))
for i, a := range args {
cArgs[i] = a.ptr
}
var cArgsPtr *C.Z3_ast
if len(cArgs) > 0 {
cArgsPtr = &cArgs[0]
}
return newExpr(c, C.Z3_mk_atmost(c.ptr, C.uint(len(args)), cArgsPtr, C.uint(k)))
}
// MkAtLeast encodes p1 + p2 + ... + pn >= k.
func (c *Context) MkAtLeast(args []*Expr, k uint) *Expr {
cArgs := make([]C.Z3_ast, len(args))
for i, a := range args {
cArgs[i] = a.ptr
}
var cArgsPtr *C.Z3_ast
if len(cArgs) > 0 {
cArgsPtr = &cArgs[0]
}
return newExpr(c, C.Z3_mk_atleast(c.ptr, C.uint(len(args)), cArgsPtr, C.uint(k)))
}
// MkPBLe encodes k1*p1 + k2*p2 + ... + kn*pn <= k.
func (c *Context) MkPBLe(args []*Expr, coeffs []int, k int) *Expr {
if len(args) != len(coeffs) {
panic("MkPBLe: args and coeffs must have the same length")
}
cArgs := make([]C.Z3_ast, len(args))
for i, a := range args {
cArgs[i] = a.ptr
}
cCoeffs := make([]C.int, len(coeffs))
for i, v := range coeffs {
cCoeffs[i] = C.int(v)
}
var cArgsPtr *C.Z3_ast
var cCoeffsPtr *C.int
if len(cArgs) > 0 {
cArgsPtr = &cArgs[0]
cCoeffsPtr = &cCoeffs[0]
}
return newExpr(c, C.Z3_mk_pble(c.ptr, C.uint(len(args)), cArgsPtr, cCoeffsPtr, C.int(k)))
}
// MkPBGe encodes k1*p1 + k2*p2 + ... + kn*pn >= k.
func (c *Context) MkPBGe(args []*Expr, coeffs []int, k int) *Expr {
if len(args) != len(coeffs) {
panic("MkPBGe: args and coeffs must have the same length")
}
cArgs := make([]C.Z3_ast, len(args))
for i, a := range args {
cArgs[i] = a.ptr
}
cCoeffs := make([]C.int, len(coeffs))
for i, v := range coeffs {
cCoeffs[i] = C.int(v)
}
var cArgsPtr *C.Z3_ast
var cCoeffsPtr *C.int
if len(cArgs) > 0 {
cArgsPtr = &cArgs[0]
cCoeffsPtr = &cCoeffs[0]
}
return newExpr(c, C.Z3_mk_pbge(c.ptr, C.uint(len(args)), cArgsPtr, cCoeffsPtr, C.int(k)))
}
// MkPBEq encodes k1*p1 + k2*p2 + ... + kn*pn = k.
func (c *Context) MkPBEq(args []*Expr, coeffs []int, k int) *Expr {
if len(args) != len(coeffs) {
panic("MkPBEq: args and coeffs must have the same length")
}
cArgs := make([]C.Z3_ast, len(args))
for i, a := range args {
cArgs[i] = a.ptr
}
cCoeffs := make([]C.int, len(coeffs))
for i, v := range coeffs {
cCoeffs[i] = C.int(v)
}
var cArgsPtr *C.Z3_ast
var cCoeffsPtr *C.int
if len(cArgs) > 0 {
cArgsPtr = &cArgs[0]
cCoeffsPtr = &cCoeffs[0]
}
return newExpr(c, C.Z3_mk_pbeq(c.ptr, C.uint(len(args)), cArgsPtr, cCoeffsPtr, C.int(k)))
}
// FuncDecl represents a function declaration.
type FuncDecl struct {
ctx *Context

6
src/api/ml/z3.ml
View file

@ -587,6 +587,12 @@ struct
let mk_eq = Z3native.mk_eq
let mk_distinct ctx args = Z3native.mk_distinct ctx (List.length args) args
let mk_atmost ctx args k = Z3native.mk_atmost ctx (List.length args) args k
let mk_atleast ctx args k = Z3native.mk_atleast ctx (List.length args) args k
let mk_pble ctx args coeffs k = Z3native.mk_pble ctx (List.length args) args coeffs k
let mk_pbge ctx args coeffs k = Z3native.mk_pbge ctx (List.length args) args coeffs k
let mk_pbeq ctx args coeffs k = Z3native.mk_pbeq ctx (List.length args) args coeffs k
let get_bool_value x = lbool_of_int (Z3native.get_bool_value (gc x) x)
let is_bool x =

15
src/api/ml/z3.mli
View file

@ -632,6 +632,21 @@ sig
(** Creates a [distinct] term. *)
val mk_distinct : context -> Expr.expr list -> Expr.expr
(** Encodes p1 + p2 + ... + pn <= k. *)
val mk_atmost : context -> Expr.expr list -> int -> Expr.expr
(** Encodes p1 + p2 + ... + pn >= k. *)
val mk_atleast : context -> Expr.expr list -> int -> Expr.expr
(** Encodes k1*p1 + k2*p2 + ... + kn*pn <= k. *)
val mk_pble : context -> Expr.expr list -> int list -> int -> Expr.expr
(** Encodes k1*p1 + k2*p2 + ... + kn*pn >= k. *)
val mk_pbge : context -> Expr.expr list -> int list -> int -> Expr.expr
(** Encodes k1*p1 + k2*p2 + ... + kn*pn = k. *)
val mk_pbeq : context -> Expr.expr list -> int list -> int -> Expr.expr
(** Indicates whether the expression is the true or false expression
or something else (L_UNDEF). *)
val get_bool_value : Expr.expr -> Z3enums.lbool