mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity
16340 commits 23 branches 48 tags 157 MiB
Commit graph

1636 commits

Author SHA1 Message Date
Nikolaj Bjorner
b82c3cfd33 remove deprecated comment 2021-11-24 11:26:13 +01:00
Nikolaj Bjorner
21c604e7b4 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-23 18:56:32 +01:00
Nikolaj Bjorner
73ffd1c1cb na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-22 18:18:01 +01:00
Nikolaj Bjorner
8db711bc3c retire deprecated functionality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-22 18:14:15 +01:00
Nikolaj Bjorner
8ec5ccbb9a roll in new-viable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-22 06:17:20 +01:00
Nikolaj Bjorner
d86570ce75 prepare for new viable 2021-11-21 06:18:35 +01:00
Nikolaj Bjorner
b0bf03457c conflict 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-19 08:23:50 -08:00
Nikolaj Bjorner
caaefef847 remove add_non_viable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-18 15:57:55 -08:00
Nikolaj Bjorner
6bf4f001d9 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-18 15:53:51 -08:00
Nikolaj Bjorner
1dcb7e6f6a remove justified vars 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-18 15:43:39 -08:00
Nikolaj Bjorner
de424713e4 if you are really reading this commit message, you must be a programmer who has no life. 2021-11-18 10:10:50 -08:00
Nikolaj Bjorner
a5fdf6ba8a Update viable2.cpp 2021-11-16 09:54:06 -08:00
Nikolaj Bjorner
69a17d0c60 test and fix viable2 2021-11-14 20:55:12 -08:00
Nikolaj Bjorner
4261345503 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-13 17:43:07 -08:00
Nikolaj Bjorner
d073583d88 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-13 06:50:11 -08:00
Nikolaj Bjorner
5708de4301 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-12 11:20:35 -08:00
Nikolaj Bjorner
c9f5ce43b2 viable 2 with dlist 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-10 14:43:10 -08:00
Nikolaj Bjorner
0bec8520e1 adding new viable using forbidden intervals 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-10 08:23:45 -08:00
Nikolaj Bjorner
733f44d141 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-10 03:03:23 -08:00
Nikolaj Bjorner
931e1624b2 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-10 02:58:35 -08:00
Nikolaj Bjorner
c1d58088be na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-10 01:42:04 -08:00
Nikolaj Bjorner
d0b47d23f6 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-10 00:43:57 -08:00
Nikolaj Bjorner
d0c8240560 refactor forbidden intervals 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-09 10:34:11 -08:00
Nikolaj Bjorner
57c40e480b na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-08 05:08:57 -08:00
Nikolaj Bjorner
e1bc9cc0bb updates 2021-11-05 12:16:35 -07:00
Nikolaj Bjorner
eaa6340a0c Merge branch 'polysat' of https://github.com/z3prover/z3 into polysat 2021-11-03 15:06:53 -07:00
Nikolaj Bjorner
7b845c7138 build warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-02 19:26:48 -07:00
Nikolaj Bjorner
6fb4e0d5a9 fix unsound backjump for out of order search stacks 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-02 19:12:49 -07:00
Nikolaj Bjorner
48e663776b build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-02 15:40:45 -07:00
Nikolaj Bjorner
87d4ce2659 working on #5614 
there are some different sources for the performance regression illustrated by the example. The mitigations will be enabled separately:
- m_bv_to_propagate is too expensive
- lp_bound_propagator misses equalities in two different ways:
   - it resets row checks after backtracking even though they could still propagate
   - it misses equalities for fixed rows when the fixed constant value does not correspond to a fixed variable.

FYI @levnach
 2021-11-02 14:55:39 -07:00
Nikolaj Bjorner
3f3bd5948f fixes/debugging 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-02 14:48:19 -07: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
3036b88f09 support threading for TRACE mode 2021-10-25 13:35:32 +02:00
Nikolaj Bjorner
4c81f8676c backtrack 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-10-10 18:23:25 -07:00
Nikolaj Bjorner
5ee5197ea9 Merge branch 'polysat' of https://github.com/z3prover/z3 into polysat 2021-10-06 13:01:29 -07:00
Nikolaj Bjorner
a50cecaefa wip 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-10-05 16:06:31 -07:00
Nikolaj Bjorner
be4bc6caed merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-10-04 17:37:12 -07:00
Nikolaj Bjorner
0d9d4bb46e wip 2021-10-04 14:44:05 -07:00
Nikolaj Bjorner
813674087e wip 2021-10-04 14:43:33 -07:00
Nikolaj Bjorner
fd8b2ba596 clear regressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-29 15:56:01 -07:00
Nikolaj Bjorner
e1224e116f na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-28 16:45:03 -07:00
Nikolaj Bjorner
f3328c743e na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-28 16:43:55 -07:00
Nikolaj Bjorner
e1edadabec na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-27 17:06:59 -07:00
Nikolaj Bjorner
95e2d174c7 fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-25 17:26:18 -07:00
Nikolaj Bjorner
a574eebd05 fixes, tests 2021-09-25 08:38:48 -07:00
Nikolaj Bjorner
e6c413b249 add variable minimization 2021-09-22 14:27:05 -07:00
Nikolaj Bjorner
c82bbaad7d update todos, working on assignment minimization 2021-09-22 13:29:36 -07:00
Nikolaj Bjorner
3447d80310 fix todo on enforcing premises 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-22 12:26:45 -07:00
Nikolaj Bjorner
e5df395380 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-22 08:44:37 -07:00
Nikolaj Bjorner
0013ae5089 elim pointer 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-22 08:15:32 -07:00