Nikolaj Bjorner
fcc1bb5da8
updated release notes
2023-01-17 14:08:41 -08:00
Nikolaj Bjorner
7368f9f7d3
increase build version, better propagation in euf-egraph, handle assumptions in sat.smt
...
- increase build version to 4.12.1. This prepares updated release for MacOs-11 build on x86
- move literal propagation mode in euf-egraph to a callback and traversal of equivalence class. Track antecedent by newest equality instead of root. This makes equality propagation to literals have similar behavior as in legacy solver and appears to result in a speedup (10% fewer conflicts on QF_UF/QG-classification/qg5/iso_icl478.smt2 in preliminary testing)
- fix interaction of pre-processing and assumptions. Pre-processing has to freeze assumption literals so they don't get eliminated. This is similar to dependencies that are already frozen.
2023-01-17 14:07:07 -08:00
Nikolaj Bjorner
c8f197d0ca
specify macos-11 in nightly to force os11 build
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-16 16:30:46 -05:00
Nikolaj Bjorner
dde5218b29
fix mbqi value caching issue raised by Clemens and Martin
2023-01-15 22:47:34 -05:00
Nikolaj Bjorner
d5fde2e578
#6538
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-15 15:58:29 -05:00
Nikolaj Bjorner
4f7f4376b8
fix bug in new core not detecting conflict, fix #6525 , add tactic doc
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-14 17:20:43 -05:00
Nikolaj Bjorner
feda706d0d
Update release.yml for Azure Pipelines
2023-01-14 06:24:26 -08:00
Nikolaj Bjorner
5dbd0bb658
add sign
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-13 23:33:39 -08:00
Nikolaj Bjorner
54524de784
Update release.yml for Azure Pipelines
2023-01-13 17:10:36 -08:00
Nikolaj Bjorner
c33b1e3082
fixup manylinux reference in release script
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-13 16:27:58 -08:00
Nikolaj Bjorner
234ff28d18
prepare release script
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-13 16:15:27 -08:00
Nikolaj Bjorner
f1805138e7
missing code signing
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-13 16:13:20 -08:00
Nikolaj Bjorner
60fef928cc
missing code signing
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-13 16:12:48 -08:00
Nikolaj Bjorner
42fbf23a8f
update code signing
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-13 14:01:18 -08:00
Nikolaj Bjorner
d289434b65
fix #6535
2023-01-12 19:06:30 -08:00
Nikolaj Bjorner
0d46787fcf
update readme
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-12 17:58:23 -08:00
Nikolaj Bjorner
d204413f2a
remove update
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-12 17:54:42 -08:00
Nikolaj Bjorner
85abbb8188
include apt-get update for doc build
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-12 16:58:42 -08:00
Nikolaj Bjorner
e4bd406675
update version of manylinux
2023-01-12 16:27:33 -08:00
Nikolaj Bjorner
25b0b1430c
move bound_manager to simplifiers, add bound manager to extract_eqs for solve-eqs #6532
2023-01-12 12:42:28 -08:00
Jerry James
e5e16268cc
Initialize m_istamp_id in lookahead::init ( #6533 )
2023-01-12 11:20:28 -08:00
Nikolaj Bjorner
8970a54eaa
expose parameters to control behavior for #5660
2023-01-10 22:06:19 -08:00
Nikolaj Bjorner
1c7ff72ae2
add tactic doc
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-10 18:58:25 -08:00
Nikolaj Bjorner
d415f07386
memory leak on proof justifications
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-10 18:58:25 -08:00
Nikolaj Bjorner
b700dbffce
fix #6528
2023-01-10 14:42:23 -08:00
Brecht Sanders
2bd933d87f
Fix hwf.cpp for MinGW-w64 32-bit clang ( #6529 )
...
Fix src/util/hwf.cpp for building with MinGW-w64 clang targetting Windows 32-bit.
Without this fix there is an arror about `__control87_2` not being defined.
2023-01-10 13:44:11 -08:00
Nikolaj Bjorner
c3e31149a5
fix #6530
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-10 13:43:17 -08:00
Nikolaj Bjorner
a4d4e2e483
track assertions
2023-01-09 15:18:33 -08:00
Nikolaj Bjorner
64ec8acd30
fix model reconstruction ordering for elim_unconstrained
2023-01-09 15:18:19 -08:00
Nikolaj Bjorner
30e0f78c16
remove exit
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-09 10:00:36 -08:00
dependabot[bot]
a4f2a1bb2e
Bump json5 from 2.2.1 to 2.2.3 in /src/api/js ( #6527 )
...
Bumps [json5](https://github.com/json5/json5 ) from 2.2.1 to 2.2.3.
- [Release notes](https://github.com/json5/json5/releases )
- [Changelog](https://github.com/json5/json5/blob/main/CHANGELOG.md )
- [Commits](https://github.com/json5/json5/compare/v2.2.1...v2.2.3 )
---
updated-dependencies:
- dependency-name: json5
dependency-type: indirect
...
Signed-off-by: dependabot[bot] <support@github.com>
2023-01-09 09:16:55 +00:00
Nikolaj Bjorner
49ee570b09
split into separate function
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-08 19:16:46 -08:00
Nuno Lopes
5899fe3cea
Add rewrite for array selects of chain of stores of a same value ( #6526 )
...
* Add rewrite for array selects of chain of stores of a same value
Example:
```smt
(declare-fun mem () (Array (_ BitVec 4) (_ BitVec 4)))
(declare-const x (_ BitVec 4))
(declare-const y (_ BitVec 4))
; simplifies to #x1
(simplify (select (store (store (store mem #x1 #x1) y #x1) x #x1) #x1))
```
* Update array_rewriter.cpp
* Update array_rewriter.cpp
2023-01-08 19:09:01 -08:00
Nikolaj Bjorner
1ddef117a2
several fixes to proof logging in legacy solver
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-08 16:11:31 -08:00
Nikolaj Bjorner
61b90e64b2
disable new simplifcation for multiplier until really understood
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-08 14:17:49 -08:00
Nikolaj Bjorner
fcea32344e
add missing tactic descriptions, add rewrite for tamagochi
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-08 13:32:26 -08:00
Nikolaj Bjorner
95cb06d8cf
add quasi macro detection
2023-01-06 19:53:55 -08:00
Nikolaj Bjorner
25112e47b4
bugfix to flatten-clases simplifier
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-05 20:59:28 -08:00
Nikolaj Bjorner
c07b6ab38f
more tactic descriptions
2023-01-05 20:23:01 -08:00
Nikolaj Bjorner
0d8a472aac
pass sign into literal definition for pbge
2023-01-04 16:55:44 -08:00
Nikolaj Bjorner
81ce57b5a8
#6429
2023-01-04 15:38:13 -08:00
Nikolaj Bjorner
e0099150ca
#6429
2023-01-04 15:28:57 -08:00
Nikolaj Bjorner
380c701cbe
restore debug clang/gcc build
2023-01-04 15:01:40 -08:00
Nikolaj Bjorner
21362c0b98
make case-def and recfun-num-rounds re-parsable for logging
2023-01-04 15:00:25 -08:00
Nikolaj Bjorner
ef10119005
#6429 fixes
2023-01-04 13:05:45 -08:00
Nikolaj Bjorner
aa080a6b19
update ignore-int handling #6429
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-04 12:22:38 -08:00
Nikolaj Bjorner
8d0d6d8f04
Merge branch 'master' of https://github.com/z3prover/z3
2023-01-04 11:56:38 -08:00
Nikolaj Bjorner
6f95c77023
fix bugs in flatten_clauses simplifier, switch proof/fml
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-04 11:56:28 -08:00
Nuno Lopes
e448191212
array rewriter: expand select of store with const array into an ite
...
This:
(simplify (select (store ((as const (Array (_ BitVec 4) (_ BitVec 4))) #x0) x #x1) y))
=>
(ite (= x y) #x1 #x0)
2023-01-03 11:08:57 +00:00
Nuno Lopes
e508ef17f6
fix Alive bug #875 : bit blaster not respecting soft memory limit
2023-01-03 10:39:28 +00:00