mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity
18831 commits 23 branches 48 tags 157 MiB
Commit graph

18831 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Nikolaj Bjorner
1c7ac12af8 wip 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-29 20:07:14 -08:00
Nikolaj Bjorner
f8a3e428ff wip 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-29 19:30:14 -08:00
Nikolaj Bjorner
96341d7f0a wip try_add_mul_bound2 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-29 18:31:39 -08:00
Nikolaj Bjorner
ed76da1458 Merge branch 'polysat' of https://github.com/z3prover/z3 into polysat 2022-12-29 16:55:56 -08:00
Nikolaj Bjorner
10589d59ba wip based on notes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-29 16:55:46 -08:00
Clemens Eisenhofer
6f78c33558 Generalized variable elimination 2022-12-29 22:36:04 +01: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
ab9a9d2308 wip - more general ranges for add_mul_bound 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-28 14:09:51 -08:00
Clemens Eisenhofer
658877365c Moved "easy part" of variable elimination to saturation.cpp 2022-12-28 15:07:03 +01:00
Nikolaj Bjorner
b4f5225ab3 outline 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-27 21:40:31 -08:00
Nikolaj Bjorner
6f8b3a997e add max forbidden based on constant intervals 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-27 20:49:17 -08:00
Nikolaj Bjorner
45e772b223 Merge branch 'polysat' of https://github.com/z3prover/z3 into polysat 2022-12-27 20:20:59 -08:00
Nikolaj Bjorner
b52379fe88 update 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-27 20:20:51 -08: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
Nikolaj Bjorner
3e8cbb6611 #5884 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-27 18:07:57 -08:00
Nikolaj Bjorner
abef260d67 Merge branch 'master' of https://github.com/z3prover/z3 2022-12-27 12:03:49 -08:00
Nikolaj Bjorner
bc19992543 add doc for ackermannize 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-27 12:02:08 -08:00
Clemens Eisenhofer
28e9014401 Merge branch 'polysat' of https://github.com/Z3Prover/z3 into polysat 2022-12-27 08:48:04 +01:00
Clemens Eisenhofer
4b8577eaa2 Reverted unintended changes 2022-12-27 08:47:27 +01:00
Clemens Eisenhofer
39a4bb025b Propagate assignment if all bits are assigned and use better justification if any found 2022-12-27 08:44:55 +01:00
Nikolaj Bjorner
8d332cc3a1
#6508 (#6509) 2022-12-26 15:42:04 -08:00
Nikolaj Bjorner
6fab4fec23
#6508 2022-12-26 15:36:58 -08:00
Nikolaj Bjorner
b9c4f5d4fa #6506 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-25 18:33:01 -08:00
Nikolaj Bjorner
8efaaaf249 Fix #6503 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-25 17:29:06 -08:00
Nikolaj Bjorner
67b9ecbd97 missing disequality parity constraint 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-25 16:13:26 -08:00
Nikolaj Bjorner
4c6499f28b updated notes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-25 15:28:34 -08:00
Nikolaj Bjorner
be5b6f2839 add analysis 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-25 15:14:40 -08:00
Nikolaj Bjorner
403a126642 remove try_factor_equality1 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-25 11:37:55 -08:00
Clemens Eisenhofer
52eefb6e85 Some more commenting 2022-12-25 12:51:13 +01:00
Clemens Eisenhofer
74ec28201e Merge remote-tracking branch 'Z3Prover/polysat' into polysat 2022-12-25 12:41:39 +01:00
Clemens Eisenhofer
674e309fa3 ... and backtracking for bits 2022-12-25 12:23:49 +01:00
Nikolaj Bjorner
49a7f8446d disable match_non_max and match_non_zero 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-24 15:19:37 -08:00
Nikolaj Bjorner
e978b81c7a add review comment to bug location 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-24 12:40:47 -08:00
Nikolaj Bjorner
48cd05c725 introduce try_factor_equality2, disabled as it exposes new bugs. Old bug on bench15.smt2 exposed in debug mode 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-24 12:05:54 -08:00
Clemens Eisenhofer
173fb9c2bd Bit-Propagation for most operations (Backtracking missing) 2022-12-24 16:37:53 +01:00
Nikolaj Bjorner
4e0604bc22 add hooks for multiplication overflow 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-23 15:48:03 -08:00
Nikolaj Bjorner
d18a2427a4 notes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-23 14:57:56 -08:00
Nikolaj Bjorner
50cbe2659a extract multiple bounds for upper/lower bound 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-23 14:52:41 -08:00
Nikolaj Bjorner
9275930f50 fix bug in add-overflow propagation, move to use viable to mind for bounds 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-23 13:38:51 -08:00
Nikolaj Bjorner
9fefa0040f added updated bounds propagation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-23 12:47:17 -08:00
Nikolaj Bjorner
6f8fb39bc9 added updated bounds propagation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-23 12:29:47 -08:00