Nikolaj Bjorner
87a839c794
fixup unit test for added argument to constructor of nla_solver
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-09-23 18:07:56 -07:00
Nikolaj Bjorner
010a994a97
Merge branch 'master' of https://github.com/z3prover/z3 into unit_prop_on_monomials
2023-09-23 17:25:35 -07: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
3433366bef
Merge branch 'unit_prop_on_monomials' of https://github.com/z3prover/z3 into unit_prop_on_monomials
2023-09-23 17:20:08 -07:00
Nikolaj Bjorner
85eacf9bb1
merge with master
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-09-23 17:20:00 -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
a3e2e68d93
Update theory_lra.cpp
2023-09-23 16:26:31 -07:00
Nikolaj Bjorner
acad9fa62c
Update smt_context.cpp
2023-09-23 16:25:46 -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
421fe94607
rmove debug out
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-09-22 17:59:07 -07:00
Nikolaj Bjorner
886d3f4351
indentation
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-09-22 16:55:34 -07:00
Nikolaj Bjorner
eac54ba084
indentation
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-09-22 16:54:12 -07:00
Nikolaj Bjorner
940775d12d
indentation
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-09-22 16:48:40 -07:00
Lev Nachmanson
caa929f01f
do not use lemmase in monomial propagation
2023-09-22 14:27:26 -07:00
Nikolaj Bjorner
5d8779b05d
Merge branch 'master' into unit_prop_on_monomials
2023-09-22 09:46:41 -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
Lev Nachmanson
576309a16f
Revert "reject rows with columns with big numbers for lp bound propagation"
...
This reverts commit c0b55d1435
.
2023-09-21 16:30:43 -07:00
Lev Nachmanson
c0b55d1435
reject rows with columns with big numbers for lp bound propagation
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2023-09-21 15:53:53 -07:00
Lev Nachmanson
f423642e9b
try the lemma scheme
2023-09-21 12:18:21 -07:00
Lev Nachmanson
e31cecf5db
transfer propagate monomial bounds to nla_solver
2023-09-21 11:27:53 -07:00
Lev Nachmanson
536930b4a1
make m_ibounds inside of lp_bound_propagator
...
a reference
2023-09-20 17:13:25 -07:00
Lev Nachmanson
20c02f4f45
fix a lambda bug
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2023-09-20 17:02:35 -07:00
Nikolaj Bjorner
f9de65a464
indetation
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-09-20 15:22:28 -07:00
Nikolaj Bjorner
615aad7779
get rid of int*, use lambda scoping
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-09-20 15:18:37 -07:00
Nikolaj Bjorner
7a74b099ba
remove experimental code
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-09-20 15:04:24 -07:00
Lev Nachmanson
24512d5ec2
typo
2023-09-20 14:12:36 -07:00
Lev Nachmanson
9648793206
add features to std_allocator
2023-09-20 14:11:38 -07:00
Lev Nachmanson
f2a0ddb385
Merge branch 'unit_prop_on_monomials' of https://github.com/z3prover/z3 into unit_prop_on_monomials
2023-09-19 15:47:01 -07:00
Lev Nachmanson
d77c91b1aa
trying to get else on a new line
...
with clang-formatter
2023-09-19 15:46:59 -07:00
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