ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Classes | Macros | Typedefs | Enumerations | Functions
wlcReadSmt.c File Reference
#include "wlc.h"
#include "misc/vec/vecWec.h"
Include dependency graph for wlcReadSmt.c:

Go to the source code of this file.

Classes

struct  Smt_Prs_t_
 
struct  Smt_Pair_t_
 

Macros

#define SMT_GLO_SUFFIX   ""
 
#define Smt_ManForEachDir(p, Type, vVec, i)
 

Typedefs

typedef typedefABC_NAMESPACE_IMPL_START struct Smt_Prs_t_ Smt_Prs_t
 DECLARATIONS ///.
 
typedef struct Smt_Pair_t_ Smt_Pair_t
 

Enumerations

enum  Smt_LineType_t {
  SMT_PRS_NONE = 0 , SMT_PRS_SET_OPTION , SMT_PRS_SET_LOGIC , SMT_PRS_SET_INFO ,
  SMT_PRS_DEFINE_FUN , SMT_PRS_DECLARE_FUN , SMT_PRS_ASSERT , SMT_PRS_LET ,
  SMT_PRS_CHECK_SAT , SMT_PRS_GET_VALUE , SMT_PRS_EXIT , SMT_PRS_END
}
 

Functions

int Smt_PrsBuildNode (Wlc_Ntk_t *pNtk, Smt_Prs_t *p, int iNode, int RangeOut, char *pName)
 
Wlc_Ntk_t * Smt_PrsBuild (Smt_Prs_t *p)
 
char * Smt_PrsGenName (Smt_Prs_t *p)
 
int Smt_PrsBuild2_rec (Wlc_Ntk_t *pNtk, Smt_Prs_t *p, int iNode, int iObjPrev, char *pName)
 
Wlc_Ntk_t * Smt_PrsBuild2 (Smt_Prs_t *p)
 
void Smt_PrsReadLines (Smt_Prs_t *p)
 
void Smt_PrsPrintParser_rec (Smt_Prs_t *p, int iObj, int Depth)
 
void Smt_PrsPrintParser (Smt_Prs_t *p)
 
Wlc_Ntk_t * Wlc_ReadSmtBuffer (char *pFileName, char *pBuffer, char *pLimit, int fOldParser, int fPrintTree)
 
Wlc_Ntk_t * Wlc_ReadSmt (char *pFileName, int fOldParser, int fPrintTree)
 

Macro Definition Documentation

◆ SMT_GLO_SUFFIX

#define SMT_GLO_SUFFIX   ""

Definition at line 52 of file wlcReadSmt.c.

◆ Smt_ManForEachDir

#define Smt_ManForEachDir ( p,
Type,
vVec,
i )
Value:
for ( i = 0; (i < Vec_WecSize(&p->vObjs)) && (((vVec) = Vec_WecEntry(&p->vObjs, i)), 1); i++ ) \
if ( !Smt_VecEntryIsType(vVec, 0, Type) ) {} else
p
Cube * p
Definition exorList.c:222

Definition at line 115 of file wlcReadSmt.c.

115#define Smt_ManForEachDir( p, Type, vVec, i ) \
116 for ( i = 0; (i < Vec_WecSize(&p->vObjs)) && (((vVec) = Vec_WecEntry(&p->vObjs, i)), 1); i++ ) \
117 if ( !Smt_VecEntryIsType(vVec, 0, Type) ) {} else

Typedef Documentation

◆ Smt_Pair_t

typedef struct Smt_Pair_t_ Smt_Pair_t

Definition at line 70 of file wlcReadSmt.c.

◆ Smt_Prs_t

typedef typedefABC_NAMESPACE_IMPL_START struct Smt_Prs_t_ Smt_Prs_t

DECLARATIONS ///.

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

FileName [wlcParse.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Verilog parser.]

Synopsis [Parses several flavors of word-level Verilog.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - August 22, 2014.]

Revision [

Id
wlcParse.c,v 1.00 2014/09/12 00:00:00 alanmi Exp

]

Definition at line 31 of file wlcReadSmt.c.

Enumeration Type Documentation

◆ Smt_LineType_t

enum Smt_LineType_t
Enumerator
SMT_PRS_NONE 
SMT_PRS_SET_OPTION 
SMT_PRS_SET_LOGIC 
SMT_PRS_SET_INFO 
SMT_PRS_DEFINE_FUN 
SMT_PRS_DECLARE_FUN 
SMT_PRS_ASSERT 
SMT_PRS_LET 
SMT_PRS_CHECK_SAT 
SMT_PRS_GET_VALUE 
SMT_PRS_EXIT 
SMT_PRS_END 

Definition at line 55 of file wlcReadSmt.c.

55 {
56 SMT_PRS_NONE = 0,
57 SMT_PRS_SET_OPTION,
58 SMT_PRS_SET_LOGIC,
59 SMT_PRS_SET_INFO,
60 SMT_PRS_DEFINE_FUN,
61 SMT_PRS_DECLARE_FUN,
62 SMT_PRS_ASSERT,
63 SMT_PRS_LET,
64 SMT_PRS_CHECK_SAT,
65 SMT_PRS_GET_VALUE,
66 SMT_PRS_EXIT,
67 SMT_PRS_END
68} Smt_LineType_t;
Smt_LineType_t
Smt_LineType_t
Definition wlcReadSmt.c:55
SMT_PRS_NONE
@ SMT_PRS_NONE
Definition wlcReadSmt.c:56
SMT_PRS_DEFINE_FUN
@ SMT_PRS_DEFINE_FUN
Definition wlcReadSmt.c:60
SMT_PRS_SET_OPTION
@ SMT_PRS_SET_OPTION
Definition wlcReadSmt.c:57
SMT_PRS_SET_INFO
@ SMT_PRS_SET_INFO
Definition wlcReadSmt.c:59
SMT_PRS_LET
@ SMT_PRS_LET
Definition wlcReadSmt.c:63
SMT_PRS_END
@ SMT_PRS_END
Definition wlcReadSmt.c:67
SMT_PRS_ASSERT
@ SMT_PRS_ASSERT
Definition wlcReadSmt.c:62
SMT_PRS_DECLARE_FUN
@ SMT_PRS_DECLARE_FUN
Definition wlcReadSmt.c:61
SMT_PRS_SET_LOGIC
@ SMT_PRS_SET_LOGIC
Definition wlcReadSmt.c:58
SMT_PRS_EXIT
@ SMT_PRS_EXIT
Definition wlcReadSmt.c:66
SMT_PRS_GET_VALUE
@ SMT_PRS_GET_VALUE
Definition wlcReadSmt.c:65
SMT_PRS_CHECK_SAT
@ SMT_PRS_CHECK_SAT
Definition wlcReadSmt.c:64

Function Documentation

◆ Smt_PrsBuild()

Wlc_Ntk_t * Smt_PrsBuild ( Smt_Prs_t * p)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 799 of file wlcReadSmt.c.

