mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-30 03:02:29 +00:00
Code Activity
18555 commits 49 branches 53 tags 180 MiB
Commit graph

18555 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
5f451182f7 missing cmake list 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-22 12:02:24 -08:00
Nikolaj Bjorner
e321643bf5 move sls core functionality to be independent of tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-22 12:00:52 -08:00
Nuno Lopes
606a9a7409 fix test build 2023-12-22 16:19:28 +00:00
Nuno Lopes
cab3c45863 remove unnecessary parameter copies 2023-12-22 16:11:06 +00:00
Nuno Lopes
ab22e763d7 some code simplifications in mpn 
plus remove duplicated assertion
 2023-12-22 15:29:04 +00:00
Nikolaj Bjorner
4fe423482a bugfix on slack 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-21 15:36:26 -08:00
Nuno Lopes
766f5f04c0 reduce memory allocs in params 2023-12-21 23:27:28 +00:00
Nikolaj Bjorner
ae1d9270b5 improve add bin/item functions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-21 15:27:11 -08:00
Nikolaj Bjorner
b09c237775 rudimentary bin cover solver using the user propagator 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-21 15:18:26 -08:00
Christoph M. Wintersteiger
68a2c08d5e
Add Z3_get_estimated_alloc_size to OCaml API (#7068) 2023-12-21 12:54:30 -08:00
Lev Nachmanson
19f3ad46ce fix the build 2023-12-20 14:14:01 -10:00
Lev Nachmanson
e9fa7db96c revert smt_enode 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2023-12-20 14:03:27 -10:00
Lev Nachmanson
a00eb08ddd Merge branch 'master' of https://github.com/z3prover/z3 2023-12-20 12:56:55 -10:00
Lev Nachmanson
4317d134bf refactor: move gomory functionaly from int_solver to gomory 2023-12-20 12:56:20 -10:00
Nuno Lopes
c4fa719751 revert last two commits; MSVC doesn't like to statically allocate flexible arrays 2023-12-20 19:10:05 +00:00
Nuno Lopes
6246c6517d fix debug build 2023-12-20 18:30:53 +00:00
Nuno Lopes
c9c53b7c65 tmp_enode: don't heap allocate an app. store it inline instead. 
Saves heap allocations and double indirections
 2023-12-20 18:19:20 +00:00
Nuno Lopes
4898a156d8 shrink ast's app by 8 bytes on 64-bit platforms when number of args > 0 2023-12-20 16:58:45 +00:00
Nuno Lopes
b2d5c24c1d remove a few string copies 2023-12-20 16:55:09 +00:00
Lev Nachmanson
e28b644a67 remove an empty line 2023-12-20 06:53:59 -10:00
Lev Nachmanson
d6365610d5 change some TRACE statements 2023-12-20 06:49:55 -10:00
dependabot[bot]
db5a1a7604
Bump actions/upload-artifact from 3 to 4 (#7065) 
Bumps [actions/upload-artifact](https://github.com/actions/upload-artifact) from 3 to 4.
- [Release notes](https://github.com/actions/upload-artifact/releases)
- [Commits](https://github.com/actions/upload-artifact/compare/v3...v4)

---
updated-dependencies:
- dependency-name: actions/upload-artifact
  dependency-type: direct:production
  update-type: version-update:semver-major
...

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
 2023-12-19 08:59:11 -08:00
Jakob Rath
97d450868e
Vector updates from polysat branch (#7066) 
* vector: add erase_if

* vector: generalize operator<<

* vector: fix missing destructor call
 2023-12-19 08:58:55 -08:00
Jakob Rath
4c9f705cd1
tptr: add pointer tagging templates (#7067) 2023-12-19 08:58:32 -08:00
Nuno Lopes
fcc7b25c19 remove a few string copies 2023-12-19 14:34:37 +00:00
Nikolaj Bjorner
e5f52e2131
Update Windows.yml 2023-12-18 20:53:51 -08:00
Lev Nachmanson
d088fe9c43 Merge branch 'master' of https://github.com/z3prover/z3 2023-12-18 18:49:39 -10:00
Lev Nachmanson
9a18628b17 remove unnecessary assignments 2023-12-18 18:49:27 -10:00
Nikolaj Bjorner
5cafda1fad remove reference to matrix bindings to see if it works 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-19 04:45:02 +00:00
Nikolaj Bjorner
2602fc2eb5 remove reference to matrix bindings to see if it works 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-19 04:41:02 +00:00
Nikolaj Bjorner
1b7550483e add path n prefix 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-19 04:33:07 +00:00
Nikolaj Bjorner
00965cbdf2 fix string 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-19 04:31:54 +00:00
Nikolaj Bjorner
394a355b19 fix string 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-19 04:29:30 +00:00
Nikolaj Bjorner
9469f7574a
Update Windows.yml 2023-12-18 20:26:39 -08:00
Nikolaj Bjorner
ea03b558c6
Update Windows.yml 2023-12-18 20:23:45 -08:00
Nikolaj Bjorner
bb8ed43cdb
Update Windows.yml 2023-12-18 20:20:21 -08:00
Nikolaj Bjorner
ea44c110bb gc expressions in the scope of updates, not old expressions 2023-12-18 20:08:29 -08:00
Nikolaj Bjorner
842385a7d7
Update Windows.yml 2023-12-18 19:48:42 -08:00
Nikolaj Bjorner
62ae9a0b72
Update Windows.yml 2023-12-18 19:46:39 -08:00
Nikolaj Bjorner
91ba893d7b
Update Windows.yml 2023-12-18 19:43:11 -08:00
Nikolaj Bjorner
ee073be3f0
Update Windows.yml 2023-12-18 19:38:50 -08:00
Nikolaj Bjorner
c7c007c2c6
Update Windows.yml 2023-12-18 19:31:17 -08:00
Nikolaj Bjorner
9e3a489a6c
Update Windows.yml 2023-12-18 19:09:01 -08:00
Nikolaj Bjorner
0dc851132e
Create Windows.yml 2023-12-18 19:07:14 -08:00
Nikolaj Bjorner
13be3c3fbb reset model converter between rounds to elim-unconstrained. 2023-12-18 16:57:52 -08:00
Nikolaj Bjorner
0daa05aab2 add ability to log selected bv rewrites 2023-12-18 16:57:52 -08:00
Nikolaj Bjorner
dff419a7cb pin expressions to fix unsound behavior 2023-12-18 16:57:52 -08:00
Nikolaj Bjorner
5d4c18dde2 fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-18 16:57:00 -08:00
Nikolaj Bjorner
6d23847482 fix typos 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-18 09:33:40 -08:00
Nikolaj Bjorner
d008dbe50a port Jakob's update to bv_internalize 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-18 09:31:59 -08:00