Куча говна / Говнокод #25841 Ссылка на оригинал

0

  1. 1
  2. 2
  3. 3
  4. 4
  5. 5
  6. 6
  7. 7
  8. 8
  9. 9
  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 j123123, (Updated )

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

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

Я, guest, находясь в здравом уме и твердой памяти, торжественно заявляю:

    А не использовать ли нам bbcode?

    ↑
    8
    ↓