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

17467 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Nikolaj Bjorner 2c3ecceb03 fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-30 15:47:24 -08:00
nikswamy 8002a51b82
tiny fix to qprofdiff (#6497) 2022-12-30 15:25:01 -08:00
Nikolaj Bjorner 293627c889 fix #6513 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-30 09:55:33 -08:00
Nikolaj Bjorner 07ab4d38b6 fix #6513 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-30 09:55:10 -08:00
Nuno Lopes 47324af210 be nicer when memout is reached in SMT internalize: return undef rather than crashing 2022-12-29 11:08:57 +00:00
Nikolaj Bjorner 7cc58c9cc3 Merge branch 'master' of https://github.com/z3prover/z3 2022-12-27 20:19:39 -08:00
Nikolaj Bjorner ec74a87423 fix #6510 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-27 20:19:26 -08:00