Perché 0 = 0,5?

Question

Ho notato un comportamento strano con Z3 4.3.1 quando si lavora con file .smt2.

Se faccio (assert (= 0 0.5)) sarà soddisfacibile. Tuttavia, se cambio l'ordine e faccio (assert (= 0.5 0)) non è soddisfacente.

La mia ipotesi su ciò che sta accadendo è che se il primo parametro è un numero intero, li inserisce entrambi in numeri interi (arrotondando 0,5 fino a 0), quindi esegue il confronto. Se cambio "0" a "0.0" funziona come previsto. Ciò è in contrasto con la maggior parte dei linguaggi di programmazione con cui ho lavorato dove se uno dei parametri è un numero in virgola mobile, entrambi sono espressi su numeri in virgola mobile e confrontati. Questo è davvero il comportamento previsto in Z3?

Answer 1

A rigor di termini, Z3 non è SMT 2.0 di default, e questo è uno di quei casi. Possiamo aggiungere

(set-option :smtlib2-compliant true) 

e quindi questa query è davvero respinto in modo corretto.

Answer 2

Uno dei nostri stagisti, che hanno lavorato su un'estensione conservativa di SMT2 con il polimorfismo ha notato lo stesso comportamento strano, quando ha cercato il capire come tipo-controllato formule di miscelazione numeri interi e reali sono:

Z3 (http://rise4fun.com/z3) dice che il seguente esempio è SAT, e trova un modello x = 1

(set-logic AUFLIRA) 
(declare-fun x() Int) 
(assert (= x 1.5)) 
(check-sat) 
(get-model) 
(exit) 

Ma, si dice che il seguente esempio "equivalente" in UNSAT

(set-logic AUFLIRA) 
(declare-fun x() Int) 
(assert (= 1.5 x)) 
(check-sat) 
(exit) 

Quindi, questo non è conforme alla proprietà simmetrica del predicato di uguaglianza. Quindi, penso che sia un bug.

Answer 3

Penso che questo sia una conseguenza della mancanza di controllo di tipo; z3 è troppo indulgente. Dovrebbe semplicemente rifiutare tali domande poiché semplicemente non sono ben formate.

Secondo lo standard SMT-Lib, v2 (http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.0-r10.12.21.pdf); pagina 30; la teoria centrale è definito nel seguente modo:

(theory Core 
:sorts ((Bool 0)) 
:funs ((true Bool) (false Bool) (not Bool Bool) 
     (=> Bool Bool Bool :right-assoc) (and Bool Bool Bool :left-assoc) 
     (or Bool Bool Bool :left-assoc) (xor Bool Bool Bool :left-assoc) 
     (par (A) (= A A Bool :chainable)) 
     (par (A) (distinct A A Bool :pairwise)) 
     (par (A) (ite Bool A A A)) 
    ) 
:definition 
"For every expanded signature Sigma, the instance of Core with that signature 
is the theory consisting of all Sigma-models in which: 
    - the sort Bool denotes the set {true, false} of Boolean values; 
    - for all sorts s in Sigma, 
     - (= s s Bool) denotes the function that 
     returns true iff its two arguments are identical; 
     - (distinct s s Bool) denotes the function that 
     returns true iff its two arguments are not identical; 
     - (ite Bool s s) denotes the function that 
     returns its second argument or its third depending on whether 
     its first argument is true or not; 
     - the other function symbols of Core denote the standard Boolean operators 
     as expected. 
     " 
    :values "The set of values for the sort Bool is {true, false}." 
) 

Così, uguaglianza definizione richiede i tipi di input per lo stesso; e quindi la query di cui sopra dovrebbe essere respinta come non valida.

Potrebbe esserci un passaggio a z3 o qualche altra impostazione che impone un controllo dei tipi più rigoroso rispetto a quello predefinito; ma mi sarei aspettato che questo caso venisse catturato anche con le implementazioni più rilassate.

Answer 4

Una possibile soluzione è

(declare-fun x() Real) 
(declare-fun y() Real) 
(assert (= x 0)) 
(assert (= y 0.5)) 
(check-sat) 
(push) 
(assert (= x y)) 
(check-sat) 
(pop) 

e l'uscita è

sat 
unsat 

Answer 5

Z3 non è il risolutore SMT unico che tipo verifiche questi esempi:

• CVC4 li accetta pure (anche con l'opzione --smtlib-strict), e risponde a UNSAT in entrambi i casi delle mie formule sopra.

• Yices li accetta e risponde UNSAT (dopo aver modificato la logica in QF_LIA, perché non supporta AUFLIRA).

• Con (set-logic QF_LIA), Z3 emette un errore: (errore "riga 3 colonna 17: la logica non supporta i real").

• Alt-Ergo dice "errore di digitazione: Int e Real non possono essere unificati" in entrambi i casi. Ma il parser SMT2 di Alt-Ergo è molto limitato e non molto testato, poiché ci siamo concentrati sul suo linguaggio polimorfico nativo. Quindi, non dovrebbe essere preso come riferimento.

Penso che gli sviluppatori di solito assumono una relazione sub-tipizzazione "implicito" tra Int e patrimonio. Questo è il motivo per cui questi esempi sono stati controllati con successo da Z3, CVC4 e Yices (e probabilmente anche da altri).

Answer 6

Non fare affidamento sulla conversione di tipo implicita di alcun risolutore. Invece, usa to_real e to_int per fare conversioni di tipo esplicito. Invia solo formule ben scritte al risolutore. Quindi gli esempi di Mohamed Iguernelala diventano i seguenti.

(set-logic AUFLIRA) 
(declare-fun x() Int) 
(assert (= (to_real x) 1.5)) 
(check-sat) 
(exit) 

(set-logic AUFLIRA) 
(declare-fun x() Int) 
(assert (= 1.5 (to_real x))) 
(check-sat) 
(exit) 

Entrambi questi ritorno UNSAT in Z3 e CVC4. Se invece, veramente volevi trovare il modello dove x = 1 avresti dovuto invece usare uno di quanto segue.

(set-option :produce-models true) 
(set-logic AUFLIRA) 
(declare-fun x() Int) 
(assert (= (to_int 1.5) x)) 
(check-sat) 
(get-model) 
(exit) 

(set-option :produce-models true) 
(set-logic AUFLIRA) 
(declare-fun x() Int) 
(assert (= x (to_int 1.5))) 
(check-sat) 
(get-model) 
(exit) 

Entrambi questi ritornano SAT con x = 1 in Z3 e CVC4.

Una volta che tutte le conversioni di tipo sono esplicite e si occupano solo di formule ben tipizzate, l'ordine degli argomenti di uguaglianza non conta più (per correttezza).

Answer 7

Jochen Hoenicke ha fornito la risposta (sulla mailing list SMT-LIB) relativa a "mixing reals e interi". Eccolo:

I just wanted to point out, that the syntax may be officially correct. There is an extension in AUFLIRA and AUFNIRA.

From http://smtlib.cs.uiowa.edu/logics/AUFLIRA.smt2

"For every operator op with declaration (op Real Real s) for some sort s, and every term t1, t2 of sort Int and t of sort Real, the expression - (op t1 t) is syntactic sugar for (op (to_real t1) t) - (op t t1) is syntactic sugar for (op t (to_real t1)) - (/ t1 t2) is syntactic sugar for (/ (to_real t1) (to_real t2)) "