800{
801 Wlc_Ntk_t * pNtk;
802 Vec_Int_t * vFans, * vFans2, * vFans3;
803 Vec_Int_t * vAsserts = Vec_IntAlloc(100);
804 char * pName, * pRange, * pValue;
805 int i, k, Fan, Fan3, iObj, Status, Range, NameId, nBits = 0;
806 // issue warnings about unknown dirs
807 vFans = Vec_WecEntry( &p->vObjs, 0 );
808 Vec_IntForEachEntry( vFans, Fan, i )
809 {
810 assert( !Smt_EntryIsName(Fan) );
811 vFans2 = Smt_VecEntryNode( p, vFans, i );
812 Fan = Vec_IntEntry(vFans2, 0);
813 assert( Smt_EntryIsName(Fan) );
814 if ( Abc_Lit2Var(Fan) >= SMT_PRS_END )
815 printf( "Ignoring directive \"%s\".\n", Smt_EntryName(p, Fan) );
816 }
817 // start network and create primary inputs
818 pNtk = Wlc_NtkAlloc( p->pName, 1000 );
819 pNtk->pManName = Abc_NamStart( 1000, 24 );
820 pNtk->fSmtLib = 1;
821 Smt_ManForEachDir( p, SMT_PRS_DECLARE_FUN, vFans, i )
822 {
823 assert( Vec_IntSize(vFans) == 4 );
824 assert( Smt_VecEntryIsType(vFans, 0, SMT_PRS_DECLARE_FUN) );
825 // get name
826 Fan = Vec_IntEntry(vFans, 1);
827 assert( Smt_EntryIsName(Fan) );
828 pName = Smt_EntryName(p, Fan);
829 // skip ()
830 Fan = Vec_IntEntry(vFans, 2);
831 assert( !Smt_EntryIsName(Fan) );
832 // check type (Bool or BitVec)
833 Fan = Vec_IntEntry(vFans, 3);
834 if ( Smt_EntryIsName(Fan) )
835 {
836 //(declare-fun s1 () Bool)
837 assert( !strcmp("Bool", Smt_VecEntryName(p, vFans, 3)) );
838 Range = 1;
839 }
840 else
841 {
842 // (declare-fun s1 () (_ BitVec 64))
843 // get range
844 Fan = Vec_IntEntry(vFans, 3);
845 assert( !Smt_EntryIsName(Fan) );
846 vFans2 = Smt_EntryNode(p, Fan);
847 assert( Vec_IntSize(vFans2) == 3 );
848 assert( !strcmp("_", Smt_VecEntryName(p, vFans2, 0)) );
849 assert( !strcmp("BitVec", Smt_VecEntryName(p, vFans2, 1)) );
850 Fan = Vec_IntEntry(vFans2, 2);
851 assert( Smt_EntryIsName(Fan) );
852 pRange = Smt_EntryName(p, Fan);
853 Range = atoi(pRange);
854 }
855 // create node
856 iObj = Wlc_ObjAlloc( pNtk, WLC_OBJ_PI, 0, Range-1, 0 );
857 NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pName, NULL );
858 assert( iObj == NameId );
859 // save values
860 Vec_IntPush( &pNtk->vValues, NameId );
861 Vec_IntPush( &pNtk->vValues, nBits );
862 Vec_IntPush( &pNtk->vValues, Range );
863 nBits += Range;
864 }
865 // create constants
866 Smt_ManForEachDir( p, SMT_PRS_DEFINE_FUN, vFans, i )
867 {
868 assert( Vec_IntSize(vFans) == 5 );
869 assert( Smt_VecEntryIsType(vFans, 0, SMT_PRS_DEFINE_FUN) );
870 // get name
871 Fan = Vec_IntEntry(vFans, 1);
872 assert( Smt_EntryIsName(Fan) );
873 pName = Smt_EntryName(p, Fan);
874 // skip ()
875 Fan = Vec_IntEntry(vFans, 2);
876 assert( !Smt_EntryIsName(Fan) );
877 // check type (Bool or BitVec)
878 Fan = Vec_IntEntry(vFans, 3);
879 if ( Smt_EntryIsName(Fan) )
880 {
881 // (define-fun s_2 () Bool false)
882 assert( !strcmp("Bool", Smt_VecEntryName(p, vFans, 3)) );
883 Range = 1;
884 pValue = Smt_VecEntryName(p, vFans, 4);
885 if ( !strcmp("false", pValue) )
886 pValue = "#b0";
887 else if ( !strcmp("true", pValue) )
888 pValue = "#b1";
889 else assert( 0 );
890 Status = Smt_PrsBuildConstant( pNtk, pValue, Range, pName );
891 }
892 else
893 {
894 // (define-fun s702 () (_ BitVec 4) #xe)
895 // (define-fun s1 () (_ BitVec 8) (bvneg #x7f))
896 // get range
897 Fan = Vec_IntEntry(vFans, 3);
898 assert( !Smt_EntryIsName(Fan) );
899 vFans2 = Smt_VecEntryNode(p, vFans, 3);
900 assert( Vec_IntSize(vFans2) == 3 );
901 assert( !strcmp("_", Smt_VecEntryName(p, vFans2, 0)) );
902 assert( !strcmp("BitVec", Smt_VecEntryName(p, vFans2, 1)) );
903 // get range
904 Fan = Vec_IntEntry(vFans2, 2);
905 assert( Smt_EntryIsName(Fan) );
906 pRange = Smt_EntryName(p, Fan);
907 Range = atoi(pRange);
908 // get constant
909 Fan = Vec_IntEntry(vFans, 4);
910 Status = Smt_PrsBuildNode( pNtk, p, Fan, Range, pName );
911 }
912 if ( !Status )
913 {
914 Wlc_NtkFree( pNtk ); pNtk = NULL;
915 goto finish;
916 }
917 }
918 // process let-statements
919 Smt_ManForEachDir( p, SMT_PRS_LET, vFans, i )
920 {
921 // let ((s35550 (bvor s48 s35549)))
922 assert( Vec_IntSize(vFans) == 3 );
923 assert( Smt_VecEntryIsType(vFans, 0, SMT_PRS_LET) );
924 // get parts
925 Fan = Vec_IntEntry(vFans, 1);
926 assert( !Smt_EntryIsName(Fan) );
927 vFans2 = Smt_EntryNode(p, Fan);
928 if ( Smt_VecEntryIsType(vFans2, 0, SMT_PRS_LET) )
929 continue;
930 // iterate through the parts
931 Vec_IntForEachEntry( vFans2, Fan, k )
932 {
933 // s35550 (bvor s48 s35549)
934 Fan = Vec_IntEntry(vFans2, 0);
935 assert( !Smt_EntryIsName(Fan) );
936 vFans3 = Smt_EntryNode(p, Fan);
937 // get the name
938 Fan3 = Vec_IntEntry(vFans3, 0);
939 assert( Smt_EntryIsName(Fan3) );
940 pName = Smt_EntryName(p, Fan3);
941 // get function
942 Fan3 = Vec_IntEntry(vFans3, 1);
943 assert( !Smt_EntryIsName(Fan3) );
944 Status = Smt_PrsBuildNode( pNtk, p, Fan3, -1, pName );
945 if ( !Status )
946 {
947 Wlc_NtkFree( pNtk ); pNtk = NULL;
948 goto finish;
949 }
950 }
951 }
952 // process assert-statements
953 Vec_IntClear( vAsserts );
954 Smt_ManForEachDir( p, SMT_PRS_ASSERT, vFans, i )
955 {
956 //(assert ; no quantifiers
957 // (let ((s2 (bvsge s0 s1)))
958 // (not s2)))
959 //(assert (not (= s0 #x00)))
960 assert( Vec_IntSize(vFans) == 2 );
961 assert( Smt_VecEntryIsType(vFans, 0, SMT_PRS_ASSERT) );
962 // get second directive
963 Fan = Vec_IntEntry(vFans, 1);
964 if ( !Smt_EntryIsName(Fan) )
965 {
966 // find the final let-statement
967 vFans2 = Smt_VecEntryNode(p, vFans, 1);
968 while ( Smt_VecEntryIsType(vFans2, 0, SMT_PRS_LET) )
969 {
970 Fan = Vec_IntEntry(vFans2, 2);
971 if ( Smt_EntryIsName(Fan) )
972 break;
973 vFans2 = Smt_VecEntryNode(p, vFans2, 2);
974 }
975 }
976 // find name or create node
977 iObj = Smt_PrsBuildNode( pNtk, p, Fan, -1, NULL );
978 if ( !iObj )
979 {
980 Wlc_NtkFree( pNtk ); pNtk = NULL;
981 goto finish;
982 }
983 Vec_IntPush( vAsserts, iObj );
984 }
985 // build AND of asserts
986 if ( Vec_IntSize(vAsserts) == 1 )
987 iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_BUF, 0, 1, vAsserts, "miter_output" );
988 else
989 {
990 iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_BIT_CONCAT, 0, Vec_IntSize(vAsserts), vAsserts, NULL );
991 Vec_IntFill( vAsserts, 1, iObj );
992 iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_REDUCT_AND, 0, 1, vAsserts, "miter_output" );
993 }
994 Wlc_ObjSetCo( pNtk, Wlc_NtkObj(pNtk, iObj), 0 );
995 // create nameIDs
996 vFans = Vec_IntStartNatural( Wlc_NtkObjNumMax(pNtk) );
997 Vec_IntAppend( &pNtk->vNameIds, vFans );
998 Vec_IntFree( vFans );
999 //Wlc_NtkReport( pNtk, NULL );
1000finish:
1001 // cleanup
1002 Vec_IntFree(vAsserts);
1003 return pNtk;
1004}
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Wlc_Ntk_t_::fSmtLib
int fSmtLib
Definition wlc.h:151
Wlc_Ntk_t_::pManName
Abc_Nam_t * pManName
Definition wlc.h:165
Wlc_Ntk_t_::vValues
Vec_Int_t vValues
Definition wlc.h:167
Wlc_Ntk_t_::vNameIds
Vec_Int_t vNameIds
Definition wlc.h:166
Abc_NamStrFindOrAdd
int Abc_NamStrFindOrAdd(Abc_Nam_t *p, char *pStr, int *pfFound)
Definition utilNam.c:453
Abc_NamStart
Abc_Nam_t * Abc_NamStart(int nObjs, int nAveSize)
FUNCTION DEFINITIONS ///.
Definition utilNam.c:80
assert
#define assert(ex)
Definition util_old.h:213
strcmp
int strcmp()
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Smt_PrsBuildNode
int Smt_PrsBuildNode(Wlc_Ntk_t *pNtk, Smt_Prs_t *p, int iNode, int RangeOut, char *pName)
Definition wlcReadSmt.c:667
Smt_ManForEachDir
#define Smt_ManForEachDir(p, Type, vVec, i)
Definition wlcReadSmt.c:115
Wlc_ObjAlloc
int Wlc_ObjAlloc(Wlc_Ntk_t *p, int Type, int Signed, int End, int Beg)
Definition wlcNtk.c:199
Wlc_ObjSetCo
void Wlc_ObjSetCo(Wlc_Ntk_t *p, Wlc_Obj_t *pObj, int fFlopInput)
Definition wlcNtk.c:188
Wlc_NtkAlloc
Wlc_Ntk_t * Wlc_NtkAlloc(char *pName, int nObjsAlloc)
Definition wlcNtk.c:152
Wlc_NtkFree
void Wlc_NtkFree(Wlc_Ntk_t *p)
Definition wlcNtk.c:253
Wlc_Ntk_t
struct Wlc_Ntk_t_ Wlc_Ntk_t
Definition wlc.h:135
WLC_OBJ_BUF
@ WLC_OBJ_BUF
Definition wlc.h:52
WLC_OBJ_REDUCT_AND
@ WLC_OBJ_REDUCT_AND
Definition wlc.h:82
WLC_OBJ_PI
@ WLC_OBJ_PI
Definition wlc.h:46
WLC_OBJ_BIT_CONCAT
@ WLC_OBJ_BIT_CONCAT
Definition wlc.h:68
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Smt_PrsBuild2()

