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

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

    • (ite (< b 0) (- (add_via_add1 (- a) (- b))) ; if (b < 0) return -add_via_add(-a,-b)

      пофиксил комментарий
      Ответить
    • Еее, наконец-то какашки на лиспе! Кок-ко!
      Ответить
      • Это не лисп, это особый язык для SMT решателей http://smtlib.cs.uiowa.edu/language.shtml
        Ответить
    • >Coq
      Милости прошу к нашему шалашу!
      Ответить
      • «Coq» вроде в INRIA разрабатывали, а петух — символ Франции (а также Валлонии — франкоязычной части Бельгии). Так что ничего удивительного.
        Ответить
      • Cock
        Ответить
    • В ПХП нет никаких солверов
      Ответить
    • Я вам свежа40k принес
      https://pbs.twimg.com/media/EEZzhZtU0AAH1OF.jpg:large
      Ответить
      • Блядь, всё-таки насрал, ой мудель, блядь!.. Твою мать, убери это говно нахуй отсюда, блядь! Сейчас будешь всё это вылизывать, блядь!
        Ответить

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