Add -smt-random-seed
MODIFY
smt/ctx.cpp
smt/ctx.cpp
@@ -29,6 +29,7 @@ void context::init() {
Z3_global_param_set("model.partial", "true");
Z3_global_param_set("smt.ematching", "false");
Z3_global_param_set("smt.mbqi.max_iterations", "1000000");
+ Z3_global_param_set("smt.random_seed", get_random_seed());
Z3_global_param_set("timeout", get_query_timeout());
Z3_global_param_set("memory_high_watermark", "2147483648"); // 2 GBs
// Disable Z3's use of UFs for NaNs when converting FPs to BVs

MODIFY
smt/smt.cpp
smt/smt.cpp
@@ -41,15 +41,24 @@ void smt_initializer::destroy() {
static string query_timeout = "10000";
+static string rand_seed = "0";
void set_query_timeout(string ms) {
query_timeout = move(ms);
}
+void set_random_seed(string seed) {
+ rand_seed = move(seed);
+}
+
const char* get_query_timeout() {
return query_timeout.c_str();
}
+const char *get_random_seed() {
+ return rand_seed.c_str();
+}
+
static uint64_t z3_memory_limit = 1ull << 30; // 1 GB

MODIFY
smt/smt.h
smt/smt.h
@@ -20,6 +20,8 @@ private:
void set_query_timeout(std::string ms);
const char* get_query_timeout();
+void set_random_seed(std::string seed);
+const char *get_random_seed();
void set_memory_limit(uint64_t limit);
bool hit_memory_limit();

MODIFY
tools/alive-tv.cpp
tools/alive-tv.cpp
@@ -63,6 +63,11 @@ static llvm::cl::opt<unsigned> opt_smt_to(
"smt-to", llvm::cl::desc("Timeout for SMT queries (default=1000)"),
llvm::cl::init(1000), llvm::cl::value_desc("ms"), llvm::cl::cat(opt_alive));
+static llvm::cl::opt<unsigned> opt_smt_random_seed(
+ "smt-random-seed",
+ llvm::cl::desc("Random seed for the SMT solver (default=0)"),
+ llvm::cl::init(0), llvm::cl::cat(opt_alive));
+
static llvm::cl::opt<bool> opt_smt_verbose(
"smt-verbose", llvm::cl::desc("SMT verbose mode"),
llvm::cl::cat(opt_alive), llvm::cl::init(false));
@@ -416,6 +421,7 @@ convenient way to demonstrate an existing optimizer bug.
smt::solver_print_queries(opt_smt_verbose);
smt::solver_tactic_verbose(opt_tactic_verbose);
smt::set_query_timeout(to_string(opt_smt_to));
+ smt::set_random_seed(to_string(opt_smt_random_seed));
smt::set_memory_limit((uint64_t)opt_max_mem * 1024 * 1024);
config::skip_smt = opt_smt_skip;
config::io_nobuiltin = opt_io_nobuiltin;

MODIFY
tools/alive.cpp
tools/alive.cpp
@@ -29,6 +29,7 @@ static void show_help() {
" -v\t\t\tVerbose mode\n"
" -smt-stats\t\tShow SMT statistics\n"
" -smt-to:x\t\tTimeout for SMT queries in ms\n"
+ " -smt-random-seed:x\tRandom seed for the SMT solver\n"
" -max-mem:x\t\tMax memory consumption in MB (aprox)\n"
" -smt-verbose\t\tPrint all SMT queries\n"
" -tactic-verbose\tDebug SMT tactics\n"
@@ -59,6 +60,8 @@ int main(int argc, char **argv) {
show_smt_stats = true;
else if (arg.compare(0, 8, "-smt-to:") == 0 && arg.size() > 8)
smt::set_query_timeout(arg.substr(8).data());
+ else if (arg.compare(0, 17, "-smt-random-seed:") == 0 && arg.size() > 17)
+ smt::set_random_seed(arg.substr(17).data());
else if (arg.compare(0, 9, "-max-mem:") == 0 && arg.size() > 9)
smt::set_memory_limit(strtoul(arg.substr(9).data(), nullptr, 10) *
1024 * 1024);

MODIFY
tv/tv.cpp
tv/tv.cpp
@@ -48,6 +48,11 @@ llvm::cl::opt<unsigned> opt_smt_to(
"tv-smt-to", llvm::cl::desc("Alive: timeout for SMT queries"),
llvm::cl::init(1000), llvm::cl::value_desc("ms"));
+llvm::cl::opt<unsigned> opt_smt_random_seed(
+ "tv-smt-random-seed",
+ llvm::cl::desc("Alive: Random seed for the SMT solver (default=0)"),
+ llvm::cl::init(0));
+
llvm::cl::opt<unsigned> opt_max_mem(
"tv-max-mem", llvm::cl::desc("Alive: max memory (aprox)"),
llvm::cl::init(1024), llvm::cl::value_desc("MB"));
@@ -261,6 +266,7 @@ struct TVPass final : public llvm::FunctionPass {
smt::solver_print_queries(opt_smt_verbose);
smt::solver_tactic_verbose(opt_tactic_verbose);
smt::set_query_timeout(to_string(opt_smt_to));
+ smt::set_random_seed(to_string(opt_smt_random_seed));
smt::set_memory_limit(opt_max_mem * 1024 * 1024);
config::skip_smt = opt_smt_skip;
config::io_nobuiltin = opt_io_nobuiltin;

Add -smt-random-seed (#496)