summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2013-07-13 23:40:51 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2013-07-13 23:40:51 -0700
commitb3e0f5b2e94e5e0da72e1ec7a41f90a3f4d302d7 (patch)
treec4f8f72566b20bb3a20a296a5af2e94b4df58132
parent118e40b809712c88fe7ddc530a8b072c1d2649d3 (diff)
downloadabc-b3e0f5b2e94e5e0da72e1ec7a41f90a3f4d302d7.tar.gz
abc-b3e0f5b2e94e5e0da72e1ec7a41f90a3f4d302d7.tar.bz2
abc-b3e0f5b2e94e5e0da72e1ec7a41f90a3f4d302d7.zip
New technology mapper.
Diffstat
-rw-r--r--src/base/abci/abc.c11
-rw-r--r--src/map/mpm/mpm.h1
-rw-r--r--src/map/mpm/mpmAbc.c8
-rw-r--r--src/map/mpm/mpmCore.c1
-rw-r--r--src/map/mpm/mpmDsd.c931
-rw-r--r--src/map/mpm/mpmInt.h32
-rw-r--r--src/map/mpm/mpmMan.c28
-rw-r--r--src/map/mpm/mpmMap.c110
-rw-r--r--src/map/mpm/mpmPre.c77
-rw-r--r--src/map/mpm/mpmTruth.c4
-rw-r--r--src/misc/vec/vecHsh.h15
11 files changed, 1106 insertions, 112 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 3ccd88e7..373db069 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -29522,7 +29522,7 @@ int Abc_CommandAbc9If2( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
Mpm_ManSetParsDefault( pPars );
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "KDtmzvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "KDtmzvwh" ) ) != EOF )
{
switch ( c )
{
@@ -29565,6 +29565,9 @@ int Abc_CommandAbc9If2( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'v':
pPars->fVerbose ^= 1;
break;
+ case 'w':
+ pPars->fVeryVerbose ^= 1;
+ break;
case 'h':
default:
goto usage;
@@ -29573,7 +29576,8 @@ int Abc_CommandAbc9If2( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->pLib == NULL )
pPars->pLib = Mpm_LibLutSetSimple( nLutSize );
if ( pPars->fCutMin )
- pPars->fUseTruth = 1;
+// pPars->fUseTruth = 1;
+ pPars->fUseDsd = 1;
// perform mapping
pNew = Mpm_ManMappingTest( pAbc->pGia, pPars );
Mpm_LibLutFree( pPars->pLib );
@@ -29590,7 +29594,7 @@ usage:
sprintf(Buffer, "best possible" );
else
sprintf(Buffer, "%d", pPars->DelayTarget );
- Abc_Print( -2, "usage: &if2 [-KD num] [-tmzvh]\n" );
+ Abc_Print( -2, "usage: &if2 [-KD num] [-tmzvwh]\n" );
Abc_Print( -2, "\t performs technology mapping of the network\n" );
Abc_Print( -2, "\t-K num : sets the LUT size for the mapping [default = %d]\n", nLutSize );
Abc_Print( -2, "\t-D num : sets the delay constraint for the mapping [default = %s]\n", Buffer );
@@ -29598,6 +29602,7 @@ usage:
Abc_Print( -2, "\t-m : enables cut minimization by removing vacuous variables [default = %s]\n", pPars->fCutMin? "yes": "no" );
Abc_Print( -2, "\t-z : toggles deriving LUTs when mapping into LUT structures [default = %s]\n", pPars->fDeriveLuts? "yes": "no" );
Abc_Print( -2, "\t-v : toggles verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-w : toggles very verbose output [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : prints the command usage\n");
return 1;
}
diff --git a/src/map/mpm/mpm.h b/src/map/mpm/mpm.h
index 9e9c116d..8008c965 100644
--- a/src/map/mpm/mpm.h
+++ b/src/map/mpm/mpm.h
@@ -65,6 +65,7 @@ struct Mpm_Par_t_
int fCutMin;
int fDeriveLuts;
int fVerbose;
+ int fVeryVerbose;
};
////////////////////////////////////////////////////////////////////////
diff --git a/src/map/mpm/mpmAbc.c b/src/map/mpm/mpmAbc.c
index 4824f08d..8ae7645a 100644
--- a/src/map/mpm/mpmAbc.c
+++ b/src/map/mpm/mpmAbc.c
@@ -183,6 +183,7 @@ void * Mpm_ManFromIfLogic( Mpm_Man_t * pMan )
Mig_Obj_t * pObj, * pFanin;
Vec_Int_t * vMapping, * vMapping2, * vPacking = NULL;
Vec_Int_t * vLeaves, * vLeaves2, * vCover;
+ word uTruth, * pTruth = &uTruth;
int i, k, Entry, iLitNew;
// assert( !pMan->pPars->fDeriveLuts || pMan->pPars->fTruth );
// start mapping and packing
@@ -211,11 +212,14 @@ void * Mpm_ManFromIfLogic( Mpm_Man_t * pMan )
pCutBest = Mpm_ObjCutBestP( pMan, pObj );
Mpm_CutForEachLeaf( pMan->pMig, pCutBest, pFanin, k )
Vec_IntPush( vLeaves, Mig_ObjCopy(pFanin) );
- if ( pMan->pPars->fDeriveLuts && pMan->pPars->fUseTruth )
+ if ( pMan->pPars->fDeriveLuts && (pMan->pPars->fUseTruth || pMan->pPars->fUseDsd) )
{
extern int Gia_ManFromIfLogicNode( Gia_Man_t * pNew, int iObj, Vec_Int_t * vLeaves, Vec_Int_t * vLeavesTemp,
word * pRes, char * pStr, Vec_Int_t * vCover, Vec_Int_t * vMapping, Vec_Int_t * vMapping2, Vec_Int_t * vPacking );
- word * pTruth = Mpm_CutTruth(pMan, Abc_Lit2Var(pCutBest->iFunc));
+ if ( pMan->pPars->fUseTruth )
+ pTruth = Mpm_CutTruth(pMan, Abc_Lit2Var(pCutBest->iFunc));
+ else
+ uTruth = Mpm_CutTruthFromDsd( pMan, pCutBest, Abc_Lit2Var(pCutBest->iFunc) );
// Kit_DsdPrintFromTruth( pTruth, Vec_IntSize(vLeaves) ); printf( "\n" );
// perform decomposition of the cut
iLitNew = Gia_ManFromIfLogicNode( pNew, Mig_ObjId(pObj), vLeaves, vLeaves2, pTruth, NULL, vCover, vMapping, vMapping2, vPacking );
diff --git a/src/map/mpm/mpmCore.c b/src/map/mpm/mpmCore.c
index a6edba8f..3bb0eeb2 100644
--- a/src/map/mpm/mpmCore.c
+++ b/src/map/mpm/mpmCore.c
@@ -54,6 +54,7 @@ void Mpm_ManSetParsDefault( Mpm_Par_t * p )
p->DelayTarget = -1; // delay target
p->fDeriveLuts = 0; // use truth tables to derive AIG structure
p->fVerbose = 0; // verbose output
+ p->fVeryVerbose = 0; // verbose output
}
/**Function*************************************************************
diff --git a/src/map/mpm/mpmDsd.c b/src/map/mpm/mpmDsd.c
index 0cff45af..2a45d684 100644
--- a/src/map/mpm/mpmDsd.c
+++ b/src/map/mpm/mpmDsd.c
@@ -19,14 +19,613 @@
***********************************************************************/
#include "mpmInt.h"
+#include "misc/extra/extra.h"
+#include "misc/util/utilTruth.h"
ABC_NAMESPACE_IMPL_START
-
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
+static Mpm_Dsd_t s_DsdClass6[595] = {
+ { 0, ABC_CONST(0x0000000000000000), "0" }, // 0
+ { 1, ABC_CONST(0xAAAAAAAAAAAAAAAA), "a" }, // 1
+ { 2, ABC_CONST(0x8888888888888888), "(ab)" }, // 2
+ { 2, ABC_CONST(0x6666666666666666), "[ab]" }, // 3
+ { 3, ABC_CONST(0x8080808080808080), "(abc)" }, // 4
+ { 3, ABC_CONST(0x7070707070707070), "(!(ab)c)" }, // 5
+ { 3, ABC_CONST(0x7878787878787878), "[(ab)c]" }, // 6
+ { 3, ABC_CONST(0x6060606060606060), "([ab]c)" }, // 7
+ { 3, ABC_CONST(0x9696969696969696), "[abc]" }, // 8
+ { 3, ABC_CONST(0xCACACACACACACACA), "<abc>" }, // 9
+ { 4, ABC_CONST(0x8000800080008000), "(abcd)" }, // 10
+ { 4, ABC_CONST(0x7F007F007F007F00), "(!(abc)d)" }, // 11
+ { 4, ABC_CONST(0x7F807F807F807F80), "[(abc)d]" }, // 12
+ { 4, ABC_CONST(0x7000700070007000), "(!(ab)cd)" }, // 13
+ { 4, ABC_CONST(0x8F008F008F008F00), "(!(!(ab)c)d)" }, // 14
+ { 4, ABC_CONST(0x8F708F708F708F70), "[(!(ab)c)d]" }, // 15
+ { 4, ABC_CONST(0x7800780078007800), "([(ab)c]d)" }, // 16
+ { 4, ABC_CONST(0x8778877887788778), "[(ab)cd]" }, // 17
+ { 4, ABC_CONST(0x6000600060006000), "([ab]cd)" }, // 18
+ { 4, ABC_CONST(0x9F009F009F009F00), "(!([ab]c)d)" }, // 19
+ { 4, ABC_CONST(0x9F609F609F609F60), "[([ab]c)d]" }, // 20
+ { 4, ABC_CONST(0x9600960096009600), "([abc]d)" }, // 21
+ { 4, ABC_CONST(0x6996699669966996), "[abcd]" }, // 22
+ { 4, ABC_CONST(0xCA00CA00CA00CA00), "(<abc>d)" }, // 23
+ { 4, ABC_CONST(0x35CA35CA35CA35CA), "[<abc>d]" }, // 24
+ { 4, ABC_CONST(0x0777077707770777), "(!(ab)!(cd))" }, // 25
+ { 4, ABC_CONST(0x7888788878887888), "[(ab)(cd)]" }, // 26
+ { 4, ABC_CONST(0x0666066606660666), "([ab]!(cd))" }, // 27
+ { 4, ABC_CONST(0x0660066006600660), "([ab][cd])" }, // 28
+ { 4, ABC_CONST(0xCAAACAAACAAACAAA), "<ab(cd)>" }, // 29
+ { 4, ABC_CONST(0xACCAACCAACCAACCA), "<ab[cd]>" }, // 30
+ { 4, ABC_CONST(0xF088F088F088F088), "<(ab)cd>" }, // 31
+ { 4, ABC_CONST(0xF066F066F066F066), "<[ab]cd>" }, // 32
+ { 5, ABC_CONST(0x8000000080000000), "(abcde)" }, // 33
+ { 5, ABC_CONST(0x7FFF00007FFF0000), "(!(abcd)e)" }, // 34
+ { 5, ABC_CONST(0x7FFF80007FFF8000), "[(abcd)e]" }, // 35
+ { 5, ABC_CONST(0x7F0000007F000000), "(!(abc)de)" }, // 36
+ { 5, ABC_CONST(0x80FF000080FF0000), "(!(!(abc)d)e)" }, // 37
+ { 5, ABC_CONST(0x80FF7F0080FF7F00), "[(!(abc)d)e]" }, // 38
+ { 5, ABC_CONST(0x7F8000007F800000), "([(abc)d]e)" }, // 39
+ { 5, ABC_CONST(0x807F7F80807F7F80), "[(abc)de]" }, // 40
+ { 5, ABC_CONST(0x7000000070000000), "(!(ab)cde)" }, // 41
+ { 5, ABC_CONST(0x8FFF00008FFF0000), "(!(!(ab)cd)e)" }, // 42
+ { 5, ABC_CONST(0x8FFF70008FFF7000), "[(!(ab)cd)e]" }, // 43
+ { 5, ABC_CONST(0x8F0000008F000000), "(!(!(ab)c)de)" }, // 44
+ { 5, ABC_CONST(0x70FF000070FF0000), "(!(!(!(ab)c)d)e)" }, // 45
+ { 5, ABC_CONST(0x70FF8F0070FF8F00), "[(!(!(ab)c)d)e]" }, // 46
+ { 5, ABC_CONST(0x8F7000008F700000), "([(!(ab)c)d]e)" }, // 47
+ { 5, ABC_CONST(0x708F8F70708F8F70), "[(!(ab)c)de]" }, // 48
+ { 5, ABC_CONST(0x7800000078000000), "([(ab)c]de)" }, // 49
+ { 5, ABC_CONST(0x87FF000087FF0000), "(!([(ab)c]d)e)" }, // 50
+ { 5, ABC_CONST(0x87FF780087FF7800), "[([(ab)c]d)e]" }, // 51
+ { 5, ABC_CONST(0x8778000087780000), "([(ab)cd]e)" }, // 52
+ { 5, ABC_CONST(0x7887877878878778), "[(ab)cde]" }, // 53
+ { 5, ABC_CONST(0x6000000060000000), "([ab]cde)" }, // 54
+ { 5, ABC_CONST(0x9FFF00009FFF0000), "(!([ab]cd)e)" }, // 55
+ { 5, ABC_CONST(0x9FFF60009FFF6000), "[([ab]cd)e]" }, // 56
+ { 5, ABC_CONST(0x9F0000009F000000), "(!([ab]c)de)" }, // 57
+ { 5, ABC_CONST(0x60FF000060FF0000), "(!(!([ab]c)d)e)" }, // 58
+ { 5, ABC_CONST(0x60FF9F0060FF9F00), "[(!([ab]c)d)e]" }, // 59
+ { 5, ABC_CONST(0x9F6000009F600000), "([([ab]c)d]e)" }, // 60
+ { 5, ABC_CONST(0x609F9F60609F9F60), "[([ab]c)de]" }, // 61
+ { 5, ABC_CONST(0x9600000096000000), "([abc]de)" }, // 62
+ { 5, ABC_CONST(0x69FF000069FF0000), "(!([abc]d)e)" }, // 63
+ { 5, ABC_CONST(0x69FF960069FF9600), "[([abc]d)e]" }, // 64
+ { 5, ABC_CONST(0x6996000069960000), "([abcd]e)" }, // 65
+ { 5, ABC_CONST(0x9669699696696996), "[abcde]" }, // 66
+ { 5, ABC_CONST(0xCA000000CA000000), "(<abc>de)" }, // 67
+ { 5, ABC_CONST(0x35FF000035FF0000), "(!(<abc>d)e)" }, // 68
+ { 5, ABC_CONST(0x35FFCA0035FFCA00), "[(<abc>d)e]" }, // 69
+ { 5, ABC_CONST(0x35CA000035CA0000), "([<abc>d]e)" }, // 70
+ { 5, ABC_CONST(0xCA3535CACA3535CA), "[<abc>de]" }, // 71
+ { 5, ABC_CONST(0x0777000007770000), "(!(ab)!(cd)e)" }, // 72
+ { 5, ABC_CONST(0xF8880000F8880000), "(!(!(ab)!(cd))e)" }, // 73
+ { 5, ABC_CONST(0xF8880777F8880777), "[(!(ab)!(cd))e]" }, // 74
+ { 5, ABC_CONST(0x7888000078880000), "([(ab)(cd)]e)" }, // 75
+ { 5, ABC_CONST(0x8777000087770000), "(![(ab)(cd)]e)" }, // 76
+ { 5, ABC_CONST(0x8777788887777888), "[(ab)(cd)e]" }, // 77
+ { 5, ABC_CONST(0x0666000006660000), "([ab]!(cd)e)" }, // 78
+ { 5, ABC_CONST(0xF9990000F9990000), "(!([ab]!(cd))e)" }, // 79
+ { 5, ABC_CONST(0xF9990666F9990666), "[([ab]!(cd))e]" }, // 80
+ { 5, ABC_CONST(0x0660000006600000), "([ab][cd]e)" }, // 81
+ { 5, ABC_CONST(0xF99F0000F99F0000), "(!([ab][cd])e)" }, // 82
+ { 5, ABC_CONST(0xF99F0660F99F0660), "[([ab][cd])e]" }, // 83
+ { 5, ABC_CONST(0xCAAA0000CAAA0000), "(<ab(cd)>e)" }, // 84
+ { 5, ABC_CONST(0x3555CAAA3555CAAA), "[<ab(cd)>e]" }, // 85
+ { 5, ABC_CONST(0xACCA0000ACCA0000), "(<ab[cd]>e)" }, // 86
+ { 5, ABC_CONST(0x5335ACCA5335ACCA), "[<ab[cd]>e]" }, // 87
+ { 5, ABC_CONST(0xF0880000F0880000), "(<(ab)cd>e)" }, // 88
+ { 5, ABC_CONST(0x0F7700000F770000), "(!<(ab)cd>e)" }, // 89
+ { 5, ABC_CONST(0x0F77F0880F77F088), "[<(ab)cd>e]" }, // 90
+ { 5, ABC_CONST(0xF0660000F0660000), "(<[ab]cd>e)" }, // 91
+ { 5, ABC_CONST(0x0F99F0660F99F066), "[<[ab]cd>e]" }, // 92
+ { 5, ABC_CONST(0x007F7F7F007F7F7F), "(!(abc)!(de))" }, // 93
+ { 5, ABC_CONST(0x7F8080807F808080), "[(abc)(de)]" }, // 94
+ { 5, ABC_CONST(0x008F8F8F008F8F8F), "(!(!(ab)c)!(de))" }, // 95
+ { 5, ABC_CONST(0x8F7070708F707070), "[(!(ab)c)(de)]" }, // 96
+ { 5, ABC_CONST(0x0078787800787878), "([(ab)c]!(de))" }, // 97
+ { 5, ABC_CONST(0x009F9F9F009F9F9F), "(!([ab]c)!(de))" }, // 98
+ { 5, ABC_CONST(0x9F6060609F606060), "[([ab]c)(de)]" }, // 99
+ { 5, ABC_CONST(0x0096969600969696), "([abc]!(de))" }, // 100
+ { 5, ABC_CONST(0x00CACACA00CACACA), "(<abc>!(de))" }, // 101
+ { 5, ABC_CONST(0x35CACACA35CACACA), "[<abc>(de)]" }, // 102
+ { 5, ABC_CONST(0x007F7F00007F7F00), "(!(abc)[de])" }, // 103
+ { 5, ABC_CONST(0x008F8F00008F8F00), "(!(!(ab)c)[de])" }, // 104
+ { 5, ABC_CONST(0x0078780000787800), "([(ab)c][de])" }, // 105
+ { 5, ABC_CONST(0x009F9F00009F9F00), "(!([ab]c)[de])" }, // 106
+ { 5, ABC_CONST(0x0096960000969600), "([abc][de])" }, // 107
+ { 5, ABC_CONST(0x00CACA0000CACA00), "(<abc>[de])" }, // 108
+ { 5, ABC_CONST(0xCAAAAAAACAAAAAAA), "<ab(cde)>" }, // 109
+ { 5, ABC_CONST(0xACCCAAAAACCCAAAA), "<ab(!(cd)e)>" }, // 110
+ { 5, ABC_CONST(0xACCCCAAAACCCCAAA), "<ab[(cd)e]>" }, // 111
+ { 5, ABC_CONST(0xACCAAAAAACCAAAAA), "<ab([cd]e)>" }, // 112
+ { 5, ABC_CONST(0xCAACACCACAACACCA), "<ab[cde]>" }, // 113
+ { 5, ABC_CONST(0xCCAACACACCAACACA), "<ab<cde>>" }, // 114
+ { 5, ABC_CONST(0xC0AAAAAAC0AAAAAA), "<a(bc)(de)>" }, // 115
+ { 5, ABC_CONST(0x3CAAAAAA3CAAAAAA), "<a[bc](de)>" }, // 116
+ { 5, ABC_CONST(0xF0888888F0888888), "<(ab)c(de)>" }, // 117
+ { 5, ABC_CONST(0x88F0F08888F0F088), "<(ab)c[de]>" }, // 118
+ { 5, ABC_CONST(0xF0666666F0666666), "<[ab]c(de)>" }, // 119
+ { 5, ABC_CONST(0x66F0F06666F0F066), "<[ab]c[de]>" }, // 120
+ { 5, ABC_CONST(0xF0008888F0008888), "<(ab)(cd)e>" }, // 121
+ { 5, ABC_CONST(0xF0007777F0007777), "<!(ab)(cd)e>" }, // 122
+ { 5, ABC_CONST(0xF0006666F0006666), "<[ab](cd)e>" }, // 123
+ { 5, ABC_CONST(0x0FF066660FF06666), "<[ab][cd]e>" }, // 124
+ { 5, ABC_CONST(0xFF008080FF008080), "<(abc)de>" }, // 125
+ { 5, ABC_CONST(0xFF007070FF007070), "<(!(ab)c)de>" }, // 126
+ { 5, ABC_CONST(0xFF007878FF007878), "<[(ab)c]de>" }, // 127
+ { 5, ABC_CONST(0xFF006060FF006060), "<([ab]c)de>" }, // 128
+ { 5, ABC_CONST(0xFF009696FF009696), "<[abc]de>" }, // 129
+ { 5, ABC_CONST(0xFF00CACAFF00CACA), "<<abc>de>" }, // 130
+ { 6, ABC_CONST(0x8000000000000000), "(abcdef)" }, // 131
+ { 6, ABC_CONST(0x7FFFFFFF00000000), "(!(abcde)f)" }, // 132
+ { 6, ABC_CONST(0x7FFFFFFF80000000), "[(abcde)f]" }, // 133
+ { 6, ABC_CONST(0x7FFF000000000000), "(!(abcd)ef)" }, // 134
+ { 6, ABC_CONST(0x8000FFFF00000000), "(!(!(abcd)e)f)" }, // 135
+ { 6, ABC_CONST(0x8000FFFF7FFF0000), "[(!(abcd)e)f]" }, // 136
+ { 6, ABC_CONST(0x7FFF800000000000), "([(abcd)e]f)" }, // 137
+ { 6, ABC_CONST(0x80007FFF7FFF8000), "[(abcd)ef]" }, // 138
+ { 6, ABC_CONST(0x7F00000000000000), "(!(abc)def)" }, // 139
+ { 6, ABC_CONST(0x80FFFFFF00000000), "(!(!(abc)de)f)" }, // 140
+ { 6, ABC_CONST(0x80FFFFFF7F000000), "[(!(abc)de)f]" }, // 141
+ { 6, ABC_CONST(0x80FF000000000000), "(!(!(abc)d)ef)" }, // 142
+ { 6, ABC_CONST(0x7F00FFFF00000000), "(!(!(!(abc)d)e)f)" }, // 143
+ { 6, ABC_CONST(0x7F00FFFF80FF0000), "[(!(!(abc)d)e)f]" }, // 144
+ { 6, ABC_CONST(0x80FF7F0000000000), "([(!(abc)d)e]f)" }, // 145
+ { 6, ABC_CONST(0x7F0080FF80FF7F00), "[(!(abc)d)ef]" }, // 146
+ { 6, ABC_CONST(0x7F80000000000000), "([(abc)d]ef)" }, // 147
+ { 6, ABC_CONST(0x807FFFFF00000000), "(!([(abc)d]e)f)" }, // 148
+ { 6, ABC_CONST(0x807FFFFF7F800000), "[([(abc)d]e)f]" }, // 149
+ { 6, ABC_CONST(0x807F7F8000000000), "([(abc)de]f)" }, // 150
+ { 6, ABC_CONST(0x7F80807F807F7F80), "[(abc)def]" }, // 151
+ { 6, ABC_CONST(0x7000000000000000), "(!(ab)cdef)" }, // 152
+ { 6, ABC_CONST(0x8FFFFFFF00000000), "(!(!(ab)cde)f)" }, // 153
+ { 6, ABC_CONST(0x8FFFFFFF70000000), "[(!(ab)cde)f]" }, // 154
+ { 6, ABC_CONST(0x8FFF000000000000), "(!(!(ab)cd)ef)" }, // 155
+ { 6, ABC_CONST(0x7000FFFF00000000), "(!(!(!(ab)cd)e)f)" }, // 156
+ { 6, ABC_CONST(0x7000FFFF8FFF0000), "[(!(!(ab)cd)e)f]" }, // 157
+ { 6, ABC_CONST(0x8FFF700000000000), "([(!(ab)cd)e]f)" }, // 158
+ { 6, ABC_CONST(0x70008FFF8FFF7000), "[(!(ab)cd)ef]" }, // 159
+ { 6, ABC_CONST(0x8F00000000000000), "(!(!(ab)c)def)" }, // 160
+ { 6, ABC_CONST(0x70FFFFFF00000000), "(!(!(!(ab)c)de)f)" }, // 161
+ { 6, ABC_CONST(0x70FFFFFF8F000000), "[(!(!(ab)c)de)f]" }, // 162
+ { 6, ABC_CONST(0x70FF000000000000), "(!(!(!(ab)c)d)ef)" }, // 163
+ { 6, ABC_CONST(0x8F00FFFF00000000), "(!(!(!(!(ab)c)d)e)f)" }, // 164
+ { 6, ABC_CONST(0x8F00FFFF70FF0000), "[(!(!(!(ab)c)d)e)f]" }, // 165
+ { 6, ABC_CONST(0x70FF8F0000000000), "([(!(!(ab)c)d)e]f)" }, // 166
+ { 6, ABC_CONST(0x8F0070FF70FF8F00), "[(!(!(ab)c)d)ef]" }, // 167
+ { 6, ABC_CONST(0x8F70000000000000), "([(!(ab)c)d]ef)" }, // 168
+ { 6, ABC_CONST(0x708FFFFF00000000), "(!([(!(ab)c)d]e)f)" }, // 169
+ { 6, ABC_CONST(0x708FFFFF8F700000), "[([(!(ab)c)d]e)f]" }, // 170
+ { 6, ABC_CONST(0x708F8F7000000000), "([(!(ab)c)de]f)" }, // 171
+ { 6, ABC_CONST(0x8F70708F708F8F70), "[(!(ab)c)def]" }, // 172
+ { 6, ABC_CONST(0x7800000000000000), "([(ab)c]def)" }, // 173
+ { 6, ABC_CONST(0x87FFFFFF00000000), "(!([(ab)c]de)f)" }, // 174
+ { 6, ABC_CONST(0x87FFFFFF78000000), "[([(ab)c]de)f]" }, // 175
+ { 6, ABC_CONST(0x87FF000000000000), "(!([(ab)c]d)ef)" }, // 176
+ { 6, ABC_CONST(0x7800FFFF00000000), "(!(!([(ab)c]d)e)f)" }, // 177
+ { 6, ABC_CONST(0x7800FFFF87FF0000), "[(!([(ab)c]d)e)f]" }, // 178
+ { 6, ABC_CONST(0x87FF780000000000), "([([(ab)c]d)e]f)" }, // 179
+ { 6, ABC_CONST(0x780087FF87FF7800), "[([(ab)c]d)ef]" }, // 180
+ { 6, ABC_CONST(0x8778000000000000), "([(ab)cd]ef)" }, // 181
+ { 6, ABC_CONST(0x7887FFFF00000000), "(!([(ab)cd]e)f)" }, // 182
+ { 6, ABC_CONST(0x7887FFFF87780000), "[([(ab)cd]e)f]" }, // 183
+ { 6, ABC_CONST(0x7887877800000000), "([(ab)cde]f)" }, // 184
+ { 6, ABC_CONST(0x8778788778878778), "[(ab)cdef]" }, // 185
+ { 6, ABC_CONST(0x6000000000000000), "([ab]cdef)" }, // 186
+ { 6, ABC_CONST(0x9FFFFFFF00000000), "(!([ab]cde)f)" }, // 187
+ { 6, ABC_CONST(0x9FFFFFFF60000000), "[([ab]cde)f]" }, // 188
+ { 6, ABC_CONST(0x9FFF000000000000), "(!([ab]cd)ef)" }, // 189
+ { 6, ABC_CONST(0x6000FFFF00000000), "(!(!([ab]cd)e)f)" }, // 190
+ { 6, ABC_CONST(0x6000FFFF9FFF0000), "[(!([ab]cd)e)f]" }, // 191
+ { 6, ABC_CONST(0x9FFF600000000000), "([([ab]cd)e]f)" }, // 192
+ { 6, ABC_CONST(0x60009FFF9FFF6000), "[([ab]cd)ef]" }, // 193
+ { 6, ABC_CONST(0x9F00000000000000), "(!([ab]c)def)" }, // 194
+ { 6, ABC_CONST(0x60FFFFFF00000000), "(!(!([ab]c)de)f)" }, // 195
+ { 6, ABC_CONST(0x60FFFFFF9F000000), "[(!([ab]c)de)f]" }, // 196
+ { 6, ABC_CONST(0x60FF000000000000), "(!(!([ab]c)d)ef)" }, // 197
+ { 6, ABC_CONST(0x9F00FFFF00000000), "(!(!(!([ab]c)d)e)f)" }, // 198
+ { 6, ABC_CONST(0x9F00FFFF60FF0000), "[(!(!([ab]c)d)e)f]" }, // 199
+ { 6, ABC_CONST(0x60FF9F0000000000), "([(!([ab]c)d)e]f)" }, // 200
+ { 6, ABC_CONST(0x9F0060FF60FF9F00), "[(!([ab]c)d)ef]" }, // 201
+ { 6, ABC_CONST(0x9F60000000000000), "([([ab]c)d]ef)" }, // 202
+ { 6, ABC_CONST(0x609FFFFF00000000), "(!([([ab]c)d]e)f)" }, // 203
+ { 6, ABC_CONST(0x609FFFFF9F600000), "[([([ab]c)d]e)f]" }, // 204
+ { 6, ABC_CONST(0x609F9F6000000000), "([([ab]c)de]f)" }, // 205
+ { 6, ABC_CONST(0x9F60609F609F9F60), "[([ab]c)def]" }, // 206
+ { 6, ABC_CONST(0x9600000000000000), "([abc]def)" }, // 207
+ { 6, ABC_CONST(0x69FFFFFF00000000), "(!([abc]de)f)" }, // 208
+ { 6, ABC_CONST(0x69FFFFFF96000000), "[([abc]de)f]" }, // 209
+ { 6, ABC_CONST(0x69FF000000000000), "(!([abc]d)ef)" }, // 210
+ { 6, ABC_CONST(0x9600FFFF00000000), "(!(!([abc]d)e)f)" }, // 211
+ { 6, ABC_CONST(0x9600FFFF69FF0000), "[(!([abc]d)e)f]" }, // 212
+ { 6, ABC_CONST(0x69FF960000000000), "([([abc]d)e]f)" }, // 213
+ { 6, ABC_CONST(0x960069FF69FF9600), "[([abc]d)ef]" }, // 214
+ { 6, ABC_CONST(0x6996000000000000), "([abcd]ef)" }, // 215
+ { 6, ABC_CONST(0x9669FFFF00000000), "(!([abcd]e)f)" }, // 216
+ { 6, ABC_CONST(0x9669FFFF69960000), "[([abcd]e)f]" }, // 217
+ { 6, ABC_CONST(0x9669699600000000), "([abcde]f)" }, // 218
+ { 6, ABC_CONST(0x6996966996696996), "[abcdef]" }, // 219
+ { 6, ABC_CONST(0xCA00000000000000), "(<abc>def)" }, // 220
+ { 6, ABC_CONST(0x35FFFFFF00000000), "(!(<abc>de)f)" }, // 221
+ { 6, ABC_CONST(0x35FFFFFFCA000000), "[(<abc>de)f]" }, // 222
+ { 6, ABC_CONST(0x35FF000000000000), "(!(<abc>d)ef)" }, // 223
+ { 6, ABC_CONST(0xCA00FFFF00000000), "(!(!(<abc>d)e)f)" }, // 224
+ { 6, ABC_CONST(0xCA00FFFF35FF0000), "[(!(<abc>d)e)f]" }, // 225
+ { 6, ABC_CONST(0x35FFCA0000000000), "([(<abc>d)e]f)" }, // 226
+ { 6, ABC_CONST(0xCA0035FF35FFCA00), "[(<abc>d)ef]" }, // 227
+ { 6, ABC_CONST(0x35CA000000000000), "([<abc>d]ef)" }, // 228
+ { 6, ABC_CONST(0xCA35FFFF00000000), "(!([<abc>d]e)f)" }, // 229
+ { 6, ABC_CONST(0xCA35FFFF35CA0000), "[([<abc>d]e)f]" }, // 230
+ { 6, ABC_CONST(0xCA3535CA00000000), "([<abc>de]f)" }, // 231
+ { 6, ABC_CONST(0x35CACA35CA3535CA), "[<abc>def]" }, // 232
+ { 6, ABC_CONST(0x0777000000000000), "(!(ab)!(cd)ef)" }, // 233
+ { 6, ABC_CONST(0xF888FFFF00000000), "(!(!(ab)!(cd)e)f)" }, // 234
+ { 6, ABC_CONST(0xF888FFFF07770000), "[(!(ab)!(cd)e)f]" }, // 235
+ { 6, ABC_CONST(0xF888000000000000), "(!(!(ab)!(cd))ef)" }, // 236
+ { 6, ABC_CONST(0x0777FFFF00000000), "(!(!(!(ab)!(cd))e)f)" }, // 237
+ { 6, ABC_CONST(0x0777FFFFF8880000), "[(!(!(ab)!(cd))e)f]" }, // 238
+ { 6, ABC_CONST(0xF888077700000000), "([(!(ab)!(cd))e]f)" }, // 239
+ { 6, ABC_CONST(0x0777F888F8880777), "[(!(ab)!(cd))ef]" }, // 240
+ { 6, ABC_CONST(0x7888000000000000), "([(ab)(cd)]ef)" }, // 241
+ { 6, ABC_CONST(0x8777FFFF00000000), "(!([(ab)(cd)]e)f)" }, // 242
+ { 6, ABC_CONST(0x8777FFFF78880000), "[([(ab)(cd)]e)f]" }, // 243
+ { 6, ABC_CONST(0x8777000000000000), "(![(ab)(cd)]ef)" }, // 244
+ { 6, ABC_CONST(0x7888FFFF00000000), "(!(![(ab)(cd)]e)f)" }, // 245
+ { 6, ABC_CONST(0x7888FFFF87770000), "[(![(ab)(cd)]e)f]" }, // 246
+ { 6, ABC_CONST(0x8777788800000000), "([(ab)(cd)e]f)" }, // 247
+ { 6, ABC_CONST(0x7888877787777888), "[(ab)(cd)ef]" }, // 248
+ { 6, ABC_CONST(0x0666000000000000), "([ab]!(cd)ef)" }, // 249
+ { 6, ABC_CONST(0xF999FFFF00000000), "(!([ab]!(cd)e)f)" }, // 250
+ { 6, ABC_CONST(0xF999FFFF06660000), "[([ab]!(cd)e)f]" }, // 251
+ { 6, ABC_CONST(0xF999000000000000), "(!([ab]!(cd))ef)" }, // 252
+ { 6, ABC_CONST(0x0666FFFF00000000), "(!(!([ab]!(cd))e)f)" }, // 253
+ { 6, ABC_CONST(0x0666FFFFF9990000), "[(!([ab]!(cd))e)f]" }, // 254
+ { 6, ABC_CONST(0xF999066600000000), "([([ab]!(cd))e]f)" }, // 255
+ { 6, ABC_CONST(0x0666F999F9990666), "[([ab]!(cd))ef]" }, // 256
+ { 6, ABC_CONST(0x0660000000000000), "([ab][cd]ef)" }, // 257
+ { 6, ABC_CONST(0xF99FFFFF00000000), "(!([ab][cd]e)f)" }, // 258
+ { 6, ABC_CONST(0xF99FFFFF06600000), "[([ab][cd]e)f]" }, // 259
+ { 6, ABC_CONST(0xF99F000000000000), "(!([ab][cd])ef)" }, // 260
+ { 6, ABC_CONST(0x0660FFFF00000000), "(!(!([ab][cd])e)f)" }, // 261
+ { 6, ABC_CONST(0x0660FFFFF99F0000), "[(!([ab][cd])e)f]" }, // 262
+ { 6, ABC_CONST(0xF99F066000000000), "([([ab][cd])e]f)" }, // 263
+ { 6, ABC_CONST(0x0660F99FF99F0660), "[([ab][cd])ef]" }, // 264
+ { 6, ABC_CONST(0xCAAA000000000000), "(<ab(cd)>ef)" }, // 265
+ { 6, ABC_CONST(0x3555FFFF00000000), "(!(<ab(cd)>e)f)" }, // 266
+ { 6, ABC_CONST(0x3555FFFFCAAA0000), "[(<ab(cd)>e)f]" }, // 267
+ { 6, ABC_CONST(0x3555CAAA00000000), "([<ab(cd)>e]f)" }, // 268
+ { 6, ABC_CONST(0xCAAA35553555CAAA), "[<ab(cd)>ef]" }, // 269
+ { 6, ABC_CONST(0xACCA000000000000), "(<ab[cd]>ef)" }, // 270
+ { 6, ABC_CONST(0x5335FFFF00000000), "(!(<ab[cd]>e)f)" }, // 271
+ { 6, ABC_CONST(0x5335FFFFACCA0000), "[(<ab[cd]>e)f]" }, // 272
+ { 6, ABC_CONST(0x5335ACCA00000000), "([<ab[cd]>e]f)" }, // 273
+ { 6, ABC_CONST(0xACCA53355335ACCA), "[<ab[cd]>ef]" }, // 274
+ { 6, ABC_CONST(0xF088000000000000), "(<(ab)cd>ef)" }, // 275
+ { 6, ABC_CONST(0x0F77FFFF00000000), "(!(<(ab)cd>e)f)" }, // 276
+ { 6, ABC_CONST(0x0F77FFFFF0880000), "[(<(ab)cd>e)f]" }, // 277
+ { 6, ABC_CONST(0x0F77000000000000), "(!<(ab)cd>ef)" }, // 278
+ { 6, ABC_CONST(0xF088FFFF00000000), "(!(!<(ab)cd>e)f)" }, // 279
+ { 6, ABC_CONST(0xF088FFFF0F770000), "[(!<(ab)cd>e)f]" }, // 280
+ { 6, ABC_CONST(0x0F77F08800000000), "([<(ab)cd>e]f)" }, // 281
+ { 6, ABC_CONST(0xF0880F770F77F088), "[<(ab)cd>ef]" }, // 282
+ { 6, ABC_CONST(0xF066000000000000), "(<[ab]cd>ef)" }, // 283
+ { 6, ABC_CONST(0x0F99FFFF00000000), "(!(<[ab]cd>e)f)" }, // 284
+ { 6, ABC_CONST(0x0F99FFFFF0660000), "[(<[ab]cd>e)f]" }, // 285
+ { 6, ABC_CONST(0x0F99F06600000000), "([<[ab]cd>e]f)" }, // 286
+ { 6, ABC_CONST(0xF0660F990F99F066), "[<[ab]cd>ef]" }, // 287
+ { 6, ABC_CONST(0x007F7F7F00000000), "(!(abc)!(de)f)" }, // 288
+ { 6, ABC_CONST(0xFF80808000000000), "(!(!(abc)!(de))f)" }, // 289
+ { 6, ABC_CONST(0xFF808080007F7F7F), "[(!(abc)!(de))f]" }, // 290
+ { 6, ABC_CONST(0x7F80808000000000), "([(abc)(de)]f)" }, // 291
+ { 6, ABC_CONST(0x807F7F7F00000000), "(![(abc)(de)]f)" }, // 292
+ { 6, ABC_CONST(0x807F7F7F7F808080), "[(abc)(de)f]" }, // 293
+ { 6, ABC_CONST(0x008F8F8F00000000), "(!(!(ab)c)!(de)f)" }, // 294
+ { 6, ABC_CONST(0xFF70707000000000), "(!(!(!(ab)c)!(de))f)" }, // 295
+ { 6, ABC_CONST(0xFF707070008F8F8F), "[(!(!(ab)c)!(de))f]" }, // 296
+ { 6, ABC_CONST(0x8F70707000000000), "([(!(ab)c)(de)]f)" }, // 297
+ { 6, ABC_CONST(0x708F8F8F00000000), "(![(!(ab)c)(de)]f)" }, // 298
+ { 6, ABC_CONST(0x708F8F8F8F707070), "[(!(ab)c)(de)f]" }, // 299
+ { 6, ABC_CONST(0x0078787800000000), "([(ab)c]!(de)f)" }, // 300
+ { 6, ABC_CONST(0xFF87878700000000), "(!([(ab)c]!(de))f)" }, // 301
+ { 6, ABC_CONST(0xFF87878700787878), "[([(ab)c]!(de))f]" }, // 302
+ { 6, ABC_CONST(0x009F9F9F00000000), "(!([ab]c)!(de)f)" }, // 303
+ { 6, ABC_CONST(0xFF60606000000000), "(!(!([ab]c)!(de))f)" }, // 304
+ { 6, ABC_CONST(0xFF606060009F9F9F), "[(!([ab]c)!(de))f]" }, // 305
+ { 6, ABC_CONST(0x9F60606000000000), "([([ab]c)(de)]f)" }, // 306
+ { 6, ABC_CONST(0x609F9F9F00000000), "(![([ab]c)(de)]f)" }, // 307
+ { 6, ABC_CONST(0x609F9F9F9F606060), "[([ab]c)(de)f]" }, // 308
+ { 6, ABC_CONST(0x0096969600000000), "([abc]!(de)f)" }, // 309
+ { 6, ABC_CONST(0xFF69696900000000), "(!([abc]!(de))f)" }, // 310
+ { 6, ABC_CONST(0xFF69696900969696), "[([abc]!(de))f]" }, // 311
+ { 6, ABC_CONST(0x00CACACA00000000), "(<abc>!(de)f)" }, // 312
+ { 6, ABC_CONST(0xFF35353500000000), "(!(<abc>!(de))f)" }, // 313
+ { 6, ABC_CONST(0xFF35353500CACACA), "[(<abc>!(de))f]" }, // 314
+ { 6, ABC_CONST(0x35CACACA00000000), "([<abc>(de)]f)" }, // 315
+ { 6, ABC_CONST(0xCA35353535CACACA), "[<abc>(de)f]" }, // 316
+ { 6, ABC_CONST(0x007F7F0000000000), "(!(abc)[de]f)" }, // 317
+ { 6, ABC_CONST(0xFF8080FF00000000), "(!(!(abc)[de])f)" }, // 318
+ { 6, ABC_CONST(0xFF8080FF007F7F00), "[(!(abc)[de])f]" }, // 319
+ { 6, ABC_CONST(0x008F8F0000000000), "(!(!(ab)c)[de]f)" }, // 320
+ { 6, ABC_CONST(0xFF7070FF00000000), "(!(!(!(ab)c)[de])f)" }, // 321
+ { 6, ABC_CONST(0xFF7070FF008F8F00), "[(!(!(ab)c)[de])f]" }, // 322
+ { 6, ABC_CONST(0x0078780000000000), "([(ab)c][de]f)" }, // 323
+ { 6, ABC_CONST(0xFF8787FF00000000), "(!([(ab)c][de])f)" }, // 324
+ { 6, ABC_CONST(0xFF8787FF00787800), "[([(ab)c][de])f]" }, // 325
+ { 6, ABC_CONST(0x009F9F0000000000), "(!([ab]c)[de]f)" }, // 326
+ { 6, ABC_CONST(0xFF6060FF00000000), "(!(!([ab]c)[de])f)" }, // 327
+ { 6, ABC_CONST(0xFF6060FF009F9F00), "[(!([ab]c)[de])f]" }, // 328
+ { 6, ABC_CONST(0x0096960000000000), "([abc][de]f)" }, // 329
+ { 6, ABC_CONST(0xFF6969FF00000000), "(!([abc][de])f)" }, // 330
+ { 6, ABC_CONST(0xFF6969FF00969600), "[([abc][de])f]" }, // 331
+ { 6, ABC_CONST(0x00CACA0000000000), "(<abc>[de]f)" }, // 332
+ { 6, ABC_CONST(0xFF3535FF00000000), "(!(<abc>[de])f)" }, // 333
+ { 6, ABC_CONST(0xFF3535FF00CACA00), "[(<abc>[de])f]" }, // 334
+ { 6, ABC_CONST(0xCAAAAAAA00000000), "(<ab(cde)>f)" }, // 335
+ { 6, ABC_CONST(0x35555555CAAAAAAA), "[<ab(cde)>f]" }, // 336
+ { 6, ABC_CONST(0xACCCAAAA00000000), "(<ab(!(cd)e)>f)" }, // 337
+ { 6, ABC_CONST(0x53335555ACCCAAAA), "[<ab(!(cd)e)>f]" }, // 338
+ { 6, ABC_CONST(0xACCCCAAA00000000), "(<ab[(cd)e]>f)" }, // 339
+ { 6, ABC_CONST(0x53333555ACCCCAAA), "[<ab[(cd)e]>f]" }, // 340
+ { 6, ABC_CONST(0xACCAAAAA00000000), "(<ab([cd]e)>f)" }, // 341
+ { 6, ABC_CONST(0x53355555ACCAAAAA), "[<ab([cd]e)>f]" }, // 342
+ { 6, ABC_CONST(0xCAACACCA00000000), "(<ab[cde]>f)" }, // 343
+ { 6, ABC_CONST(0x35535335CAACACCA), "[<ab[cde]>f]" }, // 344
+ { 6, ABC_CONST(0xCCAACACA00000000), "(<ab<cde>>f)" }, // 345
+ { 6, ABC_CONST(0x33553535CCAACACA), "[<ab<cde>>f]" }, // 346
+ { 6, ABC_CONST(0xC0AAAAAA00000000), "(<a(bc)(de)>f)" }, // 347
+ { 6, ABC_CONST(0x3F55555500000000), "(!<a(bc)(de)>f)" }, // 348
+ { 6, ABC_CONST(0x3F555555C0AAAAAA), "[<a(bc)(de)>f]" }, // 349
+ { 6, ABC_CONST(0x3CAAAAAA00000000), "(<a[bc](de)>f)" }, // 350
+ { 6, ABC_CONST(0xC35555553CAAAAAA), "[<a[bc](de)>f]" }, // 351
+ { 6, ABC_CONST(0xF088888800000000), "(<(ab)c(de)>f)" }, // 352
+ { 6, ABC_CONST(0x0F77777700000000), "(!<(ab)c(de)>f)" }, // 353
+ { 6, ABC_CONST(0x0F777777F0888888), "[<(ab)c(de)>f]" }, // 354
+ { 6, ABC_CONST(0x88F0F08800000000), "(<(ab)c[de]>f)" }, // 355
+ { 6, ABC_CONST(0x770F0F7700000000), "(!<(ab)c[de]>f)" }, // 356
+ { 6, ABC_CONST(0x770F0F7788F0F088), "[<(ab)c[de]>f]" }, // 357
+ { 6, ABC_CONST(0xF066666600000000), "(<[ab]c(de)>f)" }, // 358
+ { 6, ABC_CONST(0x0F999999F0666666), "[<[ab]c(de)>f]" }, // 359
+ { 6, ABC_CONST(0x66F0F06600000000), "(<[ab]c[de]>f)" }, // 360
+ { 6, ABC_CONST(0x990F0F9966F0F066), "[<[ab]c[de]>f]" }, // 361
+ { 6, ABC_CONST(0xF000888800000000), "(<(ab)(cd)e>f)" }, // 362
+ { 6, ABC_CONST(0x0FFF777700000000), "(!<(ab)(cd)e>f)" }, // 363
+ { 6, ABC_CONST(0x0FFF7777F0008888), "[<(ab)(cd)e>f]" }, // 364
+ { 6, ABC_CONST(0xF000777700000000), "(<!(ab)(cd)e>f)" }, // 365
+ { 6, ABC_CONST(0x0FFF8888F0007777), "[<!(ab)(cd)e>f]" }, // 366
+ { 6, ABC_CONST(0xF000666600000000), "(<[ab](cd)e>f)" }, // 367
+ { 6, ABC_CONST(0x0FFF999900000000), "(!<[ab](cd)e>f)" }, // 368
+ { 6, ABC_CONST(0x0FFF9999F0006666), "[<[ab](cd)e>f]" }, // 369
+ { 6, ABC_CONST(0x0FF0666600000000), "(<[ab][cd]e>f)" }, // 370
+ { 6, ABC_CONST(0xF00F99990FF06666), "[<[ab][cd]e>f]" }, // 371
+ { 6, ABC_CONST(0xFF00808000000000), "(<(abc)de>f)" }, // 372
+ { 6, ABC_CONST(0x00FF7F7F00000000), "(!<(abc)de>f)" }, // 373
+ { 6, ABC_CONST(0x00FF7F7FFF008080), "[<(abc)de>f]" }, // 374
+ { 6, ABC_CONST(0xFF00707000000000), "(<(!(ab)c)de>f)" }, // 375
+ { 6, ABC_CONST(0x00FF8F8F00000000), "(!<(!(ab)c)de>f)" }, // 376
+ { 6, ABC_CONST(0x00FF8F8FFF007070), "[<(!(ab)c)de>f]" }, // 377
+ { 6, ABC_CONST(0xFF00787800000000), "(<[(ab)c]de>f)" }, // 378
+ { 6, ABC_CONST(0x00FF8787FF007878), "[<[(ab)c]de>f]" }, // 379
+ { 6, ABC_CONST(0xFF00606000000000), "(<([ab]c)de>f)" }, // 380
+ { 6, ABC_CONST(0x00FF9F9F00000000), "(!<([ab]c)de>f)" }, // 381
+ { 6, ABC_CONST(0x00FF9F9FFF006060), "[<([ab]c)de>f]" }, // 382
+ { 6, ABC_CONST(0xFF00969600000000), "(<[abc]de>f)" }, // 383
+ { 6, ABC_CONST(0x00FF6969FF009696), "[<[abc]de>f]" }, // 384
+ { 6, ABC_CONST(0xFF00CACA00000000), "(<<abc>de>f)" }, // 385
+ { 6, ABC_CONST(0x00FF3535FF00CACA), "[<<abc>de>f]" }, // 386
+ { 6, ABC_CONST(0x00007FFF7FFF7FFF), "(!(abcd)!(ef))" }, // 387
+ { 6, ABC_CONST(0x7FFF800080008000), "[(abcd)(ef)]" }, // 388
+ { 6, ABC_CONST(0x000080FF80FF80FF), "(!(!(abc)d)!(ef))" }, // 389
+ { 6, ABC_CONST(0x80FF7F007F007F00), "[(!(abc)d)(ef)]" }, // 390
+ { 6, ABC_CONST(0x00007F807F807F80), "([(abc)d]!(ef))" }, // 391
+ { 6, ABC_CONST(0x00008FFF8FFF8FFF), "(!(!(ab)cd)!(ef))" }, // 392
+ { 6, ABC_CONST(0x8FFF700070007000), "[(!(ab)cd)(ef)]" }, // 393
+ { 6, ABC_CONST(0x000070FF70FF70FF), "(!(!(!(ab)c)d)!(ef))" }, // 394
+ { 6, ABC_CONST(0x70FF8F008F008F00), "[(!(!(ab)c)d)(ef)]" }, // 395
+ { 6, ABC_CONST(0x00008F708F708F70), "([(!(ab)c)d]!(ef))" }, // 396
+ { 6, ABC_CONST(0x000087FF87FF87FF), "(!([(ab)c]d)!(ef))" }, // 397
+ { 6, ABC_CONST(0x87FF780078007800), "[([(ab)c]d)(ef)]" }, // 398
+ { 6, ABC_CONST(0x0000877887788778), "([(ab)cd]!(ef))" }, // 399
+ { 6, ABC_CONST(0x00009FFF9FFF9FFF), "(!([ab]cd)!(ef))" }, // 400
+ { 6, ABC_CONST(0x9FFF600060006000), "[([ab]cd)(ef)]" }, // 401
+ { 6, ABC_CONST(0x000060FF60FF60FF), "(!(!([ab]c)d)!(ef))" }, // 402
+ { 6, ABC_CONST(0x60FF9F009F009F00), "[(!([ab]c)d)(ef)]" }, // 403
+ { 6, ABC_CONST(0x00009F609F609F60), "([([ab]c)d]!(ef))" }, // 404
+ { 6, ABC_CONST(0x000069FF69FF69FF), "(!([abc]d)!(ef))" }, // 405
+ { 6, ABC_CONST(0x69FF960096009600), "[([abc]d)(ef)]" }, // 406
+ { 6, ABC_CONST(0x0000699669966996), "([abcd]!(ef))" }, // 407
+ { 6, ABC_CONST(0x000035FF35FF35FF), "(!(<abc>d)!(ef))" }, // 408
+ { 6, ABC_CONST(0x35FFCA00CA00CA00), "[(<abc>d)(ef)]" }, // 409
+ { 6, ABC_CONST(0x000035CA35CA35CA), "([<abc>d]!(ef))" }, // 410
+ { 6, ABC_CONST(0x0000077707770777), "(!(ab)!(cd)!(ef))" }, // 411
+ { 6, ABC_CONST(0x0000F888F888F888), "(!(!(ab)!(cd))!(ef))" }, // 412
+ { 6, ABC_CONST(0xF888077707770777), "[(!(ab)!(cd))(ef)]" }, // 413
+ { 6, ABC_CONST(0x0000788878887888), "([(ab)(cd)]!(ef))" }, // 414
+ { 6, ABC_CONST(0x0000877787778777), "(![(ab)(cd)]!(ef))" }, // 415
+ { 6, ABC_CONST(0x8777788878887888), "[(ab)(cd)(ef)]" }, // 416
+ { 6, ABC_CONST(0x0000066606660666), "([ab]!(cd)!(ef))" }, // 417
+ { 6, ABC_CONST(0x0000F999F999F999), "(!([ab]!(cd))!(ef))" }, // 418
+ { 6, ABC_CONST(0xF999066606660666), "[([ab]!(cd))(ef)]" }, // 419
+ { 6, ABC_CONST(0x0000066006600660), "([ab][cd]!(ef))" }, // 420
+ { 6, ABC_CONST(0x0000F99FF99FF99F), "(!([ab][cd])!(ef))" }, // 421
+ { 6, ABC_CONST(0xF99F066006600660), "[([ab][cd])(ef)]" }, // 422
+ { 6, ABC_CONST(0x0000CAAACAAACAAA), "(<ab(cd)>!(ef))" }, // 423
+ { 6, ABC_CONST(0x3555CAAACAAACAAA), "[<ab(cd)>(ef)]" }, // 424
+ { 6, ABC_CONST(0x0000ACCAACCAACCA), "(<ab[cd]>!(ef))" }, // 425
+ { 6, ABC_CONST(0x5335ACCAACCAACCA), "[<ab[cd]>(ef)]" }, // 426
+ { 6, ABC_CONST(0x0000F088F088F088), "(<(ab)cd>!(ef))" }, // 427
+ { 6, ABC_CONST(0x00000F770F770F77), "(!<(ab)cd>!(ef))" }, // 428
+ { 6, ABC_CONST(0x0F77F088F088F088), "[<(ab)cd>(ef)]" }, // 429
+ { 6, ABC_CONST(0x0000F066F066F066), "(<[ab]cd>!(ef))" }, // 430
+ { 6, ABC_CONST(0x0F99F066F066F066), "[<[ab]cd>(ef)]" }, // 431
+ { 6, ABC_CONST(0x00007FFF7FFF0000), "(!(abcd)[ef])" }, // 432
+ { 6, ABC_CONST(0x000080FF80FF0000), "(!(!(abc)d)[ef])" }, // 433
+ { 6, ABC_CONST(0x00007F807F800000), "([(abc)d][ef])" }, // 434
+ { 6, ABC_CONST(0x00008FFF8FFF0000), "(!(!(ab)cd)[ef])" }, // 435
+ { 6, ABC_CONST(0x000070FF70FF0000), "(!(!(!(ab)c)d)[ef])" }, // 436
+ { 6, ABC_CONST(0x00008F708F700000), "([(!(ab)c)d][ef])" }, // 437
+ { 6, ABC_CONST(0x000087FF87FF0000), "(!([(ab)c]d)[ef])" }, // 438
+ { 6, ABC_CONST(0x0000877887780000), "([(ab)cd][ef])" }, // 439
+ { 6, ABC_CONST(0x00009FFF9FFF0000), "(!([ab]cd)[ef])" }, // 440
+ { 6, ABC_CONST(0x000060FF60FF0000), "(!(!([ab]c)d)[ef])" }, // 441
+ { 6, ABC_CONST(0x00009F609F600000), "([([ab]c)d][ef])" }, // 442
+ { 6, ABC_CONST(0x000069FF69FF0000), "(!([abc]d)[ef])" }, // 443
+ { 6, ABC_CONST(0x0000699669960000), "([abcd][ef])" }, // 444
+ { 6, ABC_CONST(0x000035FF35FF0000), "(!(<abc>d)[ef])" }, // 445
+ { 6, ABC_CONST(0x000035CA35CA0000), "([<abc>d][ef])" }, // 446
+ { 6, ABC_CONST(0x0000F888F8880000), "(!(!(ab)!(cd))[ef])" }, // 447
+ { 6, ABC_CONST(0x0000788878880000), "([(ab)(cd)][ef])" }, // 448
+ { 6, ABC_CONST(0x0000877787770000), "(![(ab)(cd)][ef])" }, // 449
+ { 6, ABC_CONST(0x0000F999F9990000), "(!([ab]!(cd))[ef])" }, // 450
+ { 6, ABC_CONST(0x0000066006600000), "([ab][cd][ef])" }, // 451
+ { 6, ABC_CONST(0x0000F99FF99F0000), "(!([ab][cd])[ef])" }, // 452
+ { 6, ABC_CONST(0x0000CAAACAAA0000), "(<ab(cd)>[ef])" }, // 453
+ { 6, ABC_CONST(0x0000ACCAACCA0000), "(<ab[cd]>[ef])" }, // 454
+ { 6, ABC_CONST(0x0000F088F0880000), "(<(ab)cd>[ef])" }, // 455
+ { 6, ABC_CONST(0x00000F770F770000), "(!<(ab)cd>[ef])" }, // 456
+ { 6, ABC_CONST(0x0000F066F0660000), "(<[ab]cd>[ef])" }, // 457
+ { 6, ABC_CONST(0x007F7F7F7F7F7F7F), "(!(abc)!(def))" }, // 458
+ { 6, ABC_CONST(0x7F80808080808080), "[(abc)(def)]" }, // 459
+ { 6, ABC_CONST(0x008F8F8F8F8F8F8F), "(!(!(ab)c)!(def))" }, // 460
+ { 6, ABC_CONST(0x8F70707070707070), "[(!(ab)c)(def)]" }, // 461
+ { 6, ABC_CONST(0x0078787878787878), "([(ab)c]!(def))" }, // 462
+ { 6, ABC_CONST(0x009F9F9F9F9F9F9F), "(!([ab]c)!(def))" }, // 463
+ { 6, ABC_CONST(0x9F60606060606060), "[([ab]c)(def)]" }, // 464
+ { 6, ABC_CONST(0x0096969696969696), "([abc]!(def))" }, // 465
+ { 6, ABC_CONST(0x00CACACACACACACA), "(<abc>!(def))" }, // 466
+ { 6, ABC_CONST(0x35CACACACACACACA), "[<abc>(def)]" }, // 467
+ { 6, ABC_CONST(0x8F0000008F8F8F8F), "(!(!(ab)c)!(!(de)f))" }, // 468
+ { 6, ABC_CONST(0x708F8F8F70707070), "[(!(ab)c)(!(de)f)]" }, // 469
+ { 6, ABC_CONST(0x7800000078787878), "([(ab)c]!(!(de)f))" }, // 470
+ { 6, ABC_CONST(0x9F0000009F9F9F9F), "(!([ab]c)!(!(de)f))" }, // 471
+ { 6, ABC_CONST(0x609F9F9F60606060), "[([ab]c)(!(de)f)]" }, // 472
+ { 6, ABC_CONST(0x9600000096969696), "([abc]!(!(de)f))" }, // 473
+ { 6, ABC_CONST(0xCA000000CACACACA), "(<abc>!(!(de)f))" }, // 474
+ { 6, ABC_CONST(0xCA353535CACACACA), "[<abc>(!(de)f)]" }, // 475
+ { 6, ABC_CONST(0x0078787878000000), "([(ab)c][(de)f])" }, // 476
+ { 6, ABC_CONST(0x009F9F9F9F000000), "(!([ab]c)[(de)f])" }, // 477
+ { 6, ABC_CONST(0x0096969696000000), "([abc][(de)f])" }, // 478
+ { 6, ABC_CONST(0x00CACACACA000000), "(<abc>[(de)f])" }, // 479
+ { 6, ABC_CONST(0x9F00009F9F9F9F9F), "(!([ab]c)!([de]f))" }, // 480
+ { 6, ABC_CONST(0x609F9F6060606060), "[([ab]c)([de]f)]" }, // 481
+ { 6, ABC_CONST(0x9600009696969696), "([abc]!([de]f))" }, // 482
+ { 6, ABC_CONST(0xCA0000CACACACACA), "(<abc>!([de]f))" }, // 483
+ { 6, ABC_CONST(0xCA3535CACACACACA), "[<abc>([de]f)]" }, // 484
+ { 6, ABC_CONST(0x9600009600969600), "([abc][def])" }, // 485
+ { 6, ABC_CONST(0xCA0000CA00CACA00), "(<abc>[def])" }, // 486
+ { 6, ABC_CONST(0xCACA0000CA00CA00), "(<abc><def>)" }, // 487
+ { 6, ABC_CONST(0x3535CACA35CA35CA), "[<abc><def>]" }, // 488
+ { 6, ABC_CONST(0xCAAAAAAAAAAAAAAA), "<ab(cdef)>" }, // 489
+ { 6, ABC_CONST(0xACCCCCCCAAAAAAAA), "<ab(!(cde)f)>" }, // 490
+ { 6, ABC_CONST(0xACCCCCCCCAAAAAAA), "<ab[(cde)f]>" }, // 491
+ { 6, ABC_CONST(0xACCCAAAAAAAAAAAA), "<ab(!(cd)ef)>" }, // 492
+ { 6, ABC_CONST(0xCAAACCCCAAAAAAAA), "<ab(!(!(cd)e)f)>" }, // 493
+ { 6, ABC_CONST(0xCAAACCCCACCCAAAA), "<ab[(!(cd)e)f]>" }, // 494
+ { 6, ABC_CONST(0xACCCCAAAAAAAAAAA), "<ab([(cd)e]f)>" }, // 495
+ { 6, ABC_CONST(0xCAAAACCCACCCCAAA), "<ab[(cd)ef]>" }, // 496
+ { 6, ABC_CONST(0xACCAAAAAAAAAAAAA), "<ab([cd]ef)>" }, // 497
+ { 6, ABC_CONST(0xCAACCCCCAAAAAAAA), "<ab(!([cd]e)f)>" }, // 498
+ { 6, ABC_CONST(0xCAACCCCCACCAAAAA), "<ab[([cd]e)f]>" }, // 499
+ { 6, ABC_CONST(0xCAACACCAAAAAAAAA), "<ab([cde]f)>" }, // 500
+ { 6, ABC_CONST(0xACCACAACCAACACCA), "<ab[cdef]>" }, // 501
+ { 6, ABC_CONST(0xCCAACACAAAAAAAAA), "<ab(<cde>f)>" }, // 502
+ { 6, ABC_CONST(0xAACCACACCCAACACA), "<ab[<cde>f]>" }, // 503
+ { 6, ABC_CONST(0xAAAAACCCACCCACCC), "<ab(!(cd)!(ef))>" }, // 504
+ { 6, ABC_CONST(0xACCCCAAACAAACAAA), "<ab[(cd)(ef)]>" }, // 505
+ { 6, ABC_CONST(0xAAAAACCAACCAACCA), "<ab([cd]!(ef))>" }, // 506
+ { 6, ABC_CONST(0xAAAAACCAACCAAAAA), "<ab([cd][ef])>" }, // 507
+ { 6, ABC_CONST(0xCCAACACACACACACA), "<ab<cd(ef)>>" }, // 508
+ { 6, ABC_CONST(0xCACACCAACCAACACA), "<ab<cd[ef]>>" }, // 509
+ { 6, ABC_CONST(0xCCCCAAAACAAACAAA), "<ab<(cd)ef>>" }, // 510
+ { 6, ABC_CONST(0xCCCCAAAAACCAACCA), "<ab<[cd]ef>>" }, // 511
+ { 6, ABC_CONST(0xC0AAAAAAAAAAAAAA), "<a(bc)(def)>" }, // 512
+ { 6, ABC_CONST(0xAAC0C0C0AAAAAAAA), "<a(bc)(!(de)f)>" }, // 513
+ { 6, ABC_CONST(0xAAC0C0AAAAAAAAAA), "<a(bc)([de]f)>" }, // 514
+ { 6, ABC_CONST(0x3CAAAAAAAAAAAAAA), "<a[bc](def)>" }, // 515
+ { 6, ABC_CONST(0xAA3C3C3CAAAAAAAA), "<a[bc](!(de)f)>" }, // 516
+ { 6, ABC_CONST(0xAA3C3CAAAAAAAAAA), "<a[bc]([de]f)>" }, // 517
+ { 6, ABC_CONST(0xC000AAAAAAAAAAAA), "<a(bcd)(ef)>" }, // 518
+ { 6, ABC_CONST(0x3F00AAAAAAAAAAAA), "<a(!(bc)d)(ef)>" }, // 519
+ { 6, ABC_CONST(0x3FC0AAAAAAAAAAAA), "<a[(bc)d](ef)>" }, // 520
+ { 6, ABC_CONST(0x3C00AAAAAAAAAAAA), "<a([bc]d)(ef)>" }, // 521
+ { 6, ABC_CONST(0xC33CAAAAAAAAAAAA), "<a[bcd](ef)>" }, // 522
+ { 6, ABC_CONST(0xF0CCAAAAAAAAAAAA), "<a<bcd>(ef)>" }, // 523
+ { 6, ABC_CONST(0xF088888888888888), "<(ab)c(def)>" }, // 524
+ { 6, ABC_CONST(0x88F0F0F088888888), "<(ab)c(!(de)f)>" }, // 525
+ { 6, ABC_CONST(0x88F0F0F0F0888888), "<(ab)c[(de)f]>" }, // 526
+ { 6, ABC_CONST(0x88F0F08888888888), "<(ab)c([de]f)>" }, // 527
+ { 6, ABC_CONST(0xF08888F088F0F088), "<(ab)c[def]>" }, // 528
+ { 6, ABC_CONST(0xF0F08888F088F088), "<(ab)c<def>>" }, // 529
+ { 6, ABC_CONST(0xF066666666666666), "<[ab]c(def)>" }, // 530
+ { 6, ABC_CONST(0x66F0F0F066666666), "<[ab]c(!(de)f)>" }, // 531
+ { 6, ABC_CONST(0x66F0F0F0F0666666), "<[ab]c[(de)f]>" }, // 532
+ { 6, ABC_CONST(0x66F0F06666666666), "<[ab]c([de]f)>" }, // 533
+ { 6, ABC_CONST(0xF06666F066F0F066), "<[ab]c[def]>" }, // 534
+ { 6, ABC_CONST(0xF0F06666F066F066), "<[ab]c<def>>" }, // 535
+ { 6, ABC_CONST(0xF000888888888888), "<(ab)(cd)(ef)>" }, // 536
+ { 6, ABC_CONST(0xF000777777777777), "<!(ab)(cd)(ef)>" }, // 537
+ { 6, ABC_CONST(0x8888F000F0008888), "<(ab)(cd)[ef]>" }, // 538
+ { 6, ABC_CONST(0x7777F000F0007777), "<!(ab)(cd)[ef]>" }, // 539
+ { 6, ABC_CONST(0x0FF0888888888888), "<(ab)[cd](ef)>" }, // 540
+ { 6, ABC_CONST(0xF000666666666666), "<[ab](cd)(ef)>" }, // 541
+ { 6, ABC_CONST(0x6666F000F0006666), "<[ab](cd)[ef]>" }, // 542
+ { 6, ABC_CONST(0x0FF0666666666666), "<[ab][cd](ef)>" }, // 543
+ { 6, ABC_CONST(0x66660FF00FF06666), "<[ab][cd][ef]>" }, // 544
+ { 6, ABC_CONST(0xFF00808080808080), "<(abc)d(ef)>" }, // 545
+ { 6, ABC_CONST(0x8080FF00FF008080), "<(abc)d[ef]>" }, // 546
+ { 6, ABC_CONST(0xFF00707070707070), "<(!(ab)c)d(ef)>" }, // 547
+ { 6, ABC_CONST(0x7070FF00FF007070), "<(!(ab)c)d[ef]>" }, // 548
+ { 6, ABC_CONST(0xFF00787878787878), "<[(ab)c]d(ef)>" }, // 549
+ { 6, ABC_CONST(0x7878FF00FF007878), "<[(ab)c]d[ef]>" }, // 550
+ { 6, ABC_CONST(0xFF00606060606060), "<([ab]c)d(ef)>" }, // 551
+ { 6, ABC_CONST(0x6060FF00FF006060), "<([ab]c)d[ef]>" }, // 552
+ { 6, ABC_CONST(0xFF00969696969696), "<[abc]d(ef)>" }, // 553
+ { 6, ABC_CONST(0x9696FF00FF009696), "<[abc]d[ef]>" }, // 554
+ { 6, ABC_CONST(0xFF00CACACACACACA), "<<abc>d(ef)>" }, // 555
+ { 6, ABC_CONST(0xCACAFF00FF00CACA), "<<abc>d[ef]>" }, // 556
+ { 6, ABC_CONST(0xFF00000080808080), "<(abc)(de)f>" }, // 557
+ { 6, ABC_CONST(0xFF0000007F7F7F7F), "<!(abc)(de)f>" }, // 558
+ { 6, ABC_CONST(0x00FFFF0080808080), "<(abc)[de]f>" }, // 559
+ { 6, ABC_CONST(0xFF00000070707070), "<(!(ab)c)(de)f>" }, // 560
+ { 6, ABC_CONST(0xFF0000008F8F8F8F), "<!(!(ab)c)(de)f>" }, // 561
+ { 6, ABC_CONST(0x00FFFF0070707070), "<(!(ab)c)[de]f>" }, // 562
+ { 6, ABC_CONST(0xFF00000078787878), "<[(ab)c](de)f>" }, // 563
+ { 6, ABC_CONST(0x00FFFF0078787878), "<[(ab)c][de]f>" }, // 564
+ { 6, ABC_CONST(0xFF00000060606060), "<([ab]c)(de)f>" }, // 565
+ { 6, ABC_CONST(0xFF0000009F9F9F9F), "<!([ab]c)(de)f>" }, // 566
+ { 6, ABC_CONST(0x00FFFF0060606060), "<([ab]c)[de]f>" }, // 567
+ { 6, ABC_CONST(0xFF00000096969696), "<[abc](de)f>" }, // 568
+ { 6, ABC_CONST(0x00FFFF0096969696), "<[abc][de]f>" }, // 569
+ { 6, ABC_CONST(0xFF000000CACACACA), "<<abc>(de)f>" }, // 570
+ { 6, ABC_CONST(0x00FFFF00CACACACA), "<<abc>[de]f>" }, // 571
+ { 6, ABC_CONST(0xFFFF000080008000), "<(abcd)ef>" }, // 572
+ { 6, ABC_CONST(0xFFFF00007F007F00), "<(!(abc)d)ef>" }, // 573
+ { 6, ABC_CONST(0xFFFF00007F807F80), "<[(abc)d]ef>" }, // 574
+ { 6, ABC_CONST(0xFFFF000070007000), "<(!(ab)cd)ef>" }, // 575
+ { 6, ABC_CONST(0xFFFF00008F008F00), "<(!(!(ab)c)d)ef>" }, // 576
+ { 6, ABC_CONST(0xFFFF00008F708F70), "<[(!(ab)c)d]ef>" }, // 577
+ { 6, ABC_CONST(0xFFFF000078007800), "<([(ab)c]d)ef>" }, // 578
+ { 6, ABC_CONST(0xFFFF000087788778), "<[(ab)cd]ef>" }, // 579
+ { 6, ABC_CONST(0xFFFF000060006000), "<([ab]cd)ef>" }, // 580
+ { 6, ABC_CONST(0xFFFF00009F009F00), "<(!([ab]c)d)ef>" }, // 581
+ { 6, ABC_CONST(0xFFFF00009F609F60), "<[([ab]c)d]ef>" }, // 582
+ { 6, ABC_CONST(0xFFFF000096009600), "<([abc]d)ef>" }, // 583
+ { 6, ABC_CONST(0xFFFF000069966996), "<[abcd]ef>" }, // 584
+ { 6, ABC_CONST(0xFFFF0000CA00CA00), "<(<abc>d)ef>" }, // 585
+ { 6, ABC_CONST(0xFFFF000035CA35CA), "<[<abc>d]ef>" }, // 586
+ { 6, ABC_CONST(0xFFFF000007770777), "<(!(ab)!(cd))ef>" }, // 587
+ { 6, ABC_CONST(0xFFFF000078887888), "<[(ab)(cd)]ef>" }, // 588
+ { 6, ABC_CONST(0xFFFF000006660666), "<([ab]!(cd))ef>" }, // 589
+ { 6, ABC_CONST(0xFFFF000006600660), "<([ab][cd])ef>" }, // 590
+ { 6, ABC_CONST(0xFFFF0000CAAACAAA), "<<ab(cd)>ef>" }, // 591
+ { 6, ABC_CONST(0xFFFF0000ACCAACCA), "<<ab[cd]>ef>" }, // 592
+ { 6, ABC_CONST(0xFFFF0000F088F088), "<<(ab)cd>ef>" }, // 593
+ { 6, ABC_CONST(0xFFFF0000F066F066), "<<[ab]cd>ef>" } // 594
+};
+
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -42,6 +641,336 @@ ABC_NAMESPACE_IMPL_START
SeeAlso []
***********************************************************************/
+void Mpm_ManPrintDsdStats( Mpm_Man_t * p )
+{
+ int i, Absent = 0;
+
+ for ( i = 0; i < 595; i++ )
+ {
+ if ( p->nCountDsd[i] == 0 )
+ {
+ Absent++;
+ continue;
+ }
+ if ( p->pPars->fVeryVerbose )
+ {
+ printf( "%5d : ", i );
+ printf( "%-20s ", p->pDsd6[i].pStr );
+ printf( "%8d ", p->nCountDsd[i] );
+ printf( "\n" );
+ }
+ }
+ printf( "Unused classes = %d (%.2f %%). Non-DSD cuts = %d (%.2f %%).\n",
+ Absent, 100.0 * Absent / 595,
+ p->nNonDsd, 100.0 * p->nNonDsd / p->nCutsMergedAll );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Hsh_IntMan_t * Mpm_ManBuildHashTable( Vec_Int_t ** pvConfgRes )
+{
+ FILE * pFile;
+ char * pFileName = "dsdfuncs6.dat";
+ int RetValue, size = Extra_FileSize( pFileName ) / 12; // 2866420
+ Vec_Wrd_t * vTruthRes = Vec_WrdAlloc( size );
+ Vec_Int_t * vConfgRes = Vec_IntAlloc( size );
+ Hsh_IntMan_t * pHash;
+
+ pFile = fopen( pFileName, "rb" );
+ RetValue = fread( Vec_WrdArray(vTruthRes), sizeof(word), size, pFile );
+ RetValue = fread( Vec_IntArray(vConfgRes), sizeof(int), size, pFile );
+ vTruthRes->nSize = size;
+ vConfgRes->nSize = size;
+ // create hash table
+ pHash = Hsh_WrdManHashArrayStart( vTruthRes, 1 );
+ // cleanup
+ if ( pvConfgRes )
+ *pvConfgRes = vConfgRes;
+ else
+ Vec_IntFree( vConfgRes );
+ Vec_WrdFree( vTruthRes );
+// Hsh_IntManStop( pHash );
+ return pHash;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Mpm_ManPrintPerm( unsigned s )
+{
+ int i;
+ for ( i = 0; i < 6; i++ )
+ printf( "%d ", (s >> (3*i)) & 7 );
+ printf( " " );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Mpm_ManPrecomputePerms( Mpm_Man_t * p )
+{
+ int nVars = 6;
+ // 0(1:1) 1(2:1) 2(4:2) 3(10:6) 4(33:23) 5(131:98) 6(595:464)
+ int nClasses[7] = { 1, 2, 4, 10, 33, 131, 595 };
+ int nPerms = Extra_Factorial( nVars );
+ int nSwaps = (1 << nVars);
+ int * pComp, * pPerm;
+ int i, k, x, One, OneCopy, Num;
+ Vec_Int_t * vVars;
+ abctime clk = Abc_Clock();
+ assert( p->pDsd6 == NULL );
+ p->pDsd6 = s_DsdClass6;
+ // precompute schedules
+ pComp = Extra_GreyCodeSchedule( nVars );
+ pPerm = Extra_PermSchedule( nVars );
+ // map numbers into perms
+ p->vMap2Perm = Vec_IntStartFull( (1<<(3*nVars)) );
+ // store permutations
+ One = 0;
+ for ( x = 0; x < nVars; x++ )
+ {
+ p->Perm6[0][x] = (char)x;
+ One |= (x << (3*x));
+ }
+// Vec_IntWriteEntry( p->vMap2Perm, One, 0 );
+ OneCopy = One;
+ for ( k = 0; k < nPerms; k++ )
+ {
+ if ( k > 0 )
+ for ( x = 0; x < nVars; x++ )
+ p->Perm6[k][x] = p->Perm6[k-1][x];
+ ABC_SWAP( char, p->Perm6[k][pPerm[k]], p->Perm6[k][pPerm[k]+1] );
+
+ Num = ( (One >> (3*(pPerm[k] ))) ^ (One >> (3*(pPerm[k]+1))) ) & 7;
+ One ^= (Num << (3*(pPerm[k] )));
+ One ^= (Num << (3*(pPerm[k]+1)));
+
+ Vec_IntWriteEntry( p->vMap2Perm, One, k );
+
+// Mpm_ManPrintPerm( One );
+// for ( x = 0; x < nVars; x++ )
+// printf( "%d ", p->Perm6[k][x] );
+// printf( "\n" );
+ }
+ assert( OneCopy == One );
+ // fill in the gaps
+ vVars = Vec_IntAlloc( 6 );
+ Vec_IntForEachEntry( p->vMap2Perm, Num, i )
+ {
+ // mark used variables
+ int Count = 0;
+ One = i;
+ Vec_IntFill( vVars, 6, 0 );
+ for ( k = 0; k < nVars; k++ )
+ {
+ int iVar = ((One >> (3*k)) & 7);
+ if ( iVar >= nVars && iVar < 7 )
+ break;
+ if ( iVar != 7 )
+ {
+ if ( Vec_IntEntry( vVars, iVar ) == 1 )
+ break;
+ Vec_IntWriteEntry( vVars, iVar, 1 );
+ Count++;
+ }
+ }
+ // skip ones with dups and complete
+ if ( k < nVars || Count == nVars )
+ continue;
+ // find unused variables
+ for ( x = k = 0; k < 6; k++ )
+ if ( Vec_IntEntry(vVars, k) == 0 )
+ Vec_IntWriteEntry( vVars, x++, k );
+ Vec_IntShrink( vVars, x );
+ // fill in used variables
+ x = 0;
+ for ( k = 0; k < nVars; k++ )
+ {
+ int iVar = ((One >> (3*k)) & 7);
+ if ( iVar == 7 )
+ One ^= ((Vec_IntEntry(vVars, x++) ^ 7) << (3*k));
+ }
+ assert( x == Vec_IntSize(vVars) );
+ // save this one
+ assert( Vec_IntEntry( p->vMap2Perm, One ) != -1 );
+ Vec_IntWriteEntry( p->vMap2Perm, i, Vec_IntEntry(p->vMap2Perm, One) );
+/*
+ // mapping
+ Mpm_ManPrintPerm( i );
+ printf( "-> " );
+ Mpm_ManPrintPerm( One );
+ printf( "\n" );
+*/
+ }
+ Vec_IntFree( vVars );
+
+ // store permuted truth tables
+ assert( p->vPerm6 == NULL );
+ p->vPerm6 = Vec_WrdAlloc( nPerms * 595 );
+ for ( i = 0; i < nClasses[nVars]; i++ )
+ {
+ word uTruth = s_DsdClass6[i].uTruth;
+ for ( k = 0; k < nPerms; k++ )
+ {
+ uTruth = Abc_Tt6SwapAdjacent( uTruth, pPerm[k] );
+ Vec_WrdPush( p->vPerm6, uTruth );
+ }
+ assert( uTruth == s_DsdClass6[i].uTruth );
+ }
+ ABC_FREE( pPerm );
+ ABC_FREE( pComp );
+ // build hash table
+ p->pHash = Mpm_ManBuildHashTable( &p->vConfgRes );
+ Abc_PrintTime( 1, "Setting up DSD information", Abc_Clock() - clk );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+word Mpm_CutTruthFromDsd( Mpm_Man_t * pMan, Mpm_Cut_t * pCut, int iClass )
+{
+ int i;
+ word uTruth = pMan->pDsd6[iClass].uTruth;
+ assert( pMan->pDsd6[iClass].nVars == (int)pCut->nLeaves );
+ for ( i = 0; i < (int)pCut->nLeaves; i++ )
+ if ( Abc_LitIsCompl(pCut->pLeaves[i]) )
+ uTruth = Abc_Tt6Flip( uTruth, i );
+ return uTruth;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Mpm_CutComputeDsd6( Mpm_Man_t * p, Mpm_Cut_t * pCut, Mpm_Cut_t * pCut0, Mpm_Cut_t * pCut1, Mpm_Cut_t * pCutC, int fCompl0, int fCompl1, int fComplC, int Type )
+{
+ int fVerbose = 0;
+ if ( pCutC == NULL )
+ {
+ int pLeavesNew[6] = { -1, -1, -1, -1, -1, -1 };
+ char * pPerm6;
+ word t0, t1, t = 0;
+ int i, Entry, Config, iClass, fCompl = 0;
+ int iClass0 = Abc_Lit2Var(pCut0->iFunc);
+ int iClass1 = Abc_Lit2Var(pCut1->iFunc);
+ word Truth0 = p->pDsd6[iClass0].uTruth;
+ word Truth1 = p->pDsd6[iClass1].uTruth;
+ int Perm1 = Vec_IntEntry( p->vMap2Perm, p->uPermMask[1] );
+ word Truth1p = Vec_WrdEntry( p->vPerm6, iClass1 * 720 + Perm1 );
+ if ( p->uComplMask[1] )
+ {
+ for ( i = 0; i < 6; i++ )
+ if ( (p->uComplMask[1] >> i) & 1 )
+ Truth1p = Abc_Tt6Flip( Truth1p, i );
+ }
+ t0 = (fCompl0 ^ pCut0->fCompl ^ Abc_LitIsCompl(pCut0->iFunc)) ? ~Truth0 : Truth0;
+ t1 = (fCompl1 ^ pCut1->fCompl ^ Abc_LitIsCompl(pCut1->iFunc)) ? ~Truth1p : Truth1p;
+ if ( Type == 1 )
+ t = t0 & t1;
+ else if ( Type == 2 )
+ t = t0 ^ t1;
+ else assert( 0 );
+ if ( t & 1 )
+ {
+ fCompl = 1;
+ t = ~t;
+ }
+
+if ( fVerbose )
+{
+Mpm_ManPrintPerm( p->uPermMask[1] ); printf( "\n" );
+Kit_DsdPrintFromTruth( (unsigned *)&Truth0, 6 ); printf( "\n" );
+Kit_DsdPrintFromTruth( (unsigned *)&Truth1, 6 ); printf( "\n" );
+Kit_DsdPrintFromTruth( (unsigned *)&Truth1p, 6 ); printf( "\n" );
+Kit_DsdPrintFromTruth( (unsigned *)&t, 6 ); printf( "\n" );
+}
+
+ Entry = *Hsh_IntManLookup( p->pHash, (unsigned *)&t );
+ if ( Entry == -1 )
+ {
+ p->nNonDsd++;
+ return 0;
+ }
+ Config = Vec_IntEntry( p->vConfgRes, Entry );
+ if ( Config & (1 << 16) )
+ fCompl ^= 1;
+ iClass = Config >> 17;
+ pCut->iFunc = Abc_Var2Lit( iClass, fCompl );
+ Config &= 0xFFFF;
+ assert( (Config >> 6) < 720 );
+ pPerm6 = p->Perm6[Config >> 6];
+
+if ( fVerbose )
+{
+Mpm_CutPrint( pCut0 );
+Mpm_CutPrint( pCut1 );
+Mpm_CutPrint( pCut );
+}
+
+ for ( i = 0; i < (int)pCut->nLeaves; i++ )
+ pLeavesNew[pPerm6[i]] = Abc_LitNotCond( pCut->pLeaves[i], (Config >> i) & 1 );
+ pCut->nLeaves = p->pDsd6[iClass].nVars;
+// for ( i = 0; i < (int)pCut->nLeaves; i++ )
+// assert( pLeavesNew[i] != -1 );
+ for ( i = 0; i < (int)pCut->nLeaves; i++ )
+ pCut->pLeaves[i] = pLeavesNew[i];
+
+ p->nCountDsd[iClass]++;
+ p->nSmallSupp += (int)(pCut->nLeaves < 2);
+
+if ( fVerbose )
+{
+printf( "Computed " );
+Mpm_CutPrint( pCut );
+printf( "\n" );
+}
+ }
+ else
+ {
+ assert( 0 );
+ }
+ return 1;
+}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
diff --git a/src/map/mpm/mpmInt.h b/src/map/mpm/mpmInt.h
index e64aa43b..b7e600ee 100644
--- a/src/map/mpm/mpmInt.h
+++ b/src/map/mpm/mpmInt.h
@@ -34,6 +34,7 @@
//#include "misc/tim/tim.h"
#include "misc/vec/vec.h"
#include "misc/vec/vecMem.h"
+#include "misc/vec/vecHsh.h"
#include "misc/mem/mem2.h"
#include "mpmMig.h"
#include "mpm.h"
@@ -78,6 +79,14 @@ struct Mpm_Uni_t_
int Data[MPM_VAR_MAX]; // padding
};
+typedef struct Mpm_Dsd_t_ Mpm_Dsd_t;
+struct Mpm_Dsd_t_
+{
+ int nVars; // support size
+ word uTruth; // truth table
+ char * pStr; // description
+};
+
typedef struct Mpm_Man_t_ Mpm_Man_t;
struct Mpm_Man_t_
{
@@ -111,14 +120,19 @@ struct Mpm_Man_t_
int nCuts[3]; // fanin cut counts
Mpm_Cut_t * pCuts[3][MPM_CUT_MAX+1]; // fanin cuts
word pSigns[3][MPM_CUT_MAX+1]; // fanin cut signatures
- // functionality
-// Dsd_Man_t * pManDsd;
- void * pManDsd;
- int pPerm[MPM_VAR_MAX];
+ // truth tables
Vec_Mem_t * vTtMem; // truth table memory and hash table
int funcCst0; // constant 0
int funcVar0; // variable 0
+ // DSD
+ Mpm_Dsd_t * pDsd6; // NPN class information
+ Hsh_IntMan_t * pHash; // maps DSD functions into NPN classes
+ Vec_Int_t * vConfgRes; // configurations
+ Vec_Wrd_t * vPerm6; // permutations of DSD classes
+ char Perm6[720][6]; // permutations
+ Vec_Int_t * vMap2Perm; // maps number into its permutation
unsigned uPermMask[3];
+ unsigned uComplMask[3];
// mapping attributes
Vec_Int_t vCutBests; // cut best
Vec_Int_t vCutLists; // cut list
@@ -129,8 +143,11 @@ struct Mpm_Man_t_
Vec_Int_t vTimes; // arrival time
Vec_Int_t vAreas; // area
Vec_Int_t vEdges; // edge
+ int nCountDsd[600];
+ int nNonDsd;
// statistics
int nCutsMerged;
+ int nCutsMergedAll;
int nSmallSupp;
abctime timeFanin;
abctime timeDerive;
@@ -212,15 +229,22 @@ extern void Mpm_ManStop( Mpm_Man_t * p );
extern void Mpm_ManPrintStatsInit( Mpm_Man_t * p );
extern void Mpm_ManPrintStats( Mpm_Man_t * p );
/*=== mpmDsd.c ===========================================================*/
+extern void Mpm_ManPrintDsdStats( Mpm_Man_t * p );
+extern void Mpm_ManPrintPerm( unsigned s );
+extern void Mpm_ManPrecomputePerms( Mpm_Man_t * p );
+extern word Mpm_CutTruthFromDsd( Mpm_Man_t * pMan, Mpm_Cut_t * pCut, int iDsdLit );
+extern int Mpm_CutComputeDsd6( Mpm_Man_t * p, Mpm_Cut_t * pCut, Mpm_Cut_t * pCut0, Mpm_Cut_t * pCut1, Mpm_Cut_t * pCutC, int fCompl0, int fCompl1, int fComplC, int Type );
/*=== mpmLib.c ===========================================================*/
extern Mpm_LibLut_t * Mpm_LibLutSetSimple( int nLutSize );
extern void Mpm_LibLutFree( Mpm_LibLut_t * pLib );
/*=== mpmMap.c ===========================================================*/
+extern void Mpm_CutPrint( Mpm_Cut_t * pCut );
extern void Mpm_ManPrepare( Mpm_Man_t * p );
extern void Mpm_ManPerform( Mpm_Man_t * p );
/*=== mpmTruth.c ===========================================================*/
extern int Mpm_CutComputeTruth6( Mpm_Man_t * p, Mpm_Cut_t * pCut, Mpm_Cut_t * pCut0, Mpm_Cut_t * pCut1, Mpm_Cut_t * pCutC, int fCompl0, int fCompl1, int fComplC, int Type );
+extern void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars );
ABC_NAMESPACE_HEADER_END
diff --git a/src/map/mpm/mpmMan.c b/src/map/mpm/mpmMan.c
index 6e4ce28a..98caa7df 100644
--- a/src/map/mpm/mpmMan.c
+++ b/src/map/mpm/mpmMan.c
@@ -57,7 +57,6 @@ Mpm_Man_t * Mpm_ManStart( Mig_Man_t * pMig, Mpm_Par_t * pPars )
p->nLutSize = pPars->pLib->LutMax;
p->nTruWords = pPars->fUseTruth ? Abc_Truth6WordNum(p->nLutSize) : 0;
p->nNumCuts = pPars->nNumCuts;
- p->timeTotal = Abc_Clock();
// cuts
assert( Mpm_CutWordNum(32) < 32 ); // using 5 bits for word count
p->pManCuts = Mmr_StepStart( 13, Abc_Base2Log(Mpm_CutWordNum(p->nLutSize) + 1) );
@@ -79,10 +78,9 @@ Mpm_Man_t * Mpm_ManStart( Mig_Man_t * pMig, Mpm_Par_t * pPars )
Vec_IntFill( &p->vAreas, Mig_ManObjNum(pMig), 0 );
Vec_IntFill( &p->vEdges, Mig_ManObjNum(pMig), 0 );
// start DSD manager
- p->pManDsd = NULL;
- pMig->pMan = p;
+ assert( !p->pPars->fUseTruth || !p->pPars->fUseDsd );
if ( p->pPars->fUseTruth )
- {
+ {
word Truth = 0;
p->vTtMem = Vec_MemAlloc( p->nTruWords, 12 ); // 32 KB/page for 6-var functions
Vec_MemHashAlloc( p->vTtMem, 10000 );
@@ -90,8 +88,14 @@ Mpm_Man_t * Mpm_ManStart( Mig_Man_t * pMig, Mpm_Par_t * pPars )
Truth = ABC_CONST(0xAAAAAAAAAAAAAAAA);
p->funcVar0 = Vec_MemHashInsert( p->vTtMem, &Truth );
}
- else
+ else if ( p->pPars->fUseDsd )
+ {
+ Mpm_ManPrecomputePerms( p );
p->funcVar0 = 1;
+ }
+ // finish
+ p->timeTotal = Abc_Clock();
+ pMig->pMan = p;
return p;
}
@@ -108,11 +112,21 @@ Mpm_Man_t * Mpm_ManStart( Mig_Man_t * pMig, Mpm_Par_t * pPars )
***********************************************************************/
void Mpm_ManStop( Mpm_Man_t * p )
{
+ if ( p->pPars->fUseDsd )
+ Mpm_ManPrintDsdStats( p );
if ( p->vTtMem )
{
Vec_MemHashFree( p->vTtMem );
Vec_MemFree( p->vTtMem );
}
+ if ( p->pHash )
+ {
+ Vec_WrdFree( p->vPerm6 );
+ Vec_IntFree( p->vMap2Perm );
+ Vec_IntFree( p->vConfgRes );
+ Vec_IntFree( p->pHash->vData );
+ Hsh_IntManStop( p->pHash );
+ }
Vec_PtrFree( p->vTemp );
Mmr_StepStop( p->pManCuts );
ABC_FREE( p->vObjPresUsed.pArray );
@@ -145,11 +159,11 @@ void Mpm_ManStop( Mpm_Man_t * p )
***********************************************************************/
void Mpm_ManPrintStatsInit( Mpm_Man_t * p )
{
- printf( "K = %d. C = %d. Cands = %d. XOR = %d. MUX = %d. Choices = %d. CutMin = %d. Truth = %d.\n",
+ printf( "K = %d. C = %d. Cand = %d. XOR = %d. MUX = %d. Choice = %d. CutMin = %d. Truth = %d. DSD = %d.\n",
p->nLutSize, p->nNumCuts,
Mig_ManCiNum(p->pMig) + Mig_ManNodeNum(p->pMig),
Mig_ManXorNum(p->pMig), Mig_ManMuxNum(p->pMig), 0,
- p->pPars->fCutMin, p->pPars->fUseTruth );
+ p->pPars->fCutMin, p->pPars->fUseTruth, p->pPars->fUseDsd );
}
void Mpm_ManPrintStats( Mpm_Man_t * p )
{
diff --git a/src/map/mpm/mpmMap.c b/src/map/mpm/mpmMap.c
index 1a869584..96861e33 100644
--- a/src/map/mpm/mpmMap.c
+++ b/src/map/mpm/mpmMap.c
@@ -31,63 +31,6 @@ ABC_NAMESPACE_IMPL_START
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
-/*
- // check special cases
- if ( fUseFunc )
- {
- pCut0 = p->pCuts[0][0]; pCut1 = p->pCuts[1][0];
- if ( pCut0->iFunc < 2 || pCut1->iFunc < 2 )
- {
- assert( Mig_ObjIsAnd(pObj) );
- if ( Abc_LitNotCond(pCut0->iFunc, Mig_ObjFaninC0(pObj)) == 0 ||
- Abc_LitNotCond(pCut1->iFunc, Mig_ObjFaninC1(pObj)) == 0 ) // set the resulting cut to 0
- Mig_ManObj(p, pObj)->hCutList = Mpm_CutCreateZero( p, pObj );
- else if ( Abc_LitNotCond(pCut0->iFunc, Mig_ObjFaninC0(pObj)) == 1 ) // set the resulting set to be that of Fanin1
- Mig_ManObj(p, pObj)->hCutList = Mpm_CutCopySet( p, Mig_ObjFanin1(pObj), 0 );
- else if ( Abc_LitNotCond(pCut1->iFunc, Mig_ObjFaninC1(pObj)) == 1 ) // set the resulting set to be that of Fanin0
- Mig_ManObj(p, pObj)->hCutList = Mpm_CutCopySet( p, Mig_ObjFanin0(pObj), 0 );
- else assert( 0 );
- goto finish;
- }
- }
- // compute cut function
- if ( fUseFunc )
- {
- extern int Mpm_FuncCompute( void * p, int iDsd0, int iDsd1, Vec_Str_t * vShared, int * pPerm, int * pnLeaves );
- int nLeavesOld = p->pCutTemp->nLeaves;
- int nLeaves = p->pCutTemp->nLeaves;
- iDsd0 = Abc_LitNotCond( pCut0->iFunc, Mig_ObjFaninC0(pObj) );
- iDsd1 = Abc_LitNotCond( pCut1->iFunc, Mig_ObjFaninC1(pObj) );
- if ( iDsd0 > iDsd1 )
- {
- ABC_SWAP( int, iDsd0, iDsd1 );
- ABC_SWAP( Mpm_Cut_t *, pCut0, pCut1 );
- }
- // compute functionality and filter cuts dominated by support-reduced cuts
- p->pCutTemp->iFunc = Mpm_FuncCompute( p->pManDsd, iDsd0, iDsd1, &p->vObjShared, p->pPerm, &nLeaves );
- Mpm_ObjUpdateCut( p->pCutTemp, p->pPerm, nLeaves );
- // consider filtering based on functionality
- if ( nLeaves == 0 ) // derived const cut
- {
- Mig_ManObj(p, pObj)->hCutList = Mpm_CutCreateZero( p, pObj );
- goto finish;
- }
- if ( nLeaves == 1 ) // derived unit cut
- {
- pFanin = Mig_ManObj( p->pMig, Abc_Lit2Var(p->pCutTemp->pLeaves[0]) );
- Mig_ManObj(p, pObj)->hCutList = Mpm_CutCopySet( p, pFanin, Abc_LitIsCompl(p->pCutTemp->pLeaves[0]) );
- goto finish;
- }
- if ( nLeaves < nLeavesOld ) // reduced support of the cut
- {
- ArrTime = Mpm_CutGetArrTime( p, p->pCutTemp );
- if ( ArrTime > pMapObj->mRequired )
- continue;
- }
- }
-*/
-
-
/**Function*************************************************************
Synopsis [Cut manipulation.]
@@ -170,7 +113,7 @@ static inline void Mpm_CutDeref( Mpm_Man_t * p, int * pLeaves, int nLeaves )
Mig_ManObj( p->pMig, Abc_Lit2Var(pLeaves[i]) )->nMapRefs--;
}
*/
-static inline void Mpm_CutPrint( Mpm_Cut_t * pCut )
+void Mpm_CutPrint( Mpm_Cut_t * pCut )
{
int i;
printf( "%d : { ", pCut->nLeaves );
@@ -509,6 +452,14 @@ static inline int Mpm_ObjDeriveCut( Mpm_Man_t * p, Mpm_Cut_t ** pCuts, Mpm_Cut_t
p->pObjPres[p->vObjPresUsed.pArray[i]] = (unsigned char)0xFF;
Vec_IntClear(&p->vObjPresUsed);
Vec_StrClear(&p->vObjShared);
+/*
+ if ( pCuts[0]->nLeaves == 5 && pCuts[1]->nLeaves == 5 )
+ {
+ int s = 0;
+ Mpm_CutPrint( pCuts[0] );
+ Mpm_CutPrint( pCuts[1] );
+ }
+*/
// check present objects
// for ( i = 0; i < Mig_ManObjNum(p->pMig); i++ )
// assert( p->pObjPres[i] == (unsigned char)0xFF );
@@ -524,23 +475,32 @@ static inline int Mpm_ObjDeriveCut( Mpm_Man_t * p, Mpm_Cut_t ** pCuts, Mpm_Cut_t
// remaining cuts
for ( c = 1; pCuts[c] && c < 3; c++ )
{
+ p->uPermMask[c] = 0x3FFFF; // 18 bits
+ p->uComplMask[c] = 0;
for ( i = 0; i < (int)pCuts[c]->nLeaves; i++ )
{
iObj = Abc_Lit2Var(pCuts[c]->pLeaves[i]);
- if ( p->pObjPres[iObj] != (unsigned char)0xFF )
- continue;
- if ( (int)pCut->nLeaves == p->nLutSize )
- return 0;
- Vec_IntPush( &p->vObjPresUsed, iObj );
- p->pObjPres[iObj] = pCut->nLeaves;
- pCut->pLeaves[pCut->nLeaves++] = pCuts[c]->pLeaves[i];
+ if ( p->pObjPres[iObj] == (unsigned char)0xFF )
+ {
+ if ( (int)pCut->nLeaves == p->nLutSize )
+ return 0;
+ Vec_IntPush( &p->vObjPresUsed, iObj );
+ p->pObjPres[iObj] = pCut->nLeaves;
+ pCut->pLeaves[pCut->nLeaves++] = pCuts[c]->pLeaves[i];
+ }
+ p->uPermMask[c] ^= (((i & 7) ^ 7) << (3*p->pObjPres[iObj]));
+ assert( Abc_Lit2Var(pCuts[c]->pLeaves[i]) == Abc_Lit2Var(pCut->pLeaves[p->pObjPres[iObj]]) );
+ if ( pCuts[c]->pLeaves[i] != pCut->pLeaves[p->pObjPres[iObj]] )
+ p->uComplMask[c] |= (1 << p->pObjPres[iObj]);
}
+// Mpm_ManPrintPerm( p->uPermMask[c] ); printf( "\n" );
}
pCut->hNext = 0;
pCut->iFunc = 0; pCut->iFunc = ~pCut->iFunc;
pCut->fUseless = 0;
pCut->fCompl = 0;
p->nCutsMerged++;
+ p->nCutsMergedAll++;
if ( p->pPars->fUseTruth )
Vec_IntSelectSort( pCut->pLeaves, pCut->nLeaves );
return 1;
@@ -566,6 +526,11 @@ p->timeMerge += clock() - clk;
// derive truth table
if ( p->pPars->fUseTruth )
Mpm_CutComputeTruth6( p, pCut, pCuts[0], pCuts[1], pCuts[2], Mig_ObjFaninC0(pObj), Mig_ObjFaninC1(pObj), Mig_ObjFaninC2(pObj), Mig_ObjNodeType(pObj) );
+ else if ( p->pPars->fUseDsd )
+ {
+ if ( !Mpm_CutComputeDsd6( p, pCut, pCuts[0], pCuts[1], pCuts[2], Mig_ObjFaninC0(pObj), Mig_ObjFaninC1(pObj), Mig_ObjFaninC2(pObj), Mig_ObjNodeType(pObj) ) )
+ return 1;
+ }
#ifdef MIG_RUNTIME
p->timeMerge += clock() - clk;
@@ -587,8 +552,21 @@ clk = Abc_Clock();
p->timeStore += Abc_Clock() - clk;
#endif
- return 1;
// return 0 if const or buffer cut is derived - reset all cuts to contain only one
+// if ( pCut->nLeaves < 2 && p->nCutStore == 1 )
+// return 0;
+/*
+ if ( pCut->nLeaves < 2 )
+ {
+ int i;
+ assert( p->nCutStore >= 1 );
+ for ( i = 1; i < p->nCutStore; i++ )
+ Vec_PtrPush( &p->vFreeUnits, p->pCutStore[i] );
+ p->nCutStore = 1;
+ return 0;
+ }
+*/
+ return 1;
}
int Mpm_ManDeriveCuts( Mpm_Man_t * p, Mig_Obj_t * pObj )
{
diff --git a/src/map/mpm/mpmPre.c b/src/map/mpm/mpmPre.c
index bb6bf41c..72990540 100644
--- a/src/map/mpm/mpmPre.c
+++ b/src/map/mpm/mpmPre.c
@@ -172,19 +172,32 @@ void Ifd_ObjPrint( Ifd_Man_t * p, int iLit )
{
int Counter = 0;
if ( iLit == 0 )
- { printf( "0\n" ); return; }
+ { printf( "0" ); return; }
if ( iLit == 1 )
- { printf( "1\n" ); return; }
+ { printf( "1" ); return; }
Ifd_ObjPrint_rec( p, iLit, &Counter, 1 );
- printf( "\n" );
}
-void Ifd_ManPrint( Ifd_Man_t * p )
+void Ifd_ManPrint2( Ifd_Man_t * p )
{
int i;
for ( i = 0; i < p->nObjs; i++ )
{
printf( "%4d : ", i );
Ifd_ObjPrint( p, Abc_Var2Lit( i, 0 ) );
+ printf( "\n" );
+ }
+}
+void Ifd_ManPrint( Ifd_Man_t * p )
+{
+ int i;
+ for ( i = 0; i < p->nObjs; i++ )
+ {
+ word Fun = Vec_WrdEntry( p->vTruths, i );
+ printf( " { %d, ABC_CONST(", Extra_TruthSupportSize((unsigned *)&Fun, 6) );
+ Extra_PrintHex( stdout, (unsigned *)&Fun, 6 );
+ printf( "), \"" );
+ Ifd_ObjPrint( p, Abc_Var2Lit( i, 0 ) );
+ printf( "\" }, // %4d \n", i );
}
}
@@ -532,6 +545,7 @@ void Ifd_ManDsdTest2()
int iLit = Ifd_ManFindDsd( pMan, p );
Ifd_ObjPrint( pMan, iLit );
Ifd_ManStop( pMan );
+ printf( "\n" );
}
/**Function*************************************************************
@@ -600,8 +614,8 @@ Vec_Wrd_t * Ifd_ManDsdTruths( int nVars )
// bookmark
Vec_IntPush( pMan->vMarks, pMan->nObjs );
}
-// Ifd_ManPrint( pMan );
Ifd_ManTruthAll( pMan );
+// Ifd_ManPrint( pMan );
vTruths = pMan->vTruths; pMan->vTruths = NULL;
Ifd_ManStop( pMan );
return vTruths;
@@ -753,25 +767,26 @@ Vec_Wrd_t * Extra_Truth6AllConfigs( word t, int * pComp, int * pPerm, int nVars
int nPerms = Extra_Factorial( nVars );
int nSwaps = (1 << nVars);
Vec_Wrd_t * vTruths = Vec_WrdStart( nPerms * nSwaps );
- word tCur, tTemp1, tTemp2;
- int i, p, c;
- for ( i = 1; i < 2; i++ )
+ word tCur = t, tTemp1, tTemp2;
+ int p, c, Config;
+
+ tTemp1 = tCur;
+ for ( p = 0; p < nPerms; p++ )
{
- tCur = i ? ~t : t;
- tTemp1 = tCur;
- for ( p = 0; p < nPerms; p++ )
+ tCur = Extra_Truth6SwapAdjacent( tCur, pPerm[p] );
+ Config = 0;
+ tTemp2 = tCur;
+ for ( c = 0; c < nSwaps; c++ )
{
- tTemp2 = tCur;
- for ( c = 0; c < nSwaps; c++ )
- {
- Vec_WrdWriteEntry( vTruths, (p << (nVars))|c, tCur );
- tCur = Extra_Truth6ChangePhase( tCur, pComp[c] );
- }
- assert( tTemp2 == tCur );
- tCur = Extra_Truth6SwapAdjacent( tCur, pPerm[p] );
+ Vec_WrdWriteEntry( vTruths, (p << nVars)|Config, tCur );
+ tCur = Extra_Truth6ChangePhase( tCur, pComp[c] );
+ Config ^= (1 << pComp[c]);
}
- assert( tTemp1 == tCur );
+ assert( Config == 0 );
+ assert( tTemp2 == tCur );
}
+ assert( tTemp1 == tCur );
+
if ( t )
{
int i;
@@ -793,7 +808,7 @@ Vec_Wrd_t * Extra_Truth6AllConfigs( word t, int * pComp, int * pPerm, int nVars
SeeAlso []
***********************************************************************/
-int Ifd_ManDsdTest33()
+int Ifd_ManDsdTest()
{
int nVars = 6;
FILE * pFile;
@@ -801,6 +816,7 @@ int Ifd_ManDsdTest33()
Vec_Wrd_t * vTruths = Ifd_ManDsdTruths( nVars );
Vec_Wrd_t * vVariants;
Vec_Int_t * vUniques;
+ Vec_Int_t * vCompls;
Vec_Wrd_t * vTruthRes = Vec_WrdAlloc( 4000000 );
Vec_Int_t * vConfgRes = Vec_IntAlloc( 4000000 );
int * pComp, * pPerm;
@@ -808,19 +824,29 @@ int Ifd_ManDsdTest33()
int i, k, Uniq, Runner, Counter = 0;
assert( nVars >= 3 && nVars <= 6 );
assert( Vec_WrdSize(vTruths) < (1<<10) );
+ vCompls = Vec_IntAlloc( 720 * 64 );
pComp = Extra_GreyCodeSchedule( nVars );
pPerm = Extra_PermSchedule( nVars );
Vec_WrdForEachEntry( vTruths, Truth, i )
{
vVariants = Extra_Truth6AllConfigs( Truth, pComp, pPerm, nVars );
+ // save compl bits
+ Vec_IntClear( vCompls );
+ Vec_WrdForEachEntry( vVariants, Variant, k )
+ {
+ Vec_IntPush( vCompls, (int)(Variant & 1) );
+ Vec_WrdWriteEntry( vVariants, k, Variant & 1 ? ~Variant : Variant );
+ }
+ // uniqify
vUniques = Hsh_WrdManHashArray( vVariants, 1 );
Runner = 0;
Vec_IntForEachEntry( vUniques, Uniq, k )
if ( Runner == Uniq )
{
Variant = Vec_WrdEntry(vVariants, k);
+ assert( (Variant & 1) == 0 );
Vec_WrdPush( vTruthRes, Variant );
- Vec_IntPush( vConfgRes, (Extra_TruthSupportSize((unsigned *)&Variant, 6)<<26)|(i << 16)|k );
+ Vec_IntPush( vConfgRes, (i << 17)|(Vec_IntEntry(vCompls, k) << 16)|k );
Runner++;
}
Vec_IntUniqify( vUniques );
@@ -829,7 +855,8 @@ int Ifd_ManDsdTest33()
//printf( "%5d : ", i ); Kit_DsdPrintFromTruth( &Truth, nVars ), printf( " " ), Vec_IntPrint( vUniques ), printf( "\n" );
Vec_IntFree( vUniques );
Vec_WrdFree( vVariants );
- }
+ }
+ Vec_IntFree( vCompls );
Vec_WrdFree( vTruths );
ABC_FREE( pPerm );
ABC_FREE( pComp );
@@ -847,12 +874,12 @@ int Ifd_ManDsdTest33()
return 1;
}
-int Ifd_ManDsdTest()
+int Ifd_ManDsdTest33()
{
abctime clk = Abc_Clock();
FILE * pFile;
char * pFileName = "dsdfuncs6.dat";
- int RetValue, size = Extra_FileSize( pFileName ) / 12; // 3504275
+ int RetValue, size = Extra_FileSize( pFileName ) / 12; // 2866420
Vec_Wrd_t * vTruthRes = Vec_WrdAlloc( size + 1 );
Vec_Int_t * vConfgRes = Vec_IntAlloc( size );
Hsh_IntMan_t * pHash;
diff --git a/src/map/mpm/mpmTruth.c b/src/map/mpm/mpmTruth.c
index 136b655c..481c6c94 100644
--- a/src/map/mpm/mpmTruth.c
+++ b/src/map/mpm/mpmTruth.c
@@ -94,6 +94,7 @@ static inline word Mpm_TruthStretch6( word Truth, Mpm_Cut_t * pCut, Mpm_Cut_t *
}
return Truth;
}
+//#define MPM_TRY_NEW
int Mpm_CutComputeTruth6( Mpm_Man_t * p, Mpm_Cut_t * pCut, Mpm_Cut_t * pCut0, Mpm_Cut_t * pCut1, Mpm_Cut_t * pCutC, int fCompl0, int fCompl1, int fComplC, int Type )
{
word * pTruth0 = Mpm_CutTruth( p, Abc_Lit2Var(pCut0->iFunc) );
@@ -129,9 +130,10 @@ int Mpm_CutComputeTruth6( Mpm_Man_t * p, Mpm_Cut_t * pCut, Mpm_Cut_t * pCut0, Mp
#ifdef MPM_TRY_NEW
{
+ extern unsigned Abc_TtCanonicize( word * pTruth, int nVars, char * pCanonPerm );
word tCopy = t;
char pCanonPerm[16];
- Abc_TtCanonicize( &tCopy, pCut->nLimit, pCanonPerm );
+ Abc_TtCanonicize( &tCopy, p->nLutSize, pCanonPerm );
}
#endif
diff --git a/src/misc/vec/vecHsh.h b/src/misc/vec/vecHsh.h
index a613c68b..34a6c993 100644
--- a/src/misc/vec/vecHsh.h
+++ b/src/misc/vec/vecHsh.h
@@ -210,9 +210,18 @@ static inline Vec_Int_t * Hsh_WrdManHashArray( Vec_Wrd_t * vDataW, int nSize )
static inline Hsh_IntMan_t * Hsh_WrdManHashArrayStart( Vec_Wrd_t * vDataW, int nSize )
{
Hsh_IntMan_t * p;
- Vec_Int_t Data = { 2*Vec_WrdCap(vDataW), 2*Vec_WrdSize(vDataW), (int *)Vec_WrdArray(vDataW) };
- Vec_Int_t * vData = &Data;
- int i, nEntries = Vec_IntSize(vData) / (2*nSize);
+ int i, nEntries = Vec_WrdSize(vDataW) / nSize;
+ Vec_Int_t * vData = Vec_IntAlloc( 2*Vec_WrdSize(vDataW) );
+ memcpy( Vec_IntArray(vData), Vec_WrdArray(vDataW), sizeof(word)*Vec_WrdSize(vDataW) );
+ vData->nSize = 2*Vec_WrdSize(vDataW);
+/*
+ for ( i = 0; i < 30; i++ )
+ {
+ extern void Extra_PrintHex( FILE * pFile, unsigned * pTruth, int nVars );
+ Extra_PrintHex( stdout, (unsigned *) Vec_WrdEntryP(vDataW, i), 6 ); printf( " " );
+ Kit_DsdPrintFromTruth( (unsigned *) Vec_WrdEntryP(vDataW, i), 6 ); printf( "\n" );
+ }
+*/
assert( Vec_IntSize(vData) % (2*nSize) == 0 );
p = Hsh_IntManStart( vData, (2*nSize), nEntries );
for ( i = 0; i < nEntries; i++ )
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-01 08:08:58 +0000