blob: 9a0a2d63c168853f0e2768b5def349e47b3a48d4 (
plain)
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
|
(declare Int sort)
(define arithpred_Int (! x (term Int)
(! y (term Int)
formula)))
(declare >_Int arithpred_Int)
(declare >=_Int arithpred_Int)
(declare <_Int arithpred_Int)
(declare <=_Int arithpred_Int)
(define arithterm_Int (! x (term Int)
(! y (term Int)
(term Int))))
(declare +_Int arithterm_Int)
(declare -_Int arithterm_Int)
(declare *_Int arithterm_Int) ; is * ok to use?
(declare /_Int arithterm_Int) ; is / ok to use?
; a constant term
(declare a_int (! x mpz (term Int)))
; unary negation
(declare u-_Int (! t (term Int) (term Int)))
|
