Merge remote-tracking branch 'upstream/master' into yosys-experimental

Makefile

@@ -33,7 +33,7 @@ MODULES := \
 	src/map/amap src/map/cov src/map/scl src/map/mpm \
 	src/misc/extra src/misc/mvc src/misc/st src/misc/util src/misc/nm \
 	src/misc/vec src/misc/hash src/misc/tim src/misc/bzlib src/misc/zlib \
-	src/misc/mem src/misc/bar src/misc/bbl src/misc/parse \
+	src/misc/mem src/misc/bar src/misc/bbl src/misc/parse src/misc/btor \
 	src/opt/cut src/opt/fxu src/opt/fxch src/opt/rwr src/opt/mfs src/opt/sim \
 	src/opt/ret src/opt/fret src/opt/res src/opt/lpk src/opt/nwk src/opt/rwt src/opt/rar \
 	src/opt/cgt src/opt/csw src/opt/dar src/opt/dau src/opt/dsc src/opt/sfm src/opt/sbd src/opt/eslim src/opt/ufar src/opt/untk src/opt/util \

abclib.dsp

@@ -5302,6 +5302,30 @@ SOURCE=.\src\misc\parse\parseInt.h
 SOURCE=.\src\misc\parse\parseStack.c
 # End Source File
 # End Group
+# Begin Group "btor"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\misc\btor\btor2mem.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\btor\btor2parser.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\btor\btor2parser.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\btor\btor2stack.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\btor\catbtor.c
+# End Source File
+# End Group
 # End Group
 # Begin Group "ai"
 

src/aig/gia/giaMulFind.c

