abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
csat_apis.h File Reference

Go to the source code of this file.

Data Structures

struct  _CSAT_Target_ResultT
 

Macros

#define _ABC_GATE_TYPE_
 
#define _ABC_STATUS_
 
#define _ABC_CALLER_
 
#define _ABC_OPTION_
 
#define _ABC_Target_Result
 

Typedefs

typedef
typedefABC_NAMESPACE_HEADER_START
struct ABC_ManagerStruct_t 
ABC_Manager_t
 INCLUDES ///. More...
 
typedef struct
ABC_ManagerStruct_t
ABC_Manager
 
typedef struct _CSAT_Target_ResultT CSAT_Target_ResultT
 

Enumerations

enum  GateType {
  CSAT_CONST = 0, CSAT_BPI, CSAT_BPPI, CSAT_BAND,
  CSAT_BNAND, CSAT_BOR, CSAT_BNOR, CSAT_BXOR,
  CSAT_BXNOR, CSAT_BINV, CSAT_BBUF, CSAT_BMUX,
  CSAT_BDFF, CSAT_BSDFF, CSAT_BTRIH, CSAT_BTRIL,
  CSAT_BBUS, CSAT_BPPO, CSAT_BPO, CSAT_BCNF,
  CSAT_BDC
}
 
enum  CSAT_StatusT {
  UNDETERMINED = 0, UNSATISFIABLE, SATISFIABLE, TIME_OUT,
  FRAME_OUT, NO_TARGET, ABORTED, SEQ_SATISFIABLE
}
 
enum  CSAT_CallerT { BLS = 0, SATORI, NONE }
 
enum  CSAT_OptionT { BASE_LINE = 0, IMPLICT_LEARNING, EXPLICT_LEARNING }
 

Functions

ABC_Manager ABC_InitManager (void)
 FUNCTION DEFINITIONS ///. More...
 
void ABC_ReleaseManager (ABC_Manager mng)
 
void ABC_SetSolveOption (ABC_Manager mng, enum CSAT_OptionT option)
 
void ABC_UseOnlyCoreSatSolver (ABC_Manager mng)
 
int ABC_AddGate (ABC_Manager mng, enum GateType type, char *name, int nofi, char **fanins, int dc_attr)
 
int ABC_Check_Integrity (ABC_Manager mng)
 
void ABC_Network_Finalize (ABC_Manager mng)
 
void ABC_SetTimeLimit (ABC_Manager mng, int runtime)
 
void ABC_SetLearnLimit (ABC_Manager mng, int num)
 
void ABC_SetSolveBacktrackLimit (ABC_Manager mng, int num)
 
void ABC_SetLearnBacktrackLimit (ABC_Manager mng, int num)
 
void ABC_EnableDump (ABC_Manager mng, char *dump_file)
 
void ABC_SetTotalBacktrackLimit (ABC_Manager mng, ABC_UINT64_T num)
 
void ABC_SetTotalInspectLimit (ABC_Manager mng, ABC_UINT64_T num)
 
ABC_UINT64_T ABC_GetTotalBacktracksMade (ABC_Manager mng)
 
ABC_UINT64_T ABC_GetTotalInspectsMade (ABC_Manager mng)
 
int ABC_AddTarget (ABC_Manager mng, int nog, char **names, int *values)
 
void ABC_SolveInit (ABC_Manager mng)
 
void ABC_AnalyzeTargets (ABC_Manager mng)
 
enum CSAT_StatusT ABC_Solve (ABC_Manager mng)
 
CSAT_Target_ResultTABC_Get_Target_Result (ABC_Manager mng, int TargetID)
 
void ABC_Dump_Bench_File (ABC_Manager mng)
 
void ABC_TargetResFree (CSAT_Target_ResultT *p)
 
void CSAT_SetCaller (ABC_Manager mng, enum CSAT_CallerT caller)
 

Macro Definition Documentation

#define _ABC_CALLER_

Definition at line 95 of file csat_apis.h.

#define _ABC_GATE_TYPE_

Definition at line 48 of file csat_apis.h.

#define _ABC_OPTION_

Definition at line 108 of file csat_apis.h.

#define _ABC_STATUS_

Definition at line 78 of file csat_apis.h.

#define _ABC_Target_Result

Definition at line 119 of file csat_apis.h.

Typedef Documentation

Definition at line 42 of file csat_apis.h.

typedef typedefABC_NAMESPACE_HEADER_START struct ABC_ManagerStruct_t ABC_Manager_t

INCLUDES ///.

CFile****************************************************************

FileName [csat_apis.h]

PackageName [Interface to CSAT.]

Synopsis [APIs, enums, and data structures expected from the use of CSAT.]

