blob: edfc2176becba26bb4c4a9082106a8ec9bc1518f (
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
|
; EXPECT: unsat
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic LIA)
(synth-fun inv ((x Int)) Bool
((Start Bool) (AtomicFormula Bool) (Sum Int) (Term Int) (Sign Int) (Var Int) (Const Int))
(
(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 (x))
(Const Int ((+ Const Const) (- Const Const) 0 1))
)
)
(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 s Int)
(declare-var x Int)
(constraint (implies (= x 0) (inv x)))
(constraint (implies (inv x) (= x 0)))
(constraint (implies (inv x) (inv x)))
(constraint (implies (and (inv x) false) (not (= x 0))))
(check-synth)
|
