מבוא לאימות תוכנה

ספר אלקטרוני מאת: ניר אדר

6.5.5.2. פעולת הגבלה - restriction

$plot:\[f{|_{{x_i}: = b}}\left( {{x_1},...{x_n}} \right) = f\left( {{x_1},...,{x_{i - 1}},b,{x_{i + 1}},...,{x_n}} \right)\]$ When $plot:$b \in \left\{ {0,1} \right\}$$

הפעולה מציבה ערך קבוע לאחד המשתנים של הפונקציה.

בהינתן BDD המתאר את plot:$f$ נבנה BDD עבור $plot:$f{|_{{x_{i: = b}}}}$$ באופן הבא:

נבצע DFS על ה-BDD של .
לכל צומת שיש לו בן כך ש $plot:$\operatorname{var} \left( u \right) = {x_i}$$ נשנה ההצבעה מ- אל אל $plot:$low\left( u \right)$$ אם ול- $plot:$high\left( u \right)$$ אם .
בסוף התהליך - נבצע reduce.

דוגמא:

$plot:$f\left( {{x_1},{x_2},{x_3}} \right) = \left( {{x_1} \wedge {x_2}} \right) \vee {x_3}$$

$plot:$f\left( {{x_1},{x_2},{x_3}} \right)|{x_{2 = 0}} = \left( {{x_1} \wedge 0} \right) \vee {x_3} = {x_3}$$

נשים לב שניתן לממש את הכמתים בעזרת ההצבות. נגדיר את הכמתים "קיים" ו-"לכל":

$plot:$f{|_{x = 0}} \vee f{|_{x = 1}}$$ $plot:$ \equiv $$ $plot:$\exists x:f$$ קיים

$plot:$f{|_{x = 0}} \wedge f{|_{x = 1}}$$ $plot:$ \equiv $$ $plot:$\forall x:f$$ לכל

תזכורת – אלגוריתם DFS:

   dfs-visit (Graph G, Vertex u)
    {
         the vertex u is painted gray
         
         for all white successors v of u
         {
             dfs-visit(G, v)
         }

         u is painted black
    }


    dfs (Graph G)
    {
         all vertices of G are first painted white

         dfs-visit(G, root of G)
    }