reformat code to remove brackets

Z3Prover · May 11, 2023 · f6ab5a6 · f6ab5a6
1 parent 12e45c9
commit f6ab5a6
Showing 1 changed file with 19 additions and 27 deletions.
diff --git a/src/smt/proto_model/proto_model.cpp b/src/smt/proto_model/proto_model.cpp
@@ -288,42 +288,33 @@ bool proto_model::is_finite(sort * s) const {
 }
 
 expr * proto_model::get_some_value(sort * s) {
-    if (m.is_uninterp(s)) {
-        return m_user_sort_factory->get_some_value(s);
-    }
-    else if (value_factory * f = get_factory(s->get_family_id())) {
-        return f->get_some_value(s);
-    }
-    else {
+    if (m.is_uninterp(s)) 
+        return m_user_sort_factory->get_some_value(s);    
+    else if (value_factory * f = get_factory(s->get_family_id())) 
+        return f->get_some_value(s);    
+    else 
         // there is no factory for the family id, then assume s is uninterpreted.
-        return m_user_sort_factory->get_some_value(s);
-    }
+        return m_user_sort_factory->get_some_value(s);    
 }
 
 bool proto_model::get_some_values(sort * s, expr_ref & v1, expr_ref & v2) {
-    if (m.is_uninterp(s)) {
-        return m_user_sort_factory->get_some_values(s, v1, v2);
-    }
-    else if (value_factory * f = get_factory(s->get_family_id())) {
-        return f->get_some_values(s, v1, v2);
-    }
-    else {
-        return false;
-    }
+    if (m.is_uninterp(s)) 
+        return m_user_sort_factory->get_some_values(s, v1, v2);    
+    else if (value_factory * f = get_factory(s->get_family_id())) 
+        return f->get_some_values(s, v1, v2);    
+    else 
+        return false;    
 }
 
 expr * proto_model::get_fresh_value(sort * s) {
-    if (m.is_uninterp(s)) {
-        return m_user_sort_factory->get_fresh_value(s);
-    }
-    else if (value_factory * f = get_factory(s->get_family_id())) {
-        return f->get_fresh_value(s);
-    }
-    else {
+    if (m.is_uninterp(s)) 
+        return m_user_sort_factory->get_fresh_value(s);    
+    else if (value_factory * f = get_factory(s->get_family_id())) 
+        return f->get_fresh_value(s);    
+    else 
         // Use user_sort_factory if the theory has no support for model construnction.
         // This is needed when dummy theories are used for arithmetic or arrays.
-        return m_user_sort_factory->get_fresh_value(s);
-    }
+        return m_user_sort_factory->get_fresh_value(s);    
 }
 
 void proto_model::register_value(expr * n) {
@@ -354,6 +345,7 @@ void proto_model::compress() {
 void proto_model::complete_partial_func(func_decl * f, bool use_fresh) {
     func_interp * fi = get_func_interp(f);
     if (fi && fi->is_partial()) {
+        verbose_stream() << "complete " << f->get_name() << " " << use_fresh << "\n";
         expr * else_value;
         if (use_fresh) {
             else_value = get_fresh_value(f->get_range());