From 18b8089a1ee1b060ffb0cb728acd56f24333c70b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 29 Oct 2019 11:05:50 -0700
Subject: [PATCH] Revert "remove unused random seed parameter on cmd_context"
This reverts commit e2a9cb80e27049da644cfdddf705a8e450d18743.
---
src/cmd_context/basic_cmds.cpp | 12 ++++++++++--
src/cmd_context/cmd_context.cpp | 1 +
src/cmd_context/cmd_context.h | 3 +++
3 files changed, 14 insertions(+), 2 deletions(-)
diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp
index 0728a0bd4..1c4f04ddd 100644
--- a/src/cmd_context/basic_cmds.cpp
+++ b/src/cmd_context/basic_cmds.cpp
@@ -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());
}
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index b3df1e1e0..8e844a406 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -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),
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index 140259867..fa9c2f296 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -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;