Equivalente a define-fun nell’API Z3

Usando Z3 con il formato testuale, posso usare define-fun per definire le funzioni da riutilizzare in seguito. Per esempio:

 (define-fun mydiv ((x Real) (y Real)) Real (if (not (= y 0.0)) (/ xy) 0.0)) 

Mi chiedo come creare define-fun con Z3 API (io uso F #) invece di ripetere il corpo della funzione ovunque. Voglio usarlo per evitare la duplicazione e le formule di debug più facili. Ho provato con Context.MkFuncDecl , ma sembra generare solo funzioni non interpretate.

Il comando define-fun sta semplicemente creando una macro. Si noti che lo standard SMT 2.0 non consente definizioni ricorsive. Z3 espanderà ogni occorrenza di my-div durante il tempo di analisi. Il comando define-fun può essere usato per rendere il file di input più semplice e facile da leggere, ma internamente non aiuta veramente Z3.

Nell’API corrente, non vi è alcun supporto per la creazione di macro. Questa non è una vera limitazione, dal momento che possiamo definire una funzione C o F # che crea istanze di una macro. Tuttavia, sembra che tu voglia visualizzare (e ispezionare manualmente) le formule create usando l’API Z3. In questo caso, le macro non ti aiuteranno.

Un’alternativa è usare i quantificatori. Puoi dichiarare una funzione non interpretata my-div e asserire la formula universalmente quantificata:

 (declare-fun mydiv (Real Real) Real) (assert (forall ((x Real) (y Real)) (= (mydiv xy) (if (not (= y 0.0)) (/ xy) 0.0)))) 

Ora puoi creare la tua formula usando la funzione non interpretata mydiv .

Questo tipo di formula quantificata può essere gestito da Z3. In realtà, ci sono due opzioni per gestire questo tipo di quantificatore:

  1. Usa il macro finder: questo passo di pre-elaborazione identifica i quantificatori che essenzialmente definiscono le macro e le espandono. Tuttavia, l’espansione si verifica solo durante il tempo di pre-elaborazione, non durante l’analisi (ad es. Tempo di costruzione della formula). Per abilitare il finder del modello, devi usare MACRO_FINDER=true
  2. L’altra opzione è l’uso di MBQI (istanza di quantificatore basata su modello). Questo modulo può anche gestire questo tipo di quantificatore. Tuttavia, i quantificatori saranno espansi su richiesta.

Ovviamente, il tempo di risoluzione può dipendere pesantemente dall’approccio utilizzato. Ad esempio, se la tua formula è insoddisfacente indipendentemente dal “significato” di mydiv , allora l’approccio 2 è probabilmente migliore.

Ho lo stesso problema. Più specificamente, avevo bisogno della funzione:

 Z3_ast Z3_mk_bvredxnor(Z3_context ctx, Z3_ast t) 

che esegue un xnor su tutti i bit di un bitvector dato in argomento alla funzione e restituisce un bitvector di lunghezza 1.

Poiché questa funzione non esiste nell’API, ho iniziato a utilizzare:

 Z3_ast mk_bvredxnor(Z3_context ctx, Z3_ast t) { size_t i; size_t s = Z3_get_bv_sort_size(ctx,Z3_get_sort(ctx,t)); Z3_ast ret = Z3_mk_extract(ctx,0,0,t); for(i=1;i 

Quindi, provare a eseguire il debug dei miei vincoli è stato un incubo.

Quindi mi sono inventato:

 Z3_func_decl getBvredxnorDecl(Z3_context ctx, int size) { static bool sizes[64]={0}; static Z3_func_decl declTab[64]={0}; if(sizes[size]) return declTab[size]; Z3_sort bv_size = Z3_mk_bv_sort(ctx, size); Z3_sort bv1 = Z3_mk_bv_sort(ctx, 1); stringstream buff; buff << "bvredxnor" << size; Z3_symbol var_name = Z3_mk_string_symbol(ctx,"X"); Z3_symbol func_name = Z3_mk_string_symbol(ctx, buff.str().c_str()); Z3_func_decl bvredxnorDecl = Z3_mk_func_decl(ctx, func_name, 1, &bv_size, bv1); declTab[size]=bvredxnorDecl; Z3_ast b = Z3_mk_bound(ctx,0,bv_size); /* bounded variable */ Z3_ast bvredxnorApp = Z3_mk_app(ctx,bvredxnorDecl, 1, &b); Z3_pattern pattern = Z3_mk_pattern(ctx,1,&bvredxnorApp); Z3_ast bvredxnor_def = mk_bvredxnor(ctx,b); Z3_ast def = Z3_mk_eq(ctx,bvredxnorApp,bvredxnor_def); Z3_ast axiom = Z3_mk_forall(ctx,0,1,&pattern,1,&bv_size,&name,def); Z3_assert_cnstr(ctx,axiom); return bvredxnorDecl; } Z3_ast bvredxnor(Z3_context ctx, Z3_ast t) { int size = Z3_get_bv_sort_size(ctx,Z3_get_sort(ctx,t)); return Z3_mk_app(ctx,getBvredxnorDecl(ctx,size),1, &t); } 

Qualsiasi commento per migliorare questo sarebbe il benvenuto. Nel frattempo, risolve il problema che ho avuto qui

Fa il trucco, ma complica il mio modello ...

Inoltre mi chiedo:

  • Dato che tutto questo è stato fatto in modo programmatico, suppongo che MACRO_FINDER = TRUE non avrà alcun impatto (poiché è una fase di elaborazione).
  • Poiché MBQI è attivo per impostazione predefinita, non è necessario triggersrlo, giusto?