Merge pull request #470 from MyskYko/btor

Btor

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/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();
@@ -59505,6 +59509,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/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