Skip to content

Improve solver factory #3588

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 2 commits into from
Dec 20, 2018
Merged

Improve solver factory #3588

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
b273ac8
Move solver_factoryt definitions into .cpp file
peterschrammel Dec 17, 2018
b76cd5f
Optimize imports
peterschrammel Dec 17, 2018
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
87 changes: 82 additions & 5 deletions src/goto-checker/solver_factory.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,22 +11,99 @@ Author: Daniel Kroening, Peter Schrammel

#include "solver_factory.h"

#include <fstream>
#include <iostream>
#include <memory>
#include <string>

#include <util/exception_utils.h>
#include <util/make_unique.h>
#include <util/unicode.h>
#include <util/message.h>
#include <util/namespace.h>
#include <util/options.h>
#include <util/symbol_table.h>
#include <util/version.h>

#ifdef _MSC_VER
#include <util/unicode.h>
#endif

#include <solvers/flattening/bv_dimacs.h>
#include <solvers/prop/prop.h>
#include <solvers/prop/prop_conv.h>
#include <solvers/refinement/bv_refinement.h>
#include <solvers/refinement/string_refinement.h>
#include <solvers/sat/dimacs_cnf.h>
#include <solvers/sat/satcheck.h>
#include <solvers/smt2/smt2_dec.h>

solver_factoryt::solver_factoryt(
const optionst &_options,
const symbol_tablet &_symbol_table,
message_handlert &_message_handler,
bool _output_xml_in_refinement)
: options(_options),
symbol_table(_symbol_table),
ns(_symbol_table),
message_handler(_message_handler),
output_xml_in_refinement(_output_xml_in_refinement)
{
}

solver_factoryt::solvert::solvert(std::unique_ptr<prop_convt> p)
: prop_conv_ptr(std::move(p))
{
}

solver_factoryt::solvert::solvert(
std::unique_ptr<prop_convt> p1,
std::unique_ptr<propt> p2)
: prop_ptr(std::move(p2)), prop_conv_ptr(std::move(p1))
{
}

solver_factoryt::solvert::solvert(
std::unique_ptr<prop_convt> p1,
std::unique_ptr<std::ofstream> p2)
: ofstream_ptr(std::move(p2)), prop_conv_ptr(std::move(p1))
{
}

prop_convt &solver_factoryt::solvert::prop_conv() const
{
PRECONDITION(prop_conv_ptr != nullptr);
return *prop_conv_ptr;
}

propt &solver_factoryt::solvert::prop() const
{
PRECONDITION(prop_ptr != nullptr);
return *prop_ptr;
}

void solver_factoryt::solvert::set_prop_conv(std::unique_ptr<prop_convt> p)
{
prop_conv_ptr = std::move(p);
}

void solver_factoryt::solvert::set_prop(std::unique_ptr<propt> p)
{
prop_ptr = std::move(p);
}

void solver_factoryt::solvert::set_ofstream(std::unique_ptr<std::ofstream> p)
{
ofstream_ptr = std::move(p);
}

std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_solver()
{
if(options.get_bool_option("dimacs"))
return get_dimacs();
if(options.get_bool_option("refine"))
return get_bv_refinement();
else if(options.get_bool_option("refine-strings"))
return get_string_refinement();
if(options.get_bool_option("smt2"))
return get_smt2(get_smt2_solver_type());
return get_default();
}

/// Uses the options to pick an SMT 2.0 solver
/// \return An smt2_dect::solvert giving the solver to use.
Expand Down
102 changes: 23 additions & 79 deletions src/goto-checker/solver_factory.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,109 +12,53 @@ Author: Daniel Kroening, Peter Schrammel
#ifndef CPROVER_GOTO_CHECKER_SOLVER_FACTORY_H
#define CPROVER_GOTO_CHECKER_SOLVER_FACTORY_H

#include <list>
#include <map>
#include <memory>

#include <util/options.h>

#include <goto-symex/symex_target_equation.h>
#include <solvers/prop/prop.h>
#include <solvers/prop/prop_conv.h>
#include <solvers/sat/cnf.h>
#include <solvers/sat/satcheck.h>
#include <solvers/smt2/smt2_dec.h>

class message_handlert;
class namespacet;
class optionst;
class propt;
class prop_convt;
class symbol_tablet;

class solver_factoryt
{
public:
solver_factoryt(
const optionst &_options,
const symbol_tablet &_symbol_table,
message_handlert &_message_handler,
bool _output_xml_in_refinement)
: options(_options),
symbol_table(_symbol_table),
ns(_symbol_table),
message_handler(_message_handler),
output_xml_in_refinement(_output_xml_in_refinement)
{
}
bool _output_xml_in_refinement);

// The solver class,
// which owns a variety of allocated objects.
class solvert
{
public:
solvert()
{
}

explicit solvert(std::unique_ptr<prop_convt> p)
: prop_conv_ptr(std::move(p))
{
}

solvert(std::unique_ptr<prop_convt> p1, std::unique_ptr<propt> p2)
: prop_ptr(std::move(p2)), prop_conv_ptr(std::move(p1))
{
}

solvert(std::unique_ptr<prop_convt> p1, std::unique_ptr<std::ofstream> p2)
: ofstream_ptr(std::move(p2)), prop_conv_ptr(std::move(p1))
{
}

prop_convt &prop_conv() const
{
PRECONDITION(prop_conv_ptr != nullptr);
return *prop_conv_ptr;
}

propt &prop() const
{
PRECONDITION(prop_ptr != nullptr);
return *prop_ptr;
}

void set_prop_conv(std::unique_ptr<prop_convt> p)
{
prop_conv_ptr = std::move(p);
}

void set_prop(std::unique_ptr<propt> p)
{
prop_ptr = std::move(p);
}

void set_ofstream(std::unique_ptr<std::ofstream> p)
{
ofstream_ptr = std::move(p);
}
solvert() = default;
explicit solvert(std::unique_ptr<prop_convt> p);
solvert(std::unique_ptr<prop_convt> p1, std::unique_ptr<propt> p2);
solvert(std::unique_ptr<prop_convt> p1, std::unique_ptr<std::ofstream> p2);

prop_convt &prop_conv() const;
propt &prop() const;

void set_prop_conv(std::unique_ptr<prop_convt> p);
void set_prop(std::unique_ptr<propt> p);
void set_ofstream(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
virtual std::unique_ptr<solvert> get_solver()
{
if(options.get_bool_option("dimacs"))
return get_dimacs();
if(options.get_bool_option("refine"))
return get_bv_refinement();
else if(options.get_bool_option("refine-strings"))
return get_string_refinement();
if(options.get_bool_option("smt2"))
return get_smt2(get_smt2_solver_type());
return get_default();
}

virtual ~solver_factoryt()
{
}
/// Returns a solvert object
virtual std::unique_ptr<solvert> get_solver();

virtual ~solver_factoryt() = default;

protected:
const optionst &options;
Expand Down