ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Functions
cmdPlugin.c File Reference
#include <unistd.h>
#include "base/abc/abc.h"
#include "base/main/mainInt.h"
#include "cmd.h"
#include "cmdInt.h"
#include "misc/util/utilSignal.h"
Include dependency graph for cmdPlugin.c:

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START char * Abc_GetBinaryName (Abc_Frame_t *pAbc, int argc, char **argv)
 DECLARATIONS ///.
 
Vec_Str_t * Abc_ManReadFile (char *pFileName)
 
Vec_Int_t * Abc_ManReadBinary (char *pFileName, char *pToken)
 
int Abc_ManReadInteger (char *pFileName, char *pToken)
 
int Abc_ManReadStatus (char *pFileName, char *pToken)
 
Vec_Int_t * Abc_ManExpandCex (Gia_Man_t *pGia, Vec_Int_t *vCex)
 
Gia_Man_t * Abc_ManReadAig (char *pFileName, char *pToken)
 
int Cmd_CommandAbcPlugIn (Abc_Frame_t *pAbc, int argc, char **argv)
 
int Cmd_CommandAbcLoadPlugIn (Abc_Frame_t *pAbc, int argc, char **argv)
 

Function Documentation

◆ Abc_GetBinaryName()

ABC_NAMESPACE_IMPL_START char * Abc_GetBinaryName ( Abc_Frame_t * pAbc,
int argc,
char ** argv )

DECLARATIONS ///.

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

FileName [cmdPlugin.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Command processing package.]

Synopsis [Integrating external binary.]

Author [Alan Mishchenko, Niklas Een]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - September 29, 2010.]

Revision [

Id
cmdPlugin.c,v 1.00 2010/09/29 00:00:00 alanmi Exp

] FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 130 of file cmdPlugin.c.

131{
132 char * pTemp;
133 int i;
134 Vec_PtrForEachEntry( char *, pAbc->vPlugInComBinPairs, pTemp, i )
135 {
136 i++;
137 if ( strcmp( pTemp, argv[0] ) == 0 )
138 return (char *)Vec_PtrEntry( pAbc->vPlugInComBinPairs, i );
139 }
140 assert( 0 );
141 return NULL;
142}
assert
#define assert(ex)
Definition util_old.h:213
strcmp
int strcmp()
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecPtr.h:55
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Abc_ManExpandCex()

Vec_Int_t * Abc_ManExpandCex ( Gia_Man_t * pGia,
Vec_Int_t * vCex )

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

Synopsis [Work-around to insert 0s for PIs without fanout.]

Description []

SideEffects []

SeeAlso []

Definition at line 286 of file cmdPlugin.c.

287{
288 Vec_Int_t * vCexNew;
289 Gia_Obj_t * pObj;
290 int i, k;
291
292 // start with register outputs
293 vCexNew = Vec_IntAlloc( Vec_IntSize(vCex) );
294 Gia_ManForEachRo( pGia, pObj, i )
295 Vec_IntPush( vCexNew, 0 );
296
297 ABC_FREE( pGia->pRefs );
298 Gia_ManCreateRefs( pGia );
299 k = Gia_ManRegNum( pGia );
300 while ( 1 )
301 {
302 Gia_ManForEachPi( pGia, pObj, i )
303 {
304 if ( Gia_ObjRefNum(pGia, pObj) == 0 )
305 Vec_IntPush( vCexNew, 0 );
306 else
307 {
308 if ( k == Vec_IntSize(vCex) )
309 break;
310 Vec_IntPush( vCexNew, Vec_IntEntry(vCex, k++) );
311 }
312 }
313 if ( k == Vec_IntSize(vCex) )
314 break;
315 }
316 return vCexNew;
317}
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Gia_ManForEachRo
#define Gia_ManForEachRo(p, pObj, i)
Definition gia.h:1252
Gia_ManForEachPi
#define Gia_ManForEachPi(p, pObj, i)
Definition gia.h:1248
Gia_Obj_t
struct Gia_Obj_t_ Gia_Obj_t
Definition gia.h:76
Gia_ManCreateRefs
void Gia_ManCreateRefs(Gia_Man_t *p)
Definition giaUtil.c:779
Gia_Man_t_::pRefs
int * pRefs
Definition gia.h:118
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Abc_ManReadAig()

