Merge pull request #2882 from peterschrammel/move-cbmc-dimacs

Move cbmc_dimacs to solvers/flattening/bv_dimacs

Author: peterschrammel

jbmc/src/jbmc/Makefile

@@ -41,7 +41,6 @@ OBJ += ../$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \
       ../$(CPROVER_DIR)/src/cbmc/all_properties$(OBJEXT) \
       ../$(CPROVER_DIR)/src/cbmc/bmc$(OBJEXT) \
       ../$(CPROVER_DIR)/src/cbmc/bmc_cover$(OBJEXT) \
-      ../$(CPROVER_DIR)/src/cbmc/cbmc_dimacs$(OBJEXT) \
       ../$(CPROVER_DIR)/src/cbmc/cbmc_solvers$(OBJEXT) \
       ../$(CPROVER_DIR)/src/cbmc/counterexample_beautification$(OBJEXT) \
       ../$(CPROVER_DIR)/src/cbmc/fault_localization$(OBJEXT) \

jbmc/unit/Makefile

@@ -60,7 +60,6 @@ java-testing-utils.dir:
 BMC_DEPS =$(CPROVER_DIR)/src/cbmc/all_properties$(OBJEXT) \
           $(CPROVER_DIR)/src/cbmc/bmc$(OBJEXT) \
           $(CPROVER_DIR)/src/cbmc/bmc_cover$(OBJEXT) \
-          $(CPROVER_DIR)/src/cbmc/cbmc_dimacs$(OBJEXT) \
           $(CPROVER_DIR)/src/cbmc/cbmc_languages$(OBJEXT) \
           $(CPROVER_DIR)/src/cbmc/cbmc_parse_options$(OBJEXT) \
           $(CPROVER_DIR)/src/cbmc/cbmc_solvers$(OBJEXT) \

src/cbmc/Makefile

@@ -1,7 +1,6 @@
 SRC = all_properties.cpp \
       bmc.cpp \
       bmc_cover.cpp \
-      cbmc_dimacs.cpp \
       cbmc_languages.cpp \
       cbmc_main.cpp \
       cbmc_parse_options.cpp \

src/cbmc/cbmc_solvers.cpp

@@ -19,13 +19,13 @@ Author: Daniel Kroening, [email protected]
 #include <util/unicode.h>
 #include <util/version.h>
 
-#include <solvers/sat/satcheck.h>
+#include <solvers/flattening/bv_dimacs.h>
 #include <solvers/refinement/bv_refinement.h>
 #include <solvers/refinement/string_refinement.h>
-#include <solvers/smt2/smt2_dec.h>
 #include <solvers/sat/dimacs_cnf.h>
+#include <solvers/sat/satcheck.h>
+#include <solvers/smt2/smt2_dec.h>
 
-#include "cbmc_dimacs.h"
 #include "counterexample_beautification.h"
 
 /// Uses the options to pick an SMT 2.0 solver
@@ -93,8 +93,8 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_dimacs()
 
   std::string filename=options.get_option("outfile");
 
-  auto cbmc_dimacs=util_make_unique<cbmc_dimacst>(ns, *prop, filename);
-  return util_make_unique<solvert>(std::move(cbmc_dimacs), std::move(prop));
+  auto bv_dimacs = util_make_unique<bv_dimacst>(ns, *prop, filename);
+  return util_make_unique<solvert>(std::move(bv_dimacs), std::move(prop));
 }
 
 std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_bv_refinement()

src/solvers/Makefile

@@ -132,6 +132,7 @@ SRC = $(BOOLEFORCE_SRC) \
       flattening/boolbv_vector.cpp \
       flattening/boolbv_width.cpp \
       flattening/boolbv_with.cpp \
+      flattening/bv_dimacs.cpp \
       flattening/bv_endianness_map.cpp \
       flattening/bv_minimize.cpp \
       flattening/bv_pointers.cpp \

src/cbmc/cbmc_dimacs.cpp renamed to src/solvers/flattening/bv_dimacs.cpp

@@ -9,16 +9,16 @@ Author: Daniel Kroening, [email protected]
 /// \file
 /// Writing DIMACS Files
 
-#include "cbmc_dimacs.h"
+#include "bv_dimacs.h"
 
 #include <fstream>
 #include <iostream>
 
 #include <solvers/sat/dimacs_cnf.h>
 