Author [Alan Mishchenko alanm.nosp@m.i@ee.nosp@m.cs.be.nosp@m.rkel.nosp@m.ey.ed.nosp@m.u]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - August 28, 2005]

Revision [

Id:
csat_apis.h,v 1.5 2005/12/30 10:54:40 rmukherj Exp

]PARAMETERS ///STRUCTURE DEFINITIONS ///

Definition at line 41 of file csat_apis.h.

Definition at line 120 of file csat_apis.h.

Enumeration Type Documentation

Enumerator
BLS 
SATORI 
NONE 

Definition at line 96 of file csat_apis.h.

97 {
98  BLS = 0,
99  SATORI,
100  NONE
101 };
Definition: csat_apis.h:98
Enumerator
BASE_LINE 
IMPLICT_LEARNING 
EXPLICT_LEARNING 

Definition at line 109 of file csat_apis.h.

110 {
111  BASE_LINE = 0,
112  IMPLICT_LEARNING, //default
114 };
Enumerator
UNDETERMINED 
UNSATISFIABLE 
SATISFIABLE 
TIME_OUT 
FRAME_OUT 
NO_TARGET 
ABORTED 
SEQ_SATISFIABLE 

Definition at line 79 of file csat_apis.h.

enum GateType
Enumerator
CSAT_CONST 
CSAT_BPI 
CSAT_BPPI 
CSAT_BAND 
CSAT_BNAND 
CSAT_BOR 
CSAT_BNOR 
CSAT_BXOR 
CSAT_BXNOR 
CSAT_BINV 
CSAT_BBUF 
CSAT_BMUX 
CSAT_BDFF 
CSAT_BSDFF 
CSAT_BTRIH 
CSAT_BTRIL 
CSAT_BBUS 
CSAT_BPPO 
CSAT_BPO 
CSAT_BCNF 
CSAT_BDC 

Definition at line 49 of file csat_apis.h.

50 {
51  CSAT_CONST = 0, // constant gate
52  CSAT_BPI, // boolean PI
53  CSAT_BPPI, // bit level PSEUDO PRIMARY INPUT
54  CSAT_BAND, // bit level AND
55  CSAT_BNAND, // bit level NAND
56  CSAT_BOR, // bit level OR
57  CSAT_BNOR, // bit level NOR
58  CSAT_BXOR, // bit level XOR
59  CSAT_BXNOR, // bit level XNOR
60  CSAT_BINV, // bit level INVERTER
61  CSAT_BBUF, // bit level BUFFER
62  CSAT_BMUX, // bit level MUX --not supported
63  CSAT_BDFF, // bit level D-type FF
64  CSAT_BSDFF, // bit level scan FF --not supported
65  CSAT_BTRIH, // bit level TRISTATE gate with active high control --not supported
66  CSAT_BTRIL, // bit level TRISTATE gate with active low control --not supported
67  CSAT_BBUS, // bit level BUS --not supported
68  CSAT_BPPO, // bit level PSEUDO PRIMARY OUTPUT
69  CSAT_BPO, // boolean PO
70  CSAT_BCNF, // boolean constraint
71  CSAT_BDC, // boolean don't care gate (2 input)
72 };

Function Documentation

int ABC_AddGate ( ABC_Manager  mng,
enum GateType  type,
char *  name,
int  nofi,
char **  fanins,
int  dc_attr 
)

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 []

Definition at line 175 of file csat_apis.c.