@@ -875,7 +875,11 @@ void Gia_ManMulFindPrintOne( Vec_Wec_t * vTerms, int m, int fBooth, int fInputLi
     Vec_Int_t * vIn0 = Vec_WecEntry(vTerms, 3*m+0);
     Vec_Int_t * vIn1 = Vec_WecEntry(vTerms, 3*m+1);
     Vec_Int_t * vOut = Vec_WecEntry(vTerms, 3*m+2);
-    printf( "%sooth %ssigned %d x %d: ", fBooth ? "B" : "Non-b", Vec_IntEntryLast(vOut) ? "" : "un", Vec_IntSize(vIn0), Vec_IntSize(vIn1) );
+    printf( "%sooth %s%ssigned %d x %d: ", 
+        fBooth==1 ? "B" : "Non-b", 
+        fBooth>=1 ? "radix-4 " : "", 
+        Vec_IntEntryLast(vOut) ? "" : "un", 
+        Vec_IntSize(vIn0), Vec_IntSize(vIn1) );
     Gia_ManMulFindPrintSet( vIn0, fInputLits, 0 );
     printf( " * " );
     Gia_ManMulFindPrintSet( vIn1, fInputLits, 0 );

src/base/abci/abc.c

@@ -663,6 +663,8 @@ static int Abc_CommandAbc9Test               ( Abc_Frame_t * pAbc, int argc, cha
 
 static int Abc_CommandAbc9eSLIM              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
+static int Abc_CommandAbc9CatBtor            ( Abc_Frame_t * pAbc, int argc, char ** argv );
+
 extern int Abc_CommandAbcLivenessToSafety    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 extern int Abc_CommandAbcLivenessToSafetySim ( Abc_Frame_t * pAbc, int argc, char ** argv );
 extern int Abc_CommandAbcLivenessToSafetyWithLTL( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -1502,6 +1504,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&test",         Abc_CommandAbc9Test,                   0 );
 
     Cmd_CommandAdd( pAbc, "ABC9",         "&eslim",        Abc_CommandAbc9eSLIM,                  0 );
+    
+    Cmd_CommandAdd( pAbc, "ABC9",         "&catbtor",      Abc_CommandAbc9CatBtor,                0 );
     {
 //        extern Mf_ManTruthCount();
 //        Mf_ManTruthCount();
@@ -42509,6 +42513,71 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pTopModule, int * pAbc_ReadAigerOrVerilogFileStatus )
+{
+    FILE * pFile;
+    Gia_Man_t * pGia;
+    char * pTemp;
+    int fVerilog, fSystemVerilog;
+
+    *pAbc_ReadAigerOrVerilogFileStatus = 0;
+    if ( pFileName == NULL )
+        return NULL;
+
+    // fix the wrong symbol
+    for ( pTemp = pFileName; *pTemp; pTemp++ )
+        if ( *pTemp == '>' )
+            *pTemp = '\\';
+    if ( (pFile = fopen( pFileName, "r" )) == NULL )
+    {
+        Abc_Print( -1, "Cannot open input file \"%s\". ", pFileName );
+        if ( (pFileName = Extra_FileGetSimilarName( pFileName, ".aig", NULL, NULL, NULL, NULL )) )
+            Abc_Print( 1, "Did you mean \"%s\"?", pFileName );
+        Abc_Print( 1, "\n" );
+        *pAbc_ReadAigerOrVerilogFileStatus = 1;
+        return NULL;
+    }
+    fclose( pFile );
+
+    fSystemVerilog = Extra_FileIsType( pFileName, ".sv", NULL, NULL );
+    fVerilog = fSystemVerilog || Extra_FileIsType( pFileName, ".v", NULL, NULL );
+    if ( fVerilog )
+    {
+        char pCommand[2000];
+        int RetValue;
+        snprintf( pCommand, sizeof(pCommand),
+            "yosys -qp \"read_verilog %s%s; hierarchy %s%s; flatten; proc; opt; async2sync; opt; setundef -undriven -zero; techmap; memory -nomap; memory_map; dffunmap; opt_clean; opt_expr; aigmap; write_aiger -symbols _temp_.aig\"",
+            fSystemVerilog ? "-sv " : "", pFileName, pTopModule ? "-top "    : "-auto-top", pTopModule ? pTopModule : "" );
+#if defined(__wasm)
+        RetValue = 1;
+#else
+        RetValue = system( pCommand );
+#endif
+        if ( RetValue != 0 )
+        {
+            Abc_Print( -1, "Yosys command failed: \"%s\".\n", pCommand );
+            return NULL;
+        }
+        pFileName = "_temp_.aig";
+    }
+
+    pGia = Gia_AigerRead( pFileName, 0, 0, 0 );
+    if ( pGia == NULL )
+        Abc_Print( -1, "Reading AIGER from file \"%s\" has failed.\n", pFileName );
+    return pGia;
+}
+
 /**Function*************************************************************
 
   Synopsis    []
@@ -42524,13 +42593,13 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     extern void Cec_ManPrintCexSummary( Gia_Man_t * p, Abc_Cex_t * pCex, Cec_ParCec_t * pPars );
     Cec_ParCec_t ParsCec, * pPars = &ParsCec;
-    FILE * pFile;
     Gia_Man_t * pGias[2] = {NULL, NULL}, * pMiter;
-    char ** pArgvNew;
+    char ** pArgvNew, * pTopModule = NULL;
     int c, nArgcNew, fUseSim = 0, fUseNewX = 0, fUseNewY = 0, fMiter = 0, fDualOutput = 0, fDumpMiter = 0, fSavedSpec = 0;
+    int Abc_ReadAigerOrVerilogFileStatus = 0;
     Cec_ManCecSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "CTnmdbasxytvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CTMnmdbasxytvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -42556,6 +42625,15 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->TimeLimit < 0 )
                 goto usage;
             break;
+        case 'M':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-M\" should be followed by a file name.\n" );
+                goto usage;
+            }
+            pTopModule = argv[globalUtilOptind];
+            globalUtilOptind++;
+            break;
         case 'n':
             pPars->fNaive ^= 1;
             break;
@@ -42673,29 +42751,13 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( nArgcNew == 2 )
     {
-        char * pFileNames[2] = { pArgvNew[0], pArgvNew[1] }, * pTemp;
+        char * pFileNames[2] = { pArgvNew[0], pArgvNew[1] };
         int n;
         for ( n = 0; n < 2; n++ )
         {
-            // fix the wrong symbol
+            pGias[n] = Abc_ReadAigerOrVerilogFile( pFileNames[n], pTopModule, &Abc_ReadAigerOrVerilogFileStatus );
-            for ( pTemp = pFileNames[n]; *pTemp; pTemp++ )
-                if ( *pTemp == '>' )
-                    *pTemp = '\\';
-            if ( (pFile = fopen( pFileNames[n], "r" )) == NULL )
-            {
-                Abc_Print( -1, "Cannot open input file \"%s\". ", pFileNames[n] );
-                if ( (pFileNames[n] = Extra_FileGetSimilarName( pFileNames[n], ".aig", NULL, NULL, NULL, NULL )) )
-                    Abc_Print( 1, "Did you mean \"%s\"?", pFileNames[n] );
-                Abc_Print( 1, "\n" );
-                return 1;
-            }
-            fclose( pFile );
-            pGias[n] = Gia_AigerRead( pFileNames[n], 0, 0, 0 );
             if ( pGias[n] == NULL )
-            {
+                return Abc_ReadAigerOrVerilogFileStatus;
-                Abc_Print( -1, "Reading AIGER from file \"%s\" has failed.\n", pFileNames[n] );
-                return 0;
-            }
         }
     }
     else if ( fSavedSpec )
@@ -42710,7 +42772,7 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     else
     {
-        char * FileName, * pTemp;
+        char * FileName;
         if ( pAbc->pGia == NULL )
         {
             Abc_Print( -1, "Abc_CommandAbc9Cec(): There is no current AIG.\n" );
@@ -42729,25 +42791,9 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
             }
             FileName = pAbc->pGia->pSpec;
         }
-        // fix the wrong symbol
+        pGias[1] = Abc_ReadAigerOrVerilogFile( FileName, pTopModule, &Abc_ReadAigerOrVerilogFileStatus );
-        for ( pTemp = FileName; *pTemp; pTemp++ )
-            if ( *pTemp == '>' )
-                *pTemp = '\\';
-        if ( (pFile = fopen( FileName, "r" )) == NULL )
-        {
-            Abc_Print( -1, "Cannot open input file \"%s\". ", FileName );
-            if ( (FileName = Extra_FileGetSimilarName( FileName, ".aig", NULL, NULL, NULL, NULL )) )
-                Abc_Print( 1, "Did you mean \"%s\"?", FileName );
-            Abc_Print( 1, "\n" );
-            return 1;
-        }
-        fclose( pFile );
-        pGias[1] = Gia_AigerRead( FileName, 0, 0, 0 );
         if ( pGias[1] == NULL )
-        {
+            return Abc_ReadAigerOrVerilogFileStatus;
-            Abc_Print( -1, "Reading AIGER has failed.\n" );
-            return 0;
-        }
     }
     pPars->pNameSpec = pGias[0] ? (pGias[0]->pSpec ? pGias[0]->pSpec : pGias[0]->pName) : NULL;
     pPars->pNameImpl = pGias[1] ? (pGias[1]->pSpec ? pGias[1]->pSpec : pGias[1]->pName) : NULL;
@@ -42857,10 +42903,11 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &cec [-CT num] [-nmdbasxytvwh]\n" );
+    Abc_Print( -2, "usage: &cec [-CT num] [-M str] [-nmdbasxytvwh]\n" );
     Abc_Print( -2, "\t         new combinational equivalence checker\n" );
     Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
     Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", pPars->TimeLimit );
+    Abc_Print( -2, "\t-M str : top module name if Verilog file(s) are used [default = %d]\n", pPars->TimeLimit );
     Abc_Print( -2, "\t-n     : toggle using naive SAT-based checking [default = %s]\n", pPars->fNaive? "yes":"no");
     Abc_Print( -2, "\t-m     : toggle miter vs. two circuits [default = %s]\n", fMiter? "miter":"two circuits");
     Abc_Print( -2, "\t-d     : toggle using dual output miter [default = %s]\n", fDualOutput? "yes":"no");
@@ -59476,6 +59523,42 @@ int Abc_CommandAbc9eSLIM( Abc_Frame_t * pAbc, int argc, char ** argv ) {
     return 1;
 }
 
+int Abc_CommandAbc9CatBtor( Abc_Frame_t * pAbc, int argc, char ** argv ) {
+    extern void Abc_BtorCat( char * pFileName, int fVerbose );
+  
+    int c, fVerbose = 0;
+    char * pFileName;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "v" ) ) != EOF )
+    {
+        switch ( c ) {
+        case 'v' :
+            fVerbose ^= 1;
+            break;
+        default:
+            goto usage;
+        }
+    }
+    if ( argc == globalUtilOptind + 1 )
+        pFileName = argv[globalUtilOptind];
+    else
+    {
+        Abc_Print( -1, "File name is not given on the command line.\n" );
+        return 0;
+    }
+
+    Abc_BtorCat( pFileName, fVerbose );
+    
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &catbtor [-v] <file>\n" );
+    Abc_Print( -2, "\t          parse BTOR file and print to stdout.\n" );
+    Abc_Print( -2, "\t-v      : toggle printing verbose information\n");
+    Abc_Print( -2, "\t<file>  : input BTOR file\n");
+    return 1;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/base/main/mainReal.c

@@ -293,7 +293,7 @@ int Abc_RealMain( int argc, char * argv[] )
         pAbc->pGia = Gia_ManFromBridge( stdin, NULL );
     }
     else if ( fBatch!=INTERACTIVE && fBatch!=BATCH_QUIET && fBatch!=BATCH_QUIET_THEN_INTERACTIVE && Vec_StrSize(sCommandUsr)>0 )
-        Abc_Print( 1, "\n======== ABC command line \"%s\"\n", Vec_StrArray(sCommandUsr) );
+        Abc_Print( 1, "======== ABC command line \"%s\"\n", Vec_StrArray(sCommandUsr) );
 
     if ( fBatch!=INTERACTIVE )
     {

src/base/wln/wlnCom.c

@@ -102,6 +102,7 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
     char * pDefines  = NULL;
     char * pLibrary  = NULL;
     int fBlast       =    0;
+    int fDontBlast   =    0;
     int fInvert      =    0;
     int fTechMap     =    1;
     int fLibInDir    =    0;
@@ -110,7 +111,7 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fSetUndef    =    0;
     int c, fVerbose  =    0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "TDLbisumlcvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "TMDLbdisumlcvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -123,6 +124,15 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
             pTopModule = argv[globalUtilOptind];
             globalUtilOptind++;
             break;
+        case 'M':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-M\" should be followed by a file name.\n" );
+                goto usage;
+            }
+            pTopModule = argv[globalUtilOptind];
+            globalUtilOptind++;
+            break;
         case 'D':
             if ( globalUtilOptind >= argc )
             {
@@ -144,6 +154,9 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'b':
             fBlast ^= 1;
             break;
+        case 'd':
+            fDontBlast ^= 1;
+            break;
         case 'i':
             fInvert ^= 1;
             break;
@@ -203,7 +216,7 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
         }
         Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
     }
-    else if ( fBlast )
+    else if ( !fDontBlast )
     {
         Gia_Man_t * pNew = NULL;
         if ( !strcmp( Extra_FileNameExtension(pFileName), "v" )  )
@@ -237,12 +250,14 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     return 0;
 usage:
-    Abc_Print( -2, "usage: %%yosys [-T <module>] [-D <defines>] [-L <liberty_file>] [-bisumlcvh] <file_name>\n" );
+    Abc_Print( -2, "usage: %%yosys [-TM <module>] [-D <defines>] [-L <liberty_file>] [-bdisumlcvh] <file_name>\n" );
     Abc_Print( -2, "\t         reads Verilog or SystemVerilog using Yosys\n" );
     Abc_Print( -2, "\t-T     : specify the top module name (default uses \"-auto-top\")\n" );
+    Abc_Print( -2, "\t-M     : specify the top module name (default uses \"-auto-top\") (equivalent to \"-T\")\n" );
     Abc_Print( -2, "\t-D     : specify defines to be used by Yosys (default \"not used\")\n" );
     Abc_Print( -2, "\t-L     : specify the Liberty library to read a mapped design (default \"not used\")\n" );
-    Abc_Print( -2, "\t-b     : toggle bit-blasting the design into an AIG using Yosys [default = %s]\n", fBlast? "yes": "no" );
+    Abc_Print( -2, "\t-b     : toggle bit-blasting the design into an AIG using Yosys (this switch has no effect)\n" );
+    Abc_Print( -2, "\t-d     : toggle bit-blasting the design into an AIG using Yosys [default = %s]\n", !fDontBlast? "yes": "no" );
     Abc_Print( -2, "\t-i     : toggle inverting the outputs (useful for miters) [default = %s]\n", fInvert? "yes": "no" );
     Abc_Print( -2, "\t-s     : toggle no structural hashing during bit-blasting [default = %s]\n", fSkipStrash? "no strash": "strash" );
     Abc_Print( -2, "\t-m     : toggle using \"techmap\" to blast operators [default = %s]\n", fTechMap? "yes": "no" );

src/misc/btor/LICENSE.txt

@@ -0,0 +1,25 @@
+The Btor2Tools package provides a generic parser and tools for the BTOR2 format.
+
+Copyright (c) 2012-2018 Armin Biere.
+Copyright (c) 2013-2018 Mathias Preiner.
+Copyright (c) 2015-2018 Aina Niemetz.
+
+MIT License
+
+Permission is hereby granted, free of charge, to any person obtaining a
+copy of this software and associated documentation files (the "Software"),
+to deal in the Software without restriction, including without limitation
+the rights to use, copy, modify, merge, publish, distribute, sublicense,
+and/or sell copies of the Software, and to permit persons to whom the
+Software is furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included
+in all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL
+THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR
+OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
+ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
+OTHER DEALINGS IN THE SOFTWARE.

src/misc/btor/VERSION

@@ -0,0 +1 @@
+1.0.2

src/misc/btor/btor2mem.h

@@ -0,0 +1,88 @@
+/**
+ *  Btor2Tools: A tool package for the BTOR format.
+ *
+ *  Copyright (C) 2007-2009 Robert Daniel Brummayer.
+ *  Copyright (C) 2007-2012 Armin Biere.
+ *  Copyright (C) 2012-2015 Mathias Preiner.
+ *  Copyright (c) 2018 Aina Niemetz.
+ *
+ *  All rights reserved.
+ *
+ *  This file is part of the Btor2Tools package.
+ *  See LICENSE.txt for more information on using this software.
+ */
+
+#ifndef BTOR2MEM_H_INCLUDED
+#define BTOR2MEM_H_INCLUDED
+
+#include "misc/util/abc_global.h"
+
+ABC_NAMESPACE_HEADER_START
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+
+/*------------------------------------------------------------------------*/
+
+#define BTOR2_CLRN(ptr, nelems) (memset ((ptr), 0, (nelems) * sizeof *(ptr)))
+
+#define BTOR2_CLR(ptr) BTOR2_CLRN ((ptr), 1)
+
+#define BTOR2_DELETE(ptr) (free (ptr))
+
+static inline void *
+btorsim_malloc (size_t size)
+{
+  void *res;
+  if (!size) return 0;
+  res = malloc (size);
+  if (!res)
+  {
+    fprintf (stderr, "[btorsim] memory allocation failed\n");
+    abort ();
+  }
+  return res;
+}
+
+static inline void *
+btorsim_calloc (size_t nobj, size_t size)
+{
+  void *res;
+  res = calloc (nobj, size);
+  if (!res)
+  {
+    fprintf (stderr, "[btorsim] memory allocation failed\n");
+    abort ();
+  }
+  return res;
+}
+
+static inline void *
+btorsim_realloc (void *p, size_t new_size)
+{
+  void *res;
+  res = realloc (p, new_size);
+  if (!res)
+  {
+    fprintf (stderr, "[btorsim] memory allocation failed\n");
+    abort ();
+  }
+  return res;
+}
+
+static inline char *
+btorsim_strdup (const char *str)
+{
+  char *res = 0;
+  if (str)
+  {
+    res = (char *) btorsim_malloc ((strlen (str) + 1) * sizeof (char));
+    strcpy (res, str);
+  }
+  return res;
+}
+
+ABC_NAMESPACE_HEADER_END
+
+#endif

src/misc/btor/btor2parser.h

@@ -0,0 +1,211 @@
+/**
+ *  Btor2Tools: A tool package for the BTOR2 format.
+ *
+ *  Copyright (c) 2012-2018 Armin Biere.
+ *  Copyright (c) 2017 Mathias Preiner
+ *  Copyright (c) 2017 Aina Niemetz
+ *
+ *  All rights reserved.
+ *
+ *  This file is part of the Btor2Tools package.
+ *  See LICENSE.txt for more information on using this software.
+ */
+
+#ifndef btor2parser_h_INCLUDED
+#define btor2parser_h_INCLUDED
+
+/*------------------------------------------------------------------------*/
+/* The BTOR2 format is described in                                       */
+/* "BTOR2, BtorMC and Boolector 3.0" by A. Niemetz, M. Preiner, C. Wolf   */
+/* and A. Biere at CAV 2018.                                              */
+/*------------------------------------------------------------------------*/
+
+#include <stdint.h>
+#include <stdio.h>
+
+#include "misc/util/abc_global.h"
+
+ABC_NAMESPACE_HEADER_START
+
+/*------------------------------------------------------------------------*/
+
+#define BTOR2_FORMAT_MAXID (((int64_t) 1) << 40)
+#define BTOR2_FORMAT_MAXBITWIDTH ((1l << 30) + ((1l << 30) - 1))
+
+/*------------------------------------------------------------------------*/
+
+typedef struct Btor2Parser Btor2Parser;
+typedef struct Btor2Line Btor2Line;
+typedef struct Btor2Sort Btor2Sort;
+typedef struct Btor2LineIterator Btor2LineIterator;
+
+/*------------------------------------------------------------------------*/
+
+/**
+ * BTOR2 tags can be used for fast(er) traversal and operations on BTOR2
+ * format lines, e.g., in a switch statement in client code.
+ * Alternatively, client code can use the name of the BTOR2 tag, which is a C
+ * string (redundantly) contained in the format line. Note that this requires
+ * string comparisons and is therefore slower even if client code uses an
+ * additional hash table.
+ */
+enum Btor2Tag
+{
+  BTOR2_TAG_add,
+  BTOR2_TAG_and,
+  BTOR2_TAG_bad,
+  BTOR2_TAG_concat,
+  BTOR2_TAG_const,
+  BTOR2_TAG_constraint,
+  BTOR2_TAG_constd,
+  BTOR2_TAG_consth,
+  BTOR2_TAG_dec,
+  BTOR2_TAG_eq,
+  BTOR2_TAG_fair,
+  BTOR2_TAG_iff,
+  BTOR2_TAG_implies,
+  BTOR2_TAG_inc,
+  BTOR2_TAG_init,
+  BTOR2_TAG_input,
+  BTOR2_TAG_ite,
+  BTOR2_TAG_justice,
+  BTOR2_TAG_mul,
+  BTOR2_TAG_nand,
+  BTOR2_TAG_neq,
+  BTOR2_TAG_neg,
+  BTOR2_TAG_next,
+  BTOR2_TAG_nor,
+  BTOR2_TAG_not,
+  BTOR2_TAG_one,
+  BTOR2_TAG_ones,
+  BTOR2_TAG_or,
+  BTOR2_TAG_output,
+  BTOR2_TAG_read,
+  BTOR2_TAG_redand,
+  BTOR2_TAG_redor,
+  BTOR2_TAG_redxor,
+  BTOR2_TAG_rol,
+  BTOR2_TAG_ror,
+  BTOR2_TAG_saddo,
+  BTOR2_TAG_sdiv,
+  BTOR2_TAG_sdivo,
+  BTOR2_TAG_sext,
+  BTOR2_TAG_sgt,
+  BTOR2_TAG_sgte,
+  BTOR2_TAG_slice,
+  BTOR2_TAG_sll,
+  BTOR2_TAG_slt,
+  BTOR2_TAG_slte,
+  BTOR2_TAG_sort,
+  BTOR2_TAG_smod,
+  BTOR2_TAG_smulo,
+  BTOR2_TAG_sra,
+  BTOR2_TAG_srem,
+  BTOR2_TAG_srl,
+  BTOR2_TAG_ssubo,
+  BTOR2_TAG_state,
+  BTOR2_TAG_sub,
+  BTOR2_TAG_uaddo,
+  BTOR2_TAG_udiv,
+  BTOR2_TAG_uext,
+  BTOR2_TAG_ugt,
+  BTOR2_TAG_ugte,
+  BTOR2_TAG_ult,
+  BTOR2_TAG_ulte,
+  BTOR2_TAG_umulo,
+  BTOR2_TAG_urem,
+  BTOR2_TAG_usubo,
+  BTOR2_TAG_write,
+  BTOR2_TAG_xnor,
+  BTOR2_TAG_xor,
+  BTOR2_TAG_zero,
+};
+typedef enum Btor2Tag Btor2Tag;
+
+enum Btor2SortTag
+{
+  BTOR2_TAG_SORT_array,
+  BTOR2_TAG_SORT_bitvec,
+};
+typedef enum Btor2SortTag Btor2SortTag;
+
+/*------------------------------------------------------------------------*/
+
+struct Btor2Sort
+{
+  int64_t id;
+  Btor2SortTag tag;
+  const char *name;
+  union
+  {
+    struct
+    {
+      int64_t index;
+      int64_t element;
+    } array;
+    struct
+    {
+      uint32_t width;
+    } bitvec;
+  };
+};
+
+struct Btor2Line
+{
+  int64_t id;       /* positive id (non zero)                 */
+  int64_t lineno;   /* line number in original file           */
+  const char *name; /* name in ASCII: "and", "add", ...       */
+  Btor2Tag tag;     /* same as name but encoded as integer    */
+  Btor2Sort sort;
+  int64_t init, next; /* non zero if initialized or has next    */
+  char *constant;     /* non zero for const, constd, consth     */
+  char *symbol;       /* optional for: var array state input    */
+  uint32_t nargs;     /* number of arguments                    */
+  int64_t *args;      /* non zero ids up to nargs               */
+};
+
+struct Btor2LineIterator
+{
+  Btor2Parser *reader;
+  int64_t next;
+};
+
+/*------------------------------------------------------------------------*/
+/* Constructor, setting options and destructor:
+ */
+Btor2Parser *btor2parser_new ();
+void btor2parser_delete (Btor2Parser *);
+
+/*------------------------------------------------------------------------*/
+/* The 'btor2parser_read_lines' function returns zero on failure.  In this
+ * case you can call 'btor2parser_error' to obtain a description of
+ * the actual read or parse error, which includes the line number where
+ * the error occurred.
+ */
+int32_t btor2parser_read_lines (Btor2Parser *, FILE *);
+const char *btor2parser_error (Btor2Parser *);
+
+/*------------------------------------------------------------------------*/
+/* Iterate over all read format lines:
+ *
+ *   Btor2LineIterator it = btor2parser_iter_init (bfr);
+ *   Btor2Line * l;
+ *   while ((l = btor2parser_iter_next (&it)))
+ *     do_something_with_btor_format_line (l);
+ */
+Btor2LineIterator btor2parser_iter_init (Btor2Parser *bfr);
+Btor2Line *btor2parser_iter_next (Btor2LineIterator *);
+
+/*------------------------------------------------------------------------*/
+/* The reader maintains a mapping of ids to format lines.  This mapping
+ * can be retrieved with the following function.  Note, however, that
+ * ids might be negative and denote the negation of the actual node.
+ */
+int64_t btor2parser_max_id (Btor2Parser *);
+Btor2Line *btor2parser_get_line_by_id (Btor2Parser *, int64_t id);
+
+/*------------------------------------------------------------------------*/
+
+ABC_NAMESPACE_HEADER_END
+
+#endif

src/misc/btor/btor2stack.h

@@ -0,0 +1,96 @@
+/**
+ *  Btor2Tools: A tool package for the BTOR format.
+ *
+ *  Copyright (C) 2007-2009 Robert Daniel Brummayer.
+ *  Copyright (C) 2007-2013 Armin Biere.
+ *  Copyright (C) 2013-2018 Aina Niemetz.
+ *  Copyright (C) 2015-2016 Mathias Preiner.
+ *
+ *  All rights reserved.
+ *
+ *  This file is part of the Btor2Tools package.
+ *  See LICENSE.txt for more information on using this software.
+ */
+
+#ifndef BTOR2STACK_H_INCLUDED
+#define BTOR2STACK_H_INCLUDED
+
+#include "btor2mem.h"
+
+ABC_NAMESPACE_HEADER_START
+
+#define BTOR2_DECLARE_STACK(name, type)   \
+  typedef struct name##Stack name##Stack; \
+  struct name##Stack                      \
+  {                                       \
+    type *start;                          \
+    type *top;                            \
+    type *end;                            \
+  }
+
+BTOR2_DECLARE_STACK (BtorChar, char);
+BTOR2_DECLARE_STACK (BtorCharPtr, char *);
+BTOR2_DECLARE_STACK (BtorVoidPtr, void *);
+
+#define BTOR2_INIT_STACK(stack) \
+  do                            \
+  {                             \
+    (stack).start = 0;          \
+    (stack).top   = 0;          \
+    (stack).end   = 0;          \
+  } while (0)
+
+#define BTOR2_COUNT_STACK(stack) ((stack).top - (stack).start)
+#define BTOR2_SIZE_STACK(stack) ((stack).end - (stack).start)
+#define BTOR2_EMPTY_STACK(stack) ((stack).top == (stack).start)
+#define BTOR2_FULL_STACK(stack) ((stack).top == (stack).end)
+#define BTOR2_RESET_STACK(stack) ((stack).top = (stack).start)
+
+#define BTOR2_RELEASE_STACK(stack) \
+  do                               \
+  {                                \
+    BTOR2_DELETE ((stack).start);  \
+    BTOR2_INIT_STACK ((stack));    \
+  } while (0)
+
+#define BTOR2_ENLARGE(T, p, o, n)         \
+  do                                      \
+  {                                       \
+    size_t internaln = (o) ? 2 * (o) : 1; \
+    (p) = (T *) btorsim_realloc ((p), ((internaln) * sizeof (T))); \
+    (n) = internaln;                      \
+  } while (0)
+
+#define BTOR2_ENLARGE_STACK(T, stack)                      \
+  do                                                       \
+  {                                                        \
+    size_t old_size  = BTOR2_SIZE_STACK (stack), new_size; \
+    size_t old_count = BTOR2_COUNT_STACK (stack);          \
+    BTOR2_ENLARGE (T, (stack).start, old_size, new_size);  \
+    (stack).top = (stack).start + old_count;               \
+    (stack).end = (stack).start + new_size;                \
+  } while (0)
+
+#define BTOR2_PUSH_STACK(T, stack, elem)                           \
+  do                                                               \
+  {                                                                \
+    if (BTOR2_FULL_STACK ((stack))) BTOR2_ENLARGE_STACK (T, (stack)); \
+    *((stack).top++) = (elem);                                     \
+  } while (0)
+
+#define BTOR2_POP_STACK(stack) \
+  (assert (!BTOR2_EMPTY_STACK (stack)), (*--(stack).top))
+
+#define BTOR2_PEEK_STACK(stack, idx) \
+  (assert ((idx) < BTOR2_COUNT_STACK (stack)), (stack).start[idx])
+
+#define BTOR2_POKE_STACK(stack, idx, elem)      \
+  do                                            \
+  {                                             \
+    assert ((idx) < BTOR2_COUNT_STACK (stack)); \
+    (stack).start[idx] = (elem);                \
+  } while (0)
+
+ABC_NAMESPACE_HEADER_END
+
+#endif

src/misc/btor/catbtor.c

@@ -0,0 +1,111 @@
+/**
+ *  Btor2Tools: A tool package for the BTOR format.
+ *
+ *  Copyright (c) 2012-2015 Armin Biere.
+ *  Copyright (c) 2017 Mathias Preiner.
+ *  Copyright (c) 2017-2018 Aina Niemetz.
+ *
+ *  All rights reserved.
+ *
+ *  This file is part of the Btor2Tools package.
+ *  See LICENSE.txt for more information on using this software.
+ */
+
+#include "btor2parser.h"
+
+#include <assert.h>
+#include <inttypes.h>
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+
+ABC_NAMESPACE_IMPL_START
+
+/* Parse BTOR2 file and print to stdout. */
+
+int32_t
+Abc_BtorCat (char* input_name, int verbosity)
+{
+  FILE* input_file;
+
+  Btor2Parser* reader;
+  Btor2LineIterator it;
+  Btor2Line* l;
+  uint32_t j;
+  const char* err;
+  
+  input_file = fopen (input_name, "r");
+  if (!input_file)
+  {
+    fprintf (stderr, "*** catbtor: can not open '%s' for reading\n", input_name);
+    return 1;
+  }
+
+  if (verbosity)
+  {
+    fprintf (stderr,
+             "; [catbor] simple CAT for BTOR files\n"
+             "; [catbor] reading '%s'\n",
+             input_name);
+    fflush (stderr);
+  }
+  reader = btor2parser_new ();
+  if (!btor2parser_read_lines (reader, input_file))
+  {
+    err = btor2parser_error (reader);
+    assert (err);
+    fprintf (stderr, "*** catbtor: parse error in '%s' %s\n", input_name, err);
+    btor2parser_delete (reader);
+    fclose (input_file);
+    return 1;
+  }
+  fclose (input_file);
+  if (verbosity)
+  {
+    fprintf (stderr, "; [catbor] finished parsing '%s'\n", input_name);
+    fflush (stderr);
+  }
+  if (verbosity)
+  {
+    fprintf (stderr, "; [catbor] starting to dump BTOR model to '<stdout>'\n");
+    fflush (stderr);
+  }
+  it = btor2parser_iter_init (reader);
+  while ((l = btor2parser_iter_next (&it)))
+  {
+    printf ("%" PRId64 " %s", l->id, l->name);
+    if (l->tag == BTOR2_TAG_sort)
+    {
+      printf (" %s", l->sort.name);
+      switch (l->sort.tag)
+      {
+        case BTOR2_TAG_SORT_bitvec: printf (" %u", l->sort.bitvec.width); break;
+        case BTOR2_TAG_SORT_array:
+          printf (" %" PRId64 " %" PRId64, l->sort.array.index, l->sort.array.element);
+          break;
+        default:
+          fprintf (stderr, "*** catbtor: invalid sort encountered\n");
+          btor2parser_delete (reader);
+          return 1;
+      }
+    }
+    else if (l->sort.id)
+      printf (" %" PRId64, l->sort.id);
+    for (j = 0; j < l->nargs; j++) printf (" %" PRId64, l->args[j]);
+    if (l->tag == BTOR2_TAG_slice) printf (" %" PRId64 " %" PRId64, l->args[1], l->args[2]);
+    if (l->tag == BTOR2_TAG_sext || l->tag == BTOR2_TAG_uext)
+      printf (" %" PRId64, l->args[1]);
+    if (l->constant) printf (" %s", l->constant);
+    if (l->symbol) printf (" %s", l->symbol);
+    fputc ('\n', stdout);
+  }
+  btor2parser_delete (reader);
+  if (verbosity)
+  {
+    fprintf (stderr, "; [catbor] finished dumping BTOR model to '<stdout>'\n");
+    fflush (stderr);
+  }
+  return 0;
+}
+
+ABC_NAMESPACE_IMPL_END

src/misc/btor/module.make

@@ -0,0 +1,2 @@
+SRC +=    src/misc/btor/btor2parser.c \
+	src/misc/btor/catbtor.c

src/sat/cadical/VERSION

@@ -1 +1 @@
-2.2.0-rc1
+2.2.0