mirror of
				https://github.com/Z3Prover/z3
				synced 2025-11-04 13:29:11 +00:00 
			
		
		
		
	add to release notes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
		
							parent
							
								
									115187ee2b
								
							
						
					
					
						commit
						773f90f122
					
				
					 1 changed files with 8 additions and 0 deletions
				
			
		| 
						 | 
					@ -7,6 +7,14 @@ Version 4.4.1
 | 
				
			||||||
 | 
					
 | 
				
			||||||
- A multitude of bugs has been fixed.
 | 
					- A multitude of bugs has been fixed.
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					- New Feature: Support for optimization queries. The SMT-LIB2 command language
 | 
				
			||||||
 | 
					  is augmented by three commands (maximize <expr>), (minimize <expr) 
 | 
				
			||||||
 | 
					  and (assert-soft <expr> [:weight <numeral>] [:id <identifier>]). 
 | 
				
			||||||
 | 
					  The programmatic API also contains a dedicated context for solving 
 | 
				
			||||||
 | 
					  optimization queries. The TACAS 2015 tool paper by Bjorner, Dung and 
 | 
				
			||||||
 | 
					  Fleckenstein describes additional details and the online tutorial on 
 | 
				
			||||||
 | 
					  http://rise4fun.com/z3opt illustrates some uses.
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					
 | 
				
			||||||
Version 4.4.0
 | 
					Version 4.4.0
 | 
				
			||||||
=============
 | 
					=============
 | 
				
			||||||
| 
						 | 
					
 | 
				
			||||||
		Loading…
	
	Add table
		Add a link
		
	
		Reference in a new issue