Skip to content

cleanup of CBMC solver factory #568

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Feb 22, 2017
Merged

cleanup of CBMC solver factory #568

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
146 changes: 18 additions & 128 deletions src/cbmc/cbmc_solvers.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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;
}

Expand All @@ -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);
}

/*******************************************************************\
Expand Down Expand Up @@ -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);
}

/*******************************************************************\
Expand Down Expand Up @@ -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);
}
}

Expand Down Expand Up @@ -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);
}
}

Expand Down
53 changes: 42 additions & 11 deletions src/cbmc/cbmc_solvers.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down