mirror of
				https://github.com/Z3Prover/z3
				synced 2025-10-28 10:19:23 +00:00 
			
		
		
		
	use stdbool #1526 instead of int
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
		
							parent
							
								
									78744e589c
								
							
						
					
					
						commit
						76dec85c93
					
				
					 4 changed files with 18 additions and 2 deletions
				
			
		|  | @ -957,11 +957,16 @@ def def_API(name, result, params): | |||
|                 log_c.write(" }\n") | ||||
|                 log_c.write("  Au(a%s);\n" % sz) | ||||
|                 exe_c.write("in.get_uint_array(%s)" % i) | ||||
|             elif ty == INT or ty == BOOL: | ||||
|             elif ty == INT: | ||||
|                 log_c.write("U(a%s[i]);" % i) | ||||
|                 log_c.write(" }\n") | ||||
|                 log_c.write("  Au(a%s);\n" % sz) | ||||
|                 exe_c.write("in.get_int_array(%s)" % i) | ||||
|             elif ty == BOOL: | ||||
|                 log_c.write("U(a%s[i]);" % i) | ||||
|                 log_c.write(" }\n") | ||||
|                 log_c.write("  Au(a%s);\n" % sz) | ||||
|                 exe_c.write("in.get_bool_array(%s)" % i) | ||||
|             else: | ||||
|                 error ("unsupported parameter for %s, %s, %s" % (ty, name, p)) | ||||
|         elif kind == OUT_ARRAY: | ||||
|  |  | |||
|  | @ -82,7 +82,7 @@ DEFINE_TYPE(Z3_rcf_num); | |||
| /**
 | ||||
|    \brief Z3 Boolean type. It is just an alias for \c int. | ||||
| */ | ||||
| typedef int Z3_bool; | ||||
| typedef bool Z3_bool; | ||||
| 
 | ||||
| /**
 | ||||
|    \brief Z3 string type. It is just an alias for \ccode{const char *}. | ||||
|  |  | |||
|  | @ -630,6 +630,12 @@ struct z3_replayer::imp { | |||
|         return m_int_arrays[idx].c_ptr(); | ||||
|     } | ||||
| 
 | ||||
|     bool * get_bool_array(unsigned pos) const { | ||||
|         check_arg(pos, UINT_ARRAY); | ||||
|         unsigned idx = static_cast<unsigned>(m_args[pos].m_uint); | ||||
|         return reinterpret_cast<bool*>(m_unsigned_arrays[idx].c_ptr()); | ||||
|     } | ||||
| 
 | ||||
|     Z3_symbol * get_symbol_array(unsigned pos) const { | ||||
|         check_arg(pos, SYMBOL_ARRAY); | ||||
|         unsigned idx = static_cast<unsigned>(m_args[pos].m_uint); | ||||
|  | @ -761,6 +767,10 @@ int * z3_replayer::get_int_array(unsigned pos) const { | |||
|     return m_imp->get_int_array(pos); | ||||
| } | ||||
| 
 | ||||
| bool * z3_replayer::get_bool_array(unsigned pos) const { | ||||
|     return m_imp->get_bool_array(pos); | ||||
| } | ||||
| 
 | ||||
| Z3_symbol * z3_replayer::get_symbol_array(unsigned pos) const { | ||||
|     return m_imp->get_symbol_array(pos); | ||||
| } | ||||
|  |  | |||
|  | @ -51,6 +51,7 @@ public: | |||
| 
 | ||||
|     unsigned * get_uint_array(unsigned pos) const; | ||||
|     int * get_int_array(unsigned pos) const; | ||||
|     bool * get_bool_array(unsigned pos) const; | ||||
|     Z3_symbol * get_symbol_array(unsigned pos) const; | ||||
|     void ** get_obj_array(unsigned pos) const; | ||||
| 
 | ||||
|  |  | |||
		Loading…
	
	Add table
		Add a link
		
	
		Reference in a new issue