mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-17 06:11:44 +00:00
Code Activity

Simplify Go bindings: refactor GetLowerAsVector and GetUpperAsVector to use astVectorToExprs helper

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-02-17 03:46:58 +00:00
parent 966e651b8b
commit 5a9f416837
1 changed files with 7 additions and 23 deletions
Download patch file Download diff file Expand all files Collapse all files

30
src/api/go/optimize.go
View file

@ -54,7 +54,7 @@ func (o *Optimize) AssertSoft(constraint *Expr, weight string, group string) uin
cGroup := C.CString(group)
defer C.free(unsafe.Pointer(cWeight))
defer C.free(unsafe.Pointer(cGroup))
sym := o.ctx.MkStringSymbol(group)
return uint(C.Z3_optimize_assert_soft(o.ctx.ptr, o.ptr, constraint.ptr, cWeight, sym.ptr))
}
@ -128,19 +128,11 @@ func (o *Optimize) GetUpper(index uint) *Expr {
// otherwise it's represented as value + eps * EPSILON.
func (o *Optimize) GetLowerAsVector(index uint) []*Expr {
vec := C.Z3_optimize_get_lower_as_vector(o.ctx.ptr, o.ptr, C.uint(index))
// Increment reference count for the vector since we're using it
C.Z3_ast_vector_inc_ref(o.ctx.ptr, vec)
defer C.Z3_ast_vector_dec_ref(o.ctx.ptr, vec)
size := uint(C.Z3_ast_vector_size(o.ctx.ptr, vec))
if size != 3 {
result := astVectorToExprs(o.ctx, vec)
if len(result) != 3 {
return nil
}
return []*Expr{
newExpr(o.ctx, C.Z3_ast_vector_get(o.ctx.ptr, vec, 0)),
newExpr(o.ctx, C.Z3_ast_vector_get(o.ctx.ptr, vec, 1)),
newExpr(o.ctx, C.Z3_ast_vector_get(o.ctx.ptr, vec, 2)),
}
return result
}
// GetUpperAsVector retrieves an upper bound as a vector (inf, value, eps).
@ -148,19 +140,11 @@ func (o *Optimize) GetLowerAsVector(index uint) []*Expr {
// otherwise it's represented as value + eps * EPSILON.
func (o *Optimize) GetUpperAsVector(index uint) []*Expr {
vec := C.Z3_optimize_get_upper_as_vector(o.ctx.ptr, o.ptr, C.uint(index))
// Increment reference count for the vector since we're using it
C.Z3_ast_vector_inc_ref(o.ctx.ptr, vec)
defer C.Z3_ast_vector_dec_ref(o.ctx.ptr, vec)
size := uint(C.Z3_ast_vector_size(o.ctx.ptr, vec))
if size != 3 {
result := astVectorToExprs(o.ctx, vec)
if len(result) != 3 {
return nil
}
return []*Expr{
newExpr(o.ctx, C.Z3_ast_vector_get(o.ctx.ptr, vec, 0)),
newExpr(o.ctx, C.Z3_ast_vector_get(o.ctx.ptr, vec, 1)),
newExpr(o.ctx, C.Z3_ast_vector_get(o.ctx.ptr, vec, 2)),
}
return result
}
// ReasonUnknown returns the reason why the result is unknown.