जेड 3 एपीआई

Question

में परिभाषित-मज़े के समतुल्य पाठ प्रारूप के साथ Z3 का उपयोग करके, मैं बाद में पुन: उपयोग के लिए फ़ंक्शंस को परिभाषित करने के लिए define-fun का उपयोग कर सकता हूं। उदाहरण के लिए:

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

मुझे आश्चर्य है कि जेड 3 एपीआई (मैं का उपयोग एफ #) के बजाय हर जगह समारोह के शरीर दोहरा साथ define-fun कैसे बनाते हैं। मैं डुप्लिकेशंस और डिबग सूत्रों को आसान बनाने से बचने के लिए इसका उपयोग करना चाहता हूं। मैंने Context.MkFuncDecl के साथ प्रयास किया, लेकिन ऐसा लगता है कि यह केवल अनियंत्रित कार्यों को उत्पन्न करता है।

Answer 1

define-fun कमांड सिर्फ एक मैक्रो बना रहा है। ध्यान दें कि एसएमटी 2.0 मानक रिकर्सिव परिभाषाओं की अनुमति नहीं देता है। Z3 पार्सिंग समय के दौरान my-div की हर घटना का विस्तार करेगा। कमांड define-fun का उपयोग इनपुट फ़ाइल को पढ़ने के लिए आसान और आसान बनाने के लिए किया जा सकता है, लेकिन आंतरिक रूप से यह वास्तव में Z3 की सहायता नहीं करता है।

वर्तमान API में, मैक्रोज़ बनाने के लिए कोई समर्थन नहीं है। यह वास्तविक सीमा नहीं है, क्योंकि हम एक सी या एफ # फ़ंक्शन को परिभाषित कर सकते हैं जो मैक्रो के उदाहरण बनाता है। हालांकि, ऐसा लगता है कि आप Z3 API का उपयोग करके बनाए गए सूत्रों को प्रदर्शित (और मैन्युअल रूप से निरीक्षण) करना चाहते हैं। इस मामले में, मैक्रोज़ आपकी मदद नहीं करेंगे।

एक विकल्प क्वांटिफायर का उपयोग करना है। आप एक uninterpreted समारोह my-div घोषित करने और सार्वभौमिक मात्रा निर्धारित सूत्र जोर कर सकते हैं: अब

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

, आप अपने सूत्र uninterpreted समारोह mydiv का उपयोग कर बना सकते हैं।

इस तरह के मात्राबद्ध फॉर्मूला को Z3 द्वारा नियंत्रित किया जा सकता है।

1. मैक्रो खोजकर्ता का उपयोग करें: इस preprocessing कदम परिमाणकों कि अनिवार्य रूप से मैक्रो को परिभाषित करने और उन्हें विस्तार कर रहे हैं की पहचान करता है वास्तव में, वहाँ दो विकल्प परिमाणक इस तरह की संभाल करने के लिए कर रहे हैं। हालांकि, विस्तार केवल प्रीप्रोकैसिंग समय के दौरान होता है, पार्सिंग के दौरान नहीं (यानी, फॉर्मूला निर्माण समय)। मॉडल खोजक को सक्षम करने के लिए, आपको MACRO_FINDER=true
2. का उपयोग करना होगा अन्य विकल्प MBQI (मॉडल आधारित क्वांटिफ़ायर तत्काल) का उपयोग करना है। यह मॉड्यूल इस तरह के क्वांटिफायर को भी संभाल सकता है। हालांकि, मांग पर क्वांटिफायर का विस्तार किया जाएगा।

बेशक, हल करने का समय आपके द्वारा उपयोग किए जाने वाले दृष्टिकोण पर निर्भर करता है। उदाहरण के लिए, यदि आपका सूत्र mydiv के "अर्थ" से स्वतंत्र रूप से असंतुष्ट है, तो दृष्टिकोण 2 शायद बेहतर है।

Answer 2

मेरे पास एक ही समस्या है। विशेष रूप से, मैं समारोह की जरूरत:

Z3_ast Z3_mk_bvredxnor(Z3_context ctx, Z3_ast t) 

जो एक bitvector कार्य करने के लिए तर्क में दिए गए के सभी बिट्स पर एक XNOR करता है, और लंबाई 1.

के bitvector रिटर्न इस काम नहीं करेगी जब से

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<s;i++) 
     ret = Z3_mk_bvxnor(ctx,ret,Z3_mk_extract(ctx,i,i,t)); 
    return ret; 
} 

फिर, डिबग करने के लिए मेरी कमी एक बुरा सपना था की कोशिश कर रहा: एपीआई में मौजूद हैं, मैं का उपयोग शुरू किया।सुधार करने के लिए इस स्वागत किया जाएगा

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); 
} 

कोई भी टिप्पणी:

तो मैं के साथ आया था। मतलब समय में, यह मुद्दा मैं here

यह काम कर देता है, लेकिन अपने मॉडल complexify ...

इसके अलावा मुझे आश्चर्य है कि हल करती है:

• इस के बाद से सभी प्रोग्राम के लिए किया जाता है, मैं मान लें कि MACRO_FINDER = TRUE का कोई प्रभाव नहीं होगा (क्योंकि यह एक प्रसंस्करण चरण है)।
• चूंकि एमबीक्यूआई डिफ़ॉल्ट रूप से चालू है, इसे सक्रिय करने की कोई आवश्यकता नहीं है, है ना?