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
Nikolaj Bjorner
1c7ff72ae2
add tactic doc
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-10 18:58:25 -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
e0099150ca
#6429
2023-01-04 15:28:57 -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
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
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
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
0d05e0649b
initialization order
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-12-30 18:16:24 -08:00
Nikolaj Bjorner
fe8034731d
fix #6501
2022-12-19 21:02:55 -08:00
Nikolaj Bjorner
e423fabf6a
tactic
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-12-15 20:35:36 -08:00
Nikolaj Bjorner
0768a2ead1
updated doc
2022-12-15 19:23:32 -08:00
Nikolaj Bjorner
13920c4772
more doc
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-12-15 11:42:02 -08:00
Nikolaj Bjorner
d5316e017e
add tactic descriptions
2022-12-14 20:38:28 -08:00
Nikolaj Bjorner
aed3d76a88
add doc
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-12-14 16:45:58 -08:00
Nikolaj Bjorner
7afcaa5364
update doc
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-12-12 18:56:21 -08:00
Nikolaj Bjorner
e648e68d36
add doc
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-12-12 17:29:58 -08:00
Nuno Lopes
d308b8f555
simplify code + remove unused file
2022-12-11 22:11:19 +00: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
Nikolaj Bjorner
96a2c04026
fix bug reported by Nuno
...
qhead should not be changed after tactic execution. It should remain 0 so the same tactic can be applied repeatedly on the entire state
2022-12-09 07:57:06 -08: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
c45c40e782
doc
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-12-07 08:51: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
aaabbfb594
remove comment that does not align with result
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-12-06 15:53:55 -08:00
Nikolaj Bjorner
d125d87aed
typo
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-12-06 15:51:42 -08:00
Nikolaj Bjorner
1e06c7414a
add doc
2022-12-06 15:44:21 -08:00
Nikolaj Bjorner
7df4e04a2c
add der description
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-12-06 05:46:52 -08:00
Nikolaj Bjorner
90ba225ae3
add more doc
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-12-06 05:39:05 -08:00
Nikolaj Bjorner
5a5758baaa
add documentation to initial selection of tactics
2022-12-05 20:05:06 -08:00
Nikolaj Bjorner
f1a65d9642
add documentation notes
2022-12-05 20:05:06 -08:00
Nuno Lopes
a2f5a5b50b
remove memory alloc from statistics_report
2022-12-05 14:29:14 +00: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
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
e455897178
fix #6476
2022-12-04 04:36:06 -08:00
Nikolaj Bjorner
59fa8964ca
minor code cleanup
2022-12-04 03:53:31 -08:00
Nikolaj Bjorner
cfc8e19baf
add more simplifiers, fix model reconstruction order for elim_unconstrained
...
- enable sat.smt in smt_tactic that
is invoked by default on first goals
add flatten-clauses
add push-ite
have tptp5 front-end pretty print SMT2 formulas a little nicer.
2022-12-01 02:35:43 +09:00
Nikolaj Bjorner
bec3acd146
consolidate freeze functionality into dependent_expr_state
...
rename size() to qtail() and introduce shortcuts
ensure tactic goals are not updated if they are in inconsistent state (because indices could be invalidated)
2022-11-30 08:35:29 +07:00
