cprover
Loading...
Searching...
No Matches
api_options.cpp
Go to the documentation of this file.
1// Author: Fotis Koutoulakis for Diffblue Ltd.
2
3#include "api_options.h"
4
5#include <util/cmdline.h>
6#include <util/make_unique.h>
7#include <util/options.h>
8
11
16
17static std::unique_ptr<optionst> make_internal_default_options()
18{
19 std::unique_ptr<optionst> options = util_make_unique<optionst>();
20 cmdlinet command_line;
21 PARSE_OPTIONS_GOTO_CHECK(command_line, (*options));
22 parse_solver_options(command_line, *options);
23 options->set_option("built-in-assertions", true);
24 options->set_option("arrays-uf", "auto");
25 options->set_option("depth", UINT32_MAX);
26 options->set_option("sat-preprocessor", true);
27 return options;
28}
29
31{
33 return *this;
34}
35
41
47
48std::unique_ptr<optionst> api_optionst::to_engine_options() const
49{
50 auto engine_options = make_internal_default_options();
51 engine_options->set_option("simplify", simplify_enabled);
52 return engine_options;
53}
static std::unique_ptr< optionst > make_internal_default_options()
api_optionst & drop_unused_functions(bool on)
bool simplify_enabled
Definition api_options.h:13
api_optionst & simplify(bool on)
bool drop_unused_functions_enabled
Definition api_options.h:16
std::unique_ptr< optionst > to_engine_options() const
bool validate_goto_model_enabled
Definition api_options.h:19
static api_optionst create()
api_optionst & validate_goto_model(bool on)
Program Transformation.
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
std::unique_ptr< T > util_make_unique(Ts &&... ts)
Definition make_unique.h:19
Options.
void parse_solver_options(const cmdlinet &cmdline, optionst &options)
Parse solver-related command-line parameters in cmdline and set corresponding values in options.
Solver Factory.