From 3c25decf65704916943b0569e6d0608072550a89 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 28 Aug 2005 08:01:00 -0700 Subject: Version abc50828 --- src/sat/csat/csat_apis.c | 630 +++++++++++++++++++++++++++++++++++++++++++++++ src/sat/csat/csat_apis.h | 174 +++++++++++++ 2 files changed, 804 insertions(+) create mode 100644 src/sat/csat/csat_apis.c create mode 100644 src/sat/csat/csat_apis.h (limited to 'src/sat/csat') diff --git a/src/sat/csat/csat_apis.c b/src/sat/csat/csat_apis.c new file mode 100644 index 00000000..eddd7270 --- /dev/null +++ b/src/sat/csat/csat_apis.c @@ -0,0 +1,630 @@ +/**CFile**************************************************************** + + FileName [csat_apis.h] + + PackageName [Interface to CSAT.] + + Synopsis [APIs, enums, and data structures expected from the use of CSAT.] + + Author [Alan Mishchenko ] + + 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 "abc.h" +#include "fraig.h" +#include "csat_apis.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +struct CSAT_ManagerStruct_t +{ + // information about the problem + stmm_table * tName2Node; // the hash table mapping names to nodes + Abc_Ntk_t * pNtk; // the starting ABC network + Abc_Ntk_t * pTarget; // the AIG of the target + char * pDumpFileName; // the name of the file to dump the target network + // solving parameters + int mode; // 0 = baseline; 1 = resource-aware fraiging + Fraig_Params_t Params; // the set of parameters to call FRAIG package + // 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 * CSAT_TargetResAlloc( int nVars ); +static void CSAT_TargetResFree( CSAT_Target_ResultT * p ); + +// some external procedures +extern Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fAllNodes ); +extern int Io_WriteBench( Abc_Ntk_t * pNtk, char * FileName ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Creates a new manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +CSAT_Manager CSAT_InitManager() +{ + CSAT_Manager_t * mng; + mng = ALLOC( CSAT_Manager_t, 1 ); + memset( mng, 0, sizeof(CSAT_Manager_t) ); + mng->pNtk = Abc_NtkAlloc( ABC_NTK_LOGIC_SOP ); + mng->pNtk->pName = util_strsav("csat_network"); + mng->tName2Node = stmm_init_table(strcmp, stmm_strhash); + mng->vNodes = Vec_PtrAlloc( 100 ); + mng->vValues = Vec_IntAlloc( 100 ); + return mng; +} + +/**Function************************************************************* + + Synopsis [Deletes the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void CSAT_QuitManager( CSAT_Manager mng ) +{ + if ( mng->tName2Node ) stmm_free_table( mng->tName2Node ); + 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 ); + FREE( mng->pDumpFileName ); + free( mng ); +} + +/**Function************************************************************* + + Synopsis [Sets solver options for learning.] + + Description [0 = baseline; 1 = resource-aware solving.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void CSAT_SetSolveOption( CSAT_Manager mng, enum CSAT_OptionT option ) +{ + mng->mode = option; + if ( option == 0 ) + printf( "CSAT_SetSolveOption: Setting baseline solving mode.\n" ); + else if ( option == 1 ) + printf( "CSAT_SetSolveOption: Setting resource-aware solving mode.\n" ); + else + printf( "CSAT_SetSolveOption: Unknown option.\n" ); +} + + +/**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 CSAT_AddGate( CSAT_Manager mng, enum GateType type, char * name, int nofi, char ** fanins, int dc_attr ) +{ + Abc_Obj_t * pObj, * pFanin; + char * pSop; + int i; + + switch( type ) + { + case CSAT_BPI: + case CSAT_BPPI: + if ( nofi != 0 ) + { printf( "CSAT_AddGate: The PI/PPI gate \"%s\" has fanins.\n", name ); return 0; } + // create the PI + pObj = Abc_NtkCreatePi( mng->pNtk ); + pObj->pNext = (Abc_Obj_t *)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( "CSAT_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( "CSAT_AddGate: The constant gate \"%s\" has fanins.\n", name ); return 0; } + pSop = Abc_SopCreateConst1( mng->pNtk->pManFunc ); + break; + case CSAT_BAND: + if ( nofi < 1 ) + { printf( "CSAT_AddGate: The AND gate \"%s\" no fanins.\n", name ); return 0; } + pSop = Abc_SopCreateAnd( mng->pNtk->pManFunc, nofi ); + break; + case CSAT_BNAND: + if ( nofi < 1 ) + { printf( "CSAT_AddGate: The NAND gate \"%s\" no fanins.\n", name ); return 0; } + pSop = Abc_SopCreateNand( mng->pNtk->pManFunc, nofi ); + break; + case CSAT_BOR: + if ( nofi < 1 ) + { printf( "CSAT_AddGate: The OR gate \"%s\" no fanins.\n", name ); return 0; } + pSop = Abc_SopCreateOr( mng->pNtk->pManFunc, nofi, NULL ); + break; + case CSAT_BNOR: + if ( nofi < 1 ) + { printf( "CSAT_AddGate: The NOR gate \"%s\" no fanins.\n", name ); return 0; } + pSop = Abc_SopCreateNor( mng->pNtk->pManFunc, nofi ); + break; + case CSAT_BXOR: + if ( nofi < 1 ) + { printf( "CSAT_AddGate: The XOR gate \"%s\" no fanins.\n", name ); return 0; } + if ( nofi > 2 ) + { printf( "CSAT_AddGate: The XOR gate \"%s\" has more than two fanins.\n", name ); return 0; } + pSop = Abc_SopCreateXor( mng->pNtk->pManFunc, nofi ); + break; + case CSAT_BXNOR: + if ( nofi < 1 ) + { printf( "CSAT_AddGate: The XNOR gate \"%s\" no fanins.\n", name ); return 0; } + if ( nofi > 2 ) + { printf( "CSAT_AddGate: The XNOR gate \"%s\" has more than two fanins.\n", name ); return 0; } + pSop = Abc_SopCreateNxor( mng->pNtk->pManFunc, nofi ); + break; + case CSAT_BINV: + if ( nofi != 1 ) + { printf( "CSAT_AddGate: The inverter gate \"%s\" does not have exactly one fanin.\n", name ); return 0; } + pSop = Abc_SopCreateInv( mng->pNtk->pManFunc ); + break; + case CSAT_BBUF: + if ( nofi != 1 ) + { printf( "CSAT_AddGate: The buffer gate \"%s\" does not have exactly one fanin.\n", name ); return 0; } + pSop = Abc_SopCreateBuf( mng->pNtk->pManFunc ); + break; + default : + break; + } + Abc_ObjSetData( pObj, pSop ); + break; + case CSAT_BPPO: + case CSAT_BPO: + if ( nofi != 1 ) + { printf( "CSAT_AddGate: The PO/PPO gate \"%s\" does not have exactly one fanin.\n", name ); return 0; } + // create the PO + pObj = Abc_NtkCreatePo( mng->pNtk ); + pObj->pNext = (Abc_Obj_t *)name; + // connect to the PO fanin + if ( !stmm_lookup( mng->tName2Node, fanins[0], (char **)&pFanin ) ) + { printf( "CSAT_AddGate: The fanin gate \"%s\" is not in the network.\n", fanins[0] ); return 0; } + Abc_ObjAddFanin( pObj, pFanin ); + break; + default: + printf( "CSAT_AddGate: Unknown gate type.\n" ); + break; + } + if ( stmm_insert( mng->tName2Node, name, (char *)pObj ) ) + { printf( "CSAT_AddGate: The same gate \"%s\" is added twice.\n", name ); return 0; } + return 1; +} + +/**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 CSAT_Check_Integrity( CSAT_Manager mng ) +{ + Abc_Ntk_t * pNtk = mng->pNtk; + Abc_Obj_t * pObj; + int i; + + // this procedure also finalizes construction of the ABC network + Abc_NtkFixNonDrivenNets( pNtk ); + Abc_NtkForEachPi( pNtk, pObj, i ) + Abc_NtkLogicStoreName( pObj, (char *)pObj->pNext ); + Abc_NtkForEachPo( pNtk, pObj, i ) + Abc_NtkLogicStoreName( pObj, (char *)pObj->pNext ); + assert( Abc_NtkLatchNum(pNtk) == 0 ); + + // make sure everything is okay with the network structure + if ( !Abc_NtkCheck( pNtk ) ) + { + printf( "CSAT_Check_Integrity: The internal network check has failed.\n" ); + return 0; + } + + // check that there is no dangling nodes + Abc_NtkForEachNode( pNtk, pObj, i ) + { + if ( Abc_ObjFanoutNum(pObj) == 0 ) + { + printf( "CSAT_Check_Integrity: The network has dangling nodes.\n" ); + return 0; + } + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Sets time limit for solving a target.] + + Description [Runtime: time limit (in second).] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void CSAT_SetTimeLimit( CSAT_Manager mng, int runtime ) +{ + printf( "CSAT_SetTimeLimit: The resource limit is not implemented (warning).\n" ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void CSAT_SetLearnLimit( CSAT_Manager mng, int num ) +{ + printf( "CSAT_SetLearnLimit: The resource limit is not implemented (warning).\n" ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void CSAT_SetSolveBacktrackLimit( CSAT_Manager mng, int num ) +{ + printf( "CSAT_SetSolveBacktrackLimit: The resource limit is not implemented (warning).\n" ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void CSAT_SetLearnBacktrackLimit( CSAT_Manager mng, int num ) +{ + printf( "CSAT_SetLearnBacktrackLimit: The resource limit is not implemented (warning).\n" ); +} + +/**Function************************************************************* + + Synopsis [Sets the file name to dump the structurally hashed network used for solving.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void CSAT_EnableDump( CSAT_Manager mng, char * dump_file ) +{ + FREE( mng->pDumpFileName ); + mng->pDumpFileName = util_strsav( 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 CSAT_AddTarget( CSAT_Manager mng, int nog, char ** names, int * values ) +{ + Abc_Obj_t * pObj; + int i; + if ( nog < 1 ) + { printf( "CSAT_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( "CSAT_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( "CSAT_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 CSAT_AddTarget before.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void CSAT_SolveInit( CSAT_Manager mng ) +{ + Fraig_Params_t * pParams = &mng->Params; + int nWords1, nWords2, nWordsMin; + + // check if the target is available + assert( mng->nog == Vec_PtrSize(mng->vNodes) ); + if ( mng->nog == 0 ) + { printf( "CSAT_SolveInit: Target is not specified by CSAT_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_NtkCreateCone( mng->pNtk, mng->vNodes, mng->vValues ); + + // to determine the number of simulation patterns + // use the following strategy + // at least 64 words (32 words random and 32 words dynamic) + // no more than 256M for one circuit (128M + 128M) + nWords1 = 32; + nWords2 = (1<<27) / (Abc_NtkNodeNum(mng->pTarget) + Abc_NtkCiNum(mng->pTarget)); + nWordsMin = ABC_MIN( nWords1, nWords2 ); + + // set parameters for fraiging + memset( pParams, 0, sizeof(Fraig_Params_t) ); + pParams->nPatsRand = nWordsMin * 32; // the number of words of random simulation info + pParams->nPatsDyna = nWordsMin * 32; // the number of words of dynamic simulation info + pParams->nBTLimit = 99; // the max number of backtracks to perform at a node + pParams->fFuncRed = mng->mode; // performs only one level hashing + pParams->fFeedBack = 1; // enables solver feedback + pParams->fDist1Pats = 1; // enables distance-1 patterns + pParams->fDoSparse = 0; // performs equiv tests for sparse functions + pParams->fChoicing = 0; // enables recording structural choices + pParams->fTryProve = 1; // tries to solve the final miter + pParams->fVerbose = 0; // the verbosiness flag + pParams->fVerboseP = 0; // the verbosiness flag for proof reporting +} + +/**Function************************************************************* + + Synopsis [Currently not implemented.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void CSAT_AnalyzeTargets( CSAT_Manager mng ) +{ +} + +/**Function************************************************************* + + Synopsis [Solves the targets added by CSAT_AddTarget().] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +enum CSAT_StatusT CSAT_Solve( CSAT_Manager mng ) +{ + Fraig_Man_t * pMan; + int * pModel; + int RetValue, i; + + // check if the target network is available + if ( mng->pTarget == NULL ) + { printf( "CSAT_Solve: Target network is not derived by CSAT_SolveInit().\n" ); return UNDETERMINED; } + + // transform the target into a fraig + pMan = Abc_NtkToFraig( mng->pTarget, &mng->Params, 0 ); + Fraig_ManProveMiter( pMan ); + + // analyze the result + mng->pResult = CSAT_TargetResAlloc( Abc_NtkCiNum(mng->pTarget) ); + RetValue = Fraig_ManCheckMiter( pMan ); + if ( RetValue == -1 ) + mng->pResult->status = UNDETERMINED; + else if ( RetValue == 1 ) + mng->pResult->status = UNSATISFIABLE; + else if ( RetValue == 0 ) + { + mng->pResult->status = SATISFIABLE; + pModel = Fraig_ManReadModel( pMan ); + assert( pModel != NULL ); + // create the array of PI names and values + for ( i = 0; i < mng->pResult->no_sig; i++ ) + { + mng->pResult->names[i] = (char *)Abc_NtkCi(mng->pNtk, i)->pNext; // returns the same string that was given + mng->pResult->values[i] = pModel[i]; + } + } + else + assert( 0 ); + + // delete the fraig manager + Fraig_ManFree( pMan ); + // 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 CSAT_AddTarget().] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +CSAT_Target_ResultT * CSAT_Get_Target_Result( CSAT_Manager mng, int TargetID ) +{ + return mng->pResult; +} + +/**Function************************************************************* + + Synopsis [Dumps the target AIG into the BENCH file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void CSAT_Dump_Bench_File( CSAT_Manager mng ) +{ + Abc_Ntk_t * pNtkTemp; + char * pFileName; + + // derive the netlist + pNtkTemp = Abc_NtkLogicToNetlistBench( mng->pTarget ); + if ( pNtkTemp == NULL ) + { printf( "CSAT_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 * CSAT_TargetResAlloc( int nVars ) +{ + CSAT_Target_ResultT * p; + p = ALLOC( CSAT_Target_ResultT, 1 ); + memset( p, 0, sizeof(CSAT_Target_ResultT) ); + p->no_sig = nVars; + p->names = ALLOC( char *, nVars ); + p->values = 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 CSAT_TargetResFree( CSAT_Target_ResultT * p ) +{ + if ( p == NULL ) + return; + FREE( p->names ); + FREE( p->values ); + free( p ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/sat/csat/csat_apis.h b/src/sat/csat/csat_apis.h new file mode 100644 index 00000000..124ca266 --- /dev/null +++ b/src/sat/csat/csat_apis.h @@ -0,0 +1,174 @@ +/**CFile**************************************************************** + + FileName [csat_apis.h] + + PackageName [Interface to CSAT.] + + Synopsis [APIs, enums, and data structures expected from the use of CSAT.] + + Author [Alan Mishchenko ] + + 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 $] + +***********************************************************************/ + +#ifndef __CSAT_APIS_H__ +#define __CSAT_APIS_H__ + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// STRUCTURE DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + + +typedef struct CSAT_ManagerStruct_t CSAT_Manager_t; +typedef struct CSAT_ManagerStruct_t * CSAT_Manager; + + +// GateType defines the gate type that can be added to circuit by +// CSAT_AddGate(); +#ifndef _CSAT_GATE_TYPE_ +#define _CSAT_GATE_TYPE_ +enum GateType +{ + CSAT_CONST = 0, // constant gate + CSAT_BPI, // boolean PI + CSAT_BPPI, // bit level PSEUDO PRIMARY INPUT + CSAT_BAND, // bit level AND + CSAT_BNAND, // bit level NAND + CSAT_BOR, // bit level OR + CSAT_BNOR, // bit level NOR + CSAT_BXOR, // bit level XOR + CSAT_BXNOR, // bit level XNOR + CSAT_BINV, // bit level INVERTER + CSAT_BBUF, // bit level BUFFER + CSAT_BPPO, // bit level PSEUDO PRIMARY OUTPUT + CSAT_BPO // boolean PO +}; +#endif + + +//CSAT_StatusT defines the return value by CSAT_Solve(); +#ifndef _CSAT_STATUS_ +#define _CSAT_STATUS_ +enum CSAT_StatusT +{ + UNDETERMINED = 0, + UNSATISFIABLE, + SATISFIABLE, + TIME_OUT, + FRAME_OUT, + NO_TARGET, + ABORTED, + SEQ_SATISFIABLE +}; +#endif + + +// CSAT_OptionT defines the solver option about learning +// which is used by CSAT_SetSolveOption(); +#ifndef _CSAT_OPTION_ +#define _CSAT_OPTION_ +enum CSAT_OptionT +{ + BASE_LINE = 0, + IMPLICT_LEARNING, //default + EXPLICT_LEARNING +}; +#endif + + +#ifndef _CSAT_Target_Result +#define _CSAT_Target_Result +typedef struct _CSAT_Target_ResultT CSAT_Target_ResultT; +struct _CSAT_Target_ResultT +{ + enum CSAT_StatusT status; // solve status of the target + int num_dec; // num of decisions to solve the target + int num_imp; // num of implications to solve the target + int num_cftg; // num of conflict gates learned + int num_cfts; // num of conflict signals in conflict gates + double time; // time(in second) used to solve the target + int no_sig; // if "status" is SATISFIABLE, "no_sig" is the number of + // primary inputs, if the "status" is TIME_OUT, "no_sig" is the + // number of constant signals found. + char** names; // if the "status" is SATISFIABLE, "names" is the name array of + // primary inputs, "values" is the value array of primary + // inputs that satisfy the target. + // if the "status" is TIME_OUT, "names" is the name array of + // constant signals found (signals at the root of decision + // tree), "values" is the value array of constant signals found. + int* values; +}; +#endif + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +// create a new manager +extern CSAT_Manager CSAT_InitManager(void); + +// set solver options for learning +extern void CSAT_SetSolveOption(CSAT_Manager mng, enum CSAT_OptionT option); + +// add a gate to the circuit +// 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 +extern int CSAT_AddGate(CSAT_Manager mng, + enum GateType type, + char* name, + int nofi, + char** fanins, + int dc_attr); + +// check if there are gates that are not used by any primary ouput. +// if no such gates exist, return 1 else return 0; +extern int CSAT_Check_Integrity(CSAT_Manager mng); + +// set time limit for solving a target. +// runtime: time limit (in second). +extern void CSAT_SetTimeLimit(CSAT_Manager mng, int runtime); +extern void CSAT_SetLearnLimit(CSAT_Manager mng, int num); +extern void CSAT_SetSolveBacktrackLimit(CSAT_Manager mng, int num); +extern void CSAT_SetLearnBacktrackLimit(CSAT_Manager mng, int num); +extern void CSAT_EnableDump(CSAT_Manager mng, char* dump_file); + +// 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. +extern int CSAT_AddTarget(CSAT_Manager mng, int nog, char**names, int* values); + +// initialize the solver internal data structure. +extern void CSAT_SolveInit(CSAT_Manager mng); +extern void CSAT_AnalyzeTargets(CSAT_Manager mng); + +// solve the targets added by CSAT_AddTarget() +extern enum CSAT_StatusT CSAT_Solve(CSAT_Manager mng); + +// get the solve status of a target +// TargetID: the target id returned by CSAT_AddTarget(). +extern CSAT_Target_ResultT * CSAT_Get_Target_Result(CSAT_Manager mng, int TargetID); +extern void CSAT_Dump_Bench_File(CSAT_Manager mng); + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + +#endif -- cgit v1.2.3