luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity
abc/src/base/abci/abcSat.c

1013 lines
32 KiB
C
Raw Blame History

/**CFile****************************************************************
FileName [abcSat.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Network and node package.]
Synopsis [Procedures to solve the miter using the internal SAT sat_solver.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: abcSat.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "base/abc/abc.h"
#include "base/main/main.h"
#include "base/cmd/cmd.h"
#include "sat/bsat/satSolver.h"
#include "misc/extra/extraBdd.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static sat_solver * Abc_NtkMiterSatCreateLogic( Abc_Ntk_t * pNtk, int fAllPrimes );
extern Vec_Int_t * Abc_NtkGetCiSatVarNums( Abc_Ntk_t * pNtk );
static int nMuxes;
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Attempts to solve the miter using an internal SAT sat_solver.]
Description [Returns -1 if timed out; 0 if SAT; 1 if UNSAT.]
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fVerbose, ABC_INT64_T * pNumConfs, ABC_INT64_T * pNumInspects )
{
sat_solver * pSat;
lbool status;
int RetValue;
abctime clk;
if ( pNumConfs )
*pNumConfs = 0;
if ( pNumInspects )
*pNumInspects = 0;
assert( Abc_NtkLatchNum(pNtk) == 0 );
// if ( Abc_NtkPoNum(pNtk) > 1 )
// fprintf( stdout, "Warning: The miter has %d outputs. SAT will try to prove all of them.\n", Abc_NtkPoNum(pNtk) );
// load clauses into the sat_solver
clk = Abc_Clock();
pSat = (sat_solver *)Abc_NtkMiterSatCreate( pNtk, 0 );
if ( pSat == NULL )
return 1;
//printf( "%d \n", pSat->clauses.size );
//sat_solver_delete( pSat );
//return 1;
// printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
// ABC_PRT( "Time", Abc_Clock() - clk );
// simplify the problem
clk = Abc_Clock();
status = sat_solver_simplify(pSat);
// printf( "Simplified the problem to %d variables and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
// ABC_PRT( "Time", Abc_Clock() - clk );
if ( status == 0 )
{
sat_solver_delete( pSat );
// printf( "The problem is UNSATISFIABLE after simplification.\n" );
return 1;
}
// solve the miter
clk = Abc_Clock();
if ( fVerbose )
pSat->verbosity = 1;
status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, (ABC_INT64_T)0, (ABC_INT64_T)0 );
if ( status == l_Undef )
{
// printf( "The problem timed out.\n" );
RetValue = -1;
}
else if ( status == l_True )
{
// printf( "The problem is SATISFIABLE.\n" );
RetValue = 0;
}
else if ( status == l_False )
{
// printf( "The problem is UNSATISFIABLE.\n" );
RetValue = 1;
}
else
assert( 0 );
// ABC_PRT( "SAT sat_solver time", Abc_Clock() - clk );
// printf( "The number of conflicts = %d.\n", (int)pSat->sat_solver_stats.conflicts );
// if the problem is SAT, get the counterexample
if ( status == l_True )
{
// Vec_Int_t * vCiIds = Abc_NtkGetCiIds( pNtk );
Vec_Int_t * vCiIds = Abc_NtkGetCiSatVarNums( pNtk );
pNtk->pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize );
Vec_IntFree( vCiIds );
}
// free the sat_solver
if ( fVerbose )
Sat_SolverPrintStats( stdout, pSat );
if ( pNumConfs )
*pNumConfs = (int)pSat->stats.conflicts;
if ( pNumInspects )
*pNumInspects = (int)pSat->stats.inspects;
sat_solver_store_write( pSat, "trace.cnf" );
sat_solver_store_free( pSat );
sat_solver_delete( pSat );
return RetValue;
}
/**Function*************************************************************
Synopsis [Returns the array of CI IDs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Abc_NtkGetCiSatVarNums( Abc_Ntk_t * pNtk )
{
Vec_Int_t * vCiIds;
Abc_Obj_t * pObj;
int i;
vCiIds = Vec_IntAlloc( Abc_NtkCiNum(pNtk) );
Abc_NtkForEachCi( pNtk, pObj, i )
Vec_IntPush( vCiIds, (int)(ABC_PTRINT_T)pObj->pCopy );
return vCiIds;
}
/**Function*************************************************************
Synopsis [Adds trivial clause.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NtkClauseTriv( sat_solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars )
{
//printf( "Adding triv %d. %d\n", Abc_ObjRegular(pNode)->Id, (int)pSat->sat_solver_stats.clauses );
vVars->nSize = 0;
Vec_IntPush( vVars, toLitCond( (int)(ABC_PTRINT_T)Abc_ObjRegular(pNode)->pCopy, Abc_ObjIsComplement(pNode) ) );
// Vec_IntPush( vVars, toLitCond( (int)Abc_ObjRegular(pNode)->Id, Abc_ObjIsComplement(pNode) ) );
return sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
}
/**Function*************************************************************
Synopsis [Adds trivial clause.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NtkClauseTop( sat_solver * pSat, Vec_Ptr_t * vNodes, Vec_Int_t * vVars )
{
Abc_Obj_t * pNode;
int i;
//printf( "Adding triv %d. %d\n", Abc_ObjRegular(pNode)->Id, (int)pSat->sat_solver_stats.clauses );
vVars->nSize = 0;
Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
Vec_IntPush( vVars, toLitCond( (int)(ABC_PTRINT_T)Abc_ObjRegular(pNode)->pCopy, Abc_ObjIsComplement(pNode) ) );
// Vec_IntPush( vVars, toLitCond( (int)Abc_ObjRegular(pNode)->Id, Abc_ObjIsComplement(pNode) ) );
return sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
}
/**Function*************************************************************
Synopsis [Adds trivial clause.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NtkClauseAnd( sat_solver * pSat, Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, Vec_Int_t * vVars )
{
int fComp1, Var, Var1, i;
//printf( "Adding AND %d. (%d) %d\n", pNode->Id, vSuper->nSize+1, (int)pSat->sat_solver_stats.clauses );
assert( !Abc_ObjIsComplement( pNode ) );
assert( Abc_ObjIsNode( pNode ) );
// nVars = sat_solver_nvars(pSat);
Var = (int)(ABC_PTRINT_T)pNode->pCopy;
// Var = pNode->Id;
// assert( Var < nVars );
for ( i = 0; i < vSuper->nSize; i++ )
{
// get the predecessor nodes
// get the complemented attributes of the nodes
fComp1 = Abc_ObjIsComplement((Abc_Obj_t *)vSuper->pArray[i]);
// determine the variable numbers
Var1 = (int)(ABC_PTRINT_T)Abc_ObjRegular((Abc_Obj_t *)vSuper->pArray[i])->pCopy;
// Var1 = (int)Abc_ObjRegular(vSuper->pArray[i])->Id;
// check that the variables are in the SAT manager
// assert( Var1 < nVars );
// suppose the AND-gate is A * B = C
// add !A => !C or A + !C
// fprintf( pFile, "%d %d 0%c", Var1, -Var, 10 );
vVars->nSize = 0;
Vec_IntPush( vVars, toLitCond(Var1, fComp1) );
Vec_IntPush( vVars, toLitCond(Var, 1 ) );
if ( !sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
return 0;
}
// add A & B => C or !A + !B + C
// fprintf( pFile, "%d %d %d 0%c", -Var1, -Var2, Var, 10 );
vVars->nSize = 0;
for ( i = 0; i < vSuper->nSize; i++ )
{
// get the predecessor nodes
// get the complemented attributes of the nodes
fComp1 = Abc_ObjIsComplement((Abc_Obj_t *)vSuper->pArray[i]);
// determine the variable numbers
Var1 = (int)(ABC_PTRINT_T)Abc_ObjRegular((Abc_Obj_t *)vSuper->pArray[i])->pCopy;
// Var1 = (int)Abc_ObjRegular(vSuper->pArray[i])->Id;
// add this variable to the array
Vec_IntPush( vVars, toLitCond(Var1, !fComp1) );
}
Vec_IntPush( vVars, toLitCond(Var, 0) );
return sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
}
/**Function*************************************************************
Synopsis [Adds trivial clause.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NtkClauseMux( sat_solver * pSat, Abc_Obj_t * pNode, Abc_Obj_t * pNodeC, Abc_Obj_t * pNodeT, Abc_Obj_t * pNodeE, Vec_Int_t * vVars )
{
int VarF, VarI, VarT, VarE, fCompT, fCompE;
//printf( "Adding mux %d. %d\n", pNode->Id, (int)pSat->sat_solver_stats.clauses );
assert( !Abc_ObjIsComplement( pNode ) );
assert( Abc_NodeIsMuxType( pNode ) );
// get the variable numbers
VarF = (int)(ABC_PTRINT_T)pNode->pCopy;
VarI = (int)(ABC_PTRINT_T)pNodeC->pCopy;
VarT = (int)(ABC_PTRINT_T)Abc_ObjRegular(pNodeT)->pCopy;
VarE = (int)(ABC_PTRINT_T)Abc_ObjRegular(pNodeE)->pCopy;
// VarF = (int)pNode->Id;
// VarI = (int)pNodeC->Id;
// VarT = (int)Abc_ObjRegular(pNodeT)->Id;
// VarE = (int)Abc_ObjRegular(pNodeE)->Id;
// get the complementation flags
fCompT = Abc_ObjIsComplement(pNodeT);
fCompE = Abc_ObjIsComplement(pNodeE);
// f = ITE(i, t, e)
// i' + t' + f
// i' + t + f'
// i + e' + f
// i + e + f'
// create four clauses
vVars->nSize = 0;
Vec_IntPush( vVars, toLitCond(VarI, 1) );
Vec_IntPush( vVars, toLitCond(VarT, 1^fCompT) );
Vec_IntPush( vVars, toLitCond(VarF, 0) );
if ( !sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
return 0;
vVars->nSize = 0;
Vec_IntPush( vVars, toLitCond(VarI, 1) );
Vec_IntPush( vVars, toLitCond(VarT, 0^fCompT) );
Vec_IntPush( vVars, toLitCond(VarF, 1) );
if ( !sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
return 0;
vVars->nSize = 0;
Vec_IntPush( vVars, toLitCond(VarI, 0) );
Vec_IntPush( vVars, toLitCond(VarE, 1^fCompE) );
Vec_IntPush( vVars, toLitCond(VarF, 0) );
if ( !sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
return 0;
vVars->nSize = 0;
Vec_IntPush( vVars, toLitCond(VarI, 0) );
Vec_IntPush( vVars, toLitCond(VarE, 0^fCompE) );
Vec_IntPush( vVars, toLitCond(VarF, 1) );
if ( !sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
return 0;
if ( VarT == VarE )
{
// assert( fCompT == !fCompE );
return 1;
}
// two additional clauses
// t' & e' -> f' t + e + f'
// t & e -> f t' + e' + f
vVars->nSize = 0;
Vec_IntPush( vVars, toLitCond(VarT, 0^fCompT) );
Vec_IntPush( vVars, toLitCond(VarE, 0^fCompE) );
Vec_IntPush( vVars, toLitCond(VarF, 1) );
if ( !sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
return 0;
vVars->nSize = 0;
Vec_IntPush( vVars, toLitCond(VarT, 1^fCompT) );
Vec_IntPush( vVars, toLitCond(VarE, 1^fCompE) );
Vec_IntPush( vVars, toLitCond(VarF, 0) );
return sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
}
/**Function*************************************************************
Synopsis [Returns the array of nodes to be combined into one multi-input AND-gate.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NtkCollectSupergate_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, int fFirst, int fStopAtMux )
{
int RetValue1, RetValue2, i;
// check if the node is visited
if ( Abc_ObjRegular(pNode)->fMarkB )
{
// check if the node occurs in the same polarity
for ( i = 0; i < vSuper->nSize; i++ )
if ( vSuper->pArray[i] == pNode )
return 1;
// check if the node is present in the opposite polarity
for ( i = 0; i < vSuper->nSize; i++ )
if ( vSuper->pArray[i] == Abc_ObjNot(pNode) )
return -1;
assert( 0 );
return 0;
}
// if the new node is complemented or a PI, another gate begins
if ( !fFirst )
if ( Abc_ObjIsComplement(pNode) || !Abc_ObjIsNode(pNode) || Abc_ObjFanoutNum(pNode) > 1 || (fStopAtMux && Abc_NodeIsMuxType(pNode)) )
{
Vec_PtrPush( vSuper, pNode );
Abc_ObjRegular(pNode)->fMarkB = 1;
return 0;
}
assert( !Abc_ObjIsComplement(pNode) );
assert( Abc_ObjIsNode(pNode) );
// go through the branches
RetValue1 = Abc_NtkCollectSupergate_rec( Abc_ObjChild0(pNode), vSuper, 0, fStopAtMux );
RetValue2 = Abc_NtkCollectSupergate_rec( Abc_ObjChild1(pNode), vSuper, 0, fStopAtMux );
if ( RetValue1 == -1 || RetValue2 == -1 )
return -1;
// return 1 if at least one branch has a duplicate
return RetValue1 || RetValue2;
}
/**Function*************************************************************
Synopsis [Returns the array of nodes to be combined into one multi-input AND-gate.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkCollectSupergate( Abc_Obj_t * pNode, int fStopAtMux, Vec_Ptr_t * vNodes )
{
int RetValue, i;
assert( !Abc_ObjIsComplement(pNode) );
// collect the nodes in the implication supergate
Vec_PtrClear( vNodes );
RetValue = Abc_NtkCollectSupergate_rec( pNode, vNodes, 1, fStopAtMux );
assert( vNodes->nSize > 1 );
// unmark the visited nodes
for ( i = 0; i < vNodes->nSize; i++ )
Abc_ObjRegular((Abc_Obj_t *)vNodes->pArray[i])->fMarkB = 0;
// if we found the node and its complement in the same implication supergate,
// return empty set of nodes (meaning that we should use constant-0 node)
if ( RetValue == -1 )
vNodes->nSize = 0;
}
/**Function*************************************************************
Synopsis [Computes the factor of the node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NtkNodeFactor( Abc_Obj_t * pObj, int nLevelMax )
{
// nLevelMax = ((nLevelMax)/2)*3;
assert( (int)pObj->Level <= nLevelMax );
// return (int)(100000000.0 * pow(0.999, nLevelMax - pObj->Level));
return (int)(100000000.0 * (1 + 0.01 * pObj->Level));
// return (int)(100000000.0 / ((nLevelMax)/2)*3 - pObj->Level);
}
/**Function*************************************************************
Synopsis [Sets up the SAT sat_solver.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NtkMiterSatCreateInt( sat_solver * pSat, Abc_Ntk_t * pNtk )
{
Abc_Obj_t * pNode, * pFanin, * pNodeC, * pNodeT, * pNodeE;
Vec_Ptr_t * vNodes, * vSuper;
Vec_Int_t * vVars;
int i, k, fUseMuxes = 1;
// int fOrderCiVarsFirst = 0;
int RetValue = 0;
assert( Abc_NtkIsStrash(pNtk) );
// clean the CI node pointers
Abc_NtkForEachCi( pNtk, pNode, i )
pNode->pCopy = NULL;
// start the data structures
vNodes = Vec_PtrAlloc( 1000 ); // the nodes corresponding to vars in the sat_solver
vSuper = Vec_PtrAlloc( 100 ); // the nodes belonging to the given implication supergate
vVars = Vec_IntAlloc( 100 ); // the temporary array for variables in the clause
// add the clause for the constant node
pNode = Abc_AigConst1(pNtk);
pNode->fMarkA = 1;
pNode->pCopy = (Abc_Obj_t *)(ABC_PTRINT_T)vNodes->nSize;
Vec_PtrPush( vNodes, pNode );
Abc_NtkClauseTriv( pSat, pNode, vVars );
/*
// add the PI variables first
Abc_NtkForEachCi( pNtk, pNode, i )
{
pNode->fMarkA = 1;
pNode->pCopy = (Abc_Obj_t *)vNodes->nSize;
Vec_PtrPush( vNodes, pNode );
}
*/
// collect the nodes that need clauses and top-level assignments
Vec_PtrClear( vSuper );
Abc_NtkForEachCo( pNtk, pNode, i )
{
// get the fanin
pFanin = Abc_ObjFanin0(pNode);
// create the node's variable
if ( pFanin->fMarkA == 0 )
{
pFanin->fMarkA = 1;
pFanin->pCopy = (Abc_Obj_t *)(ABC_PTRINT_T)vNodes->nSize;
Vec_PtrPush( vNodes, pFanin );
}
// add the trivial clause
Vec_PtrPush( vSuper, Abc_ObjChild0(pNode) );
}
if ( !Abc_NtkClauseTop( pSat, vSuper, vVars ) )
goto Quits;
// add the clauses
Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
{
assert( !Abc_ObjIsComplement(pNode) );
if ( !Abc_AigNodeIsAnd(pNode) )
continue;
//printf( "%d ", pNode->Id );
// add the clauses
if ( fUseMuxes && Abc_NodeIsMuxType(pNode) )
{
nMuxes++;
pNodeC = Abc_NodeRecognizeMux( pNode, &pNodeT, &pNodeE );
Vec_PtrClear( vSuper );
Vec_PtrPush( vSuper, pNodeC );
Vec_PtrPush( vSuper, pNodeT );
Vec_PtrPush( vSuper, pNodeE );
// add the fanin nodes to explore
Vec_PtrForEachEntry( Abc_Obj_t *, vSuper, pFanin, k )
{
pFanin = Abc_ObjRegular(pFanin);
if ( pFanin->fMarkA == 0 )
{
pFanin->fMarkA = 1;
pFanin->pCopy = (Abc_Obj_t *)(ABC_PTRINT_T)vNodes->nSize;
Vec_PtrPush( vNodes, pFanin );
}
}
// add the clauses
if ( !Abc_NtkClauseMux( pSat, pNode, pNodeC, pNodeT, pNodeE, vVars ) )
goto Quits;
}
else
{
// get the supergate
Abc_NtkCollectSupergate( pNode, fUseMuxes, vSuper );
// add the fanin nodes to explore
Vec_PtrForEachEntry( Abc_Obj_t *, vSuper, pFanin, k )
{
pFanin = Abc_ObjRegular(pFanin);
if ( pFanin->fMarkA == 0 )
{
pFanin->fMarkA = 1;
pFanin->pCopy = (Abc_Obj_t *)(ABC_PTRINT_T)vNodes->nSize;
Vec_PtrPush( vNodes, pFanin );
}
}
// add the clauses
if ( vSuper->nSize == 0 )
{
if ( !Abc_NtkClauseTriv( pSat, Abc_ObjNot(pNode), vVars ) )
// if ( !Abc_NtkClauseTriv( pSat, pNode, vVars ) )
goto Quits;
}
else
{
if ( !Abc_NtkClauseAnd( pSat, pNode, vSuper, vVars ) )
goto Quits;
}
}
}
/*
// set preferred variables
if ( fOrderCiVarsFirst )
{
int * pPrefVars = ABC_ALLOC( int, Abc_NtkCiNum(pNtk) );
int nVars = 0;
Abc_NtkForEachCi( pNtk, pNode, i )
{
if ( pNode->fMarkA == 0 )
continue;
pPrefVars[nVars++] = (int)pNode->pCopy;
}
nVars = Abc_MinInt( nVars, 10 );
ASat_SolverSetPrefVars( pSat, pPrefVars, nVars );
}
*/
/*
Abc_NtkForEachObj( pNtk, pNode, i )
{
if ( !pNode->fMarkA )
continue;
printf( "%10s : ", Abc_ObjName(pNode) );
printf( "%3d\n", (int)pNode->pCopy );
}
printf( "\n" );
*/
RetValue = 1;
Quits :
// delete
Vec_IntFree( vVars );
Vec_PtrFree( vNodes );
Vec_PtrFree( vSuper );
return RetValue;
}
/**Function*************************************************************
Synopsis [Sets up the SAT sat_solver.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk, int fAllPrimes )
{
sat_solver * pSat;
Abc_Obj_t * pNode;
int RetValue, i; //, clk = Abc_Clock();
assert( Abc_NtkIsStrash(pNtk) || Abc_NtkIsBddLogic(pNtk) );
if ( Abc_NtkIsBddLogic(pNtk) )
return Abc_NtkMiterSatCreateLogic(pNtk, fAllPrimes);
nMuxes = 0;
pSat = sat_solver_new();
//sat_solver_store_alloc( pSat );
RetValue = Abc_NtkMiterSatCreateInt( pSat, pNtk );
sat_solver_store_mark_roots( pSat );
Abc_NtkForEachObj( pNtk, pNode, i )
pNode->fMarkA = 0;
// ASat_SolverWriteDimacs( pSat, "temp_sat.cnf", NULL, NULL, 1 );
if ( RetValue == 0 )
{
sat_solver_delete(pSat);
return NULL;
}
// printf( "Ands = %6d. Muxes = %6d (%5.2f %%). ", Abc_NtkNodeNum(pNtk), nMuxes, 300.0*nMuxes/Abc_NtkNodeNum(pNtk) );
// ABC_PRT( "Creating sat_solver", Abc_Clock() - clk );
return pSat;
}
/**Function*************************************************************
Synopsis [Adds clauses for the internal node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NodeAddClauses( sat_solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * pNode, Vec_Int_t * vVars )
{
Abc_Obj_t * pFanin;
int i, c, nFanins;
int RetValue;
char * pCube;
nFanins = Abc_ObjFaninNum( pNode );
assert( nFanins == Abc_SopGetVarNum( pSop0 ) );
// if ( nFanins == 0 )
if ( Cudd_Regular((Abc_Obj_t *)pNode->pData) == Cudd_ReadOne((DdManager *)pNode->pNtk->pManFunc) )
{
vVars->nSize = 0;
// if ( Abc_SopIsConst1(pSop1) )
if ( !Cudd_IsComplement(pNode->pData) )
Vec_IntPush( vVars, toLit(pNode->Id) );
else
Vec_IntPush( vVars, lit_neg(toLit(pNode->Id)) );
RetValue = sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
if ( !RetValue )
{
printf( "The CNF is trivially UNSAT.\n" );
return 0;
}
return 1;
}
// add clauses for the negative phase
for ( c = 0; ; c++ )
{
// get the cube
pCube = pSop0 + c * (nFanins + 3);
if ( *pCube == 0 )
break;
// add the clause
vVars->nSize = 0;
Abc_ObjForEachFanin( pNode, pFanin, i )
{
if ( pCube[i] == '0' )
Vec_IntPush( vVars, toLit(pFanin->Id) );
else if ( pCube[i] == '1' )
Vec_IntPush( vVars, lit_neg(toLit(pFanin->Id)) );
}
Vec_IntPush( vVars, lit_neg(toLit(pNode->Id)) );
RetValue = sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
if ( !RetValue )
{
printf( "The CNF is trivially UNSAT.\n" );
return 0;
}
}
// add clauses for the positive phase
for ( c = 0; ; c++ )
{
// get the cube
pCube = pSop1 + c * (nFanins + 3);
if ( *pCube == 0 )
break;
// add the clause
vVars->nSize = 0;
Abc_ObjForEachFanin( pNode, pFanin, i )
{
if ( pCube[i] == '0' )
Vec_IntPush( vVars, toLit(pFanin->Id) );
else if ( pCube[i] == '1' )
Vec_IntPush( vVars, lit_neg(toLit(pFanin->Id)) );
}
Vec_IntPush( vVars, toLit(pNode->Id) );
RetValue = sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
if ( !RetValue )
{
printf( "The CNF is trivially UNSAT.\n" );
return 0;
}
}
return 1;
}
/**Function*************************************************************
Synopsis [Adds clauses for the PO node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NodeAddClausesTop( sat_solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars )
{
Abc_Obj_t * pFanin;
int RetValue;
pFanin = Abc_ObjFanin0(pNode);
if ( Abc_ObjFaninC0(pNode) )
{
vVars->nSize = 0;
Vec_IntPush( vVars, toLit(pFanin->Id) );
Vec_IntPush( vVars, toLit(pNode->Id) );
RetValue = sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
if ( !RetValue )
{
printf( "The CNF is trivially UNSAT.\n" );
return 0;
}
vVars->nSize = 0;
Vec_IntPush( vVars, lit_neg(toLit(pFanin->Id)) );
Vec_IntPush( vVars, lit_neg(toLit(pNode->Id)) );
RetValue = sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
if ( !RetValue )
{
printf( "The CNF is trivially UNSAT.\n" );
return 0;
}
}
else
{
vVars->nSize = 0;
Vec_IntPush( vVars, lit_neg(toLit(pFanin->Id)) );
Vec_IntPush( vVars, toLit(pNode->Id) );
RetValue = sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
if ( !RetValue )
{
printf( "The CNF is trivially UNSAT.\n" );
return 0;
}
vVars->nSize = 0;
Vec_IntPush( vVars, toLit(pFanin->Id) );
Vec_IntPush( vVars, lit_neg(toLit(pNode->Id)) );
RetValue = sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
if ( !RetValue )
{
printf( "The CNF is trivially UNSAT.\n" );
return 0;
}
}
vVars->nSize = 0;
Vec_IntPush( vVars, toLit(pNode->Id) );
RetValue = sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
if ( !RetValue )
{
printf( "The CNF is trivially UNSAT.\n" );
return 0;
}
return 1;
}
/**Function*************************************************************
Synopsis [Sets up the SAT sat_solver.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
sat_solver * Abc_NtkMiterSatCreateLogic( Abc_Ntk_t * pNtk, int fAllPrimes )
{
sat_solver * pSat;
Mem_Flex_t * pMmFlex;
Abc_Obj_t * pNode;
Vec_Str_t * vCube;
Vec_Int_t * vVars;
char * pSop0, * pSop1;
int i;
assert( Abc_NtkIsBddLogic(pNtk) );
// transfer the IDs to the copy field
Abc_NtkForEachPi( pNtk, pNode, i )
pNode->pCopy = (Abc_Obj_t *)(ABC_PTRINT_T)pNode->Id;
// start the data structures
pSat = sat_solver_new();
sat_solver_store_alloc( pSat );
pMmFlex = Mem_FlexStart();
vCube = Vec_StrAlloc( 100 );
vVars = Vec_IntAlloc( 100 );
// add clauses for each internal nodes
Abc_NtkForEachNode( pNtk, pNode, i )
{
// derive SOPs for both phases of the node
Abc_NodeBddToCnf( pNode, pMmFlex, vCube, fAllPrimes, &pSop0, &pSop1 );
// add the clauses to the sat_solver
if ( !Abc_NodeAddClauses( pSat, pSop0, pSop1, pNode, vVars ) )
{
sat_solver_delete( pSat );
pSat = NULL;
goto finish;
}
}
// add clauses for each PO
Abc_NtkForEachPo( pNtk, pNode, i )
{
if ( !Abc_NodeAddClausesTop( pSat, pNode, vVars ) )
{
sat_solver_delete( pSat );
pSat = NULL;
goto finish;
}
}
sat_solver_store_mark_roots( pSat );
finish:
// delete
Vec_StrFree( vCube );
Vec_IntFree( vVars );
Mem_FlexStop( pMmFlex, 0 );
return pSat;
}
/**Function*************************************************************
Synopsis [Writes CNF for the sorter with N inputs asserting Q ones.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkWriteSorterCnf( char * pFileName, int nVars, int nQueens )
{
char Command[100];
void * pAbc;
Abc_Ntk_t * pNtk;
Abc_Obj_t * pObj, * ppNodes[2], * ppRoots[2];
Vec_Ptr_t * vNodes;
FILE * pFile;
int i, Counter;
if ( nQueens <= 0 && nQueens >= nVars )
{
printf( "The number of queens (Q = %d) should belong to the interval: 0 < Q < %d.\n", nQueens, nQueens);
return;
}
assert( nQueens > 0 && nQueens < nVars );
pAbc = Abc_FrameGetGlobalFrame();
// generate sorter
sprintf( Command, "gen -s -N %d sorter%d.blif", nVars, nVars );
if ( Cmd_CommandExecute( (Abc_Frame_t *)pAbc, Command ) )
{
fprintf( stdout, "Cannot execute command \"%s\".\n", Command );
return;
}
// read the file
sprintf( Command, "read sorter%d.blif; strash", nVars );
if ( Cmd_CommandExecute( (Abc_Frame_t *)pAbc, Command ) )
{
fprintf( stdout, "Cannot execute command \"%s\".\n", Command );
return;
}
// get the current network
pNtk = Abc_FrameReadNtk((Abc_Frame_t *)pAbc);
// collect the nodes for the given two primary outputs
ppNodes[0] = Abc_NtkPo( pNtk, nVars - nQueens - 1 );
ppNodes[1] = Abc_NtkPo( pNtk, nVars - nQueens );
ppRoots[0] = Abc_ObjFanin0( ppNodes[0] );
ppRoots[1] = Abc_ObjFanin0( ppNodes[1] );
vNodes = Abc_NtkDfsNodes( pNtk, ppRoots, 2 );
// assign CNF variables
Counter = 0;
Abc_NtkForEachObj( pNtk, pObj, i )
pObj->pCopy = (Abc_Obj_t *)~0;
Abc_NtkForEachPi( pNtk, pObj, i )
pObj->pCopy = (Abc_Obj_t *)(ABC_PTRINT_T)Counter++;
Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
pObj->pCopy = (Abc_Obj_t *)(ABC_PTRINT_T)Counter++;
/*
OutVar = pCnf->pVarNums[ pObj->Id ];
pVars[0] = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
pVars[1] = pCnf->pVarNums[ Aig_ObjFanin1(pObj)->Id ];
// positive phase
*pClas++ = pLits;
*pLits++ = 2 * OutVar;
*pLits++ = 2 * pVars[0] + !Aig_ObjFaninC0(pObj);
*pLits++ = 2 * pVars[1] + !Aig_ObjFaninC1(pObj);
// negative phase
*pClas++ = pLits;
*pLits++ = 2 * OutVar + 1;
*pLits++ = 2 * pVars[0] + Aig_ObjFaninC0(pObj);
*pClas++ = pLits;
*pLits++ = 2 * OutVar + 1;
*pLits++ = 2 * pVars[1] + Aig_ObjFaninC1(pObj);
*/
// add clauses for these nodes
pFile = fopen( pFileName, "w" );
fprintf( pFile, "c CNF for %d-bit sorter with %d bits set to 1 generated by ABC.\n", nVars, nQueens );
fprintf( pFile, "p cnf %d %d\n", Counter, 3 * Vec_PtrSize(vNodes) + 2 );
Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
{
// positive phase
fprintf( pFile, "%d %s%d %s%d 0\n", 1+(int)(ABC_PTRINT_T)pObj->pCopy,
Abc_ObjFaninC0(pObj)? "" : "-", 1+(int)(ABC_PTRINT_T)Abc_ObjFanin0(pObj)->pCopy,
Abc_ObjFaninC1(pObj)? "" : "-", 1+(int)(ABC_PTRINT_T)Abc_ObjFanin1(pObj)->pCopy );
// negative phase
fprintf( pFile, "-%d %s%d 0\n", 1+(int)(ABC_PTRINT_T)pObj->pCopy,
Abc_ObjFaninC0(pObj)? "-" : "", 1+(int)(ABC_PTRINT_T)Abc_ObjFanin0(pObj)->pCopy );
fprintf( pFile, "-%d %s%d 0\n", 1+(int)(ABC_PTRINT_T)pObj->pCopy,
Abc_ObjFaninC1(pObj)? "-" : "", 1+(int)(ABC_PTRINT_T)Abc_ObjFanin1(pObj)->pCopy );
}
Vec_PtrFree( vNodes );
/*
*pClas++ = pLits;
*pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj);
*/
// assert the first literal to zero
fprintf( pFile, "%s%d 0\n",
Abc_ObjFaninC0(ppNodes[0])? "" : "-", 1+(int)(ABC_PTRINT_T)Abc_ObjFanin0(ppNodes[0])->pCopy );
// assert the second literal to one
fprintf( pFile, "%s%d 0\n",
Abc_ObjFaninC0(ppNodes[1])? "-" : "", 1+(int)(ABC_PTRINT_T)Abc_ObjFanin0(ppNodes[1])->pCopy );
fclose( pFile );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END
Reference in New Issue View Git Blame Copy Permalink