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

18822 commits

This branch
This branch
All branches
Author SHA1 Message Date
Jakob Rath
fa0a481fc8 Fix verbose logs 2022-12-22 19:25:31 +01:00
Jakob Rath
0cfc0af7ee no need to alloc sets 2022-12-22 18:55:18 +01:00
Jakob Rath
29a547e0b4 forbidden_intervals::match_max 2022-12-22 18:28:18 +01:00
Jakob Rath
8096e82101 remove unnecessary check 2022-12-22 18:22:10 +01:00
Jakob Rath
b42b027a40 Add stub for match_max 2022-12-22 17:47:33 +01:00
Jakob Rath
516eb55442 forbidden_intervals::match_non_max 2022-12-22 17:39:16 +01:00
Jakob Rath
3739372776 remove commented code 2022-12-22 17:38:17 +01:00
Jakob Rath
9207bb5d1e Add test 2022-12-22 16:37:32 +01:00
Jakob Rath
e57bcdfeab Strengthen forbidden_intervals::match_non_zero 2022-12-22 16:30:23 +01:00
Jakob Rath
21ea05b31c Weaken evaluation for new constraints in viable lemma 2022-12-22 16:24:27 +01:00
Jakob Rath
be20c0d54e Less allocation during lookup, remove unused argument 2022-12-22 15:09:18 +01:00
Jakob Rath
b5af2164f4 Add simplify_clause::try_remove_equations 2022-12-22 14:53:42 +01:00
Jakob Rath
5bd63ab7c5 simplify note, and no need to be exclusive 2022-12-22 13:09:12 +01:00
Jakob Rath
5f2fd039ba Perform clause simplification earlier 2022-12-22 13:07:38 +01:00
Jakob Rath
44f0f88172 test 2022-12-21 16:23:05 +01:00
Jakob Rath
d51031f19b debug 2022-12-21 16:05:27 +01:00
Clemens Eisenhofer
c8b9127028 Added justifications for intermediate values [e.g., 2 * x in the pdd (2 * x) + y] 
This might allow propagation in both directions
 2022-12-21 13:52:27 +01:00
Jakob Rath
ec158845fc Add test for sat branch 2022-12-21 12:24:49 +01:00
Jakob Rath
109ab0be40 Detect more equations in refine_equal_lin 2022-12-21 12:21:22 +01:00
Jakob Rath
8da9850d45 Add rational::pseudo_inverse 2022-12-21 12:13:05 +01:00
Jakob Rath
4a1781d747 more viable refinement tests 2022-12-21 11:18:27 +01:00
Nikolaj Bjorner
0a75585073 revamp parity propagation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-20 17:45:33 -08:00
Nikolaj Bjorner
ca855fbad3 redoing parity lemmas 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-20 15:46:25 -08:00
Nikolaj Bjorner
a8d401864b review 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-20 12:46:15 -08:00
Jakob Rath
5c54ea87f1 Add unit test based on bench27 2022-12-20 09:40:15 +01:00
Jakob Rath
e5b142b265 Rotate first entry for refinement 2022-12-20 09:32:27 +01:00
Nikolaj Bjorner
fe8034731d fix #6501 2022-12-19 21:02:55 -08:00
Nikolaj Bjorner
f961300036 Merge branch 'master' of https://github.com/z3prover/z3 2022-12-19 12:40:51 -08:00
Nikolaj Bjorner
603597a22e deal with cancellation in qe for #6500 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-19 12:40:39 -08:00
Jakob Rath
86a36a524a Fix unsoundness in viable fallback 
(the src constraint of forbidden intervals is not necessarily univariate)
 2022-12-19 15:37:49 +01:00
Jakob Rath
868a3710e0 fix segfault 2022-12-19 14:25:58 +01:00
Jakob Rath
59592754d8 minor univariate tweak 2022-12-19 14:07:57 +01:00
Jakob Rath
ac0e9ebe5f Don't lose variables when aborting decisions 2022-12-19 14:02:47 +01:00
Jakob Rath
69b41a7e70 Check invariant on pvars 2022-12-19 13:55:50 +01:00
Clemens Eisenhofer
ec06027515 First step towards explaining single bits 2022-12-19 12:27:37 +01:00
Jakob Rath
208f166934 Merge remote-tracking branch 'origin/polysat' into polysat 2022-12-19 09:11:18 +01:00
Nikolaj Bjorner
30bbb5399f add stub 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-18 22:02:42 -08:00
Nikolaj Bjorner
1c884c8d72 allow multiple lemmas during processing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-18 19:03:28 -08:00
Nikolaj Bjorner
1940f53b31 fix memory smash in cache push 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-18 12:33:58 -08:00
Nikolaj Bjorner
8c775f55a1 adding stub for non-overflow lemma (disabled as not seen to be of use) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-18 12:26:30 -08:00
Nikolaj Bjorner
899b1f8f7e fiddle with univariate 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-17 20:02:46 -08:00
Nikolaj Bjorner
4e8bd4425f add find_two 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-17 19:41:09 -08:00
Nikolaj Bjorner
3c035daaa6 fix missing parity propagation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-17 19:08:40 -08:00
Nikolaj Bjorner
b581cbf062 add lemmas 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-17 18:25:21 -08:00
Jakob Rath
bf92fa4882 clause_iterator 2022-12-16 15:21:32 +01:00
Jakob Rath
342774eff8 test_ineq_non_axiom4 is slow but doesn't block anymore 2022-12-16 15:02:04 +01:00
Jakob Rath
75a64975b5 test 2022-12-16 15:00:50 +01:00
Jakob Rath
3e6e1e1a8a test 2022-12-16 14:37:31 +01:00
Jakob Rath
ca373836af Merge remote-tracking branch 'origin/polysat' into polysat 2022-12-16 14:26:38 +01:00
Jakob Rath
3b3636b30e Remove conflict::set 2022-12-16 14:25:41 +01:00