mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-18 22:59:02 +00:00
Code Activity
16868 commits 23 branches 48 tags 157 MiB
Commit graph

782 commits

Author SHA1 Message Date
Bruce Mitchener 5014b1a34d Use = default for virtual constructors. 2022-08-05 18:11:46 +03:00
Bruce Mitchener 1d9345c3de Fix typos. 2022-08-05 07:40:50 +03:00
Bruce Mitchener 5d0dea05aa
Remove empty leaf destructors. (#6211) 2022-07-30 10:07:03 +01:00
Nikolaj Bjorner ac822acb0f add parameter incremental to ensure preprocessing does not interefere with adding constraints during search 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-07-05 08:10:20 -07:00
Nikolaj Bjorner 94a2477fa0 totalizer 2022-06-30 19:49:19 -07:00
Nikolaj Bjorner c3d2120bdd add totalizer version of rc2 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-06-29 23:10:42 -07:00
Nikolaj Bjorner 5afcb489e0 adding totalizer 2022-06-29 08:20:01 -07:00
Nikolaj Bjorner 61f5489223 fix #6107 2022-06-27 16:53:18 -07:00
Nikolaj Bjorner 911134b3c7 add new heuristic rc2bin (to be tested) to maxsat 
The rc2bin heuristic is a hybrid of rc2 and binary maxres.
It follows the suggestion by Nina to use rc2 on large cores after a single maxres relaxation step; otherwise maxres (binary) on smaller cores. In the design space of possible hybrids, this variant chooses to always apply a single layer of maxres and then rc2 for large cores.
 2022-06-20 11:50:25 -07:00
Nuno Lopes 73a24ca0a9 remove '#include <iostream>' from headers and from unneeded places 
It's harmful to have iostream everywhere as it injects functions in the compiled files
 2022-06-17 14:10:19 +01:00
Christoph M. Wintersteiger ed7db892f9
Fix a couple compiler warnings 2022-06-04 08:00:56 +01:00
Nikolaj Bjorner b8532bec7e remove pragma from cpp file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-28 14:48:38 -07:00
Nikolaj Bjorner c850259f89 rw 2022-05-22 07:54:27 -04:00
Nikolaj Bjorner 386c511f54 core opt 2022-05-21 10:27:37 -04:00
Nikolaj Bjorner 1e7a9e3e61 fix #6023 2022-05-08 12:03:13 -07:00
Nikolaj Bjorner be653dab0e init value 2022-05-01 15:26:57 -07:00
Nikolaj Bjorner d1f1e4ce34 selectively enable dual strengthening 2022-05-01 15:26:57 -07:00
Nikolaj Bjorner 98e1c86128 na 2022-05-01 15:26:57 -07:00
Nikolaj Bjorner 9cc5f6901a na 2022-05-01 15:26:57 -07:00
Nikolaj Bjorner b5c7f000de add option to "rotate" cores during core finding 
enable to find multiple cores in a round and at the same time facilitate rotation around satisfiable subsets to explore neighborhoods for improved assignments.
 2022-05-01 15:26:56 -07:00
Nikolaj Bjorner 0dd0fd26d4 remove buggy prototype 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-04-21 10:44:49 +01:00
Nikolaj Bjorner d9f3625f93 change default output to print objective value 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-04-20 17:11:46 +01:00
Nikolaj Bjorner ec57d3b15c missing switch cases 2022-04-19 16:20:02 +01:00
Nikolaj Bjorner df981666fd na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-04-18 16:27:46 +02:00
Nikolaj Bjorner c727e2d048 add rc2 option 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-04-18 10:31:56 +02:00
Nikolaj Bjorner 4a59ae41b3 fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-04-16 19:19:05 +02:00
Nikolaj Bjorner 7496f11542 na 2022-04-16 18:30:35 +02:00
Nikolaj Bjorner b5309d5fd0 na 2022-04-16 16:42:57 +02:00
Nikolaj Bjorner c131eb4db1 build fix 2022-04-16 16:42:45 +02:00
Nikolaj Bjorner f4c500c519 fix build 
reference types are not part of C
 2022-04-16 15:16:53 +02:00
Nikolaj Bjorner 807121aa03 wip 2022-04-16 14:55:43 +02:00
Nikolaj Bjorner 3cc9d7f443 improve pre-processing 2022-04-15 12:55:26 +02:00
Nikolaj Bjorner 3f5eb7fcf2 re-enable pre-process 2022-04-13 11:24:24 +02:00
Nikolaj Bjorner ac55e29a56 disable propagation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-04-11 22:23:42 +02:00
Nikolaj Bjorner c996a66da0 separate pre-processing, add callback parameter to push/pop in python API 2022-04-11 17:05:59 +02:00
Nikolaj Bjorner 405a26c585 allow adding constraints during on_model 2022-04-09 09:55:02 +02:00
Nikolaj Bjorner d6d9b25c68 Allow adding constraints in the model_eh callback 2022-04-08 17:12:20 +02:00
Nikolaj Bjorner 994c7ef52d format 2022-01-31 12:00:26 -08:00
Nikolaj Bjorner 7baa4f88b0 build failure 2022-01-06 15:17:57 -08:00
Nikolaj Bjorner 6a3fe514f0 build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-06 14:07:54 -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 122b0fec0f fix #5710 2021-12-16 12:30:29 -08:00
Nikolaj Bjorner b6f7deacf4 fix #5663 2021-11-12 11:36:42 -08:00
Henrich Lauko 96671cfc73
Add and fix a few general compiler warnings. (#5628) 
* rewriter: fix unused variable warnings

* cmake: make missing non-virtual dtors error

* treewide: add missing virtual destructors

* cmake: add a few more checks

* api: add missing virtual destructor to user_propagator_base

* examples: compile cpp example with compiler warnings

* model: fix unused variable warnings

* rewriter: fix logical-op-parentheses warnings

* sat: fix unused variable warnings

* smt: fix unused variable warnings
 2021-10-29 15:42:32 +02:00
Nikolaj Bjorner 6eed885379 print bounded terms for better efficiency 2021-10-21 10:42:39 -04:00
Nikolaj Bjorner f9dde2e8a4 #5605 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-10-19 12:21:54 -04:00
Nikolaj Bjorner fd77f0c111 fix #5594 2021-10-13 17:17:05 -07:00
Nikolaj Bjorner b1bc890992 fix #5515 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-28 18:05:51 -07:00