Nuno Lopes
3586b613f7
remove default destructors
2024-10-02 22:20:12 +01:00
THE Spellchecker
dc0887db5a
Typo Fixes ( #6803 )
2023-07-09 11:56:10 -07:00
Nikolaj Bjorner
41b40c3a51
remove dead code
2022-11-19 18:45:07 +07:00
J Sailor
f5d2b9b89a
fix typo in comment defining macros ( #6306 )
...
The existing comment describes macros as "formulas of the form
`(forall X (= (f X) T[X]))` ... where `T[X]` does not contain `X`". This is
incorrect; of course the macros' definitions are allowed to be in terms of
the macros' arguments. The comment should say "...does not contain `f`" because
macros can't be recursive.
2022-08-28 17:49:52 -07:00
Nikolaj Bjorner
9eb4237dfe
fix #6292
...
this patches a case where macro-finder is used with arrays. It doesn't work so macro quantifiers have to be re-instated to ensure correctness
2022-08-21 16:32:01 -07:00
Nikolaj Bjorner
e6264a80ff
extend macro detection to negated equivalences #5496
2021-08-25 17:47:30 -07:00
Nikolaj Bjorner
d0e20e44ff
booyah
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-07-04 15:56:30 -07:00
Nikolaj Bjorner
68f1f1e62f
fix #4162
2020-04-30 10:22:46 -07:00
Nikolaj Bjorner
fdabaa6cd2
fix #3807
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-10 13:43:00 -07:00
Nikolaj Bjorner
37f080b877
fix #3523
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-26 09:44:00 -07:00
Bruce Mitchener
76eb7b9ede
Use nullptr.
2018-02-12 14:05:55 +07:00
Nikolaj Bjorner
0d5cfe9292
separate out, add copy constructor
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-08-26 09:23:15 -07:00
Nikolaj Bjorner
c03be16039
merge
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-08-26 01:33:19 -07:00
Nikolaj Bjorner
881f90d17d
remove simplify dependencies
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-08-26 00:48:49 -07:00
Nikolaj Bjorner
ebcacaa26d
update new assertions
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-08-25 17:44:33 -07:00
Christoph M. Wintersteiger
b8a81bcb09
Added unsat core support to the macro-finder.
2017-08-25 20:21:57 +01:00
Christoph M. Wintersteiger
ed4477c9e4
Whitespace
2017-08-24 18:32:50 +01:00
Nikolaj Bjorner
655b3d9c19
removing dependency on simplifier in pattern_inference
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-08-23 12:17:30 -07:00
Nikolaj Bjorner
ce04c18a7a
trying to get rid of last simplifier dependency in macros
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-08-22 22:14:13 -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
0a4446ae26
reorganizing the code
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-10-23 22:14:35 -07:00
