/**CFile****************************************************************
FileName [csat_apis.h]
PackageName [Interface to CSAT.]
Synopsis [APIs, enums, and data structures expected from the use of CSAT.]
Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - August 28, 2005]
Revision [$Id: csat_apis.h,v 1.00 2005/08/28 00:00:00 alanmi Exp $]
***********************************************************************/
#include "base/abc/abc.h"
#include "proof/fraig/fraig.h"
#include "csat_apis.h"
#include "misc/st/stmm.h"
#include "base/main/main.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
#define ABC_DEFAULT_CONF_LIMIT 0 // limit on conflicts
#define ABC_DEFAULT_IMP_LIMIT 0 // limit on implications
struct ABC_ManagerStruct_t
{
// information about the problem
stmm_table * tName2Node; // the hash table mapping names to nodes
stmm_table * tNode2Name; // the hash table mapping nodes to names
Abc_Ntk_t * pNtk; // the starting ABC network
Abc_Ntk_t * pTarget; // the AIG representing the target
char * pDumpFileName; // the name of the file to dump the target network
Mem_Flex_t * pMmNames; // memory manager for signal names
// solving parameters
int mode; // 0 = resource-aware integration; 1 = brute-force SAT
Prove_Params_t Params; // integrated CEC parameters
// information about the target
int nog; // the numbers of gates in the target
Vec_Ptr_t * vNodes; // the gates in the target
Vec_Int_t * vValues; // the values of gate's outputs in the target
// solution
CSAT_Target_ResultT * pResult; // the result of solving the target
};
static CSAT_Target_ResultT * ABC_TargetResAlloc( int nVars );
static char * ABC_GetNodeName( ABC_Manager mng, Abc_Obj_t * pNode );
// procedures to start and stop the ABC framework
extern void Abc_Start();
extern void Abc_Stop();
// some external procedures
extern int Io_WriteBench( Abc_Ntk_t * pNtk, const char * FileName );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Creates a new manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
ABC_Manager ABC_InitManager()
{
ABC_Manager_t * mng;
Abc_Start();
mng = ABC_ALLOC( ABC_Manager_t, 1 );
memset( mng, 0, sizeof(ABC_Manager_t) );
mng->pNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 );
mng->pNtk->pName = Extra_UtilStrsav("csat_network");
mng->tName2Node = stmm_init_table(strcmp, stmm_strhash);
mng->tNode2Name = stmm_init_table(stmm_ptrcmp, stmm_ptrhash);
mng->pMmNames = Mem_FlexStart();
mng->vNodes = Vec_PtrAlloc( 100 );
mng->vValues = Vec_IntAlloc( 100 );
mng->mode = 0; // set "resource-aware integration" as the default mode
// set default parameters for CEC
Prove_ParamsSetDefault( &mng->Params );
// set infinite resource limit for the final mitering
// mng->Params.nMiteringLimitLast = ABC_INFINITY;
return mng;
}
/**Function*************************************************************
Synopsis [Deletes the manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void ABC_ReleaseManager( ABC_Manager mng )
{
CSAT_Target_ResultT * p_res = ABC_Get_Target_Result( mng,0 );
ABC_TargetResFree(p_res);
if ( mng->tNode2Name ) stmm_free_table( mng->tNode2Name );
if ( mng->tName2Node ) stmm_free_table( mng->tName2Node );
if ( mng->pMmNames ) Mem_FlexStop( mng->pMmNames, 0 );
if ( mng->pNtk ) Abc_NtkDelete( mng->pNtk );
if ( mng->pTarget ) Abc_NtkDelete( mng->pTarget );
if ( mng->vNodes ) Vec_PtrFree( mng->vNodes );
if ( mng->vValues ) Vec_IntFree( mng->vValues );
ABC_FREE( mng->pDumpFileName );
ABC_FREE( mng );
Abc_Stop();
}
/**Function*************************************************************
Synopsis [Sets solver options for learning.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void ABC_SetSolveOption( ABC_Manager mng, enum CSAT_OptionT option )
{
}
/**Function*************************************************************
Synopsis [Sets solving mode by brute-force SAT.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void ABC_UseOnlyCoreSatSolver( ABC_Manager mng )
{
mng->mode = 1; // switch to "brute-force SAT" as the solving option
}
/**Function*************************************************************
Synopsis [Adds a gate to the circuit.]
Description [The meaning of the parameters are:
type: the type of the gate to be added
name: the name of the gate to be added, name should be unique in a circuit.
nofi: number of fanins of the gate to be added;
fanins: the name array of fanins of the gate to be added.]
SideEffects []
SeeAlso []
***********************************************************************/
int ABC_AddGate( ABC_Manager mng, enum GateType type, char * name, int nofi, char ** fanins, int dc_attr )
{
Abc_Obj_t * pObj = NULL; // Suppress "might be used uninitialized"
Abc_Obj_t * pFanin;
char * pSop = NULL; // Suppress "might be used uninitialized"
char * pNewName;
int i;
// save the name in the local memory manager
pNewName = Mem_FlexEntryFetch( mng->pMmNames, strlen(name) + 1 );
strcpy( pNewName, name );
name = pNewName;
// consider different cases, create the node, and map the node into the name
switch( type )
{
case CSAT_BPI:
case CSAT_BPPI:
if ( nofi != 0 )
{ printf( "ABC_AddGate: The PI/PPI gate \"%s\" has fanins.\n", name ); return 0; }
// create the PI
pObj = Abc_NtkCreatePi( mng->pNtk );
stmm_insert( mng->tNode2Name, (char *)pObj, name );
break;
case CSAT_CONST:
case CSAT_BAND:
case CSAT_BNAND:
case CSAT_BOR:
case CSAT_BNOR:
case CSAT_BXOR:
case CSAT_BXNOR:
case CSAT_BINV:
case CSAT_BBUF:
// create the node
pObj = Abc_NtkCreateNode( mng->pNtk );
// create the fanins
for ( i = 0; i < nofi; i++ )
{
if ( !stmm_lookup( mng->tName2Node, fanins[i], (char **)&pFanin ) )
{ printf( "ABC_AddGate: The fanin gate \"%s\" is not in the network.\n", fanins[i] ); return 0; }
Abc_ObjAddFanin( pObj, pFanin );
}
// create the node function
switch( type )
{
case CSAT_CONST:
if ( nofi != 0 )
{ printf( "ABC_AddGate: The constant gate \"%s\" has fanins.\n", name ); return 0; }
pSop = Abc_SopCreateConst1( (Mem_Flex_t *)mng->pNtk->pManFunc );
break;
case CSAT_BAND:
if ( nofi < 1 )
{ printf( "ABC_AddGate: The AND gate \"%s\" no fanins.\n", name ); return 0; }
pSop = Abc_SopCreateAnd( (Mem_Flex_t *)mng->pNtk->pManFunc, nofi, NULL );
break;
case CSAT_BNAND:
if ( nofi < 1 )
{ printf( "ABC_AddGate: The NAND gate \"%s\" no fanins.\n", name ); return 0; }
pSop = Abc_SopCreateNand( (Mem_Flex_t *)mng->pNtk->pManFunc, nofi );
break;
case CSAT_BOR:
if ( nofi < 1 )
{ printf( "ABC_AddGate: The OR gate \"%s\" no fanins.\n", name ); return 0; }
pSop = Abc_SopCreateOr( (Mem_Flex_t *)mng->pNtk->pManFunc, nofi, NULL );
break;
case CSAT_BNOR:
if ( nofi < 1 )
{ printf( "ABC_AddGate: The NOR gate \"%s\" no fanins.\n", name ); return 0; }
pSop = Abc_SopCreateNor( (Mem_Flex_t *)mng->pNtk->pManFunc, nofi );
break;
case CSAT_BXOR:
if ( nofi < 1 )
{ printf( "ABC_AddGate: The XOR gate \"%s\" no fanins.\n", name ); return 0; }
if ( nofi > 2 )
{ printf( "ABC_AddGate: The XOR gate \"%s\" has more than two fanins.\n", name ); return 0; }
pSop = Abc_SopCreateXor( (Mem_Flex_t *)mng->pNtk->pManFunc, nofi );
break;
case CSAT_BXNOR:
if ( nofi < 1 )
{ printf( "ABC_AddGate: The XNOR gate \"%s\" no fanins.\n", name ); return 0; }
if ( nofi > 2 )
{ printf( "ABC_AddGate: The XNOR gate \"%s\" has more than two fanins.\n", name ); return 0; }
pSop = Abc_SopCreateNxor( (Mem_Flex_t *)mng->pNtk->pManFunc, nofi );
break;
case CSAT_BINV:
if ( nofi != 1 )
{ printf( "ABC_AddGate: The inverter gate \"%s\" does not have exactly one fanin.\n", name ); return 0; }
pSop = Abc_SopCreateInv( (Mem_Flex_t *)mng->pNtk->pManFunc );
break;
case CSAT_BBUF:
if ( nofi != 1 )
{ printf( "ABC_AddGate: The buffer gate \"%s\" does not have exactly one fanin.\n", name ); return 0; }
pSop = Abc_SopCreateBuf( (Mem_Flex_t *)mng->pNtk->pManFunc );
break;
default :
break;
}
Abc_ObjSetData( pObj, pSop );
break;
case CSAT_BPPO:
case CSAT_BPO:
if ( nofi != 1 )
{ printf( "ABC_AddGate: The PO/PPO gate \"%s\" does not have exactly one fanin.\n", name ); return 0; }
// create the PO
pObj = Abc_NtkCreatePo( mng->pNtk );
stmm_insert( mng->tNode2Name, (char *)pObj, name );
// connect to the PO fanin
if ( !stmm_lookup( mng->tName2Node, fanins[0], (char **)&pFanin ) )
{ printf( "ABC_AddGate: The fanin gate \"%s\" is not in the network.\n", fanins[0] ); return 0; }
Abc_ObjAddFanin( pObj, pFanin );
break;
default:
printf( "ABC_AddGate: Unknown gate type.\n" );
break;
}
// map the name into the node
if ( stmm_insert( mng->tName2Node, name, (char *)pObj ) )
{ printf( "ABC_AddGate: The same gate \"%s\" is added twice.\n", name ); return 0; }
return 1;
}
/**Function*************************************************************
Synopsis [This procedure also finalizes construction of the ABC network.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void ABC_Network_Finalize( ABC_Manager mng )
{
Abc_Ntk_t * pNtk = mng->pNtk;
Abc_Obj_t * pObj;
int i;
Abc_NtkForEachPi( pNtk, pObj, i )
Abc_ObjAssignName( pObj, ABC_GetNodeName(mng, pObj), NULL );
Abc_NtkForEachPo( pNtk, pObj, i )
Abc_ObjAssignName( pObj, ABC_GetNodeName(mng, pObj), NULL );
assert( Abc_NtkLatchNum(pNtk) == 0 );
}
/**Function*************************************************************
Synopsis [Checks integraty of the manager.]
Description [Checks if there are gates that are not used by any primary output.
If no such gates exist, return 1 else return 0.]
SideEffects []
SeeAlso []
***********************************************************************/
int ABC_Check_Integrity( ABC_Manager mng )
{
Abc_Ntk_t * pNtk = mng->pNtk;
Abc_Obj_t * pObj;
int i;
// check that there are no dangling nodes
Abc_NtkForEachNode( pNtk, pObj, i )
{
if ( i == 0 )
continue;
if ( Abc_ObjFanoutNum(pObj) == 0 )
{
// printf( "ABC_Check_Integrity: The network has dangling nodes.\n" );
return 0;
}
}
// make sure everything is okay with the network structure
if ( !Abc_NtkDoCheck( pNtk ) )
{
printf( "ABC_Check_Integrity: The internal network check has failed.\n" );
return 0;
}
return 1;
}
/**Function*************************************************************
Synopsis [Sets time limit for solving a target.]
Description [Runtime: time limit (in second).]
SideEffects []
SeeAlso []
***********************************************************************/
void ABC_SetTimeLimit( ABC_Manager mng, int runtime )
{
// printf( "ABC_SetTimeLimit: The resource limit is not implemented (warning).\n" );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void ABC_SetLearnLimit( ABC_Manager mng, int num )
{
// printf( "ABC_SetLearnLimit: The resource limit is not implemented (warning).\n" );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void ABC_SetLearnBacktrackLimit( ABC_Manager mng, int num )
{
// printf( "ABC_SetLearnBacktrackLimit: The resource limit is not implemented (warning).\n" );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void ABC_SetSolveBacktrackLimit( ABC_Manager mng, int num )
{
mng->Params.nMiteringLimitLast = num;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void ABC_SetSolveImplicationLimit( ABC_Manager mng, int num )
{
// printf( "ABC_SetSolveImplicationLimit: The resource limit is not implemented (warning).\n" );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void ABC_SetTotalBacktrackLimit( ABC_Manager mng, ABC_UINT64_T num )
{
mng->Params.nTotalBacktrackLimit = num;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void ABC_SetTotalInspectLimit( ABC_Manager mng, ABC_UINT64_T num )
{
mng->Params.nTotalInspectLimit = num;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
ABC_UINT64_T ABC_GetTotalBacktracksMade( ABC_Manager mng )
{
return mng->Params.nTotalBacktracksMade;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
ABC_UINT64_T ABC_GetTotalInspectsMade( ABC_Manager mng )
{
return mng->Params.nTotalInspectsMade;
}
/**Function*************************************************************
Synopsis [Sets the file name to dump the structurally hashed network used for solving.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void ABC_EnableDump( ABC_Manager mng, char * dump_file )
{
ABC_FREE( mng->pDumpFileName );
mng->pDumpFileName = Extra_UtilStrsav( dump_file );
}
/**Function*************************************************************
Synopsis [Adds a new target to the manager.]
Description [The meaning of the parameters are:
nog: number of gates that are in the targets,
names: name array of gates,
values: value array of the corresponding gates given in "names" to be solved.
The relation of them is AND.]
SideEffects []
SeeAlso []
***********************************************************************/
int ABC_AddTarget( ABC_Manager mng, int nog, char ** names, int * values )
{
Abc_Obj_t * pObj;
int i;
if ( nog < 1 )
{ printf( "ABC_AddTarget: The target has no gates.\n" ); return 0; }
// clear storage for the target
mng->nog = 0;
Vec_PtrClear( mng->vNodes );
Vec_IntClear( mng->vValues );
// save the target
for ( i = 0; i < nog; i++ )
{
if ( !stmm_lookup( mng->tName2Node, names[i], (char **)&pObj ) )
{ printf( "ABC_AddTarget: The target gate \"%s\" is not in the network.\n", names[i] ); return 0; }
Vec_PtrPush( mng->vNodes, pObj );
if ( values[i] < 0 || values[i] > 1 )
{ printf( "ABC_AddTarget: The value of gate \"%s\" is not 0 or 1.\n", names[i] ); return 0; }
Vec_IntPush( mng->vValues, values[i] );
}
mng->nog = nog;
return 1;
}
/**Function*************************************************************
Synopsis [Initialize the solver internal data structure.]
Description [Prepares the solver to work on one specific target
set by calling ABC_AddTarget before.]
SideEffects []
SeeAlso []
***********************************************************************/
void ABC_SolveInit( ABC_Manager mng )
{
// check if the target is available
assert( mng->nog == Vec_PtrSize(mng->vNodes) );
if ( mng->nog == 0 )
{ printf( "ABC_SolveInit: Target is not specified by ABC_AddTarget().\n" ); return; }
// free the previous target network if present
if ( mng->pTarget ) Abc_NtkDelete( mng->pTarget );
// set the new target network
// mng->pTarget = Abc_NtkCreateTarget( mng->pNtk, mng->vNodes, mng->vValues );
mng->pTarget = Abc_NtkStrash( mng->pNtk, 0, 1, 0 );
}
/**Function*************************************************************
Synopsis [Currently not implemented.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void ABC_AnalyzeTargets( ABC_Manager mng )
{
}
/**Function*************************************************************
Synopsis [Solves the targets added by ABC_AddTarget().]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
enum CSAT_StatusT ABC_Solve( ABC_Manager mng )
{
Prove_Params_t * pParams = &mng->Params;
int RetValue, i;
// check if the target network is available
if ( mng->pTarget == NULL )
{ printf( "ABC_Solve: Target network is not derived by ABC_SolveInit().\n" ); return UNDETERMINED; }
// try to prove the miter using a number of techniques
if ( mng->mode )
RetValue = Abc_NtkMiterSat( mng->pTarget, (ABC_INT64_T)pParams->nMiteringLimitLast, (ABC_INT64_T)0, 0, NULL, NULL );
else
// RetValue = Abc_NtkMiterProve( &mng->pTarget, pParams ); // old CEC engine
RetValue = Abc_NtkIvyProve( &mng->pTarget, pParams ); // new CEC engine
// analyze the result
mng->pResult = ABC_TargetResAlloc( Abc_NtkCiNum(mng->pTarget) );
if ( RetValue == -1 )
mng->pResult->status = UNDETERMINED;
else if ( RetValue == 1 )
mng->pResult->status = UNSATISFIABLE;
else if ( RetValue == 0 )
{
mng->pResult->status = SATISFIABLE;
// create the array of PI names and values
for ( i = 0; i < mng->pResult->no_sig; i++ )
{
mng->pResult->names[i] = Extra_UtilStrsav( ABC_GetNodeName(mng, Abc_NtkCi(mng->pNtk, i)) );
mng->pResult->values[i] = mng->pTarget->pModel[i];
}
ABC_FREE( mng->pTarget->pModel );
}
else assert( 0 );
// delete the target
Abc_NtkDelete( mng->pTarget );
mng->pTarget = NULL;
// return the status
return mng->pResult->status;
}
/**Function*************************************************************
Synopsis [Gets the solve status of a target.]
Description [TargetID: the target id returned by ABC_AddTarget().]
SideEffects []
SeeAlso []
***********************************************************************/
CSAT_Target_ResultT * ABC_Get_Target_Result( ABC_Manager mng, int TargetID )
{
return mng->pResult;
}
/**Function*************************************************************
Synopsis [Dumps the original network into the BENCH file.]
Description [This procedure should be modified to dump the target.]
SideEffects []
SeeAlso []
***********************************************************************/
void ABC_Dump_Bench_File( ABC_Manager mng )
{
Abc_Ntk_t * pNtkTemp, * pNtkAig;
const char * pFileName;
// derive the netlist
pNtkAig = Abc_NtkStrash( mng->pNtk, 0, 0, 0 );
pNtkTemp = Abc_NtkToNetlistBench( pNtkAig );
Abc_NtkDelete( pNtkAig );
if ( pNtkTemp == NULL )
{ printf( "ABC_Dump_Bench_File: Dumping BENCH has failed.\n" ); return; }
pFileName = mng->pDumpFileName? mng->pDumpFileName: "abc_test.bench";
Io_WriteBench( pNtkTemp, pFileName );
Abc_NtkDelete( pNtkTemp );
}
/**Function*************************************************************
Synopsis [Allocates the target result.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
CSAT_Target_ResultT * ABC_TargetResAlloc( int nVars )
{
CSAT_Target_ResultT * p;
p = ABC_ALLOC( CSAT_Target_ResultT, 1 );
memset( p, 0, sizeof(CSAT_Target_ResultT) );
p->no_sig = nVars;
p->names = ABC_ALLOC( char *, nVars );
p->values = ABC_ALLOC( int, nVars );
memset( p->names, 0, sizeof(char *) * nVars );
memset( p->values, 0, sizeof(int) * nVars );
return p;
}
/**Function*************************************************************
Synopsis [Deallocates the target result.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void ABC_TargetResFree( CSAT_Target_ResultT * p )
{
if ( p == NULL )
return;
if( p->names )
{
int i = 0;
for ( i = 0; i < p->no_sig; i++ )
{
ABC_FREE(p->names[i]);
}
}
ABC_FREE( p->names );
ABC_FREE( p->values );
ABC_FREE( p );
}
/**Function*************************************************************
Synopsis [Dumps the target AIG into the BENCH file.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
char * ABC_GetNodeName( ABC_Manager mng, Abc_Obj_t * pNode )
{
char * pName = NULL;
if ( !stmm_lookup( mng->tNode2Name, (char *)pNode, (char **)&pName ) )
{
assert( 0 );
}
return pName;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END