Wlc_Ntk_t * Smt_PrsBuild2 ( Smt_Prs_t * p)

Definition at line 1257 of file wlcReadSmt.c.

1258{
1259 Wlc_Ntk_t * pNtk;
1260 Vec_Int_t * vFansRoot, * vFans, * vFans2;
1261 Vec_Int_t * vAsserts = Vec_IntAlloc(100);
1262 int i, Root, Fan, iObj, NameId, Range, nBits = 0;
1263 char * pName, * pRange;
1264 // start network and create primary inputs
1265 pNtk = Wlc_NtkAlloc( p->pName, 1000 );
1266 pNtk->pManName = Abc_NamStart( 1000, 24 );
1267 pNtk->fSmtLib = 1;
1268 // collect top-level asserts
1269 vFansRoot = Vec_WecEntry( &p->vObjs, 0 );
1270 Vec_IntForEachEntry( vFansRoot, Root, i )
1271 {
1272 assert( !Smt_EntryIsName(Root) );
1273 vFans = Smt_VecEntryNode( p, vFansRoot, i );
1274 Fan = Vec_IntEntry(vFans, 0);
1275 assert( Smt_EntryIsName(Fan) );
1276 // create variables
1277 if ( Abc_Lit2Var(Fan) == SMT_PRS_DECLARE_FUN )
1278 {
1279 char * pName_glb;
1280 assert( Vec_IntSize(vFans) == 4 );
1281 assert( Smt_VecEntryIsType(vFans, 0, SMT_PRS_DECLARE_FUN) );
1282 // get name
1283 Fan = Vec_IntEntry(vFans, 1);
1284 assert( Smt_EntryIsName(Fan) );
1285 pName = Smt_EntryName(p, Fan);
1286 // added: giving a global suffix
1287 pName_glb = (char *) malloc(strlen(pName) + 4 + 1);
1288 strcpy(pName_glb,pName);
1289 strcat(pName_glb,SMT_GLO_SUFFIX);
1290 // FIXME: delete memory of pName
1291 pName = pName_glb;
1292 // skip ()
1293 Fan = Vec_IntEntry(vFans, 2);
1294 assert( !Smt_EntryIsName(Fan) );
1295 // check type (Bool or BitVec)
1296 Fan = Vec_IntEntry(vFans, 3);
1297 if ( Smt_EntryIsName(Fan) )
1298 { //(declare-fun s1 () Bool)
1299 assert( !strcmp("Bool", Smt_VecEntryName(p, vFans, 3)) );
1300 Range = 1;
1301 }
1302 else
1303 { // (declare-fun s1 () (_ BitVec 64))
1304 Fan = Vec_IntEntry(vFans, 3);
1305 assert( !Smt_EntryIsName(Fan) );
1306 vFans2 = Smt_EntryNode(p, Fan);
1307 assert( Vec_IntSize(vFans2) == 3 );
1308 assert( !strcmp("_", Smt_VecEntryName(p, vFans2, 0)) );
1309 assert( !strcmp("BitVec", Smt_VecEntryName(p, vFans2, 1)) );
1310 Fan = Vec_IntEntry(vFans2, 2);
1311 assert( Smt_EntryIsName(Fan) );
1312 pRange = Smt_EntryName(p, Fan);
1313 Range = atoi(pRange);
1314 }
1315 // create node
1316 iObj = Wlc_ObjAlloc( pNtk, WLC_OBJ_PI, 0, Range-1, 0 );
1317 NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pName, NULL );
1318 assert( iObj == NameId );
1319 // save values
1320 Vec_IntPush( &pNtk->vValues, NameId );
1321 Vec_IntPush( &pNtk->vValues, nBits );
1322 Vec_IntPush( &pNtk->vValues, Range );
1323 nBits += Range;
1324 ABC_FREE( pName_glb );
1325 }
1326 // create constants
1327 /*
1328 else if ( Abc_Lit2Var(Fan) == SMT_PRS_DEFINE_FUN ) // added: we parse DEFINE_FUN in LET
1329 {
1330 assert( Vec_IntSize(vFans) == 5 );
1331 assert( Smt_VecEntryIsType(vFans, 0, SMT_PRS_DEFINE_FUN) );
1332 // get name
1333 Fan = Vec_IntEntry(vFans, 1);
1334 assert( Smt_EntryIsName(Fan) );
1335 pName = Smt_EntryName(p, Fan);
1336
1337 // added: giving a global suffix
1338 char * pName_glb = (char *) malloc(strlen(pName) + 4 + 1);
1339 strcpy(pName_glb,pName);
1340 strcat(pName_glb,SMT_GLO_SUFFIX);
1341 // FIXME: delete memory of pName
1342 pName = pName_glb;
1343
1344 // skip ()
1345 Fan = Vec_IntEntry(vFans, 2);
1346 assert( !Smt_EntryIsName(Fan) );
1347 // check type (Bool or BitVec)
1348 Fan = Vec_IntEntry(vFans, 3);
1349 if ( Smt_EntryIsName(Fan) )
1350 {
1351 // (define-fun s_2 () Bool false)
1352 assert( !strcmp("Bool", Smt_VecEntryName(p, vFans, 3)) );
1353 Range = 1;
1354 pValue = Smt_VecEntryName(p, vFans, 4);
1355
1356 //printf("value: %s\n",pValue);
1357
1358 if ( !strcmp("false", pValue) )
1359 pValue = "#b0";
1360 else if ( !strcmp("true", pValue) )
1361 pValue = "#b1";
1362 else assert( 0 );
1363 Status = Smt_PrsBuildConstant( pNtk, pValue, Range, pName );
1364 }
1365 else
1366 {
1367 // (define-fun s702 () (_ BitVec 4) #xe)
1368 // (define-fun s1 () (_ BitVec 8) (bvneg #x7f))
1369 // get range
1370 Fan = Vec_IntEntry(vFans, 3);
1371
1372 assert( !Smt_EntryIsName(Fan) );
1373 vFans2 = Smt_VecEntryNode(p, vFans, 3);
1374 assert( Vec_IntSize(vFans2) == 3 );
1375 assert( !strcmp("_", Smt_VecEntryName(p, vFans2, 0)) );
1376 assert( !strcmp("BitVec", Smt_VecEntryName(p, vFans2, 1)) );
1377 // get range
1378 Fan = Vec_IntEntry(vFans2, 2);
1379
1380 assert( Smt_EntryIsName(Fan) );
1381 pRange = Smt_EntryName(p, Fan);
1382 Range = atoi(pRange);
1383
1384 // added: can parse functions too
1385 Vec_Int_t * vFans3 = Smt_VecEntryNode(p, vFans, 4);
1386 Fan = Vec_IntEntry(vFans3, 0);
1387
1388 // get constant
1389 //Fan = Vec_IntEntry(vFans, 4);
1390
1391 //printf("fan3: %s\n",Fan);
1392 //printf("fan0: %s\n",Smt_VecEntryName(p, vFans3, 0));
1393 //printf("fan1: %s\n",Smt_VecEntryName(p, vFans3, 1));
1394 //printf("fan2: %s\n",Smt_VecEntryName(p, vFans3, 2));
1395 //printf("fan3: %s\n",Smt_VecEntryName(p, vFans3, 3));
1396
1397 Status = Smt_PrsBuildNode( pNtk, p, Fan, Range, pName );
1398 }
1399 if ( !Status )
1400 {
1401 Wlc_NtkFree( pNtk ); pNtk = NULL;
1402 goto finish;
1403 }
1404 }
1405 */
1406 // added: new way to parse define-fun
1407 // create constants
1408 else if ( Abc_Lit2Var(Fan) == SMT_PRS_DEFINE_FUN )
1409 {
1410 char * pName_glb;
1411 // (define-fun def_16001 () Bool (or def_15999 def_16000))
1412 // (define-fun def_15990 () (_ BitVec 24) (concat def_15988 def_15989))
1413 assert( Smt_VecEntryIsType(vFans, 0, SMT_PRS_DEFINE_FUN) );
1414 assert( Vec_IntSize(vFans) == 5 ); // const or definition
1415
1416 // get name
1417 Fan = Vec_IntEntry(vFans, 1);
1418 assert( Smt_EntryIsName(Fan) );
1419 pName = Smt_EntryName(p, Fan);
1420 // added: giving a global suffix
1421 pName_glb = (char *) malloc(strlen(pName) + 4 + 1);
1422 strcpy(pName_glb,pName);
1423 strcat(pName_glb,SMT_GLO_SUFFIX);
1424 // FIXME: delete memory of pName
1425 pName = pName_glb;
1426
1427 //get range
1428 Fan = Vec_IntEntry(vFans, 3);
1429 if ( Smt_EntryIsName(Fan) )
1430 {
1431 // (define-fun s_2 () Bool false)
1432 assert( !strcmp("Bool", Smt_VecEntryName(p, vFans, 3)) );
1433 Range = 1;
1434 }
1435 else
1436 {
1437 // (define-fun s702 () (_ BitVec 4) #xe)
1438 // (define-fun s1 () (_ BitVec 8) (bvneg #x7f))
1439 assert( !Smt_EntryIsName(Fan) );
1440 vFans2 = Smt_VecEntryNode(p, vFans, 3);
1441 assert( Vec_IntSize(vFans2) == 3 );
1442 assert( !strcmp("_", Smt_VecEntryName(p, vFans2, 0)) );
1443 assert( !strcmp("BitVec", Smt_VecEntryName(p, vFans2, 1)) );
1444 // get range
1445 Fan = Vec_IntEntry(vFans2, 2);
1446 assert( Smt_EntryIsName(Fan) );
1447 pRange = Smt_EntryName(p, Fan);
1448 Range = atoi(pRange);
1449 }
1450
1451 iObj = Smt_PrsBuild2_rec( pNtk, p, Vec_IntEntry(vFans, 4), Range, pName );
1452 assert( iObj );
1453 ABC_FREE( pName_glb );
1454 }
1455
1456 // collect assertion outputs
1457 else if ( Abc_Lit2Var(Fan) == SMT_PRS_ASSERT )
1458 {
1459 //(assert ; no quantifiers
1460 // (let ((s2 (bvsge s0 s1)))
1461 // (not s2)))
1462 //(assert (not (= s0 #x00)))
1463 assert( Vec_IntSize(vFans) == 2 );
1464 assert( Smt_VecEntryIsType(vFans, 0, SMT_PRS_ASSERT) );
1465 pNtk->nAssert++; // added
1466 iObj = Smt_PrsBuild2_rec( pNtk, p, Vec_IntEntry(vFans, 1), -1, NULL );
1467 if ( iObj == 0 )
1468 {
1469 Wlc_NtkFree( pNtk ); pNtk = NULL;
1470 goto finish;
1471 }
1472 Vec_IntPush( vAsserts, iObj );
1473 }
1474 // issue warnings about unknown dirs
1475 else if ( Abc_Lit2Var(Fan) >= SMT_PRS_END )
1476 printf( "Ignoring directive \"%s\".\n", Smt_EntryName(p, Fan) );
1477 }
1478 // build AND of asserts
1479 if ( Vec_IntSize(vAsserts) == 1 )
1480 iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_BUF, 0, 1, vAsserts, "miter" );
1481 // added: 0 asserts
1482 else if ( Vec_IntSize(vAsserts) == 0 )
1483 iObj = Smt_PrsBuildConstant( pNtk, "#b1", 1, "miter" );
1484 else
1485 {
1486 iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_BIT_CONCAT, 0, Vec_IntSize(vAsserts), vAsserts, NULL );
1487 Vec_IntFill( vAsserts, 1, iObj );
1488 iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_REDUCT_AND, 0, 1, vAsserts, "miter" );
1489 }
1490 Wlc_ObjSetCo( pNtk, Wlc_NtkObj(pNtk, iObj), 0 );
1491 // create nameIDs
1492 vFans = Vec_IntStartNatural( Wlc_NtkObjNumMax(pNtk) );
1493 Vec_IntAppend( &pNtk->vNameIds, vFans );
1494 Vec_IntFree( vFans );
1495 //Wlc_NtkReport( pNtk, NULL );
1496finish:
1497 // cleanup
1498 Vec_IntFree(vAsserts);
1499 return pNtk;
1500}
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
Wlc_Ntk_t_::nAssert
int nAssert
Definition wlc.h:155
strlen
int strlen()
strcpy
char * strcpy()
strcat
char * strcat()
malloc
char * malloc()
SMT_GLO_SUFFIX
#define SMT_GLO_SUFFIX
Definition wlcReadSmt.c:52
Smt_PrsBuild2_rec
int Smt_PrsBuild2_rec(Wlc_Ntk_t *pNtk, Smt_Prs_t *p, int iNode, int iObjPrev, char *pName)
Definition wlcReadSmt.c:1025
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Smt_PrsBuild2_rec()

