5
Dire che hoCome nascondere variabile con Z3
t1<x and x<t2
è possibile nascondere x variabile in modo che t1<t2 in Z3?
A
risposta
6
È possibile utilizzare l'eliminazione del quantificatore per farlo. Ecco un esempio:
(declare-const t1 Int)
(declare-const t2 Int)
(elim-quantifiers (exists ((x Int)) (and (< t1 x) (< x t2))))
Si può provare questo esempio online all'indirizzo: http://rise4fun.com/Z3/kp0X
1
Possibile soluzione utilizzando Redlog di Reduce:
Problemi correlati
- 1. Controlla overflow con Z3
- 2. Lettura interp di un array z3 dal modello z3
- 3. Z3 Performance con aritmetica non lineare
- 4. Supporto quantificatore Z3
- 5. Quantificatore in Z3
- 6. Interpretazione delle statistiche Z3
- 7. z3 C++ API & ite
- 8. Come funziona la risoluzione incrementale in Z3?
- 9. Come ottenere risultati casuali da Microsoft Z3?
- 10. Problemi di trigger in Z3
- 11. Output di controesempio di Z3
- 12. Come nascondere gli avvisi di "variabile obsoleta" di Emacs?
- 13. Comprensione dell'indicizzazione delle variabili associate in Z3
- 14. Definizione di una teoria di insiemi con Z3/SMT-LIB2
- 15. Nascondere l'indirizzo email con jQuery
- 16. Alla ricerca di esempi pratici di applicazioni SMT Z3 (come DbC) e alternative open source a Z3?
- 17. formule di risolutore interno in z3
- 18. QF_FPA? Z3 supporta l'aritmetica IEEE-754?
- 19. Z3: trovare tutti i modelli soddisfacenti
- 20. (get-unsat-core) restituisce vuoto in Z3
- 21. Nascondere una variabile un'entità dal messaggio XML - non @XmlTransient lavoro
- 22. Come nascondere parte dell'immagine?
- 23. Come nascondere un UIBarButtonItem?
- 24. Nascondere una directory con htaccess
- 25. Nascondere il testo con QSyntaxHighlighter
- 26. Come nascondere il miniprofiler?
- 27. come nascondere codice javascript
- 28. Come nascondere _id dall'aggregazione?
- 29. Come nascondere/mostrare l'UIimageview?
- 30. Come nascondere ListView ColumnHeader?
Grazie, ma il motivo per cui il risultato è T1-T2 < = -2? e non t1-t2 <0? – william007
Perché, 't1',' t2' e 'x' sono numeri interi. Per gli interi abbiamo che se 'a
Questa risposta sembra essere superata, in quanto produce "non supportato" come risultato (anche su rise4fun) – DCTLib