mirror of
				https://github.com/Z3Prover/z3
				synced 2025-11-04 13:29:11 +00:00 
			
		
		
		
	Add missing mkLastIndexOf method and CharSort case to Java API (#8002)
* Initial plan * Add mkLastIndexOf method and CharSort support to Java API - Added mkLastIndexOf method to Context.java for extracting last index of sub-string - Added Z3_CHAR_SORT case to Sort.java's create() method switch statement - Added test file to verify both fixes work correctly Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Fix author field in test file Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Delete examples/java/TestJavaAPICompleteness.java --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
		
							parent
							
								
									4a8a2adbb1
								
							
						
					
					
						commit
						0ebc1070da
					
				
					 2 changed files with 11 additions and 0 deletions
				
			
		| 
						 | 
				
			
			@ -2226,6 +2226,15 @@ public class Context implements AutoCloseable {
 | 
			
		|||
        return (IntExpr)Expr.create(this, Native.mkSeqIndex(nCtx(), s.getNativeObject(), substr.getNativeObject(), offset.getNativeObject()));
 | 
			
		||||
    }
 | 
			
		||||
 | 
			
		||||
    /**
 | 
			
		||||
     * Extract the last index of sub-string.
 | 
			
		||||
     */
 | 
			
		||||
    public final <R extends Sort> IntExpr mkLastIndexOf(Expr<SeqSort<R>> s, Expr<SeqSort<R>> substr)
 | 
			
		||||
    {
 | 
			
		||||
        checkContextMatch(s, substr);
 | 
			
		||||
        return (IntExpr)Expr.create(this, Native.mkSeqLastIndex(nCtx(), s.getNativeObject(), substr.getNativeObject()));
 | 
			
		||||
    }
 | 
			
		||||
 | 
			
		||||
    /**
 | 
			
		||||
     * Replace the first occurrence of src by dst in s.
 | 
			
		||||
     */
 | 
			
		||||
| 
						 | 
				
			
			
 | 
			
		|||
| 
						 | 
				
			
			@ -144,6 +144,8 @@ public class Sort extends AST
 | 
			
		|||
            return new SeqSort<>(ctx, obj);
 | 
			
		||||
        case Z3_RE_SORT:
 | 
			
		||||
            return new ReSort<>(ctx, obj);
 | 
			
		||||
        case Z3_CHAR_SORT:
 | 
			
		||||
            return new CharSort(ctx, obj);
 | 
			
		||||
        default:
 | 
			
		||||
            throw new Z3Exception("Unknown sort kind");
 | 
			
		||||
        }
 | 
			
		||||
| 
						 | 
				
			
			
 | 
			
		|||
		Loading…
	
	Add table
		Add a link
		
	
		Reference in a new issue