z3 - Biblioteca eccellente

z3

7calore

2risposta

QF_FPA? Z3 supporta l'aritmetica IEEE-754?

Navigando sul codice sorgente Z3, mi sono imbattuto in un mucchio di file che si riferiscono a QF_FPA, che sembra rappresentare un'aritmetica a virgola mobile, senza quantificatori. Tuttavia, non ries

7calore

1risposta

(get-unsat-core) restituisce vuoto in Z3

Sto usando Z3 per estrarre il unsat-core di una formula insoddisfacente. Sto usando Z3 @ Aumento di interfaccia (web based) per scrivere il codice seguente, (set-logic QF_LIA) (set-option :produce-un

45calore

1risposta

Come funziona la risoluzione incrementale in Z3?

Ho una domanda su come Z3 risolve in modo incrementale i problemi. Dopo aver letto alcune risposte, ho trovato quanto segue: Esistono due modi per utilizzare Z3 per la risoluzione incrementale: uno è

5calore

1risposta

Come ottenere un elenco di tutte le impostazioni di configurazione disponibili per un contesto Z3?

L'API .NET ha la seguente costruzione per una Contesto: Context (Dictionary< string, string > settings) come ottenere un elenco di tutte le possibili impostazioni? In particolare, sono interessato a

7calore

1risposta

effetti Comprensione di prodotti-prove, i nomi dei campi, e intermedi check-SAT sulle prestazioni

Per il codice qui sotto, ho osservato risultati molto veloci che sembrano essere causato/colpiti da tre aspetti insoliti: Quando usando (set-option :produce-proof true), l'UNSAT finale è molto veloce.

5calore

1risposta

eliminando forall utilizzando UNSAT

Sappiamo che, siamo in grado di dimostrare la validità di un teorema dicendo: let Demorgan(x, y) = formula1(x,y) iff formula2(x,y) assert (forall (x,y) . Demorgan(x,y)) In alternativa possiamo elim

10calore

1risposta

Definizione di una teoria di insiemi con Z3/SMT-LIB2

Sto provando a definire una teoria di insiemi (unione, intersezione ecc.) per Z3 utilizzando l'interfaccia SMTLIB. Sfortunatamente, la mia attuale definizione blocca z3 per una query banale, quindi su

8calore

2risposta

Quali sono i limiti del ragionamento nell'aritmetica quantificata in SMT?

Ho provato diversi solutori SMT (CVC3, CVC4 e Z3) sul seguente parametro di riferimento apparentemente banale: (set-logic LIA) (set-info :smt-lib-version 2.0) (assert (forall ((x Int)) (forall ((y I

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