176 {
177  Abc_Obj_t * pObj = NULL; // Suppress "might be used uninitialized"
178  Abc_Obj_t * pFanin;
179  char * pSop = NULL; // Suppress "might be used uninitialized"
180  char * pNewName;
181  int i;
182 
183  // save the name in the local memory manager
184  pNewName = Mem_FlexEntryFetch( mng->pMmNames, strlen(name) + 1 );
185  strcpy( pNewName, name );
186  name = pNewName;
187 
188  // consider different cases, create the node, and map the node into the name
189  switch( type )
190  {
191  case CSAT_BPI:
192  case CSAT_BPPI:
193  if ( nofi != 0 )
194  { printf( "ABC_AddGate: The PI/PPI gate \"%s\" has fanins.\n", name ); return 0; }
195  // create the PI
196  pObj = Abc_NtkCreatePi( mng->pNtk );
197  stmm_insert( mng->tNode2Name, (char *)pObj, name );
198  break;
199  case CSAT_CONST:
200  case CSAT_BAND:
201  case CSAT_BNAND:
202  case CSAT_BOR:
203  case CSAT_BNOR:
204  case CSAT_BXOR:
205  case CSAT_BXNOR:
206  case CSAT_BINV:
207  case CSAT_BBUF:
208  // create the node
209  pObj = Abc_NtkCreateNode( mng->pNtk );
210  // create the fanins
211  for ( i = 0; i < nofi; i++ )
212  {
213  if ( !stmm_lookup( mng->tName2Node, fanins[i], (char **)&pFanin ) )
214  { printf( "ABC_AddGate: The fanin gate \"%s\" is not in the network.\n", fanins[i] ); return 0; }
215  Abc_ObjAddFanin( pObj, pFanin );
216  }
217  // create the node function
218  switch( type )
219  {
220  case CSAT_CONST:
221  if ( nofi != 0 )
222  { printf( "ABC_AddGate: The constant gate \"%s\" has fanins.\n", name ); return 0; }
223  pSop = Abc_SopCreateConst1( (Mem_Flex_t *)mng->pNtk->pManFunc );
224  break;
225  case CSAT_BAND:
226  if ( nofi < 1 )
227  { printf( "ABC_AddGate: The AND gate \"%s\" no fanins.\n", name ); return 0; }
228  pSop = Abc_SopCreateAnd( (Mem_Flex_t *)mng->pNtk->pManFunc, nofi, NULL );
229  break;
230  case CSAT_BNAND:
231  if ( nofi < 1 )
232  { printf( "ABC_AddGate: The NAND gate \"%s\" no fanins.\n", name ); return 0; }
233  pSop = Abc_SopCreateNand( (Mem_Flex_t *)mng->pNtk->pManFunc, nofi );
234  break;
235  case CSAT_BOR:
236  if ( nofi < 1 )
237  { printf( "ABC_AddGate: The OR gate \"%s\" no fanins.\n", name ); return 0; }
238  pSop = Abc_SopCreateOr( (Mem_Flex_t *)mng->pNtk->pManFunc, nofi, NULL );
239  break;
240  case CSAT_BNOR:
241  if ( nofi < 1 )
242  { printf( "ABC_AddGate: The NOR gate \"%s\" no fanins.\n", name ); return 0; }
243  pSop = Abc_SopCreateNor( (Mem_Flex_t *)mng->pNtk->pManFunc, nofi );
244  break;
245  case CSAT_BXOR:
246  if ( nofi < 1 )
247  { printf( "ABC_AddGate: The XOR gate \"%s\" no fanins.\n", name ); return 0; }
248  if ( nofi > 2 )
249  { printf( "ABC_AddGate: The XOR gate \"%s\" has more than two fanins.\n", name ); return 0; }
250  pSop = Abc_SopCreateXor( (Mem_Flex_t *)mng->pNtk->pManFunc, nofi );
251  break;
252  case CSAT_BXNOR:
253  if ( nofi < 1 )
254  { printf( "ABC_AddGate: The XNOR gate \"%s\" no fanins.\n", name ); return 0; }
255  if ( nofi > 2 )
256  { printf( "ABC_AddGate: The XNOR gate \"%s\" has more than two fanins.\n", name ); return 0; }
257  pSop = Abc_SopCreateNxor( (Mem_Flex_t *)mng->pNtk->pManFunc, nofi );
258  break;
259  case CSAT_BINV:
260  if ( nofi != 1 )
261  { printf( "ABC_AddGate: The inverter gate \"%s\" does not have exactly one fanin.\n", name ); return 0; }
262  pSop = Abc_SopCreateInv( (Mem_Flex_t *)mng->pNtk->pManFunc );
263  break;
264  case CSAT_BBUF:
265  if ( nofi != 1 )
266  { printf( "ABC_AddGate: The buffer gate \"%s\" does not have exactly one fanin.\n", name ); return 0; }
267  pSop = Abc_SopCreateBuf( (Mem_Flex_t *)mng->pNtk->pManFunc );
268  break;
269  default :
270  break;
271  }
272  Abc_ObjSetData( pObj, pSop );
273  break;
274  case CSAT_BPPO:
275  case CSAT_BPO:
276  if ( nofi != 1 )
277  { printf( "ABC_AddGate: The PO/PPO gate \"%s\" does not have exactly one fanin.\n", name ); return 0; }
278  // create the PO
279  pObj = Abc_NtkCreatePo( mng->pNtk );
280  stmm_insert( mng->tNode2Name, (char *)pObj, name );
281  // connect to the PO fanin
282  if ( !stmm_lookup( mng->tName2Node, fanins[0], (char **)&pFanin ) )
283  { printf( "ABC_AddGate: The fanin gate \"%s\" is not in the network.\n", fanins[0] ); return 0; }
284  Abc_ObjAddFanin( pObj, pFanin );
285  break;
286  default:
287  printf( "ABC_AddGate: Unknown gate type.\n" );
288  break;
289  }
290 
291  // map the name into the node
292  if ( stmm_insert( mng->tName2Node, name, (char *)pObj ) )
293  { printf( "ABC_AddGate: The same gate \"%s\" is added twice.\n", name ); return 0; }
294  return 1;
295 }
stmm_table * tNode2Name
Definition: csat_apis.c:40
int stmm_insert(stmm_table *table, char *key, char *value)
Definition: stmm.c:200
ABC_DLL char * Abc_SopCreateAnd(Mem_Flex_t *pMan, int nVars, int *pfCompl)
Definition: abcSop.c:162
ABC_DLL char * Abc_SopCreateInv(Mem_Flex_t *pMan)
Definition: abcSop.c:345
ABC_DLL char * Abc_SopCreateNand(Mem_Flex_t *pMan, int nVars)
Definition: abcSop.c:184
char * Mem_FlexEntryFetch(Mem_Flex_t *p, int nBytes)
Definition: mem.c:372
static void Abc_ObjSetData(Abc_Obj_t *pObj, void *pData)
Definition: abc.h:343
ABC_DLL char * Abc_SopCreateConst1(Mem_Flex_t *pMan)
Definition: abcSop.c:107
ABC_DLL void Abc_ObjAddFanin(Abc_Obj_t *pObj, Abc_Obj_t *pFanin)
Definition: abcFanio.c:84
ABC_DLL char * Abc_SopCreateBuf(Mem_Flex_t *pMan)
Definition: abcSop.c:361
Mem_Flex_t * pMmNames
Definition: csat_apis.c:44
stmm_table * tName2Node
Definition: csat_apis.c:39
void * pManFunc
Definition: abc.h:191
Abc_Ntk_t * pNtk
Definition: csat_apis.c:41
int stmm_lookup(stmm_table *table, char *key, char **value)
Definition: stmm.c:134
ABC_DLL char * Abc_SopCreateNxor(Mem_Flex_t *pMan, int nVars)
Definition: abcSop.c:311
char * name
ABC_DLL char * Abc_SopCreateXor(Mem_Flex_t *pMan, int nVars)
Definition: abcSop.c:274
static Abc_Obj_t * Abc_NtkCreatePi(Abc_Ntk_t *pNtk)
Definition: abc.h:303
char * strcpy()
ABC_DLL char * Abc_SopCreateNor(Mem_Flex_t *pMan, int nVars)
Definition: abcSop.c:253
static Abc_Obj_t * Abc_NtkCreateNode(Abc_Ntk_t *pNtk)
Definition: abc.h:308
int strlen()
static Abc_Obj_t * Abc_NtkCreatePo(Abc_Ntk_t *pNtk)
Definition: abc.h:304
ABC_DLL char * Abc_SopCreateOr(Mem_Flex_t *pMan, int nVars, int *pfCompl)
Definition: abcSop.c:206
int ABC_AddTarget ( ABC_Manager  mng,
int  nog,
char **  names,
int *  values 
)

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 []

