mirror of
				https://github.com/Z3Prover/z3
				synced 2025-11-04 13:29:11 +00:00 
			
		
		
		
	FPA API: Naming consistency
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
		
							parent
							
								
									3d91510565
								
							
						
					
					
						commit
						06051989be
					
				
					 2 changed files with 9 additions and 9 deletions
				
			
		| 
						 | 
				
			
			@ -3043,9 +3043,9 @@ public class Context extends IDisposable
 | 
			
		|||
     * @param s FloatingPoint sort.
 | 
			
		||||
     * @throws Z3Exception 
 | 
			
		||||
     **/            
 | 
			
		||||
    public FPNum mkFPNumeral(boolean sgn, int sig, int exp, FPSort s) throws Z3Exception
 | 
			
		||||
    public FPNum mkFPNumeral(boolean sgn, int exp, int sig, FPSort s) throws Z3Exception
 | 
			
		||||
    {
 | 
			
		||||
        return new FPNum(this, Native.mkFpaNumeralUintInt(nCtx(), sgn, sig, exp, s.getNativeObject()));    
 | 
			
		||||
        return new FPNum(this, Native.mkFpaNumeralIntUint(nCtx(), sgn, exp, sig, s.getNativeObject()));    
 | 
			
		||||
    }
 | 
			
		||||
 | 
			
		||||
    /**
 | 
			
		||||
| 
						 | 
				
			
			@ -3056,9 +3056,9 @@ public class Context extends IDisposable
 | 
			
		|||
     * @param s FloatingPoint sort.
 | 
			
		||||
     * @throws Z3Exception 
 | 
			
		||||
     **/
 | 
			
		||||
    public FPNum mkFPNumeral(boolean sgn, long sig, long exp, FPSort s) throws Z3Exception
 | 
			
		||||
    public FPNum mkFPNumeral(boolean sgn, long exp, long sig, FPSort s) throws Z3Exception
 | 
			
		||||
    {
 | 
			
		||||
        return new FPNum(this, Native.mkFpaNumeralUint64Int64(nCtx(), sgn, sig, exp, s.getNativeObject()));
 | 
			
		||||
        return new FPNum(this, Native.mkFpaNumeralInt64Uint64(nCtx(), sgn, exp, sig, s.getNativeObject()));
 | 
			
		||||
    }
 | 
			
		||||
 | 
			
		||||
    /**
 | 
			
		||||
| 
						 | 
				
			
			
 | 
			
		|||
		Loading…
	
	Add table
		Add a link
		
	
		Reference in a new issue