Copilot
2436943794
Standardize for-loop increments to prefix form (++i) ( #8199 )
...
* Initial plan
* Convert postfix to prefix increment in for loops
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Fix member variable increment conversion bug
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Update API generator to produce prefix increments
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
2026-01-14 19:55:31 -08:00
Nuno Lopes
499ed5d844
remove unneeded iterator functions
2024-09-23 12:59:04 +01:00
Nikolaj Bjorner
6366f8f6b2
na
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-08-13 14:05:07 -07:00
Nikolaj Bjorner
7cd8edce1f
perf and memory smash fixes to internal node count routine
2023-04-12 21:01:05 -07:00
Nikolaj Bjorner
e8222433c3
count internal nodes, use to block expanding use of hoist, #6683
2023-04-12 19:40:31 -07:00
Nikolaj Bjorner
efbe0a6554
wip - updated version of elim_uncstr_tactic
...
- remove reduce_invertible. It is subsumed by reduce_uncstr(2)
- introduce a simplifier for reduce_unconstrained. It uses reference counting to deal with inefficiency bug of legacy reduce_uncstr. It decomposes theory plugins into expr_inverter.
reduce_invertible is a tactic used in most built-in scenarios. It is useful for removing subterms that can be eliminated using "cheap" quantifier elimination. Specifically variables that occur only once can be removed in many cases by computing an expression that represents the effect computing a value for the eliminated occurrence.
The theory plugins for variable elimination are very partial and should be augmented by extensions, esp. for the case of bit-vectors where the invertibility conditions are thoroughly documented by Niemetz and Preiner.
2022-11-12 17:56:45 -08:00
Nikolaj Bjorner
6c12aaad74
wip - testing solve-eqs2, added as tactic
2022-11-05 22:42:59 -07:00
Nikolaj Bjorner
6f31d83633
fix #5541
2021-09-20 10:10:28 -07:00
Nikolaj Bjorner
4b6d7ca097
working on mam
2021-01-25 17:54:53 -08:00
Nikolaj Bjorner
c5432dbd88
merge
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-01-20 09:12:09 -08:00
Nuno Lopes
3a572edb9c
fix build
2021-01-20 10:42:29 +00:00
Nikolaj Bjorner
d0e20e44ff
booyah
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-07-04 15:56:30 -07:00
Nikolaj Bjorner
e5504247e9
use propagation filter
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-10-20 16:00:20 -07:00
Nikolaj Bjorner
68e4ed3c9c
fix #2531
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-09-02 09:59:58 -07:00
Nikolaj Bjorner
49279d7047
debugging mbi
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-14 16:08:52 -07:00
Nikolaj Bjorner
b19f94ae5b
make include paths uniformly use path relative to src. #534
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-31 13:24:11 -07:00
Nikolaj Bjorner
4bc044c982
update header guards to be C++ style. Fixes issue #9
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-07-08 23:18:40 -07:00
Leonardo de Moura
9a84cba6c9
Reorganizing the code. Moved nlsat to its own directory.
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-10-20 15:48:18 -07:00
