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

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