Definition at line 534 of file csat_apis.c.

535 {
536  Abc_Obj_t * pObj;
537  int i;
538  if ( nog < 1 )
539  { printf( "ABC_AddTarget: The target has no gates.\n" ); return 0; }
540  // clear storage for the target
541  mng->nog = 0;
542  Vec_PtrClear( mng->vNodes );
543  Vec_IntClear( mng->vValues );
544  // save the target
545  for ( i = 0; i < nog; i++ )
546  {
547  if ( !stmm_lookup( mng->tName2Node, names[i], (char **)&pObj ) )
548  { printf( "ABC_AddTarget: The target gate \"%s\" is not in the network.\n", names[i] ); return 0; }
549  Vec_PtrPush( mng->vNodes, pObj );
550  if ( values[i] < 0 || values[i] > 1 )
551  { printf( "ABC_AddTarget: The value of gate \"%s\" is not 0 or 1.\n", names[i] ); return 0; }
552  Vec_IntPush( mng->vValues, values[i] );
553  }
554  mng->nog = nog;
555  return 1;
556 }
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
Vec_Ptr_t * vNodes
Definition: csat_apis.c:50
stmm_table * tName2Node
Definition: csat_apis.c:39
Vec_Int_t * vValues
Definition: csat_apis.c:51
int stmm_lookup(stmm_table *table, char *key, char **value)
Definition: stmm.c:134
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
static void Vec_PtrClear(Vec_Ptr_t *p)
Definition: vecPtr.h:545
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
void ABC_AnalyzeTargets ( ABC_Manager  mng)

Function*************************************************************

Synopsis [Currently not implemented.]

Description []

SideEffects []

SeeAlso []

Definition at line 596 of file csat_apis.c.

597 {
598 }
int ABC_Check_Integrity ( ABC_Manager  mng)

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 []

Definition at line 332 of file csat_apis.c.

