mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity
19142 commits 23 branches 48 tags 156 MiB
Commit graph

19142 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner fa6f3f2dba fixing prop-queue 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-11-04 17:18:02 -08:00
Nikolaj Bjorner b870ed192a include disequality expansion for non-unit case. 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-11-04 09:26:32 -08:00
Nikolaj Bjorner 6559584502 use original gai 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-11-02 12:23:36 -07:00
Nikolaj Bjorner d702e68fb9 fix build warning 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-11-02 11:26:25 -07:00
Nikolaj Bjorner 40b927ff2b remove package and package lock 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-11-02 11:12:54 -07:00
Nikolaj Bjorner 7875c95866 Merge branch 'master' into sls 2024-11-02 10:41:15 -07:00
Nikolaj Bjorner c7ec2afedb fixes to model construction 2024-11-01 15:38:30 -07:00
Nikolaj Bjorner 040c29a152 update model generation to fix model bug 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-11-01 14:41:15 -07:00
Nikolaj Bjorner 55b64e1f29 use glue as computed without adjustment 2024-11-01 13:57:56 -07:00
Nikolaj Bjorner 289f8360f2 fix non-termination 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-29 23:39:39 -07:00
Nikolaj Bjorner 0a404f94be rework elim_unconstrained 2024-10-29 22:31:26 -07:00
Nikolaj Bjorner ecdfab81a6 fix #7434 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-28 17:51:01 -07:00
Nikolaj Bjorner fbf3012864 add virtual destructor 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-27 22:24:45 -07:00
Nikolaj Bjorner 7e9d0537d7 normalizing inequality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-27 22:23:01 -07:00
Nikolaj Bjorner 9a5fa60e98 add missing operator handling for bitwise operators 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-27 21:51:36 -07:00
Nikolaj Bjorner 077b173858 add missing operator handling for bitwise operators 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-27 21:32:55 -07:00
Nikolaj Bjorner e35eab000c use th-axioms to track origins of assertions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-27 19:08:44 -07:00
Nikolaj Bjorner 5e2cefea9f mk_value needs to accept more cases where integer expression doesn't evalate 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-27 19:03:20 -07:00
Nikolaj Bjorner bdf3689c6e na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-27 18:53:25 -07:00
Nikolaj Bjorner 98bc3d392d fixup model generation for theory_intblast 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-27 14:08:22 -07:00
Nikolaj Bjorner 7e2acad030 add intblast to legacy SMT solver 2024-10-27 12:28:36 -07:00
Nikolaj Bjorner aa67c3655f bugfixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-26 16:10:44 -07:00
Nikolaj Bjorner 6f37da5a07 validate sls-arith lemmas 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-26 14:56:38 -07:00
Nikolaj Bjorner c6f5e3232c use independent completion flag for sls to avoid conflating with genuine cancelation 2024-10-26 14:48:13 -07:00
Nikolaj Bjorner 646eacd2aa check delayed eqs before nla 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-26 11:48:26 -07:00
Nikolaj Bjorner fb78a9e3a5 change namespace for single threaded 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-26 11:28:54 -07:00
Nikolaj Bjorner f902feb478 reorder inclusion order to define smt_context before theory_sls 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-26 10:46:23 -07:00
Nikolaj Bjorner b0fef6429f
Add assert_and_track support to Optimize class in .NET binding (#7437) 
Related to #7436

#7436

---

For more details, open the [Copilot Workspace session](https://copilot-workspace.githubnext.com/Z3Prover/z3/issues/7436?shareId=XXXX-XXXX-XXXX-XXXX).
 2024-10-26 01:33:09 -07:00
Nikolaj Bjorner ab2c992aa1 build warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-26 01:31:41 -07:00
Nikolaj Bjorner d7b1a5e3be add virtual destructor 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-26 01:24:22 -07:00
Nikolaj Bjorner 0c2e09db7f remove declaration of context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-26 00:11:08 -07:00
Nikolaj Bjorner a88daf246e fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-25 23:45:14 -07:00
Nikolaj Bjorner ba1630f380 fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-25 23:40:05 -07:00
Nikolaj Bjorner 848bfb14a1 use common infrastructure for sls-smt 2024-10-25 23:29:26 -07:00
Nikolaj Bjorner 894bfc7e17 fixes 2024-10-25 22:46:15 -07:00
Nikolaj Bjorner 22ab598d73 bug fixes 2024-10-25 17:26:33 -07:00
Nikolaj Bjorner ef95b4eaf2 add plugin to smt_context, factor out sls_smt_plugin functionality. 2024-10-25 17:15:05 -07:00
Nikolaj Bjorner 8b657f27aa add shortcut to retrieve kind of application 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-22 13:05:58 -07:00
Nikolaj Bjorner 78d1139ba0 add shortcut to retrieve kind of application 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-22 13:04:41 -07:00
Nikolaj Bjorner 0ebea1c298 remove debug out 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-22 11:58:16 -07:00
Nikolaj Bjorner 253f7d7675 fix non-termination bug in elim-unconstrained, add parameter validation to fix #7432 2024-10-22 09:59:20 -07:00
Nikolaj Bjorner d18831c8d5 Update sat_ddfw.cpp 2024-10-22 09:59:20 -07:00
Nikolaj Bjorner f453cdec92 update log level 2024-10-22 09:58:36 -07:00
Jonas Jongejan 45ef6d0109
js: Adding manual release methods (#7428) 
* js: Adding manual release methods

* Add unregister token

* Add pointer assertion

* Add missing line
 2024-10-22 09:15:49 -07:00
Nikolaj Bjorner 93086143b3 fix dirty flag setting 2024-10-21 19:57:47 -07:00
Nikolaj Bjorner b0dd83cc60 debugging parallel integration 2024-10-21 13:27:01 -07:00
Kirill A. Korinsky 5cee19fa09
It uses C++20 BTW (#7429) 2024-10-20 20:00:36 -07:00
Nikolaj Bjorner 185ddd6488 Track shared variables using a unit set 2024-10-20 17:54:44 -07:00
Nikolaj Bjorner 59b0e46d99 rename aux functions 2024-10-20 16:46:19 -07:00
Nikolaj Bjorner cc430987b7 add value transfer option 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-20 16:38:00 -07:00