Juliano Cardoso / circusRefine

set-1.smt 1.38 KB
edit raw blame history 
  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
(benchmark set_1
  :logic UNKNOWN
  :status unsat
  :extrasorts (ELEMENT)
  :extrafuns ((x ELEMENT) (y ELEMENT) (f ELEMENT ELEMENT))
  :extrapreds ((B ELEMENT) (C ELEMENT) (D 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))))))
  :formula
  (not (in x (singleton x)))
)