| 
								
								
									 Nikolaj Bjorner | 3f8083dfa6 | fix push/pop bugs in optimize context, add example to c++, fix bug in arithemtic bounds axiom addition Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> | 2014-09-02 09:32:38 -07:00 |  | 
				
					
						| 
								
								
									 Nikolaj Bjorner | d118f07e37 | fix maximize name in C++ API Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> | 2014-04-22 14:48:05 +02:00 |  | 
				
					
						| 
								
								
									 Leonardo de Moura | edb2f8554d | Add new example Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> | 2013-05-27 17:45:56 -07:00 |  | 
				
					
						| 
								
								
									 Leonardo de Moura | c8c5f30b49 | Add new C++ APIs for creating forall/exists expressions. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> | 2013-05-09 21:30:31 -07:00 |  | 
				
					
						| 
								
								
									 Leonardo de Moura | 157b5f0d9c | Add expr_vector example Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> | 2013-05-07 08:10:43 -07:00 |  | 
				
					
						| 
								
								
									 Leonardo de Moura | b2810592e6 | Add enumeration_sort method to C++ API. Add as_expr method to goal class in C++ API. Add enum_sort_example to C++ examples/c++/example.cpp Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> | 2013-02-26 08:29:01 -08:00 |  | 
				
					
						| 
								
								
									 Leonardo de Moura | c430fe26aa | Add ite operator to the C++ API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> | 2013-01-04 08:29:25 -08:00 |  | 
				
					
						| 
								
								
									 Leonardo de Moura | 7b1fac11e6 | Add new C++ examples Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> | 2012-12-19 12:33:14 -08:00 |  | 
				
					
						| 
								
								
									 Leonardo de Moura | 0ec6e2f218 | adjusting examples Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> | 2012-12-03 15:19:47 -08:00 |  | 
				
					
						| 
								
								
									 Leonardo de Moura | caced62f40 | New API for adding 'tracked assertions'. Added wrappers for creating existential and universal quantifiers in the C++ API fronted. Added new examples for the C++ API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> | 2012-11-10 15:54:31 -08:00 |  | 
				
					
						| 
								
								
									 Leonardo de Moura | a5ceff98ea | cleaned exampled Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> | 2012-11-08 07:11:22 -08:00 |  | 
				
					
						| 
								
								
									 Leonardo de Moura | 1cf8d61def | new example Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> | 2012-11-08 07:00:27 -08:00 |  | 
				
					
						| 
								
								
									 Leonardo de Moura | e08c569d8d | new qe example Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> | 2012-11-02 12:04:02 -07:00 |  | 
				
					
						| 
								
								
									 Leonardo de Moura | be97785253 | c++ example Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> | 2012-10-28 10:06:02 -07:00 |  | 
				
					
						| 
								
								
									 Leonardo de Moura | e2f4943b4e | moved dll and examples Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> | 2012-10-23 16:33:20 -07:00 |  |