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

17920 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
5b2519d7a3 #6523 
attach original variable to pb expression.
 2023-08-01 08:41:26 -07:00
Nikolaj Bjorner
adad468cd7 allow copy within a user scope #6827 
this will allow copying the solver state within a scope.
The new solver state has its state at level 0. It is not possible to pop scopes from the new solver (you can still pop scopes from the original solver). The reason for this semantics is the relative difficulty of implementing (getting it right) of a state copy that preserves scopes.
 2023-07-31 19:46:08 -07:00
Nikolaj Bjorner
403340498c format 2023-07-31 19:41:11 -07:00
Nikolaj Bjorner
afe1218bc6 update release.yml with linux-arm64 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-31 10:46:16 -07:00
Nikolaj Bjorner
0606ca15d9 track lia conflicts as cuts 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-28 17:40:56 -07:00
Nikolaj Bjorner
de1cf30ea8 strengthen Tseitin checker to take true/false constants into account 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-28 16:54:33 -07:00
Nikolaj Bjorner
6c5434f988 rename artifacts apart 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-28 11:40:37 -07:00
Nikolaj Bjorner
1b2b8809c0 try to add Ubuntu ARM64 to nightly #6835 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-28 11:10:14 -07:00
Nikolaj Bjorner
7135283135 update format and checker for implied-eq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-27 13:23:17 -07:00
Nikolaj Bjorner
f0184c3fde update format and checker for implied-eq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-27 13:21:45 -07:00
Nikolaj Bjorner
249f0de80b fix order for inequalities in arithmetic justifications such that implied bound literal is last. The self-checker uses this property to identify the implied bound 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-26 10:06:41 -07:00
Nikolaj Bjorner
c6aab89662 add rewrite for partially interpreted arithmetic functions 2023-07-25 14:57:27 -07:00
Nikolaj Bjorner
0f2fe6031a patching up trim 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-25 11:32:20 -07:00
Nikolaj Bjorner
6da4f6815e Merge branch 'master' of https://github.com/z3prover/z3 2023-07-25 09:47:09 -07:00
Nikolaj Bjorner
423a7b6888 also add separate cut rule 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-25 09:46:59 -07:00
Nikolaj Bjorner
68a437e615 revert to logging conflict to get EUF trim to work 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-25 09:45:35 -07:00
Bruce Mitchener
8cc6969510
Remove Z3_literals remnants. (#6829) 
The bulk of the functionality using these was removed between
Z3 4.4.1 and 4.5.0, back in 2015.

Co-authored-by: Bruce Mitchener <bruce.mitchener@configura.com>
 2023-07-23 19:38:57 -07:00
Nikolaj Bjorner
6c8b8609ee tweak control flow for empty clauses 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-23 18:16:00 -07:00
Nikolaj Bjorner
48deb4d3e0 fix proof generation for euf-solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-23 14:31:44 -07:00
Nikolaj Bjorner
e64bab4bb8 simplify code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-22 13:19:03 -07:00
Nikolaj Bjorner
d0f2b00f96 fix build warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-22 12:24:30 -07:00
Nikolaj Bjorner
a0892c6669 rename antecedent utilities for clarity 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-22 11:30:34 -07:00
Nikolaj Bjorner
df8ccce08e #6822 string matching against version number of glibc to ensure inclusino 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-21 11:03:20 -07:00
Nikolaj Bjorner
4d31ff7a38 remove unused variable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-21 08:35:09 -07:00
Nikolaj Bjorner
3479cdc10b separate hint literals 2023-07-20 10:52:58 -07: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
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
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
Nikolaj Bjorner
3e58f0cff1 build fixes 2023-07-13 09:25:20 -07:00