z3py

10calore

1risposta

Z3/Python che ottiene i valori di python dal modello

Come posso ottenere valori Python reali da un modello Z3? E.g. p = Bool('p') x = Real('x') s = Solver() s.add(Or(x < 5, x > 10), Or(p, x**2 == 2), Not(p)) s.check() print s.model()[x] print s.mo

12calore

1risposta

(Z3Py) verifica tutte le soluzioni per l'equazione

In Z3Py, come posso controllare se l'equazione per i vincoli dati ha una sola soluzione? Se più di una soluzione, come posso elencare?

5calore

2risposta

Come posso accedere alla mappatura delle variabili utilizzata durante il bit-blasting?

Sto modificando uno strumento che utilizza Z3 (in particolare l'API Python) per risolvere i vincoli di bitvector. Ho bisogno di utilizzare un particolare SAT esterna risolutore al posto del Z3 interno

6calore

2risposta

Controlla overflow con Z3

Sono nuovo di Z3 e stavo controllando il tutorial online su Python. Quindi ho pensato di poter controllare il comportamento di overflow in BitVecs. Ho scritto questo codice: x = BitVec('x', 3) y = In

5calore

2risposta

Come modellare il numero intero con segno con BitVector?

Supponiamo che a sia un numero intero di 8 bit del valore 254. Se a è un numero intero con segno, viene in realtà considerato -2. Al contrario, se a non è firmato, rimane 254. Sto provando a modellare

5calore

2risposta

Python - Ottimizza il sistema di disuguaglianza

Sto lavorando ad un programma in Python in cui una piccola parte comporta l'ottimizzazione di un sistema di equazioni/disuguaglianze. Idealmente, avrei voluto fare come si può fare in Modelica, scrive

5calore

3risposta

Dove posso trovare tutorial z3py

rise4fun z3py non è disponibile da diverse settimane a causa di alcuni problemi di sicurezza. Ho cercato di scoprire alcune risorse per l'apprendimento di z3py ma sono finito invano. Si prega di sugge