Nikolaj Bjorner
|
0482e7fe72
|
cache datatype util in context to avoid performance bug, codeplex issue 195
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
|
2015-03-25 11:46:28 -07:00 |
|
Nikolaj Bjorner
|
39892aae10
|
cache datatype util in context to avoid performance bug, codeplex issue 195
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
|
2015-03-25 11:46:17 -07:00 |
|
Nikolaj Bjorner
|
8059a5a0b7
|
cache datatype util in context to avoid performance bug, codeplex issue 195
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
|
2015-03-25 11:36:01 -07:00 |
|
Nikolaj Bjorner
|
86ac20faf6
|
cache datatype util in context to avoid performance bug, codeplex issue 195
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
|
2015-03-25 11:35:44 -07:00 |
|
Nikolaj Bjorner
|
2aa91eee70
|
cache datatype util in context to avoid performance bug, codeplex issue 195
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
|
2015-03-25 11:24:47 -07:00 |
|
nikolajbjorner
|
3ca3c948cf
|
add bit-vector extract shortcuts to C++ API
Signed-off-by: nikolajbjorner <nbjorner@microsoft.com>
|
2015-02-27 11:08:49 -08:00 |
|
Nikolaj Bjorner
|
b4600ffda0
|
add print to SMT-LIB format from solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2014-10-31 14:24:21 +01:00 |
|
Nikolaj Bjorner
|
7ef1e8a3de
|
turn friends into inliers to respect namespace for non-operator friends. Operaor friends will stil be in file scope so do not take name-space qualifier
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2014-10-05 19:04:15 -07: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 |
|