mirror of
				https://github.com/Z3Prover/z3
				synced 2025-10-31 19:52:29 +00:00 
			
		
		
		
	have solver pretty print declarations, include also datatype declarations
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
		
							parent
							
								
									052ac51ed7
								
							
						
					
					
						commit
						c7649088e7
					
				
					 2 changed files with 3 additions and 3 deletions
				
			
		|  | @ -18,6 +18,8 @@ Revision History: | |||
| --*/ | ||||
| 
 | ||||
| #include "ast_pp_util.h" | ||||
| #include "ast_smt2_pp.h" | ||||
| #include "ast_smt_pp.h" | ||||
| 
 | ||||
| void ast_pp_util::collect(expr* e) { | ||||
|     coll.visit(e); | ||||
|  |  | |||
|  | @ -7,7 +7,7 @@ Module Name: | |||
| 
 | ||||
| Abstract: | ||||
| 
 | ||||
|     <abstract> | ||||
|     Utilities for printing SMT2 declarations and assertions. | ||||
| 
 | ||||
| Author: | ||||
| 
 | ||||
|  | @ -20,8 +20,6 @@ Revision History: | |||
| #define AST_PP_UTIL_H_ | ||||
| 
 | ||||
| #include "decl_collector.h" | ||||
| #include "ast_smt2_pp.h" | ||||
| #include "ast_smt_pp.h" | ||||
| 
 | ||||
| class ast_pp_util { | ||||
|     ast_manager&        m; | ||||
|  |  | |||
		Loading…
	
	Add table
		Add a link
		
	
		Reference in a new issue