Merge pull request #2681 from diffblue/remove-aig

remove AIGs

Author: Daniel Kroening

src/cbmc/cbmc_parse_options.cpp

@@ -309,9 +309,6 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
       "max-node-refinement",
       cmdline.get_value("max-node-refinement"));
 
-  if(cmdline.isset("aig"))
-    options.set_option("aig", true);
-
   // SMT Options
 
   if(cmdline.isset("smt1"))

src/cbmc/cbmc_parse_options.h

@@ -52,7 +52,7 @@ class optionst;
   "(string-printable)" \
   "(string-max-length):" \
   "(string-max-input-length):" \
-  "(aig)(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
+  "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
   "(little-endian)(big-endian)" \
   OPT_SHOW_GOTO_FUNCTIONS \
   OPT_SHOW_PROPERTIES \

src/cbmc/cbmc_solvers.cpp

@@ -23,7 +23,6 @@ Author: Daniel Kroening, [email protected]
 #include <solvers/refinement/bv_refinement.h>
 #include <solvers/refinement/string_refinement.h>
 #include <solvers/smt2/smt2_dec.h>
-#include <solvers/prop/aig_prop.h>
 #include <solvers/sat/dimacs_cnf.h>
 
 #include "bv_cbmc.h"

src/cbmc/cbmc_solvers.h

@@ -23,7 +23,6 @@ Author: Daniel Kroening, [email protected]
 #include <solvers/prop/prop_conv.h>
 #include <solvers/sat/cnf.h>
 #include <solvers/sat/satcheck.h>
-#include <solvers/prop/aig_prop.h>
 #include <solvers/smt2/smt2_dec.h>
 #include <goto-symex/symex_target_equation.h>
 

src/solvers/Makefile

@@ -146,8 +146,6 @@ SRC = $(BOOLEFORCE_SRC) \
       floatbv/float_approximation.cpp \
       lowering/popcount.cpp \
       miniBDD/miniBDD.cpp \
-      prop/aig.cpp \
-      prop/aig_prop.cpp \
       prop/bdd_expr.cpp \
       prop/cover_goals.cpp \
       prop/literal.cpp \