Z3 - Satisfiability Modulo Theories (SMT)
In modo molto semplice, questo strumento ci aiuterà a trovare valori per le variabili che devono soddisfare alcune condizioni e calcolarli a mano sarebbe molto fastidioso. Pertanto, è possibile indicare a Z3 le condizioni che le variabili devono soddisfare e troverà alcuni valori (se possibile).
Alcuni testi ed esempi sono tratti da https://ericpony.github.io/z3py-tutorial/guide-examples.htm
Operazioni di base
Booleani/And/Or/Not
Int/Semplifica/Reali
SMT solvers like Z3 can handle not only boolean formulas but also formulas involving integers and real numbers. In this section, we will explore some basic methods for working with integer and real arithmetic in Z3.
Integers
Z3 provides support for integer arithmetic operations such as addition, subtraction, multiplication, and division. These operations can be used to build complex formulas involving integers.
Constants
To represent integer constants in Z3, you can use the IntVal
function. For example, IntVal(42)
represents the integer constant 42.
Variables
To represent integer variables in Z3, you can use the Int
function. For example, Int('x')
represents an integer variable named 'x'.
Arithmetic Operations
Z3 provides functions for performing arithmetic operations on integers. Some of the commonly used functions are:
Add
: performs addition of two integers.Sub
: performs subtraction of two integers.Mul
: performs multiplication of two integers.Div
: performs integer division of two integers.Mod
: computes the remainder of integer division.
Constraints
To add constraints involving integers, you can use the And
function to combine multiple constraints. For example, And(x > 0, y < 10)
represents the constraint that variable 'x' is greater than 0 and variable 'y' is less than 10.
Reals
Z3 also provides support for real numbers. You can use the RealVal
function to represent real constants and the Real
function to represent real variables.
Constants
To represent real constants in Z3, you can use the RealVal
function. For example, RealVal(3.14)
represents the real constant 3.14.
Variables
To represent real variables in Z3, you can use the Real
function. For example, Real('x')
represents a real variable named 'x'.
Arithmetic Operations
Z3 provides functions for performing arithmetic operations on real numbers. Some of the commonly used functions are:
Add
: performs addition of two real numbers.Sub
: performs subtraction of two real numbers.Mul
: performs multiplication of two real numbers.Div
: performs division of two real numbers.
Constraints
To add constraints involving real numbers, you can use the And
function to combine multiple constraints. For example, And(x > 0.0, y < 1.0)
represents the constraint that variable 'x' is greater than 0.0 and variable 'y' is less than 1.0.
Stampa del Modello
To print the model, you can use the model
object obtained from the solver. The model
object contains the assignments for each variable in the formula.
Per stampare il modello, puoi utilizzare l'oggetto model
ottenuto dal risolutore. L'oggetto model
contiene le assegnazioni per ogni variabile nella formula.
This will print the assignments for each variable in the model.
Questo stamperà le assegnazioni per ogni variabile nel modello.
Aritmetica delle macchine
Le CPU moderne e i linguaggi di programmazione di uso comune utilizzano l'aritmetica su vettori di bit di dimensione fissa. L'aritmetica delle macchine è disponibile in Z3Py come Bit-Vectors.
Numeri con segno/senza segno
Z3 fornisce versioni speciali con segno delle operazioni aritmetiche in cui fa differenza se il bit-vector viene trattato come con segno o senza segno. In Z3Py, gli operatori <, <=, >, >=, /, % e >> corrispondono alle versioni con segno. Gli operatori corrispondenti senza segno sono ULT, ULE, UGT, UGE, UDiv, URem e LShR.
Funzioni
Le funzioni interpretate come l'aritmetica, in cui la funzione + ha una interpretazione standard fissa (aggiunge due numeri). Le funzioni non interpretate e le costanti sono massimamente flessibili; consentono qualsiasi interpretazione che sia coerente con i vincoli sulla funzione o costante.
Esempio: l'applicazione di f due volte a x produce di nuovo x, ma l'applicazione di f una volta a x è diversa da x.
Esempi
Risolutore di Sudoku
Questo esempio mostra come utilizzare Z3 per risolvere un Sudoku. Il Sudoku viene rappresentato come una griglia 9x9 di numeri interi, dove i numeri dati sono rappresentati come numeri diversi da zero e le celle vuote sono rappresentate come zeri. Il risolutore Z3 viene utilizzato per trovare una soluzione valida per il Sudoku. Se una soluzione viene trovata, viene stampata; altrimenti, viene stampato un messaggio che indica che il Sudoku non ha soluzione.
Riferimenti
Last updated