Nikolaj Bjorner
|
e9f45695c1
|
fix #3443 - some properties checked by invariant isn't valid during destructor when using threads
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-22 10:57:22 -07:00 |
|
Nikolaj Bjorner
|
945cd3169e
|
fix #3440
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-22 10:43:52 -07:00 |
|
Nikolaj Bjorner
|
cd434d8bd5
|
fix #3420
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-19 17:49:48 -07:00 |
|
Nikolaj Bjorner
|
24dd047892
|
fix #3397, use it or lose it
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-18 11:06:19 -07:00 |
|
Nikolaj Bjorner
|
e7ec842cf5
|
fix #3348
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-16 12:14:19 -07:00 |
|
Nikolaj Bjorner
|
0768701744
|
fix #3220
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-10 16:08:16 -07:00 |
|
Nikolaj Bjorner
|
3d7098ec85
|
fix #3137
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-09 07:15:06 +01:00 |
|
Nikolaj Bjorner
|
7d976e4f4d
|
fix #3120
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-06 06:52:38 +01:00 |
|
Nikolaj Bjorner
|
bba2cf9f20
|
fix #3163
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-06 06:31:44 +01:00 |
|
Nikolaj Bjorner
|
bd3024e837
|
fix #3161
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-05 17:37:38 +01:00 |
|
Nikolaj Bjorner
|
6b0e599b88
|
fix #3140
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-05 11:22:13 +01:00 |
|
Nikolaj Bjorner
|
7d73069798
|
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-05 10:36:24 +01:00 |
|
Nikolaj Bjorner
|
8b0d540cca
|
fix #3148
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-05 10:35:24 +01:00 |
|
Nikolaj Bjorner
|
76d91f7d2b
|
fix #3142
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-04 14:27:32 -08:00 |
|
Nikolaj Bjorner
|
fcbf660592
|
fix #3133
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-03 19:29:15 -08:00 |
|
Nikolaj Bjorner
|
2989d9c241
|
fix #3124
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-03 12:39:25 -08:00 |
|
Nikolaj Bjorner
|
05158b3914
|
add cut redundancies
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-01 12:49:59 -08:00 |
|
Mathias Soeken
|
20c3f75740
|
No need to hash quaternaries for AND.
|
2020-03-01 04:10:25 -08:00 |
|
Nikolaj Bjorner
|
e8f7a08289
|
add stubs for npn3
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-27 21:19:40 -08:00 |
|
Mathias Soeken
|
595fea7434
|
Find AND and XOR clauses.
|
2020-02-27 11:13:24 -08:00 |
|
Mathias Soeken
|
0713d1cdb1
|
More finders.
|
2020-02-27 11:13:24 -08:00 |
|
Mathias Soeken
|
f3c8cae730
|
More finders.
|
2020-02-27 11:13:24 -08:00 |
|
Mathias Soeken
|
ec3f4929cf
|
Fewer checks necessary.
|
2020-02-27 11:13:24 -08:00 |
|
Mathias Soeken
|
34a3f8db6e
|
Gamble finder.
|
2020-02-27 11:13:24 -08:00 |
|
Mathias Soeken
|
0caa2f27a1
|
More finders.
|
2020-02-27 11:13:24 -08:00 |
|
Mathias Soeken
|
4d0519fe3c
|
Initial NPN3 finder with MUX and MAJ finder.
|
2020-02-27 11:13:24 -08:00 |
|
Nikolaj Bjorner
|
dc31478d82
|
detect conflicts in cut_simplifier
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-26 20:53:58 -08:00 |
|
Nikolaj Bjorner
|
4f3fbd3c11
|
align parity with signs
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-26 15:49:58 -08:00 |
|
Nikolaj Bjorner
|
dddd740846
|
make aig/ite extraction conditional
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-25 16:27:13 -08:00 |
|
Nikolaj Bjorner
|
39061d7388
|
disable unsound simplify, rename stats, delay region allocation for cutsets
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-25 12:40:16 -08:00 |
|
Nikolaj Bjorner
|
238ff78374
|
fix #3082
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-24 09:01:31 -08:00 |
|
Nikolaj Bjorner
|
5af139055d
|
fix #3079
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-23 09:45:05 -08:00 |
|
Nikolaj Bjorner
|
c71da17a10
|
add output for inprocessing
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-22 11:50:51 -08:00 |
|
Nikolaj Bjorner
|
d1e95a133b
|
add simplifiation pass
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-22 11:21:53 -08:00 |
|
Nikolaj Bjorner
|
dcd4fff284
|
fixes to cuts
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-21 18:06:57 -08:00 |
|
Nikolaj Bjorner
|
8b97e26fd7
|
cut fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-20 09:55:17 -08:00 |
|
Nikolaj Bjorner
|
3bb05b5e01
|
fix lut augment
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-19 18:36:28 -08:00 |
|
Nikolaj Bjorner
|
ff436ecb10
|
fix #3038 again
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-19 09:52:27 -08:00 |
|
Nikolaj Bjorner
|
a4d81b2847
|
fix #3045 fix #3046
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-19 09:52:26 -08:00 |
|
Mathias Soeken
|
290b4dfabc
|
More cases needed to find all ite clauses.
|
2020-02-19 09:03:58 -08:00 |
|
Mathias Soeken
|
00e43b6b88
|
Constructor compares arguments, not member variables.
|
2020-02-19 07:00:37 -08:00 |
|
Mathias Soeken
|
b464cf26bc
|
Passing functor by const-reference allows to use lambdas as arguments.
|
2020-02-19 07:00:37 -08:00 |
|
Nikolaj Bjorner
|
44a79d05c8
|
debugging cuts
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-19 06:45:23 -08:00 |
|
Nikolaj Bjorner
|
cc2cd5b557
|
fix #3041
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-18 22:57:30 -08:00 |
|
Nikolaj Bjorner
|
dd3e77107e
|
rename aig_simplifier to cut_simplifier
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-18 18:29:59 -08:00 |
|
Nikolaj Bjorner
|
8860de39bb
|
ull
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-18 18:08:11 -08:00 |
|
Nikolaj Bjorner
|
e016979ff6
|
ull
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-18 18:07:18 -08:00 |
|
Nikolaj Bjorner
|
c428db0bf2
|
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-18 14:51:58 -08:00 |
|
Nikolaj Bjorner
|
559c3ca012
|
fix #3035
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-18 10:46:25 -10:00 |
|
Nikolaj Bjorner
|
1ce0d7512a
|
fix #2974 by using same code path as qe. It now diverges, but this is due to the use of an uninterpreted predicate which the use of mbp doesn't handle
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-13 20:20:08 -08:00 |
|