AbstractedNames is a list of char*. If the list is not NULL, then this list is interpreted as a list of variables to abstract. If a given name in the list does not correspond to the hierarchical name of a node in the network, then NULL is returned, and an error message is written to error_string. Otherwise, a new primary input is created to drive the net identified by the variable name. See the documentation for the command flatten_hierarchy for more information.
The verification routines assume deterministic and completely specified tables. If a table is found that is locally non-deterministic or incompletely specified, then a message is written to vis_stderr, and a NIL network is returned (the non-deterministic test is not performed on non-deterministic constant tables). This test can be bypassed (in order to save time) by passing FALSE for buildMvfs. Note that this should be done with extreme caution, because bad tables could inadvertantly be allowed through and invalidate verification results obtained downstream.
Also, if a table has no inputs and more than 1 output, and its output space is not complete (i.e. the outputs are correlated), then the table is declared a "relation", and NIL is returned.] SideEffects [] Comment [Proceeds in 3 phases: 1) builds a map from formals to actuals, 2) adds a node for each actual (i.e. for each node that will appear in the network) and 3) sets the types (and tables, where appropriate) for each node.] SeeAlso [Ntk_NetworkAlloc NetworkBuildFormalToActualTableRecursively NetworkCreateNodesRecursively NetworkDeclareNodesRecursively] ******************************************************************************/ Ntk_Network_t * Ntk_HrcNodeConvertToNetwork( Hrc_Node_t *hrcNode, boolean buildMvfs, lsList abstractedNames) { mdd_manager *mddMgr; boolean status1 = TRUE; boolean status2 = TRUE; char *hrcNodeName = Hrc_NodeReadInstanceName(hrcNode); Ntk_Network_t *network = Ntk_NetworkAlloc(hrcNodeName); NetworkBuildFormalToActualTableRecursively(network, hrcNode); NetworkCreateNodesRecursively(network, hrcNode); /* * The MDD manager is for building temporary MDDs. For robustness, enable * reordering. */ mddMgr = mdd_init_empty(); bdd_dynamic_reordering(mddMgr, BDD_REORDER_SIFT, BDD_REORDER_VERBOSITY_DEFAULT); status1 = NetworkDeclareNodesRecursively(network, hrcNode, buildMvfs, &mddMgr); mdd_quit(mddMgr); if (abstractedNames != (lsList) NULL) { status2 = NetworkAbstractNodes(network, abstractedNames); } if (!(status1 && status2)) { Ntk_NetworkFree(network); return NIL(Ntk_Network_t); } else { return network; } } /*---------------------------------------------------------------------------*/ /* Definition of internal functions */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Definition of static functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Creates mapping from formal names to actual names.] Description [Loads the formal-to-actual table of network. For each formal variable name in hrcNode, maps it to a unique actual variable name. The map is many-to-one. The rule is that a formal is resolved to the actual as high in the hierarchy as possible. Proceeds recursively by examining subcircuits. Note that only formals are in the domain of the map. Also, care has to be taken when looking at net in parent since they may also be formals.] SideEffects [] ******************************************************************************/ static void NetworkBuildFormalToActualTableRecursively( Ntk_Network_t *network, Hrc_Node_t *hrcNode) { st_generator *stGen; char *childName; Hrc_Node_t *childHrcNode; /* * For each child of the current hnode, process its I/O variables, and * then recurse on its children. */ Hrc_NodeForEachChild(hrcNode, stGen, childName, childHrcNode) { int i; array_t *childFormalInputs = Hrc_NodeReadFormalInputs(childHrcNode); array_t *childFormalOutputs = Hrc_NodeReadFormalOutputs(childHrcNode); array_t *childFormalIoArray = LocalArrayJoin(childFormalInputs, childFormalOutputs); array_t *childActualInputs = Hrc_NodeReadActualInputs(childHrcNode); array_t *childActualOutputs = Hrc_NodeReadActualOutputs(childHrcNode); array_t *childActualIoArray = LocalArrayJoin(childActualInputs, childActualOutputs); /* * For each I/O variable, construct the appropriate hierarchical name for * the variable in childHrcNode (formalName) and the variable in the * hrcNode (actualName). If actualName already has a corresponding * actual, then use that, otherwise use actualName as is. Add * correspondence from formal (formalName) to actual (actualName). */ for(i = 0 ; i < array_n(childActualIoArray) ; i++) { Var_Variable_t *actualVar = array_fetch(Var_Variable_t *, childActualIoArray, i); Var_Variable_t *formalVar = array_fetch(Var_Variable_t *, childFormalIoArray, i); char *nodeName = Hrc_NodeFindHierarchicalName(hrcNode, TRUE); /* Special case the situation where hrcNode is current node. */ char *actualName = (strcmp(nodeName, "")) ? util_strcat3(nodeName, ".", Var_VariableReadName(actualVar)) : util_strsav(Var_VariableReadName(actualVar)); char *childNodeName = Hrc_NodeFindHierarchicalName(childHrcNode, TRUE); char *formalName = util_strcat3(childNodeName, ".", Var_VariableReadName(formalVar)); /* * It is correct to call this function with actualName. We want to * check if actualVar is itself a formalVar one level up. */ char *tempName = Ntk_NetworkReadActualNameFromFormalName(network, actualName); FREE(nodeName); FREE(childNodeName); /* * (tempName != NIL) => this net is a formal in hrcNode */ if (tempName != NIL(char)) { FREE(actualName); actualName = tempName; } /* * Ntk_NetworkInsertFormalNameToActualName makes copies of the strings */ Ntk_NetworkInsertFormalNameToActualName(network, formalName, actualName); if (tempName == NIL(char)) { FREE(actualName); } FREE(formalName); } array_free(childFormalIoArray); array_free(childActualIoArray); /* * Recurse. */ NetworkBuildFormalToActualTableRecursively(network, childHrcNode); } } /**Function******************************************************************** Synopsis [Creates placeholders for all the nodes in the network.] Description [Working top-down, creates placeholders for all the nodes in the network. After this function is executed, each node will have a name and Var_Variable_t, but nothing else. Note that nodes are created for reset logic; they are given the name of their corresponding latch, suffixed by $INIT.] SideEffects [] SeeAlso [NodeCreateAsNecessary] ******************************************************************************/ static void NetworkCreateNodesRecursively( Ntk_Network_t *network, Hrc_Node_t *hrcNode) { st_generator *stGen; Var_Variable_t *var; Hrc_Latch_t *latch; char *varName; char *latchName; char *childName; Hrc_Node_t *childHrcNode; char *path = Hrc_NodeFindHierarchicalName(hrcNode, TRUE); char *separator = (char *) ((strcmp(path, "")) ? "." : ""); /* * The separator is used to handle the special case when hrcNode is the * current node in the hierarchy. If it is, we don't want a "." before the * variable names. */ Hrc_NodeForEachVariable(hrcNode, stGen, varName, var) { char *nodeName = util_strcat3(path, separator, varName); NodeCreateAsNecessary(network, nodeName, var); FREE(nodeName); } /* * Variable for reset is the same as for present state. Hence, iterating * through the list of variables gets us just the present state. Therefore, * we need to special case the reset (or init) nodes. */ Hrc_NodeForEachLatch(hrcNode, stGen, latchName, latch) { char *partialNodeName = util_strcat3(path, separator, latchName); char *nodeName = util_strcat3(partialNodeName, "$INIT", ""); FREE(partialNodeName); NodeCreateAsNecessary(network, nodeName, Hrc_LatchReadOutput(latch)); FREE(nodeName); } FREE(path); /* Recurse. */ Hrc_NodeForEachChild(hrcNode, stGen, childName, childHrcNode) { NetworkCreateNodesRecursively(network, childHrcNode); } } /**Function******************************************************************** Synopsis [Creates a node with a given name, if one doesn't already exist.] Description [If a node with nodeName already exists in the network, then does nothing. Otherwise, creates a new node in the network with nodeName and variable.] SideEffects [] ******************************************************************************/ static void NodeCreateAsNecessary( Ntk_Network_t *network, char *nodeName, Var_Variable_t *var) { if (Ntk_NetworkFindNodeByName(network, nodeName)) { return; } (void) Ntk_NodeCreateInNetwork(network, nodeName, var); } /**Function******************************************************************** Synopsis [Add functionality to the Ntk_Node_t's for this Hrc_Node_t.] Description [Add functionality to the Ntk_Node_t's for this Hrc_Node_t. Proceeds in 3 stages: 1) sets PI's and PO's; this is achieved by looking at PI/POs which are not formals, 2) adds tables to combinational logic, taking care to get the non-deterministic/deterministic constants right, 3) iterates over latches, adding type latch to nodes which have a name correspoding to this latch's ps name, and declaring the initialization logic for the latch.
If a table is found that is non-deterministic or incompletely specified, then a message is written to vis_stderr, and FALSE is returned (the non-deterministic test is not performed on non-deterministic constant tables). Also, if a table has no inputs and more than 1 output and its output space is not complete, then it's declared a "relation", and FALSE is returned. However, even if FALSE is returned, the nodes are still declared.
The non-deterministic or incompletely specified tests can be bypassed by passing FALSE for buildMvfs. See Ntk_HrcNodeConvertToNetwork for more info.] SideEffects [] ******************************************************************************/ static boolean NetworkDeclareNodesRecursively( Ntk_Network_t *network, Hrc_Node_t *hrcNode, boolean buildMvfs, mdd_manager **mddMgr) { int i; st_generator *stGen; char *latchName; Var_Variable_t *var; Hrc_Latch_t *latch; Tbl_Table_t *table; char *childName; Hrc_Node_t *childHrcNode; boolean result = TRUE; char *path = Hrc_NodeFindHierarchicalName(hrcNode, TRUE); char *separator = (char *) ((strcmp(path, "")) ? "." : ""); /* * First declare the network's PI/PO nodes. */ NetworkDeclareIONodes(network, hrcNode); /* * Next, declare those nodes whose function is represented by a table. Note * that his iterator does not pick up those tables that define the * initialization logic of latches. */ Hrc_NodeForEachNameTable(hrcNode, i, table) { int index; Tbl_TableForEachOutputVar(table, index, var) { boolean status; char *fullVarName = util_strcat3(path, separator, Var_VariableReadName(var)); Ntk_Node_t *node = Ntk_NetworkFindNodeByName(network, fullVarName); FREE(fullVarName); status = NodeDeclareWithTable(node, table, index, path, buildMvfs, *mddMgr); if (!status) { result = FALSE; } MddManagerResetIfNecessary(mddMgr); } } /* * Declare each latch and its corresponding next state shadow node. */ NetworkDeclareLatches(network, hrcNode); /* * Declare the "initial" node corresponding to each latch. */ Hrc_NodeForEachLatch(hrcNode, stGen, latchName, latch) { int index; table = Hrc_LatchReadResetTable(latch); /* * There is only one output variable (the 0th output) for any table * defining the initial function of a latch, but we use an iterator to get * the variable for convenience. */ Tbl_TableForEachOutputVar(table, index, var) { boolean status; char *fullVarName = util_strcat3(path, separator, Var_VariableReadName(var)); char *initName = util_strcat3(fullVarName, "$INIT", ""); Ntk_Node_t *node = Ntk_NetworkFindNodeByName(network, initName); /* * Since the output of this table corresponds to a latch PS, can get name * of the initial node by attaching $INIT. */ FREE(fullVarName); FREE(initName); status = NodeDeclareWithTable(node, table, index, path, buildMvfs, *mddMgr); if (!status) { result = FALSE; } MddManagerResetIfNecessary(mddMgr); } } FREE(path); /* Recurse. */ Hrc_NodeForEachChild(hrcNode, stGen, childName, childHrcNode) { boolean status = NetworkDeclareNodesRecursively(network, childHrcNode, buildMvfs, mddMgr); if (!status) { result = FALSE; } } return result; } /**Function******************************************************************** Synopsis [Creates a new array consisting of array1 and array2.] Description [Returns a new array which consists of the elements of array 1 followed by the elements of array2.] Comment [It is suspected that the array_join from the array package is buggy when one of the arrays has 0 length. Hence, we defined our own.] SideEffects [] ******************************************************************************/ static array_t * LocalArrayJoin( array_t *array1, array_t *array2) { if (array_n(array1) == 0) { return (array_dup(array2)); } else if (array_n(array2) == 0) { return (array_dup(array1)); } else { return (array_join(array1, array2)); } } /**Function******************************************************************** Synopsis [Creates an array of table input names.] Description [Creates an array of table input names. For the ith input of table, the string "namePrefix.variableName_i" is placed in the ith position of the returned array, where variableName_i is the name of the variable corresponding to the ith input. (If namePrefix is "", then just "variableName_i" is used.) It is the responsiblity of the caller to free the strings in the returned array.] SideEffects [] SeeAlso [NameArrayFree] ******************************************************************************/ static array_t * TableCreateFormalInputNameArray( Tbl_Table_t *table, char *namePrefix) { int index; array_t *nameArray; Var_Variable_t *var; char *separator = (char *) ((strcmp(namePrefix, "")) ? "." : ""); /* * Allocate an array of length equal to the number of inputs of the table. * Then, for each input, add the full path name of the input to the array. */ nameArray = array_alloc(char *, Tbl_TableReadNumInputs(table)); Tbl_TableForEachInputVar(table, index, var) { char *inputFullName = util_strcat3(namePrefix, separator, Var_VariableReadName(var)); array_insert(char *, nameArray, index, inputFullName); } return (nameArray); } /**Function******************************************************************** Synopsis [Frees the strings in an array, and frees the array itself.] SideEffects [] SeeAlso [TableCreateFormalInputNameArray] ******************************************************************************/ static void NameArrayFree( array_t *nameArray) { int i; for (i = 0; i < array_n(nameArray); i++) { char *name = array_fetch(char *, nameArray, i); FREE(name); } array_free(nameArray); } /**Function******************************************************************** Synopsis [Abstract each node named in abstractedNames.] Description [Abstract each node named in abstractedNames. A node x is abstracted by creating a single new primary input node, with the name x$ABS and with the same variable as x, which will fanout to every node the original node fanned out to. The old node will continue to exists as before but will have no fanouts after abstraction; it can still be referred to in CTL formulas, etc.] SideEffects [] ******************************************************************************/ static boolean NetworkAbstractNodes( Ntk_Network_t *network, lsList abstractedNames) { char *name; lsGen gen; /* * For each abstracted name, cut the corresponding net, and introduce a new * node. */ lsForEachItem(abstractedNames, gen, name) { Var_Variable_t *var; Ntk_Node_t *abstractNode; array_t *abstractNodeFanouts; int i; Ntk_Node_t *fanout; char *abstractNodeName; Ntk_Node_t *node = Ntk_NetworkFindNodeByName(network, name); /* Make sure the name corresponds to a node in the network. */ if (node == NIL(Ntk_Node_t)) { error_append("Could not find node corresponding to name: "); error_append(name); error_append("\n"); return FALSE; } /* Create the new node in the network as a primary input. */ abstractNodeName = util_strcat3(name, "$ABS", ""); var = Ntk_NodeReadVariable(node); abstractNode = Ntk_NodeCreateInNetwork(network, abstractNodeName, var); FREE(abstractNodeName); Ntk_NodeDeclareAsPrimaryInput(abstractNode); /* * For each fanout y of the node x being abstracted, replace x in y's * fanin list by the new node, and add y to the fanout list of the new * node. */ abstractNodeFanouts = Ntk_NodeReadFanouts(abstractNode); Ntk_NodeForEachFanout(node, i, fanout) { int index = Ntk_NodeReadFaninIndex(fanout, node); array_t *fanoutFanins = Ntk_NodeReadFanins(fanout); array_insert(Ntk_Node_t *, fanoutFanins, index, abstractNode); array_insert_last(Ntk_Node_t *, abstractNodeFanouts, fanout); } /* * Replace the fanout array of the node being abstracted with an empty * array. */ array_free(node->fanouts); node->fanouts = array_alloc(Ntk_Node_t *, 0); } return TRUE; } /**Function******************************************************************** Synopsis [Declare a node with a table, and run some tests.] Description [Declare a node with a table, and run some tests. Creates the MVF for the output of table denoted by outIndex, in terms of the table inputs (new MDD variables are created). This MVF is created within mddMgr, and freed at the end of the function. The MVF is checked to see if it represents nondeterministic or incompletely specified behavior. If it does, a message is written to vis_stderr, and FALSE is returned. Also, if a table has no inputs and more than 1 output and its output space is not complete, then it's declared a "relation", and FALSE is returned.
If the table passes these tests, then a reduced table is built for this table output, consisting of just that output and the input columns in the support of that output. The node is then declared as a "pseudo-input" if the table represents a nondeterministic constant, or a "combinational" node otherwise.
Building the MVF, performing the tests, and building the reduced table, is bypassed if the input buildMvfs is FALSE. Note that this should be done with extreme caution, because bad tables could inadvertantly be allowed through and invalidate verification results obtained downstream.] SideEffects [] ******************************************************************************/ static boolean NodeDeclareWithTable( Ntk_Node_t *node, Tbl_Table_t *table, int outIndex, char *path, boolean buildMvfs, mdd_manager *mddMgr) { Tbl_Table_t *newTable; int newOutIndex; boolean result = TRUE; char *nodeName = Ntk_NodeReadName(node); /* * If table has no inputs and more than one output, and its output space is * not complete (i.e. not all output minterms are present, so the outputs * are correlated), then declare the table a relation. */ if ((Tbl_TableReadNumInputs(table) == 0) && (Tbl_TableReadNumOutputs(table) > 1)) { if (!Tbl_TableTestIsOutputSpaceComplete(table, mddMgr)) { (void) fprintf(vis_stderr, "Table %s is a relation\n", nodeName); result = FALSE; } } if (!buildMvfs) { newTable = Tbl_TableSoftDup(table); newOutIndex = outIndex; } else { Mvf_Function_t *outMvf; int offset; int numInputs = Tbl_TableReadNumInputs(table); array_t *varMap = array_alloc(int, numInputs); outMvf = LocalMvfFunctionForTable(table, outIndex, mddMgr, varMap, &offset); /* * If the function is not a non-deterministic constant, or it has some * inputs, then check that it is deterministic. Always check that it is * completely specified. */ if ((numInputs > 0) || !Mvf_FunctionTestIsNonDeterministicConstant(outMvf)) { if (!Mvf_FunctionTestIsDeterministic(outMvf)) { (void) fprintf(vis_stderr, "Table %s is not deterministic\n", nodeName); result = FALSE; } } if (!Mvf_FunctionTestIsCompletelySpecified(outMvf)) { (void) fprintf(vis_stderr, "Table %s is not completely specified\n", nodeName); result = FALSE; } /* * Build the reduced table for the output corresponding to outIndex. The * reduced table will have only one output column (column 0), and will have * only those input columns corresponding to the variables appearing in the * support of outMvf. */ newTable = Tbl_TableCreateTrueSupportTableForOutput(table, outMvf, mddMgr, offset, outIndex, varMap); newOutIndex = 0; array_free(varMap); Mvf_FunctionFree(outMvf); } /* * Declare the node with the reduced table. */ if (Tbl_TableTestIsNonDeterministicConstant(newTable, newOutIndex)) { Ntk_NodeDeclareAsPseudoInput(node, newTable, newOutIndex); } else { array_t *formalInputNameArray = TableCreateFormalInputNameArray(newTable, path); /* Ntk_NodeDeclareAsCombinational will test for constants. */ Ntk_NodeDeclareAsCombinational(node, newTable, formalInputNameArray, newOutIndex); NameArrayFree(formalInputNameArray); } return result; } /**Function******************************************************************** Synopsis [Declares the primary inputs and outputs of the network.] Description [Declares the primary inputs and outputs of the network. Does this by iterating over the variables of the hrcNode. Any variable it finds that doesn't have a corresponding actual name in the network's corresponding formal-to-actual table is considered a primary IO.] SideEffects [] ******************************************************************************/ static void NetworkDeclareIONodes( Ntk_Network_t *network, Hrc_Node_t *hrcNode) { st_generator *stGen; char *varName; Var_Variable_t *var; char *path = Hrc_NodeFindHierarchicalName(hrcNode, TRUE); char *separator = (char *) ((strcmp(path, "")) ? "." : ""); Hrc_NodeForEachVariable(hrcNode, stGen, varName, var) { if (Var_VariableTestIsPO(var) || Var_VariableTestIsPI(var)) { char *fullVarName = util_strcat3(path, separator, Var_VariableReadName(var)); char *tmpName = Ntk_NetworkReadActualNameFromFormalName(network, fullVarName); /* * If tmpName == NIL, this must be a PI/PO of the top most node in the hierarchy of * nodes. Hence, this is a true input/output of the hierarchy. */ if (tmpName == NIL(char)) { Ntk_Node_t *node = Ntk_NetworkFindNodeByName(network, fullVarName); if (Var_VariableTestIsPO(var)) { Ntk_NodeDeclareAsPrimaryOutput(node); } else { Ntk_NodeDeclareAsPrimaryInput(node); } } FREE(fullVarName); } } FREE(path); } /**Function******************************************************************** Synopsis [Declares the latches of the network.] Description [Declares the latches of the network. Does this by iterating over the latches of the hrcNode. For each latch, also creates and declares a corresponding next state shadow node.] SideEffects [] ******************************************************************************/ static void NetworkDeclareLatches( Ntk_Network_t *network, Hrc_Node_t *hrcNode) { st_generator *stGen; char *name; Hrc_Latch_t *latch; char *path = Hrc_NodeFindHierarchicalName(hrcNode, TRUE); char *separator = (char *) ((strcmp(path, "")) ? "." : ""); Hrc_NodeForEachLatch(hrcNode, stGen, name, latch) { char *nextStateName; Ntk_Node_t *nextStateNode; char *latchName = util_strcat3(path, separator, Var_VariableReadName(Hrc_LatchReadOutput(latch))); char *initName = util_strcat3(latchName, "$INIT", ""); char *dataName = util_strcat3(path, separator, Var_VariableReadName(Hrc_LatchReadInput(latch))); Ntk_Node_t *latchNode = Ntk_NetworkFindNodeByName(network, latchName); FREE(latchName); Ntk_NodeDeclareAsLatch(latchNode, dataName, initName); FREE(initName); FREE(dataName); /* * Create the corresponding shadow next state node for the latch. This holds * the next state variable. */ nextStateName = util_strcat3(Ntk_NodeReadName(latchNode), "$NS", ""); nextStateNode = Ntk_NodeCreateInNetwork(network, nextStateName, Hrc_LatchReadOutput(latch)); FREE(nextStateName); Ntk_NodeDeclareAsShadow(nextStateNode, latchNode); } FREE(path); } /**Function******************************************************************** Synopsis [Potentially quits mddMgr and starts a new one.] Description [Quits mddMgr if the number of binary variables exceeds MAX_NUMBER_BDD_VARS, and starts a new manager with no variables. Initializing an empty MDD manager is costly in some BDD packages, so we want to avoid doing it often (say, once per table). On the other hand, we don't want the manager to have too many variables, because then reordering becomes expensive.] SideEffects [] ******************************************************************************/ static void MddManagerResetIfNecessary( mdd_manager **mddMgr) { if (bdd_num_vars(*mddMgr) > MAX_NUMBER_BDD_VARS) { mdd_quit(*mddMgr); *mddMgr = mdd_init_empty(); bdd_dynamic_reordering(*mddMgr, BDD_REORDER_SIFT, BDD_REORDER_VERBOSITY_DEFAULT); } } /**Function******************************************************************** Synopsis [Builds the MVF of a table in terms of local variables.] Description [Builds the MVF of a table in terms of local variables. Also computes the offset of the local variables in the MDD manager and builds a map from the input columns of the table to the MDD id's. The offset is always 0 if the MDD manager is restarted.] SideEffects [varMap and offsetPtr are returned as side effects] ******************************************************************************/ static Mvf_Function_t * LocalMvfFunctionForTable( Tbl_Table_t *table, int outIndex, mdd_manager *mddMgr, array_t *varMap, int *offsetPtr ) { Mvf_Function_t *outMvf; Var_Variable_t *var; int colNum; int offset; int i; int numInputs = Tbl_TableReadNumInputs(table); array_t *faninMvfArray = array_alloc(Mvf_Function_t *, numInputs); array_t *mvarValues = array_alloc(int, numInputs); st_table *varTable = st_init_table(st_ptrcmp,st_ptrhash); /* Create MDD variables for the table inputs. If there are more inputs * tied to the sameVar_Variable_t, create just one MDD variable. Record * the mapping from inputs to variable indices in varMap. */ Tbl_TableForEachInputVar(table, colNum, var) { int index; if (st_lookup_int(varTable,var,&index)) { array_insert_last(int, varMap, index); } else { index = array_n(mvarValues); array_insert_last(int, varMap, index); st_insert(varTable, var, (char *) (long) index); array_insert_last(int, mvarValues, Var_VariableReadNumValues(var)); } } st_free_table(varTable); /* Restarting the manager is optional. The effect is to get rid of the * MDD variable information in the manager, without incurring the cost * of quitting and re-initializing the manager. */ mdd_restart(mddMgr); offset = array_n(mdd_ret_mvar_list(mddMgr)); /* number of existing mvars */ assert(offset == 0); mdd_create_variables(mddMgr, mvarValues, NIL(array_t), NIL(array_t)); array_free(mvarValues); /* * Construct an MVF for each table input. The MVF for column i is the MVF * for MDD variable i. */ for (i = 0; i < numInputs; i++) { int index = array_fetch(int, varMap, i); Mvf_Function_t *faninMvf = Mvf_FunctionCreateFromVariable(mddMgr, (index + offset)); array_insert_last(Mvf_Function_t *, faninMvfArray, faninMvf); } /* Compute the MVF of the output indexed by outIndex. */ outMvf = Tbl_TableBuildMvfFromFanins(table, outIndex, faninMvfArray, mddMgr); Mvf_FunctionArrayFree(faninMvfArray); *offsetPtr = offset; return outMvf; } /* LocalMvfFunctionForTable */