mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-05 17:14:07 +00:00
Code Activity

Revert "remove unused random seed parameter on cmd_context"

Browse source 
This reverts commit e2a9cb80e2.
This commit is contained in:
Nikolaj Bjorner 2019-10-29 11:05:50 -07:00
parent 4faaff5b76
commit 18b8089a1e
3 changed files with 14 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/cmd_context/basic_cmds.cpp
View file

@ -323,6 +323,7 @@ protected:
symbol m_produce_assertions;
symbol m_regular_output_channel;
symbol m_diagnostic_output_channel;
symbol m_random_seed;
symbol m_verbosity;
symbol m_global_decls;
symbol m_global_declarations;
@ -337,7 +338,7 @@ protected:
s == m_interactive_mode || s == m_produce_proofs || s == m_produce_unsat_cores || s == m_produce_unsat_assumptions ||
s == m_produce_models || s == m_produce_assignments ||
s == m_regular_output_channel || s == m_diagnostic_output_channel ||
s == m_verbosity || s == m_global_decls || s == m_global_declarations ||
s == m_random_seed || s == m_verbosity || s == m_global_decls || s == m_global_declarations ||
s == m_produce_assertions || s == m_reproducible_resource_limit;
}
@ -358,6 +359,7 @@ public:
m_produce_assertions(":produce-assertions"),
m_regular_output_channel(":regular-output-channel"),
m_diagnostic_output_channel(":diagnostic-output-channel"),
m_random_seed(":random-seed"),
m_verbosity(":verbosity"),
m_global_decls(":global-decls"),
m_global_declarations(":global-declarations"),
@ -501,7 +503,10 @@ public:
}
void set_next_arg(cmd_context & ctx, rational const & val) override {
if (m_option == m_reproducible_resource_limit) {
if (m_option == m_random_seed) {
ctx.set_random_seed(to_unsigned(val));
}
else if (m_option == m_reproducible_resource_limit) {
ctx.params().set_rlimit(to_unsigned(val));
}
else if (m_option == m_verbosity) {
@ -589,6 +594,9 @@ public:
else if (opt == m_global_decls || opt == m_global_declarations) {
print_bool(ctx, ctx.global_decls());
}
else if (opt == m_random_seed) {
print_unsigned(ctx, ctx.random_seed());
}
else if (opt == m_verbosity) {
print_unsigned(ctx, get_verbosity_level());
}

1
src/cmd_context/cmd_context.cpp
View file

@ -466,6 +466,7 @@ cmd_context::cmd_context(bool main_ctx, ast_manager * m, symbol const & l):
m_interactive_mode(false),
m_global_decls(false),
m_print_success(m_params.m_smtlib2_compliant),
m_random_seed(0),
m_produce_unsat_cores(false),
m_produce_unsat_assumptions(false),
m_produce_assignments(false),

3
src/cmd_context/cmd_context.h
View file

@ -185,6 +185,7 @@ protected:
bool m_interactive_mode;
bool m_global_decls;
bool m_print_success;
unsigned m_random_seed;
bool m_produce_unsat_cores;
bool m_produce_unsat_assumptions;
bool m_produce_assignments;
@ -336,6 +337,8 @@ public:
void print_unsupported(symbol const & s, int line, int pos) { print_unsupported_msg(); print_unsupported_info(s, line, pos); }
bool global_decls() const { return m_global_decls; }
void set_global_decls(bool flag) { SASSERT(!has_manager()); m_global_decls = flag; }
unsigned random_seed() const { return m_random_seed; }
void set_random_seed(unsigned s) { m_random_seed = s; }
bool produce_models() const;
bool produce_proofs() const;
bool produce_unsat_cores() const;