cprover
Toggle main menu visibility
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/options.h
>
7
8
#include <
ansi-c/goto-conversion/goto_check_c.h
>
9
#include <
goto-checker/solver_factory.h
>
10
11
api_optionst
api_optionst::create
()
12
{
13
return
api_optionst
{};
14
}
15
16
static
std::unique_ptr<optionst>
make_internal_default_options
()
17
{
18
std::unique_ptr<optionst> options = std::make_unique<optionst>();
19
cmdlinet
command_line;
20
PARSE_OPTIONS_GOTO_CHECK
(command_line, (*options));
21
parse_solver_options
(command_line, *options);
22
options->set_option(
"built-in-assertions"
,
true
);
23
options->set_option(
"arrays-uf"
,
"auto"
);
24
options->set_option(
"depth"
, UINT32_MAX);
25
options->set_option(
"sat-preprocessor"
,
true
);
26
return
options;
27
}
28
29
api_optionst
&
api_optionst::simplify
(
bool
on)
30
{
31
simplify_enabled
= on;
32
return
*
this
;
33
}
34
35
api_optionst
&
api_optionst::drop_unused_functions
(
bool
on)
36
{
37
drop_unused_functions_enabled
= on;
38
return
*
this
;
39
}
40
41
api_optionst
&
api_optionst::validate_goto_model
(
bool
on)
42
{
43
validate_goto_model_enabled
= on;
44
return
*
this
;
45
}
46
47
std::unique_ptr<optionst>
api_optionst::to_engine_options
()
const
48
{
49
auto
engine_options =
make_internal_default_options
();
50
engine_options->set_option(
"simplify"
,
simplify_enabled
);
51
return
engine_options;
52
}
make_internal_default_options
static std::unique_ptr< optionst > make_internal_default_options()
Definition
api_options.cpp:16
api_options.h
api_optionst::drop_unused_functions
api_optionst & drop_unused_functions(bool on)
Definition
api_options.cpp:35
api_optionst::simplify_enabled
bool simplify_enabled
Definition
api_options.h:13
api_optionst::simplify
api_optionst & simplify(bool on)
Definition
api_options.cpp:29
api_optionst::drop_unused_functions_enabled
bool drop_unused_functions_enabled
Definition
api_options.h:16
api_optionst::api_optionst
api_optionst()=default
api_optionst::to_engine_options
std::unique_ptr< optionst > to_engine_options() const
Definition
api_options.cpp:47
api_optionst::validate_goto_model_enabled
bool validate_goto_model_enabled
Definition
api_options.h:19
api_optionst::create
static api_optionst create()
Definition
api_options.cpp:11
api_optionst::validate_goto_model
api_optionst & validate_goto_model(bool on)
Definition
api_options.cpp:41
cmdlinet
Definition
cmdline.h:20
cmdline.h
goto_check_c.h
Program Transformation.
PARSE_OPTIONS_GOTO_CHECK
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
Definition
goto_check_c.h:109
options.h
Options.
parse_solver_options
void parse_solver_options(const cmdlinet &cmdline, optionst &options)
Parse solver-related command-line parameters in cmdline and set corresponding values in options.
Definition
solver_factory.cpp:720
solver_factory.h
Solver Factory.
libcprover-cpp
api_options.cpp
Generated by
1.17.0