mirror of
				https://github.com/Z3Prover/z3
				synced 2025-11-04 13:29:11 +00:00 
			
		
		
		
	added repr method to ParamDescrs
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
		
							parent
							
								
									1f61381172
								
							
						
					
					
						commit
						b0a2d8488d
					
				
					 1 changed files with 15 additions and 0 deletions
				
			
		
							
								
								
									
										15
									
								
								python/z3.py
									
										
									
									
									
								
							
							
						
						
									
										15
									
								
								python/z3.py
									
										
									
									
									
								
							| 
						 | 
					@ -43,6 +43,7 @@ from z3types import *
 | 
				
			||||||
from z3consts import *
 | 
					from z3consts import *
 | 
				
			||||||
from z3tactics import *
 | 
					from z3tactics import *
 | 
				
			||||||
from z3printer import *
 | 
					from z3printer import *
 | 
				
			||||||
 | 
					import io
 | 
				
			||||||
 | 
					
 | 
				
			||||||
# We use _z3_assert instead of the assert command because we want to
 | 
					# We use _z3_assert instead of the assert command because we want to
 | 
				
			||||||
# produce nice error messages in Z3Py at rise4fun.com
 | 
					# produce nice error messages in Z3Py at rise4fun.com
 | 
				
			||||||
| 
						 | 
					@ -4419,6 +4420,20 @@ class ParamDescrsRef:
 | 
				
			||||||
        else:
 | 
					        else:
 | 
				
			||||||
            return self.get_kind(arg)
 | 
					            return self.get_kind(arg)
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					    def __repr__(self):
 | 
				
			||||||
 | 
					        r = io.StringIO()
 | 
				
			||||||
 | 
					        first = True
 | 
				
			||||||
 | 
					        r.write(u'(')
 | 
				
			||||||
 | 
					        for i in range(self.size()):
 | 
				
			||||||
 | 
					            if first:
 | 
				
			||||||
 | 
					                first = False
 | 
				
			||||||
 | 
					            else:
 | 
				
			||||||
 | 
					                r.write(u' ')
 | 
				
			||||||
 | 
					            r.write(u'%s' % self.get_name(i))
 | 
				
			||||||
 | 
					        r.write(u')')
 | 
				
			||||||
 | 
					        return r.getvalue()
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					
 | 
				
			||||||
#########################################
 | 
					#########################################
 | 
				
			||||||
#
 | 
					#
 | 
				
			||||||
# Goals
 | 
					# Goals
 | 
				
			||||||
| 
						 | 
					
 | 
				
			||||||
		Loading…
	
	Add table
		Add a link
		
	
		Reference in a new issue