mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-03 17:05:15 +00:00
Code Activity

Fix trailing whitespace in Go source files

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-02-16 06:06:48 +00:00 • committed by Nikolaj Bjorner
parent c61ee6b16c
commit dd09b89557
2 changed files with 7 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/api/go/fixedpoint.go
View file

@ -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) C.Z3_fixedpoint_add_fact(f.ctx.ptr, f.ptr, pred.ptr, 0, nil)
return return
} }
cArgs := make([]C.uint, len(args)) cArgs := make([]C.uint, len(args))
for i, arg := range args { for i, arg := range args {
cArgs[i] = C.uint(arg) cArgs[i] = C.uint(arg)
@ -109,12 +109,12 @@ func (f *Fixedpoint) QueryRelations(relations []*FuncDecl) Status {
if len(relations) == 0 { if len(relations) == 0 {
return Unknown return Unknown
} }
cRelations := make([]C.Z3_func_decl, len(relations)) cRelations := make([]C.Z3_func_decl, len(relations))
for i, rel := range relations { for i, rel := range relations {
cRelations[i] = rel.ptr cRelations[i] = rel.ptr
} }
result := C.Z3_fixedpoint_query_relations(f.ctx.ptr, f.ptr, C.uint(len(relations)), &cRelations[0]) result := C.Z3_fixedpoint_query_relations(f.ctx.ptr, f.ptr, C.uint(len(relations)), &cRelations[0])
switch result { switch result {
case C.Z3_L_TRUE: case C.Z3_L_TRUE:
@ -253,12 +253,12 @@ func (s *Statistics) GetKey(idx int) string {
// IsUint returns true if the statistical data at the given index is unsigned integer // IsUint returns true if the statistical data at the given index is unsigned integer
func (s *Statistics) IsUint(idx int) bool { func (s *Statistics) IsUint(idx int) bool {
return bool(C.Z3_stats_is_uint(s.ctx.ptr, s.ptr, C.uint(idx))) 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 // IsDouble returns true if the statistical data at the given index is double
func (s *Statistics) IsDouble(idx int) bool { func (s *Statistics) IsDouble(idx int) bool {
return bool(C.Z3_stats_is_double(s.ctx.ptr, s.ptr, C.uint(idx))) 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 // GetUintValue returns the unsigned integer value at the given index

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

@ -547,12 +547,12 @@ return newExpr(q.ctx, q.ptr)
// IsUniversal returns true if this is a universal quantifier (forall) // IsUniversal returns true if this is a universal quantifier (forall)
func (q *Quantifier) IsUniversal() bool { func (q *Quantifier) IsUniversal() bool {
return bool(C.Z3_is_quantifier_forall(q.ctx.ptr, q.ptr)) return bool(C.Z3_is_quantifier_forall(q.ctx.ptr, q.ptr))
} }
// IsExistential returns true if this is an existential quantifier (exists) // IsExistential returns true if this is an existential quantifier (exists)
func (q *Quantifier) IsExistential() bool { func (q *Quantifier) IsExistential() bool {
return bool(C.Z3_is_quantifier_exists(q.ctx.ptr, q.ptr)) return bool(C.Z3_is_quantifier_exists(q.ctx.ptr, q.ptr))
} }
// GetWeight returns the weight of the quantifier // GetWeight returns the weight of the quantifier