src/puresat/puresatAig.c File Reference
#include "maigInt.h"#include "baig.h"#include "ntk.h"#include "puresatInt.h"
Include dependency graph for puresatAig.c:
Go to the source code of this file.
Functions | |
| void | PureSat_unconnectOutput (bAig_Manager_t *manager, bAigEdge_t from, bAigEdge_t to) |
| void | PureSat_connectOutput (bAig_Manager_t *manager, bAigEdge_t from, bAigEdge_t to, int inputIndex) |
| bAigEdge_t | PureSat_HashTableLookup (bAig_Manager_t *manager, bAigEdge_t node1, bAigEdge_t node2) |
| int | PureSat_HashTableAdd (bAig_Manager_t *manager, bAigEdge_t nodeIndexParent, bAigEdge_t nodeIndex1, bAigEdge_t nodeIndex2) |
| bAigEdge_t | PureSat_CreateAndNode (bAig_Manager_t *manager, bAigEdge_t node1, bAigEdge_t node2) |
| bAigEdge_t | PureSat_And2 (bAig_Manager_t *manager, bAigEdge_t nodeIndex1, bAigEdge_t nodeIndex2) |
| bAigEdge_t | PureSat_And3 (bAig_Manager_t *manager, bAigEdge_t l, bAigEdge_t r) |
| bAigEdge_t | PureSat_And4 (bAig_Manager_t *manager, bAigEdge_t l, bAigEdge_t r) |
| int | PureSat_Test2LevelMini (bAig_Manager_t *manager, bAigEdge_t l, bAigEdge_t r) |
| bAigEdge_t | PureSat_And (bAig_Manager_t *manager, bAigEdge_t nodeIndex1, bAigEdge_t nodeIndex2) |
| bAigEdge_t | PureSat_Or (bAig_Manager_t *manager, bAigEdge_t nodeIndex1, bAigEdge_t nodeIndex2) |
| bAigEdge_t | PureSat_Xor (bAig_Manager_t *manager, bAigEdge_t nodeIndex1, bAigEdge_t nodeIndex2) |
| bAigEdge_t | PureSat_Eq (bAig_Manager_t *manager, bAigEdge_t nodeIndex1, bAigEdge_t nodeIndex2) |
| bAigEdge_t | PureSat_Then (bAig_Manager_t *manager, bAigEdge_t nodeIndex1, bAigEdge_t nodeIndex2) |
| bAigEdge_t | PureSat_CreateVarNode (bAig_Manager_t *manager, nameType_t *name) |
Function Documentation
| bAigEdge_t PureSat_And | ( | bAig_Manager_t * | manager, |
| bAigEdge_t | nodeIndex1, | ||
| bAigEdge_t | nodeIndex2 | ||
| ) |
Function********************************************************************
Synopsis [And function for two AIG nodes. The difference with bAigCreateAndNode is that here two level minimization is only allowed with the same timeframe, otherwise the global variable for interpolation generation may not be latch variables]
Description []
SideEffects []
SeeAlso []
Definition at line 920 of file puresatAig.c.
{
bAigEdge_t newNodeIndex;
nodeIndex1 = bAig_GetCanonical(manager, nodeIndex1);
nodeIndex2 = bAig_GetCanonical(manager, nodeIndex2);
newNodeIndex = nodeIndex1; /* The left node has the smallest index */
if (bAig_NonInvertedEdge(nodeIndex1) > bAig_NonInvertedEdge(nodeIndex2)){
nodeIndex1 = nodeIndex2;
nodeIndex2 = newNodeIndex;
}
if ( nodeIndex2 == bAig_Zero ) {
return bAig_Zero;
}
if ( nodeIndex1 == bAig_Zero ) {
return bAig_Zero;
}
if ( nodeIndex2 == bAig_One ) {
return nodeIndex1;
}
if ( nodeIndex1 == bAig_One ) {
return nodeIndex2;
}
if ( nodeIndex1 == nodeIndex2 ) {
return nodeIndex1;
}
if ( nodeIndex1 == bAig_Not(nodeIndex2) ) {
return bAig_Zero;
}
/* Look for the new node in the Hash table */
newNodeIndex = PureSat_HashTableLookup(manager, nodeIndex1, nodeIndex2);
if (newNodeIndex == bAig_NULL){
if(!PureSat_Test2LevelMini(manager,nodeIndex1,nodeIndex2)){
newNodeIndex = PureSat_And2(manager, nodeIndex1, nodeIndex2);
return newNodeIndex;
}
if(bAigIsVar(manager, nodeIndex1) && bAigIsVar(manager, nodeIndex2))
newNodeIndex = PureSat_And2(manager, nodeIndex1, nodeIndex2);
else if(bAigIsVar(manager, nodeIndex1))
newNodeIndex = PureSat_And3(manager, nodeIndex1, nodeIndex2);
else if(bAigIsVar(manager, nodeIndex2))
newNodeIndex = PureSat_And3(manager, nodeIndex2, nodeIndex1);
else {
newNodeIndex = PureSat_And4(manager, nodeIndex1, nodeIndex2);
}
}
return newNodeIndex;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| bAigEdge_t PureSat_And2 | ( | bAig_Manager_t * | manager, |
| bAigEdge_t | nodeIndex1, | ||
| bAigEdge_t | nodeIndex2 | ||
| ) |
Function********************************************************************
Synopsis [And function for 2 aig nodes]
Description []
SideEffects []
SeeAlso []
Definition at line 322 of file puresatAig.c.
{
bAigEdge_t newNodeIndex;
newNodeIndex = PureSat_CreateAndNode(manager, nodeIndex1, nodeIndex2) ;
PureSat_HashTableAdd(manager, newNodeIndex, nodeIndex1, nodeIndex2);
PureSat_connectOutput(manager, nodeIndex1, newNodeIndex, 0);
PureSat_connectOutput(manager, nodeIndex2, newNodeIndex, 1);
return newNodeIndex;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| bAigEdge_t PureSat_And3 | ( | bAig_Manager_t * | manager, |
| bAigEdge_t | l, | ||
| bAigEdge_t | r | ||
| ) |
Function********************************************************************
Synopsis [And function for 3 aig nodes]
Description []
SideEffects []
SeeAlso []
Definition at line 353 of file puresatAig.c.
{
int caseIndex, caseSig;
bAigEdge_t rl, rr;
rl = leftChild(r);
rr = rightChild(r);
caseIndex = 0; /* (a)(b c) */
if(bAigCompareNode(l, rl)) {
caseIndex = 1; /* (a)(a b) */
}
else if(bAigCompareNode(l, rr)) {
caseIndex = 2; /* (a)(b a) */
}
caseSig = 0;
if(bAig_IsInverted(l)) caseSig += 8;
if(bAig_IsInverted(rl)) caseSig += 4;
if(bAig_IsInverted(rr)) caseSig += 2;
if(bAig_IsInverted(r)) caseSig += 1;
if(caseIndex == 0) {
return(PureSat_And2(manager, l, r));
}
else if(caseIndex == 1) {
switch(caseSig) {
case 2 :
case 0 :
case 14 :
case 12 :
return(r);
case 10 :
case 8 :
case 6 :
case 4 :
return(bAig_Zero);
case 3 :
case 1 :
case 15 :
case 13 :
return(PureSat_And(manager, rl, bAig_Not(rr)));
case 11 :
case 9 :
case 7 :
case 5 :
return(l);
}
}
else if(caseIndex == 2) {
switch(caseSig) {
case 4 :
case 0 :
case 14 :
case 10 :
return(r);
case 12 :
case 8 :
case 6 :
case 2 :
return(bAig_Zero);
case 5 :
case 1 :
case 15 :
case 11 :
return(PureSat_And(manager, bAig_Not(rl), rr));
case 13 :
case 9 :
case 7 :
case 3 :
return(l);
}
}
return(0);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| bAigEdge_t PureSat_And4 | ( | bAig_Manager_t * | manager, |
| bAigEdge_t | l, | ||
| bAigEdge_t | r | ||
| ) |
Function********************************************************************
Synopsis [And function for 4 aig nodes]
Description []
SideEffects []
SeeAlso []
Definition at line 445 of file puresatAig.c.
{
int caseIndex, caseSig;
bAigEdge_t ll, lr, rl, rr;
bAigEdge_t t1, t2;
ll = leftChild(l);
lr = rightChild(l);
rl = leftChild(r);
rr = rightChild(r);
if(bAigCompareNode(l, rl) ||
bAigCompareNode(l, rr)) {
return(PureSat_And3(manager, l, r));
}
else if(bAigCompareNode(r, ll) ||
bAigCompareNode(r, lr)) {
return(PureSat_And3(manager, r, l));
}
if(ll > lr+1) bAigSwap(ll, lr);
if(rl > rr+1) bAigSwap(rl, rr);
caseIndex = 0; /* (a b)(c d) */
if(bAigCompareNode(ll, rl)) {
if(bAigCompareNode(lr, rr)) {
caseIndex = 4; /* (a b) (a b) */
}
else {
caseIndex = 1; /* (a b) (a c) */
if(lr > rr+1) {
bAigSwap(ll, rl);
bAigSwap(lr, rr);
bAigSwap(l, r);
}
}
}
else if(bAigCompareNode(lr, rl)) {
caseIndex = 2; /* (b a)(a c) */
}
else if(bAigCompareNode(lr, rr)) {
caseIndex = 3; /* (b a)(c a) */
if(ll > rl+1) {
bAigSwap(ll, rl);
bAigSwap(lr, rr);
bAigSwap(l, r);
}
}
else if(bAigCompareNode(ll, rr)) {
/* (a b)(c a) */
bAigSwap(ll, rl);
bAigSwap(lr, rr);
bAigSwap(l, r);
caseIndex = 2; /* (c a )(a b) because of c < b */
}
caseSig = 0;
if(bAig_IsInverted(ll)) caseSig += 32;
if(bAig_IsInverted(lr)) caseSig += 16;
if(bAig_IsInverted(l)) caseSig += 8;
if(bAig_IsInverted(rl)) caseSig += 4;
if(bAig_IsInverted(rr)) caseSig += 2;
if(bAig_IsInverted(r)) caseSig += 1;
if(caseIndex == 0) {
return(PureSat_And2(manager, l, r));
}
else if(caseIndex == 1) {
switch(caseSig) {
case 19 :
case 17 :
case 3 :
case 1 :
case 55 :
case 53 :
case 39 :
case 37 :
t1 = PureSat_And(manager, lr, bAig_Not(rr));
t2 = PureSat_And(manager, ll, t1);
return(t2);
case 18 :
case 16 :
case 2 :
case 0 :
case 54 :
case 52 :
case 38 :
case 36 :
t1 = PureSat_And(manager, lr, rr);
t2 = PureSat_And(manager, ll, t1);
return(t2);
case 26 :
case 24 :
case 10 :
case 8 :
case 62 :
case 60 :
case 46 :
case 44 :
t1 = PureSat_And(manager, bAig_Not(lr), rr);
t2 = PureSat_And(manager, ll, t1);
return(t2);
case 61 :
case 27 :
case 25 :
case 11 :
case 63 :
case 47 :
case 9 :
case 45 :
t1 = PureSat_And(manager, bAig_Not(lr), bAig_Not(rr));
t2 = PureSat_Or(manager, bAig_Not(ll), t1);
return(t2);
case 23 :
case 21 :
case 7 :
case 5 :
case 51 :
case 49 :
case 35 :
case 33 :
return(l);
case 30 :
case 28 :
case 14 :
case 12 :
case 58 :
case 56 :
case 42 :
case 40 :
return(r);
case 22 :
case 20 :
case 6 :
case 4 :
case 50 :
case 48 :
case 34 :
case 32 :
return(bAig_Zero);
case 31 :
case 29 :
case 15 :
case 13 :
case 59 :
case 57 :
case 43 :
case 41 :
t1 = PureSat_And2(manager, l, r);
return(t1);
}
}
else if(caseIndex == 2) {
switch(caseSig) {
case 35 :
case 33 :
case 3 :
case 1 :
case 55 :
case 53 :
case 23 :
case 21 :
t1 = PureSat_And(manager, lr, bAig_Not(rr));
t2 = PureSat_And(manager, ll, t1);
return(t2);
case 34 :
case 32 :
case 2 :
case 0 :
case 54 :
case 52 :
case 22 :
case 20 :
t1 = PureSat_And(manager, lr, rr);
t2 = PureSat_And(manager, ll, t1);
return(t2);
case 42 :
case 40 :
case 10 :
case 8 :
case 62 :
case 60 :
case 30 :
case 28 :
t1 = PureSat_And(manager, lr, rr);
t2 = PureSat_And(manager, bAig_Not(ll), t1);
return(t2);
case 43 :
case 41 :
case 11 :
case 9 :
case 63 :
case 61 :
case 31 :
case 29 :
t1 = PureSat_And(manager, bAig_Not(ll), bAig_Not(rr));
t2 = PureSat_Or(manager, bAig_Not(lr), t1);
return(t2);
case 39 :
case 37 :
case 7 :
case 5 :
case 51 :
case 49 :
case 19 :
case 17 :
return(l);
case 46 :
case 44 :
case 14 :
case 12 :
case 58 :
case 56 :
case 26 :
case 24 :
return(r);
case 38 :
case 36 :
case 6 :
case 4 :
case 50 :
case 48 :
case 18 :
case 16 :
return(bAig_Zero);
case 45 :
case 15 :
case 13 :
case 59 :
case 57 :
case 47 :
case 27 :
case 25 :
t1 = PureSat_And2(manager, l, r);
return(t1);
}
}
else if(caseIndex == 3) {
switch(caseSig) {
case 37 :
case 33 :
case 5 :
case 1 :
case 55 :
case 51 :
case 23 :
case 19 :
t1 = PureSat_And(manager, bAig_Not(rl), lr);
t2 = PureSat_And(manager, ll, t1);
return(t2);
case 36 :
case 32 :
case 4 :
case 0 :
case 54 :
case 50 :
case 22 :
case 18 :
t1 = PureSat_And(manager, rl, lr);
t2 = PureSat_And(manager, ll, t1);
return(t2);
case 44 :
case 40 :
case 12 :
case 8 :
case 62 :
case 58 :
case 30 :
case 26 :
t1 = PureSat_And(manager, rl, lr);
t2 = PureSat_And(manager, bAig_Not(ll), t1);
return(t2);
case 45 :
case 41 :
case 13 :
case 9 :
case 63 :
case 59 :
case 31 :
case 27 :
t1 = PureSat_And(manager, bAig_Not(ll), bAig_Not(rl));
t2 = PureSat_Or(manager, bAig_Not(lr), t1);
return(t2);
case 39 :
case 35 :
case 7 :
case 3 :
case 53 :
case 49 :
case 21 :
case 17 :
return(l);
case 46 :
case 42 :
case 14 :
case 10 :
case 60 :
case 56 :
case 28 :
case 24 :
return(r);
case 38 :
case 34 :
case 6 :
case 2 :
case 52 :
case 48 :
case 20 :
case 16 :
return(bAig_Zero);
case 47 :
case 43 :
case 15 :
case 11 :
case 61 :
case 57 :
case 29 :
case 25 :
t1 = PureSat_And2(manager, l, r);
return(t1);
}
}
else if(caseIndex == 4) {
switch(caseSig) {
case 22 :
case 20 :
case 6 :
case 4 :
case 50 :
case 48 :
case 34 :
case 32 :
case 2 :
case 16 :
case 52 :
case 1 :
case 8 :
case 19 :
case 26 :
case 37 :
case 44 :
case 38 :
case 55 :
case 62 :
return(bAig_Zero);
case 0 :
case 18 :
case 36 :
case 54 :
case 9 :
case 27 :
case 45 :
case 63 :
case 5 :
case 23 :
case 33 :
case 51 :
case 3 :
case 17 :
case 49 :
case 7 :
case 35 :
case 21 :
case 39 :
case 53 :
return(l);
case 40 :
case 58 :
case 12 :
case 30 :
case 24 :
case 10 :
case 14 :
case 56 :
case 28 :
case 42 :
case 60 :
case 46 :
return(r);
case 11 :
case 47 :
case 25 :
case 61 :
return(bAig_Not(ll));
case 41 :
case 59 :
case 13 :
case 31 :
return(bAig_Not(lr));
case 15 :
t1 = PureSat_And(manager, ll, bAig_Not(lr));
t2 = PureSat_And(manager, bAig_Not(ll), lr);
return(bAig_Not(PureSat_And2(manager, bAig_Not(t1), bAig_Not(t2))));
case 57 :
t1 = PureSat_And(manager, rl, bAig_Not(rr));
t2 = PureSat_And(manager, bAig_Not(rl), rr);
return(bAig_Not(PureSat_And2(manager, bAig_Not(t1), bAig_Not(t2))));
case 29 :
t1 = PureSat_And(manager, ll, lr);
t2 = PureSat_And(manager, bAig_Not(ll), bAig_Not(lr));
return((PureSat_And2(manager, bAig_Not(t1), bAig_Not(t2))));
case 43 :
t1 = PureSat_And(manager, rl, rr);
t2 = PureSat_And(manager, bAig_Not(rl), bAig_Not(rr));
return((PureSat_And2(manager, bAig_Not(t1), bAig_Not(t2))));
}
}
return(0);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void PureSat_connectOutput | ( | bAig_Manager_t * | manager, |
| bAigEdge_t | from, | ||
| bAigEdge_t | to, | ||
| int | inputIndex | ||
| ) |
Function********************************************************************
Synopsis [for AIG generation---create connection between new and old aig nodes]
Description []
SideEffects []
SeeAlso []
Definition at line 155 of file puresatAig.c.
{
bAigEdge_t *pfan;
bAigEdge_t nfan;
to = bAig_NonInvertedEdge(to);
pfan = (bAigEdge_t *)fanout(from);
nfan = nFanout(from);
if(nfan == 0) pfan = malloc((sizeof(bAigEdge_t)*2));
else pfan = realloc(pfan, sizeof(bAigEdge_t)*(nfan+2));
to += bAig_IsInverted(from);
to = to << 1;
to += inputIndex;
pfan[nfan++] = to;
pfan[nfan] = 0;
fanout(from) = (bAigEdge_t)pfan;
nFanout(from) = nfan;
}
Here is the caller graph for this function:
| bAigEdge_t PureSat_CreateAndNode | ( | bAig_Manager_t * | manager, |
| bAigEdge_t | node1, | ||
| bAigEdge_t | node2 | ||
| ) |
Function********************************************************************
Synopsis [Create a node for AND operation]
Description []
SideEffects []
SeeAlso []
Definition at line 276 of file puresatAig.c.
{
bAigEdge_t varIndex;
char *name = NIL(char);
char *node1Str = util_inttostr(node1);
char *node2Str = util_inttostr(node2);
long class_ = manager->class_;
name = util_strcat4("Nd", node1Str,"_", node2Str);
while (st_lookup(manager->SymbolTableArray[class_], name, &varIndex)){
fprintf(vis_stdout, "Find redundant node at %ld %ld\n", node1, node2);
name = util_strcat3(name, node1Str, node2Str);
}
FREE(node1Str);
FREE(node2Str);
varIndex = bAig_CreateNode(manager, node1, node2);
if (varIndex == bAig_NULL){
FREE(name);
return (varIndex);
}
/* Insert the varaible in the Symbol Table */
st_insert(manager->SymbolTableArray[class_], name, (char*) (long) varIndex);
manager->nameList[bAigNodeID(varIndex)] = name;
return(varIndex);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| bAigEdge_t PureSat_CreateVarNode | ( | bAig_Manager_t * | manager, |
| nameType_t * | name | ||
| ) |
Function********************************************************************
Synopsis [Create variable AIG nodes]
Description []
SideEffects []
SeeAlso []
Definition at line 1092 of file puresatAig.c.
{
bAigEdge_t varIndex;
int class_ = manager->class_;
if (!st_lookup(manager->SymbolTableArray[class_], name, &varIndex)){
varIndex = bAig_CreateNode(manager, bAig_NULL, bAig_NULL);
if (varIndex == bAig_NULL){
return (varIndex);
}
/* Insert the varaible in the Symbol Table */
st_insert(manager->SymbolTableArray[class_],
name, (char*) (long) varIndex);
manager->nameList[bAigNodeID(varIndex)] = name;
return(varIndex);
}
else {
return (varIndex);
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| bAigEdge_t PureSat_Eq | ( | bAig_Manager_t * | manager, |
| bAigEdge_t | nodeIndex1, | ||
| bAigEdge_t | nodeIndex2 | ||
| ) |
Function********************************************************************
Synopsis [EQ operation for two aig nodes]
Description []
SideEffects []
SeeAlso []
Definition at line 1042 of file puresatAig.c.
{
return bAig_Not(
PureSat_Xor(manager, nodeIndex1, nodeIndex2)
);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| int PureSat_HashTableAdd | ( | bAig_Manager_t * | manager, |
| bAigEdge_t | nodeIndexParent, | ||
| bAigEdge_t | nodeIndex1, | ||
| bAigEdge_t | nodeIndex2 | ||
| ) |
Function********************************************************************
Synopsis [Add one new node to hash table]
Description []
SideEffects []
SeeAlso []
Definition at line 233 of file puresatAig.c.
{
bAigEdge_t key = HashTableFunction(nodeIndex1, nodeIndex2);
bAigEdge_t nodeIndex;
bAigEdge_t node;
nodeIndex = manager->HashTableArray[manager->class_][key];
if (nodeIndex == bAig_NULL) {
manager->HashTableArray[manager->class_][key] = nodeIndexParent;
return TRUE;
}
else{
node = nodeIndex;
nodeIndex = next(bAig_NonInvertedEdge(nodeIndex)); /* Get the Node */
while (nodeIndex != bAig_NULL) {
node = nodeIndex;
nodeIndex = next(bAig_NonInvertedEdge(nodeIndex));
}
next(bAig_NonInvertedEdge(node)) = nodeIndexParent;
return TRUE;
}
}
Here is the caller graph for this function:
| bAigEdge_t PureSat_HashTableLookup | ( | bAig_Manager_t * | manager, |
| bAigEdge_t | node1, | ||
| bAigEdge_t | node2 | ||
| ) |
Function********************************************************************
Synopsis [Check whether a node has been created or not]
Description []
SideEffects []
SeeAlso []
Definition at line 192 of file puresatAig.c.
{
bAigEdge_t key = HashTableFunction(node1, node2);
bAigEdge_t node;
node = manager->HashTableArray[manager->class_][key];
if (node == bAig_NULL) {
return bAig_NULL;
}
else{
while ( (rightChild(bAig_NonInvertedEdge(node)) != node2) ||
(leftChild(bAig_NonInvertedEdge(node)) != node1)) {
if (next(bAig_NonInvertedEdge(node)) == bAig_NULL){
return(bAig_NULL);
}
node = next(bAig_NonInvertedEdge(node)); /* Get the next Node */
} /* While loop */
return(node);
} /* If Then Else */
} /* End of HashTableLookup() */
Here is the caller graph for this function:
| bAigEdge_t PureSat_Or | ( | bAig_Manager_t * | manager, |
| bAigEdge_t | nodeIndex1, | ||
| bAigEdge_t | nodeIndex2 | ||
| ) |
Function********************************************************************
Synopsis [OR operation for two aig nodes]
Description []
SideEffects []
SeeAlso []
Definition at line 995 of file puresatAig.c.
{
return ( bAig_Not(PureSat_And(manager, bAig_Not(nodeIndex1), bAig_Not(nodeIndex2))));
}
Here is the call graph for this function:
Here is the caller graph for this function:
| int PureSat_Test2LevelMini | ( | bAig_Manager_t * | manager, |
| bAigEdge_t | l, | ||
| bAigEdge_t | r | ||
| ) |
Function********************************************************************
Synopsis [test whether two level minimization can be enabled--iff the two nodes are in the same timeframe]
Description [output, l,r,ll,lr,rl,rr must be in the same class to pass the test]
SideEffects []
SeeAlso []
Definition at line 874 of file puresatAig.c.
{
int class_ = bAig_Class(l);
bAigEdge_t ll,lr,rl,rr;
if(!manager->test2LevelMini)
return 0;
if(class_!= bAig_Class(r) || class_ != manager->class_)
return 0;
ll = leftChild(l);
if(ll!=bAig_NULL && class_!=bAig_Class(ll))
return 0;
lr = rightChild(l);
if(lr!=bAig_NULL && class_!=bAig_Class(lr))
return 0;
rl = leftChild(r);
if(rl!=bAig_NULL && class_!=bAig_Class(rl))
return 0;
rr = rightChild(r);
if(rr!=bAig_NULL && class_!=bAig_Class(rr))
return 0;
return 1;
}
Here is the caller graph for this function:
| bAigEdge_t PureSat_Then | ( | bAig_Manager_t * | manager, |
| bAigEdge_t | nodeIndex1, | ||
| bAigEdge_t | nodeIndex2 | ||
| ) |
Function********************************************************************
Synopsis [THEN operation for two aig nodes]
Description []
SideEffects []
SeeAlso []
Definition at line 1066 of file puresatAig.c.
{
return PureSat_Or(manager,
bAig_Not(nodeIndex1),
nodeIndex2);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void PureSat_unconnectOutput | ( | bAig_Manager_t * | manager, |
| bAigEdge_t | from, | ||
| bAigEdge_t | to | ||
| ) |
CFile***********************************************************************
FileName [puresatAig.c]
PackageName [puresat]
Synopsis [Abstraction refinement for large scale invariant checking.]
Description [This file contains the functions to check invariant properties by the PureSAT abstraction refinement algorithm, which is entirely based on SAT solver, the input of which could be either CNF or AIG. It has several parts:
Localization-reduction base Abstraction K-induction or interpolation to prove the truth of a property Bounded Model Checking to find bugs Incremental concretization based methods to verify abstract bugs Incremental SAT solver to improve efficiency UNSAT proof based method to obtain refinement AROSAT to bring in only necessary latches into unsat proofs Bridge abstraction to get compact coarse refinement Refinement minization to guarrantee minimal refinements Unsat proof-based refinement minimization to eliminate multiple candidate by on SAT test Refinement prediction to decrease the number of refinement iterations Dynamic switching to redistribute computional resources to improve efficiency
For more information, please check the BMC'03, ICCAD'04, STTT'05 and TACAS'05 paper of Li et al., "A satisfiability-based appraoch to abstraction refinement in model checking", " Abstraction in symbolic model checking using satisfiability as the only decision procedure", "Efficient computation of small abstraction refinements", and "Efficient abstraction refinement in interpolation-based unbounded model checking"]
Author [Bing Li]
Copyright [Copyright (c) 2004 The Regents of the Univ. of Colorado. All rights reserved.
Permission is hereby granted, without written agreement and without license or royalty fees, to use, copy, modify, and distribute this software and its documentation for any purpose, provided that the above copyright notice and the following two paragraphs appear in all copies of this software.]AutomaticStart AutomaticEnd Function********************************************************************
Synopsis [For AIG recovery--unconnect output for nodes eliminated]
Description [For AIG recovery--unconnect output for nodes eliminated]
SideEffects []
SeeAlso []
Definition at line 105 of file puresatAig.c.
{
bAigEdge_t cur, *pfan, *newfan;
int i, nfan,find=0;
from = bAig_NonInvertedEdge(from);
to = bAig_NonInvertedEdge(to);
pfan = (bAigEdge_t *)fanout(from);
nfan = nFanout(from);
newfan = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*(nfan));
for(i=0; i<nfan; i++) {
cur = pfan[i];
cur = cur >> 1;
cur = bAig_NonInvertedEdge(cur);
if(cur == to) {
find = 1;
memcpy(newfan, pfan, sizeof(bAigEdge_t)*i);
memcpy(&(newfan[i]), &(pfan[i+1]), sizeof(bAigEdge_t)*(nfan-i-1));
newfan[nfan-1] = 0;
fanout(from) = (bAigEdge_t)newfan;
free(pfan);
nFanout(from) = nfan-1;
break;
}
}
assert(find);
}
| bAigEdge_t PureSat_Xor | ( | bAig_Manager_t * | manager, |
| bAigEdge_t | nodeIndex1, | ||
| bAigEdge_t | nodeIndex2 | ||
| ) |
Function********************************************************************
Synopsis [XOR operation for two aig nodes]
Description []
SideEffects []
SeeAlso []
Definition at line 1017 of file puresatAig.c.
{
return PureSat_Or(manager,
PureSat_And(manager, nodeIndex1, bAig_Not(nodeIndex2)),
PureSat_And(manager, bAig_Not(nodeIndex1),nodeIndex2)
);
}
Here is the call graph for this function:
Here is the caller graph for this function:
