3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 01:54:08 +00:00
Commit graph

16090 commits

Author SHA1 Message Date
Nikolaj Bjorner 08294d62e5 separate dependencies for qe_lite 2022-01-12 03:26:22 -08:00
Nikolaj Bjorner 2bcc814031 add macro to track closures declared in z3_api
This is to ease integration with external API wrappers that rely on accessing
information about type names that are used.
#5762
2022-01-12 02:47:39 -08:00
Nikolaj Bjorner e5eaea46aa ensure m_true is assigned #5753 2022-01-11 10:42:05 -08:00
Nikolaj Bjorner dbd5512d8c ensure enode without recursion
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-01-11 08:35:57 -08:00
Nikolaj Bjorner 055732423c ensure enode without recursion
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-01-11 08:35:25 -08:00
Nikolaj Bjorner 571a74c061 counting function applications #5766
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-01-10 14:51:25 -08:00
Nikolaj Bjorner 4cd818b578 #5766 2022-01-10 14:40:27 -08:00
Nikolaj Bjorner d3bc11dd3a bvs have to be expressions
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-01-10 12:38:25 -08:00
Nikolaj Bjorner 21feefeac5 Add character access functions #5764 2022-01-10 12:33:58 -08:00
Kevin Gibbons 2b934b601d
Add WebAssembly/TypeScript bindings (#5762)
* Add TypeScript bindings

* mark Z3_eval_smtlib2_string as async
2022-01-09 17:16:38 -08:00
Nikolaj Bjorner 9ac57fc510 update version number for next release
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-01-09 17:11:08 -08:00
Nikolaj Bjorner f1bf660adc add case for abs (normally simplified, but not with default_tactic=smt). 2022-01-09 11:55:21 -08:00
Nikolaj Bjorner 671d071e54 #5753 2022-01-09 11:39:21 -08:00
Nikolaj Bjorner 010bccf353
Update wasm.yml
add some more limited retention
2022-01-09 11:35:50 -08:00
Nikolaj Bjorner bf3c213fd3 #5753 2022-01-09 11:03:29 -08:00
Nikolaj Bjorner 90fd3d82fc enable propagation 2022-01-08 19:00:56 -08:00
Nadav Rotem 9f9543ef69
Fix unused variable warnings. (#5760)
This commit fixes a few cases of unused variables in release builds.
The commit uses the (void)xxx; syntax which is used in other parts of
the code.
2022-01-08 18:18:30 -08:00
Nikolaj Bjorner 174889ad5e id 2022-01-08 16:28:12 -08:00
Nikolaj Bjorner afbfea8ce6 name the package
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-01-08 15:52:50 -08:00
Nikolaj Bjorner 36ed1ffac2 update name of artifact
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-01-08 15:13:46 -08:00
Nikolaj Bjorner 40761ebb0d bug in script
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-01-08 12:10:16 -08:00
Nikolaj Bjorner c2aff52dd7 os-info back to common 2022-01-08 11:33:43 -08:00
Nikolaj Bjorner d391043ffd only one arch at a time 2022-01-08 11:32:08 -08:00
Nikolaj Bjorner ef481073b2 make static features avoid stack #5758 2022-01-08 11:20:18 -08:00
Nikolaj Bjorner 2c44454a17 self -> env 2022-01-08 10:58:36 -08:00
Nikolaj Bjorner d6ce05009b try separate x86
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-01-08 10:14:28 -08:00
Nikolaj Bjorner 6013d5da47 #5755
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-01-07 14:05:06 -08:00
Nikolaj Bjorner 0bc8518cb5 na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-01-07 11:53:27 -08:00
Nikolaj Bjorner 199daead50 remove Z3_bool_opt #5757
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-01-07 11:52:10 -08:00
Nikolaj Bjorner 7baa4f88b0 build failure 2022-01-06 15:17:57 -08:00
Nikolaj Bjorner 2be71cfc43 #5753 2022-01-06 15:17:37 -08:00
Nikolaj Bjorner 6a3fe514f0 build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-01-06 14:07:54 -08:00
Nikolaj Bjorner 592b1d7f65 #5752 2022-01-06 13:32:50 -08:00
Nikolaj Bjorner d14f00d61a with no last model
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-01-06 13:02:13 -08:00
Nikolaj Bjorner dadda86bdc #5751 2022-01-06 11:43:17 -08:00
Nikolaj Bjorner 130a0c4aa0 resurrect infinitesimals from maximization function #5720
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-01-06 08:34:45 -08:00
Nikolaj Bjorner d7c7fbb8f1 setting roots breaks relevancy propagation 2022-01-05 21:16:25 -08:00
Nikolaj Bjorner bd8de964f7 more fixes on relevancy 2022-01-04 22:02:28 -08:00
Nikolaj Bjorner 5ec7a66a45 change class name, add comment 2022-01-04 22:02:14 -08:00
Nikolaj Bjorner 964a5cd761 lump java together
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-01-04 20:48:05 -08:00
Nikolaj Bjorner e943bee625 apply delcypher's todo
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-01-04 20:25:14 -08:00
Nikolaj Bjorner ef3dd32364 some cleanup
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-01-04 20:21:53 -08:00
Nikolaj Bjorner d1fb831030 relevancy overhaul 2022-01-04 16:03:31 -08:00
Nikolaj Bjorner 4a1975053f cleanup 2022-01-03 17:37:04 -08:00
Nikolaj Bjorner 614c66f1e2 missing relevancy propagation 2022-01-03 17:21:37 -08:00
Nikolaj Bjorner fc741cf018 rename module
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-01-03 14:23:22 -08:00
Nikolaj Bjorner a086f6218b na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-01-03 14:15:41 -08:00
Nikolaj Bjorner a2a5924e5c purge more 2022-01-03 14:14:09 -08:00
Nikolaj Bjorner 8e3185ffe3 remove dual solver approach
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-01-03 14:08:01 -08:00
Nikolaj Bjorner 1f964eea90 na 2022-01-03 11:12:28 -08:00