Gia_Man_t * Abc_ManReadAig ( char * pFileName,
char * pToken )

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

Synopsis [Derives AIG from the text string in the file.]

Description []

SideEffects []

SeeAlso []

Definition at line 359 of file cmdPlugin.c.

360{
361 Gia_Man_t * pGia = NULL;
362 unsigned nBinaryPart;
363 Vec_Str_t * vStr;
364 char * pStr, * pEnd;
365 vStr = Abc_ManReadFile( pFileName );
366 if ( vStr == NULL )
367 return NULL;
368 pStr = Vec_StrArray( vStr );
369 pStr = strstr( pStr, pToken );
370 if ( pStr != NULL )
371 {
372 // skip token
373 pStr += strlen(pToken);
374 // skip spaces
375 while ( *pStr == ' ' )
376 pStr++;
377 // set the end at newline
378 for ( pEnd = pStr; *pEnd; pEnd++ )
379 if ( *pEnd == '\r' || *pEnd == '\n' )
380 {
381 *pEnd = 0;
382 break;
383 }
384 // convert into binary AIGER
385 nBinaryPart = textToBin( pStr, strlen(pStr) );
386 // dump it into file
387 if ( 0 )
388 {
389 FILE * pFile = fopen( "test.aig", "wb" );
390 fwrite( pStr, 1, nBinaryPart, pFile );
391 fclose( pFile );
392 }
393 // derive AIG
394 pGia = Gia_AigerReadFromMemory( pStr, nBinaryPart, 0, 0, 0 );
395 }
396 Vec_StrFree( vStr );
397 return pGia;
398
399}
Vec_Str_t
struct Vec_Str_t_ Vec_Str_t
Definition bblif.c:46
Abc_ManReadFile
Vec_Str_t * Abc_ManReadFile(char *pFileName)
Definition cmdPlugin.c:155
Gia_AigerReadFromMemory
Gia_Man_t * Gia_AigerReadFromMemory(char *pContents, int nFileSize, int fGiaSimple, int fSkipStrash, int fCheck)
Definition giaAiger.c:176
Gia_Man_t
struct Gia_Man_t_ Gia_Man_t
Definition gia.h:96
strlen
int strlen()
strstr
char * strstr()
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Abc_ManReadBinary()

Vec_Int_t * Abc_ManReadBinary ( char * pFileName,
char * pToken )

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

Synopsis [Read flop map.]

Description []

SideEffects []

SeeAlso []

Definition at line 185 of file cmdPlugin.c.

186{
187 Vec_Int_t * vMap = NULL;
188 Vec_Str_t * vStr;
189 char * pStr;
190 int i, Length;
191 vStr = Abc_ManReadFile( pFileName );
192 if ( vStr == NULL )
193 return NULL;
194 pStr = Vec_StrArray( vStr );
195 pStr = strstr( pStr, pToken );
196 if ( pStr != NULL )
197 {
198 pStr += strlen( pToken );
199 vMap = Vec_IntAlloc( 100 );
200 Length = strlen( pStr );
201 for ( i = 0; i < Length; i++ )
202 {
203 if ( pStr[i] == '0' || pStr[i] == '?' )
204 Vec_IntPush( vMap, 0 );
205 else if ( pStr[i] == '1' )
206 Vec_IntPush( vMap, 1 );
207 if ( ('a' <= pStr[i] && pStr[i] <= 'z') ||
208 ('A' <= pStr[i] && pStr[i] <= 'Z') )
209 break;
210 }
211 }
212 Vec_StrFree( vStr );
213 return vMap;
214}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Abc_ManReadFile()