333 {
334  Abc_Ntk_t * pNtk = mng->pNtk;
335  Abc_Obj_t * pObj;
336  int i;
337 
338  // check that there are no dangling nodes
339  Abc_NtkForEachNode( pNtk, pObj, i )
340  {
341  if ( i == 0 )
342  continue;
343  if ( Abc_ObjFanoutNum(pObj) == 0 )
344  {
345 // printf( "ABC_Check_Integrity: The network has dangling nodes.\n" );
346  return 0;
347  }
348  }
349 
350  // make sure everything is okay with the network structure
351  if ( !Abc_NtkDoCheck( pNtk ) )
352  {
353  printf( "ABC_Check_Integrity: The internal network check has failed.\n" );
354  return 0;
355  }
356  return 1;
357 }
static int Abc_ObjFanoutNum(Abc_Obj_t *pObj)
Definition: abc.h:365
Abc_Ntk_t * pNtk
Definition: csat_apis.c:41
ABC_DLL int Abc_NtkDoCheck(Abc_Ntk_t *pNtk)
Definition: abcCheck.c:93
#define Abc_NtkForEachNode(pNtk, pNode, i)
Definition: abc.h:461
void ABC_Dump_Bench_File ( ABC_Manager  mng)

Function*************************************************************

Synopsis [Dumps the original network into the BENCH file.]

Description [This procedure should be modified to dump the target.]

SideEffects []

SeeAlso []

Definition at line 680 of file csat_apis.c.

681 {
682  Abc_Ntk_t * pNtkTemp, * pNtkAig;
683  const char * pFileName;
684 
685  // derive the netlist
686  pNtkAig = Abc_NtkStrash( mng->pNtk, 0, 0, 0 );
687  pNtkTemp = Abc_NtkToNetlistBench( pNtkAig );
688  Abc_NtkDelete( pNtkAig );
689  if ( pNtkTemp == NULL )
690  { printf( "ABC_Dump_Bench_File: Dumping BENCH has failed.\n" ); return; }
691  pFileName = mng->pDumpFileName? mng->pDumpFileName: "abc_test.bench";
692  Io_WriteBench( pNtkTemp, pFileName );
693  Abc_NtkDelete( pNtkTemp );
694 }
int Io_WriteBench(Abc_Ntk_t *pNtk, const char *FileName)
FUNCTION DEFINITIONS ///.
Definition: ioWriteBench.c:53
ABC_DLL Abc_Ntk_t * Abc_NtkStrash(Abc_Ntk_t *pNtk, int fAllNodes, int fCleanup, int fRecord)
Definition: abcStrash.c:265
ABC_DLL Abc_Ntk_t * Abc_NtkToNetlistBench(Abc_Ntk_t *pNtk)
Definition: abcNetlist.c:122
char * pDumpFileName
Definition: csat_apis.c:43
ABC_DLL void Abc_NtkDelete(Abc_Ntk_t *pNtk)
Definition: abcNtk.c:1233
Abc_Ntk_t * pNtk
Definition: csat_apis.c:41
void ABC_EnableDump ( ABC_Manager  mng,
char *  dump_file 
)

Function*************************************************************

Synopsis [Sets the file name to dump the structurally hashed network used for solving.]

Description []

SideEffects []

SeeAlso []

Definition at line 513 of file csat_apis.c.

514 {
515  ABC_FREE( mng->pDumpFileName );
516  mng->pDumpFileName = Extra_UtilStrsav( dump_file );
517 }
char * pDumpFileName
Definition: csat_apis.c:43
char * Extra_UtilStrsav(const char *s)
#define ABC_FREE(obj)
Definition: abc_global.h:232
CSAT_Target_ResultT* ABC_Get_Target_Result ( ABC_Manager  mng,
int  TargetID 
)

Function*************************************************************

Synopsis [Gets the solve status of a target.]

Description [TargetID: the target id returned by ABC_AddTarget().]

SideEffects []

SeeAlso []

Definition at line 664 of file csat_apis.c.

665 {
666  return mng->pResult;
667 }
CSAT_Target_ResultT * pResult
Definition: csat_apis.c:53
ABC_UINT64_T ABC_GetTotalBacktracksMade ( ABC_Manager  mng)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 481 of file csat_apis.c.

482 {
483  return mng->Params.nTotalBacktracksMade;
484 }
Prove_Params_t Params
Definition: csat_apis.c:47
ABC_INT64_T nTotalBacktracksMade
Definition: ivyFraig.c:136
ABC_UINT64_T ABC_GetTotalInspectsMade ( ABC_Manager  mng)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 497 of file csat_apis.c.

