mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity
17474 commits 23 branches 48 tags 156 MiB
Commit graph

17474 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
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
Nikolaj Bjorner c0f1f33898 dampen second setup of theory_bv 2022-12-30 18:47:32 -08:00
Nikolaj Bjorner 5f6f2fc758 rename bit_blaster class to bit_blaster_simplifier to avoid name clash 2022-12-30 18:39:02 -08:00
Nikolaj Bjorner 0d05e0649b initialization order 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-30 18:16:24 -08:00