-
Notifications
You must be signed in to change notification settings - Fork 0
/
int.go
91 lines (76 loc) · 2.29 KB
/
int.go
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
// Copyright 2017 The Go Authors. All rights reserved.
// Use of this source code is governed by a BSD-style
// license that can be found in the LICENSE file.
package z3
/*
#cgo LDFLAGS: -lz3
#include <z3.h>
#include <stdlib.h>
*/
import "C"
import "math/big"
// Int is a symbolic value representing an integer with infinite precision.
//
// Int implements Value.
type Int value
func init() {
kindWrappers[KindInt] = func(x value) Value {
return Int(x)
}
}
// IntSort returns the integer sort.
func (ctx *Context) IntSort() Sort {
var sort Sort
ctx.do(func() {
sort = wrapSort(ctx, C.Z3_mk_int_sort(ctx.c), KindInt)
})
return sort
}
// IntConst returns a int constant named "name".
func (ctx *Context) IntConst(name string) Int {
return ctx.Const(name, ctx.IntSort()).(Int)
}
// AsInt64 returns the value of lit as an int64. If lit is not a
// literal, it returns 0, false, false. If lit is a literal, but its
// value cannot be represented as an int64, it returns 0, true, false.
func (lit Int) AsInt64() (val int64, isLiteral, ok bool) {
return lit.asInt64()
}
// AsUint64 is like AsInt64, but returns a uint64 and fails if lit
// cannot be represented as a uint64.
func (lit Int) AsUint64() (val uint64, isLiteral, ok bool) {
return lit.asUint64()
}
// AsBigInt returns the value of lit as a math/big.Int. If lit is not
// a literal, it returns nil, false.
func (lit Int) AsBigInt() (val *big.Int, isConst bool) {
return lit.asBigInt()
}
//go:generate go run genwrap.go -t Int $GOFILE intreal.go
// Div returns the floor of l / r.
//
// If r is 0, the result is unconstrained.
//
// Note that this differs from Go division: Go rounds toward zero
// (truncated division), whereas this rounds toward -inf.
//
//wrap:expr Div Z3_mk_div l r
// Mod returns modulus of l / r.
//
// The sign of the result follows the sign of r.
//
//wrap:expr Mod Z3_mk_mod l r
// Rem returns remainder of l / r.
//
// The sign of the result follows the sign of l.
//
// Note that this differs subtly from Go's remainder operator because
// this is based floored division rather than truncated division.
//
//wrap:expr Rem Z3_mk_rem l r
// ToReal converts l to sort Real.
//
//wrap:expr ToReal:Real Z3_mk_int2real l
// ToBV converts l to a bit-vector of width bits.
//
//wrap:expr ToBV:BV l bits:int : Z3_mk_int2bv bits:unsigned l