int Smt_PrsBuild2_rec ( Wlc_Ntk_t * pNtk,
Smt_Prs_t * p,
int iNode,
int iObjPrev,
char * pName )

Definition at line 1025 of file wlcReadSmt.c.

1026{
1027 char suffix[100];
1028 sprintf(suffix,"_as%d",pNtk->nAssert);
1029
1030 //char * prepStr = Abc_NamStr(p->pStrs, Abc_Lit2Var(iNode));
1031 //printf("prestr: %s\n",prepStr);
1032
1033 //printf("inode: %d %d\n",iNode,Smt_EntryIsName(iNode));
1034
1035 if ( Smt_EntryIsName(iNode) )
1036 {
1037 char * pStr = Abc_NamStr(p->pStrs, Abc_Lit2Var(iNode));
1038 // handle built-in constants
1039 if ( !strcmp(pStr, "false") )
1040 pStr = "#b0";
1041 else if ( !strcmp(pStr, "true") )
1042 pStr = "#b1";
1043 if ( pStr[0] == '#' )
1044 return Smt_PrsBuildConstant( pNtk, pStr, -1, pName ? pName : Smt_PrsGenName(p) );
1045 else
1046 {
1047 int fFound, iObj;
1048 // look either for global DECLARE-FUN variable or local LET
1049 char * pStr_glb = (char *)malloc(strlen(pStr) + 4 +1); //glb
1050 char * pStr_loc = (char *)malloc(strlen(pStr) + strlen(suffix) +1);
1051 strcpy(pStr_glb,pStr);
1052 strcat(pStr_glb,SMT_GLO_SUFFIX);
1053 strcpy(pStr_loc,pStr);
1054 strcat(pStr_loc,suffix);
1055
1056 fFound = Abc_NamStrFind( pNtk->pManName, pStr_glb );
1057
1058 if (fFound)
1059 pStr = pStr_glb;
1060 else
1061 {
1062 assert( Abc_NamStrFind( pNtk->pManName, pStr_loc ));
1063 pStr = pStr_loc;
1064 }
1065 // FIXME: delete memory of pStr
1066
1067 iObj = Abc_NamStrFindOrAdd( pNtk->pManName, pStr, &fFound );
1068 assert( fFound );
1069 // create buffer if the name of the fanin has different name
1070 if ( pName && strcmp(Wlc_ObjName(pNtk, iObj), pName) )
1071 {
1072 Vec_IntFill( &p->vTempFans, 1, iObj );
1073 iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_BUF, 0, Wlc_ObjRange(Wlc_NtkObj(pNtk, iObj)), &p->vTempFans, pName );
1074 }
1075 ABC_FREE( pStr_glb );
1076 ABC_FREE( pStr_loc );
1077 return iObj;
1078 }
1079 }
1080 else
1081 {
1082 Vec_Int_t * vRoots, * vRoots1, * vFans3;
1083 int iObj, iRoot0, iRoot1, iRoot2, Fan, Fan3, k;
1084 assert( !Smt_EntryIsName(iNode) );
1085 vRoots = Smt_EntryNode( p, iNode );
1086 iRoot0 = Vec_IntEntry( vRoots, 0 );
1087 if ( Smt_EntryIsName(iRoot0) )
1088 {
1089 char * pName2, * pStr0 = Abc_NamStr(p->pStrs, Abc_Lit2Var(iRoot0));
1090 if ( Abc_Lit2Var(iRoot0) == SMT_PRS_LET || Abc_Lit2Var(iRoot0) == SMT_PRS_DEFINE_FUN) //added define-fun is similar to let
1091 {
1092 // let ((s35550 (bvor s48 s35549)))
1093 assert( Vec_IntSize(vRoots) == 3 );
1094 assert( Smt_VecEntryIsType(vRoots, 0, SMT_PRS_LET) );
1095 // get parts
1096 iRoot1 = Vec_IntEntry(vRoots, 1);
1097 assert( !Smt_EntryIsName(iRoot1) );
1098 vRoots1 = Smt_EntryNode(p, iRoot1);
1099 // iterate through the parts
1100 Vec_IntForEachEntry( vRoots1, Fan, k )
1101 {
1102 char * temp;
1103 // s35550 (bvor s48 s35549)
1104 assert( !Smt_EntryIsName(Fan) );
1105 vFans3 = Smt_EntryNode(p, Fan);
1106 assert( Vec_IntSize(vFans3) == 2 );
1107 // get the name
1108 Fan3 = Vec_IntEntry(vFans3, 0);
1109 assert( Smt_EntryIsName(Fan3) );
1110 pName2 = Smt_EntryName(p, Fan3);
1111 // create a local name with suffix
1112 if ( Abc_Lit2Var(iRoot0) == SMT_PRS_LET )
1113 {
1114 temp = (char *)malloc(strlen(pName2) + strlen(suffix) + 1);
1115 strcpy(temp, pName2);
1116 strcat(temp,suffix);
1117 }
1118 else
1119 { temp = (char *)malloc(strlen(pName2) + 4 + 1);
1120 strcpy(temp, pName2);
1121 strcat(temp,SMT_GLO_SUFFIX);
1122 }
1123 // FIXME: need to delete memory of pName2
1124 pName2 = temp;
1125 // get function
1126 Fan3 = Vec_IntEntry(vFans3, 1);
1127 //assert( !Smt_EntryIsName(Fan3) );
1128 // solve the problem
1129 iObj = Smt_PrsBuild2_rec( pNtk, p, Fan3, -1, pName2 ); // NULL ); //pName2 );
1130 ABC_FREE( temp );
1131 if ( iObj == 0 )
1132 return 0;
1133 // create buffer
1134 //Vec_IntFill( &p->vTempFans, 1, iObj );
1135 //Smt_PrsCreateNode( pNtk, WLC_OBJ_BUF, 0, Wlc_ObjRange(Wlc_NtkObj(pNtk, iObj)), &p->vTempFans, pName2 );
1136 }
1137 // process the final part of let
1138 iRoot2 = Vec_IntEntry(vRoots, 2);
1139 return Smt_PrsBuild2_rec( pNtk, p, iRoot2, -1, pName );
1140 }
1141 else if ( pStr0[0] == '_' )
1142 {
1143 char * pStr1 = Smt_VecEntryName( p, vRoots, 1 );
1144 if ( pStr1[0] == 'b' && pStr1[1] == 'v' )
1145 {
1146 // (_ bv1 32)
1147 char * pStr2 = Smt_VecEntryName( p, vRoots, 2 );
1148 assert( Vec_IntSize(vRoots) == 3 );
1149 return Smt_PrsBuildConstant( pNtk, pStr1+2, atoi(pStr2), pName ? pName : Smt_PrsGenName(p) );
1150 }
1151 else
1152 {
1153 int Type1, fSigned = 0, Range = -1;
1154 assert( iObjPrev != -1 );
1155 Type1 = Smt_StrToType( pStr1, &fSigned );
1156 if ( Type1 == 0 )
1157 return 0;
1158 // find out this branch
1159 Vec_IntFill( &p->vTempFans, 1, iObjPrev );
1160 if ( Type1 == WLC_OBJ_BIT_SIGNEXT || Type1 == WLC_OBJ_BIT_ZEROPAD || Type1 == WLC_OBJ_ROTATE_R || Type1 == WLC_OBJ_ROTATE_L )
1161 {
1162 int iRoot2 = Vec_IntEntry(vRoots, 2);
1163 char * pStr2 = Abc_NamStr(p->pStrs, Abc_Lit2Var(iRoot2));
1164 int Num = atoi( pStr2 );
1165 //fSigned = (Type1 == WLC_OBJ_BIT_SIGNEXT);
1166 if ( Type1 == WLC_OBJ_ROTATE_R || Type1 == WLC_OBJ_ROTATE_L )
1167 {
1168 int iConst = Smt_PrsBuildConstant( pNtk, pStr2, -1, Smt_PrsGenName(p) );
1169 Vec_IntClear( &p->vTempFans );
1170 Vec_IntPushTwo( &p->vTempFans, iObjPrev, iConst );
1171 Range = Wlc_ObjRange( Wlc_NtkObj(pNtk, iObjPrev) );
1172 }
1173 else
1174 Range = Num + Wlc_ObjRange( Wlc_NtkObj(pNtk, iObjPrev) );
1175 }
1176 else if ( Type1 == WLC_OBJ_BIT_SELECT )
1177 {
1178 int iRoot2 = Vec_IntEntry( vRoots, 2 );
1179 int iRoot3 = Vec_IntEntry( vRoots, 3 );
1180 char * pStr2 = Abc_NamStr(p->pStrs, Abc_Lit2Var(iRoot2));
1181 char * pStr3 = Abc_NamStr(p->pStrs, Abc_Lit2Var(iRoot3));
1182 int Num1 = atoi( pStr2 );
1183 int Num2 = atoi( pStr3 );
1184 assert( Num1 >= Num2 );
1185 Range = Num1 - Num2 + 1;
1186 Vec_IntPushTwo( &p->vTempFans, Num1, Num2 );
1187 }
1188 else assert( 0 );
1189 iObj = Smt_PrsCreateNode( pNtk, Type1, fSigned, Range, &p->vTempFans, pName ? pName : Smt_PrsGenName(p) );
1190 return iObj;
1191 }
1192 }
1193 else
1194 {
1195 Vec_Int_t * vFanins;
1196 int i, Fan, fSigned = 0, Range, Type0;
1197 int iObj = Abc_NamStrFind( pNtk->pManName, pStr0 );
1198 if ( iObj )
1199 return iObj;
1200 Type0 = Smt_StrToType( pStr0, &fSigned );
1201 if ( Type0 == 0 )
1202 return 0;
1203 assert( Type0 != WLC_OBJ_BIT_SIGNEXT && Type0 != WLC_OBJ_BIT_ZEROPAD && Type0 != WLC_OBJ_BIT_SELECT && Type0 != WLC_OBJ_ROTATE_R && Type0 != WLC_OBJ_ROTATE_L );
1204
1205 // collect fanins
1206 vFanins = Vec_IntAlloc( 100 );
1207 Vec_IntForEachEntryStart( vRoots, Fan, i, 1 )
1208 {
1209 iObj = Smt_PrsBuild2_rec( pNtk, p, Fan, -1, NULL );
1210 if ( iObj == 0 )
1211 {
1212 Vec_IntFree( vFanins );
1213 return 0;
1214 }
1215 Vec_IntPush( vFanins, iObj );
1216 }
1217 // find range
1218 Range = 0;
1219 if ( Type0 >= WLC_OBJ_LOGIC_NOT && Type0 <= WLC_OBJ_REDUCT_XOR )
1220 Range = 1;
1221 else if ( Type0 == WLC_OBJ_BIT_CONCAT )
1222 {
1223 Vec_IntForEachEntry( vFanins, Fan, i )
1224 Range += Wlc_ObjRange( Wlc_NtkObj(pNtk, Fan) );
1225 }
1226 else if ( Type0 == WLC_OBJ_MUX )
1227 {
1228 int * pArray = Vec_IntArray(vFanins);
1229 assert( Vec_IntSize(vFanins) == 3 );
1230 ABC_SWAP( int, pArray[1], pArray[2] );
1231 iObj = Vec_IntEntry(vFanins, 1);
1232 Range = Wlc_ObjRange( Wlc_NtkObj(pNtk, iObj) );
1233 }
1234 else // to determine range, look at the first argument
1235 {
1236 iObj = Vec_IntEntry(vFanins, 0);
1237 Range = Wlc_ObjRange( Wlc_NtkObj(pNtk, iObj) );
1238 }
1239 // create node
1240 assert( Range > 0 );
1241 iObj = Smt_PrsCreateNode( pNtk, Type0, fSigned, Range, vFanins, pName ? pName : Smt_PrsGenName(p) );
1242 Vec_IntFree( vFanins );
1243 return iObj;
1244 }
1245 }
1246 else if ( Vec_IntSize(vRoots) == 2 ) // could be ((_ extract 48 16) (bvmul ?v_5 ?v_12))
1247 {
1248 int iObjPrev = Smt_PrsBuild2_rec( pNtk, p, Vec_IntEntry(vRoots, 1), -1, NULL );
1249 if ( iObjPrev == 0 )
1250 return 0;
1251 return Smt_PrsBuild2_rec( pNtk, p, Vec_IntEntry(vRoots, 0), iObjPrev, pName );
1252 }
1253 else assert( 0 ); // return Smt_PrsBuild2_rec( pNtk, p, iRoot0 );
1254 return 0;
1255 }
1256}
ABC_SWAP
#define ABC_SWAP(Type, a, b)
Definition abc_global.h:253
Abc_NamStrFind
int Abc_NamStrFind(Abc_Nam_t *p, char *pStr)
Definition utilNam.c:433
Abc_NamStr
char * Abc_NamStr(Abc_Nam_t *p, int NameId)
Definition utilNam.c:555
sprintf
char * sprintf()
Vec_IntForEachEntryStart
#define Vec_IntForEachEntryStart(vVec, Entry, i, Start)
Definition vecInt.h:56
Smt_PrsGenName
char * Smt_PrsGenName(Smt_Prs_t *p)
Definition wlcReadSmt.c:1019
Wlc_ObjName
char * Wlc_ObjName(Wlc_Ntk_t *p, int iObj)
Definition wlcNtk.c:225
WLC_OBJ_BIT_SIGNEXT
@ WLC_OBJ_BIT_SIGNEXT
Definition wlc.h:70
WLC_OBJ_BIT_ZEROPAD
@ WLC_OBJ_BIT_ZEROPAD
Definition wlc.h:69
WLC_OBJ_BIT_SELECT
@ WLC_OBJ_BIT_SELECT
Definition wlc.h:67
WLC_OBJ_MUX
@ WLC_OBJ_MUX
Definition wlc.h:53
WLC_OBJ_LOGIC_NOT
@ WLC_OBJ_LOGIC_NOT
Definition wlc.h:71
WLC_OBJ_REDUCT_XOR
@ WLC_OBJ_REDUCT_XOR
Definition wlc.h:84
WLC_OBJ_ROTATE_L
@ WLC_OBJ_ROTATE_L
Definition wlc.h:59
WLC_OBJ_ROTATE_R
@ WLC_OBJ_ROTATE_R
Definition wlc.h:58
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Smt_PrsBuildNode()

