1. Куча / Говнокод #25841

    0

    1. 01
    2. 02
    3. 03
    4. 04
    5. 05
    6. 06
    7. 07
    8. 08
    9. 09
    10. 10
    11. 11
    12. 12
    13. 13
    14. 14
    15. 15
    16. 16
    17. 17
    18. 18
    19. 19
    20. 20
    21. 21
    (set-logic LIA)
;(set-option :produce-proofs true)

(define-fun-rec add_via_add1 ((a Int) (b Int)) Int
  (ite (= b 0) a                                ; if (b == 0) return a 
    (ite (< b 0) (- (add_via_add1 (- a) (- b))) ; if (b < 0) return add_via_add(-a,-b)
      (+ (add_via_add1 a (- b 1)) 1)            ; return add_via_add(a, b-1) + 1;
    )
  )
)


(assert
  (not (forall ((a Int) (b Int))
    (= (add_via_add1 a b) (+ a b))
  ))
)

(check-sat)
(get-model)
(exit)

    Хуйня, которую SMT солверы Z3 и CVC4 доказать не могут. Надо переходить на Coq, Metamath, LEAN, Mizar или еще какую-то такую хуйню

    Запостил: j123123, 15 Сентября 2019

    Комментарии (11) RSS

    Добавить комментарий