cprover
Loading...
Searching...
No Matches
solver_factory.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Solver Factory
4
5Author: Daniel Kroening, Peter Schrammel
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_GOTO_CHECKER_SOLVER_FACTORY_H
13#define CPROVER_GOTO_CHECKER_SOLVER_FACTORY_H
14
15#include <memory>
16
18
20class namespacet;
21class optionst;
22class propt;
25
26class solver_factoryt final
27{
28public:
31 const optionst &_options,
32 const namespacet &_ns,
35
36 // The solver class,
37 // which owns a variety of allocated objects.
38 class solvert final
39 {
40 public:
41 solvert() = default;
42 explicit solvert(std::unique_ptr<decision_proceduret> p);
43 solvert(std::unique_ptr<decision_proceduret> p1, std::unique_ptr<propt> p2);
44 solvert(
45 std::unique_ptr<decision_proceduret> p1,
46 std::unique_ptr<std::ofstream> p2);
47
50 propt &prop() const;
51
52 void set_decision_procedure(std::unique_ptr<decision_proceduret> p);
53 void set_prop(std::unique_ptr<propt> p);
54 void set_ofstream(std::unique_ptr<std::ofstream> p);
55
56 // the objects are deleted in the opposite order they appear below
57 std::unique_ptr<std::ofstream> ofstream_ptr;
58 std::unique_ptr<propt> prop_ptr;
59 std::unique_ptr<decision_proceduret> decision_procedure_ptr;
60 };
61
63 virtual std::unique_ptr<solvert> get_solver();
64
65 virtual ~solver_factoryt() = default;
66
67protected:
69 const namespacet &ns;
72
73 std::unique_ptr<solvert> get_default();
74 std::unique_ptr<solvert> get_dimacs();
75 std::unique_ptr<solvert> get_external_sat();
76 std::unique_ptr<solvert> get_bv_refinement();
77 std::unique_ptr<solvert> get_string_refinement();
78 std::unique_ptr<solvert> get_incremental_smt2(std::string solver_command);
79 std::unique_ptr<solvert> get_smt2(smt2_dect::solvert solver);
80
82
86 void
88
89 // consistency checks during solver creation
90 void no_beautification();
92};
93
94#endif // CPROVER_GOTO_CHECKER_SOLVER_FACTORY_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
TO_BE_DOCUMENTED.
Definition prop.h:24
std::unique_ptr< propt > prop_ptr
std::unique_ptr< decision_proceduret > decision_procedure_ptr
void set_decision_procedure(std::unique_ptr< decision_proceduret > p)
std::unique_ptr< std::ofstream > ofstream_ptr
decision_proceduret & decision_procedure() const
stack_decision_proceduret & stack_decision_procedure() const
void set_ofstream(std::unique_ptr< std::ofstream > p)
void set_prop(std::unique_ptr< propt > p)
message_handlert & message_handler
const optionst & options
const namespacet & ns
std::unique_ptr< solvert > get_external_sat()
std::unique_ptr< solvert > get_default()
std::unique_ptr< solvert > get_dimacs()
void set_decision_procedure_time_limit(decision_proceduret &decision_procedure)
Sets the timeout of decision_procedure if the solver-time-limit option has a positive value (in secon...
std::unique_ptr< solvert > get_string_refinement()
the string refinement adds to the bit vector refinement specifications for functions from the Java st...
std::unique_ptr< solvert > get_smt2(smt2_dect::solvert solver)
const bool output_xml_in_refinement
smt2_dect::solvert get_smt2_solver_type() const
Uses the options to pick an SMT 2.0 solver.
virtual ~solver_factoryt()=default
virtual std::unique_ptr< solvert > get_solver()
Returns a solvert object.
std::unique_ptr< solvert > get_incremental_smt2(std::string solver_command)
std::unique_ptr< solvert > get_bv_refinement()
int solver(std::istream &in)