mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 09:35:32 +00:00
Code Activity
20014 commits 24 branches 48 tags 158 MiB
Commit graph

20014 commits

This branch
This branch
All branches
Author SHA1 Message Date
Jakob Rath
ec4be975ee no need to handle both x=y and y=x 2023-07-20 14:54:21 +02:00
Jakob Rath
73757e3fa4 mk_extract 2023-07-19 19:37:21 +02:00
Jakob Rath
69e54b62c5 no need to store bit-width separately 2023-07-19 12:56:35 +02:00
Jakob Rath
114e7b73e5 move callback into member function 2023-07-19 12:51:35 +02:00
Jakob Rath
b67caf5fc3 fix get_name for variables 2023-07-19 12:40:18 +02:00
Jakob Rath
85d80a0ae1 track origin slice for concat nodes 2023-07-19 12:06:02 +02:00
Jakob Rath
af73f26941 slicing: track disequalities 2023-07-19 12:04:45 +02:00
Jakob Rath
970e68c70e slicing: use proper bv sorts for expressions 2023-07-19 08:58:34 +02:00
Nikolaj Bjorner
e8a38c5482 build fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-18 19:14:45 -07:00
Nikolaj Bjorner
3d8f75b3d8 enable on-clause with dependencies 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-18 16:59:02 -07:00
Jakob Rath
66f813154b basic slicing integration 2023-07-18 16:19:54 +02:00
Jakob Rath
28ed3bd7ab fix backtracking of m_needs_congruence 2023-07-18 16:00:26 +02:00
Jakob Rath
a96df2292e fix build 2023-07-18 15:13:53 +02:00
Jakob Rath
68b151b0d2 move some todos 2023-07-18 15:11:46 +02:00
Jakob Rath
4742985906 add proposed query interface 2023-07-18 15:07:53 +02:00
Jakob Rath
bac52313da move function impl 2023-07-18 14:53:20 +02:00
Jakob Rath
c124cbae97 Add virtual concat terms on demand during propagation 2023-07-18 14:48:32 +02:00
Jakob Rath
4049716946 explain conflict 2023-07-18 11:26:18 +02:00
Jakob Rath
5e5164ed2c add_value 2023-07-18 11:24:12 +02:00
Jakob Rath
0d80e47350 update deps handling (need to support pvars as well) 2023-07-18 11:22:02 +02:00
Nikolaj Bjorner
9db636c38b Merge branch 'master' of https://github.com/z3prover/z3 2023-07-17 11:00:11 -07:00
Nikolaj Bjorner
3e74989a9d fixup dependencies for trim' 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-17 11:00:02 -07:00
Lev Nachmanson
bfc37bd266 add to m_touched_rows only when bound 
propagation is required
 2023-07-17 08:00:01 -10:00
Jakob Rath
11d9e5c862 minor 2023-07-17 19:04:17 +02:00
Jakob Rath
d1cb02b735 use abstract sort also for value slices 2023-07-17 18:31:17 +02:00
Jakob Rath
a2fdb03625 propagate value when splitting a slice 2023-07-17 18:18:12 +02:00
Jakob Rath
490b77d8a1 mk_value_slice 2023-07-17 14:41:45 +02:00
Jakob Rath
30323a6ba1 update unit test 2023-07-17 14:41:45 +02:00
Jakob Rath
741e37c2d7 find is now get_root 2023-07-17 14:41:45 +02:00
Jakob Rath
b8d118a558 use enode* instead of custom slice index; extract explanations from egraph 2023-07-17 14:41:45 +02:00
Jakob Rath
82b1f9297b utils 2023-07-17 14:41:45 +02:00
Nuno Lopes
013d5dc4db remove garbage file 2023-07-17 08:45:18 +01:00
Lev Nachmanson
0a91465e13 comment out debug output 2023-07-16 18:40:53 -10:00
Nikolaj Bjorner
75a9038aa2 add missing dependencies in rup 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-16 16:54:26 -07:00
Lev Nachmanson
fd5902f76e relax an assertion in int_solver::patcher 2023-07-16 11:55:42 -10:00
Nikolaj Bjorner
305c1c1dc2 fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-15 17:52:33 -07:00
Nikolaj Bjorner
715081cbd1 Merge branch 'master' of https://github.com/z3prover/z3 2023-07-15 17:04:54 -07:00
Nikolaj Bjorner
30e8330907 fix #6813 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-15 17:03:44 -07:00
Nikolaj Bjorner
8a913981f6 fix #6813 - proofs terms are fragile with respect to simplificiation of not(not(e)). It would be better if proof terms didn't have to track this level of detail, but the legacy proof format assumes strictly checkable proofs. A patch is to fixup terms within the mk_transitivity constructor 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-15 17:03:04 -07:00
Lev Nachmanson
144c9a7b82 restore the change_rows population in lar_solver 2023-07-15 10:09:48 -07:00
Lev Nachmanson
401ec04ec3
code cleaning around m_touched_rows of lar_solver (#6814) 2023-07-14 20:19:13 -07:00
Nikolaj Bjorner
3849f665d6 #6523 2023-07-14 10:17:19 -07:00
Nikolaj Bjorner
a8da0a6851 #6696 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-13 21:48:46 -07:00
Nikolaj Bjorner
dda9242616 revert lt change 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-13 21:39:04 -07:00
Nikolaj Bjorner
b78c7887f6 updating release-readme 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-13 19:31:35 -07:00
Nikolaj Bjorner
3727f70363 fix #6742 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-13 19:22:31 -07:00
Nikolaj Bjorner
4a9c4ca2ce initialize poly solver in incremental mode 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-13 14:12:29 -07:00
Nikolaj Bjorner
d1482287d4 fix #6793, disable unbound_compressor when used in context of a moel converter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-13 14:03:40 -07:00
Nikolaj Bjorner
08599177d0 fix #6808 
remove bv_eq_axioms as an external option to toggle.
Diseqalities have to be enforced for extensionality.
There are no internal code paths where the option is set to false.
 2023-07-13 10:47:55 -07:00
Nikolaj Bjorner
d0d434e4f1 fix #6807 2023-07-13 10:23:28 -07:00