Nikolaj Bjorner
05957803a3
update release notes for 12.2
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-19 20:25:30 -08:00
Nikolaj Bjorner
f3d6856736
remove msf example, add option to make model converter not reduce models
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-19 20:24:31 -08:00
Nikolaj Bjorner
d11e5c8ca6
address compiler warnings, and user question #6544
2023-01-19 19:02:43 -08:00
Nikolaj Bjorner
523a3f34b0
change to manylinux2014 in setup.py
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-19 17:27:07 -08:00
Nikolaj Bjorner
59c41bd8ce
increment release version
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-18 07:59:47 -08:00
Nikolaj Bjorner
9290de8223
make euf-egraph resilient to when there are no consumers to literal propagation.
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-18 07:57:19 -08:00
Nikolaj Bjorner
3012293c35
update release script
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-17 19:10:26 -08:00
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