int Smt_PrsBuildNode ( Wlc_Ntk_t * pNtk,
Smt_Prs_t * p,
int iNode,
int RangeOut,
char * pName )

Definition at line 667 of file wlcReadSmt.c.

668{
669 if ( Smt_EntryIsName(iNode) ) // name or constant
670 {
671 char * pStr = Abc_NamStr(p->pStrs, Abc_Lit2Var(iNode));
672 if ( (pStr[0] >= '0' && pStr[0] <= '9') || pStr[0] == '#' )
673 {
674 // (_ BitVec 8) #x19
675 return Smt_PrsBuildConstant( pNtk, pStr, RangeOut, pName );
676 }
677 else
678 {
679 // s3087
680 int fFound, iObj = Abc_NamStrFindOrAdd( pNtk->pManName, pStr, &fFound );
681 assert( fFound );
682 return iObj;
683 }
684 }
685 else // node
686 {
687 Vec_Int_t * vFans = Smt_EntryNode( p, iNode );
688 char * pStr0 = Smt_VecEntryName( p, vFans, 0 );
689 char * pStr1 = Smt_VecEntryName( p, vFans, 1 );
690 if ( pStr0 && pStr1 && pStr0[0] == '_' && pStr1[0] == 'b' && pStr1[1] == 'v' )
691 {
692 // (_ bv1 32)
693 char * pStr2 = Smt_VecEntryName( p, vFans, 2 );
694 assert( Vec_IntSize(vFans) == 3 );
695 return Smt_PrsBuildConstant( pNtk, pStr1+2, atoi(pStr2), pName );
696 }
697 else if ( pStr0 && pStr0[0] == '=' )
698 {
699 assert( Vec_IntSize(vFans) == 3 );
700 iNode = Vec_IntEntry(vFans, 2);
701 assert( Smt_EntryIsName(iNode) );
702 pStr0 = Smt_EntryName(p, iNode);
703 // check the last one is "#b1"
704 if ( !strcmp("#b1", pStr0) )
705 {
706 iNode = Vec_IntEntry(vFans, 1);
707 return Smt_PrsBuildNode( pNtk, p, iNode, -1, pName );
708 }
709 else
710 {
711 Vec_Int_t * vFanins = Vec_IntAlloc( 2 );
712 // get the constant
713 int iObj, iOper, iConst = Smt_PrsBuildConstant( pNtk, pStr0, -1, NULL );
714 // check the middle one is an operator
715 iNode = Vec_IntEntry(vFans, 1);
716 iOper = Smt_PrsBuildNode( pNtk, p, iNode, -1, pName );
717 // build comparator
718 Vec_IntPushTwo( vFanins, iOper, iConst );
719 iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_COMP_EQU, 0, 1, vFanins, pName );
720 Vec_IntFree( vFanins );
721 return iObj;
722 }
723 }
724 else
725 {
726 int i, Fan, NameId, iFanin, fSigned, Range, Value1 = -1, Value2 = -1;
727 int Type = Smt_PrsReadType( p, Vec_IntEntry(vFans, 0), &fSigned, &Value1, &Value2 );
728 // collect fanins
729 Vec_Int_t * vFanins = Vec_IntAlloc( 100 );
730 Vec_IntForEachEntryStart( vFans, Fan, i, 1 )
731 {
732 iFanin = Smt_PrsBuildNode( pNtk, p, Fan, -1, NULL );
733 if ( iFanin == 0 )
734 {
735 Vec_IntFree( vFanins );
736 return 0;
737 }
738 Vec_IntPush( vFanins, iFanin );
739 }
740 // update specialized nodes
741 assert( Type != WLC_OBJ_BIT_SIGNEXT && Type != WLC_OBJ_BIT_ZEROPAD );
742 if ( Type == WLC_OBJ_BIT_SELECT )
743 {
744 assert( Value1 >= 0 && Value2 >= 0 && Value1 >= Value2 );
745 Vec_IntPushTwo( vFanins, Value1, Value2 );
746 }
747 else if ( Type == WLC_OBJ_ROTATE_R || Type == WLC_OBJ_ROTATE_L )
748 {
749 char Buffer[100];
750 assert( Value1 >= 0 );
751 sprintf( Buffer, "%d", Value1 );
752 NameId = Smt_PrsBuildConstant( pNtk, Buffer, -1, NULL );
753 Vec_IntPush( vFanins, NameId );
754 }
755 // find range
756 Range = 0;
757 if ( Type >= WLC_OBJ_LOGIC_NOT && Type <= WLC_OBJ_REDUCT_XOR )
758 Range = 1;
759 else if ( Type == WLC_OBJ_BIT_SELECT )
760 Range = Value1 - Value2 + 1;
761 else if ( Type == WLC_OBJ_BIT_CONCAT )
762 {
763 Vec_IntForEachEntry( vFanins, NameId, i )
764 Range += Wlc_ObjRange( Wlc_NtkObj(pNtk, NameId) );
765 }
766 else if ( Type == WLC_OBJ_MUX )
767 {
768 int * pArray = Vec_IntArray(vFanins);
769 assert( Vec_IntSize(vFanins) == 3 );
770 ABC_SWAP( int, pArray[1], pArray[2] );
771 NameId = Vec_IntEntry(vFanins, 1);
772 Range = Wlc_ObjRange( Wlc_NtkObj(pNtk, NameId) );
773 }
774 else // to determine range, look at the first argument
775 {
776 NameId = Vec_IntEntry(vFanins, 0);
777 Range = Wlc_ObjRange( Wlc_NtkObj(pNtk, NameId) );
778 }
779 // create node
780 assert( Range > 0 );
781 NameId = Smt_PrsCreateNode( pNtk, Type, fSigned, Range, vFanins, pName );
782 Vec_IntFree( vFanins );
783 return NameId;
784 }
785 }
786}
WLC_OBJ_COMP_EQU
@ WLC_OBJ_COMP_EQU
Definition wlc.h:76
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Smt_PrsGenName()

