diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index decf70477..498658f31 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -279,22 +279,22 @@ jobs: - name: releaseClang setupCmd1: '' setupCmd2: '' - buildCmd: 'CC=clang CXX=clang++ cmake -DCMAKE_BUILD_TYPE=Release -DZ3_BUILD_DOTNET_BINDINGS=True -DZ3_BUILD_JAVA_BINDINGS=True -DZ3_BUILD_PYTHON_BINDINGS=True -G "Ninja" ../' + buildCmd: 'CC=clang CXX=clang++ cmake -DCMAKE_BUILD_TYPE=Release -DZ3_BUILD_DOTNET_BINDINGS=True -DZ3_BUILD_JAVA_BINDINGS=True -DZ3_BUILD_PYTHON_BINDINGS=True -DZ3_BUILD_GO_BINDINGS=True -G "Ninja" ../' runTests: true - name: debugClang setupCmd1: 'julia -e "using Pkg; Pkg.add(PackageSpec(name=\"libcxxwrap_julia_jll\"))"' setupCmd2: 'JlCxxDir=$(julia -e "using libcxxwrap_julia_jll; print(dirname(libcxxwrap_julia_jll.libcxxwrap_julia_path))")' - buildCmd: 'CC=clang CXX=clang++ cmake -DJlCxx_DIR=$JlCxxDir/cmake/JlCxx -DZ3_BUILD_JULIA_BINDINGS=True -DZ3_BUILD_DOTNET_BINDINGS=True -DZ3_BUILD_JAVA_BINDINGS=True -DZ3_BUILD_PYTHON_BINDINGS=True -G "Ninja" ../' + buildCmd: 'CC=clang CXX=clang++ cmake -DJlCxx_DIR=$JlCxxDir/cmake/JlCxx -DZ3_BUILD_JULIA_BINDINGS=True -DZ3_BUILD_DOTNET_BINDINGS=True -DZ3_BUILD_JAVA_BINDINGS=True -DZ3_BUILD_PYTHON_BINDINGS=True -DZ3_BUILD_GO_BINDINGS=True -G "Ninja" ../' runTests: true - name: debugGcc setupCmd1: '' setupCmd2: '' - buildCmd: 'CC=gcc CXX=g++ cmake -DZ3_BUILD_DOTNET_BINDINGS=True -DZ3_BUILD_JAVA_BINDINGS=True -DZ3_BUILD_PYTHON_BINDINGS=True -G "Ninja" ../' + buildCmd: 'CC=gcc CXX=g++ cmake -DZ3_BUILD_DOTNET_BINDINGS=True -DZ3_BUILD_JAVA_BINDINGS=True -DZ3_BUILD_PYTHON_BINDINGS=True -DZ3_BUILD_GO_BINDINGS=True -G "Ninja" ../' runTests: true - name: releaseSTGcc setupCmd1: '' setupCmd2: '' - buildCmd: 'CC=gcc CXX=g++ cmake -DCMAKE_BUILD_TYPE=Release -DZ3_SINGLE_THREADED=ON -DZ3_BUILD_DOTNET_BINDINGS=True -DZ3_BUILD_JAVA_BINDINGS=True -DZ3_BUILD_PYTHON_BINDINGS=True -G "Ninja" ../' + buildCmd: 'CC=gcc CXX=g++ cmake -DCMAKE_BUILD_TYPE=Release -DZ3_SINGLE_THREADED=ON -DZ3_BUILD_DOTNET_BINDINGS=True -DZ3_BUILD_JAVA_BINDINGS=True -DZ3_BUILD_PYTHON_BINDINGS=True -DZ3_BUILD_GO_BINDINGS=True -G "Ninja" ../' runTests: false steps: - name: Checkout code @@ -308,6 +308,11 @@ jobs: - name: Install Ninja run: sudo apt-get update && sudo apt-get install -y ninja-build + - name: Setup Go + uses: actions/setup-go@v5 + with: + go-version: '1.20' + - name: Setup Julia (if needed) if: matrix.name == 'debugClang' uses: julia-actions/setup-julia@v2 @@ -352,6 +357,20 @@ jobs: examples/c_maxsat_example_build_dir/c_maxsat_example ../examples/maxsat/ex.smt cd .. + - name: Build Go bindings + if: matrix.runTests + run: | + cd build + ninja go-bindings + cd .. + + - name: Test Go bindings + if: matrix.runTests + run: | + cd build + ninja test-go-examples + cd .. + - name: Clone z3test if: matrix.runTests run: git clone https://github.com/z3prover/z3test z3test diff --git a/examples/go/basic_example.go b/examples/go/basic_example.go index 73bcf84df..8a6c82823 100644 --- a/examples/go/basic_example.go +++ b/examples/go/basic_example.go @@ -82,7 +82,6 @@ func main() { fmt.Println("\nExample 4: Checking unsatisfiability") solver.Reset() a := ctx.MkIntConst("a") - one := ctx.MkInt(1, ctx.MkIntSort()) // a > 0 ∧ a < 0 (unsatisfiable) solver.Assert(ctx.MkGt(a, zero)) diff --git a/src/api/go/CMakeLists.txt b/src/api/go/CMakeLists.txt index f21bb4e37..d817a3f31 100644 --- a/src/api/go/CMakeLists.txt +++ b/src/api/go/CMakeLists.txt @@ -4,7 +4,7 @@ # Go bindings use CGO and are typically built using the Go toolchain directly. # However, we can set up installation targets here. -if(BUILD_GO_BINDINGS) +if(Z3_BUILD_GO_BINDINGS) message(STATUS "Z3 Go bindings will be installed") # Install Go source files @@ -27,26 +27,30 @@ if(BUILD_GO_BINDINGS) message(STATUS "Found Go: ${GO_EXECUTABLE}") # Custom target to build Go bindings + set(CGO_LDFLAGS_VALUE "-L${CMAKE_BINARY_DIR} -lz3") add_custom_target(go-bindings COMMAND ${CMAKE_COMMAND} -E env CGO_CFLAGS=-I${CMAKE_SOURCE_DIR}/src/api - CGO_LDFLAGS=-L${CMAKE_BINARY_DIR} -lz3 + CGO_LDFLAGS=${CGO_LDFLAGS_VALUE} ${GO_EXECUTABLE} build -v WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR} COMMENT "Building Go bindings" DEPENDS libz3 + VERBATIM ) # Custom target to test Go examples add_custom_target(test-go-examples COMMAND ${CMAKE_COMMAND} -E env CGO_CFLAGS=-I${CMAKE_SOURCE_DIR}/src/api - CGO_LDFLAGS=-L${CMAKE_BINARY_DIR} -lz3 + CGO_LDFLAGS=${CGO_LDFLAGS_VALUE} LD_LIBRARY_PATH=${CMAKE_BINARY_DIR}:$ENV{LD_LIBRARY_PATH} - PATH=${CMAKE_BINARY_DIR}\;$ENV{PATH} - ${GO_EXECUTABLE} run ${CMAKE_SOURCE_DIR}/examples/go/basic_example.go + PATH=${CMAKE_BINARY_DIR}$$ENV{PATH} + ${GO_EXECUTABLE} run basic_example.go + WORKING_DIRECTORY ${CMAKE_SOURCE_DIR}/examples/go COMMENT "Running Go examples" DEPENDS libz3 + VERBATIM ) else() message(STATUS "Go not found - Go bindings can be built manually") diff --git a/src/api/go/datatype.go b/src/api/go/datatype.go index 2dd9d8555..f4ae8a4d4 100644 --- a/src/api/go/datatype.go +++ b/src/api/go/datatype.go @@ -19,9 +19,10 @@ type Constructor struct { // newConstructor creates a new Constructor and manages its reference count. func newConstructor(ctx *Context, ptr C.Z3_constructor) *Constructor { c := &Constructor{ctx: ctx, ptr: ptr} - C.Z3_constructor_inc_ref(ctx.ptr, ptr) + // Note: Z3_constructor doesn't use inc_ref/dec_ref pattern + // It uses Z3_del_constructor for cleanup runtime.SetFinalizer(c, func(cons *Constructor) { - C.Z3_constructor_dec_ref(cons.ctx.ptr, cons.ptr) + C.Z3_del_constructor(cons.ctx.ptr, cons.ptr) }) return c } @@ -90,9 +91,10 @@ type ConstructorList struct { // newConstructorList creates a new ConstructorList and manages its reference count. func newConstructorList(ctx *Context, ptr C.Z3_constructor_list) *ConstructorList { cl := &ConstructorList{ctx: ctx, ptr: ptr} - C.Z3_constructor_list_inc_ref(ctx.ptr, ptr) + // Note: Z3_constructor_list doesn't use inc_ref/dec_ref pattern + // It uses Z3_del_constructor_list for cleanup runtime.SetFinalizer(cl, func(list *ConstructorList) { - C.Z3_constructor_list_dec_ref(list.ctx.ptr, list.ptr) + C.Z3_del_constructor_list(list.ctx.ptr, list.ptr) }) return cl } @@ -152,7 +154,7 @@ func (c *Context) MkDatatypeSorts(names []string, constructorLists [][]*Construc // Clean up constructor lists for i := range cLists { - C.Z3_constructor_list_dec_ref(c.ptr, cLists[i]) + C.Z3_del_constructor_list(c.ptr, cLists[i]) } sorts := make([]*Sort, numTypes) diff --git a/src/api/go/fixedpoint.go b/src/api/go/fixedpoint.go index c22926467..ab28569fc 100644 --- a/src/api/go/fixedpoint.go +++ b/src/api/go/fixedpoint.go @@ -70,7 +70,7 @@ func (f *Fixedpoint) AddRule(rule *Expr, name *Symbol) { if name != nil { namePtr = name.ptr } else { - namePtr = 0 + namePtr = nil } C.Z3_fixedpoint_add_rule(f.ctx.ptr, f.ptr, rule.ptr, namePtr) } @@ -81,7 +81,7 @@ func (f *Fixedpoint) AddFact(pred *FuncDecl, args []int) { C.Z3_fixedpoint_add_fact(f.ctx.ptr, f.ptr, pred.ptr, 0, nil) return } - + cArgs := make([]C.uint, len(args)) for i, arg := range args { cArgs[i] = C.uint(arg) @@ -109,12 +109,12 @@ func (f *Fixedpoint) QueryRelations(relations []*FuncDecl) Status { if len(relations) == 0 { return Unknown } - + cRelations := make([]C.Z3_func_decl, len(relations)) for i, rel := range relations { cRelations[i] = rel.ptr } - + result := C.Z3_fixedpoint_query_relations(f.ctx.ptr, f.ptr, C.uint(len(relations)), &cRelations[0]) switch result { case C.Z3_L_TRUE: @@ -132,7 +132,7 @@ func (f *Fixedpoint) UpdateRule(rule *Expr, name *Symbol) { if name != nil { namePtr = name.ptr } else { - namePtr = 0 + namePtr = nil } C.Z3_fixedpoint_update_rule(f.ctx.ptr, f.ptr, rule.ptr, namePtr) } @@ -195,16 +195,6 @@ func (f *Fixedpoint) GetAssertions() *ASTVector { return newASTVector(f.ctx, ptr) } -// Push creates a backtracking point -func (f *Fixedpoint) Push() { - C.Z3_fixedpoint_push(f.ctx.ptr, f.ptr) -} - -// Pop backtracks one backtracking point -func (f *Fixedpoint) Pop() { - C.Z3_fixedpoint_pop(f.ctx.ptr, f.ptr) -} - // SetPredicateRepresentation sets the predicate representation for a given relation func (f *Fixedpoint) SetPredicateRepresentation(funcDecl *FuncDecl, kinds []C.Z3_symbol) { if len(kinds) == 0 { @@ -263,12 +253,12 @@ func (s *Statistics) GetKey(idx int) string { // IsUint returns true if the statistical data at the given index is unsigned integer func (s *Statistics) IsUint(idx int) bool { - return C.Z3_stats_is_uint(s.ctx.ptr, s.ptr, C.uint(idx)) != 0 + return bool(C.Z3_stats_is_uint(s.ctx.ptr, s.ptr, C.uint(idx))) } // IsDouble returns true if the statistical data at the given index is double func (s *Statistics) IsDouble(idx int) bool { - return C.Z3_stats_is_double(s.ctx.ptr, s.ptr, C.uint(idx)) != 0 + return bool(C.Z3_stats_is_double(s.ctx.ptr, s.ptr, C.uint(idx))) } // GetUintValue returns the unsigned integer value at the given index diff --git a/src/api/go/log.go b/src/api/go/log.go index dc43419ae..bd6e3f1b7 100644 --- a/src/api/go/log.go +++ b/src/api/go/log.go @@ -28,7 +28,7 @@ func OpenLog(filename string) bool { defer C.free(unsafe.Pointer(cFilename)) result := C.Z3_open_log(cFilename) - if result != 0 { + if bool(result) { isLogOpen = true return true } diff --git a/src/api/go/solver.go b/src/api/go/solver.go index 3dec5cc70..6988d83c1 100644 --- a/src/api/go/solver.go +++ b/src/api/go/solver.go @@ -7,7 +7,6 @@ package z3 import "C" import ( "runtime" - "unsafe" ) // Status represents the result of a satisfiability check. diff --git a/src/api/go/z3.go b/src/api/go/z3.go index 810308047..3e11dadf6 100644 --- a/src/api/go/z3.go +++ b/src/api/go/z3.go @@ -119,6 +119,11 @@ ctx *Context ptr C.Z3_symbol } +// newSymbol creates a new Symbol. +func newSymbol(ctx *Context, ptr C.Z3_symbol) *Symbol { + return &Symbol{ctx: ctx, ptr: ptr} +} + // MkIntSymbol creates an integer symbol. func (c *Context) MkIntSymbol(i int) *Symbol { return &Symbol{ @@ -253,6 +258,55 @@ func (e *Expr) GetSort() *Sort { return newSort(e.ctx, C.Z3_get_sort(e.ctx.ptr, e.ptr)) } +// Pattern represents a Z3 pattern for quantifier instantiation. +type Pattern struct { + ctx *Context + ptr C.Z3_pattern +} + +// newPattern creates a new Pattern and manages its reference count. +func newPattern(ctx *Context, ptr C.Z3_pattern) *Pattern { + p := &Pattern{ctx: ctx, ptr: ptr} + // Patterns are ASTs in the C API + C.Z3_inc_ref(ctx.ptr, (C.Z3_ast)(unsafe.Pointer(ptr))) + runtime.SetFinalizer(p, func(pat *Pattern) { + C.Z3_dec_ref(pat.ctx.ptr, (C.Z3_ast)(unsafe.Pointer(pat.ptr))) + }) + return p +} + +// ASTVector represents a vector of Z3 ASTs. +type ASTVector struct { + ctx *Context + ptr C.Z3_ast_vector +} + +// newASTVector creates a new ASTVector and manages its reference count. +func newASTVector(ctx *Context, ptr C.Z3_ast_vector) *ASTVector { + v := &ASTVector{ctx: ctx, ptr: ptr} + C.Z3_ast_vector_inc_ref(ctx.ptr, ptr) + runtime.SetFinalizer(v, func(vec *ASTVector) { + C.Z3_ast_vector_dec_ref(vec.ctx.ptr, vec.ptr) + }) + return v +} + +// ParamDescrs represents parameter descriptions for Z3 objects. +type ParamDescrs struct { + ctx *Context + ptr C.Z3_param_descrs +} + +// newParamDescrs creates a new ParamDescrs and manages its reference count. +func newParamDescrs(ctx *Context, ptr C.Z3_param_descrs) *ParamDescrs { + pd := &ParamDescrs{ctx: ctx, ptr: ptr} + C.Z3_param_descrs_inc_ref(ctx.ptr, ptr) + runtime.SetFinalizer(pd, func(descrs *ParamDescrs) { + C.Z3_param_descrs_dec_ref(descrs.ctx.ptr, descrs.ptr) + }) + return pd +} + // MkTrue creates the Boolean constant true. func (c *Context) MkTrue() *Expr { return newExpr(c, C.Z3_mk_true(c.ptr)) @@ -341,36 +395,6 @@ func (c *Context) MkXor(lhs, rhs *Expr) *Expr { return newExpr(c, C.Z3_mk_xor(c.ptr, lhs.ptr, rhs.ptr)) } -if len(exprs) == 1 { -return exprs[0] -} -cExprs := make([]C.Z3_ast, len(exprs)) -for i, e := range exprs { -cExprs[i] = e.ptr -} -return newExpr(c, C.Z3_mk_add(c.ptr, C.uint(len(exprs)), &cExprs[0])) -} - -if len(exprs) == 1 { -return newExpr(c, C.Z3_mk_unary_minus(c.ptr, exprs[0].ptr)) -} -cExprs := make([]C.Z3_ast, len(exprs)) -for i, e := range exprs { -cExprs[i] = e.ptr -} -return newExpr(c, C.Z3_mk_sub(c.ptr, C.uint(len(exprs)), &cExprs[0])) -} - -if len(exprs) == 1 { -return exprs[0] -} -cExprs := make([]C.Z3_ast, len(exprs)) -for i, e := range exprs { -cExprs[i] = e.ptr -} -return newExpr(c, C.Z3_mk_mul(c.ptr, C.uint(len(exprs)), &cExprs[0])) -} - // Comparison operations // MkEq creates an equality. @@ -464,28 +488,30 @@ return newExpr(c, C.Z3_mk_app(c.ptr, decl.ptr, C.uint(len(args)), argsPtr)) // MkForall creates a universal quantifier. func (c *Context) MkForall(bound []*Expr, body *Expr) *Expr { -cBound := make([]C.Z3_ast, len(bound)) -for i, b := range bound { -cBound[i] = b.ptr -} -var boundPtr *C.Z3_ast -if len(bound) > 0 { -boundPtr = &cBound[0] -} -return newExpr(c, C.Z3_mk_forall_const(c.ptr, 0, C.uint(len(bound)), boundPtr, 0, nil, body.ptr)) + cBound := make([]C.Z3_app, len(bound)) + for i, b := range bound { + // Z3_app is a subtype of Z3_ast; constants are apps + cBound[i] = (C.Z3_app)(unsafe.Pointer(b.ptr)) + } + var boundPtr *C.Z3_app + if len(bound) > 0 { + boundPtr = &cBound[0] + } + return newExpr(c, C.Z3_mk_forall_const(c.ptr, 0, C.uint(len(bound)), boundPtr, 0, nil, body.ptr)) } // MkExists creates an existential quantifier. func (c *Context) MkExists(bound []*Expr, body *Expr) *Expr { -cBound := make([]C.Z3_ast, len(bound)) -for i, b := range bound { -cBound[i] = b.ptr -} -var boundPtr *C.Z3_ast -if len(bound) > 0 { -boundPtr = &cBound[0] -} -return newExpr(c, C.Z3_mk_exists_const(c.ptr, 0, C.uint(len(bound)), boundPtr, 0, nil, body.ptr)) + cBound := make([]C.Z3_app, len(bound)) + for i, b := range bound { + // Z3_app is a subtype of Z3_ast; constants are apps + cBound[i] = (C.Z3_app)(unsafe.Pointer(b.ptr)) + } + var boundPtr *C.Z3_app + if len(bound) > 0 { + boundPtr = &cBound[0] + } + return newExpr(c, C.Z3_mk_exists_const(c.ptr, 0, C.uint(len(bound)), boundPtr, 0, nil, body.ptr)) } // Simplify simplifies an expression. @@ -521,12 +547,12 @@ return newExpr(q.ctx, q.ptr) // IsUniversal returns true if this is a universal quantifier (forall) func (q *Quantifier) IsUniversal() bool { -return C.Z3_is_quantifier_forall(q.ctx.ptr, q.ptr) != 0 +return bool(C.Z3_is_quantifier_forall(q.ctx.ptr, q.ptr)) } // IsExistential returns true if this is an existential quantifier (exists) func (q *Quantifier) IsExistential() bool { -return C.Z3_is_quantifier_exists(q.ctx.ptr, q.ptr) != 0 +return bool(C.Z3_is_quantifier_exists(q.ctx.ptr, q.ptr)) } // GetWeight returns the weight of the quantifier @@ -553,7 +579,7 @@ return int(C.Z3_get_quantifier_num_no_patterns(q.ctx.ptr, q.ptr)) // GetNoPattern returns the no-pattern at the given index func (q *Quantifier) GetNoPattern(idx int) *Pattern { ptr := C.Z3_get_quantifier_no_pattern_ast(q.ctx.ptr, q.ptr, C.uint(idx)) -return newPattern(q.ctx, ptr) +return newPattern(q.ctx, (C.Z3_pattern)(unsafe.Pointer(ptr))) } // GetNumBound returns the number of bound variables @@ -586,11 +612,11 @@ return q.AsExpr().String() // MkQuantifier creates a quantifier with patterns func (c *Context) MkQuantifier(isForall bool, weight int, sorts []*Sort, names []*Symbol, body *Expr, patterns []*Pattern) *Quantifier { -var forallInt C.int +var forallInt C.bool if isForall { -forallInt = 1 +forallInt = true } else { -forallInt = 0 +forallInt = false } numBound := len(sorts) @@ -634,11 +660,11 @@ return newQuantifier(c, ptr) // MkQuantifierConst creates a quantifier using constant bound variables func (c *Context) MkQuantifierConst(isForall bool, weight int, bound []*Expr, body *Expr, patterns []*Pattern) *Quantifier { -var forallInt C.int +var forallInt C.bool if isForall { -forallInt = 1 +forallInt = true } else { -forallInt = 0 +forallInt = false } numBound := len(bound) @@ -647,7 +673,7 @@ var boundPtr *C.Z3_app if numBound > 0 { cBound = make([]C.Z3_app, numBound) for i := 0; i < numBound; i++ { -cBound[i] = C.Z3_app(bound[i].ptr) +cBound[i] = (C.Z3_app)(unsafe.Pointer(bound[i].ptr)) } boundPtr = &cBound[0] } @@ -753,7 +779,7 @@ var boundPtr *C.Z3_app if numBound > 0 { cBound = make([]C.Z3_app, numBound) for i := 0; i < numBound; i++ { -cBound[i] = C.Z3_app(bound[i].ptr) +cBound[i] = (C.Z3_app)(unsafe.Pointer(bound[i].ptr)) } boundPtr = &cBound[0] }