blob: 5496f3c0a12e3d7bd8abb92aec49fa5306cf4c25 (
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
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
|
; EXPECT: unsat
; COMMAND-LINE: --no-dump-synth
(set-logic LIA)
(synth-fun inv ((l Int)) Bool
(
(Start Bool ((and AtomicFormula AtomicFormula)
(or AtomicFormula AtomicFormula)))
(AtomicFormula Bool ((<= Sum Const) (= Sum Const)))
(Sum Int ((+ Term Term)))
(Term Int ((* Sign Var)))
(Sign Int (0 1 -1))
(Var Int (l))
(Const Int (-3 -2 -1 0 1 2 3))
)
)
(define-fun implies ((b1 Bool) (b2 Bool)) Bool (or (not b1) b2))
(define-fun and3 ((b1 Bool) (b2 Bool) (b3 Bool)) Bool (and (and b1 b2) b3))
(define-fun and4 ((b1 Bool) (b2 Bool) (b3 Bool) (b4 Bool)) Bool (and (and3 b1 b2 b3) b4))
(define-fun and5 ((b1 Bool) (b2 Bool) (b3 Bool) (b4 Bool) (b5 Bool)) Bool (and (and4 b1 b2 b3 b4) b5))
(define-fun and6 ((b1 Bool) (b2 Bool) (b3 Bool) (b4 Bool) (b5 Bool) (b6 Bool)) Bool (and (and5 b1 b2 b3 b4 b5) b6))
(define-fun or3 ((b1 Bool) (b2 Bool) (b3 Bool)) Bool (or (or b1 b2) b3))
(define-fun or4 ((b1 Bool) (b2 Bool) (b3 Bool) (b4 Bool)) Bool (or (or3 b1 b2 b3) b4))
(define-fun or5 ((b1 Bool) (b2 Bool) (b3 Bool) (b4 Bool) (b5 Bool)) Bool (or (or4 b1 b2 b3 b4) b5))
(declare-var x0 Int)
(declare-var x1 Int)
(declare-var x2 Int)
(declare-var x3 Int)
(declare-var x4 Int)
(declare-var l Int)
(declare-var x0p Int)
(declare-var x1p Int)
(declare-var x2p Int)
(declare-var x3p Int)
(declare-var x4p Int)
(constraint (implies (and6 (= l 0) (or (= x0p (+ x0 1)) (= x0p (- x0 1)))
(or (= x1p (+ x1 1)) (= x1p (- x1 1)))
(or (= x2p (+ x2 1)) (= x2p (- x2 1)))
(or (= x3p (+ x3 1)) (= x3p (- x3 1)))
(or (= x4p (+ x4 1)) (= x4p (- x4 1))))
(inv l)))
(constraint (implies (and (inv l) (not (= l 0))) false))
(check-synth)
|
