3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 02:15:19 +00:00
Commit graph

18031 commits

Author SHA1 Message Date
Clemens Eisenhofer 4133a1cc5a
Fix UP registration in final callback (#6929)
* Fix registration in final

* Don't make it too complicated...
2023-10-03 09:51:02 +09:00
Nikolaj Bjorner ab8fe199c5 fix case for 0 multiplier in monomial_bounds
disabled in master - it violates invariants in the lra solver.
2023-10-01 18:41:23 +09:00
Nikolaj Bjorner 50654f1f46 add theory propagation to linear monomial propagation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-09-30 08:52:09 +09:00
Nikolaj Bjorner ddcd1ee992 non-fixed term should have bound 0
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-09-28 09:25:36 -07:00
Nikolaj Bjorner 65e59e3ec4 sketch of internal propagation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-09-27 20:43:38 -07:00
Nikolaj Bjorner 7207f0ff9c sketch of internal propagation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-09-27 20:40:55 -07:00
Nikolaj Bjorner 9033b826f4 debug output with the variable that is fixed and its value
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-09-27 00:52:26 -07:00
Nikolaj Bjorner 2297b0334b re-introduce simple implementation of linear monomial propagation for evaluation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-09-26 23:53:14 -07:00
Nikolaj Bjorner 6559e5fb32 port over std_vector and std-allocator functionality from monomial propagation branch
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-09-26 21:15:07 -07:00
Nikolaj Bjorner aaa587398e add propagation flag to monic and method for updating it to emonics. This replaces the bool-vector tracking for propagation and internalizes it to the emonics class
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-09-26 20:52:34 -07:00
Nikolaj Bjorner 9c63ea3135 port over cosmetics from unit_prop_on_monomials branch
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-09-26 20:24:49 -07:00
Nikolaj Bjorner 36566d6193 port over moving m_nla_lemmas into nla_core from the linear monomial propagation branch
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-09-26 20:15:22 -07:00
Nikolaj Bjorner e4e1d6148c port over moving m_nla_lemmas into nla_core from the linear monomial propagation branch
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-09-26 20:14:42 -07:00
Nikolaj Bjorner ec2937e2de port over moving m_nla_lemmas into nla_core from the linear monomial propagation branch
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-09-26 20:08:30 -07:00
Nikolaj Bjorner 8d2b65b20b add options to allow testing the effect of non-linear hammers
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-09-26 19:18:44 -07:00
Nuno Lopes 029d726eb8 minor code simplification 2023-09-25 15:33:40 +01:00
Nikolaj Bjorner db097bae05 use format from unit_prop_on_monomials branch
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-09-23 17:24:46 -07:00
Nikolaj Bjorner 61319ffd85 cache is_shared information in the enode
observed perf overhead for QF_NIA is that assume_eqs in theory_lra incurs significant overhead when calling is_relevant_and_shared. The call to context::is_shared and the loop checking for beta redexes is a main bottleneck. The bottleneck is avoided by caching the result if is_shared inside the enode. It is invalidated for every merge/unmerge.
2023-09-23 17:19:06 -07:00
Nikolaj Bjorner eea9c0bec6 fix #6914 2023-09-23 11:22:25 -07:00
Nikolaj Bjorner 30d1800c31 #6916
short circuiting equality consequence appears to have the wrong sign
2023-09-23 10:32:51 -07:00
Nikolaj Bjorner eff3f5f65e port bug fixes from unit prop branch
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-09-22 09:45:58 -07:00
Nikolaj Bjorner fba5de3a25 remove unused code
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-09-19 14:43:02 -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
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
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
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
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
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
Nikolaj Bjorner 09f911d8a8 include rewriter for recursive functions in model-evaluator
fixes bug reported by Tahina and Nick, @tahina-pro
2023-08-28 11:31:40 -07:00
Hari Govind V K 5ba06f4e28
print deq in lits2pure. fix #6877 (#6878) 2023-08-26 20:53:15 -07:00
Nikolaj Bjorner 63467f9dfa fix #6876
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-08-25 17:14:35 -07:00
Nikolaj Bjorner e8929041b8 fixing calls, signs 2023-08-22 09:29:12 -07:00
Nikolaj Bjorner 818b1129a5 fix regression in sign of literals from new solver 2023-08-22 09:04:08 -07:00
Lev Nachmanson 4564752c2f
Merge pull request #6863 from Z3Prover/nl_branches
split free vars in nla
2023-08-21 18:19:21 -07:00
Lev Nachmanson 61a7c6b28d init m_literal_vec
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2023-08-21 17:11:55 -07:00