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
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
|
from typing import overload, Tuple, Any, List, Iterable, Union, TypeVar
from .z3types import Ast, ContextObj
TExprRef = TypeVar("TExprRef", bound="ExprRef")
class Context:
...
class Z3PPObject:
...
class AstRef(Z3PPObject):
@overload
def __init__(self, ast: Ast, ctx: Context) -> None:
self.ast: Ast = ...
self.ctx: Context= ...
@overload
def __init__(self, ast: Ast) -> None:
self.ast: Ast = ...
self.ctx: Context= ...
def ctx_ref(self) -> ContextObj: ...
def as_ast(self) -> Ast: ...
def children(self) -> List[AstRef]: ...
class SortRef(AstRef):
...
class FuncDeclRef(AstRef):
def arity(self) -> int: ...
def name(self) -> str: ...
class ExprRef(AstRef):
def eq(self, other: ExprRef) -> ExprRef: ...
def sort(self) -> SortRef: ...
def decl(self) -> FuncDeclRef: ...
class BoolSortRef(SortRef):
...
class BoolRef(ExprRef):
...
def is_true(a: BoolRef) -> bool: ...
def is_false(a: BoolRef) -> bool: ...
def is_int_value(a: AstRef) -> bool: ...
def substitute(a: AstRef, *m: Tuple[AstRef, AstRef]) -> AstRef: ...
class ArithSortRef(SortRef):
...
class ArithRef(ExprRef):
def __neg__(self) -> ExprRef: ...
def __le__(self, other: ArithRef) -> ArithRef: ...
def __lt__(self, other: ArithRef) -> ArithRef: ...
def __ge__(self, other: ArithRef) -> ArithRef: ...
def __gt__(self, other: ArithRef) -> ArithRef: ...
def __add__(self, other: ArithRef) -> ArithRef: ...
def __sub__(self, other: ArithRef) -> ArithRef: ...
def __mul__(self, other: ArithRef) -> ArithRef: ...
def __div__(self, other: ArithRef) -> ArithRef: ...
def __mod__(self, other: ArithRef) -> ArithRef: ...
class IntNumRef(ArithRef):
def as_long(self) -> int: ...
class BitVecRef(ExprRef):
def __neg__(self) -> ExprRef: ...
def __le__(self, other: BitVecRef) -> ExprRef: ...
def __lt__(self, other: BitVecRef) -> ExprRef: ...
def __ge__(self, other: BitVecRef) -> ExprRef: ...
def __gt__(self, other: BitVecRef) -> ExprRef: ...
def __add__(self, other: BitVecRef) -> BitVecRef: ...
def __sub__(self, other: BitVecRef) -> BitVecRef: ...
def __mul__(self, other: BitVecRef) -> BitVecRef: ...
def __div__(self, other: BitVecRef) -> BitVecRef: ...
def __mod__(self, other: BitVecRef) -> BitVecRef: ...
class BitVecNumRef(BitVecRef):
def as_long(self) -> int: ...
class CheckSatResult: ...
class ModelRef(Z3PPObject):
def __getitem__(self, k: FuncDeclRef) -> IntNumRef: ...
def decls(self) -> Iterable[FuncDeclRef]: ...
class Solver(Z3PPObject):
@overload
def __init__(self) -> None:
self.ctx: Context = ...
@overload
def __init__(self, ctx:Context) -> None:
self.ctx: Context = ...
def add(self, e:ExprRef) -> None: ...
def to_smt2(self) -> str: ...
def check(self) -> CheckSatResult: ...
def push(self) -> None: ...
def pop(self) -> None: ...
def model(self) -> ModelRef: ...
sat: CheckSatResult = ...
unsat: CheckSatResult = ...
@overload
def Int(name: str) -> ArithRef: ...
@overload
def Int(name: str, ctx: Context) -> ArithRef: ...
@overload
def Bool(name: str) -> BoolRef: ...
@overload
def Bool(name: str, ctx: Context) -> BoolRef: ...
def BitVec(name: str, width: int) -> BitVecRef: ...
@overload
def parse_smt2_string(s: str) -> ExprRef: ...
@overload
def parse_smt2_string(s: str, ctx: Context) -> ExprRef: ...
# Can't give more precise types here since func signature is
# a vararg list of ExprRef optionally followed by a Context
def Or(*args: Union[ExprRef, Context]) -> ExprRef: ...
def And(*args: Union[ExprRef, Context]) -> ExprRef: ...
@overload
def Not(p: ExprRef) -> ExprRef: ...
@overload
def Not(p: ExprRef, ctx: Context) -> ExprRef: ...
def Implies(a: ExprRef, b: ExprRef, ctx:Context) -> ExprRef: ...
def If(a: ExprRef, b:TExprRef, c:TExprRef) -> TExprRef: ...
def ZeroExt(width: int, expr: BitVecRef) -> BitVecRef: ...
def SignExt(width: int, expr: BitVecRef) -> BitVecRef: ...
def Extract(hi: int, lo: int, expr: BitVecRef) -> BitVecRef: ...
def Concat(expr1: BitVecRef, expr2: BitVecRef) -> BitVecRef: ...
def Function(name: str, *sig: Tuple[SortRef,...]) -> FuncDeclRef: ...
def IntVal(val: int, ctx: Context) -> IntNumRef: ...
@overload
def BoolVal(val: bool, ctx: Context) -> BoolRef: ...
@overload
def BoolVal(val: bool) -> BoolRef: ...
@overload
def BitVecVal(val: int, bits: int, ctx: Context) -> BitVecNumRef: ...
@overload
def BitVecVal(val: int, bits: int) -> BitVecNumRef: ...
|
