mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity
17813 commits 24 branches 48 tags 158 MiB
Commit graph

15076 commits

Author SHA1 Message Date
Nikolaj Bjorner
0f4f32c5d0 apply relevancy filtering on unsupported ops, fix term construction bug in bv2fpa_converter fix #6548 2023-01-20 13:05:01 -08:00
Nuno Lopes
37652e7e17 fix tactic name in docs 2023-01-20 17:30:40 +00: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
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
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
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
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
d289434b65 fix #6535 2023-01-12 19:06:30 -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
Nuno Lopes
a2cc504d4a remove a couple more std::endl 2023-01-03 09:49:58 +00:00
Nuno Lopes
d30cb55bae don't flush stream when printing param vals 2023-01-03 09:35:17 +00:00
Nikolaj Bjorner
d4490738bc Merge branch 'master' of https://github.com/z3prover/z3 2023-01-02 16:49:43 -08:00
Nikolaj Bjorner
ea0d09b6c8 add pointer to build parameters to README #6518 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-02 16:49:31 -08:00
Walden Yan
dbf93c5fbd
Fixing array select for lambda expressions in Python API (#6516) 
* fix: making array select work for lambda expressions

* more elegant solution
 2023-01-01 15:27:54 -08:00
Nikolaj Bjorner
f6d411d54b experimental feature to access congruence closure of SimpleSolver 
This update includes an experimental feature to access a congruence closure data-structure after search.
It comes with several caveats as pre-processing is free to eliminate terms. It is therefore necessary to use a solver that does not eliminate the terms you want to track for congruence of. This is partially addressed by using SimpleSolver or incremental mode solving.

```python
from z3 import *
s = SimpleSolver()
x, y, z = Ints('x y z')
s.add(x == y)
s.add(y == z)
s.check()
print(s.root(x), s.root(y), s.root(z))
print(s.next(x), s.next(y), s.next(z))
```
 2022-12-30 21:41:27 -08:00