mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-30 11:12:28 +00:00
Code Activity
18338 commits 49 branches 53 tags 181 MiB
Commit graph

18338 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
f07553ed3a formatting updates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-09-19 15:18:38 -07:00
Nikolaj Bjorner
db84d21e3b
Merge branch 'master' into unit_prop_on_monomials 2023-09-19 14:44:01 -07:00
Nikolaj Bjorner
fba5de3a25 remove unused code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-09-19 14:43:02 -07:00
Nikolaj Bjorner
4d742001ab formatting of else 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-09-19 14:36:21 -07:00
Nikolaj Bjorner
85db8163fa move allocator to memory_manager and std_vector to vector 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-09-19 13:57:28 -07:00
Lev Nachmanson
c5cfd62e0a remove dead code related to nla unit propagation 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2023-09-19 10:56:09 -07:00
dependabot[bot]
345d6ec8a5
Bump docker/login-action from 2 to 3 (#6911) 
Bumps [docker/login-action](https://github.com/docker/login-action) from 2 to 3.
- [Release notes](https://github.com/docker/login-action/releases)
- [Commits](https://github.com/docker/login-action/compare/v2...v3)

---
updated-dependencies:
- dependency-name: docker/login-action
  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-09-18 17:49:00 -07:00
dependabot[bot]
17a38b7ae0
Bump docker/metadata-action from 4 to 5 (#6910) 
Bumps [docker/metadata-action](https://github.com/docker/metadata-action) from 4 to 5.
- [Release notes](https://github.com/docker/metadata-action/releases)
- [Upgrade guide](https://github.com/docker/metadata-action/blob/master/UPGRADE.md)
- [Commits](https://github.com/docker/metadata-action/compare/v4...v5)

---
updated-dependencies:
- dependency-name: docker/metadata-action
  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-09-18 17:48:35 -07:00
dependabot[bot]
3b78c6318c
Bump docker/build-push-action from 4.2.1 to 5.0.0 (#6909) 
Bumps [docker/build-push-action](https://github.com/docker/build-push-action) from 4.2.1 to 5.0.0.
- [Release notes](https://github.com/docker/build-push-action/releases)
- [Commits](https://github.com/docker/build-push-action/compare/v4.2.1...v5.0.0)

---
updated-dependencies:
- dependency-name: docker/build-push-action
  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-09-18 17:48:16 -07:00
Lev Nachmanson
cf63e75898 using structures from util in lp_bound_propagator 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2023-09-18 13:25:24 -07:00
Nikolaj Bjorner
643512613a simplify last_index function 2023-09-18 12:52:59 -07:00
Nikolaj Bjorner
31c91e1674 #6902 
add parse check for identifiers used for datatype declarations.
 2023-09-18 12:52:59 -07:00
John Fleisher
858477f3e3
Add c++ flags for vulcan assembly compliance (#6906) 2023-09-18 09:03:56 -07:00
Nuno Lopes
b1c52c0b16 don't crash when a function doesn't have a model when converting a solver to string 2023-09-18 10:16:19 +01:00
Nuno Lopes
ff33fa355a fix debug single-thread build 2023-09-18 09:44:37 +01:00
Lev Nachmanson
af8d192392 add an include 2023-09-17 13:14:36 -07:00
Lev Nachmanson
10095a30b7 add an include file 2023-09-17 12:25:11 -07:00
Lev Nachmanson
66f6a0327f change type of m_ibounds to std::vector 2023-09-17 11:00:48 -07:00
Lev Nachmanson
30b743d7b3 refactor propagat_monic 2023-09-17 10:45:54 -07:00
Lev Nachmanson
7353d7fb4d fix dep calculations in lp_bound_propagator 2023-09-17 06:48:12 -07:00
Lev Nachmanson
77e56b0a69 debug 2023-09-16 13:54:14 -07:00
Lev Nachmanson
c240f62ca8 is_linear does not check for is_big 2023-09-15 17:44:10 -07:00
Lev Nachmanson
b621c9fa1c remove an extrac check in bound_is_interesting 2023-09-15 17:42:18 -07:00
Lev Nachmanson
4cfba9787b debug lp_bound_propagator 2023-09-15 17:41:10 -07:00
Lev Nachmanson
762ade2a79 check m_unassigned_bounds in bound_is_interesting 2023-09-15 06:15:22 -07:00
Lev Nachmanson
a55aa1a648 add a comment 2023-09-14 19:29:48 -07:00
Lev Nachmanson
b3673d491e fix the build for gcc 2023-09-14 19:20:47 -07:00
Nikolaj Bjorner
278d5a3482 Merge branch 'master' of https://github.com/z3prover/z3 2023-09-14 17:14:24 -07:00
Nikolaj Bjorner
b87a91379c fix #6894 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-09-14 17:14:14 -07:00
Nikolaj Bjorner
50d76a2fe3 fix #6894 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-09-14 17:14:14 -07:00
Lev Nachmanson
cbad61ba2e propagate monics with lp_bound_propagator 2023-09-13 14:27:34 -07:00
Lev Nachmanson
c309d52283 runs a simple test 2023-09-13 08:12:00 -07:00
dependabot[bot]
e718bb6473
Bump docker/build-push-action from 4.1.1 to 4.2.1 (#6896) 
Bumps [docker/build-push-action](https://github.com/docker/build-push-action) from 4.1.1 to 4.2.1.
- [Release notes](https://github.com/docker/build-push-action/releases)
- [Commits](https://github.com/docker/build-push-action/compare/v4.1.1...v4.2.1)

---
updated-dependencies:
- dependency-name: docker/build-push-action
  dependency-type: direct:production
  update-type: version-update:semver-minor
...

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
 2023-09-12 08:09:01 +01:00
Sijmen
0a444f357a
Slightly improve Z3_LIBRARY_PATH error message (#6895) 2023-09-11 12:58:03 -07:00
Lev Nachmanson
c050af922f fixing the bugs 2023-09-07 15:59:20 -07:00
Lev Nachmanson
c43b99daae renaming 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2023-09-07 11:57:20 -07:00
Lev Nachmanson
47b64e689c restore the lemma scheme 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2023-09-07 11:33:14 -07:00
Lev Nachmanson
288e66de59 restore m_crossed* and create lemmas 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2023-09-06 09:27:30 -07:00
Lev Nachmanson
41f59cb1ed propagate monomial is nla 2023-09-05 18:49:59 -07:00
dependabot[bot]
3aea4ebf42
Bump actions/checkout from 3 to 4 (#6888) 
Bumps [actions/checkout](https://github.com/actions/checkout) from 3 to 4.
- [Release notes](https://github.com/actions/checkout/releases)
- [Changelog](https://github.com/actions/checkout/blob/main/CHANGELOG.md)
- [Commits](https://github.com/actions/checkout/compare/v3...v4)

---
updated-dependencies:
- dependency-name: actions/checkout
  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-09-05 16:58:47 -07:00
Nikolaj Bjorner
4d9af7848d add parameter to disable pattern inference #6884 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-09-03 15:27:37 -07:00
Nikolaj Bjorner
99239068ba some template instantiations #6869 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-09-03 15:21:49 -07:00
Nikolaj Bjorner
c2e73a6aae logging pre-processing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-09-03 15:19:31 -07:00
Lev Nachmanson
318d7d7564 fixes a bug 2023-09-01 11:32:26 -07:00
Lev Nachmanson
d3258e7084 propagate lineal monomial 2023-09-01 11:18:03 -07:00
Lev Nachmanson
5509b468e9 handle monomial_bounds::unit_propagate() 2023-08-31 17:35:41 -07:00
Nikolaj Bjorner
ff3268e636 move unit propagation into monomial_bounds 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-31 14:32:05 -07:00
Nikolaj Bjorner
c2cbe72b64 sketch linear monomial propagation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-31 11:49:05 -07:00
Nikolaj Bjorner
38b131386d add stubs for monomial unit propagation 2023-08-30 17:21:48 -07:00
Nuno Lopes
00593609c5 minor code simplification 2023-08-30 12:50:29 +01:00