mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-27 05:26:01 +00:00
Code Activity
17442 commits 64 branches 52 tags 178 MiB
Commit graph

2863 commits

Author SHA1 Message Date
Nikolaj Bjorner
21362c0b98 make case-def and recfun-num-rounds re-parsable for logging 2023-01-04 15:00:25 -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
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
5f6f2fc758 rename bit_blaster class to bit_blaster_simplifier to avoid name clash 2022-12-30 18:39:02 -08:00
Nikolaj Bjorner
2c3ecceb03 fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-30 15:47:24 -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
b9c4f5d4fa #6506 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-25 18:33:01 -08:00
Nikolaj Bjorner
fe8034731d fix #6501 2022-12-19 21:02:55 -08:00
Nikolaj Bjorner
ecf25a4fe2 outline scheme 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-15 14:57:52 -08:00
Nikolaj Bjorner
2d7a38e95e fix #6488 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-13 16:07:41 -08:00
Nikolaj Bjorner
aded8e5bf4 fix #6488 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-12 11:40:59 -08:00
Nikolaj Bjorner
4598af70c8 fix #6488 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-12 11:04:46 -08:00
Nikolaj Bjorner
a3e6885680 fix #6488 2022-12-12 09:50:44 -08:00
Nikolaj Bjorner
039de6a2c8 build issues 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-11 15:05:13 -08:00
Nuno Lopes
cb8603177e fix build 2022-12-11 22:17:11 +00:00
Nuno Lopes
d308b8f555 simplify code + remove unused file 2022-12-11 22:11:19 +00:00
Nikolaj Bjorner
2520dcb04b merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-11 14:03:22 -08:00
Nuno Lopes
2d43ccc4c6 Revert "fix crashes in elim-uncnstr2" 
This reverts commit a302c2f15e.
 2022-12-11 21:37:25 +00:00
Nikolaj Bjorner
6a1b3f7344 move debug output to before state update 2022-12-11 12:51:46 -08:00
Nikolaj Bjorner
f7269bb60a update doc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-11 10:16:17 -08:00
Nikolaj Bjorner
a9f52b0069 doc fixes 2022-12-11 10:04:01 -08:00
Nikolaj Bjorner
527fb18366 add doc for card2bv 2022-12-11 09:51:49 -08:00
Nuno Lopes
a302c2f15e fix crashes in elim-uncnstr2 
This would crash before:
(declare-fun x () (_ BitVec 4))
(assert (not (bvule x #x1)))
(apply elim-uncnstr2)

That's because the index_set iterator was querying qtail to compute the end of the iteration
But the problem is that elim-uncnstr2 may add new fmls to the goal, as in this case.
The bvule is replaced with an 'or', but since it's negated, it turns into 2 goals
Solve the issue by freezing the qtail for the iteration loop.
This is the right behavior for elim-uncnstr2, as it can't rewrite exprs that haven't been analyzed before

@NikolajBjorner please check if this the right behavior for the other simplifiers. Thank you
 2022-12-11 15:21:23 +00:00
Nuno Lopes
c6f9c09d70 cleanup more in dependent_expr_state_tactic to reduce mem consumption 2022-12-09 11:34:53 +00:00
Nikolaj Bjorner
7e69dab8f6 distribute forall cpp code 2022-12-06 18:15:18 -08:00
Nikolaj Bjorner
c33e58ee1a update distribute forall 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-06 17:59:33 -08:00
Nikolaj Bjorner
80033e8744 cave in to supporting proofs (partially) in simplifiers, updated doc 2022-12-06 17:02:04 -08:00
Nikolaj Bjorner
5a5758baaa add documentation to initial selection of tactics 2022-12-05 20:05:06 -08:00
Nuno Lopes
eb8c53c164 simplify factory of dependent_expr_state_tactic 
And as a side-effect, remove heap allocations for factories
 2022-12-05 14:07:57 +00:00
Nikolaj Bjorner
de916f50d6 add demodulator tactic based on demodulator-simplifier 
- some handling for commutative operators
- fix bug in demodulator_index where fwd and bwd are swapped
 2022-12-05 03:20:46 -08:00
Nikolaj Bjorner
87095950cb fix #6477 2022-12-04 13:02:45 -08:00
Nikolaj Bjorner
ead2a46a88 build 2022-12-04 10:38:24 -08:00
Nikolaj Bjorner
b76ed6a47f proper fix to #6476 2022-12-04 10:19:39 -08:00
Nikolaj Bjorner
9b58135876 try to fix linux builds 2022-12-04 09:55:31 -08:00
Nikolaj Bjorner
0f7bebcbed try big M for linux build 2022-12-04 09:49:32 -08:00
Nikolaj Bjorner
1974c224ab add demodulator simplifier 
refactor demodulator-rewriter a bit to separate reusable features.
 2022-12-04 09:39:28 -08:00
Nikolaj Bjorner
9acbfa3923 move it into substitution to handle dependencies 2022-12-04 06:23:32 -08:00
Nikolaj Bjorner
3d7bd40a87 a round of cleanup 2022-12-04 06:07:45 -08:00
Nikolaj Bjorner
d218083145 The demodulator doesn't produce proofs so remove code path that depends it does. 2022-12-04 04:48:48 -08:00
Nikolaj Bjorner
7fe6787748 ufbv-rewriter is really a demodulator rewriter and does not reference ufbv 
so moving first the rewriter into place of other rewriters
 2022-12-04 04:44:02 -08:00
Nikolaj Bjorner
79e6d4e32d tune and debug elim-unconstrained (v2 - for simplifiers infrastructure) 2022-12-04 03:53:31 -08:00
Nikolaj Bjorner
3ebbb8472a fix perf bugs in new value propagation 2022-12-04 03:53:30 -08:00
Nikolaj Bjorner
758c3b2c3b fix filtering for recursive functions 2022-12-04 03:53:30 -08:00
Nikolaj Bjorner
cf7bba6288 use ast_manager as an attribute 2022-12-04 03:53:30 -08:00
Nikolaj Bjorner
5073959ae0 add macro attribute 2022-12-04 03:53:29 -08:00
Nikolaj Bjorner
a96b7d243a remove incorrect check for quantifier 2022-12-01 00:04:08 -08:00