Blame view
circus/smt-solvers/generatedFile.smt
2.51 KB
8d0dc533f
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 |
;;Proof Obligations of Module in Harvey/SMT Language
(benchmark filePO0
:logic UNKNOWN
:extrasorts (Int boolean)
:extrafuns ((MININT Int)
(MAXINT Int)
(mod Int Int Int))
:extrafuns ( (second Int )
(second' Int ))
:extrapreds ((INTEGER Int)
(NATURAL Int)
(FINSET Int)
(NATURAL_1 Int))
:extramacros ((in (lambda (?x Int) (?p (Int boolean)) . (?p ?x)))
(emptyset (lambda (?v Int) . false))
(omega (lambda (?x Int) . true))
(singleton (lambda (?x Int) . (lambda (?y Int) . (= ?x ?y))))
(intersection (lambda (?p (Int boolean)) (?q (Int boolean)) .
(lambda (?x Int) . (and (?p ?x) (?q ?x)))))
(union (lambda (?p (Int boolean)) (?q (Int boolean)) .
(lambda (?x Int) . (or (?p ?x) (?q ?x)))))
(difference (lambda (?p (Int boolean)) (?q (Int boolean)) .
(lambda (?x Int) .
(and (?p ?x) (not (?q ?x))))))
(symmetric_difference
(lambda (?p (Int boolean)) (?q (Int boolean)) .
(lambda (?x Int) .
(or (and (?p ?x) (not (?q ?x)))
(and (?q ?x) (not (?p ?x)))))))
(subset (lambda (?p (Int boolean)) (?q (Int boolean)) .
(forall (?x Int) . (implies (?p ?x) (?q ?x)))))
(range (lambda (?n Int) (?m Int) .
(lambda (?x Int) . (and (<= ?x ?m) (<= ?n ?x))))
)
(succ (lambda (?n Int). (+ ?n 1)))
(pred (lambda (?n Int). (- ?n 1)))
)
:assumption (= MININT (~ 2147483647) )
:assumption (= MAXINT 2147483647)
:assumption (forall (?i Int) (iff (in ?i INTEGER) (and (<= MININT ?i) (<= ?i MAXINT))))
:assumption (forall (?i Int) (iff (in ?i NATURAL) (and (<= 0 ?i) (<= ?i MAXINT))))
:assumption (forall (?i Int) (iff (in ?i NATURAL_1) (and (< 0 ?i) (<= ?i MAXINT))))
:assumption (forall (?x Int) (?y Int) (implies (and (>= ?x 0) (> ?y 0)) (and (<= (mod ?x ?y) 0) (< (mod ?x ?y) ?y))))
;;UNKOWN-PO
:formula (not
(iff (and (and (and (and (in second (range 0 59)) true) true) (and (and (and (in second' (range 0 59)) true) true) true)) true) (and (in second (range 0 59)) (in second' (range 0 59))))
)
)
|