-bool cbmc_dimacst::write_dimacs(const std::string &filename)
+bool bv_dimacst::write_dimacs(const std::string &filename)
 {
-  if(filename.empty() || filename=="-")
+  if(filename.empty() || filename == "-")
     return write_dimacs(std::cout);
 
   std::ofstream out(filename);
@@ -32,25 +32,24 @@ bool cbmc_dimacst::write_dimacs(const std::string &filename)
   return write_dimacs(out);
 }
 
-bool cbmc_dimacst::write_dimacs(std::ostream &out)
+bool bv_dimacst::write_dimacs(std::ostream &out)
 {
-  dynamic_cast<dimacs_cnft&>(prop).write_dimacs_cnf(out);
+  dynamic_cast<dimacs_cnft &>(prop).write_dimacs_cnf(out);
 
   // we dump the mapping variable<->literals
   for(const auto &s : get_symbols())
   {
     if(s.second.is_constant())
-      out << "c " << s.first << " "
-          << (s.second.is_true()?"TRUE":"FALSE") << "\n";
+      out << "c " << s.first << " " << (s.second.is_true() ? "TRUE" : "FALSE")
+          << "\n";
     else
-      out << "c " << s.first << " "
-          << s.second.dimacs() << "\n";
+      out << "c " << s.first << " " << s.second.dimacs() << "\n";
   }
 
   // dump mapping for selected bit-vectors
   for(const auto &m : get_map().mapping)
   {
-    const boolbv_mapt::literal_mapt &literal_map=m.second.literal_map;
+    const boolbv_mapt::literal_mapt &literal_map = m.second.literal_map;
 
     if(literal_map.empty())
       continue;
@@ -59,9 +58,10 @@ bool cbmc_dimacst::write_dimacs(std::ostream &out)
 
     for(const auto &lit : literal_map)
       if(!lit.is_set)
-        out << " " << "?";
+        out << " "
+            << "?";
       else if(lit.l.is_constant())
-        out << " " << (lit.l.is_true()?"TRUE":"FALSE");
+        out << " " << (lit.l.is_true() ? "TRUE" : "FALSE");
       else
         out << " " << lit.l.dimacs();
 

src/cbmc/cbmc_dimacs.h renamed to src/solvers/flattening/bv_dimacs.h

@@ -9,23 +9,20 @@ Author: Daniel Kroening, [email protected]
 /// \file
 /// Writing DIMACS Files
 
-#ifndef CPROVER_CBMC_CBMC_DIMACS_H
-#define CPROVER_CBMC_CBMC_DIMACS_H
+#ifndef CPROVER_SOLVERS_FLATTENING_BV_DIMACS_H
+#define CPROVER_SOLVERS_FLATTENING_BV_DIMACS_H
 
-#include <solvers/flattening/bv_pointers.h>
+#include "bv_pointers.h"
 
-class cbmc_dimacst : public bv_pointerst
+class bv_dimacst : public bv_pointerst
 {
 public:
-  cbmc_dimacst(
-    const namespacet &_ns,
-    propt &_prop,
-    const std::string &_filename)
+  bv_dimacst(const namespacet &_ns, propt &_prop, const std::string &_filename)
     : bv_pointerst(_ns, _prop), filename(_filename)
   {
   }
 
-  virtual ~cbmc_dimacst()
+  virtual ~bv_dimacst()
   {
     write_dimacs(filename);
   }
@@ -36,4 +33,4 @@ class cbmc_dimacst : public bv_pointerst
   bool write_dimacs(std::ostream &);
 };
 
-#endif // CPROVER_CBMC_CBMC_DIMACS_H
+#endif // CPROVER_SOLVERS_FLATTENING_BV_DIMACS_H

unit/Makefile

@@ -62,7 +62,6 @@ testing-utils.dir:
 BMC_DEPS =../src/cbmc/all_properties$(OBJEXT) \
           ../src/cbmc/bmc$(OBJEXT) \
           ../src/cbmc/bmc_cover$(OBJEXT) \
-          ../src/cbmc/cbmc_dimacs$(OBJEXT) \
           ../src/cbmc/cbmc_languages$(OBJEXT) \
           ../src/cbmc/cbmc_parse_options$(OBJEXT) \
           ../src/cbmc/cbmc_solvers$(OBJEXT) \