Vec_Str_t * Abc_ManReadFile ( char * pFileName)

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

Synopsis [Read flop map.]

Description []

SideEffects []

SeeAlso []

Definition at line 155 of file cmdPlugin.c.

156{
157 FILE * pFile;
158 Vec_Str_t * vStr;
159 int c;
160 pFile = fopen( pFileName, "r" );
161 if ( pFile == NULL )
162 {
163 printf( "Cannot open file \"%s\".\n", pFileName );
164 return NULL;
165 }
166 vStr = Vec_StrAlloc( 100 );
167 while ( (c = fgetc(pFile)) != EOF )
168 Vec_StrPush( vStr, (char)c );
169 Vec_StrPush( vStr, '\0' );
170 fclose( pFile );
171 return vStr;
172}
Here is the caller graph for this function:

◆ Abc_ManReadInteger()

int Abc_ManReadInteger ( char * pFileName,
char * pToken )

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

Synopsis [Read flop map.]

Description []

SideEffects []

SeeAlso []

Definition at line 227 of file cmdPlugin.c.

228{
229 int Result = -1;
230 Vec_Str_t * vStr;
231 char * pStr;
232 vStr = Abc_ManReadFile( pFileName );
233 if ( vStr == NULL )
234 return -1;
235 pStr = Vec_StrArray( vStr );
236 pStr = strstr( pStr, pToken );
237 if ( pStr != NULL )
238 Result = atoi( pStr + strlen(pToken) );
239 Vec_StrFree( vStr );
240 return Result;
241}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Abc_ManReadStatus()

int Abc_ManReadStatus ( char * pFileName,
char * pToken )

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

Synopsis [Read flop map.]

Description []

SideEffects []

SeeAlso []

Definition at line 254 of file cmdPlugin.c.

255{
256 int Result = -1;
257 Vec_Str_t * vStr;
258 char * pStr;
259 vStr = Abc_ManReadFile( pFileName );
260 if ( vStr == NULL )
261 return -1;
262 pStr = Vec_StrArray( vStr );
263 pStr = strstr( pStr, pToken );
264 if ( pStr != NULL )
265 {
266 if ( strncmp(pStr+8, "proved", 6) == 0 )
267 Result = 1;
268 else if ( strncmp(pStr+8, "failed", 6) == 0 )
269 Result = 0;
270 }
271 Vec_StrFree( vStr );
272 return Result;
273}
strncmp
int strncmp()
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Cmd_CommandAbcLoadPlugIn()

int Cmd_CommandAbcLoadPlugIn ( Abc_Frame_t * pAbc,
int argc,
char ** argv )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 631 of file cmdPlugin.c.

