diff --git a/src/cbmc/cbmc_solvers.cpp b/src/cbmc/cbmc_solvers.cpp index 9c13f9ce964..ccd660dc586 100644 --- a/src/cbmc/cbmc_solvers.cpp +++ b/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); } } diff --git a/src/cbmc/cbmc_solvers.h b/src/cbmc/cbmc_solvers.h index 4e31415743f..42d47fcaed3 100644 --- a/src/cbmc/cbmc_solvers.h +++ b/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(p); + } + + void set_prop(propt *p) + { + prop_ptr=std::unique_ptr(p); + } + + void set_ofstream(std::ofstream *p) + { + ofstream_ptr=std::unique_ptr(p); + } + + // the objects are deleted in the opposite order they appear below + std::unique_ptr ofstream_ptr; + std::unique_ptr prop_ptr; + std::unique_ptr prop_conv_ptr; }; // returns a solvert object