498 {
499  return mng->Params.nTotalInspectsMade;
500 }
Prove_Params_t Params
Definition: csat_apis.c:47
ABC_INT64_T nTotalInspectsMade
Definition: ivyFraig.c:137
ABC_Manager ABC_InitManager ( void  )

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis [Creates a new manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 81 of file csat_apis.c.

82 {
83  ABC_Manager_t * mng;
84  Abc_Start();
85  mng = ABC_ALLOC( ABC_Manager_t, 1 );
86  memset( mng, 0, sizeof(ABC_Manager_t) );
87  mng->pNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 );
88  mng->pNtk->pName = Extra_UtilStrsav("csat_network");
89  mng->tName2Node = stmm_init_table(strcmp, stmm_strhash);
90  mng->tNode2Name = stmm_init_table(stmm_ptrcmp, stmm_ptrhash);
91  mng->pMmNames = Mem_FlexStart();
92  mng->vNodes = Vec_PtrAlloc( 100 );
93  mng->vValues = Vec_IntAlloc( 100 );
94  mng->mode = 0; // set "resource-aware integration" as the default mode
95  // set default parameters for CEC
96  Prove_ParamsSetDefault( &mng->Params );
97  // set infinite resource limit for the final mitering
98 // mng->Params.nMiteringLimitLast = ABC_INFINITY;
99  return mng;
100 }
char * memset()
stmm_table * stmm_init_table(stmm_compare_func_type compare, stmm_hash_func_type hash)
Definition: stmm.c:69
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
void Prove_ParamsSetDefault(Prove_Params_t *pParams)
FUNCTION DEFINITIONS ///.
Definition: fraigMan.c:46
char * Extra_UtilStrsav(const char *s)
ABC_DLL Abc_Ntk_t * Abc_NtkAlloc(Abc_NtkType_t Type, Abc_NtkFunc_t Func, int fUseMemMan)
DECLARATIONS ///.
Definition: abcNtk.c:50
int strcmp()
Mem_Flex_t * Mem_FlexStart()
Definition: mem.c:311
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
int stmm_ptrhash(const char *x, int size)
Definition: stmm.c:533
typedefABC_NAMESPACE_HEADER_START struct ABC_ManagerStruct_t ABC_Manager_t
INCLUDES ///.
Definition: csat_apis.h:41
int stmm_strhash(const char *string, int modulus)
Definition: stmm.c:514
int stmm_ptrcmp(const char *x, const char *y)
Definition: stmm.c:545
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
void Abc_Start()
DECLARATIONS ///.
Definition: mainLib.c:52
void ABC_Network_Finalize ( ABC_Manager  mng)

Function*************************************************************

Synopsis [This procedure also finalizes construction of the ABC network.]

Description []

SideEffects []

SeeAlso []

Definition at line 308 of file csat_apis.c.

309 {
310  Abc_Ntk_t * pNtk = mng->pNtk;
311  Abc_Obj_t * pObj;
312  int i;
313  Abc_NtkForEachPi( pNtk, pObj, i )
314  Abc_ObjAssignName( pObj, ABC_GetNodeName(mng, pObj), NULL );
315  Abc_NtkForEachPo( pNtk, pObj, i )
316  Abc_ObjAssignName( pObj, ABC_GetNodeName(mng, pObj), NULL );
317  assert( Abc_NtkLatchNum(pNtk) == 0 );
318 }
static int Abc_NtkLatchNum(Abc_Ntk_t *pNtk)
Definition: abc.h:294
static char * ABC_GetNodeName(ABC_Manager mng, Abc_Obj_t *pNode)
Definition: csat_apis.c:761
ABC_DLL char * Abc_ObjAssignName(Abc_Obj_t *pObj, char *pName, char *pSuffix)
Definition: abcNames.c:68
Abc_Ntk_t * pNtk
Definition: csat_apis.c:41
#define assert(ex)
Definition: util_old.h:213
#define Abc_NtkForEachPo(pNtk, pPo, i)
Definition: abc.h:517
#define Abc_NtkForEachPi(pNtk, pPi, i)
Definition: abc.h:513
void ABC_ReleaseManager ( ABC_Manager  mng)

Function*************************************************************

