smt

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

Apprendimento Z3py - È disponibile il supporto per array e loop

Sto passando per Z3py e ho una domanda su come utilizzare l'API in un paio di casi specifici. Il codice seguente è una versione semplificata di qualcosa che alla fine vorrei usare per Z3. Alcune delle

5calore

2risposta

Come generare una formula proposizionale casuale (CNF) in haskell?

Come posso ottenere una formula proposizionale casuale in haskell? Preferibilmente ho bisogno della formula in CNF, ma vorrei Voglio usare le formule per il test delle prestazioni che coinvolge anche

5calore

1risposta

Interpretazione delle statistiche Z3

Ho ottenuto diverse statistiche dalle corse di Z3. Devo capire cosa significano. Sono piuttosto arrugginito e non aggiornato per i recenti sviluppi di Sat e SMT solving, per questo motivo ho cercato d

5calore

1risposta

Utilizzo tattica Z3 QFNRA con tipi di dati: interazione o interlining

In Non-linear arithmetic and uninterpreted functions, Leonardo de Moura afferma che la tattica qfnra-nlsat non è stata ancora completamente integrata con il resto di Z3. Ho pensato che la situazione s

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

18calore

1risposta

Z3: trovare tutti i modelli soddisfacenti

Sto cercando di recuperare tutti i possibili modelli per alcune teorie del primo ordine usando Z3, un risolutore SMT sviluppato da Microsoft Research. Ecco un esempio di lavoro minima: (declare-const

5calore

1risposta

Lettura interp di un array z3 dal modello z3

Supponiamo di disporre di 2 array in una formula di cui si desidera verificare l'affidabilità utilizzando z3. Se z3 restituisce sat, voglio leggere la prima matrice nel modello z3 e stamparla piuttost