char * Smt_PrsGenName ( Smt_Prs_t * p)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1019 of file wlcReadSmt.c.

1020{
1021 static char Buffer[16];
1022 sprintf( Buffer, "_%0*X_", p->nDigits, ++p->NameCount );
1023 return Buffer;
1024}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Smt_PrsPrintParser()

void Smt_PrsPrintParser ( Smt_Prs_t * p)

Definition at line 1734 of file wlcReadSmt.c.

1735{
1736// Vec_WecPrint( &p->vDepth, 0 );
1737 Smt_PrsPrintParser_rec( p, 0, 0 );
1738}
Smt_PrsPrintParser_rec
void Smt_PrsPrintParser_rec(Smt_Prs_t *p, int iObj, int Depth)
Definition wlcReadSmt.c:1717
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Smt_PrsPrintParser_rec()

void Smt_PrsPrintParser_rec ( Smt_Prs_t * p,
int iObj,
int Depth )

Definition at line 1717 of file wlcReadSmt.c.

1718{
1719 Vec_Int_t * vFans; int i, Fan;
1720 printf( "%*s(\n", Depth, "" );
1721 vFans = Vec_WecEntry( &p->vObjs, iObj );
1722 Vec_IntForEachEntry( vFans, Fan, i )
1723 {
1724 if ( Abc_LitIsCompl(Fan) )
1725 {
1726 printf( "%*s", Depth+2, "" );
1727 printf( "%s\n", Abc_NamStr(p->pStrs, Abc_Lit2Var(Fan)) );
1728 }
1729 else
1730 Smt_PrsPrintParser_rec( p, Abc_Lit2Var(Fan), Depth+4 );
1731 }
1732 printf( "%*s)\n", Depth, "" );
1733}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Smt_PrsReadLines()

