CBMC
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
17
18#include <fstream>
19#include <memory>
20
21class cmdlinet;
23class namespacet;
24class optionst;
26
27class solver_factoryt final
28{
29public:
32 const optionst &_options,
33 const namespacet &_ns,
36
37 // The solver class,
38 // which owns a variety of allocated objects.
39 class solvert final
40 {
41 public:
42 explicit solvert(std::unique_ptr<stack_decision_proceduret> p);
43 solvert(
44 std::unique_ptr<stack_decision_proceduret> p1,
45 std::unique_ptr<propt> p2);
46 solvert(
47 std::unique_ptr<stack_decision_proceduret> p1,
48 std::unique_ptr<std::ofstream> p2);
49 solvert(std::unique_ptr<boolbvt> p1, std::unique_ptr<propt> p2);
50
53
54 private:
55 // the objects are deleted in the opposite order they appear below
56 std::unique_ptr<std::ofstream> ofstream_ptr;
57 std::unique_ptr<propt> prop_ptr;
58 std::unique_ptr<stack_decision_proceduret> decision_procedure_ptr;
59 std::unique_ptr<boolbvt> decision_procedure_is_boolbvt_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
87 solver_resource_limitst &decision_procedure);
88
89 // consistency checks during solver creation
90 void no_beautification();
92};
93
96void parse_solver_options(const cmdlinet &cmdline, optionst &options);
97
98#define OPT_SOLVER \
99 "(smt1)" /* rejected, will eventually disappear */ \
100 "(smt2)" \
101 "(fpa)" \
102 "(cvc3)" \
103 "(cvc4)(cvc5)(bitwuzla)(boolector)(yices)(z3)" \
104 "(mathsat)" \
105 "(cprover-smt2)" \
106 "(incremental-smt2-solver):" \
107 "(sat-solver):" \
108 "(external-sat-solver):" \
109 "(no-sat-preprocessor)" \
110 "(beautify)" \
111 "(dimacs)" \
112 "(refine)" \
113 "(max-node-refinement):" \
114 "(refine-arrays)" \
115 "(refine-arithmetic)" \
116 "(outfile):" \
117 "(dump-smt-formula):" \
118 "(write-solver-stats-to):"
119
120#define HELP_SOLVER \
121 " {y--sat-solver} {usolver} \t use specified SAT solver\n" \
122 " {y--external-sat-solver} {ucmd} \t command to invoke SAT solver process\n" \
123 " {y--no-sat-preprocessor} \t disable the SAT solver's simplifier\n" \
124 " {y--dimacs} \t generate CNF in DIMACS format\n" \
125 " {y--beautify} \t beautify the counterexample (greedy heuristic)\n" \
126 " {y--smt1} \t use default SMT1 solver (obsolete)\n" \
127 " {y--smt2} \t use default SMT2 solver (Z3)\n" \
128 " {y--bitwuzla} \t use Bitwuzla\n" \
129 " {y--boolector} \t use Boolector\n" \
130 " {y--cprover-smt2} \t use CPROVER SMT2 solver\n" \
131 " {y--cvc3} \t use CVC3\n" \
132 " {y--cvc4} \t use CVC4\n" \
133 " {y--cvc5} \t use CVC5\n" \
134 " {y--mathsat} \t use MathSAT\n" \
135 " {y--yices} \t use Yices\n" \
136 " {y--z3} \t use Z3\n" \
137 " {y--fpa} \t use theory of floating-point arithmetic\n" \
138 " {y--refine} \t use refinement procedure (experimental)\n" \
139 " {y--refine-arrays} \t use refinement for arrays only\n" \
140 " {y--refine-arithmetic} \t refinement of arithmetic expressions only\n" \
141 " {y--max-node-refinement} \t " \
142 "maximum refinement iterations for arithmetic expressions\n" \
143 " {y--incremental-smt2-solver} {ucmd} \t " \
144 "command to invoke external SMT solver for incremental solving " \
145 "(experimental)\n" \
146 " {y--outfile} {ufilename} \t output formula to given file\n" \
147 " {y--dump-smt-formula} {ufilename} \t " \
148 "output smt incremental formula to the given file\n" \
149 " {y--write-solver-stats-to} {ujson-file} \t " \
150 "collect the solver query complexity\n"
151
152#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:562
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
std::unique_ptr< stack_decision_proceduret > decision_procedure_ptr
std::unique_ptr< propt > prop_ptr
std::unique_ptr< std::ofstream > ofstream_ptr
boolbvt & boolbv_decision_procedure() const
stack_decision_proceduret & decision_procedure() const
std::unique_ptr< boolbvt > decision_procedure_is_boolbvt_ptr
message_handlert & message_handler
const optionst & options
const namespacet & ns
std::unique_ptr< solvert > get_external_sat()
std::unique_ptr< solvert > get_default()
void set_decision_procedure_time_limit(solver_resource_limitst &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_dimacs()
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()
void solver(std::vector< framet > &frames, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const solver_optionst &solver_options, const namespacet &ns, std::vector< propertyt > &properties, std::size_t property_index)
Definition solver.cpp:44
void parse_solver_options(const cmdlinet &cmdline, optionst &options)
Parse solver-related command-line parameters in cmdline and set corresponding values in options.