632{
633 int fPath, fVerbose;
634 int fd = -1, RetValue = -1, c;
635 FILE * pFile = NULL;
636 char * pStrDirBin = NULL, * pStrSection = NULL;
637 Vec_Str_t * sCommandLine = NULL;
638 char * pTempFile = NULL;
639 char pBuffer[1000];
640
641 // set defaults
642 fPath = 0;
643 fVerbose = 0;
644
645 Extra_UtilGetoptReset();
646 while ( ( c = Extra_UtilGetopt( argc, argv, "vph" ) ) != EOF )
647 {
648 switch ( c )
649 {
650 case 'p':
651 fPath ^= 1;
652 break;
653 case 'v':
654 fVerbose ^= 1;
655 break;
656 default:
657 goto usage;
658 }
659 }
660
661 if ( argc != globalUtilOptind + 2 )
662 goto usage;
663
664 pStrDirBin = argv[argc-2];
665 pStrSection = argv[argc-1];
666
667 // check if the file exists
668 if ( !fPath )
669 {
670 FILE* pFile = fopen( pStrDirBin, "r" );
671
672 if ( !pFile )
673 {
674 Abc_Print( ABC_ERROR, "Cannot run the binary \"%s\". File does not exist.\n", pStrDirBin );
675 goto cleanup;
676 }
677
678 fclose( pFile );
679 }
680
681 // create temp file
682 fd = Util_SignalTmpFile( "__abctmp_", ".txt", &pTempFile );
683
684 if ( fd == -1 )
685 {
686 Abc_Print( ABC_ERROR, "Cannot create a temporary file.\n" );
687 goto cleanup;
688 }
689
690#ifdef WIN32
691 _close( fd );
692#else
693 close( fd );
694#endif
695
696 // get command list
697 sCommandLine = Vec_StrAlloc(1000);
698
699 Vec_StrPrintF(sCommandLine, "%s -abc -list-commands > %s", pStrDirBin, pTempFile );
700 Vec_StrPush(sCommandLine, '\0');
701
702 if(fVerbose)
703 {
704 Abc_Print(ABC_VERBOSE, "Running command %s\n", Vec_StrArray(sCommandLine));
705 }
706
707 RetValue = Util_SignalSystem( Vec_StrArray(sCommandLine) );
708
709 if ( RetValue != 0 )
710 {
711 Abc_Print( ABC_ERROR, "Command \"%s\" failed.\n", Vec_StrArray(sCommandLine) );
712 goto cleanup;
713 }
714
715 // create commands
716 pFile = fopen( pTempFile, "r" );
717
718 if ( pFile == NULL )
719 {
720 Abc_Print( -1, "Cannot open file with the list of commands.\n" );
721
722 RetValue = -1;
723 goto cleanup;
724 }
725
726 while ( fgets( pBuffer, 1000, pFile ) != NULL )
727 {
728 if ( pBuffer[strlen(pBuffer)-1] == '\n' )
729 pBuffer[strlen(pBuffer)-1] = 0;
730
731 Cmd_CommandAdd( pAbc, pStrSection, pBuffer, Cmd_CommandAbcPlugIn, 1 );
732
733 Vec_PtrPush( pAbc->vPlugInComBinPairs, Extra_UtilStrsav(pBuffer) );
734 Vec_PtrPush( pAbc->vPlugInComBinPairs, Extra_UtilStrsav(pStrDirBin) );
735
736 if ( fVerbose )
737 {
738 Abc_Print(ABC_VERBOSE, "Creating command %s with binary %s\n", pBuffer, pStrDirBin);
739 }
740 }
741
742cleanup:
743
744 if( pFile )
745 fclose( pFile );
746
747 if( pTempFile )
748 Util_SignalTmpFileRemove( pTempFile, 0 );
749
750 Vec_StrFreeP(&sCommandLine);
751
752 ABC_FREE( pTempFile );
753
754 return RetValue;
755
756usage:
757
758 Abc_Print( -2, "usage: load_plugin [-pvh] <plugin_dir\\binary_name> <section_name>\n" );
759 Abc_Print( -2, "\t loads external binary as a plugin\n" );
760 Abc_Print( -2, "\t-p : toggle searching the command in PATH [default = %s].\n", fPath? "yes": "no" );
761 Abc_Print( -2, "\t-v : enable verbose output [default = %s].\n", fVerbose? "yes": "no" );
762 Abc_Print( -2, "\t-h : print the command usage\n");
763
764 return 1;
765}
ABC_ERROR
@ ABC_ERROR
Definition abc_global.h:376
ABC_VERBOSE
@ ABC_VERBOSE
Definition abc_global.h:379
Cmd_CommandAbcPlugIn
int Cmd_CommandAbcPlugIn(Abc_Frame_t *pAbc, int argc, char **argv)
Definition cmdPlugin.c:412
Cmd_CommandAdd
void Cmd_CommandAdd(Abc_Frame_t *pAbc, const char *sGroup, const char *sName, Cmd_CommandFuncType pFunc, int fChanges)
Definition cmdApi.c:63
globalUtilOptind
int globalUtilOptind
Definition extraUtilUtil.c:45
Extra_UtilStrsav
char * Extra_UtilStrsav(const char *s)
Definition extraUtilUtil.c:179
Extra_UtilGetopt
int Extra_UtilGetopt(int argc, char *argv[], const char *optstring)
Definition extraUtilUtil.c:98
Extra_UtilGetoptReset
ABC_DLL void Extra_UtilGetoptReset()
Definition extraUtilUtil.c:80
usage
usage()
Definition main.c:626
Util_SignalSystem
ABC_NAMESPACE_IMPL_START int Util_SignalSystem(const char *cmd)
DECLARATIONS ///.
Definition utilSignal.c:44
Util_SignalTmpFileRemove
void Util_SignalTmpFileRemove(const char *fname, int fLeave)
Definition utilSignal.c:60
Util_SignalTmpFile
int Util_SignalTmpFile(const char *prefix, const char *suffix, char **out_name)
INCLUDES ///.
Definition utilSignal.c:55
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Cmd_CommandAbcPlugIn()

