remove unused random seed parameter on cmd_context

Signed-off-by: Nikolaj Bjorner <[email protected]>
Z3Prover · Oct 22, 2019 · e2a9cb8 · e2a9cb8
1 parent 9847675
commit e2a9cb8
Show file tree

Hide file tree

Showing 3 changed files with 2 additions and 14 deletions.
diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp
@@ -323,7 +323,6 @@ 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;
@@ -338,7 +337,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_random_seed || s == m_verbosity || s == m_global_decls || s == m_global_declarations ||
+            s == m_verbosity || s == m_global_decls || s == m_global_declarations ||
             s == m_produce_assertions || s == m_reproducible_resource_limit;
     }
 
@@ -359,7 +358,6 @@ 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"),
@@ -503,10 +501,7 @@ class set_option_cmd : public set_get_option_cmd {
     }
 
     void set_next_arg(cmd_context & ctx, rational const & val) override {
-        if (m_option == m_random_seed) {
-            ctx.set_random_seed(to_unsigned(val));
-        }
-        else if (m_option == m_reproducible_resource_limit) {
+        if (m_option == m_reproducible_resource_limit) {
             ctx.params().set_rlimit(to_unsigned(val));
         }
         else if (m_option == m_verbosity) {
@@ -594,9 +589,6 @@ 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());
         }

diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
@@ -466,7 +466,6 @@ 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
@@ -185,7 +185,6 @@ 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;
@@ -337,8 +336,6 @@ 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;