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
Lev Nachmanson
9aeaed8f53
Merge branch 'master' into nl_branches
2023-08-21 16:15:20 -07:00
Nikolaj Bjorner
1d9e0feb84
Merge branch 'master' of https://github.com/z3prover/z3
2023-08-21 09:19:16 -07:00
Nikolaj Bjorner
79aa317af4
remove if-def inside cpp file that should not be there #6869
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-08-21 09:19:06 -07:00
Hari Govind V K
b8d8553c41
support or, and, implies, distinct in mbp_basic ( #6867 )
2023-08-20 15:36:22 -07:00
Nikolaj Bjorner
37ddaaef69
make destructors virtual
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-08-20 15:30:57 -07:00
Nuno Lopes
dda0c8ff42
array theory: use expr_ref for mk_default() so it doesnt leak if internalize throws
...
like on timeout/memout
2023-08-20 22:28:57 +01:00
Lev Nachmanson
9b672bc5cc
remove tracking of bounds
2023-08-20 10:10:48 -07:00
Nuno Lopes
57c667e355
remove unused code
2023-08-20 15:16:47 +01:00
Nuno Lopes
a694d27557
revert removal of virtual destructor of relevancy_eh since clang doesnt play along
2023-08-20 14:20:20 +01:00
Nuno Lopes
8210aafb69
ast compare_nodes: fail faster when comparing quantifier expressions
2023-08-20 14:09:04 +01:00
Nuno Lopes
c469c6e1d5
attempt to fix clang buildbots
2023-08-20 13:39:15 +01:00
Nuno Lopes
28884b398c
remove unneeded virtual destructor (optimization)
2023-08-20 12:57:47 +01:00