Synopsis [Deletes the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 113 of file csat_apis.c.

114 {
115  CSAT_Target_ResultT * p_res = ABC_Get_Target_Result( mng,0 );
116  ABC_TargetResFree(p_res);
117  if ( mng->tNode2Name ) stmm_free_table( mng->tNode2Name );
118  if ( mng->tName2Node ) stmm_free_table( mng->tName2Node );
119  if ( mng->pMmNames ) Mem_FlexStop( mng->pMmNames, 0 );
120  if ( mng->pNtk ) Abc_NtkDelete( mng->pNtk );
121  if ( mng->pTarget ) Abc_NtkDelete( mng->pTarget );
122  if ( mng->vNodes ) Vec_PtrFree( mng->vNodes );
123  if ( mng->vValues ) Vec_IntFree( mng->vValues );
124  ABC_FREE( mng->pDumpFileName );
125  ABC_FREE( mng );
126  Abc_Stop();
127 }
void Abc_Stop()
Definition: mainLib.c:76
CSAT_Target_ResultT * ABC_Get_Target_Result(ABC_Manager mng, int TargetID)
Definition: csat_apis.c:664
stmm_table * tNode2Name
Definition: csat_apis.c:40
void ABC_TargetResFree(CSAT_Target_ResultT *p)
Definition: csat_apis.c:733
char * pDumpFileName
Definition: csat_apis.c:43
ABC_DLL void Abc_NtkDelete(Abc_Ntk_t *pNtk)
Definition: abcNtk.c:1233
Mem_Flex_t * pMmNames
Definition: csat_apis.c:44
Vec_Ptr_t * vNodes
Definition: csat_apis.c:50
stmm_table * tName2Node
Definition: csat_apis.c:39
Vec_Int_t * vValues
Definition: csat_apis.c:51
Abc_Ntk_t * pNtk
Definition: csat_apis.c:41
Abc_Ntk_t * pTarget
Definition: csat_apis.c:42
void Mem_FlexStop(Mem_Flex_t *p, int fVerbose)
Definition: mem.c:343
void stmm_free_table(stmm_table *table)
Definition: stmm.c:79
#define ABC_FREE(obj)
Definition: abc_global.h:232
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
void ABC_SetLearnBacktrackLimit ( ABC_Manager  mng,
int  num 
)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 402 of file csat_apis.c.

403 {
404 // printf( "ABC_SetLearnBacktrackLimit: The resource limit is not implemented (warning).\n" );
405 }
void ABC_SetLearnLimit ( ABC_Manager  mng,
int  num 
)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 386 of file csat_apis.c.

387 {
388 // printf( "ABC_SetLearnLimit: The resource limit is not implemented (warning).\n" );
389 }
void ABC_SetSolveBacktrackLimit ( ABC_Manager  mng,
int  num 
)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 418 of file csat_apis.c.

419 {
420  mng->Params.nMiteringLimitLast = num;
421 }
Prove_Params_t Params
Definition: csat_apis.c:47
void ABC_SetSolveOption ( ABC_Manager  mng,
enum CSAT_OptionT  option 
)

Function*************************************************************

Synopsis [Sets solver options for learning.]

Description []

SideEffects []

SeeAlso []

Definition at line 140 of file csat_apis.c.

141 {
142 }
void ABC_SetTimeLimit ( ABC_Manager  mng,
int  runtime 
)

Function*************************************************************

Synopsis [Sets time limit for solving a target.]

Description [Runtime: time limit (in second).]

SideEffects []

SeeAlso []

Definition at line 370 of file csat_apis.c.

371 {
372 // printf( "ABC_SetTimeLimit: The resource limit is not implemented (warning).\n" );
373 }
void ABC_SetTotalBacktrackLimit ( ABC_Manager  mng,
ABC_UINT64_T  num 
)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 450 of file csat_apis.c.

451 {
452  mng->Params.nTotalBacktrackLimit = num;
453 }
Prove_Params_t Params
Definition: csat_apis.c:47
ABC_INT64_T nTotalBacktrackLimit
Definition: ivyFraig.c:133
void ABC_SetTotalInspectLimit ( ABC_Manager  mng,
ABC_UINT64_T  num 
)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 466 of file csat_apis.c.

467 {
468  mng->Params.nTotalInspectLimit = num;
469 }
Prove_Params_t Params
Definition: csat_apis.c:47
ABC_INT64_T nTotalInspectLimit
Definition: ivyFraig.c:134
enum CSAT_StatusT ABC_Solve ( ABC_Manager  mng)

Function*************************************************************

Synopsis [Solves the targets added by ABC_AddTarget().]

Description []

SideEffects []

SeeAlso []

Definition at line 611 of file csat_apis.c.

612 {
613  Prove_Params_t * pParams = &mng->Params;
614  int RetValue, i;
615 
616  // check if the target network is available
617  if ( mng->pTarget == NULL )
618  { printf( "ABC_Solve: Target network is not derived by ABC_SolveInit().\n" ); return UNDETERMINED; }
619 
620  // try to prove the miter using a number of techniques
621  if ( mng->mode )
622  RetValue = Abc_NtkMiterSat( mng->pTarget, (ABC_INT64_T)pParams->nMiteringLimitLast, (ABC_INT64_T)0, 0, NULL, NULL );
623  else
624 // RetValue = Abc_NtkMiterProve( &mng->pTarget, pParams ); // old CEC engine
625  RetValue = Abc_NtkIvyProve( &mng->pTarget, pParams ); // new CEC engine
626 
627  // analyze the result
629  if ( RetValue == -1 )
630  mng->pResult->status = UNDETERMINED;
631  else if ( RetValue == 1 )
632  mng->pResult->status = UNSATISFIABLE;
633  else if ( RetValue == 0 )
634  {
635  mng->pResult->status = SATISFIABLE;
636  // create the array of PI names and values
637  for ( i = 0; i < mng->pResult->no_sig; i++ )
638  {
639  mng->pResult->names[i] = Extra_UtilStrsav( ABC_GetNodeName(mng, Abc_NtkCi(mng->pNtk, i)) );
640  mng->pResult->values[i] = mng->pTarget->pModel[i];
641  }
642  ABC_FREE( mng->pTarget->pModel );
643  }
644  else assert( 0 );
645 
646  // delete the target
647  Abc_NtkDelete( mng->pTarget );
648  mng->pTarget = NULL;
649  // return the status
650  return mng->pResult->status;
651 }
Prove_Params_t Params
Definition: csat_apis.c:47
static int Abc_NtkCiNum(Abc_Ntk_t *pNtk)
Definition: abc.h:287
static char * ABC_GetNodeName(ABC_Manager mng, Abc_Obj_t *pNode)
Definition: csat_apis.c:761
static Abc_Obj_t * Abc_NtkCi(Abc_Ntk_t *pNtk, int i)
Definition: abc.h:317
ABC_DLL void Abc_NtkDelete(Abc_Ntk_t *pNtk)
Definition: abcNtk.c:1233
char * Extra_UtilStrsav(const char *s)
int * pModel
Definition: abc.h:198
Abc_Ntk_t * pNtk
Definition: csat_apis.c:41
Abc_Ntk_t * pTarget
Definition: csat_apis.c:42
ABC_DLL int Abc_NtkIvyProve(Abc_Ntk_t **ppNtk, void *pPars)
Definition: abcIvy.c:498
ABC_DLL 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)
FUNCTION DEFINITIONS ///.
Definition: abcSat.c:53
enum CSAT_StatusT status
Definition: csat_apis.h:123
static CSAT_Target_ResultT * ABC_TargetResAlloc(int nVars)
Definition: csat_apis.c:709
#define ABC_FREE(obj)
Definition: abc_global.h:232
#define assert(ex)
Definition: util_old.h:213
CSAT_Target_ResultT * pResult
Definition: csat_apis.c:53
void ABC_SolveInit ( ABC_Manager  mng)

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 []

