make generation of "some" Boolean value fair

Z3Prover · Mar 20, 2023 · a9e6e56 · a9e6e56
1 parent d1c7ff1
commit a9e6e56
Show file tree

Hide file tree

Showing 3 changed files with 7 additions and 6 deletions.
diff --git a/src/model/value_factory.cpp b/src/model/value_factory.cpp
@@ -28,13 +28,13 @@ value_factory::value_factory(ast_manager & m, family_id fid):
 value_factory::~value_factory() {
 }
 
-basic_factory::basic_factory(ast_manager & m):
-    value_factory(m, m.get_basic_family_id()) {
+basic_factory::basic_factory(ast_manager & m, unsigned seed):
+    value_factory(m, m.get_basic_family_id()), m_rand(seed) {
 }
 
 expr * basic_factory::get_some_value(sort * s) {
-    if (m_manager.is_bool(s))
-        return m_manager.mk_false();
+    if (m_manager.is_bool(s)) 
+        return (m_rand() % 2 == 0) ? m_manager.mk_false() : m_manager.mk_true();
     return nullptr;
 }
 

diff --git a/src/model/value_factory.h b/src/model/value_factory.h
@@ -60,8 +60,9 @@ class value_factory {
 };
 
 class basic_factory : public value_factory {
+    random_gen m_rand;
 public:
-    basic_factory(ast_manager & m);
+    basic_factory(ast_manager & m, unsigned seed);
 
     expr * get_some_value(sort * s) override;
 

diff --git a/src/smt/proto_model/proto_model.cpp b/src/smt/proto_model/proto_model.cpp
@@ -32,7 +32,7 @@ proto_model::proto_model(ast_manager & m, params_ref const & p):
     model_core(m),
     m_eval(*this),
     m_rewrite(m) {
-    register_factory(alloc(basic_factory, m));
+    register_factory(alloc(basic_factory, m, m.get_num_asts()));
     m_user_sort_factory = alloc(user_sort_factory, m);
     register_factory(m_user_sort_factory);
     m_model_partial = model_params(p).partial();