एक सूत्र को विघटनकारी सामान्य रूप में कैसे परिवर्तित करें?

Question

एक सूत्र दिया कहना

(t1> = 2 या t2> = 3) और (t3> = 1)

मैं अपने वियोगी सामान्य रूप प्राप्त करना चाहते हैं (t1> = 2 और T3> = 1) या (टी 2> = 3 और टी 3> = 1)

जेड 3 में इसे कैसे प्राप्त किया जाए?

Answer 1

Z3 में डीएनएफ में सूत्रों को परिवर्तित करने के लिए एपीआई या रणनीति नहीं है। हालांकि, इस रणनीति को split-clause का उपयोग करके कई उपगोर्गों में एक लक्ष्य तोड़ने का समर्थन है। सीएनएफ में एक इनपुट फॉर्मूला को देखते हुए, यदि हम इस रणनीति को पूरी तरह से लागू करते हैं, तो प्रत्येक आउटपुट सबगोल को एक बड़े संयोजन के रूप में देखा जा सकता है। यहां एक उदाहरण दिया गया है कि इसे कैसे करें।

(apply (then simplify (repeat (or-else split-clause skip)))) 

repeat Combinator रणनीति को लागू करने, जब तक यह किसी भी संशोधन के प्रदर्शन नहीं करता रहता है:

http://rise4fun.com/Z3/zMjO

यहाँ आदेश है। रणनीति split-clause विफल रहता है अगर इनपुट में कोई क्लॉज नहीं है। यही कारण है कि हम (कुछ भी नहीं) रणनीति के साथ or-else संयोजक का उपयोग करते हैं। हम प्रत्येक खंड को मामलों में विभाजित करने के बाद सरलीकरण लागू करने वाली रणनीतियों का उपयोग करके कमांड को बेहतर बना सकते हैं (उदा। simplify, solve-eqs)।

ध्यान दें कि उपर्युक्त स्क्रिप्ट इनपुट सूत्र को सीएनएफ में मानती है।