Skip to content

Commit

Permalink
Revert "remove unused random seed parameter on cmd_context"
Browse files Browse the repository at this point in the history
This reverts commit e2a9cb8.
  • Loading branch information
NikolajBjorner committed Oct 29, 2019
1 parent 4faaff5 commit 18b8089
Show file tree
Hide file tree
Showing 3 changed files with 14 additions and 2 deletions.
12 changes: 10 additions & 2 deletions src/cmd_context/basic_cmds.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -323,6 +323,7 @@ class set_get_option_cmd : public cmd {
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;
Expand All @@ -337,7 +338,7 @@ class set_get_option_cmd : public cmd {
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;
}

Expand All @@ -358,6 +359,7 @@ class set_get_option_cmd : public cmd {
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"),
Expand Down Expand Up @@ -501,7 +503,10 @@ class set_option_cmd : public set_get_option_cmd {
}

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) {
Expand Down Expand Up @@ -589,6 +594,9 @@ class get_option_cmd : public set_get_option_cmd {
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());
}
Expand Down
1 change: 1 addition & 0 deletions src/cmd_context/cmd_context.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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),
Expand Down
3 changes: 3 additions & 0 deletions src/cmd_context/cmd_context.h
Original file line number Diff line number Diff line change
Expand Up @@ -185,6 +185,7 @@ class cmd_context : public progress_callback, public tactic_manager, public ast_
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;
Expand Down Expand Up @@ -336,6 +337,8 @@ class cmd_context : public progress_callback, public tactic_manager, public ast_
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;
Expand Down

0 comments on commit 18b8089

Please sign in to comment.