Definition at line 570 of file csat_apis.c.

571 {
572  // check if the target is available
573  assert( mng->nog == Vec_PtrSize(mng->vNodes) );
574  if ( mng->nog == 0 )
575  { printf( "ABC_SolveInit: Target is not specified by ABC_AddTarget().\n" ); return; }
576 
577  // free the previous target network if present
578  if ( mng->pTarget ) Abc_NtkDelete( mng->pTarget );
579 
580  // set the new target network
581 // mng->pTarget = Abc_NtkCreateTarget( mng->pNtk, mng->vNodes, mng->vValues );
582  mng->pTarget = Abc_NtkStrash( mng->pNtk, 0, 1, 0 );
583 }
ABC_DLL Abc_Ntk_t * Abc_NtkStrash(Abc_Ntk_t *pNtk, int fAllNodes, int fCleanup, int fRecord)
Definition: abcStrash.c:265
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
ABC_DLL void Abc_NtkDelete(Abc_Ntk_t *pNtk)
Definition: abcNtk.c:1233
Vec_Ptr_t * vNodes
Definition: csat_apis.c:50
Abc_Ntk_t * pNtk
Definition: csat_apis.c:41
Abc_Ntk_t * pTarget
Definition: csat_apis.c:42
#define assert(ex)
Definition: util_old.h:213
void ABC_TargetResFree ( CSAT_Target_ResultT p)

Function*************************************************************

Synopsis [Deallocates the target result.]

Description []

SideEffects []

SeeAlso []

Definition at line 733 of file csat_apis.c.

734 {
735  if ( p == NULL )
736  return;
737  if( p->names )
738  {
739  int i = 0;
740  for ( i = 0; i < p->no_sig; i++ )
741  {
742  ABC_FREE(p->names[i]);
743  }
744  }
745  ABC_FREE( p->names );
746  ABC_FREE( p->values );
747  ABC_FREE( p );
748 }
#define ABC_FREE(obj)
Definition: abc_global.h:232
void ABC_UseOnlyCoreSatSolver ( ABC_Manager  mng)

Function*************************************************************

Synopsis [Sets solving mode by brute-force SAT.]

Description []

SideEffects []

SeeAlso []

Definition at line 155 of file csat_apis.c.

156 {
157  mng->mode = 1; // switch to "brute-force SAT" as the solving option
158 }
void CSAT_SetCaller ( ABC_Manager  mng,
enum CSAT_CallerT  caller 
)