summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2017-12-28 23:04:24 -0800
committerAlan Mishchenko <alanmi@berkeley.edu>2017-12-28 23:04:24 -0800
commit7d7ce3ecd03059602f70f26612aabd4a2ec49422 (patch)
treeb811916386ecfb045cc08f9be78a43a2f0307f30
parentc3dccf3020e467da9fa62c9f609bce86b55ccd0a (diff)
downloadabc-7d7ce3ecd03059602f70f26612aabd4a2ec49422.tar.gz
abc-7d7ce3ecd03059602f70f26612aabd4a2ec49422.tar.bz2
abc-7d7ce3ecd03059602f70f26612aabd4a2ec49422.zip
New exact synthesis command 'allexact'.
-rw-r--r--abclib.dsp4
-rw-r--r--src/base/abci/abc.c171
-rw-r--r--src/sat/bmc/bmc.h27
-rw-r--r--src/sat/bmc/bmcMaj.c24
-rw-r--r--src/sat/bmc/bmcMaj2.c24
-rw-r--r--src/sat/bmc/bmcMaj3.c1098
-rw-r--r--src/sat/bmc/module.make1
-rw-r--r--src/sat/glucose/Glucose.cpp6
8 files changed, 1340 insertions, 15 deletions
diff --git a/abclib.dsp b/abclib.dsp
index 74cd3f44..d79f578e 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -2031,6 +2031,10 @@ SOURCE=.\src\sat\bmc\bmcMaj2.c
# End Source File
# Begin Source File
+SOURCE=.\src\sat\bmc\bmcMaj3.c
+# End Source File
+# Begin Source File
+
SOURCE=.\src\sat\bmc\bmcMaxi.c
# End Source File
# Begin Source File
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index c925fa42..7660dc0d 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -152,6 +152,7 @@ static int Abc_CommandBmsPs ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandMajExact ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTwoExact ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandLutExact ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAllExact ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandLogic ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandComb ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -821,6 +822,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Exact synthesis", "majexact", Abc_CommandMajExact, 0 );
Cmd_CommandAdd( pAbc, "Exact synthesis", "twoexact", Abc_CommandTwoExact, 0 );
Cmd_CommandAdd( pAbc, "Exact synthesis", "lutexact", Abc_CommandLutExact, 0 );
+ Cmd_CommandAdd( pAbc, "Exact synthesis", "allexact", Abc_CommandAllExact, 0 );
Cmd_CommandAdd( pAbc, "Various", "logic", Abc_CommandLogic, 1 );
Cmd_CommandAdd( pAbc, "Various", "comb", Abc_CommandComb, 1 );
@@ -8385,7 +8387,7 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv )
usage:
Abc_Print( -2, "usage: lutexact [-INK <num>] [-aogvh] <hex>\n" );
- Abc_Print( -2, "\t exact synthesis of multi-input function using two-input gates\n" );
+ Abc_Print( -2, "\t exact synthesis of I-input function using N K-input gates\n" );
Abc_Print( -2, "\t-I <num> : the number of input variables [default = %d]\n", pPars->nVars );
Abc_Print( -2, "\t-N <num> : the number of K-input nodes [default = %d]\n", pPars->nNodes );
Abc_Print( -2, "\t-K <num> : the number of node fanins [default = %d]\n", pPars->nLutSize );
@@ -8409,6 +8411,173 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandAllExact( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ extern void Zyx_ManExactSynthesis( Bmc_EsPar_t * pPars );
+ int c;
+ Bmc_EsPar_t Pars, * pPars = &Pars;
+ Bmc_EsParSetDefault( pPars );
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "MINKaoegvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'M':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nMajSupp = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nMajSupp < 0 )
+ goto usage;
+ break;
+ case 'I':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nVars = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nVars < 0 )
+ goto usage;
+ break;
+ case 'N':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nNodes = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nNodes < 0 )
+ goto usage;
+ break;
+ case 'K':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-K\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nLutSize = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nLutSize < 0 )
+ goto usage;
+ break;
+ case 'a':
+ pPars->fOnlyAnd ^= 1;
+ break;
+ case 'o':
+ pPars->fOrderNodes ^= 1;
+ break;
+ case 'e':
+ pPars->fGenAll ^= 1;
+ break;
+ case 'g':
+ pPars->fGlucose ^= 1;
+ break;
+ case 'v':
+ pPars->fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pPars->nMajSupp > 0 )
+ {
+ if ( pPars->nMajSupp != 5 && pPars->nMajSupp != 7 && pPars->nMajSupp != 9 )
+ {
+ Abc_Print( -1, "Currently only support majority with 5, 7 or 9 inputs.\n" );
+ return 1;
+ }
+ pPars->nVars = pPars->nMajSupp;
+ pPars->nLutSize = 3;
+ pPars->fMajority = 1;
+ if ( pPars->nNodes == 0 )
+ {
+ if ( pPars->nMajSupp == 5 )
+ pPars->nNodes = 4;
+ if ( pPars->nMajSupp == 7 )
+ pPars->nNodes = 7;
+ if ( pPars->nMajSupp == 9 )
+ pPars->nNodes = 10;
+ }
+ }
+ else
+ {
+ if ( pPars->nVars == 0 )
+ {
+ Abc_Print( -1, "The number of variables (-I num) needs to be specified on the command line.\n" );
+ return 1;
+ }
+ if ( pPars->nNodes == 0 )
+ {
+ Abc_Print( -1, "The number of nodes (-N num) needs to be specified on the command line.\n" );
+ return 1;
+ }
+ if ( argc == globalUtilOptind + 1 )
+ pPars->pTtStr = argv[globalUtilOptind];
+ if ( pPars->pTtStr == NULL )
+ {
+ Abc_Print( -1, "Truth table should be given on the command line.\n" );
+ return 1;
+ }
+ if ( (1 << (pPars->nVars-2)) != (int)strlen(pPars->pTtStr) )
+ {
+ Abc_Print( -1, "Truth table is expected to have %d hex digits (instead of %d).\n", (1 << (pPars->nVars-2)), strlen(pPars->pTtStr) );
+ return 1;
+ }
+ }
+ if ( pPars->nVars > pPars->nNodes * (pPars->nLutSize - 1) + 1 )
+ {
+ Abc_Print( -1, "Function with %d variales cannot be implemented with %d %d-input LUTs.\n", pPars->nVars, pPars->nNodes, pPars->nLutSize );
+ return 1;
+ }
+ if ( pPars->nVars > 10 )
+ {
+ Abc_Print( -1, "Function should not have more than 10 inputs.\n" );
+ return 1;
+ }
+ if ( pPars->nLutSize > 6 )
+ {
+ Abc_Print( -1, "Node size should not be more than 6 inputs.\n" );
+ return 1;
+ }
+ Zyx_ManExactSynthesis( pPars );
+ return 0;
+
+usage:
+ Abc_Print( -2, "usage: allexact [-MIKN <num>] [-aoevh] <hex>\n" );
+ Abc_Print( -2, "\t exact synthesis of I-input function using N K-input gates\n" );
+ Abc_Print( -2, "\t-M <num> : the majority support size (overrides -I and -K) [default = %d]\n", pPars->nMajSupp );
+ Abc_Print( -2, "\t-I <num> : the number of input variables [default = %d]\n", pPars->nVars );
+ Abc_Print( -2, "\t-K <num> : the number of node fanins [default = %d]\n", pPars->nLutSize );
+ Abc_Print( -2, "\t-N <num> : the number of K-input nodes [default = %d]\n", pPars->nNodes );
+ Abc_Print( -2, "\t-a : toggle using only AND-gates when K = 2 [default = %s]\n", pPars->fOnlyAnd ? "yes" : "no" );
+ Abc_Print( -2, "\t-o : toggle using node ordering by fanins [default = %s]\n", pPars->fOrderNodes ? "yes" : "no" );
+ Abc_Print( -2, "\t-e : toggle enumerating all solutions [default = %s]\n", pPars->fGenAll ? "yes" : "no" );
+// Abc_Print( -2, "\t-g : toggle using Glucose 3.0 by Gilles Audemard and Laurent Simon [default = %s]\n", pPars->fGlucose ? "yes" : "no" );
+ Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose ? "yes" : "no" );
+ Abc_Print( -2, "\t-h : print the command usage\n" );
+ Abc_Print( -2, "\t<hex> : truth table in hex notation\n" );
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_CommandLogic( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk, * pNtkRes;
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index 5b914741..be06c279 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -50,8 +50,13 @@ struct Bmc_EsPar_t_
int nVars;
int nNodes;
int nLutSize;
- int fGlucose;
+ int nMajSupp;
+ int fMajority;
+ int fEnumSols;
int fOnlyAnd;
+ int fGlucose;
+ int fOrderNodes;
+ int fGenAll;
int fFewerVars;
int fVerbose;
char * pTtStr;
@@ -59,13 +64,19 @@ struct Bmc_EsPar_t_
static inline void Bmc_EsParSetDefault( Bmc_EsPar_t * pPars )
{
- pPars->nVars = 5; // when first GC happens (4096) (degree of 2)
- pPars->nNodes = 4; // when each next GC happens (5)
- pPars->nLutSize = 3; // log difference compared to unique table
- pPars->fGlucose = 0; // minimum gain when reodering is not performed
- pPars->fOnlyAnd = 0; // minimum gain when reodering is not performed
- pPars->fFewerVars = 0; // minimum gain when reodering is not performed
- pPars->fVerbose = 1; // verbose output
+ memset( pPars, 0, sizeof(Bmc_EsPar_t) );
+ pPars->nVars = 0;
+ pPars->nNodes = 0;
+ pPars->nLutSize = 2;
+ pPars->nMajSupp = 0;
+ pPars->fMajority = 0;
+ pPars->fEnumSols = 0;
+ pPars->fOnlyAnd = 0;
+ pPars->fGlucose = 0;
+ pPars->fOrderNodes = 0;
+ pPars->fGenAll = 0;
+ pPars->fFewerVars = 0;
+ pPars->fVerbose = 1;
}
diff --git a/src/sat/bmc/bmcMaj.c b/src/sat/bmc/bmcMaj.c
index 67dcb26c..92ff06ee 100644
--- a/src/sat/bmc/bmcMaj.c
+++ b/src/sat/bmc/bmcMaj.c
@@ -184,6 +184,7 @@ static inline int Maj_ManFindFanin( Maj_Man_t * p, int i, int k )
}
static inline int Maj_ManEval( Maj_Man_t * p )
{
+ int fUseMiddle = 1;
static int Flag = 0;
int i, k, iMint; word * pFanins[3];
for ( i = p->nVars + 2; i < p->nObjs; i++ )
@@ -192,10 +193,27 @@ static inline int Maj_ManEval( Maj_Man_t * p )
pFanins[k] = Maj_ManTruth( p, Maj_ManFindFanin(p, i, k) );
Abc_TtMaj( Maj_ManTruth(p, i), pFanins[0], pFanins[1], pFanins[2], p->nWords );
}
- if ( Flag && p->nVars >= 6 )
- iMint = Abc_TtFindLastDiffBit( Maj_ManTruth(p, p->nObjs-1), Maj_ManTruth(p, p->nObjs), p->nVars );
+ if ( fUseMiddle )
+ {
+ iMint = -1;
+ for ( i = 0; i < (1 << p->nVars); i++ )
+ {
+ int nOnes = Abc_TtBitCount16(i);
+ if ( nOnes < p->nVars/2 || nOnes > p->nVars/2+1 )
+ continue;
+ if ( Abc_TtGetBit(Maj_ManTruth(p, p->nObjs), i) == Abc_TtGetBit(Maj_ManTruth(p, p->nObjs-1), i) )
+ continue;
+ iMint = i;
+ break;
+ }
+ }
else
- iMint = Abc_TtFindFirstDiffBit( Maj_ManTruth(p, p->nObjs-1), Maj_ManTruth(p, p->nObjs), p->nVars );
+ {
+ if ( Flag && p->nVars >= 6 )
+ iMint = Abc_TtFindLastDiffBit( Maj_ManTruth(p, p->nObjs-1), Maj_ManTruth(p, p->nObjs), p->nVars );
+ else
+ iMint = Abc_TtFindFirstDiffBit( Maj_ManTruth(p, p->nObjs-1), Maj_ManTruth(p, p->nObjs), p->nVars );
+ }
//Flag ^= 1;
assert( iMint < (1 << p->nVars) );
return iMint;
diff --git a/src/sat/bmc/bmcMaj2.c b/src/sat/bmc/bmcMaj2.c
index b0827b09..32bbc102 100644
--- a/src/sat/bmc/bmcMaj2.c
+++ b/src/sat/bmc/bmcMaj2.c
@@ -280,6 +280,7 @@ static inline int Maj_ManFindFanin( Maj_Man_t * p, int i, int k )
}
static inline int Maj_ManEval( Maj_Man_t * p )
{
+ int fUseMiddle = 1;
static int Flag = 0;
int i, k, iMint; word * pFanins[3];
for ( i = p->nVars + 2; i < p->nObjs; i++ )
@@ -288,10 +289,27 @@ static inline int Maj_ManEval( Maj_Man_t * p )
pFanins[k] = Maj_ManTruth( p, Maj_ManFindFanin(p, i, k) );
Abc_TtMaj( Maj_ManTruth(p, i), pFanins[0], pFanins[1], pFanins[2], p->nWords );
}
- if ( Flag && p->nVars >= 6 )
- iMint = Abc_TtFindLastDiffBit( Maj_ManTruth(p, p->nObjs-1), Maj_ManTruth(p, p->nObjs), p->nVars );
+ if ( fUseMiddle )
+ {
+ iMint = -1;
+ for ( i = 0; i < (1 << p->nVars); i++ )
+ {
+ int nOnes = Abc_TtBitCount16(i);
+ if ( nOnes < p->nVars/2 || nOnes > p->nVars/2+1 )
+ continue;
+ if ( Abc_TtGetBit(Maj_ManTruth(p, p->nObjs), i) == Abc_TtGetBit(Maj_ManTruth(p, p->nObjs-1), i) )
+ continue;
+ iMint = i;
+ break;
+ }
+ }
else
- iMint = Abc_TtFindFirstDiffBit( Maj_ManTruth(p, p->nObjs-1), Maj_ManTruth(p, p->nObjs), p->nVars );
+ {
+ if ( Flag && p->nVars >= 6 )
+ iMint = Abc_TtFindLastDiffBit( Maj_ManTruth(p, p->nObjs-1), Maj_ManTruth(p, p->nObjs), p->nVars );
+ else
+ iMint = Abc_TtFindFirstDiffBit( Maj_ManTruth(p, p->nObjs-1), Maj_ManTruth(p, p->nObjs), p->nVars );
+ }
//Flag ^= 1;
assert( iMint < (1 << p->nVars) );
return iMint;
diff --git a/src/sat/bmc/bmcMaj3.c b/src/sat/bmc/bmcMaj3.c
new file mode 100644
index 00000000..e35b2e87
--- /dev/null
+++ b/src/sat/bmc/bmcMaj3.c
@@ -0,0 +1,1098 @@
+/**CFile****************************************************************
+
+ FileName [bmcMaj3.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [SAT-based bounded model checking.]
+
+ Synopsis [Majority gate synthesis.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: bmcMaj3.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "bmc.h"
+#include "misc/extra/extra.h"
+#include "misc/util/utilTruth.h"
+#include "sat/glucose/AbcGlucose.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+#define MAJ3_OBJS 32 // nVars + nNodes
+
+typedef struct Maj3_Man_t_ Maj3_Man_t;
+struct Maj3_Man_t_
+{
+ int nVars; // inputs
+ int nNodes; // internal nodes
+ int nObjs; // total objects (nVars inputs, nNodes internal nodes)
+ int nWords; // the truth table size in 64-bit words
+ int iVar; // the next available SAT variable
+ Vec_Wrd_t * vInfo; // nVars + nNodes + 1
+ Vec_Int_t * vLevels; // distriction of nodes by levels
+ int VarMarks[MAJ3_OBJS][MAJ3_OBJS]; // variable marks
+ int ObjVals[MAJ3_OBJS]; // object values
+ int pLits[2][MAJ3_OBJS]; // neg, pos literals
+ int nLits[3]; // neg, pos, fixed literal
+ bmcg_sat_solver * pSat; // SAT solver
+};
+
+static inline word * Maj3_ManTruth( Maj3_Man_t * p, int v ) { return Vec_WrdEntryP( p->vInfo, p->nWords * v ); }
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Maj3_ManValue( int iMint, int nVars )
+{
+ int k, Count = 0;
+ for ( k = 0; k < nVars; k++ )
+ Count += (iMint >> k) & 1;
+ return (int)(Count > nVars/2);
+}
+Vec_Wrd_t * Maj3_ManTruthTables( Maj3_Man_t * p )
+{
+ Vec_Wrd_t * vInfo = p->vInfo = Vec_WrdStart( p->nWords * (p->nObjs + 1) );
+ int i, nMints = Abc_MaxInt( 64, 1 << p->nVars );
+ for ( i = 0; i < p->nVars; i++ )
+ Abc_TtIthVar( Maj3_ManTruth(p, i), i, p->nVars );
+ for ( i = 0; i < nMints; i++ )
+ if ( Maj3_ManValue(i, p->nVars) )
+ Abc_TtSetBit( Maj3_ManTruth(p, p->nObjs), i );
+ //Dau_DsdPrintFromTruth( Maj3_ManTruth(p, p->nObjs), p->nVars );
+ return vInfo;
+}
+void Maj3_ManFirstAndLevel( Vec_Int_t * vLevels, int Firsts[MAJ3_OBJS], int Levels[MAJ3_OBJS], int nVars, int nObjs )
+{
+ int i, k, Entry, Obj = 0;
+ Firsts[0] = Obj;
+ for ( k = 0; k < nVars; k++ )
+ Levels[Obj++] = 0;
+ Vec_IntReverseOrder( vLevels );
+ Vec_IntForEachEntry( vLevels, Entry, i )
+ {
+ Firsts[i+1] = Obj;
+ for ( k = 0; k < Entry; k++ )
+ Levels[Obj++] = i+1;
+ }
+ Vec_IntReverseOrder( vLevels );
+ assert( Obj == nObjs );
+}
+int Maj3_ManMarkup( Maj3_Man_t * p )
+{
+ int nSatVars = 2; // SAT variable counter
+ int nLevels = Vec_IntSize(p->vLevels);
+ int nSecond = Vec_IntEntry(p->vLevels, 1);
+ int i, k, Firsts[MAJ3_OBJS], Levels[MAJ3_OBJS];
+ assert( Vec_IntEntry(p->vLevels, 0) == 1 );
+ assert( p->nObjs <= MAJ3_OBJS );
+ assert( p->nNodes == Vec_IntSum(p->vLevels) );
+ Maj3_ManFirstAndLevel( p->vLevels, Firsts, Levels, p->nVars, p->nObjs );
+ // create map
+ for ( i = 0; i < p->nObjs; i++ )
+ for ( k = 0; k < p->nObjs; k++ )
+ p->VarMarks[i][k] = -1;
+ for ( k = 0; k < 3; k++ ) // first node
+ p->VarMarks[p->nVars][k] = 1;
+ for ( k = 0; k < nSecond; k++ ) // top node
+ p->VarMarks[p->nObjs-1][p->nObjs-2-k] = 1;
+ for ( k = 2; k < nLevels; k++ ) // cascade
+ p->VarMarks[Firsts[k]][Firsts[k-1]] = 1;
+ for ( i = p->nVars+1; i < (nSecond == 3 ? p->nObjs-1 : p->nObjs); i++ )
+ for ( k = 0; k < Firsts[Levels[i]]; k++ )
+ if ( p->VarMarks[i][k] == -1 )
+ p->VarMarks[i][k] = nSatVars++;
+ //printf( "The number of variables is %d.\n", nSatVars );
+ return nSatVars;
+}
+void Maj3_ManVarMapPrint( Maj3_Man_t * p )
+{
+ int i, k, Firsts[MAJ3_OBJS], Levels[MAJ3_OBJS];
+ Maj3_ManFirstAndLevel( p->vLevels, Firsts, Levels, p->nVars, p->nObjs );
+ // print
+ printf( "Variable map for problem with %d inputs, %d nodes and %d levels: ", p->nVars, p->nNodes, Vec_IntSize(p->vLevels) );
+ Vec_IntPrint( p->vLevels );
+ printf( " " );
+ printf( " " );
+ for ( i = 0; i < p->nObjs; i++ )
+ printf( "%3d ", i );
+ printf( "\n" );
+ for ( i = p->nObjs-1; i >= p->nVars; i-- )
+ {
+ printf( " %2d ", i );
+ printf( " %2d ", Levels[i] );
+ for ( k = 0; k < p->nObjs; k++ )
+ if ( p->VarMarks[i][k] == -1 )
+ printf( " . " );
+ else if ( p->VarMarks[i][k] == 1 )
+ printf( " + " );
+ else
+ printf( "%3d%c ", p->VarMarks[i][k], bmcg_sat_solver_read_cex_varvalue(p->pSat, p->VarMarks[i][k]) ? '+' : ' ' );
+ printf( "\n" );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Maj3_ManFindFanin( Maj3_Man_t * p, int i, int * pFanins )
+{
+ int f, nFanins = 0;
+ p->nLits[0] = p->nLits[1] = p->nLits[2] = 0;
+ for ( f = 0; f < i; f++ )
+ {
+ if ( p->VarMarks[i][f] < 0 )
+ continue;
+ assert( p->VarMarks[i][f] > 0 );
+ if ( p->VarMarks[i][f] == 1 ) // fixed
+ {
+ p->nLits[2]++;
+ pFanins[nFanins++] = f;
+ }
+ else if ( bmcg_sat_solver_read_cex_varvalue(p->pSat, p->VarMarks[i][f]) ) // pos
+ {
+ p->pLits[1][p->nLits[1]++] = Abc_Var2Lit(p->VarMarks[i][f], 1);
+ pFanins[nFanins++] = f;
+ }
+ else // neg
+ p->pLits[0][p->nLits[0]++] = Abc_Var2Lit(p->VarMarks[i][f], 0);
+ }
+ return nFanins;
+}
+static inline void Maj3_ManPrintSolution( Maj3_Man_t * p )
+{
+ int i, k, iVar, nFanins, pFanins[MAJ3_OBJS];
+ printf( "Realization of %d-input majority using %d MAJ3 gates:\n", p->nVars, p->nNodes );
+// for ( i = p->nVars; i < p->nObjs; i++ )
+ for ( i = p->nObjs - 1; i >= p->nVars; i-- )
+ {
+ printf( "%02d = MAJ(", i );
+ nFanins = Maj3_ManFindFanin( p, i, pFanins );
+ assert( nFanins == 3 );
+ for ( k = 0; k < 3; k++ )
+ {
+ iVar = pFanins[k];
+ if ( iVar >= 0 && iVar < p->nVars )
+ printf( " %c", 'a'+iVar );
+ else
+ printf( " %02d", iVar );
+ }
+ printf( " )\n" );
+ }
+}
+static inline int Maj3_ManEval( Maj3_Man_t * p )
+{
+ int fUseMiddle = 1;
+ static int Flag = 0;
+ int i, k, iMint, pFanins[3]; word * pFaninsW[3];
+ for ( i = p->nVars; i < p->nObjs; i++ )
+ {
+ int nFanins = Maj3_ManFindFanin( p, i, pFanins );
+ assert( nFanins == 3 );
+ for ( k = 0; k < 3; k++ )
+ pFaninsW[k] = Maj3_ManTruth( p, pFanins[k] );
+ Abc_TtMaj( Maj3_ManTruth(p, i), pFaninsW[0], pFaninsW[1], pFaninsW[2], p->nWords );
+ }
+ if ( fUseMiddle )
+ {
+ iMint = -1;
+ for ( i = 0; i < (1 << p->nVars); i++ )
+ {
+ int nOnes = Abc_TtBitCount16(i);
+ if ( nOnes < p->nVars/2 || nOnes > p->nVars/2+1 )
+ continue;
+ if ( Abc_TtGetBit(Maj3_ManTruth(p, p->nObjs), i) == Abc_TtGetBit(Maj3_ManTruth(p, p->nObjs-1), i) )
+ continue;
+ iMint = i;
+ break;
+ }
+ }
+ else
+ {
+ if ( Flag && p->nVars >= 6 )
+ iMint = Abc_TtFindLastDiffBit( Maj3_ManTruth(p, p->nObjs-1), Maj3_ManTruth(p, p->nObjs), p->nVars );
+ else
+ iMint = Abc_TtFindFirstDiffBit( Maj3_ManTruth(p, p->nObjs-1), Maj3_ManTruth(p, p->nObjs), p->nVars );
+ }
+ //Flag ^= 1;
+ assert( iMint < (1 << p->nVars) );
+ return iMint;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Maj3_PrintClause( int * pLits, int nLits )
+{
+ int i;
+ for ( i = 0; i < nLits; i++ )
+ printf( "%c%d ", Abc_LitIsCompl(pLits[i]) ? '-' : '+', Abc_Lit2Var(pLits[i]) );
+ printf( "\n" );
+}
+int Maj3_ManAddCnfStart( Maj3_Man_t * p )
+{
+ int i, k, status, nLits, pLits[MAJ3_OBJS];
+ // nodes have at least one fanin
+ //printf( "Fanin clauses:\n" );
+ for ( i = p->nVars; i < p->nObjs; i++ )
+ {
+ // check if it is already connected
+ int Count = 0;
+ for ( k = 0; k < p->nObjs; k++ )
+ Count += p->VarMarks[i][k] == 1;
+ assert( Count <= 3 );
+ if ( Count == 3 )
+ continue;
+ // collect connections
+ nLits = 0;
+ for ( k = 0; k < p->nObjs; k++ )
+ if ( p->VarMarks[i][k] > 1 )
+ pLits[nLits++] = Abc_Var2Lit( p->VarMarks[i][k], 0 );
+ //Maj3_PrintClause( pLits, nLits );
+ assert( nLits > 0 );
+ if ( nLits > 0 && !bmcg_sat_solver_addclause( p->pSat, pLits, nLits ) )
+ assert(0);
+ }
+ // nodes have at least one fanout
+ //printf( "Fanout clauses:\n" );
+ for ( k = 0; k < p->nObjs-1; k++ )
+ {
+ // check if it is already connected
+ int Count = 0;
+ for ( i = 0; i < p->nObjs; i++ )
+ Count += p->VarMarks[i][k] == 1;
+ assert( Count <= 3 );
+ if ( Count > 0 )
+ continue;
+ // collect connections
+ nLits = 0;
+ for ( i = 0; i < p->nObjs; i++ )
+ if ( p->VarMarks[i][k] > 1 )
+ pLits[nLits++] = Abc_Var2Lit( p->VarMarks[i][k], 0 );
+ //Maj3_PrintClause( pLits, nLits );
+ //assert( nLits > 0 );
+ if ( nLits > 0 && !bmcg_sat_solver_addclause( p->pSat, pLits, nLits ) )
+ assert(0);
+ }
+ status = bmcg_sat_solver_solve( p->pSat, NULL, 0 );
+ assert( status == GLUCOSE_SAT );
+ Maj3_ManVarMapPrint( p );
+ return 1;
+}
+int Maj3_ManAddCnf( Maj3_Man_t * p, int iMint )
+{
+ // input values
+ int i, k, j, n, * pVals = p->ObjVals;
+ for ( i = 0; i < p->nVars; i++ )
+ pVals[i] = (iMint >> i) & 1;
+ // first node value
+ pVals[p->nVars] = (pVals[0] && pVals[1]) || (pVals[0] && pVals[2]) || (pVals[1] && pVals[2]);
+ // last node value
+ pVals[p->nObjs-1] = Maj3_ManValue(iMint, p->nVars);
+ // intermediate node values
+ for ( i = p->nVars + 1; i < p->nObjs - 1; i++ )
+ pVals[i] = p->iVar++;
+ //printf( "Adding clauses for minterm %d.\n", iMint );
+ bmcg_sat_solver_set_nvars( p->pSat, p->iVar );
+ for ( n = 0; n < 2; n++ )
+ for ( i = p->nVars + 1; i < p->nObjs; i++ )
+ {
+ //printf( "\nNode %d. Phase %d.\n", i, n );
+ for ( k = 0; k < p->nObjs; k++ ) if ( p->VarMarks[i][k] >= 1 )
+ {
+ // add first input
+ int pLits[5], nLits = 0;
+ if ( pVals[k] == !n )
+ continue;
+ if ( pVals[k] > 1 )
+ pLits[nLits++] = Abc_Var2Lit( pVals[k], n );
+ if ( p->VarMarks[i][k] > 1 )
+ pLits[nLits++] = Abc_Var2Lit( p->VarMarks[i][k], 1 );
+ for ( j = k+1; j < p->nObjs; j++ ) if ( p->VarMarks[i][j] >= 1 )
+ {
+ // add second input
+ int nLits2 = nLits;
+ if ( pVals[j] == !n )
+ continue;
+ if ( pVals[j] > 1 )
+ pLits[nLits2++] = Abc_Var2Lit( pVals[j], n );
+ if ( p->VarMarks[i][j] > 1 )
+ pLits[nLits2++] = Abc_Var2Lit( p->VarMarks[i][j], 1 );
+ // add output
+ if ( pVals[i] == n )
+ continue;
+ if ( pVals[i] > 1 )
+ pLits[nLits2++] = Abc_Var2Lit( pVals[i], !n );
+ assert( nLits2 > 0 && nLits2 <= 5 );
+ //Maj3_PrintClause( pLits, nLits2 );
+ if ( !bmcg_sat_solver_addclause( p->pSat, pLits, nLits2 ) )
+ return 0;
+ }
+ }
+ }
+ return 1;
+}
+int Maj3_ManAddConstraintsLazy( Maj3_Man_t * p )
+{
+ int i, pFanins[MAJ3_OBJS], nConstr = 0;
+ //Maj3_ManVarMapPrint( p );
+ for ( i = p->nVars+1; i < p->nObjs; i++ )
+ {
+ int nFanins = Maj3_ManFindFanin( p, i, pFanins );
+ if ( nFanins == 3 )
+ continue;
+ //printf( "Node %d has %d fanins.\n", i, nFanins );
+ nConstr++;
+ if ( nFanins < 3 )
+ {
+ assert( p->nLits[0] > 0 );
+ //Maj3_PrintClause( p->pLits[0], p->nLits[0] );
+ if ( !bmcg_sat_solver_addclause( p->pSat, p->pLits[0], p->nLits[0] ) )
+ return -1;
+ }
+ else if ( nFanins > 3 )
+ {
+ int nLits = Abc_MinInt(4 - p->nLits[2], p->nLits[1]);
+ assert( nLits > 0 );
+ //Maj3_PrintClause( p->pLits[1], nLits );
+ if ( !bmcg_sat_solver_addclause( p->pSat, p->pLits[1], nLits ) )
+ return -1;
+ }
+ }
+ return nConstr;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Maj3_Man_t * Maj3_ManAlloc( int nVars, int nNodes, Vec_Int_t * vLevels )
+{
+ Maj3_Man_t * p = ABC_CALLOC( Maj3_Man_t, 1 );
+ p->vLevels = vLevels;
+ p->nVars = nVars;
+ p->nNodes = nNodes;
+ p->nObjs = nVars + nNodes;
+ p->nWords = Abc_TtWordNum(nVars);
+ p->iVar = Maj3_ManMarkup( p );
+ p->vInfo = Maj3_ManTruthTables( p );
+ p->pSat = bmcg_sat_solver_start();
+ bmcg_sat_solver_set_nvars( p->pSat, p->iVar );
+ Maj3_ManAddCnfStart( p );
+ return p;
+}
+void Maj3_ManFree( Maj3_Man_t * p )
+{
+ bmcg_sat_solver_stop( p->pSat );
+ Vec_WrdFree( p->vInfo );
+ ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Maj3_ManExactSynthesis( int nVars, int nNodes, int fVerbose, Vec_Int_t * vLevels )
+{
+ Maj3_Man_t * p; abctime clkTotal = Abc_Clock();
+ int i, status, nLazy, nLazyAll = 0, iMint = 0;
+ printf( "Running exact synthesis for %d-input majority with %d MAJ3 gates...\n", nVars, nNodes );
+ p = Maj3_ManAlloc( nVars, nNodes, vLevels );
+ for ( i = 0; iMint != -1; i++ )
+ {
+ abctime clk = Abc_Clock();
+ if ( !Maj3_ManAddCnf( p, iMint ) )
+ break;
+ while ( (status = bmcg_sat_solver_solve(p->pSat, NULL, 0)) == GLUCOSE_SAT )
+ {
+ nLazy = Maj3_ManAddConstraintsLazy( p );
+ if ( nLazy == -1 )
+ {
+ printf( "Became UNSAT after adding lazy constraints.\n" );
+ status = GLUCOSE_UNSAT;
+ break;
+ }
+ //printf( "Added %d lazy constraints.\n\n", nLazy );
+ if ( nLazy == 0 )
+ break;
+ nLazyAll += nLazy;
+ }
+ if ( fVerbose )
+ {
+ printf( "Iter %3d : ", i );
+ Extra_PrintBinary( stdout, (unsigned *)&iMint, p->nVars );
+ printf( " Var =%5d ", p->iVar );
+ printf( "Cla =%6d ", bmcg_sat_solver_clausenum(p->pSat) );
+ printf( "Conf =%9d ", bmcg_sat_solver_conflictnum(p->pSat) );
+ printf( "Lazy =%9d ", nLazyAll );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ }
+ if ( status == GLUCOSE_UNSAT )
+ {
+ printf( "The problem has no solution.\n" );
+ break;
+ }
+ iMint = Maj3_ManEval( p );
+ }
+ if ( iMint == -1 )
+ Maj3_ManPrintSolution( p );
+ Maj3_ManFree( p );
+ Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
+ return iMint == -1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Maj3_ManTest()
+{
+/*
+ int nVars = 5;
+ int nNodes = 4;
+ int fVerbose = 1;
+ int Levels[MAJ3_OBJS] = { 1, 2, 1 };
+ Vec_Int_t vLevels = { 3, 3, Levels };
+*/
+
+ int nVars = 7;
+ int nNodes = 7;
+ int fVerbose = 1;
+ int Levels[MAJ3_OBJS] = { 1, 2, 2, 2 };
+ Vec_Int_t vLevels = { 4, 4, Levels };
+
+/*
+ int nVars = 9;
+ int nNodes = 10;
+ int fVerbose = 1;
+ int Levels[MAJ3_OBJS] = { 1, 2, 3, 2, 2 };
+ Vec_Int_t vLevels = { 5, 5, Levels };
+*/
+/*
+ int nVars = 9;
+ int nNodes = 10;
+ int fVerbose = 1;
+ int Levels[MAJ3_OBJS] = { 1, 1, 1, 1, 1, 1, 1, 1, 1, 1 };
+ Vec_Int_t vLevels = { 10, 10, Levels };
+*/
+
+// Maj3_Man_t * p = Maj3_ManAlloc( nVars, nNodes, &vLevels );
+// Maj3_ManFree( p );
+ Maj3_ManExactSynthesis( nVars, nNodes, fVerbose, &vLevels );
+ return 0;
+}
+
+
+
+
+
+typedef struct Zyx_Man_t_ Zyx_Man_t;
+struct Zyx_Man_t_
+{
+ Bmc_EsPar_t * pPars; // parameters
+ word * pTruth; // truth table
+ int nObjs; // total objects (nVars inputs, nNodes internal nodes)
+ int nWords; // the truth table size in 64-bit words
+ int LutMask; // 1 << nLutSize
+ int TopoBase; // (1 << nLutSize) * nObjs
+ int MintBase; // TopoBase + nObjs * nObjs
+ Vec_Wrd_t * vInfo; // nVars + nNodes + 1
+ Vec_Int_t * vVarValues; // variable values
+ int pFanins[MAJ3_OBJS][MAJ3_OBJS]; // fanins
+ int pLits[2][2*MAJ3_OBJS]; // neg/pos literals
+ int nLits[2]; // neg/pos literal
+ int Counts[1024];
+ bmcg_sat_solver * pSat; // SAT solver
+};
+
+static inline word * Zyx_ManTruth( Zyx_Man_t * p, int v ) { return Vec_WrdEntryP( p->vInfo, p->nWords * v ); }
+
+static inline int Zyx_FuncVar( Zyx_Man_t * p, int i, int m ) { return (1 << p->pPars->nLutSize) * i + m; }
+static inline int Zyx_TopoVar( Zyx_Man_t * p, int i, int f ) { return p->TopoBase + p->nObjs * i + f; }
+static inline int Zyx_MintVar( Zyx_Man_t * p, int m, int i ) { return p->MintBase + p->nObjs * m + i; }
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Zyx_SetConstVar( Zyx_Man_t * p, int Var, int Value )
+{
+ int iLit = Abc_Var2Lit( Var, !Value );
+ int status = bmcg_sat_solver_addclause( p->pSat, &iLit, 1 );
+ assert( status );
+ assert( Vec_IntEntry(p->vVarValues, Var) == -1 );
+ Vec_IntWriteEntry( p->vVarValues, Var, Value );
+ //printf( "Setting var %d to value %d.\n", Var, Value );
+}
+void Zyx_ManSetupVars( Zyx_Man_t * p )
+{
+ int i, k, m;
+ word * pSpec = p->pPars->fMajority ? Zyx_ManTruth(p, p->nObjs) : p->pTruth;
+ // set unused functionality vars to 0
+ for ( i = p->pPars->nVars; i < p->nObjs; i++ )
+ Zyx_SetConstVar( p, Zyx_FuncVar(p, i, 0), 0 );
+ // set unused topology vars
+ for ( i = p->pPars->nVars; i < p->nObjs; i++ )
+ for ( k = i; k < p->nObjs; k++ )
+ Zyx_SetConstVar( p, Zyx_TopoVar(p, i, k), 0 );
+ // connect topmost node
+ Zyx_SetConstVar( p, Zyx_TopoVar(p, p->nObjs-1, p->nObjs-2), 1 );
+ // connect first node
+ if ( p->pPars->fMajority )
+ for ( k = 0; k < p->pPars->nVars; k++ )
+ Zyx_SetConstVar( p, Zyx_TopoVar(p, p->pPars->nVars, k), k < 3 );
+ // set minterm vars
+ for ( m = 0; m < (1 << p->pPars->nVars); m++ )
+ {
+ for ( i = 0; i < p->pPars->nVars; i++ )
+ Zyx_SetConstVar( p, Zyx_MintVar(p, m, i), (m >> i) & 1 );
+ Zyx_SetConstVar( p, Zyx_MintVar(p, m, p->nObjs-1), Abc_TtGetBit(pSpec, m) );
+ }
+}
+int Zyx_ManAddCnfStart( Zyx_Man_t * p )
+{
+ // nodes have fanins
+ int i, k, pLits[MAJ3_OBJS];
+ //printf( "Adding initial clauses:\n" );
+ for ( i = p->pPars->nVars; i < p->nObjs; i++ )
+ {
+ int nLits = 0;
+ for ( k = 0; k < i; k++ )
+ pLits[nLits++] = Abc_Var2Lit( Zyx_TopoVar(p, i, k), 0 );
+ assert( nLits > 0 );
+ if ( !bmcg_sat_solver_addclause( p->pSat, pLits, nLits ) )
+ return 0;
+ }
+
+ // nodes have fanouts
+ for ( k = 0; k < p->nObjs-1; k++ )
+ {
+ int nLits = 0;
+ for ( i = p->pPars->nVars; i < p->nObjs; i++ )
+ pLits[nLits++] = Abc_Var2Lit( Zyx_TopoVar(p, i, k), 0 );
+ assert( nLits > 0 );
+ if ( !bmcg_sat_solver_addclause( p->pSat, pLits, nLits ) )
+ return 0;
+ }
+
+ // two input functions
+ if ( p->pPars->nLutSize != 2 )
+ return 1;
+ for ( i = p->pPars->nVars; i < p->nObjs; i++ )
+ {
+ for ( k = 0; k < 3; k++ )
+ {
+ pLits[0] = Abc_Var2Lit( Zyx_FuncVar(p, i, 1), k==1 );
+ pLits[1] = Abc_Var2Lit( Zyx_FuncVar(p, i, 2), k==2 );
+ pLits[2] = Abc_Var2Lit( Zyx_FuncVar(p, i, 3), k!=0 );
+ if ( !bmcg_sat_solver_addclause( p->pSat, pLits, 3 ) )
+ return 0;
+ }
+ if ( p->pPars->fOnlyAnd )
+ {
+ pLits[0] = Abc_Var2Lit( Zyx_FuncVar(p, i, 1), 1 );
+ pLits[1] = Abc_Var2Lit( Zyx_FuncVar(p, i, 2), 1 );
+ pLits[2] = Abc_Var2Lit( Zyx_FuncVar(p, i, 3), 0 );
+ if ( !bmcg_sat_solver_addclause( p->pSat, pLits, 3 ) )
+ return 0;
+ }
+ }
+ return 1;
+}
+void Zyx_ManPrintVarMap( Zyx_Man_t * p, int fSat )
+{
+ int i, k, nTopoVars = 0;
+ printf( " " );
+ for ( k = 0; k < p->nObjs-1; k++ )
+ printf( "%3d ", k );
+ printf( "\n" );
+ for ( i = p->nObjs-1; i >= p->pPars->nVars; i-- )
+ {
+ printf( "%3d ", i );
+ for ( k = 0; k < p->nObjs-1; k++ )
+ {
+ int iVar = Zyx_TopoVar(p, i, k);
+ if ( Vec_IntEntry(p->vVarValues, iVar) == -1 )
+ printf( "%3d%c ", iVar, (fSat && bmcg_sat_solver_read_cex_varvalue(p->pSat, iVar)) ? '*' : ' ' ), nTopoVars++;
+ else
+ printf( "%3d ", Vec_IntEntry(p->vVarValues, iVar) );
+ }
+ printf( "\n" );
+ }
+ if ( fSat ) return;
+ printf( "Using %d active functionality vars and %d active topology vars (out of %d SAT vars).\n",
+ p->pPars->fMajority ? 0 : p->pPars->nNodes * p->LutMask, nTopoVars, bmcg_sat_solver_varnum(p->pSat) );
+}
+void Zyx_PrintClause( int * pLits, int nLits )
+{
+ int i;
+ for ( i = 0; i < nLits; i++ )
+ printf( "%c%d ", Abc_LitIsCompl(pLits[i]) ? '-' : '+', Abc_Lit2Var(pLits[i]) );
+ printf( "\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Zyx_ManValue( int iMint, int nVars )
+{
+ int k, Count = 0;
+ for ( k = 0; k < nVars; k++ )
+ Count += (iMint >> k) & 1;
+ return (int)(Count > nVars/2);
+}
+Vec_Wrd_t * Zyx_ManTruthTables( Zyx_Man_t * p, word * pTruth )
+{
+ Vec_Wrd_t * vInfo = p->vInfo = Vec_WrdStart( p->nWords * (p->nObjs + 1) );
+ int i, nMints = Abc_MaxInt( 64, 1 << p->pPars->nVars );
+ assert( p->pPars->fMajority == (pTruth == NULL) );
+ for ( i = 0; i < p->pPars->nVars; i++ )
+ Abc_TtIthVar( Zyx_ManTruth(p, i), i, p->pPars->nVars );
+ if ( p->pPars->fMajority )
+ for ( i = 0; i < nMints; i++ )
+ if ( Zyx_ManValue(i, p->pPars->nVars) )
+ Abc_TtSetBit( Zyx_ManTruth(p, p->nObjs), i );
+ //Dau_DsdPrintFromTruth( Zyx_ManTruth(p, p->nObjs), p->pPars->nVars );
+ return vInfo;
+}
+Zyx_Man_t * Zyx_ManAlloc( Bmc_EsPar_t * pPars, word * pTruth )
+{
+ Zyx_Man_t * p = ABC_CALLOC( Zyx_Man_t, 1 );
+ p->pPars = pPars;
+ p->pTruth = pTruth;
+ p->nObjs = p->pPars->nVars + p->pPars->nNodes;
+ p->nWords = Abc_TtWordNum(p->pPars->nVars);
+ p->LutMask = (1 << p->pPars->nLutSize) - 1;
+ p->TopoBase = (1 << p->pPars->nLutSize) * p->nObjs;
+ p->MintBase = p->TopoBase + p->nObjs * p->nObjs;
+ p->vVarValues = Vec_IntStartFull( p->MintBase + (1 << p->pPars->nVars) * p->nObjs );
+ p->vInfo = Zyx_ManTruthTables( p, pTruth );
+ p->pSat = bmcg_sat_solver_start();
+ bmcg_sat_solver_set_nvars( p->pSat, p->MintBase + (1 << p->pPars->nVars) * p->nObjs );
+ Zyx_ManSetupVars( p );
+ Zyx_ManAddCnfStart( p );
+ Zyx_ManPrintVarMap( p, 0 );
+ return p;
+}
+void Zyx_ManFree( Zyx_Man_t * p )
+{
+ bmcg_sat_solver_stop( p->pSat );
+ Vec_WrdFree( p->vInfo );
+ Vec_IntFree( p->vVarValues );
+ ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Zyx_ManCollectFanins( Zyx_Man_t * p, int i )
+{
+ int k, Val;
+ assert( i >= p->pPars->nVars && i < p->nObjs );
+ p->nLits[0] = p->nLits[1] = 0;
+ for ( k = 0; k < i; k++ )
+ {
+ Val = bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_TopoVar(p, i, k));
+ p->pFanins[i][p->nLits[1]] = k;
+ p->pLits[Val][p->nLits[Val]++] = Abc_Var2Lit(Zyx_TopoVar(p, i, k), Val);
+ }
+ return p->nLits[1];
+}
+int Zyx_ManAddCnfLazyTopo( Zyx_Man_t * p )
+{
+ int i, k, j, nLazy = 0;
+ // fanin count
+ //printf( "Adding topology clauses.\n" );
+ for ( i = p->pPars->nVars; i < p->nObjs; i++ )
+ {
+ int nFanins = Zyx_ManCollectFanins( p, i );
+ if ( nFanins == p->pPars->nLutSize )
+ continue;
+ nLazy++;
+ assert( nFanins == p->nLits[1] );
+ if ( p->nLits[1] > p->pPars->nLutSize )
+ {
+ p->nLits[1] = p->pPars->nLutSize + 1;
+ //Zyx_PrintClause( p->pLits[1], p->nLits[1] );
+ if ( !bmcg_sat_solver_addclause( p->pSat, p->pLits[1], p->nLits[1] ) )
+ return -1;
+ }
+ else // if ( p->nLits[1] < p->pPars->nLutSize )
+ {
+ //Zyx_PrintClause( p->pLits[0], p->nLits[0] );
+ if ( !bmcg_sat_solver_addclause( p->pSat, p->pLits[0], p->nLits[0] ) )
+ return -1;
+ }
+ }
+ if ( nLazy || !p->pPars->fOrderNodes )
+ return nLazy;
+ // ordering
+ for ( i = p->pPars->nVars + 1; i < p->nObjs; i++ )
+ {
+ for ( k = p->pPars->nLutSize - 1; k >= 0; k-- )
+ if ( p->pFanins[i-1][k] != p->pFanins[i][k] )
+ break;
+ if ( k == -1 )
+ {
+ if ( !p->pPars->fMajority )
+ {
+ // compare by LUT functions
+ }
+ continue;
+ }
+ if ( p->pFanins[i-1][k] < p->pFanins[i][k] )
+ {
+ assert( bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_TopoVar(p, i-1, p->pFanins[i][k])) == 0 );
+ assert( bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_TopoVar(p, i , p->pFanins[i][k])) == 1 );
+ continue;
+ }
+ nLazy++;
+ assert( bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_TopoVar(p, i-1, p->pFanins[i-1][k])) == 1 );
+ assert( bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_TopoVar(p, i , p->pFanins[i-1][k])) == 0 );
+ // rule out this order
+ p->nLits[0] = 0;
+ for ( j = p->pFanins[i-1][k]; j < p->nObjs-1; j++ )
+ {
+ int ValA = bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_TopoVar(p, i-1, j));
+ int ValB = bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_TopoVar(p, i, j));
+ p->pLits[0][p->nLits[0]++] = Abc_Var2Lit(Zyx_TopoVar(p, i-1, j), ValA );
+ p->pLits[0][p->nLits[0]++] = Abc_Var2Lit(Zyx_TopoVar(p, i, j), ValB );
+ }
+ //printf( "\n" );
+ //Zyx_ManPrintVarMap( p, 1 );
+ //Zyx_PrintClause( p->pLits[0], p->nLits[0] );
+ if ( !bmcg_sat_solver_addclause( p->pSat, p->pLits[0], p->nLits[0] ) )
+ return -1;
+ //break;
+ }
+ return nLazy;
+}
+int Zyx_ManAddCnfBlockSolution( Zyx_Man_t * p )
+{
+ Vec_Int_t * vLits = Vec_IntAlloc( 100 ); int i, k;
+ for ( i = p->pPars->nVars; i < p->nObjs; i++ )
+ {
+ int nFanins = Zyx_ManCollectFanins( p, i );
+ assert( nFanins == p->pPars->nLutSize );
+ for ( k = 0; k < p->pPars->nLutSize; k++ )
+ Vec_IntPush( vLits, Abc_Var2Lit(Zyx_TopoVar(p, i, p->pFanins[i][k]), 1) );
+ }
+ //Zyx_ManPrintVarMap( p, 1 );
+ //Zyx_PrintClause( Vec_IntArray(vLits), Vec_IntSize(vLits) );
+ if ( !bmcg_sat_solver_addclause( p->pSat, Vec_IntArray(vLits), Vec_IntSize(vLits) ) )
+ return 0;
+ Vec_IntFree( vLits );
+ return 1;
+}
+int Zyx_ManAddCnfLazyFunc( Zyx_Man_t * p, int iMint )
+{
+ int Sets[3][2] = {{0, 1}, {0, 2}, {1, 2}};
+ int i, k, n, j, s;
+ assert( !p->pPars->fMajority || p->pPars->nLutSize == 3 );
+ //printf( "Adding functionality clauses for minterm %d.\n", iMint );
+ p->Counts[iMint]++;
+ for ( i = p->pPars->nVars; i < p->nObjs; i++ )
+ {
+ int nFanins = Zyx_ManCollectFanins( p, i );
+ assert( nFanins == p->pPars->nLutSize );
+ for ( n = 0; n < 2; n++ )
+ {
+ if ( p->pPars->fMajority )
+ {
+ for ( k = 0; k < 3; k++ )
+ {
+ p->nLits[0] = 0;
+ for ( s = 0; s < 2; s++ )
+ {
+ p->pLits[0][p->nLits[0]++] = Abc_Var2Lit( Zyx_TopoVar(p, i, p->pFanins[i][Sets[k][s]]), 1 );
+ p->pLits[0][p->nLits[0]++] = Abc_Var2Lit( Zyx_MintVar(p, iMint, p->pFanins[i][Sets[k][s]]), n );
+ }
+ p->pLits[0][p->nLits[0]++] = Abc_Var2Lit( Zyx_MintVar(p, iMint, i), !n );
+ if ( !bmcg_sat_solver_addclause( p->pSat, p->pLits[0], p->nLits[0] ) )
+ return 0;
+ }
+ }
+ else
+ {
+ for ( k = 0; k <= p->LutMask; k++ )
+ {
+ p->nLits[0] = 0;
+ p->pLits[0][p->nLits[0]++] = Abc_Var2Lit( Zyx_FuncVar(p, i, k), n );
+ for ( j = 0; j < p->pPars->nLutSize; j++ )
+ {
+ p->pLits[0][p->nLits[0]++] = Abc_Var2Lit( Zyx_TopoVar(p, i, p->pFanins[i][j]), 1 );
+ p->pLits[0][p->nLits[0]++] = Abc_Var2Lit( Zyx_MintVar(p, iMint, p->pFanins[i][j]), (k >> j) & 1 );
+ }
+ p->pLits[0][p->nLits[0]++] = Abc_Var2Lit( Zyx_MintVar(p, iMint, i), !n );
+ //Zyx_PrintClause( p->pLits[0], p->nLits[0] );
+ if ( !bmcg_sat_solver_addclause( p->pSat, p->pLits[0], p->nLits[0] ) )
+ return 0;
+ }
+ }
+ }
+ }
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static void Zyx_ManPrintSolution( Zyx_Man_t * p, int fCompl )
+{
+ int i, k;
+ printf( "Realization of given %d-input function using %d %d-input %s:\n",
+ p->pPars->nVars, p->pPars->nNodes, p->pPars->nLutSize, p->pPars->fMajority ? "MAJ-gates" : "LUTs" );
+ for ( i = p->nObjs - 1; i >= p->pPars->nVars; i-- )
+ {
+ printf( "%02d = ", i );
+ if ( p->pPars->fMajority )
+ printf( "MAJ3" );
+ else
+ {
+ printf( "%d\'b", 1 << p->pPars->nLutSize );
+ for ( k = p->LutMask; k >= 0; k-- )
+ printf( "%d", bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_FuncVar(p, i, k)) ^ (i == p->nObjs - 1 && fCompl) );
+ }
+ printf( "(" );
+ for ( k = 0; k < i; k++ )
+ if ( bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_TopoVar(p, i, k)) )
+ if ( k >= 0 && k < p->pPars->nVars )
+ printf( " %c", 'a'+k );
+ else
+ printf( " %02d", k );
+ printf( " )\n" );
+ }
+}
+static inline int Zyx_ManEval( Zyx_Man_t * p )
+{
+ static int Flag = 0;
+ int i, k, j, iMint; word * pFaninsW[6], * pSpec;
+ for ( i = p->pPars->nVars; i < p->nObjs; i++ )
+ {
+ int nFanins = Zyx_ManCollectFanins( p, i );
+ assert( nFanins == p->pPars->nLutSize );
+ for ( k = 0; k < p->pPars->nLutSize; k++ )
+ pFaninsW[k] = Zyx_ManTruth( p, p->pFanins[i][k] );
+ if ( p->pPars->fMajority )
+ Abc_TtMaj( Zyx_ManTruth(p, i), pFaninsW[0], pFaninsW[1], pFaninsW[2], p->nWords );
+ else
+ {
+ Abc_TtConst0( Zyx_ManTruth(p, i), p->nWords );
+ for ( k = 1; k <= p->LutMask; k++ )
+ if ( bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_FuncVar(p, i, k)) )
+ {
+ Abc_TtConst1( Zyx_ManTruth(p, p->nObjs), p->nWords );
+ for ( j = 0; j < p->pPars->nLutSize; j++ )
+ Abc_TtAndCompl( Zyx_ManTruth(p, p->nObjs), Zyx_ManTruth(p, p->nObjs), 0, pFaninsW[j], !((k >> j) & 1), p->nWords );
+ Abc_TtOr( Zyx_ManTruth(p, i), Zyx_ManTruth(p, i), Zyx_ManTruth(p, p->nObjs), p->nWords );
+ }
+ }
+ }
+ pSpec = p->pPars->fMajority ? Zyx_ManTruth(p, p->nObjs) : p->pTruth;
+ if ( Flag && p->pPars->nVars >= 6 )
+ iMint = Abc_TtFindLastDiffBit( Zyx_ManTruth(p, p->nObjs-1), pSpec, p->pPars->nVars );
+ else
+ iMint = Abc_TtFindFirstDiffBit( Zyx_ManTruth(p, p->nObjs-1), pSpec, p->pPars->nVars );
+ //Flag ^= 1;
+ assert( iMint < (1 << p->pPars->nVars) );
+ return iMint;
+}
+static inline void Zyx_ManEvalStats( Zyx_Man_t * p )
+{
+ int i;
+ for ( i = 0; i < (1 << p->pPars->nVars); i++ )
+ printf( "%d=%d ", i, p->Counts[i] );
+ printf( "\n" );
+}
+static inline void Zyx_ManPrint( Zyx_Man_t * p, int Iter, int iMint, int nLazyAll, abctime clk )
+{
+ printf( "Iter %6d : ", Iter );
+ Extra_PrintBinary( stdout, (unsigned *)&iMint, p->pPars->nVars );
+ printf( " " );
+ printf( "Cla =%9d ", bmcg_sat_solver_clausenum(p->pSat) );
+ printf( "Lazy =%6d ", nLazyAll );
+ printf( "Conf =%9d ", bmcg_sat_solver_conflictnum(p->pSat) );
+ Abc_PrintTime( 1, "Time", clk );
+ //Zyx_ManEvalStats( p );
+}
+void Zyx_ManExactSynthesis( Bmc_EsPar_t * pPars )
+{
+ int status, Iter, iMint = 0, fCompl = 0, nLazyAll = 0, nSols = 0;
+ abctime clkTotal = Abc_Clock(), clk = Abc_Clock(); Zyx_Man_t * p;
+ word pTruth[16];
+ if ( !pPars->fMajority )
+ {
+ Abc_TtReadHex( pTruth, pPars->pTtStr );
+ if ( pTruth[0] & 1 ) { fCompl = 1; Abc_TtNot( pTruth, Abc_TtWordNum(pPars->nVars) ); }
+ }
+ assert( pPars->nVars <= 10 );
+ assert( pPars->nLutSize <= 6 );
+ p = Zyx_ManAlloc( pPars, pPars->fMajority ? NULL : pTruth );
+ printf( "Running exact synthesis for %d-input function with %d %d-input %s...\n",
+ p->pPars->nVars, p->pPars->nNodes, p->pPars->nLutSize, p->pPars->fMajority ? "MAJ-gates" : "LUTs" );
+ for ( Iter = 0 ; ; Iter++ )
+ {
+ while ( (status = bmcg_sat_solver_solve(p->pSat, NULL, 0)) == GLUCOSE_SAT )
+ {
+ int nLazy = Zyx_ManAddCnfLazyTopo( p );
+ if ( nLazy == -1 )
+ {
+ printf( "Became UNSAT after adding lazy constraints.\n" );
+ status = GLUCOSE_UNSAT;
+ break;
+ }
+ //printf( "Added %d lazy constraints.\n\n", nLazy );
+ if ( nLazy == 0 )
+ break;
+ nLazyAll += nLazy;
+ }
+ if ( status == GLUCOSE_UNSAT )
+ break;
+ // find mismatch
+ iMint = Zyx_ManEval( p );
+ if ( iMint == -1 )
+ {
+ if ( pPars->fGenAll )
+ {
+ nSols++;
+ if ( pPars->fVerbose )
+ {
+ Zyx_ManPrint( p, Iter, iMint, nLazyAll, Abc_Clock() - clkTotal );
+ clk = Abc_Clock();
+ }
+ Zyx_ManPrintSolution( p, fCompl );
+ if ( !Zyx_ManAddCnfBlockSolution( p ) )
+ break;
+ continue;
+ }
+ else
+ break;
+ }
+ if ( !Zyx_ManAddCnfLazyFunc(p, iMint) )
+ {
+ printf( "Became UNSAT after adding constraints for minterm %d\n", iMint );
+ status = GLUCOSE_UNSAT;
+ break;
+ }
+ status = bmcg_sat_solver_solve( p->pSat, NULL, 0 );
+ if ( pPars->fVerbose && Iter % 100 == 0 )
+ {
+ Zyx_ManPrint( p, Iter, iMint, nLazyAll, Abc_Clock() - clk );
+ clk = Abc_Clock();
+ }
+ if ( status == GLUCOSE_UNSAT )
+ break;
+ }
+ if ( pPars->fVerbose )
+ Zyx_ManPrint( p, Iter, iMint, nLazyAll, Abc_Clock() - clkTotal );
+ if ( pPars->fGenAll )
+ printf( "Finished enumerating %d solutions.\n", nSols );
+ else if ( iMint == -1 )
+ Zyx_ManPrintSolution( p, fCompl );
+ else
+ printf( "The problem has no solution.\n" );
+ Zyx_ManFree( p );
+ Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
+}
+
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/bmc/module.make b/src/sat/bmc/module.make
index cf19feaa..ae254433 100644
--- a/src/sat/bmc/module.make
+++ b/src/sat/bmc/module.make
@@ -24,6 +24,7 @@ SRC += src/sat/bmc/bmcBCore.c \
src/sat/bmc/bmcLoad.c \
src/sat/bmc/bmcMaj.c \
src/sat/bmc/bmcMaj2.c \
+ src/sat/bmc/bmcMaj3.c \
src/sat/bmc/bmcMaxi.c \
src/sat/bmc/bmcMesh.c \
src/sat/bmc/bmcMesh2.c \
diff --git a/src/sat/glucose/Glucose.cpp b/src/sat/glucose/Glucose.cpp
index 3ca372a8..0f2d2fce 100644
--- a/src/sat/glucose/Glucose.cpp
+++ b/src/sat/glucose/Glucose.cpp
@@ -253,6 +253,12 @@ bool Solver::addClause_(vec<Lit>& ps)
else if (value(ps[i]) != l_False && ps[i] != p)
ps[j++] = p = ps[i];
ps.shrink(i - j);
+
+ if ( 0 ) {
+ for ( int i = 0; i < ps.size(); i++ )
+ printf( "%s%d ", (toInt(ps[i]) & 1) ? "-":"", toInt(ps[i]) >> 1 );
+ printf( "\n" );
+ }
if (flag && (certifiedUNSAT)) {
for (i = j = 0, p = lit_Undef; i < ps.size(); i++)