diff --git a/src/aig/gia/giaTim.c b/src/aig/gia/giaTim.c index 271c6d4ee..54012bbde 100644 --- a/src/aig/gia/giaTim.c +++ b/src/aig/gia/giaTim.c @@ -953,20 +953,6 @@ Gia_Man_t * Gia_ManDupCollapse( Gia_Man_t * p, Gia_Man_t * pBoxes, Vec_Int_t * v ***********************************************************************/ -/* -› Please have a look at how name mapping is done in procedure Abc_FrameReadMiniLutNameMapping() in file "src/aig/gia/ - giaMini.c". The main idea is to map the object IDs in the design after synthesis (pAbc->pGiaMiniLut) into the object IDs in - the design before synthesis (pAbc->pGiaMiniAig). The computation is divided into three steps: (1) computing object - equivalences using Gia_ManComputeGiaEquivs(), which annotates the input AIG (pGia) containing both designs before and after - synthesis with equivalence class information; this information contains equivalence classes of objects from both designs; (2) - creating a map (pRes) of the resulting object IDs (in pAbc->pGiaMiniLut) into the original object IDs (in pAbc->pGiaMiniAig) - using procedure Gia_ManMapMiniLut2MiniAig(); this map is enabled by having two arrays (one of them is pAbc->vCopyMiniAig - mapping objects of pAbc->pGiaMiniAig in the original object IDs; the other one is pAbc->vCopyMiniLut mapping objects of - pAbc->pGiaMiniLut into the IDs of pAbc->pGiaMiniLut); (3) verification procedure (commented out by default) - Gia_ManNameMapVerify() which checks that the resulting mapping computed by Gia_ManMapMiniLut2MiniAig() is correct. Please - let me know if this computation is clear. -*/ - Vec_Int_t * Gia_ManVerifyFindNameMapping( Gia_Man_t * p, Gia_Man_t * p1, Gia_Man_t * p2, Vec_Int_t * vMap1, Vec_Int_t * vMap2 ) { Vec_Int_t * vRes = Vec_IntStartFull(Vec_IntSize(vMap2)); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 669632be2..d4ec89b41 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -172,6 +172,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_CommandAndExact ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAllExact ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandTestExact ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandMajGen ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -1002,6 +1003,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", "andexact", Abc_CommandAndExact, 0 ); Cmd_CommandAdd( pAbc, "Exact synthesis", "allexact", Abc_CommandAllExact, 0 ); Cmd_CommandAdd( pAbc, "Exact synthesis", "testexact", Abc_CommandTestExact, 0 ); Cmd_CommandAdd( pAbc, "Exact synthesis", "majgen", Abc_CommandMajGen, 0 ); @@ -10992,7 +10994,7 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv ) usage: Abc_Print( -2, "usage: lutexact [-NMKTFUS ] [-Y string] [-P string] [-iaorfgckdsmpvh] \n" ); - Abc_Print( -2, "\t exact synthesis of I-input function using N K-input gates\n" ); + Abc_Print( -2, "\t exact synthesis of N-input function using M K-input lookup-tables\n" ); Abc_Print( -2, "\t-N : the number of input variables [default = %d]\n", pPars->nVars ); Abc_Print( -2, "\t-M : the number of K-input nodes [default = %d]\n", pPars->nNodes ); Abc_Print( -2, "\t-K : the number of node fanins [default = %d]\n", pPars->nLutSize ); @@ -11020,6 +11022,186 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAndExact( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern int Exa9_ManExactSynthesis( Bmc_EsPar_t * pPars ); + extern int Exa9_ManExactSynthesisIter( Bmc_EsPar_t * pPars ); + extern char * Abc_NtkReadTruth( Abc_Ntk_t * pNtk ); + int c; + Bmc_EsPar_t Pars, * pPars = &Pars; + Bmc_EsParSetDefault( pPars ); + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "NMTSHYiadsmvh" ) ) != EOF ) + { + switch ( c ) + { + case 'N': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nVars = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nVars < 0 ) + goto usage; + break; + case 'M': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nNodes = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nNodes < 0 ) + goto usage; + break; + case 'T': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" ); + goto usage; + } + pPars->RuntimeLim = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->RuntimeLim < 0 ) + goto usage; + break; + case 'S': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" ); + goto usage; + } + pPars->Seed = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->Seed < 0 ) + goto usage; + break; + case 'H': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-H\" should be followed by a string.\n" ); + goto usage; + } + pPars->n1HotAlgo = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + break; + case 'Y': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-Y\" should be followed by a string.\n" ); + goto usage; + } + pPars->pSymStr = argv[globalUtilOptind]; + globalUtilOptind++; + break; + case 'i': + pPars->fUseIncr ^= 1; + break; + case 'a': + pPars->fOnlyAnd ^= 1; + break; + case 'd': + pPars->fDumpBlif ^= 1; + break; + case 's': + pPars->fSilent ^= 1; + break; + case 'm': + pPars->fMinNodes ^= 1; + break; + case 'v': + pPars->fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( argc == globalUtilOptind + 1 ) + pPars->pTtStr = argv[globalUtilOptind]; + else if ( argc == globalUtilOptind && Abc_FrameReadNtk(pAbc) ) + { + pPars->pTtStr = Abc_NtkReadTruth( Abc_FrameReadNtk(pAbc) ); + if ( pPars->pTtStr ) + pPars->nVars = Abc_NtkCiNum(Abc_FrameReadNtk(pAbc)); + } + if ( pPars->pTtStr == NULL && pPars->pSymStr == NULL && pPars->nRandFuncs == 0 ) + { + Abc_Print( -1, "Truth table should be given on the command line.\n" ); + return 1; + } + if ( pPars->nVars == 0 && pPars->pTtStr ) + pPars->nVars = 2 + Abc_Base2Log((int)strlen(pPars->pTtStr)); + if ( pPars->pTtStr && (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 == 0 && pPars->pSymStr ) + pPars->nVars = (int)strlen(pPars->pSymStr) - 1; + if ( pPars->pSymStr && pPars->nVars+1 != strlen(pPars->pSymStr) ) + { + Abc_Print( -1, "The char string of the %d-variable symmetric function should have %d zeros and ones (instead of %d).\n", pPars->nVars, pPars->nVars+1, strlen(pPars->pSymStr) ); + return 1; + } + if ( pPars->nVars > pPars->nNodes + 1 ) + { + Abc_Print( -1, "Function with %d variales cannot be implemented with %d two-input nodes.\n", pPars->nVars, pPars->nNodes ); + return 1; + } + if ( pPars->nVars > 14 ) + { + Abc_Print( -1, "Function should not have more than 14 inputs.\n" ); + return 1; + } + if ( pPars->nNodes > 16 ) + { + Abc_Print( -1, "Node count cannot be more than 16 inputs.\n" ); + return 1; + } + if ( pPars->fMinNodes ) + Exa9_ManExactSynthesisIter( pPars ); + else + Exa9_ManExactSynthesis( pPars ); + if ( argc == globalUtilOptind && Abc_FrameReadNtk(pAbc) ) + ABC_FREE( pPars->pTtStr ); + return 0; + +usage: + Abc_Print( -2, "usage: andexact [-NMTSH ] [-Y str] [-iadmsvh] \n" ); + Abc_Print( -2, "\t exact synthesis of N-input function using two-input gates\n" ); + Abc_Print( -2, "\t-N : the number of input variables [default = %d]\n", pPars->nVars ); + Abc_Print( -2, "\t-M : the number of two-input nodes [default = %d]\n", pPars->nNodes ); + Abc_Print( -2, "\t-T : the runtime limit in seconds [default = %d]\n", pPars->RuntimeLim ); + Abc_Print( -2, "\t-S : the random seed for random function generation with -F [default = %d]\n", pPars->Seed ); + Abc_Print( -2, "\t-H : the 1-hotness algorithm used (0 = naive; 1 = seq; 2 = bim; 3 = cmd) [default = %d]\n", pPars->n1HotAlgo ); + Abc_Print( -2, "\t-Y : charasteristic string of a symmetric function [default = %s]\n", pPars->pSymStr ? pPars->pSymStr : "unused" ); + Abc_Print( -2, "\t-i : toggle using incremental SAT (CEGAR over minterms) [default = %s]\n", pPars->fUseIncr ? "yes" : "no" ); + Abc_Print( -2, "\t-a : toggle using only AND-gates when K = 2 [default = %s]\n", pPars->fOnlyAnd ? "yes" : "no" ); + Abc_Print( -2, "\t-m : toggle minimum-node solution possibly smaller than \"-M \" [default = %s]\n", pPars->fMinNodes ? "yes" : "no" ); + Abc_Print( -2, "\t-d : toggle dumping decomposed networks into BLIF files [default = %s]\n", pPars->fDumpBlif ? "yes" : "no" ); + Abc_Print( -2, "\t-s : toggle silent computation (no messages, except when a solution is found) [default = %s]\n", pPars->fSilent ? "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 : truth table in hex notation\n" ); + return 1; +} + /**Function************************************************************* Synopsis [] diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h index 3b591bb4e..93d3ea326 100644 --- a/src/sat/bmc/bmc.h +++ b/src/sat/bmc/bmc.h @@ -73,6 +73,7 @@ struct Bmc_EsPar_t_ int nRandFuncs; int nMintNum; int Seed; + int n1HotAlgo; int fDumpBlif; int fVerbose; int fSilent; @@ -102,6 +103,7 @@ static inline void Bmc_EsParSetDefault( Bmc_EsPar_t * pPars ) pPars->fUniqFans = 0; pPars->fLutCascade = 0; pPars->RuntimeLim = 0; + pPars->n1HotAlgo = 1; pPars->fVerbose = 0; } @@ -274,4 +276,3 @@ ABC_NAMESPACE_HEADER_END //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// - diff --git a/src/sat/bmc/bmcMaj9.c b/src/sat/bmc/bmcMaj9.c new file mode 100644 index 000000000..cc15c153a --- /dev/null +++ b/src/sat/bmc/bmcMaj9.c @@ -0,0 +1,1011 @@ +/**CFile**************************************************************** + + FileName [bmcMaj9.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [SAT-based bounded model checking.] + + Synopsis [Exact synthesis with majority gates.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - October 1, 2017.] + + Revision [$Id: bmcMaj9.c,v 1.00 2017/10/01 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "bmc.h" +#include "misc/extra/extra.h" +#include "misc/util/utilTruth.h" +#include "sat/kissat/kissat.h" +#include "aig/miniaig/miniaig.h" +#include "base/io/ioResub.h" +#include "base/main/main.h" +#include "base/cmd/cmd.h" + +#include +#include + +#define KISSAT_UNSAT 20 +#define KISSAT_SAT 10 +#define KISSAT_UNDEC 0 + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +#define MAJ_NOBJS 64 // Const0 + Const1 + nVars + nNodes + +typedef struct Exa9_Man_t_ Exa9_Man_t; +struct Exa9_Man_t_ +{ + Bmc_EsPar_t * pPars; // parameters + 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 nMints; // number of input minterms + int nSelVars; // number of selection variables (fanin + output) + int nValVars; // number of value variables + int nVarAlloc; // total vars reserved in the solver + int nClausesStart; // clauses added in the structural part (excluding 1-hot) + int nClausesHot; // clauses added for 1-hot constraints + int nClausesMints; // clauses added per-minterm + int fCountStruct; // flag: counting structural clauses + int fCountHot; // flag: counting 1-hot clauses + word * pTruth; // truth table + Vec_Wrd_t * vTruths; // computed truth tables + kissat * pSat; // SAT solver + abctime timeStop; // runtime limit (0 = unlimited) +}; + +static inline int Exa9_LitToKissat( int Lit ) +{ + int v = Abc_Lit2Var( Lit ); + assert( v > 0 ); + return Abc_LitIsCompl( Lit ) ? -v : v; +} +static inline int Exa9_KissatAddClause( Exa9_Man_t * p, int * pLits, int nLits ) +{ + int i; + for ( i = 0; i < nLits; i++ ) + kissat_add( p->pSat, Exa9_LitToKissat( pLits[i] ) ); + kissat_add( p->pSat, 0 ); + if ( p->fCountStruct ) + { + if ( p->fCountHot ) + p->nClausesHot++; + else + p->nClausesStart++; + } + else + p->nClausesMints++; + return !kissat_is_inconsistent( p->pSat ); +} +static inline int Exa9_KissatVarValue( Exa9_Man_t * p, int v ) +{ + assert( v > 0 ); + return kissat_value( p->pSat, v ) > 0; +} +static int Exa9_KissatTerminate( void * pData ) +{ + Exa9_Man_t * p = (Exa9_Man_t *)pData; + return p && p->timeStop && Abc_Clock() > p->timeStop; +} + +static inline word * Exa9_ManTruth( Exa9_Man_t * p, int v ) { return Vec_WrdEntryP( p->vTruths, p->nWords * v ); } + +static inline int Exa9_ManSelVar( Exa9_Man_t * p, int iNode, int iFanin, int fCompl, int iObj ) +{ + return 1 + (((iNode * 2 + iFanin) * 2 + fCompl) * p->nObjs + (iObj - 1)); +} +static inline int Exa9_ManSelVarAux( Exa9_Man_t * p, int iNode, int iFanin, int fCompl, int iObj ) +{ + return 1 + p->nSelVars + (((iNode * 2 + iFanin) * 2 + fCompl) * p->nObjs + (iObj - 1)); +} +static inline int Exa9_ManSelVarOut( Exa9_Man_t * p, int fCompl, int iObj ) +{ + return 1 + 4 * p->nNodes * p->nObjs + fCompl * p->nObjs + (iObj - 1); +} +static inline int Exa9_ManSelVarOutAux( Exa9_Man_t * p, int fCompl, int iObj ) +{ + return 1 + p->nSelVars + 4 * p->nNodes * p->nObjs + fCompl * p->nObjs + (iObj - 1); +} +static inline int Exa9_ManValueVar( Exa9_Man_t * p, int iObj, int Place, int iMint ) +{ + int Base = 1 + 2 * p->nSelVars; + return Base + ((iObj - 1) * 3 + Place) * p->nMints + iMint; +} + +// return auxiliary vars actually used by a 1-hot of size nLits under the chosen encoding +static inline int Exa9_ManCountAuxOneHot( int nLits, int Algo ) +{ + if ( nLits <= 1 ) + return 0; + if ( Algo == 0 ) // naive pairwise + return 0; + if ( Algo == 1 ) // sequential + return nLits - 1; + if ( Algo == 2 ) // bimander + { + const int GroupSize = 6; + if ( nLits <= GroupSize ) + return 0; + { + int nGroups = (nLits + GroupSize - 1) / GroupSize; + int nBits = Abc_Base2Log( nGroups ); + return nBits; + } + } + if ( Algo == 3 ) // commander + { + const int GroupSize = 5; + if ( nLits <= GroupSize ) + return 0; + { + int nGroups = (nLits + GroupSize - 1) / GroupSize; + return nGroups; + } + } + return 0; +} + +static int Exa9_ManCountAuxTotal( Exa9_Man_t * p ) +{ + int Algo = p->pPars->n1HotAlgo; + int Total = 0; + int n; + // fanin selectors (two fanins * two polarities per node) + for ( n = 0; n < p->nNodes; n++ ) + { + int Obj = p->nVars + n + 1; + int nLits = Obj - 1; // choices for each polarity + int AuxPerGroup = Exa9_ManCountAuxOneHot( nLits, Algo ); + Total += 4 * AuxPerGroup; + } + // output selector (two polarities over all objects) + Total += Exa9_ManCountAuxOneHot( 2 * p->nObjs, Algo ); + return Total; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static int Exa9_ManVarReserve( Exa9_Man_t * p ) +{ + int64_t Count = 2 * (int64_t)p->nSelVars + (int64_t)p->nValVars; + if ( Count > INT_MAX ) + Count = INT_MAX; + return (int)Count; +} +static Exa9_Man_t * Exa9_ManAlloc( Bmc_EsPar_t * pPars, word * pTruth ) +{ + Exa9_Man_t * p = ABC_CALLOC( Exa9_Man_t, 1 ); + p->pPars = pPars; + p->nVars = pPars->nVars; + p->nNodes = pPars->nNodes; + p->nObjs = pPars->nVars + pPars->nNodes; + p->nWords = Abc_TtWordNum(pPars->nVars); + p->nMints = 1 << pPars->nVars; + p->nSelVars = p->nNodes * 4 * p->nObjs + 2 * p->nObjs; + p->nValVars = 3 * p->nObjs * p->nMints; + p->nVarAlloc = Exa9_ManVarReserve( p ); + p->nClausesStart = p->nClausesHot = p->nClausesMints = 0; + p->fCountStruct = 0; + p->fCountHot = 0; + p->pTruth = pTruth; + p->vTruths = Vec_WrdStart( p->nWords * (p->nObjs + 1) ); + p->pSat = kissat_init(); + { + int nBias = 0; // 0=neutral, 1=SAT bias, -1=UNSAT bias + if ( nBias > 0 ) + { + kissat_set_option( p->pSat, "target", 2 ); + kissat_set_option( p->pSat, "restartint", 50 ); + } + else if ( nBias < 0 ) + kissat_set_option( p->pSat, "stable", 0 ); + } + assert( Exa9_ManValueVar( p, p->nObjs, 2, p->nMints - 1 ) <= p->nVarAlloc ); + kissat_reserve( p->pSat, p->nVarAlloc ); + if ( pPars->Seed > 0 ) + kissat_set_option( p->pSat, "seed", pPars->Seed ); + p->timeStop = 0; + return p; +} +static void Exa9_ManFree( Exa9_Man_t * p ) +{ + kissat_release( p->pSat ); + Vec_WrdFree( p->vTruths ); + ABC_FREE( p ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Exa9_ManAddUnit( Exa9_Man_t * p, int Var, int fCompl ) +{ + int Lit = Abc_Var2Lit( Var, fCompl ); + return Exa9_KissatAddClause( p, &Lit, 1 ); +} +static inline int Exa9_ManAddEquality( Exa9_Man_t * p, int iSel, int iFan, int iOut, int fCompl ) +{ + int pLits[3]; + pLits[0] = Abc_Var2Lit( iSel, 1 ); + pLits[1] = Abc_Var2Lit( iFan, 1 ); + pLits[2] = Abc_Var2Lit( iOut, fCompl ); + if ( !Exa9_KissatAddClause( p, pLits, 3 ) ) + return 0; + pLits[1] = Abc_Var2Lit( iFan, 0 ); + pLits[2] = Abc_Var2Lit( iOut, !fCompl ); + return Exa9_KissatAddClause( p, pLits, 3 ); +} +static int Exa9_ManAddOneHotQuad( Exa9_Man_t * p, Vec_Int_t * vLits ) +{ + int * pArray = Vec_IntArray( vLits ); + int nLits = Vec_IntSize( vLits ); + int i, k; + assert( nLits > 0 ); + if ( !Exa9_KissatAddClause( p, pArray, nLits ) ) + return 0; + for ( i = 0; i < nLits; i++ ) + for ( k = i + 1; k < nLits; k++ ) + { + int pLits[2] = { Abc_LitNot(pArray[i]), Abc_LitNot(pArray[k]) }; + if ( !Exa9_KissatAddClause( p, pLits, 2 ) ) + return 0; + } + return 1; +} +static int Exa9_ManAddOneHotSeq( Exa9_Man_t * p, Vec_Int_t * vLits, Vec_Int_t * vAux ) +{ + int nLits = Vec_IntSize( vLits ); + int * x = Vec_IntArray( vLits ); + int * y = Vec_IntArray( vAux ); + int pLits[2], i; + assert( nLits > 0 ); + if ( !Exa9_KissatAddClause( p, x, nLits ) ) + return 0; + if ( nLits == 1 ) + return 1; + assert( Vec_IntSize(vAux) >= nLits - 1 ); + // (¬x1 ∨ y1) + pLits[0] = Abc_LitNot( x[0] ); + pLits[1] = Abc_Var2Lit( y[0], 0 ); + if ( !Exa9_KissatAddClause( p, pLits, 2 ) ) + return 0; + // middle constraints + for ( i = 1; i < nLits - 1; i++ ) + { + // (¬xi ∨ yi) + pLits[0] = Abc_LitNot( x[i] ); + pLits[1] = Abc_Var2Lit( y[i], 0 ); + if ( !Exa9_KissatAddClause( p, pLits, 2 ) ) + return 0; + // (¬yi-1 ∨ yi) + pLits[0] = Abc_LitNot( Abc_Var2Lit( y[i-1], 0 ) ); + pLits[1] = Abc_Var2Lit( y[i], 0 ); + if ( !Exa9_KissatAddClause( p, pLits, 2 ) ) + return 0; + // (¬xi ∨ ¬yi-1) + pLits[0] = Abc_LitNot( x[i] ); + pLits[1] = Abc_LitNot( Abc_Var2Lit( y[i-1], 0 ) ); + if ( !Exa9_KissatAddClause( p, pLits, 2 ) ) + return 0; + } + // (¬xn ∨ ¬y_{n-1}) + pLits[0] = Abc_LitNot( x[nLits-1] ); + pLits[1] = Abc_LitNot( Abc_Var2Lit( y[nLits-2], 0 ) ); + return Exa9_KissatAddClause( p, pLits, 2 ); +} +static inline int Exa9_ManAddAtMostOnePair( Exa9_Man_t * p, Vec_Int_t * vLits ) +{ + int nLits = Vec_IntSize( vLits ); + int * x = Vec_IntArray( vLits ); + int pLits[2], i, j; + for ( i = 0; i < nLits; i++ ) + for ( j = i + 1; j < nLits; j++ ) + { + pLits[0] = Abc_LitNot( x[i] ); + pLits[1] = Abc_LitNot( x[j] ); + if ( !Exa9_KissatAddClause( p, pLits, 2 ) ) + return 0; + } + return 1; +} +static int Exa9_ManAddOneHotBim( Exa9_Man_t * p, Vec_Int_t * vLits, Vec_Int_t * vAux ) +{ + int nLits = Vec_IntSize( vLits ); + int * x = Vec_IntArray( vLits ); + int * y = Vec_IntArray( vAux ); + int pLits[2], i, j, g; + int GroupSize = 6; + if ( nLits == 0 ) + return 0; + if ( !Exa9_KissatAddClause( p, x, nLits ) ) + return 0; + if ( nLits == 1 ) + return 1; + if ( nLits <= GroupSize ) + return Exa9_ManAddOneHotQuad( p, vLits ); + { + int nGroups = (nLits + GroupSize - 1) / GroupSize; + int nBits = Abc_Base2Log( nGroups ); + if ( nBits == 0 ) + return Exa9_ManAddOneHotQuad( p, vLits ); + assert( Vec_IntSize(vAux) >= nBits ); + // pairwise inside each group + for ( g = 0; g < nGroups; g++ ) + { + int iStart = g * GroupSize; + int iStop = Abc_MinInt( iStart + GroupSize, nLits ); + for ( i = iStart; i < iStop; i++ ) + for ( j = i + 1; j < iStop; j++ ) + { + pLits[0] = Abc_LitNot( x[i] ); + pLits[1] = Abc_LitNot( x[j] ); + if ( !Exa9_KissatAddClause( p, pLits, 2 ) ) + return 0; + } + // connect literals in the group to shared binary variables + for ( i = iStart; i < iStop; i++ ) + { + int Code = g; + int b; + for ( b = 0; b < nBits; b++, Code >>= 1 ) + { + pLits[0] = Abc_LitNot( x[i] ); + pLits[1] = (Code & 1) ? Abc_Var2Lit( y[b], 0 ) : Abc_LitNot( Abc_Var2Lit( y[b], 0 ) ); + if ( !Exa9_KissatAddClause( p, pLits, 2 ) ) + return 0; + } + } + } + } + return 1; +} +static int Exa9_ManAddOneHotCom( Exa9_Man_t * p, Vec_Int_t * vLits, Vec_Int_t * vAux ) +{ + int nLits = Vec_IntSize( vLits ); + int * x = Vec_IntArray( vLits ); + int * y = Vec_IntArray( vAux ); + int GroupSize = 4; + int i, j, g; + Vec_Int_t * vCmd; + if ( nLits == 0 ) + return 0; + if ( !Exa9_KissatAddClause( p, x, nLits ) ) + return 0; + if ( nLits == 1 ) + return 1; + if ( nLits <= GroupSize ) + return Exa9_ManAddOneHotQuad( p, vLits ); + vCmd = Vec_IntAlloc(16); + { + int nGroups = (nLits + GroupSize - 1) / GroupSize; + if ( nGroups > Vec_IntSize(vAux) ) + { + Vec_IntFree( vCmd ); + return Exa9_ManAddOneHotQuad( p, vLits ); + } + for ( g = 0; g < nGroups; g++ ) + { + int CmdVar = y[g]; + Vec_IntPush( vCmd, Abc_Var2Lit( CmdVar, 0 ) ); + int iStart = g * GroupSize; + int iStop = Abc_MinInt( iStart + GroupSize, nLits ); + // CmdVar => at least one literal in the group + { + int pLits[6]; // GroupSize <= 5 + int nCls = 0; + pLits[nCls++] = Abc_LitNot( Abc_Var2Lit( CmdVar, 0 ) ); + for ( i = iStart; i < iStop; i++ ) + pLits[nCls++] = x[i]; + assert( nCls <= 6 ); + if ( !Exa9_KissatAddClause( p, pLits, nCls ) ) + { + Vec_IntFree( vCmd ); + return 0; + } + } + for ( i = iStart; i < iStop; i++ ) + { + int pLits[2] = { Abc_LitNot( x[i] ), Abc_Var2Lit( CmdVar, 0 ) }; + if ( !Exa9_KissatAddClause( p, pLits, 2 ) ) + { + Vec_IntFree( vCmd ); + return 0; + } + } + for ( i = iStart; i < iStop; i++ ) + for ( j = i + 1; j < iStop; j++ ) + { + int pLits[2] = { Abc_LitNot( x[i] ), Abc_LitNot( x[j] ) }; + if ( !Exa9_KissatAddClause( p, pLits, 2 ) ) + { + Vec_IntFree( vCmd ); + return 0; + } + } + } + } + if ( !Exa9_ManAddAtMostOnePair( p, vCmd ) ) + { + Vec_IntFree( vCmd ); + return 0; + } + Vec_IntFree( vCmd ); + return 1; +} +static int Exa9_ManAddOneHot( Exa9_Man_t * p, Vec_Int_t * vLits, Vec_Int_t * vAux ) +{ + int Res = 0; + int fOldHot = p->fCountHot; + p->fCountHot = 1; + if ( Vec_IntSize(vLits) < 7 ) + Res = Exa9_ManAddOneHotQuad( p, vLits ); + else if ( p->pPars->n1HotAlgo == 1 ) + Res = Exa9_ManAddOneHotSeq( p, vLits, vAux ); + else if ( p->pPars->n1HotAlgo == 2 ) + Res = Exa9_ManAddOneHotBim( p, vLits, vAux ); + else if ( p->pPars->n1HotAlgo == 3 ) + Res = Exa9_ManAddOneHotCom( p, vLits, vAux ); + else + Res = Exa9_ManAddOneHotQuad( p, vLits ); + p->fCountHot = fOldHot; + return Res; +} +static int Exa9_ManAddCnfStart( Exa9_Man_t * p ) +{ + p->fCountStruct = 1; + Vec_Int_t * vLits = Vec_IntAlloc( 100 ); + Vec_Int_t * vAux = Vec_IntAlloc( 100 ); + Vec_Int_t * vUse = Vec_IntAlloc( 100 ); + int n, j, k, c, Var; + for ( n = 0; n < p->nNodes; n++ ) + { + int Obj = p->nVars + n + 1; + for ( k = 0; k < 2; k++ ) + { + Vec_IntClear( vLits ); + Vec_IntClear( vAux ); + for ( j = 1; j <= p->nObjs; j++ ) + for ( c = 0; c < 2; c++ ) + { + Var = Exa9_ManSelVar( p, n, k, c, j ); + if ( j >= Obj ) + { + if ( !Exa9_ManAddUnit( p, Var, 1 ) ) + { + Vec_IntFree( vLits ); + Vec_IntFree( vAux ); + return 0; + } + continue; + } + Vec_IntPush( vLits, Abc_Var2Lit( Var, 0 ) ); + Vec_IntPush( vAux, Exa9_ManSelVarAux( p, n, k, c, j ) ); + } + if ( Vec_IntSize(vLits) == 0 || !Exa9_ManAddOneHot( p, vLits, vAux ) ) + { + Vec_IntFree( vLits ); + Vec_IntFree( vAux ); + return 0; + } + } + // enforce first fanin index < second fanin index + for ( j = 1; j < Obj; j++ ) + for ( c = 0; c < 2; c++ ) + { + int Var0 = Exa9_ManSelVar( p, n, 0, c, j ); + int j2, c2; + for ( j2 = 1; j2 <= j; j2++ ) + for ( c2 = 0; c2 < 2; c2++ ) + { + int Var1 = Exa9_ManSelVar( p, n, 1, c2, j2 ); + int pLits[2] = { Abc_Var2Lit( Var0, 1 ), Abc_Var2Lit( Var1, 1 ) }; + if ( !Exa9_KissatAddClause( p, pLits, 2 ) ) + { + Vec_IntFree( vLits ); + Vec_IntFree( vAux ); + return 0; + } + } + } + /* + // order nodes by larger (second) fanin index + for ( j = 1; j < Obj; j++ ) + for ( c = 0; c < 2; c++ ) + { + int VarLargeThis = Exa9_ManSelVar( p, n, 1, c, j ); + int m, k, c3; + for ( m = 0; m < n; m++ ) + { + int ObjM = p->nVars + m + 1; + if ( j + 1 >= ObjM ) + continue; + for ( k = j + 1; k < ObjM; k++ ) + for ( c3 = 0; c3 < 2; c3++ ) + { + int VarLargePrev = Exa9_ManSelVar( p, m, 1, c3, k ); + int pLits[2] = { Abc_Var2Lit( VarLargeThis, 1 ), Abc_Var2Lit( VarLargePrev, 1 ) }; + if ( !Exa9_KissatAddClause( p, pLits, 2 ) ) + { + Vec_IntFree( vLits ); + Vec_IntFree( vAux ); + Vec_IntFree( vUse ); + return 0; + } + } + } + } + // forbid duplicate fanin pairs across nodes (respecting polarity) + for ( int m = 0; m < n; m++ ) + { + int j2, c2, ObjM = p->nVars + m + 1; + for ( j = 1; j + 1 < ObjM; j++ ) + for ( j2 = j + 1; j2 < ObjM; j2++ ) + for ( c = 0; c < 2; c++ ) + for ( c2 = 0; c2 < 2; c2++ ) + { + int VarN0 = Exa9_ManSelVar( p, n, 0, c, j ); + int VarN1 = Exa9_ManSelVar( p, n, 1, c2, j2 ); + int VarM0 = Exa9_ManSelVar( p, m, 0, c, j ); + int VarM1 = Exa9_ManSelVar( p, m, 1, c2, j2 ); + int pLits4[4] = { Abc_Var2Lit( VarN0, 1 ), Abc_Var2Lit( VarN1, 1 ), + Abc_Var2Lit( VarM0, 1 ), Abc_Var2Lit( VarM1, 1 ) }; + if ( !Exa9_KissatAddClause( p, pLits4, 4 ) ) + { + Vec_IntFree( vLits ); + Vec_IntFree( vAux ); + Vec_IntFree( vUse ); + return 0; + } + } + } + */ + } + // output connectivity (one-hot over all objects and two polarities) + Vec_IntClear( vLits ); + Vec_IntClear( vAux ); + for ( j = 1; j <= p->nObjs; j++ ) + for ( c = 0; c < 2; c++ ) + { + Vec_IntPush( vLits, Abc_Var2Lit( Exa9_ManSelVarOut(p, c, j), 0 ) ); + Vec_IntPush( vAux, Exa9_ManSelVarOutAux( p, c, j ) ); + } + if ( Vec_IntSize(vLits) == 0 || !Exa9_ManAddOneHot( p, vLits, vAux ) ) + { + Vec_IntFree( vLits ); + Vec_IntFree( vAux ); + Vec_IntFree( vUse ); + return 0; + } + // ensure each object (PI or internal) is used at least once as a fanin of some node/output + for ( j = 1; j <= p->nObjs; j++ ) + { + Vec_IntClear( vUse ); + for ( n = 0; n < p->nNodes; n++ ) + { + int Obj = p->nVars + n + 1; + if ( Obj <= j ) + continue; + for ( k = 0; k < 2; k++ ) + for ( c = 0; c < 2; c++ ) + Vec_IntPush( vUse, Abc_Var2Lit( Exa9_ManSelVar(p, n, k, c, j), 0 ) ); + } + for ( c = 0; c < 2; c++ ) + Vec_IntPush( vUse, Abc_Var2Lit( Exa9_ManSelVarOut(p, c, j), 0 ) ); + if ( Vec_IntSize(vUse) == 0 ) + continue; + if ( !Exa9_KissatAddClause( p, Vec_IntArray(vUse), Vec_IntSize(vUse) ) ) + { + Vec_IntFree( vLits ); + Vec_IntFree( vAux ); + Vec_IntFree( vUse ); + return 0; + } + } + Vec_IntFree( vLits ); + Vec_IntFree( vAux ); + Vec_IntFree( vUse ); + return 1; +} +static int Exa9_ManAddCnf( Exa9_Man_t * p, int iMint ) +{ + p->fCountStruct = 0; + int i, j, k, c; + // assign primary input values for this minterm + for ( i = 1; i <= p->nVars; i++ ) + { + int Value = (iMint >> (i-1)) & 1; + int VarOut = Exa9_ManValueVar( p, i, 2, iMint ); + if ( !Exa9_ManAddUnit( p, VarOut, !Value ) ) + return 0; + } + // internal nodes + for ( i = 0; i < p->nNodes; i++ ) + { + int Obj = p->nVars + i + 1; + int VarFan[2] = { Exa9_ManValueVar( p, Obj, 0, iMint ), Exa9_ManValueVar( p, Obj, 1, iMint ) }; + int VarOut = Exa9_ManValueVar( p, Obj, 2, iMint ); + for ( k = 0; k < 2; k++ ) + { + for ( j = 1; j < Obj; j++ ) + for ( c = 0; c < 2; c++ ) + { + int SelVar = Exa9_ManSelVar( p, i, k, c, j ); + int SrcVal = Exa9_ManValueVar( p, j, 2, iMint ); + if ( !Exa9_ManAddEquality( p, SelVar, VarFan[k], SrcVal, c ) ) + return 0; + } + } + // functionality clauses for a*b = out + { + int pLits1[2] = { Abc_Var2Lit( VarFan[0], 0 ), Abc_Var2Lit( VarOut, 1 ) }; + int pLits2[2] = { Abc_Var2Lit( VarFan[1], 0 ), Abc_Var2Lit( VarOut, 1 ) }; + int pLits3[3] = { Abc_Var2Lit( VarFan[0], 1 ), Abc_Var2Lit( VarFan[1], 1 ), Abc_Var2Lit( VarOut, 0 ) }; + if ( !Exa9_KissatAddClause( p, pLits1, 2 ) ) return 0; + if ( !Exa9_KissatAddClause( p, pLits2, 2 ) ) return 0; + if ( !Exa9_KissatAddClause( p, pLits3, 3 ) ) return 0; + } + } + // constrain the output to match the target function via selected source + { + int Value = Abc_TtGetBit( p->pTruth, iMint ); + for ( j = 1; j <= p->nObjs; j++ ) + for ( c = 0; c < 2; c++ ) + { + int SelVar = Exa9_ManSelVarOut( p, c, j ); + int SrcVal = Exa9_ManValueVar( p, j, 2, iMint ); + int pLits[2] = { Abc_Var2Lit( SelVar, 1 ), Abc_Var2Lit( SrcVal, (Value ^ c) ? 0 : 1 ) }; + if ( !Exa9_KissatAddClause( p, pLits, 2 ) ) + return 0; + } + } + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Exa9_ManFindFanin( Exa9_Man_t * p, int Obj, int k, int * pCompl ) +{ + int n = Obj - p->nVars - 1; + int j, c; + assert( Obj > p->nVars && n >= 0 && n < p->nNodes ); + for ( j = 1; j < Obj; j++ ) + for ( c = 0; c < 2; c++ ) + { + int Var = Exa9_ManSelVar( p, n, k, c, j ); + if ( Exa9_KissatVarValue(p, Var) ) + { + if ( pCompl ) + *pCompl = c; + return j; + } + } + assert( 0 ); + return -1; +} +static inline int Exa9_ManFindOutput( Exa9_Man_t * p, int * pCompl ) +{ + int j, c; + for ( j = 1; j <= p->nObjs; j++ ) + for ( c = 0; c < 2; c++ ) + if ( Exa9_KissatVarValue(p, Exa9_ManSelVarOut(p, c, j)) ) + { + if ( pCompl ) + *pCompl = c; + return j; + } + assert( 0 ); + return -1; +} +static int Exa9_ManEval( Exa9_Man_t * p ) +{ + int i, c0, c1, i0, i1; + int cOut, iOutObj; + for ( i = 1; i <= p->nVars; i++ ) + Abc_TtIthVar( Exa9_ManTruth(p, i), i-1, p->nVars ); + for ( i = p->nVars + 1; i <= p->nObjs; i++ ) + { + i0 = Exa9_ManFindFanin( p, i, 0, &c0 ); + i1 = Exa9_ManFindFanin( p, i, 1, &c1 ); + Abc_TtAndCompl( Exa9_ManTruth(p, i), Exa9_ManTruth(p, i0), c0, Exa9_ManTruth(p, i1), c1, p->nWords ); + } + iOutObj = Exa9_ManFindOutput( p, &cOut ); + if ( cOut ) + { + Abc_TtNot( Exa9_ManTruth(p, iOutObj), p->nWords ); + i0 = Abc_TtFindFirstDiffBit( Exa9_ManTruth(p, iOutObj), p->pTruth, p->nVars ); + Abc_TtNot( Exa9_ManTruth(p, iOutObj), p->nWords ); + return i0; + } + return Abc_TtFindFirstDiffBit( Exa9_ManTruth(p, iOutObj), p->pTruth, p->nVars ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static void Exa9_ManName( Exa9_Man_t * p, int Obj, char * pBuf, int fFinal ) +{ + if ( Obj <= p->nVars ) + sprintf( pBuf, "%c", 'a'+Obj-1 ); + else if ( fFinal ) + sprintf( pBuf, "F" ); + else + sprintf( pBuf, "%02d", Obj ); +} +static void Exa9_ManPrintSolution( Exa9_Man_t * p ) +{ + int i, c0, c1, i0, i1, cOut, iOutObj; + int nInv = 0; + char Buf0[16], Buf1[16]; + iOutObj = Exa9_ManFindOutput( p, &cOut ); + nInv += cOut; + for ( i = p->nVars + 1; i <= p->nObjs; i++ ) + { + Exa9_ManFindFanin( p, i, 0, &c0 ); + Exa9_ManFindFanin( p, i, 1, &c1 ); + nInv += c0 + c1; + } + printf( "Realization of given %d-input function using %d two-input and-nodes and %d inverters:\n", p->nVars, p->nNodes, nInv ); + if ( iOutObj <= p->nVars ) sprintf( Buf0, "%c", 'a'+iOutObj-1 ); + else sprintf( Buf0, "%c", 'A'+iOutObj-p->nVars-1 ); + printf( "F =%s%s\n", cOut ? " !" : " ", Buf0 ); + for ( i = p->nObjs; i > p->nVars; i-- ) + { + i0 = Exa9_ManFindFanin( p, i, 0, &c0 ); + i1 = Exa9_ManFindFanin( p, i, 1, &c1 ); + if ( i0 <= p->nVars ) sprintf( Buf0, "%c", 'a'+i0-1 ); + else sprintf( Buf0, "%c", 'A'+i0-p->nVars-1 ); + if ( i1 <= p->nVars ) sprintf( Buf1, "%c", 'a'+i1-1 ); + else sprintf( Buf1, "%c", 'A'+i1-p->nVars-1 ); + printf( "%c =%s%s & %s%s\n", 'A'+i-p->nVars-1, c0 ? " !" : " ", Buf0, c1 ? " !" : " ", Buf1 ); + } +} +static void Exa9_ManDumpBlif( Exa9_Man_t * p ) +{ + int i, c0, c1, i0, i1, cOut, iOutObj; + char pFileName[1000]; + char Buf0[16], Buf1[16], BufOut[16]; + char * pStr = Abc_UtilStrsav(p->pPars->pSymStr ? p->pPars->pSymStr : p->pPars->pTtStr); + if ( strlen(pStr) > 16 ) { + pStr[16] = '_'; + pStr[17] = '\0'; + } + sprintf( pFileName, "%s.blif", pStr ); + FILE * pFile = fopen( pFileName, "wb" ); + if ( pFile == NULL ) return; + fprintf( pFile, "# Realization of given %d-input function using %d two-input and-nodes synthesized by ABC on %s\n", p->nVars, p->nNodes, Extra_TimeStamp() ); + fprintf( pFile, ".model %s\n", pStr ); + fprintf( pFile, ".inputs" ); + for ( i = 0; i < p->nVars; i++ ) + fprintf( pFile, " %c", 'a'+i ); + fprintf( pFile, "\n.outputs F\n" ); + for ( i = p->nVars + 1; i <= p->nObjs; i++ ) + { + i0 = Exa9_ManFindFanin( p, i, 0, &c0 ); + i1 = Exa9_ManFindFanin( p, i, 1, &c1 ); + Exa9_ManName( p, i0, Buf0, 0 ); + Exa9_ManName( p, i1, Buf1, 0 ); + Exa9_ManName( p, i, BufOut, 0 ); + fprintf( pFile, ".names %s %s %s\n", Buf0, Buf1, BufOut ); + fprintf( pFile, "%d%d 1\n", !c0, !c1 ); + } + iOutObj = Exa9_ManFindOutput( p, &cOut ); + Exa9_ManName( p, iOutObj, Buf0, iOutObj == p->nObjs ); + fprintf( pFile, ".names %s F\n", Buf0 ); + fprintf( pFile, "%d 1\n", cOut ? 0 : 1 ); + fprintf( pFile, ".end\n\n" ); + fclose( pFile ); + if ( !p->pPars->fSilent ) printf( "Finished dumping the resulting network into file \"%s\".\n", pFileName ); + ABC_FREE( pStr ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Exa9_ManExactSynthesis( Bmc_EsPar_t * pPars ) +{ + extern int Exa9_ManExactSynthesisIter( Bmc_EsPar_t * pPars ); + if ( pPars->fMinNodes ) + return Exa9_ManExactSynthesisIter( pPars ); + if ( pPars->fVerbose && !pPars->fSilent ) + Abc_Print( 1, "Params: I = %d M = %d H = %d S = %d T = %d i = %d a = %d m = %d d = %d v = %d s = %d\n", + pPars->nVars, pPars->nNodes, pPars->n1HotAlgo, pPars->Seed, pPars->RuntimeLim, pPars->fUseIncr, pPars->fOnlyAnd, pPars->fMinNodes, pPars->fDumpBlif, pPars->fVerbose, pPars->fSilent ); + int status = KISSAT_UNDEC; + int Res = 0; + abctime clkTotal = Abc_Clock(); + Exa9_Man_t * p; + assert( pPars->nVars <= 14 ); + int nTruthWords = Abc_TtWordNum( pPars->nVars ); + word * pTruth = ABC_CALLOC( word, nTruthWords ); + assert( pTruth ); + if ( pPars->pSymStr ) { + word * pFun = Abc_TtSymFunGenerate( pPars->pSymStr, pPars->nVars ); + pPars->pTtStr = ABC_CALLOC( char, pPars->nVars > 2 ? (1 << (pPars->nVars-2)) + 1 : 2 ); + Extra_PrintHexadecimalString( pPars->pTtStr, (unsigned *)pFun, pPars->nVars ); + if ( !pPars->fSilent ) printf( "Generated symmetric function: %s\n", pPars->pTtStr ); + ABC_FREE( pFun ); + } + if ( pPars->pTtStr ) + Abc_TtReadHex( pTruth, pPars->pTtStr ); + else assert( 0 ); + if ( pPars->fUseIncr && !pPars->fSilent ) + printf( "Warning: Ignoring incremental option when using Kissat.\n" ); + pPars->fUseIncr = 0; + p = Exa9_ManAlloc( pPars, pTruth ); + if ( pPars->fVerbose && !pPars->fSilent ) { + int nStruct = p->nNodes * 4 * p->nObjs + 2 * p->nObjs; + int nAux = Exa9_ManCountAuxTotal( p ); + int nTotal = nStruct + nAux + p->nValVars; + const char * pAlgo = p->pPars->n1HotAlgo == 1 ? "seq" : (p->pPars->n1HotAlgo == 2 ? "bim" : (p->pPars->n1HotAlgo == 3 ? "cmd" : "naive")); + printf( "Variables: Structure = %6d. Uniqueness (%s) = %6d. Internal = %6d. Total = %6d.\n", + nStruct, pAlgo, nAux, p->nValVars, nTotal ); + //if ( pPars->Seed > 0 ) + // printf( "Kissat seed set to %d.\n", pPars->Seed ); + } + if ( Exa9_ManAddCnfStart( p ) ) + { + if ( pPars->fVerbose && !pPars->fSilent ) + { + int clausesPerMint = 0; + clausesPerMint += p->nVars; // PI assignments + for ( int i = 0; i < p->nNodes; i++ ) + { + int Obj = p->nVars + i + 1; + int choices = Obj - 1; + clausesPerMint += 2 /*fanins*/ * 2 /*polarity*/ * choices * 2; // two clauses per equality + clausesPerMint += 3; // functionality + } + clausesPerMint += 2 * p->nObjs; // output selector + const char * pAlgo = p->pPars->n1HotAlgo == 1 ? "seq" : (p->pPars->n1HotAlgo == 2 ? "bim" : (p->pPars->n1HotAlgo == 3 ? "cmd" : "naive")); + int internalTotal = clausesPerMint * p->nMints; + printf( "Clauses: Structure = %6d. Uniqueness (%s) = %6d. Internal = %6d. Total = %6d.\n", + p->nClausesStart, pAlgo, p->nClausesHot, internalTotal, p->nClausesStart + p->nClausesHot + internalTotal ); + } + if ( !pPars->fSilent ) + printf( "Running exact synthesis for %d-input function with %d two-input and-nodes...\n", p->nVars, p->nNodes ); + int iMint; + Vec_Int_t * vMints = Vec_IntAlloc( p->nMints ); + for ( iMint = 0; iMint < p->nMints; iMint++ ) + Vec_IntPush( vMints, iMint ); + if ( pPars->Seed > 0 ) + { + Abc_Random( pPars->Seed ); + for ( iMint = 1; iMint < p->nMints; iMint++ ) + { + int jMint = Abc_Random(0) % (iMint + 1); + int Temp = Vec_IntEntry( vMints, iMint ); + Vec_IntWriteEntry( vMints, iMint, Vec_IntEntry(vMints, jMint) ); + Vec_IntWriteEntry( vMints, jMint, Temp ); + } + } + status = KISSAT_UNSAT; + for ( iMint = 0; iMint < p->nMints; iMint++ ) + { + int Mint = Vec_IntEntry( vMints, iMint ); + if ( !Exa9_ManAddCnf( p, Mint ) ) + break; + } + Vec_IntFree( vMints ); + if ( iMint == p->nMints ) + { + if ( pPars->RuntimeLim ) + { + p->timeStop = Abc_Clock() + pPars->RuntimeLim * CLOCKS_PER_SEC; + kissat_set_terminate( p->pSat, p, Exa9_KissatTerminate ); + } + else + { + p->timeStop = 0; + kissat_set_terminate( p->pSat, NULL, NULL ); + } + status = kissat_solve( p->pSat ); + } + } + else + status = KISSAT_UNSAT; + + if ( status == KISSAT_SAT ) + { + int DiffMint = Exa9_ManEval( p ); + if ( DiffMint != -1 ) + printf( "******** Warning: Verification detected a mismatch at minterm %d.\n", DiffMint ); + Exa9_ManPrintSolution( p ); + if ( pPars->fDumpBlif ) + Exa9_ManDumpBlif( p ); + Res = 1; + } + else if ( status == KISSAT_UNSAT ) + { + if ( !p->pPars->fSilent ) + printf( "The problem has no solution.\n" ); + Res = 2; + } + else + { + Res = 0; + if ( pPars->RuntimeLim ) + printf( "The solver timed out after %d sec.\n", pPars->RuntimeLim ); + } + if ( !pPars->fSilent ) + Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal ); + if ( pPars->pSymStr ) + ABC_FREE( pPars->pTtStr ); + Exa9_ManFree( p ); + ABC_FREE( pTruth ); + return Res; +} + +int Exa9_ManExactSynthesisIter( Bmc_EsPar_t * pPars ) +{ + pPars->fMinNodes = 0; + int nNodeMin = pPars->nVars - 1; + int nNodeMax = pPars->nNodes, Result = 0; + for ( int n = nNodeMin; n <= nNodeMax; n++ ) { + //printf( "\nTrying M = %d:\n", n ); + printf( "\n" ); + pPars->nNodes = n; + Result = Exa9_ManExactSynthesis(pPars); + fflush( stdout ); + if ( Result == 1 ) + break; + } + return Result; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + +ABC_NAMESPACE_IMPL_END diff --git a/src/sat/bmc/module.make b/src/sat/bmc/module.make index e0e86212b..3bb7babf4 100644 --- a/src/sat/bmc/module.make +++ b/src/sat/bmc/module.make @@ -27,6 +27,7 @@ SRC += src/sat/bmc/bmcBCore.c \ src/sat/bmc/bmcMaj3.c \ src/sat/bmc/bmcMaj7.c \ src/sat/bmc/bmcMaj8.c \ + src/sat/bmc/bmcMaj9.c \ src/sat/bmc/bmcMaxi.c \ src/sat/bmc/bmcMesh.c \ src/sat/bmc/bmcMesh2.c \