mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-26 09:24:36 +00:00
Code Activity
19040 commits 45 branches 52 tags 177 MiB
Commit graph

19040 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
ce1f3987d9 fix unsoundness in quantifier propagation #6116 and add initial lemma logging 2022-08-23 19:10:01 -07:00
Nikolaj Bjorner
912b284602 disable validate_hint too permissive 2022-08-23 19:07:55 -07:00
Nikolaj Bjorner
2f8b13368d add redirect for warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-23 15:55:55 -07:00
Nikolaj Bjorner
fbf9e3004f ack 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-23 10:16:13 -07:00
Nikolaj Bjorner
fbfb28eba9 update release notes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-23 10:15:41 -07:00
Nuno Lopes
916d1dbb13 fix default parameter regression 
bug introduced in commit 63f48f8fd4
 2022-08-23 15:26:29 +01:00
Nuno Lopes
7ab904bfc6 remove spurious file 2022-08-23 14:39:44 +01:00
Nikolaj Bjorner
0eea021dc3 include global parameters and fixup for HTML meta-characters 2022-08-22 14:25:18 -07:00
Nikolaj Bjorner
f6e4a45f4b Merge branch 'master' of https://github.com/z3prover/z3 2022-08-21 18:28:19 -07:00
Nikolaj Bjorner
64e0e785e7 #5953 2022-08-21 18:28:07 -07:00
Nikolaj Bjorner
09ab575d29 parens 2022-08-21 18:27:14 -07:00
Nikolaj Bjorner
daa24ef4ce add missing error check 2022-08-21 18:26:53 -07:00
Nikolaj Bjorner
9eb4237dfe fix #6292 
this patches a case where macro-finder is used with arrays. It doesn't work so macro quantifiers have to be re-instated to ensure correctness
 2022-08-21 16:32:01 -07:00
Nikolaj Bjorner
a38308792e #6288 
floating points may also track bit-literals.
Since the legacy solver doesn't handle dual tracking of literals we just let the floating point solver track.
 2022-08-21 15:47:19 -07:00
Nikolaj Bjorner
4092302590 use interface for creating unary equalities 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-21 15:37:43 -07:00
Nikolaj Bjorner
17fc438476 don't have bv-ackerman influence simplification 
previous scheme has Ackmerman module instrument main solver to backjump and simplify when reaching a threshold.
This destroys overall performance: simplification does many more things than invoking Ackerman axioms.
Having a dependency between simplification (in-processing) and depleting a priority queue of auxiliary axioms therefore hurts overall performance. It has to be decoupled. The current approach is now to empty the axiom queue on occasion.
It is still not ideal - it should be coupled with the search level - axioms don't survive higher levels where redundant clauses get garbage collected as they don't have a chance of being used.
 2022-08-21 15:25:18 -07:00
Nikolaj Bjorner
be0cd74c71 #6289 2022-08-21 15:25:17 -07:00
Nikolaj Bjorner
2181a0ff74 #6289 2022-08-21 15:25:17 -07:00
Clemens Eisenhofer
56fb161532
ADT-constructor generation crashed in .NET/Java when no (= default) fields are given (#6287) 2022-08-21 12:40:38 -07:00
Bruce Mitchener
6ba9ada1e2
Fix typos. (#6291) 2022-08-21 12:40:07 -07:00
Bruce Mitchener
706f7fbdc7
Fix some warnings about unused stuff. (#6290) 2022-08-21 12:39:30 -07:00
Nuno Lopes
d5d77dfe64 minor code simplifications 2022-08-20 12:56:45 +01:00
Nikolaj Bjorner
08bf7a6293 fix name 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-19 18:22:42 -07:00
Nikolaj Bjorner
665ef2c6ba add missing new 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-19 18:21:03 -07:00
Nikolaj Bjorner
bb5d81195c use equalities 2022-08-19 18:17:16 -07:00
Nikolaj Bjorner
b26420ed99 #6285 2022-08-19 18:17:16 -07:00
Eric Kilmer
ea8b118eb1
Android CI: Configure with CMAKE_ANDROID_API (#6284) 
CMAKE_ANDROID_API will set CMAKE_SYSTEM_VERSION if it's not defined.

Also remove setting CMake variable values that don't affect the ability
to successfully configure in CI.
 2022-08-19 11:02:26 -07:00
Nikolaj Bjorner
e83a70f9ad add newlines for description 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-19 06:57:39 -07:00
Nikolaj Bjorner
514eaf33aa Merge branch 'master' of https://github.com/z3prover/z3 2022-08-18 19:07:55 -07:00
Nikolaj Bjorner
600b4491aa don't forget parameter documentation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-18 19:07:39 -07:00
Nikolaj Bjorner
540e36e6cb roll version number 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-18 15:47:08 -07:00
Nikolaj Bjorner
19da3c7086 fix closing parnetheses 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-18 13:26:29 -07:00
Nikolaj Bjorner
d094f6a856 fixing interface and test' 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-18 13:00:46 -07:00
Nikolaj Bjorner
c7eda4e687 fixing interface and test' 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-18 12:59:00 -07:00
Nikolaj Bjorner
103cd248f1 update release notes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-18 12:51:33 -07:00
Nikolaj Bjorner
c3d635cf77 handle build warning 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-18 12:50:30 -07:00
Nikolaj Bjorner
6fb7a049ea test fromString 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-18 12:41:02 -07:00
Nikolaj Bjorner
53e168879a add fromString method 2022-08-18 12:33:10 -07:00
Nikolaj Bjorner
4be26eb543 #6116 
handle also nan/oo/0+ as numerals
 2022-08-18 04:26:14 -07:00
Nikolaj Bjorner
8e167aa213 #6116 
fix unsoundness issue due to book-keeping changes for whether the solver uses assumptions.
 2022-08-18 03:58:06 -07:00
Nikolaj Bjorner
1a5503c87b enable new code path for mod handling 2022-08-17 07:31:26 -07:00
Nikolaj Bjorner
cb272bd7a8 fix missing removal of x in solve_mod 2022-08-17 07:31:26 -07:00
John Fleisher
b3f4d3fdc7
Publish Z3 symbols (#6280) 
* WiP: publish symbols for package

* set debugtype to full

* fix internal nuget feed publishing

* Try pipeline github authorization

* Update github service connection

* WiP: try symbol publish in build

* try Z3Prover for GitHub connection

* WiP: collect symbols

* revert symbol type to pdbonly (only portable is not supported for publishing)

* Publish symbols in nightly and release

* Revert this: comment out publish to test release build pipe

* restore publishing

* Turn of index sources to eliminate warning that it is not supported for Github

Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-17 07:30:55 -07:00
Nikolaj Bjorner
48b13291d1 add bv-size reduce #6137 
- add option smt.bv.reduce_size.
  - it allows to apply incremental pre-processing of bit-vectors by identifying ranges that are known to be constant.
    This rewrite is beneficial, for instance, when bit-vectors are constrained to have many high-level bits set to 0.
 2022-08-16 16:35:14 -07:00
Nikolaj Bjorner
45a4b810de fixup github connection 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-16 15:12:05 -07:00
Nikolaj Bjorner
21033790be add parameter documentation to nightly 2022-08-16 15:07:19 -07:00
Nikolaj Bjorner
fe00e95f72 remove \r from output 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-16 09:20:50 -07:00
Nikolaj Bjorner
9d6de2f873 parameters neatified 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-16 09:14:34 -07:00
Nikolaj Bjorner
498b6de3a7 finish parameter help 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-16 08:29:24 -07:00
Nikolaj Bjorner
b169292743 add parameter descriptions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-16 08:26:53 -07:00