Commit Graph

68 Commits

Author SHA1 Message Date
Bruce Mitchener
6835522a7f z3++.h: No longer include unused sstream.
This makes some code using the C++ API have to include `<sstream>`
if they used the functionality but didn't include it themselves.
2022-08-05 09:41:49 +03:00
Nikolaj Bjorner
5b219aab76 add mutual recursive datatypes to c++ API #6179
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-20 20:32:00 -07:00
Nikolaj Bjorner
2e13c0bf41 add API and example for one dimensional algebraic datatype #6179 2022-07-20 19:43:18 -07:00
Nikolaj Bjorner
393c63fe0c fix #6114 2022-07-18 09:33:39 -07:00
Nuno Lopes
fcbbf7ba76 fix build warning+error in c++ example 2022-06-17 16:43:34 +01:00
Nikolaj Bjorner
eb8c8da8a7 ex handler
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-10-27 09:38:36 +02:00
Nikolaj Bjorner
7f41d6140f use some suggestions from #5615
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-10-22 12:39:55 -04:00
Nikolaj Bjorner
f05ac8a429 updated C++ API for escaped and unescaped strings #5615
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-10-21 14:52:59 -04:00
Nikolaj Bjorner
55285b2193 make it easier to iterate over arguments of an application
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-09-02 09:51:59 -07:00
Nikolaj Bjorner
eacef5f3f9 deal with warnings over unused variables and procedures
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-11-29 19:45:35 -08:00
Nuno Lopes
9c08b60b5a c++ example: call Z3_finalize_memory() so that the buildbot leak checker doesnt complain about reachable memory 2020-10-24 15:35:56 +01:00
Nikolaj Bjorner
773b27296f translate optimize from c++ API #2859
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-01-15 04:24:51 -08:00
Nikolaj Bjorner
31a6788859 comment
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-10-11 12:39:57 -07:00
Nikolaj Bjorner
a990e7f02e add visitor example, fix double conversion
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-10-11 12:37:26 -07:00
Bruce Mitchener
0edd587e5a Fix typos in examples. 2019-08-14 22:00:50 -07:00
Nikolaj Bjorner
25c93410b1 add #2298 to regression/example
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-05-29 07:24:42 -07:00
Nikolaj Bjorner
082a0f4df4 add get_lstring per #2286
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-05-22 18:32:57 +04:00
Nikolaj Bjorner
886c62ef41 add example from #2138
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-02-16 10:30:44 -08:00
Nikolaj Bjorner
51a0022450 add recfun to API
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-10-27 11:41:18 -05:00
Nikolaj Bjorner
694a6a26c9 bump version, add double access
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-10-19 20:20:08 -07:00
rainoftime
bb534f6103 Add example of using z3's model construction C++ API 2018-07-10 11:16:20 +08:00
Nikolaj Bjorner
46ea054784 merge get_value and get_ivalue that produced different results
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-07-02 03:55:40 -07:00
Nikolaj Bjorner
f525f43e43 merge
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-04-30 09:30:43 -07:00
Nikolaj Bjorner
3b78bdc8e5 shorthands in enode to access args and partents
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-04-06 14:01:09 -07:00
Nikolaj Bjorner
5ba939ad5e add tuple shortcut and example to C++ API
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-04-03 12:40:18 -07:00