mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-15 17:06:39 +00:00
Code Activity
16920 commits 43 branches 51 tags 169 MiB
Commit graph

3966 commits

Author SHA1 Message Date
Nikolaj Bjorner
0059e88036 fix #5808 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-07 20:10:32 +02:00
Nikolaj Bjorner
9958cab5cc fix #5808 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-07 07:43:30 +02:00
Nikolaj Bjorner
3f3d058567 extract also units from search state 2022-02-07 06:16:22 +02:00
Nikolaj Bjorner
9d655cc658 track all unhandled operators instead of latest 2022-02-04 22:07:29 -08:00
Nikolaj Bjorner
474949542e Merge branch 'master' of https://github.com/z3prover/z3 2022-02-04 13:08:59 -08:00
Nikolaj Bjorner
05e28e4344 fix #5812 2022-02-04 13:08:52 -08:00
Nikolaj Bjorner
a326ad4cd9 flag incomplete on lambdas #5803 2022-01-31 11:54:06 -08:00
Nikolaj Bjorner
c6539deb61 fixing null check 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-25 17:25:42 +01:00
Nikolaj Bjorner
435f79eab0 tup 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-25 16:40:55 +01:00
Nikolaj Bjorner
9294b2ceb2 created 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-25 16:33:23 +01:00
Nikolaj Bjorner
3de9d37772 fix overrides for created_eh 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-25 16:24:08 +01:00
Nikolaj Bjorner
bf6454dccc throw error if created-eh has not been registered 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-25 13:01:57 +01:00
Nikolaj Bjorner
ea6827505e add missing callback to m_created_eh 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-25 10:13:09 +01:00
Nikolaj Bjorner
a1f7676c81 remove assertion - literals could be assigned but propagation incomplete 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-21 03:10:41 +01:00
Nikolaj Bjorner
17280846f8 added comments to explain #5781 2022-01-21 01:40:31 +01:00
Nikolaj Bjorner
af9ae35984 term 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-20 14:43:16 +01:00
Nikolaj Bjorner
c527fda0b6 term 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-20 14:41:27 +01:00
Nikolaj Bjorner
f1a302bba7 term 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-20 14:38:34 +01:00
Nikolaj Bjorner
7a8c969033 ensure b_internalized 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-20 13:27:23 +01:00
Nikolaj Bjorner
c00591daaf finish is-fixed 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-19 16:28:34 +01:00
Nikolaj Bjorner
e5767bf2b8 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-19 15:19:07 +01:00
Nikolaj Bjorner
0f03ef4ab0 for Clemens: ensure fixed values are propagated after registration 
Also allow to register expressions that the rewriter changes to ensure they get picked up.
 2022-01-19 14:38:11 +01:00
Nikolaj Bjorner
d09abdf58e fix #5771 
Missing congruence closure enforcement on auxiliary guard predicates.
It diverges but is sound.
 2022-01-14 15:46:40 -08:00
Nikolaj Bjorner
56d3718cde add simplification with qe-lite as an option #5767 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-12 03:41:21 -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
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
592b1d7f65 #5752 2022-01-06 13:32:50 -08:00
Nikolaj Bjorner
d7c7fbb8f1 setting roots breaks relevancy propagation 2022-01-05 21:16:25 -08:00
Nikolaj Bjorner
9d3c8a6a2f na 2022-01-01 17:59:31 -08:00
Nikolaj Bjorner
fc77345bec breaking change. Enforce append semantics everywhere for parameter updates #5744 
Replace semantics doesn't work with assumptions made elsewhere in code.
The remedy is to apply append (override) semantics for parameter changes.
 2021-12-30 19:11:14 -08:00
Nikolaj Bjorner
d88f125818 build 2021-12-26 15:24:03 -08:00
Nikolaj Bjorner
09ee60ccce update comment 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-21 11:04:07 -08:00
Nikolaj Bjorner
4b813bac1c na 2021-12-19 12:31:47 -08:00
Nikolaj Bjorner
f0740bdf60 move user propagte declare to context level 
declaration of user propagate functions are declared at context level instead of at solver scope.
 2021-12-18 10:56:42 -08:00
Nikolaj Bjorner
4856581b68 na 2021-12-17 16:40:19 -08:00
Nikolaj Bjorner
8ca023d541 expose propagate created 2021-12-17 16:12:47 -08:00
Nikolaj Bjorner
9c8800bdde adding a new toy for Clemens 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-17 10:45:59 -08:00
Nikolaj Bjorner
6cc9aa3562 prepare user propagator declared functions for likely Clemens use case 2021-12-16 19:37:30 -08:00
Nikolaj Bjorner
dd6a11b526 fix #5715 2021-12-16 09:35:54 -08:00
Nikolaj Bjorner
3b58f548f7 remove dead code 2021-12-14 13:42:52 -08:00
Nikolaj Bjorner
b1d167de5b fix co-factoring' 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-14 10:12:38 -08:00
Nikolaj Bjorner
5348af3c4c fix co-factoring 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-14 10:05:09 -08:00
Nikolaj Bjorner
f40becf099 remove case for non-emptiness to combine with standard membership 
as part of revising engine for addressing #5693
 2021-12-13 18:17:40 -08:00
Nikolaj Bjorner
b2af7ea68f stdout 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-13 15:19:29 -08:00
Nikolaj Bjorner
9ec0f94ab9 hoisting out blocker for empty 
#5693
 2021-12-13 14:25:05 -08:00
Nikolaj Bjorner
9f2b18cac5 add tactic name 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-07 13:37:57 -08:00
Nikolaj Bjorner
1e95fb44d1 add ability to register expressions during callback 2021-12-07 09:47:05 -08:00
Nikolaj Bjorner
658a334ecf clear tactic user propagate state on solver destructor 2021-12-07 03:14:50 -08:00