void Smt_PrsReadLines ( Smt_Prs_t * p)

Definition at line 1649 of file wlcReadSmt.c.

1650{
1651 int fFirstTime = 1;
1652 assert( Vec_IntSize(&p->vStack) == 0 );
1653 //assert( Vec_WecSize(&p->vDepth) == 0 );
1654 assert( Vec_WecSize(&p->vObjs) == 0 );
1655 // add top node at level 0
1656 //Vec_WecPushLevel( &p->vDepth );
1657 //Vec_WecPush( &p->vDepth, Vec_IntSize(&p->vStack), Vec_WecSize(&p->vObjs) );
1658 // add top node
1659 Vec_IntPush( &p->vStack, Vec_WecSize(&p->vObjs) );
1660 Vec_WecPushLevel( &p->vObjs );
1661 // add other nodes
1662 for ( p->pCur = p->pBuffer; p->pCur < p->pLimit; p->pCur++ )
1663 {
1664 Smt_PrsSkipSpaces( p );
1665 if ( fFirstTime && *p->pCur == '|' )
1666 {
1667 fFirstTime = 0;
1668 *p->pCur = ' ';
1669 while ( *p->pCur && *p->pCur != '|' )
1670 *p->pCur++ = ' ';
1671 if ( *p->pCur == '|' )
1672 *p->pCur = ' ';
1673 continue;
1674 }
1675 if ( *p->pCur == '(' )
1676 {
1677 // add new node at this depth
1678 //assert( Vec_WecSize(&p->vDepth) >= Vec_IntSize(&p->vStack) );
1679 //if ( Vec_WecSize(&p->vDepth) == Vec_IntSize(&p->vStack) )
1680 // Vec_WecPushLevel(&p->vDepth);
1681 //Vec_WecPush( &p->vDepth, Vec_IntSize(&p->vStack), Vec_WecSize(&p->vObjs) );
1682 // add fanin to node on the previous level
1683 Vec_IntPush( Vec_WecEntry(&p->vObjs, Vec_IntEntryLast(&p->vStack)), Abc_Var2Lit(Vec_WecSize(&p->vObjs), 0) );
1684 // add node to the stack
1685 Vec_IntPush( &p->vStack, Vec_WecSize(&p->vObjs) );
1686 Vec_WecPushLevel( &p->vObjs );
1687 }
1688 else if ( *p->pCur == ')' )
1689 {
1690 Vec_IntPop( &p->vStack );
1691 }
1692 else // token
1693 {
1694 char * pStart = p->pCur;
1695 Smt_PrsSkipNonSpaces( p );
1696 if ( p->pCur < p->pLimit )
1697 {
1698 // remove strange characters (this can lead to name clashes)
1699 int iToken;
1700 /* commented out for SMT comp
1701 char * pTemp;
1702 if ( *pStart == '?' )
1703 *pStart = '_';
1704 for ( pTemp = pStart; pTemp < p->pCur; pTemp++ )
1705 if ( *pTemp == '.' )
1706 *pTemp = '_';*/
1707 // create and save token for this string
1708 iToken = Abc_NamStrFindOrAddLim( p->pStrs, pStart, p->pCur--, NULL );
1709 Vec_IntPush( Vec_WecEntry(&p->vObjs, Vec_IntEntryLast(&p->vStack)), Abc_Var2Lit(iToken, 1) );
1710 }
1711 }
1712 }
1713 assert( Vec_IntSize(&p->vStack) == 1 );
1714 assert( Vec_WecSize(&p->vObjs) == Vec_WecCap(&p->vObjs) );
1715 p->nDigits = Abc_Base16Log( Vec_WecSize(&p->vObjs) );
1716}
Abc_NamStrFindOrAddLim
int Abc_NamStrFindOrAddLim(Abc_Nam_t *p, char *pStr, char *pLim, int *pfFound)
Definition utilNam.c:492
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Wlc_ReadSmt()

