cvc4

8Ciepło

2Odpowiedz

Jakie są ograniczenia rozumowania w ilościowej arytmetyki w SMT?

Próbowałem kilka rozwiązują SMT (CVC3, CVC4 i Z3) na poniższym pozornie trywialny odniesienia: (set-logic LIA) (set-info :smt-lib-version 2.0) (assert (forall ((x Int)) (forall ((y Int)) (= y x))))