Juliano Cardoso / circusRefine

Blame view

circus/smt-solvers/veriT/linux/PO/switch1Operation3.smt 3.2 KB
edit raw normal view history
8d0dc533f   Madiel de Souza Conserva Filho   first 
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
 
  (benchmark autogen
    :logic QF_UF
    :extrasorts (ELEMENT)
    :extrafuns ((normal ELEMENT)
                (reverse ELEMENT)
                (void ELEMENT)
                (actual_pos ELEMENT))
    :extrapreds ((POSITION ELEMENT))
    :extramacros ((in (lambda (?x ELEMENT) (?p (ELEMENT boolean)) . (?p ?x)))
                  (emptyset (lambda (?v ELEMENT) . false))
                  (omega (lambda (?x ELEMENT) . true))
                  (singleton (lambda (?x ELEMENT) . (lambda (?y ELEMENT) . (= ?x ?y))))
                  (intersection (lambda (?p (ELEMENT boolean)) (?q (ELEMENT boolean)) .
                                        (lambda (?x ELEMENT) . (and (?p ?x) (?q ?x)))))
                  (union (lambda (?p (ELEMENT boolean)) (?q (ELEMENT boolean)) .
                                 (lambda (?x ELEMENT) . (or (?p ?x) (?q ?x)))))
                  (difference (lambda (?p (ELEMENT boolean)) (?q (ELEMENT boolean)) .
                                      (lambda (?x ELEMENT) .
                                              (and (?p ?x) (not (?q ?x))))))
                  (symmetric_difference
                   (lambda (?p (ELEMENT boolean)) (?q (ELEMENT boolean)) .
                           (lambda (?x ELEMENT) .
                                   (or (and (?p ?x) (not (?q ?x)))
                                       (and (?q ?x) (not (?p ?x)))))))
                  (subset (lambda (?p (ELEMENT boolean)) (?q (ELEMENT boolean)) .
                                  (forall (?x ELEMENT) . (implies (?p ?x) (?q ?x)))))
                  (set3 (lambda (?e1 ELEMENT) (?e2 ELEMENT) (?e3 ELEMENT) .
                        (lambda (?y ELEMENT) . (or (= ?y ?e1) (= ?y ?e2) (= ?y ?e3)))))
                  (set5 (lambda (?e1 ELEMENT) (?e2 ELEMENT) (?e3 ELEMENT) (?e4 ELEMENT) (?e5 ELEMENT) .
                        (lambda (?y ELEMENT) . (or (= ?y ?e1) (= ?y ?e2) (= ?y ?e3) (= ?y ?e4) (= ?y ?e5)))))
                  )
    :formula
  (and
    (and
      (in normal POSITION)
      (in reverse POSITION)
      (in void POSITION)
      (and (not (= void reverse)) (not (= void normal)) (not (= reverse normal)))
      (forall (?e4 ELEMENT) (implies (in ?e4 POSITION) (or (= ?e4 normal) (= ?e4 reverse) (= ?e4 void)))))
    (and (not (= reverse normal)) (not (= void normal)) (not (= void reverse)))
    (in actual_pos POSITION)
    (not
      (implies
        (and
          (and
            (in normal POSITION)
            (in reverse POSITION)
            (in void POSITION)
            (and (not (= void reverse)) (not (= void normal)) (not (= reverse normal)))
            (forall (?e4 ELEMENT) (implies (in ?e4 POSITION) (or (= ?e4 normal) (= ?e4 reverse) (= ?e4 void)))))
          (and (not (= reverse normal)) (not (= void normal)) (not (= void reverse)))
          (in actual_pos POSITION))
        (forall (?m1 ELEMENT) (?m2 ELEMENT) (?m3 ELEMENT) (implies
  true
  (and
    (implies (and (in normal (set3 ?m1 ?m2 ?m3)) (not (in reverse (set3 ?m1 ?m2 ?m3)))) (in actual_pos POSITION))
    (implies (and (in reverse (set3 ?m1 ?m2 ?m3)) (not (in normal (set3 ?m1 ?m2 ?m3)))) (in actual_pos POSITION))
    (implies
      (not
        (or
          (and (in normal (set3 ?m1 ?m2 ?m3)) (not (in reverse (set3 ?m1 ?m2 ?m3))))
          (and (in reverse (set3 ?m1 ?m2 ?m3)) (not (in normal (set3 ?m1 ?m2 ?m3))))))
      (in actual_pos POSITION))))))))
  
    :status unknown
  )