5
A
Odpowiedz
6
Do tego celu można użyć eliminacji kwantyfikatora. Oto przykład:
(declare-const t1 Int)
(declare-const t2 Int)
(elim-quantifiers (exists ((x Int)) (and (< t1 x) (< x t2))))
Można spróbować tego przykładu w Internecie pod adresem: http://rise4fun.com/Z3/kp0X
1
Możliwe rozwiązanie używając Redlog redukuj:
Powiązane problemy
- 1. Czytaj func interp tablicy z3 z modelu z3
- 2. kwantyfikatorów w Z3
- 3. Biegunowość Z3 za pomocą Z3 jako SAT Solver
- 4. Obsługa kwantyfikatora Z3
- 5. z3 C++ API & ite
- 6. Wynik kontrprzykładu Z3
- 7. Jak uzyskać losowe wyniki z Microsoft Z3?
- 8. Różnica między Z3 i coq
- 9. Szukasz praktycznych przykładów zastosowań SMT Z3 (jak DbC) i alternatywy open source dla Z3?
- 10. Czy obsługa Z3 Interpolacja Craiga
- 11. Sprawdź przepełnienie za pomocą Z3
- 12. Z3: znajdowanie wszystkich satysfakcjonujących modeli
- 13. Jak ukryć nagłówek PivotItem?
- 14. Jak "ukryć" UIRefreshControl?
- 15. Jak ukryć część obrazu?
- 16. jak ukryć wyjście systemowe()
- 17. Jak ukryć granicę UITextField?
- 18. Jak ukryć schemat mikrodanych?
- 19. Jak ukryć obrazy apk?
- 20. Jak ukryć ikonę Docku
- 21. Jak ukryć podramkę UIView?
- 22. Jak ukryć metodę utylizacji?
- 23. typ danych zawiera zestaw w Z3
- 24. Czy Z3 może pracować w trybie przyrostowym?
- 25. Jak dekompilować zmienną zmienną w Javie?
- 26. drukowanie formuł wewnętrznych solver w z3
- 27. Równoważnik określenia-zabawy w Z3 API
- 28. Zrozumienie indeksowania powiązanych zmiennych w Z3
- 29. Ocenianie się „zmienną zmienną”
- 30. QF_FPA? Czy Z3 obsługuje arytmetykę IEEE-754?
Dzięki ale dlaczego wynik jest t1-t2 < = -2? a nie t1-t2 <0? – william007
Ponieważ 't1',' t2' i 'x' są liczbami całkowitymi. Dla liczb całkowitych mamy to, jeśli 'a
Ta odpowiedź wydaje się być nieaktualna, ponieważ w rezultacie daje "nieobsługiwane" (również w wersji wschodzącej) – DCTLib