bump aiger version and support arbitrary initialization functions in …

…btor2aiger Signed-off-by: Yuheng Su <[email protected]>
hwmcc · Aug 27, 2024 · 504ed14 · 504ed14
1 parent 44bcadb
commit 504ed14
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 11 deletions.
diff --git a/setup-deps.sh b/setup-deps.sh
@@ -6,10 +6,10 @@ rm -rf deps
 mkdir -p deps
 
 # Setup AIGER
-rm -rf aiger-1.9.4.tar.gz
-wget http://fmv.jku.at/aiger/aiger-1.9.4.tar.gz
-tar xf aiger-1.9.4.tar.gz
-mv aiger-1.9.4 deps/aiger
+rm -rf aiger-1.9.18.tar.gz
+wget https://github.com/arminbiere/aiger/archive/refs/tags/rel-1.9.18.tar.gz
+tar xf rel-1.9.18.tar.gz
+mv aiger-rel-1.9.18 deps/aiger
 
 
 # Setup Boolector

diff --git a/src/btor2aiger.cpp b/src/btor2aiger.cpp
@@ -414,16 +414,10 @@ add_state_to_aiger (Btor *btor,
 
   for (size_t i = 0; i < nbits; ++i)
   {
-    if (init_bits && init_bits[i] != 0 && init_bits[i] != 1)
-    {
-      /* Note: BTOR2 supports arbitrary initialization functions, but AIGER
-       * only supports 0/1/undefined. */
-      die ("Found non-constant initialization");
-    }
     sym = boolector_aig_get_symbol (amgr, state_bits[i]);
     if (next_bits)
     {
-      reset_val = init_bits ? init_bits[i] : state_bits[i];
+      reset_val = init_bits && init_bits[i] <= 1 ? init_bits[i] : state_bits[i];
       aiger_add_latch (aig, state_bits[i], next_bits[i], sym);
       aiger_add_reset (aig, state_bits[i], reset_val);
     }