UPVARBDD(3)

📦 version 5.1.1, in fedora 43, fedora 44

💖 UPVARBDD 💖 (the upVarBdd situation, from the BDD functions manual)

okay bestie, welcome to upVarBdd(3) — yes that's the manual section number, we're in the big-kid library docs now 💅

🌈 ORIGIN 🌈

This software belongs to the ALLIANCE CAD SYSTEM, developed by the ASIM team at the LIP6 laboratory of Université Pierre et Marie CURIE, in Paris, France. 🇫🇷✨

✨ NAME ✨

upVarBdd — brings up an index in a BDD. that's it, that's the whole job, and it ate 💅

🎀 SYNOPSIS 🎀

#include "logmmm.h"
pNode upVarBdd(pBdd,oldIndex,newIndex)
pNode pBdd;
short oldIndex,newIndex;

🦋 PARAMETERS 🦋

  • pBdd — the BDD in which the index is being came up (yes, the original says "came up", we're keeping the vibe, no cap).
  • oldIndex — the index that's coming up. the one on the move.
  • newIndex — the new index. where it's headed.

💜 DESCRIPTION 💜

upVarBdd() constructs a graph obtained by bringing up oldIndex to newIndex. literally it's a glow-up for one single index, moving it to a higher spot in the ordering ✨

and the way this function gets called? it's called by the BDDs reordering function. so it's not out here doing solo main character work — it's a team player in the reordering process, iykyk 🫶

🌸 EXAMPLE 🌸

#include "mutnnn.h"      /* mbk utilities */
#include "logmmm.h"
pNode nodeA,nodeB;
pNode res;

initializeBdd(SMALL_BDD);
nodeA = createNodeTermBdd(3);
nodeB = createNodeTermBdd(3);
res = applyBinBdd(OR,nodeA,nodeB); /* res = (OR a b)
res = upVarBdd(res,2,4);
displayBdd(res,1);

/* it will display
@res     INDEX 4    LOW = @nodeB     HIGH = ONE
@nodeB   INDEX 3    LOW = ZERO       HIGH = ONE
*/

destroyBdd(1);

so we initialize the BDD with SMALL_BDD, make two term nodes at index 3, smash them together with applyBinBdd(OR,nodeA,nodeB), then call upVarBdd(res,2,4) to bump index 2 up to index 4, and displayBdd(res,1) shows you the whole thing. iconic. and then destroyBdd(1) cleans up because we're responsible queens 👑

😭 ERROR 😭

"upVarBdd : error - newIndex <= oldIndex"

The new index must be higher than the old index. periodt. if you try to make newIndex equal to or lower than oldIndex, you get that error and the function is NOT happy about it 🚫

fr fr, newIndex strictly greater than oldIndex or nothing. don't test her.

🌈 SEE ALSO 🌈

log(1), bdd(1), applyBdd(3), notBdd(3), constraintBdd(3), composeBdd(3), applyBinBdd(3), addListBdd(3), displayBdd(3), createNodeTermBdd(3).

go read those too bestie, the whole friend group is slaying 💖

🫶 BUG REPORT 🫶

This tool is under development at the ASIM department of the LIP6 laboratory.

We need your feedback to improve documentation and tools.

so like… if something's broken, TELL THEM. they literally said they need your feedback. it's giving "please help us help you" 🙈

and that's the whole page!! from the ASIM/LIP6 girlies, dated October 1, 1997 — yeah she's vintage and she still serves. UPVARBDD(3) forever, no cap 👑💅✨

📦 where this page comes from