mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 09:55:19 +00:00
Code Activity
15137 commits 23 branches 48 tags 156 MiB
Commit graph

15137 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nuno Lopes c47ab023e5 remove a few trivial destructors so they get inlined 2021-04-04 17:13:59 +01:00
Nikolaj Bjorner c0e74f946b patch to fix #5145 
underlying issue is that model updates for multi-objective and single objective solving are too brittle to serve its use cases among different plugins.
For maxlex, the last model is always the best and it doesn't use multiple objectives.
 2021-04-02 12:23:01 -07:00
Nikolaj Bjorner cebf83c460 fix #5146 2021-04-02 11:48:44 -07:00
Nikolaj Bjorner 1fc9a7ba84 fix regression, fix #5115 2021-03-30 17:43:12 -07:00
Nikolaj Bjorner 1fcd537d81 fix #5117 2021-03-30 14:23:30 -07:00
Nikolaj Bjorner c71bbb6391 fix #5136, regression when removing variable registration for mod/div operations 2021-03-30 13:45:54 -07:00
Nikolaj Bjorner c629f09f21 fix #5139 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-03-29 15:46:47 -07:00
Nikolaj Bjorner 94b4d1b442 fix travis build for python doc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-03-29 15:30:31 -07:00
Nikolaj Bjorner 2fdb703865 remove redundant assertion 2021-03-29 15:17:01 -07:00
Nikolaj Bjorner 5cc29bec14 simplify ""* to "" 2021-03-29 14:18:57 -07:00
Nikolaj Bjorner 6d28b1a858 fix #5134 2021-03-29 14:11:49 -07:00
Nikolaj Bjorner 6bdf377e11 remove unneeded assertion fix #5131 2021-03-28 21:20:05 -07:00
Nikolaj Bjorner dfb696becf fix #5119 2021-03-28 16:47:56 -07:00
Nikolaj Bjorner 974ef3c147 port equality propagation changes to new core 2021-03-28 16:15:04 -07:00
Nikolaj Bjorner 0432311b11 fix #5121 2021-03-28 16:14:37 -07:00
Nikolaj Bjorner 6aa766a544 fix perf regression for new arithmetic solver, missing equality propagation #5106 2021-03-28 14:17:50 -07:00
Nikolaj Bjorner d6691830c7 fix perf regression for new solver, missing equality propagations #5106 2021-03-28 14:17:50 -07:00
Nikolaj Bjorner bb2c40072e skip div 1 2021-03-28 14:17:49 -07:00
Nikolaj Bjorner 22d66f57f1 pp 2021-03-28 14:17:49 -07:00
Zachary Wimer 531a828c57
Update setup.py to use cmake build system (#5128) 2021-03-28 14:17:33 -07:00
Nikolaj Bjorner 0c25d2560d improve diagnosability 2021-03-26 14:58:25 -07:00
Nikolaj Bjorner e89071d366 #5125 2021-03-26 14:58:24 -07:00
Nikolaj Bjorner c2b353ba72 adding factorization 2021-03-26 14:58:24 -07:00
Nikolaj Bjorner a352a6638a fix #5126 2021-03-26 14:58:24 -07:00
Nikolaj Bjorner 7fab0f5923 updated experiment 2021-03-26 14:58:23 -07:00
Luca Bruno b918f121ef
zstring: fix encode rountrip for '\' as printable ASCII (#5120) 
This fixes encode roundtripping for all printable ASCII characters.
In particular, this now leaves a plain '\' untouched by the
encoding logic, instead of converting it to escaped hex-digits.
It also adds unit testing covering this specific zstring encoding
property, in order to avoid future regressions.
 2021-03-23 11:25:59 -07:00
Luca Bruno 119c5a995b
cmake/git: tweak submodule detection logic (#5118) 
This removes an incomplete check in cmake git-submodule detection
logic, directly using filepath probing instead. As a direct usecase,
it fixes submodule building for https://github.com/prove-rs/z3.rs.
 2021-03-22 16:10:17 -07:00
Nikolaj Bjorner 67e419d20d yada yada 2021-03-21 19:57:17 -07:00
Nikolaj Bjorner 2ee971ef68 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-03-21 12:32:01 -07:00
Nikolaj Bjorner 2fef6dc502 more scaffolding 2021-03-21 11:31:14 -07:00
Nikolaj Bjorner a1f484fa35 na 2021-03-19 16:42:45 -07:00
Nikolaj Bjorner 731cf9b885 ensure compilation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-03-19 15:37:05 -07:00
Nikolaj Bjorner 560f072786 elaborate on header 2021-03-19 14:26:52 -07:00
Lev Nachmanson 3b67dd8288 add a trace statement 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2021-03-19 13:17:27 -07:00
Nikolaj Bjorner 1971ee60e1 Create polysat.h 2021-03-19 11:15:06 -07:00
Nikolaj Bjorner 15a7621e27 remove template dependency for trail objects 2021-03-19 11:15:05 -07:00
Nikolaj Bjorner c05c5caab5 fix #5111 2021-03-19 11:15:04 -07:00
Murphy Berzish 064b1f0721
z3str3: address code reviews and remove some dead code (#5116) 2021-03-19 10:37:16 -07:00
Nikolaj Bjorner bf692a5076 dependency 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-03-17 17:10:01 -07:00
Nikolaj Bjorner eb13ad14e5 python build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-03-17 16:26:44 -07:00
Nikolaj Bjorner 97f560054d Create CMakeLists.txt 2021-03-17 15:51:50 -07:00
Nikolaj Bjorner ab0735fde2 separate component for asserted_formulas to break dependency cycles 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-03-17 15:51:38 -07:00
Nikolaj Bjorner 25343232ca add dependency 2021-03-17 15:36:02 -07:00
Nikolaj Bjorner 156139622c delay (lazy) process equalities. 2021-03-17 15:34:04 -07:00
Nikolaj Bjorner ddbcd08d46 move asserted_formulas to solver scope 2021-03-17 15:02:16 -07:00
Nikolaj Bjorner 0b8939d86e self-contained function for merge_tf 2021-03-16 15:24:48 -07:00
Nikolaj Bjorner 0949ad26c2 fix #5107 2021-03-16 15:24:34 -07:00
Nikolaj Bjorner 9c716a2788 fix #5108 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-03-16 07:37:06 -07:00
Andrew V. Jones d0515dca50
Circular seq axioms node (#5104) 
* Dealing with ambiguity when calling 'find_file' #5089

Signed-off-by: Andrew V. Jones <andrewvaughanj@gmail.com>

* Correcting ambiguity when calling 'find_file' if the file is in the current src dir #5089

Signed-off-by: Andrew V. Jones <andrewvaughanj@gmail.com>

* Ensuring consistency when obtaining the original include #5089

Signed-off-by: Andrew V. Jones <andrewvaughanj@gmail.com>
 2021-03-16 06:58:54 -07:00
Nikolaj Bjorner 648568489c internalize only terms not atoms 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-03-16 06:53:14 -07:00