int Cmd_CommandAbcPlugIn ( Abc_Frame_t * pAbc,
int argc,
char ** argv )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 412 of file cmdPlugin.c.

413{
414 char * pFileIn, * pFileOut;
415 Vec_Str_t * vCommand;
416 Vec_Int_t * vCex;
417 FILE * pFile;
418 Gia_Man_t * pGia;
419 int i, fd;
420 abctime clk;
421 int fLeaveFiles;
422/*
423 Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
424 if ( pNtk == NULL )
425 {
426 Abc_Print( -1, "Current network does not exist\n" );
427 return 1;
428 }
429 if ( !Abc_NtkIsStrash( pNtk) )
430 {
431 Abc_Print( -1, "The current network is not an AIG. Cannot continue.\n" );
432 return 1;
433 }
434*/
435
436 if ( pAbc->pGia == NULL )
437 {
438 if (argc == 2 && strcmp(argv[1], "-h") == 0)
439 {
440 // Run command to produce help string:
441 vCommand = Vec_StrAlloc( 100 );
442 Vec_StrAppend( vCommand, Abc_GetBinaryName( pAbc, argc, argv ) );
443 Vec_StrAppend( vCommand, " -abc " );
444 Vec_StrAppend( vCommand, argv[0] );
445 Vec_StrAppend( vCommand, " -h" );
446 Vec_StrPush( vCommand, 0 );
447 Util_SignalSystem( Vec_StrArray(vCommand) );
448 Vec_StrFree( vCommand );
449 }
450 else
451 {
452 Abc_Print( -1, "Current AIG does not exist (try command &ps).\n" );
453 }
454 return 1;
455 }
456
457 // create temp file
458 fd = Util_SignalTmpFile( "__abctmp_", ".aig", &pFileIn );
459 if ( fd == -1 )
460 {
461 Abc_Print( -1, "Cannot create a temporary file.\n" );
462 return 1;
463 }
464#ifdef WIN32
465 _close( fd );
466#else
467 close( fd );
468#endif
469
470 // create temp file
471 fd = Util_SignalTmpFile( "__abctmp_", ".out", &pFileOut );
472 if ( fd == -1 )
473 {
474 ABC_FREE( pFileIn );
475 Abc_Print( -1, "Cannot create a temporary file.\n" );
476 return 1;
477 }
478#ifdef WIN32
479 _close( fd );
480#else
481 close( fd );
482#endif
483
484
485 // write current network into a file
486/*
487 {
488 extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
489 Aig_Man_t * pAig;
490 pAig = Abc_NtkToDar( pNtk, 0, 1 );
491 Ioa_WriteAiger( pAig, pFileIn, 0, 0 );
492 Aig_ManStop( pAig );
493 }
494*/
495 // check what to do with the files
496 fLeaveFiles = 0;
497 if ( strcmp( argv[argc-1], "!" ) == 0 )
498 {
499 Abc_Print( 0, "Input file \"%s\" and output file \"%s\" are not deleted.\n", pFileIn, pFileOut );
500 fLeaveFiles = 1;
501 argc--;
502 }
503
504 // create input file
505 Gia_AigerWrite( pAbc->pGia, pFileIn, 0, 0, 0 );
506
507 // create command line
508 vCommand = Vec_StrAlloc( 100 );
509 Vec_StrAppend( vCommand, Abc_GetBinaryName( pAbc, argc, argv ) );
510 // add input/output file
511 Vec_StrAppend( vCommand, " -abc" );
512// Vec_StrAppend( vCommand, " -input=C:/_projects/abc/_TEST/hwmcc/139442p0.aig" );
513 Vec_StrAppend( vCommand, " -input=" );
514 Vec_StrAppend( vCommand, pFileIn );
515 Vec_StrAppend( vCommand, " -output=" );
516 Vec_StrAppend( vCommand, pFileOut );
517 // add other arguments
518 for ( i = 0; i < argc; i++ )
519 {
520 Vec_StrAppend( vCommand, " " );
521 Vec_StrAppend( vCommand, argv[i] );
522 }
523 Vec_StrPush( vCommand, 0 );
524
525 // run the command line
526//printf( "Running command line: %s\n", Vec_StrArray(vCommand) );
527
528 clk = Abc_Clock();
529 if ( Util_SignalSystem( Vec_StrArray(vCommand) ) )
530 {
531 Abc_Print( -1, "The following command has returned non-zero exit status:\n" );
532 Abc_Print( -1, "\"%s\"\n", Vec_StrArray(vCommand) );
533 return 1;
534 }
535 clk = Abc_Clock() - clk;
536 Vec_StrFree( vCommand );
537
538 // check if the output file exists
539 if ( (pFile = fopen( pFileOut, "r" )) == NULL )
540 {
541 Abc_Print( -1, "There is no output file \"%s\".\n", pFileOut );
542 return 1;
543 }
544 fclose( pFile );
545
546 // process the output
547 if ( Extra_FileSize(pFileOut) > 0 )
548 {
549 // get status
550 pAbc->Status = Abc_ManReadStatus( pFileOut, "result:" );
551 // get bug-free depth
552 pAbc->nFrames = Abc_ManReadInteger( pFileOut, "bug-free-depth:" );
553 // get abstraction
554 pAbc->pGia->vFlopClasses = Abc_ManReadBinary( pFileOut, "abstraction:" );
555 // get counter-example
556 vCex = Abc_ManReadBinary( pFileOut, "counter-example:" );
557 if ( vCex )
558 {
559 int nFrames, nRemain;
560
561 nFrames = (Vec_IntSize(vCex) - Gia_ManRegNum(pAbc->pGia)) / Gia_ManPiNum(pAbc->pGia);
562 nRemain = (Vec_IntSize(vCex) - Gia_ManRegNum(pAbc->pGia)) % Gia_ManPiNum(pAbc->pGia);
563 if ( nRemain != 0 )
564 {
565 Vec_Int_t * vTemp;
566 Abc_Print( 1, "Adjusting counter-example by adding zeros for PIs without fanout.\n" );
567 // expand the counter-example to include PIs without fanout
568 vCex = Abc_ManExpandCex( pAbc->pGia, vTemp = vCex );
569 Vec_IntFree( vTemp );
570 }
571
572 nFrames = (Vec_IntSize(vCex) - Gia_ManRegNum(pAbc->pGia)) / Gia_ManPiNum(pAbc->pGia);
573 nRemain = (Vec_IntSize(vCex) - Gia_ManRegNum(pAbc->pGia)) % Gia_ManPiNum(pAbc->pGia);
574 if ( nRemain != 0 )
575 Abc_Print( 1, "Counter example has a wrong length.\n" );
576 else
577 {
578 Abc_Print( 1, "Problem is satisfiable. Found counter-example in frame %d. ", nFrames-1 );
579 Abc_PrintTime( 1, "Time", clk );
580 ABC_FREE( pAbc->pCex );
581 pAbc->pCex = Abc_CexCreate( Gia_ManRegNum(pAbc->pGia), Gia_ManPiNum(pAbc->pGia), Vec_IntArray(vCex), nFrames-1, 0, 0 );
582
583// Abc_CexPrint( pAbc->pCex );
584
585// if ( !Gia_ManVerifyCex( pAbc->pGia, pAbc->pCex, 0 ) )
586// Abc_Print( 1, "Generated counter-example is INVALID.\n" );
587
588 // remporary work-around to detect the output number - October 18, 2010
589 pAbc->pCex->iPo = Gia_ManFindFailedPoCex( pAbc->pGia, pAbc->pCex, 0 );
590 if ( pAbc->pCex->iPo == -1 )
591 {
592 Abc_Print( 1, "Generated counter-example is INVALID.\n" );
593 ABC_FREE( pAbc->pCex );
594 }
595 else
596 {
597 Abc_Print( 1, "Returned counter-example successfully verified in ABC.\n" );
598 }
599 }
600 Vec_IntFreeP( &vCex );
601 }
602 // get AIG if present
603 pGia = Abc_ManReadAig( pFileOut, "aig:" );
604 if ( pGia != NULL )
605 {
606 Gia_ManStopP( &pAbc->pGia );
607 pAbc->pGia = pGia;
608 }
609 }
610
611 // clean up
612 Util_SignalTmpFileRemove( pFileIn, fLeaveFiles );
613 Util_SignalTmpFileRemove( pFileOut, fLeaveFiles );
614
615 ABC_FREE( pFileIn );
616 ABC_FREE( pFileOut );
617 return 0;
618}
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
Abc_ManExpandCex
Vec_Int_t * Abc_ManExpandCex(Gia_Man_t *pGia, Vec_Int_t *vCex)
Definition cmdPlugin.c:286
Abc_ManReadInteger
int Abc_ManReadInteger(char *pFileName, char *pToken)
Definition cmdPlugin.c:227
Abc_ManReadStatus
int Abc_ManReadStatus(char *pFileName, char *pToken)
Definition cmdPlugin.c:254
Abc_ManReadBinary
Vec_Int_t * Abc_ManReadBinary(char *pFileName, char *pToken)
Definition cmdPlugin.c:185
Abc_ManReadAig
Gia_Man_t * Abc_ManReadAig(char *pFileName, char *pToken)
Definition cmdPlugin.c:359
Abc_GetBinaryName
ABC_NAMESPACE_IMPL_START char * Abc_GetBinaryName(Abc_Frame_t *pAbc, int argc, char **argv)
DECLARATIONS ///.
Definition cmdPlugin.c:130
Extra_FileSize
int Extra_FileSize(char *pFileName)
Definition extraUtilFile.c:327
Gia_ManFindFailedPoCex
int Gia_ManFindFailedPoCex(Gia_Man_t *pAig, Abc_Cex_t *p, int nOutputs)
Definition giaCex.c:91
Gia_ManStopP
void Gia_ManStopP(Gia_Man_t **p)
Definition giaMan.c:224
Gia_AigerWrite
void Gia_AigerWrite(Gia_Man_t *p, char *pFileName, int fWriteSymbols, int fCompact, int fWriteNewLine)
Definition giaAiger.c:1595
Abc_CexCreate
Abc_Cex_t * Abc_CexCreate(int nRegs, int nPis, int *pArray, int iFrame, int iPo, int fSkipRegs)
Definition utilCex.c:110
Here is the call graph for this function:
Here is the caller graph for this function: