Merge pull request #568 from diffblue/solvert-cleanup

cleanup of CBMC solver factory

Author: Daniel Kroening

src/cbmc/cbmc_solvers.cpp

@@ -102,100 +102,6 @@ smt2_dect::solvert cbmc_solverst::get_smt2_solver_type() const
   return s;
 }
 
-/*******************************************************************\
-
-   Class: cbmc_solver_with_propt
-
- Purpose: Solvers with additional objects
-
-\*******************************************************************/
-
-class cbmc_solver_with_propt:public cbmc_solverst::solvert
-{
-public:
-  cbmc_solver_with_propt(
-    prop_convt *_prop_conv,
-    propt *_prop):
-    cbmc_solverst::solvert(_prop_conv),
-    prop(_prop)
-  {
-    assert(_prop!=NULL);
-  }
-
-  ~cbmc_solver_with_propt()
-  {
-    delete prop;
-  }
-
-protected:
-  propt *prop;
-};
-
-/*******************************************************************\
-
-   Class: cbmc_solver_with_aigpropt
-
- Purpose: Solvers with additional objects
-
-\*******************************************************************/
-
-class cbmc_solver_with_aigpropt:public cbmc_solver_with_propt
-{
-public:
-  cbmc_solver_with_aigpropt(
-    prop_convt *_prop_conv,
-    propt *_prop,
-    aigt *_aig):
-    cbmc_solver_with_propt(_prop_conv, _prop),
-    aig(_aig)
-  {
-    assert(_aig!=NULL);
-  }
-
-  ~cbmc_solver_with_aigpropt()
-  {
-    // delete prop before the AIG
-    delete prop;
-    prop=NULL;
-    delete aig;
-  }
-
-protected:
-  aigt *aig;
-};
-
-/*******************************************************************\
-
-   Class: cbmc_solver_with_filet
-
- Purpose: Solvers with additional objects
-
-\*******************************************************************/
-
-class cbmc_solver_with_filet:public cbmc_solverst::solvert
-{
-public:
-  cbmc_solver_with_filet(
-    prop_convt *_prop_conv,
-    std::ofstream *_out):
-    cbmc_solverst::solvert(_prop_conv),
-    out(_out)
-  {
-    assert(_out!=NULL);
-  }
-
-  ~cbmc_solver_with_filet()
-  {
-    // delete the prop before the file
-    delete prop_conv_ptr;
-    prop_conv_ptr=NULL;
-    delete out;
-  }
-
-protected:
-  std::ofstream *out;
-};
-
 /*******************************************************************\
 
 Function: cbmc_solverst::get_default
@@ -210,45 +116,30 @@ Function: cbmc_solverst::get_default
 
 cbmc_solverst::solvert* cbmc_solverst::get_default()
 {
-  solvert *solver;
+  solvert *solver=new solvert;
 
   if(options.get_bool_option("beautify") ||
      !options.get_bool_option("sat-preprocessor")) // no simplifier
   {
     // simplifier won't work with beautification
-    propt *prop=new satcheck_no_simplifiert();
-    prop->set_message_handler(get_message_handler());
-
-    bv_cbmct *bv_cbmc=new bv_cbmct(ns, *prop);
-
-    if(options.get_option("arrays-uf")=="never")
-      bv_cbmc->unbounded_array=bv_cbmct::U_NONE;
-    else if(options.get_option("arrays-uf")=="always")
-      bv_cbmc->unbounded_array=bv_cbmct::U_ALL;
-
-    solver=new cbmc_solver_with_propt(bv_cbmc, prop);
+    solver->set_prop(new satcheck_no_simplifiert());
   }
   else // with simplifier
   {
-  #if 1
-    propt *prop=new satcheckt();
-    prop->set_message_handler(get_message_handler());
-    bv_cbmct *bv_cbmc=new bv_cbmct(ns, *prop);
-    solver=new cbmc_solver_with_propt(bv_cbmc, prop);
-  #else
-    aigt *aig=new aigt();
-    propt *prop=new aig_propt(*aig);
-    prop->set_message_handler(get_message_handler());
-    bv_cbmct *bv_cbmc=new bv_cbmct(ns, *prop);
-    solver=new cbmc_solver_with_aigpropt(bv_cbmc, prop, aig);
-  #endif
-
-    if(options.get_option("arrays-uf")=="never")
-      bv_cbmc->unbounded_array=bv_cbmct::U_NONE;
-    else if(options.get_option("arrays-uf")=="always")
-      bv_cbmc->unbounded_array=bv_cbmct::U_ALL;
+    solver->set_prop(new satcheckt());
   }
 
+  solver->prop().set_message_handler(get_message_handler());
+
+  bv_cbmct *bv_cbmc=new bv_cbmct(ns, solver->prop());
+
+  if(options.get_option("arrays-uf")=="never")
+    bv_cbmc->unbounded_array=bv_cbmct::U_NONE;
+  else if(options.get_option("arrays-uf")=="always")
+    bv_cbmc->unbounded_array=bv_cbmct::U_ALL;
+
+  solver->set_prop_conv(bv_cbmc);
+
   return solver;
 }
 
@@ -274,8 +165,7 @@ cbmc_solverst::solvert* cbmc_solverst::get_dimacs()
 
   std::string filename=options.get_option("outfile");
 
-  return
-    new cbmc_solver_with_propt(new cbmc_dimacst(ns, *prop, filename), prop);
+  return new solvert(new cbmc_dimacst(ns, *prop, filename), prop);
 }
 
 /*******************************************************************\
@@ -318,7 +208,7 @@ cbmc_solverst::solvert* cbmc_solverst::get_bv_refinement()
   bv_refinement->do_arithmetic_refinement =
     options.get_bool_option("refine-arithmetic");
 
-  return new cbmc_solver_with_propt(bv_refinement, prop);
+  return new solvert(bv_refinement, prop);
 }
 
 /*******************************************************************\
@@ -398,7 +288,7 @@ cbmc_solverst::solvert* cbmc_solverst::get_smt1(smt1_dect::solvert solver)
 
     smt1_conv->set_message_handler(get_message_handler());
 
-    return new cbmc_solver_with_filet(smt1_conv, out);
+    return new solvert(smt1_conv, out);
   }
 }
 
@@ -487,7 +377,7 @@ cbmc_solverst::solvert* cbmc_solverst::get_smt2(smt2_dect::solvert solver)
 
     smt2_conv->set_message_handler(get_message_handler());
 
-    return new cbmc_solver_with_filet(smt2_conv, out);
+    return new solvert(smt2_conv, out);
   }
 }
 

src/cbmc/cbmc_solvers.h

@@ -47,31 +47,62 @@ class cbmc_solverst:public messaget
   {
   }
 
-  // The solver class (that takes care of allocated objects)
+  // The solver class,
+  // which owns a variety of allocated objects.
   class solvert
   {
   public:
-    explicit solvert(prop_convt* _prop_conv)
+    solvert()
     {
-      assert(_prop_conv!=NULL);
-      prop_conv_ptr = _prop_conv;
     }
 
-    ~solvert()
+    explicit solvert(prop_convt *p):prop_conv_ptr(p)
+    {
+    }
+
+    solvert(prop_convt *p1, propt *p2):
+      prop_ptr(p2),
+      prop_conv_ptr(p1)
+    {
+    }
+
+    solvert(prop_convt *p1, std::ofstream *p2):
+      ofstream_ptr(p2),
+      prop_conv_ptr(p1)
     {
-      assert(prop_conv_ptr!=NULL);
-      delete prop_conv_ptr;
     }
 
-    // use this to get the prop_conv
     prop_convt &prop_conv() const
     {
-      assert(prop_conv_ptr!=NULL);
+      assert(prop_conv_ptr!=nullptr);
       return *prop_conv_ptr;
     }
 
-  protected:
-    prop_convt *prop_conv_ptr;
+    propt &prop() const
+    {
+      assert(prop_ptr!=nullptr);
+      return *prop_ptr;
+    }
+
+    void set_prop_conv(prop_convt *p)
+    {
+      prop_conv_ptr=std::unique_ptr<prop_convt>(p);
+    }
+
+    void set_prop(propt *p)
+    {
+      prop_ptr=std::unique_ptr<propt>(p);
+    }
+
+    void set_ofstream(std::ofstream *p)
+    {
+      ofstream_ptr=std::unique_ptr<std::ofstream>(p);
+    }
+
+    // the objects are deleted in the opposite order they appear below
+    std::unique_ptr<std::ofstream> ofstream_ptr;
+    std::unique_ptr<propt> prop_ptr;
+    std::unique_ptr<prop_convt> prop_conv_ptr;
   };
 
   // returns a solvert object