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

18931 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
8c67c23883 update print to elide overly long sets of intervals 2023-04-17 16:14:33 -07:00
Nikolaj Bjorner
7f3b518a71 bug fixes to bounds propagation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-04-05 17:53:19 -07:00
Nikolaj Bjorner
00306731f6 cosmetic updates to bounds 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-04-05 16:40:18 -07:00
Nikolaj Bjorner
2f992a7c9f adjust bounds 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-04-04 09:28:44 -07:00
Nikolaj Bjorner
50630bf8f5 prep for bilinear adt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-04-03 10:22:57 -07:00
Jakob Rath
9e1afc5916 Remove repropagate_units as well 2023-04-03 17:12:15 +02:00
Jakob Rath
21d315ba58 Fix try_ugt_z as well 2023-04-03 16:27:09 +02:00
Jakob Rath
76c18ee6e3 Fix try_ugt_y 2023-04-03 16:18:01 +02:00
Jakob Rath
c3c9883b0a Remove repropagate 2023-04-03 15:50:47 +02:00
Nikolaj Bjorner
9d751576bc add utility to count clauses 2023-04-02 16:12:26 -07:00
Nikolaj Bjorner
3302ab9dc5 fix bug introduced in is_valid() 2023-04-02 16:12:11 -07:00
Nikolaj Bjorner
ae57475483 fix bug in conflict::is_valid exposed by testing unit propagation 2023-04-02 14:54:20 -07:00
Nikolaj Bjorner
dcc87a682c disable assertion notification during shutdown 2023-04-01 14:59:35 -07:00
Nikolaj Bjorner
7b60c37ad8 remaining issue fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-04-01 10:30:49 -07:00
Nikolaj Bjorner
63ebd4fcba another unsoundness bug 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-03-31 16:13:46 -07:00
Nikolaj Bjorner
5e0db02753 reset conflict after unsat core 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-03-30 17:27:55 -07:00
Nikolaj Bjorner
9614e428a6 wip: enabling reinit approach 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-03-30 08:41:22 -07:00
Nikolaj Bjorner
bee3320ff6 put reinit-stack code path under ENALBE_REINIT_STACK macro 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-03-29 13:03:00 -07:00
Nikolaj Bjorner
8cefa02b0d Merge branch 'polysat' of https://github.com/z3prover/z3 into polysat 2023-03-29 09:58:46 -07:00
Nikolaj Bjorner
c0f43b9206 expose watch/unwatch 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-03-29 09:58:44 -07:00
Jakob Rath
f9147a7dc0 remove old code/notes 2023-03-29 16:14:01 +02:00
Jakob Rath
5e16a17f90 alternative bor 2023-03-29 15:57:15 +02:00
Jakob Rath
0704f90e9f fix log in release mode 2023-03-29 15:56:50 +02:00
Jakob Rath
67a4480410 comments, minor 2023-03-29 15:53:22 +02:00
Jakob Rath
1f58a906ed no more unassigned constraints in value propagation 2023-03-29 15:49:31 +02:00
Jakob Rath
d7930b3997 Find more undetected bool/eval conflicts in viable::resolve_interval 2023-03-29 15:47:10 +02:00
Jakob Rath
810a68ace9 disable some debug output 2023-03-29 15:40:17 +02:00
Jakob Rath
64e452e086 Add some clause names 2023-03-29 15:30:05 +02:00
Jakob Rath
c516d6fe0c get_watch_level: prefer true literals at lower search index 2023-03-29 15:23:43 +02:00
Nikolaj Bjorner
2a11be5c39 reorder 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-03-28 16:27:08 -07:00
Nikolaj Bjorner
2a8c7a7cd7 build issue for linux/clang 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-03-28 16:02:09 -07:00
Nikolaj Bjorner
d0e016c35d elaborate on clause reinitialization code path 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-03-28 12:57:34 -07:00
Nikolaj Bjorner
67efd6531b add stubs for reinit_clauses 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-03-28 12:34:09 -07:00
Nikolaj Bjorner
a82408e89b add int-blast experiment 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-03-27 16:40:22 -07:00
Jakob Rath
3796770e46 Fix subsumption (need to check whether entry is valid) 2023-03-23 14:46:04 +01:00
Jakob Rath
4f7a25eb73 fix IF_LOGGING macro 2023-03-23 14:16:48 +01:00
Jakob Rath
73b97f3a32 unsat core validity check works only if m_conflict.m_dep.is_null() 2023-03-23 14:15:17 +01:00
Jakob Rath
df82d9b0f9 unsat core dbg 2023-03-23 13:53:13 +01:00
Jakob Rath
f364ba8c8a remove unused code 2023-03-23 13:40:19 +01:00
Jakob Rath
50814c952a nicer output 2023-03-23 13:39:01 +01:00
Jakob Rath
f0ac81a149 remove output (related bug has been fixed) 2023-03-23 09:53:47 +01:00
Jakob Rath
095dfb2115 minor, debug output 2023-03-23 09:49:00 +01:00
Jakob Rath
d2397deb8d propagate before push 2023-03-23 09:35:10 +01:00
Jakob Rath
51025a75b4 fix conflict reset condition 2023-03-23 09:29:59 +01:00
Jakob Rath
4e9db7c4d9 eval justifications are determined by chronological order 2023-03-23 09:25:46 +01:00
Jakob Rath
5b3f500900 Try to keep conflict alive for longer 2023-03-23 07:18:36 +01:00
Jakob Rath
e433951e27 Active lemmas need to be queued for repropagation after resetting conflict 2023-03-22 17:44:02 +01:00
Jakob Rath
2804453039 resolve_conflict should stop at base index 2023-03-22 12:43:39 +01:00
Nikolaj Bjorner
da782a9dc7 remove references to linear propagate 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-03-20 09:20:00 +01:00
Nikolaj Bjorner
3dbca1042c review comments 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-03-20 09:12:07 +01:00