mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-03 12:16:54 +00:00
Code Activity

Add 8 missing BV overflow/underflow check functions to Go bindings

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-03-01 01:51:27 +00:00
parent f80f279da9
commit 2b8615f4fc
1 changed files with 48 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

48
src/api/go/bitvec.go
View file

@ -158,3 +158,51 @@ func (c *Context) MkSignExt(i uint, expr *Expr) *Expr {
func (c *Context) MkZeroExt(i uint, expr *Expr) *Expr {
return newExpr(c, C.Z3_mk_zero_ext(c.ptr, C.uint(i), expr.ptr))
}
// MkBVAddNoOverflow creates a predicate that checks that the bit-wise addition
// of t1 and t2 does not overflow. If isSigned is true, checks for signed overflow.
func (c *Context) MkBVAddNoOverflow(t1, t2 *Expr, isSigned bool) *Expr {
return newExpr(c, C.Z3_mk_bvadd_no_overflow(c.ptr, t1.ptr, t2.ptr, C.bool(isSigned)))
}
// MkBVAddNoUnderflow creates a predicate that checks that the bit-wise signed addition
// of t1 and t2 does not underflow.
func (c *Context) MkBVAddNoUnderflow(t1, t2 *Expr) *Expr {
return newExpr(c, C.Z3_mk_bvadd_no_underflow(c.ptr, t1.ptr, t2.ptr))
}
// MkBVSubNoOverflow creates a predicate that checks that the bit-wise signed subtraction
// of t1 and t2 does not overflow.
func (c *Context) MkBVSubNoOverflow(t1, t2 *Expr) *Expr {
return newExpr(c, C.Z3_mk_bvsub_no_overflow(c.ptr, t1.ptr, t2.ptr))
}
// MkBVSubNoUnderflow creates a predicate that checks that the bit-wise subtraction
// of t1 and t2 does not underflow. If isSigned is true, checks for signed underflow.
func (c *Context) MkBVSubNoUnderflow(t1, t2 *Expr, isSigned bool) *Expr {
return newExpr(c, C.Z3_mk_bvsub_no_underflow(c.ptr, t1.ptr, t2.ptr, C.bool(isSigned)))
}
// MkBVSdivNoOverflow creates a predicate that checks that the bit-wise signed division
// of t1 and t2 does not overflow.
func (c *Context) MkBVSdivNoOverflow(t1, t2 *Expr) *Expr {
return newExpr(c, C.Z3_mk_bvsdiv_no_overflow(c.ptr, t1.ptr, t2.ptr))
}
// MkBVNegNoOverflow creates a predicate that checks that bit-wise negation does not overflow
// when t1 is interpreted as a signed bit-vector.
func (c *Context) MkBVNegNoOverflow(t1 *Expr) *Expr {
return newExpr(c, C.Z3_mk_bvneg_no_overflow(c.ptr, t1.ptr))
}
// MkBVMulNoOverflow creates a predicate that checks that the bit-wise multiplication
// of t1 and t2 does not overflow. If isSigned is true, checks for signed overflow.
func (c *Context) MkBVMulNoOverflow(t1, t2 *Expr, isSigned bool) *Expr {
return newExpr(c, C.Z3_mk_bvmul_no_overflow(c.ptr, t1.ptr, t2.ptr, C.bool(isSigned)))
}
// MkBVMulNoUnderflow creates a predicate that checks that the bit-wise signed multiplication
// of t1 and t2 does not underflow.
func (c *Context) MkBVMulNoUnderflow(t1, t2 *Expr) *Expr {
return newExpr(c, C.Z3_mk_bvmul_no_underflow(c.ptr, t1.ptr, t2.ptr))
}