Wlc_Ntk_t * Wlc_ReadSmt ( char * pFileName,
int fOldParser,
int fPrintTree )

Definition at line 1766 of file wlcReadSmt.c.

1767{
1768 Wlc_Ntk_t * pNtk = NULL;
1769 char * pBuffer, * pLimit;
1770 pBuffer = Smt_PrsLoadFile( pFileName, &pLimit );
1771 if ( pBuffer == NULL )
1772 return NULL;
1773 pNtk = Wlc_ReadSmtBuffer( pFileName, pBuffer, pLimit, fOldParser, fPrintTree );
1774 ABC_FREE( pBuffer );
1775 return pNtk;
1776}
Wlc_ReadSmtBuffer
Wlc_Ntk_t * Wlc_ReadSmtBuffer(char *pFileName, char *pBuffer, char *pLimit, int fOldParser, int fPrintTree)
Definition wlcReadSmt.c:1751
Here is the call graph for this function:

◆ Wlc_ReadSmtBuffer()

Wlc_Ntk_t * Wlc_ReadSmtBuffer ( char * pFileName,
char * pBuffer,
char * pLimit,
int fOldParser,
int fPrintTree )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1751 of file wlcReadSmt.c.

1752{
1753 Wlc_Ntk_t * pNtk = NULL;
1754 int nCount = Smt_PrsRemoveComments( pBuffer, pLimit );
1755 Smt_Prs_t * p = Smt_PrsAlloc( pFileName, pBuffer, pLimit, nCount );
1756 if ( p == NULL )
1757 return NULL;
1758 Smt_PrsReadLines( p );
1759 if ( fPrintTree )
1760 Smt_PrsPrintParser( p );
1761 if ( Smt_PrsErrorPrint(p) )
1762 pNtk = fOldParser ? Smt_PrsBuild(p) : Smt_PrsBuild2(p);
1763 Smt_PrsFree( p );
1764 return pNtk;
1765}
Smt_PrsBuild
Wlc_Ntk_t * Smt_PrsBuild(Smt_Prs_t *p)
Definition wlcReadSmt.c:799
Smt_PrsReadLines
void Smt_PrsReadLines(Smt_Prs_t *p)
Definition wlcReadSmt.c:1649
Smt_PrsBuild2
Wlc_Ntk_t * Smt_PrsBuild2(Smt_Prs_t *p)
Definition wlcReadSmt.c:1257
Smt_PrsPrintParser
void Smt_PrsPrintParser(Smt_Prs_t *p)
Definition wlcReadSmt.c:1734
Smt_Prs_t
typedefABC_NAMESPACE_IMPL_START struct Smt_Prs_t_ Smt_Prs_t
DECLARATIONS ///.
Definition wlcReadSmt.c:31
Here is the call graph for this function:
Here is the caller graph for this function: