mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

reorder fields of context_params to save memory

Browse source 
plus improve error checking in context_params::set_uint
This commit is contained in:
Nuno Lopes 2021-04-13 18:35:58 +01:00
parent 49906a5a58
commit 524dcd35f9
2 changed files with 7 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/params/context_params.cpp
View file

@ -40,18 +40,11 @@ void context_params::set_bool(bool & opt, char const * param, char const * value
}
void context_params::set_uint(unsigned & opt, char const * param, char const * value) {
bool is_uint = true;
size_t sz = strlen(value);
for (unsigned i = 0; i < sz; i++) {
if (!(value[i] >= '0' && value[i] <= '9'))
is_uint = false;
}
char *endptr;
long val = strtol(value, &endptr, 10);
opt = static_cast<unsigned>(val);
if (is_uint) {
long val = strtol(value, nullptr, 10);
opt = static_cast<unsigned>(val);
}
else {
if (!*value || *endptr) {
std::stringstream strm;
strm << "invalid value '" << value << "' for unsigned int parameter '" << param << "'";
throw default_exception(strm.str());

8
src/params/context_params.h
View file

@ -28,19 +28,19 @@ class context_params {
unsigned m_rlimit { 0 };
public:
unsigned m_timeout { UINT_MAX } ;
std::string m_dot_proof_file;
std::string m_trace_file_name;
bool m_auto_config { true };
bool m_proof { false };
std::string m_dot_proof_file;
bool m_debug_ref_count { false };
bool m_trace { false };
std::string m_trace_file_name;
bool m_well_sorted_check { false };
bool m_model { true };
bool m_model_validate { false };
bool m_dump_models { false };
bool m_unsat_core { false };
bool m_smtlib2_compliant { false }; // it must be here because it enable/disable the use of coercions in the ast_manager.
unsigned m_timeout { UINT_MAX } ;
bool m_statistics { false };
bool m_unicode { true };
@ -71,5 +71,3 @@ public:
};