mirror of
				https://github.com/Z3Prover/z3
				synced 2025-11-04 13:29:11 +00:00 
			
		
		
		
	missing files?
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
		
							parent
							
								
									b0d244c1e0
								
							
						
					
					
						commit
						752a973e53
					
				
					 4 changed files with 124 additions and 0 deletions
				
			
		
							
								
								
									
										33
									
								
								src/api/java/ReExpr.java
									
										
									
									
									
										Normal file
									
								
							
							
						
						
									
										33
									
								
								src/api/java/ReExpr.java
									
										
									
									
									
										Normal file
									
								
							| 
						 | 
					@ -0,0 +1,33 @@
 | 
				
			||||||
 | 
					/**
 | 
				
			||||||
 | 
					Copyright (c) 2012-2016 Microsoft Corporation
 | 
				
			||||||
 | 
					   
 | 
				
			||||||
 | 
					Module Name:
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					    ReExpr.java
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					Abstract:
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					Author:
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					    @author Christoph Wintersteiger (cwinter) 2012-03-15
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					Notes:
 | 
				
			||||||
 | 
					    
 | 
				
			||||||
 | 
					**/ 
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					package com.microsoft.z3;
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					/**
 | 
				
			||||||
 | 
					 * Re expressions
 | 
				
			||||||
 | 
					 **/
 | 
				
			||||||
 | 
					public class ReExpr extends Expr
 | 
				
			||||||
 | 
					{
 | 
				
			||||||
 | 
					    /**
 | 
				
			||||||
 | 
					     * Constructor for ReExpr
 | 
				
			||||||
 | 
					     * @throws Z3Exception on error
 | 
				
			||||||
 | 
					     **/
 | 
				
			||||||
 | 
					    ReExpr(Context ctx, long obj)
 | 
				
			||||||
 | 
					    {
 | 
				
			||||||
 | 
					        super(ctx, obj);
 | 
				
			||||||
 | 
					    }
 | 
				
			||||||
 | 
					}
 | 
				
			||||||
							
								
								
									
										29
									
								
								src/api/java/ReSort.java
									
										
									
									
									
										Normal file
									
								
							
							
						
						
									
										29
									
								
								src/api/java/ReSort.java
									
										
									
									
									
										Normal file
									
								
							| 
						 | 
					@ -0,0 +1,29 @@
 | 
				
			||||||
 | 
					/**
 | 
				
			||||||
 | 
					Copyright (c) 2012-2014 Microsoft Corporation
 | 
				
			||||||
 | 
					   
 | 
				
			||||||
 | 
					Module Name:
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					    ReSort.java
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					Abstract:
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					Author:
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					    @author Christoph Wintersteiger (cwinter) 2012-03-15
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					Notes:
 | 
				
			||||||
 | 
					    
 | 
				
			||||||
 | 
					**/ 
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					package com.microsoft.z3;
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					/**
 | 
				
			||||||
 | 
					 * A Regular expression sort
 | 
				
			||||||
 | 
					 **/
 | 
				
			||||||
 | 
					public class ReSort extends Sort
 | 
				
			||||||
 | 
					{
 | 
				
			||||||
 | 
					    ReSort(Context ctx, long obj)
 | 
				
			||||||
 | 
					    {
 | 
				
			||||||
 | 
					        super(ctx, obj);
 | 
				
			||||||
 | 
					    }
 | 
				
			||||||
 | 
					}
 | 
				
			||||||
							
								
								
									
										33
									
								
								src/api/java/SeqExpr.java
									
										
									
									
									
										Normal file
									
								
							
							
						
						
									
										33
									
								
								src/api/java/SeqExpr.java
									
										
									
									
									
										Normal file
									
								
							| 
						 | 
					@ -0,0 +1,33 @@
 | 
				
			||||||
 | 
					/**
 | 
				
			||||||
 | 
					Copyright (c) 2012-2016 Microsoft Corporation
 | 
				
			||||||
 | 
					   
 | 
				
			||||||
 | 
					Module Name:
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					    SeqExpr.java
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					Abstract:
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					Author:
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					    @author Christoph Wintersteiger (cwinter) 2012-03-15
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					Notes:
 | 
				
			||||||
 | 
					    
 | 
				
			||||||
 | 
					**/ 
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					package com.microsoft.z3;
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					/**
 | 
				
			||||||
 | 
					 * Seq expressions
 | 
				
			||||||
 | 
					 **/
 | 
				
			||||||
 | 
					public class SeqExpr extends Expr
 | 
				
			||||||
 | 
					{
 | 
				
			||||||
 | 
					    /**
 | 
				
			||||||
 | 
					     * Constructor for SeqExpr
 | 
				
			||||||
 | 
					     * @throws Z3Exception on error
 | 
				
			||||||
 | 
					     **/
 | 
				
			||||||
 | 
					    SeqExpr(Context ctx, long obj)
 | 
				
			||||||
 | 
					    {
 | 
				
			||||||
 | 
					        super(ctx, obj);
 | 
				
			||||||
 | 
					    }
 | 
				
			||||||
 | 
					}
 | 
				
			||||||
							
								
								
									
										29
									
								
								src/api/java/SeqSort.java
									
										
									
									
									
										Normal file
									
								
							
							
						
						
									
										29
									
								
								src/api/java/SeqSort.java
									
										
									
									
									
										Normal file
									
								
							| 
						 | 
					@ -0,0 +1,29 @@
 | 
				
			||||||
 | 
					/**
 | 
				
			||||||
 | 
					Copyright (c) 2012-2014 Microsoft Corporation
 | 
				
			||||||
 | 
					   
 | 
				
			||||||
 | 
					Module Name:
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					    SeqSort.java
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					Abstract:
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					Author:
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					    @author Christoph Wintersteiger (cwinter) 2012-03-15
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					Notes:
 | 
				
			||||||
 | 
					    
 | 
				
			||||||
 | 
					**/ 
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					package com.microsoft.z3;
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					/**
 | 
				
			||||||
 | 
					 * A Sequence sort
 | 
				
			||||||
 | 
					 **/
 | 
				
			||||||
 | 
					public class SeqSort extends Sort
 | 
				
			||||||
 | 
					{
 | 
				
			||||||
 | 
					    SeqSort(Context ctx, long obj)
 | 
				
			||||||
 | 
					    {
 | 
				
			||||||
 | 
					        super(ctx, obj);
 | 
				
			||||||
 | 
					    }
 | 
				
			||||||
 | 
					}
 | 
				
			||||||
		Loading…
	
	Add table
		Add a link
		
	
		Reference in a new issue