mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-10 07:10:30 +00:00
Code Activity

Go: Add MkBVRotateLeft, MkBVRotateRight, MkRepeat to bitvec.go

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-03-09 16:20:13 +00:00
parent 0af49cdf10
commit 47e9c37fbb
1 changed files with 15 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -159,6 +159,21 @@ func (c *Context) MkZeroExt(i uint, expr *Expr) *Expr {
return newExpr(c, C.Z3_mk_zero_ext(c.ptr, C.uint(i), expr.ptr))
}
// MkBVRotateLeft rotates the bits of t to the left by i positions.
func (c *Context) MkBVRotateLeft(i uint, t *Expr) *Expr {
return newExpr(c, C.Z3_mk_rotate_left(c.ptr, C.uint(i), t.ptr))
}
// MkBVRotateRight rotates the bits of t to the right by i positions.
func (c *Context) MkBVRotateRight(i uint, t *Expr) *Expr {
return newExpr(c, C.Z3_mk_rotate_right(c.ptr, C.uint(i), t.ptr))
}
// MkRepeat repeats the given bit-vector t a total of i times.
func (c *Context) MkRepeat(i uint, t *Expr) *Expr {
return newExpr(c, C.Z3_mk_repeat(c.ptr, C.uint(i), t.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 {