ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Classes | Macros | Typedefs | Functions
bmcMaj.c File Reference
#include "bmc.h"
#include "misc/extra/extra.h"
#include "misc/util/utilTruth.h"
#include "sat/glucose/AbcGlucose.h"
#include "aig/miniaig/miniaig.h"
#include "base/io/ioResub.h"
#include "base/main/main.h"
#include "base/cmd/cmd.h"
#include <unistd.h>
Include dependency graph for bmcMaj.c:

Go to the source code of this file.

Classes

struct  Maj_Man_t_
 
struct  Exa_Man_t_
 
struct  Exa3_Man_t_
 
struct  Exa4_Man_t_
 
struct  Exa5_Man_t_
 
struct  Exa6_Man_t_
 

Macros

#define MAJ_NOBJS   64
 DECLARATIONS ///.
 

Typedefs

typedef struct Maj_Man_t_ Maj_Man_t
 
typedef struct Exa_Man_t_ Exa_Man_t
 
typedef struct Exa3_Man_t_ Exa3_Man_t
 
typedef struct Exa4_Man_t_ Exa4_Man_t
 
typedef struct Exa5_Man_t_ Exa5_Man_t
 
typedef struct Exa6_Man_t_ Exa6_Man_t
 

Functions

int Maj_ManValue (int iMint, int nVars)
 FUNCTION DEFINITIONS ///.
 
Vec_Wrd_t * Maj_ManTruthTables (Maj_Man_t *p)
 
int Maj_ManMarkup (Maj_Man_t *p)
 
Maj_Man_t * Maj_ManAlloc (int nVars, int nNodes, int fUseConst, int fUseLine)
 
void Maj_ManFree (Maj_Man_t *p)
 
void Maj_ManPrintSolution (Maj_Man_t *p)
 
int Maj_ManAddCnfStart (Maj_Man_t *p)
 
int Maj_ManAddCnf (Maj_Man_t *p, int iMint)
 
int Maj_ManExactSynthesis (int nVars, int nNodes, int fUseConst, int fUseLine, int fVerbose)
 
Vec_Wrd_t * Exa_ManTruthTables (Exa_Man_t *p)
 
int Exa_ManMarkup (Exa_Man_t *p)
 
Exa_Man_t * Exa_ManAlloc (Bmc_EsPar_t *pPars, word *pTruth)
 
void Exa_ManFree (Exa_Man_t *p)
 
void Exa_ManDumpBlif (Exa_Man_t *p, int fCompl)
 
void Exa_ManPrintSolution (Exa_Man_t *p, int fCompl)
 
int Exa_ManAddCnfAdd (Exa_Man_t *p, int *pnAdded)
 
int Exa_ManSolverSolve (Exa_Man_t *p)
 
int Exa_ManAddCnfStart (Exa_Man_t *p, int fOnlyAnd)
 
int Exa_ManAddCnf (Exa_Man_t *p, int iMint)
 
void Exa_ManExactSynthesis (Bmc_EsPar_t *pPars)
 
Vec_Wec_t * Exa3_ChooseInputVars_int (int nVars, int nLuts, int nLutSize)
 
Vec_Int_t * Exa3_CountInputVars (int nVars, Vec_Wec_t *p)
 
Vec_Wec_t * Exa3_ChooseInputVars (int nVars, int nLuts, int nLutSize)
 
void Exa3_ManPrint (Exa3_Man_t *p, int i, int iMint, abctime clk)
 
int Exa3_ManExactSynthesis (Bmc_EsPar_t *pPars)
 
void Exa3_ManExactSynthesisRand (Bmc_EsPar_t *pPars)
 
void Exa_ManIsNormalized (Vec_Wrd_t *vSimsIn, Vec_Wrd_t *vSimsOut)
 
void Exa_ManMiniPrint (Mini_Aig_t *p, int nIns)
 
void Exa_ManMiniVerify (Mini_Aig_t *p, Vec_Wrd_t *vSimsIn, Vec_Wrd_t *vSimsOut)
 
Vec_Int_t * Exa4_ManParse (char *pFileName)
 DECLARATIONS ///.
 
Vec_Int_t * Exa4_ManSolve (char *pFileNameIn, char *pFileNameOut, int TimeOut, int fVerbose)
 
int Exa4_ManMarkup (Exa4_Man_t *p)
 
Exa4_Man_t * Exa4_ManAlloc (Vec_Wrd_t *vSimsIn, Vec_Wrd_t *vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, int fVerbose)
 
void Exa4_ManFree (Exa4_Man_t *p)
 
int Exa4_ManGenStart (Exa4_Man_t *p, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fCard, char *pGuide)
 
void Exa4_ManGenMint (Exa4_Man_t *p, int iMint, int fOnlyAnd, int fFancy)
 
void Exa4_ManGenCnf (Exa4_Man_t *p, char *pFileName, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fCard, char *pGuide)
 
void Exa4_ManPrintSolution (Exa4_Man_t *p, Vec_Int_t *vValues, int fFancy)
 
Mini_Aig_t * Exa4_ManMiniAig (Exa4_Man_t *p, Vec_Int_t *vValues, int fFancy)
 
Mini_Aig_t * Exa4_ManGenTest (Vec_Wrd_t *vSimsIn, Vec_Wrd_t *vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, int TimeOut, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fVerbose, int fCard, char *pGuide)
 
void Exa_ManExactSynthesis4_ (Bmc_EsPar_t *pPars)
 
void Exa_ManExactSynthesis4 (Bmc_EsPar_t *pPars)
 
int Exa5_ManMarkup (Exa5_Man_t *p)
 
Exa5_Man_t * Exa5_ManAlloc (Vec_Wrd_t *vSimsIn, Vec_Wrd_t *vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, int fVerbose)
 
void Exa5_ManFree (Exa5_Man_t *p)
 
int Exa5_ManGenStart (Exa5_Man_t *p, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans)
 
void Exa5_ManGenMint (Exa5_Man_t *p, int iMint, int fOnlyAnd, int fFancy)
 
void Exa5_ManGenCnf (Exa5_Man_t *p, char *pFileName, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans)
 
void Exa5_ManPrintSolution (Exa5_Man_t *p, Vec_Int_t *vValues, int fFancy)
 
Mini_Aig_t * Exa5_ManMiniAig (Exa5_Man_t *p, Vec_Int_t *vValues)
 
Mini_Aig_t * Exa5_ManGenTest (Vec_Wrd_t *vSimsIn, Vec_Wrd_t *vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, int TimeOut, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fVerbose)
 
void Exa_ManExactSynthesis5 (Bmc_EsPar_t *pPars)
 
void Mini_AigPrintArray (FILE *pFile, Mini_Aig_t *p)
 
word Mini_AigWriteEntry (Mini_Aig_t *p)
 
word Abc_TtConvertEntry (word Res)
 
word Exa_ManExactSynthesis4VarsOne (int Index, int Truth, int nNodes)
 
void Exa_ManExactSynthesis4Vars ()
 
void Exa6_SortSims (Vec_Wrd_t *vSimsDiv, Vec_Wrd_t *vSimsOut)
 
int Exa6_ReadFile (char *pFileName, Vec_Wrd_t **pvSimsDiv, Vec_Wrd_t **pvSimsOut, int *pnDivs, int *pnOuts)
 
void Exa6_WriteFile (char *pFileName, int nVars, word *pTruths, int nTruths)
 
void Exa6_WriteFile2 (char *pFileName, int nVars, int nDivs, int nOuts, Vec_Wrd_t *vSimsDiv, Vec_Wrd_t *vSimsOut)
 
void Exa6_GenCount (word *pTruths, int nVars)
 
void Exa6_GenProd (word *pTruths, int nVars)
 
void Exa_ManExactSynthesis6_ (Bmc_EsPar_t *pPars, char *pFileName)
 
int Gia_ManDupMini_rec (Gia_Man_t *pNew, Gia_Man_t *p, Gia_Obj_t *pObj)
 
Gia_Man_t * Gia_ManDupMini (Gia_Man_t *p, Vec_Int_t *vIns, Vec_Int_t *vDivs, Vec_Int_t *vOuts, Mini_Aig_t *pMini)
 
int Exa6_ManMarkup (Exa6_Man_t *p)
 
Exa6_Man_t * Exa6_ManAlloc (Vec_Wrd_t *vSimsIn, Vec_Wrd_t *vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, int fVerbose)
 
void Exa6_ManFree (Exa6_Man_t *p)
 
int Exa6_ManGenStart (Exa6_Man_t *p, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans)
 
void Exa6_ManGenMint (Exa6_Man_t *p, int iMint, int fOnlyAnd, int fFancy)
 
void Exa6_ManGenCnf (Exa6_Man_t *p, char *pFileName, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans)
 
void Exa6_ManPrintSolution (Exa6_Man_t *p, Vec_Int_t *vValues, int fFancy)
 
Mini_Aig_t * Exa6_ManMiniAig (Exa6_Man_t *p, Vec_Int_t *vValues, int fFancy)
 
Mini_Aig_t * Exa6_ManGenTest (Vec_Wrd_t *vSimsIn, Vec_Wrd_t *vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, int TimeOut, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fVerbose)
 
Mini_Aig_t * Mini_AigDupCompl (Mini_Aig_t *p, int ComplIns, int ComplOuts)
 
word Exa6_ManPolarMinterm (word Mint, int nOuts, int Polar)
 
int Exa6_ManFindPolar (word First, int nOuts)
 
Vec_Wrd_t * Exa6_ManTransformOutputs (Vec_Wrd_t *vOuts, int nOuts)
 
Vec_Wrd_t * Exa6_ManTransformInputs (Vec_Wrd_t *vIns)
 
void Exa_ManExactPrint (Vec_Wrd_t *vSimsDiv, Vec_Wrd_t *vSimsOut, int nDivs, int nOuts)
 
Mini_Aig_t * Exa_ManExactSynthesis6Int (Vec_Wrd_t *vSimsDiv, Vec_Wrd_t *vSimsOut, int nVars, int nDivs, int nOuts, int nNodes, int fOnlyAnd, int fVerbose, char *pFileName)
 
void Exa_ManExactSynthesis6 (Bmc_EsPar_t *pPars, char *pFileName)
 
int Exa7_GetVar (int n, int i, int j, int m)
 
int Exa7_ManGenCnf (char *pFileName, word *pTruth, int nVars, int nNodes, int GateSize)
 
void Exa_ManDumpVerilog (Vec_Int_t *vValues, int nVars, int nNodes, int GateSize, word *pTruth)
 
void Exa_ManExactSynthesis7 (Bmc_EsPar_t *pPars, int GateSize)
 
void Exa_NpnCascadeTest ()
 
void Exa_NpnCascadeTest6 ()
 

Macro Definition Documentation

◆ MAJ_NOBJS

#define MAJ_NOBJS   64

DECLARATIONS ///.

CFile****************************************************************

FileName [bmcMaj.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
bmcMaj.c,v 1.00 2017/10/01 00:00:00 alanmi Exp

]

Definition at line 44 of file bmcMaj.c.

Typedef Documentation

◆ Exa3_Man_t

typedef struct Exa3_Man_t_ Exa3_Man_t

Definition at line 994 of file bmcMaj.c.

◆ Exa4_Man_t

typedef struct Exa4_Man_t_ Exa4_Man_t

Definition at line 1889 of file bmcMaj.c.

◆ Exa5_Man_t

typedef struct Exa5_Man_t_ Exa5_Man_t

Definition at line 2475 of file bmcMaj.c.

◆ Exa6_Man_t

typedef struct Exa6_Man_t_ Exa6_Man_t

Definition at line 3420 of file bmcMaj.c.

◆ Exa_Man_t

typedef struct Exa_Man_t_ Exa_Man_t

Definition at line 421 of file bmcMaj.c.

◆ Maj_Man_t

typedef struct Maj_Man_t_ Maj_Man_t

Definition at line 46 of file bmcMaj.c.

Function Documentation

◆ Abc_TtConvertEntry()

word Abc_TtConvertEntry ( word Res)

Definition at line 3027 of file bmcMaj.c.

3028{
3029 unsigned First = (unsigned)Res;
3030 unsigned Second = (unsigned)(Res >> 32);
3031 word Fun0, Fun1, Nodes[16] = {0}; int i, k = 5;
3032 for ( i = 0; i < 4; i++ )
3033 Nodes[i+1] = s_Truths6[i];
3034 for ( i = 0; i < 4; i++ )
3035 {
3036 int Lit0, Lit1, Pair = (First >> (i*8)) & 0xFF;
3037 if ( Pair == 0 )
3038 break;
3039 Lit0 = Pair & 0xF;
3040 Lit1 = Pair >> 4;
3041 assert( Lit0 != Lit1 );
3042 Fun0 = (Lit0 & 1) ? ~Nodes[Lit0 >> 1] : Nodes[Lit0 >> 1];
3043 Fun1 = (Lit1 & 1) ? ~Nodes[Lit1 >> 1] : Nodes[Lit1 >> 1];
3044 Nodes[k++] = Lit0 < Lit1 ? Fun0 & Fun1 : Fun0 ^ Fun1;
3045 }
3046 for ( i = 0; i < 3; i++ )
3047 {
3048 int Lit0, Lit1, Pair = (Second >> (i*10)) & 0x3FF;
3049 if ( Pair == 0 )
3050 break;
3051 Lit0 = Pair & 0x1F;
3052 Lit1 = Pair >> 5;
3053 assert( Lit0 != Lit1 );
3054 Fun0 = (Lit0 & 1) ? ~Nodes[Lit0 >> 1] : Nodes[Lit0 >> 1];
3055 Fun1 = (Lit1 & 1) ? ~Nodes[Lit1 >> 1] : Nodes[Lit1 >> 1];
3056 Nodes[k++] = Lit0 < Lit1 ? Fun0 & Fun1 : Fun0 ^ Fun1;
3057 }
3058 return (Res >> 62) ? ~Nodes[k-1] : Nodes[k-1];
3059}
word
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
assert
#define assert(ex)
Definition util_old.h:213
Here is the caller graph for this function:

◆ Exa3_ChooseInputVars()

Vec_Wec_t * Exa3_ChooseInputVars ( int nVars,
int nLuts,
int nLutSize )

Definition at line 1077 of file bmcMaj.c.

1078{
1079 for ( int i = 0; i < 1000; i++ ) {
1080 Vec_Wec_t * p = Exa3_ChooseInputVars_int( nVars, nLuts, nLutSize );
1081 Vec_Int_t * q = Exa3_CountInputVars( nVars, p );
1082 int RetValue = Vec_IntFind( q, 0 );
1083 Vec_IntFree( q );
1084 if ( RetValue == -1 )
1085 return p;
1086 Vec_WecFree( p );
1087 }
1088 assert( 0 );
1089 return NULL;
1090}
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Exa3_CountInputVars
Vec_Int_t * Exa3_CountInputVars(int nVars, Vec_Wec_t *p)
Definition bmcMaj.c:1068
Exa3_ChooseInputVars_int
Vec_Wec_t * Exa3_ChooseInputVars_int(int nVars, int nLuts, int nLutSize)
Definition bmcMaj.c:1055
p
Cube * p
Definition exorList.c:222
Vec_Wec_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Wec_t_ Vec_Wec_t
INCLUDES ///.
Definition vecWec.h:42
Here is the call graph for this function:

◆ Exa3_ChooseInputVars_int()

Vec_Wec_t * Exa3_ChooseInputVars_int ( int nVars,
int nLuts,
int nLutSize )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1055 of file bmcMaj.c.

1056{
1057 Vec_Wec_t * p = Vec_WecStart( nLuts );
1058 Vec_Int_t * vLevel; int i;
1059 Vec_WecForEachLevel( p, vLevel, i ) {
1060 do {
1061 int iVar = (Abc_Random(0) ^ Abc_Random(0) ^ Abc_Random(0)) % nVars;
1062 Vec_IntPushUniqueOrder( vLevel, iVar );
1063 }
1064 while ( Vec_IntSize(vLevel) < nLutSize-(int)(i>0) );
1065 }
1066 return p;
1067}
Abc_Random
unsigned Abc_Random(int fReset)
Definition utilSort.c:1004
Vec_WecForEachLevel
#define Vec_WecForEachLevel(vGlob, vVec, i)
MACRO DEFINITIONS ///.
Definition vecWec.h:55
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Exa3_CountInputVars()

Vec_Int_t * Exa3_CountInputVars ( int nVars,
Vec_Wec_t * p )

Definition at line 1068 of file bmcMaj.c.

1069{
1070 Vec_Int_t * vLevel; int i, k, Obj;
1071 Vec_Int_t * vCounts = Vec_IntStart( nVars );
1072 Vec_WecForEachLevel( p, vLevel, i )
1073 Vec_IntForEachEntry( vLevel, Obj, k )
1074 Vec_IntAddToEntry( vCounts, Obj, 1 );
1075 return vCounts;
1076}
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Here is the caller graph for this function:

◆ Exa3_ManExactSynthesis()

int Exa3_ManExactSynthesis ( Bmc_EsPar_t * pPars)

Definition at line 1598 of file bmcMaj.c.

1599{
1600 int i, status, Res = 0, iMint = 1;
1601 abctime clkTotal = Abc_Clock();
1602 Exa3_Man_t * p; int fCompl = 0;
1603 word pTruth[16];
1604 if ( pPars->pSymStr ) {
1605 word * pFun = Abc_TtSymFunGenerate( pPars->pSymStr, pPars->nVars );
1606 pPars->pTtStr = ABC_CALLOC( char, pPars->nVars > 2 ? (1 << (pPars->nVars-2)) + 1 : 2 );
1607 Extra_PrintHexadecimalString( pPars->pTtStr, (unsigned *)pFun, pPars->nVars );
1608 printf( "Generated symmetric function: %s\n", pPars->pTtStr );
1609 ABC_FREE( pFun );
1610 }
1611 if ( pPars->pTtStr )
1612 Abc_TtReadHex( pTruth, pPars->pTtStr );
1613 else assert( 0 );
1614 assert( pPars->nVars <= 10 );
1615 assert( pPars->nLutSize <= 6 );
1616 p = Exa3_ManAlloc( pPars, pTruth );
1617 if ( pTruth[0] & 1 ) { fCompl = 1; Abc_TtNot( pTruth, p->nWords ); }
1618 status = Exa3_ManAddCnfStart( p, pPars->fOnlyAnd );
1619 assert( status );
1620 printf( "Running exact synthesis for %d-input function with %d %d-input LUTs...\n", p->nVars, p->nNodes, p->nLutSize );
1621 if ( pPars->fUseIncr )
1622 {
1623 bmcg_sat_solver_set_nvars( p->pSat, p->iVar + p->nNodes*(1 << p->nVars) );
1624 status = bmcg_sat_solver_solve( p->pSat, NULL, 0 );
1625 assert( status == GLUCOSE_SAT );
1626 }
1627 for ( i = 0; iMint != -1; i++ )
1628 {
1629 if ( pPars->fUseIncr ? !Exa3_ManAddCnf2( p, iMint ) : !Exa3_ManAddCnf( p, iMint ) )
1630 break;
1631 status = bmcg_sat_solver_solve( p->pSat, NULL, 0 );
1632 if ( pPars->fVerbose && (!pPars->fUseIncr || i % 100 == 0) )
1633 Exa3_ManPrint( p, i, iMint, Abc_Clock() - clkTotal );
1634 if ( status == GLUCOSE_UNSAT || status == GLUCOSE_UNDEC )
1635 break;
1636 iMint = Exa3_ManEval( p );
1637 }
1638 if ( pPars->fVerbose && status != GLUCOSE_UNDEC )
1639 Exa3_ManPrint( p, i, iMint, Abc_Clock() - clkTotal );
1640 if ( iMint == -1 )
1641 Exa3_ManPrintSolution( p, fCompl ), Res = 1;
1642 else if ( status == GLUCOSE_UNDEC )
1643 printf( "The solver timed out after %d sec.\n", pPars->RuntimeLim );
1644 else
1645 printf( "The problem has no solution.\n" );
1646 printf( "Added = %d. Tried = %d. ", p->nUsed[1], p->nUsed[0] );
1647 Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
1648 if ( iMint == -1 )
1649 Exa3_ManDumpBlif( p, fCompl );
1650 if ( pPars->pSymStr )
1651 ABC_FREE( pPars->pTtStr );
1652 Exa3_ManFree( p );
1653 return Res;
1654}
bmcg_sat_solver_solve
int bmcg_sat_solver_solve(bmcg_sat_solver *s, int *plits, int nlits)
Definition AbcGlucose.cpp:170
bmcg_sat_solver_set_nvars
void bmcg_sat_solver_set_nvars(bmcg_sat_solver *s, int nvars)
Definition AbcGlucose.cpp:186
GLUCOSE_UNDEC
#define GLUCOSE_UNDEC
Definition AbcGlucose.h:36
GLUCOSE_UNSAT
#define GLUCOSE_UNSAT
INCLUDES ///.
Definition AbcGlucose.h:34
GLUCOSE_SAT
#define GLUCOSE_SAT
Definition AbcGlucose.h:35
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition abc_global.h:265
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
Exa3_ManPrint
void Exa3_ManPrint(Exa3_Man_t *p, int i, int iMint, abctime clk)
Definition bmcMaj.c:1589
Exa3_Man_t
struct Exa3_Man_t_ Exa3_Man_t
Definition bmcMaj.c:994
Extra_PrintHexadecimalString
void Extra_PrintHexadecimalString(char *pString, unsigned Sign[], int nVars)
Definition extraUtilFile.c:611
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Exa3_ManExactSynthesisRand()

void Exa3_ManExactSynthesisRand ( Bmc_EsPar_t * pPars)

Definition at line 1655 of file bmcMaj.c.

1656{
1657 int i, k, nDecs = 0, nWords = Abc_TtWordNum(pPars->nVars);
1658 word * pFun = ABC_ALLOC( word, nWords );
1659 unsigned Rand0 = Abc_Random(1);
1660 for ( i = 0; i < pPars->Seed; i++ )
1661 Rand0 = Abc_Random(0);
1662 for ( i = 0; i < pPars->nRandFuncs; i++ ) {
1663 if ( pPars->nMintNum == 0 )
1664 for ( k = 0; k < nWords; k++ )
1665 pFun[k] = Rand0 ^ Abc_RandomW(0);
1666 else {
1667 Abc_TtClear( pFun, nWords );
1668 for ( k = 0; k < pPars->nMintNum; k++ ) {
1669 int iMint = 0;
1670 do iMint = (Rand0 ^ Abc_Random(0)) % (1 << pPars->nVars);
1671 while ( Abc_TtGetBit(pFun, iMint) );
1672 Abc_TtSetBit( pFun, iMint );
1673 }
1674 }
1675 pPars->pTtStr = ABC_CALLOC( char, pPars->nVars > 2 ? (1 << (pPars->nVars-2)) + 1 : 2 );
1676 Extra_PrintHexadecimalString( pPars->pTtStr, (unsigned *)pFun, pPars->nVars );
1677 printf( "\nFunction %4d : ", i );
1678 if ( pPars->nMintNum )
1679 printf( "Random function has %d positive minterms.", pPars->nMintNum );
1680 printf( "\n" );
1681 if ( pPars->fVerbose )
1682 printf( "Truth table : %s\n", pPars->pTtStr );
1683 nDecs += Exa3_ManExactSynthesis( pPars );
1684 ABC_FREE( pPars->pTtStr );
1685 }
1686 printf( "\nDecomposable are %d (out of %d) functions (%.2f %%).\n\n", nDecs, pPars->nRandFuncs, 100.0*nDecs/pPars->nRandFuncs );
1687 ABC_FREE( pFun );
1688}
nWords
int nWords
Definition abcNpn.c:127
Abc_RandomW
word Abc_RandomW(int fReset)
Definition utilSort.c:1022
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
Exa3_ManExactSynthesis
int Exa3_ManExactSynthesis(Bmc_EsPar_t *pPars)
Definition bmcMaj.c:1598
Here is the call graph for this function:

◆ Exa3_ManPrint()

void Exa3_ManPrint ( Exa3_Man_t * p,
int i,
int iMint,
abctime clk )

Definition at line 1589 of file bmcMaj.c.

1590{
1591 printf( "Iter%6d : ", i );
1592 Extra_PrintBinary( stdout, (unsigned *)&iMint, p->nVars );
1593 printf( " Var =%5d ", bmcg_sat_solver_varnum(p->pSat) );
1594 printf( "Cla =%6d ", bmcg_sat_solver_clausenum(p->pSat) );
1595 printf( "Conf =%9d ", bmcg_sat_solver_conflictnum(p->pSat) );
1596 Abc_PrintTime( 1, "Time", clk );
1597}
bmcg_sat_solver_conflictnum
int bmcg_sat_solver_conflictnum(bmcg_sat_solver *s)
Definition AbcGlucose.cpp:257
bmcg_sat_solver_varnum
int bmcg_sat_solver_varnum(bmcg_sat_solver *s)
Definition AbcGlucose.cpp:245
bmcg_sat_solver_clausenum
int bmcg_sat_solver_clausenum(bmcg_sat_solver *s)
Definition AbcGlucose.cpp:249
Extra_PrintBinary
void Extra_PrintBinary(FILE *pFile, unsigned Sign[], int nBits)
Definition extraUtilFile.c:516
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Exa4_ManAlloc()

Exa4_Man_t * Exa4_ManAlloc ( Vec_Wrd_t * vSimsIn,
Vec_Wrd_t * vSimsOut,
int nIns,
int nDivs,
int nOuts,
int nNodes,
int fVerbose )

Definition at line 1976 of file bmcMaj.c.

1977{
1978 Exa4_Man_t * p = ABC_CALLOC( Exa4_Man_t, 1 );
1979 assert( Vec_WrdSize(vSimsIn) == Vec_WrdSize(vSimsOut) );
1980 p->vSimsIn = vSimsIn;
1981 p->vSimsOut = vSimsOut;
1982 p->fVerbose = fVerbose;
1983 p->nIns = nIns;
1984 p->nDivs = nDivs;
1985 p->nNodes = nNodes;
1986 p->nOuts = nOuts;
1987 p->nObjs = p->nDivs + p->nNodes + p->nOuts;
1988 p->nCnfVars = Exa4_ManMarkup( p );
1989 return p;
1990}
Exa4_ManMarkup
int Exa4_ManMarkup(Exa4_Man_t *p)
Definition bmcMaj.c:1917
Exa4_Man_t
struct Exa4_Man_t_ Exa4_Man_t
Definition bmcMaj.c:1889
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Exa4_ManFree()

void Exa4_ManFree ( Exa4_Man_t * p)

Definition at line 1991 of file bmcMaj.c.

1992{
1993 ABC_FREE( p );
1994}
Here is the caller graph for this function:

◆ Exa4_ManGenCnf()

void Exa4_ManGenCnf ( Exa4_Man_t * p,
char * pFileName,
int fOnlyAnd,
int fFancy,
int fOrderNodes,
int fUniqFans,
int fCard,
char * pGuide )

Definition at line 2221 of file bmcMaj.c.

2222{
2223 int m;
2224 assert( p->pFile == NULL );
2225 p->pFile = fopen( pFileName, "wb" );
2226 fputs( "p cnf \n", p->pFile );
2227 Exa4_ManGenStart( p, fOnlyAnd, fFancy, fOrderNodes, fUniqFans, fCard, pGuide );
2228 for ( m = 1; m < Vec_WrdSize(p->vSimsIn); m++ )
2229 Exa4_ManGenMint( p, m, fOnlyAnd, fFancy );
2230 rewind( p->pFile );
2231 fprintf( p->pFile, "p %cnf %d %d", fCard ? 'k' : 'c', p->nCnfVars, p->nCnfClauses );
2232 fclose( p->pFile );
2233}
Exa4_ManGenMint
void Exa4_ManGenMint(Exa4_Man_t *p, int iMint, int fOnlyAnd, int fFancy)
Definition bmcMaj.c:2142
Exa4_ManGenStart
int Exa4_ManGenStart(Exa4_Man_t *p, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fCard, char *pGuide)
Definition bmcMaj.c:2041
rewind
VOID_HACK rewind()
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Exa4_ManGenMint()

void Exa4_ManGenMint ( Exa4_Man_t * p,
int iMint,
int fOnlyAnd,
int fFancy )

Definition at line 2142 of file bmcMaj.c.

2143{
2144 int iNodeVar = p->nCnfVars + 3*p->nNodes*(iMint - Vec_WrdSize(p->vSimsIn));
2145 int iOutMint = Abc_Tt6FirstBit( Vec_WrdEntry(p->vSimsOut, iMint) );
2146 int i, k, n, j, VarVals[MAJ_NOBJS];
2147 assert( p->nObjs <= MAJ_NOBJS );
2148 assert( iMint < Vec_WrdSize(p->vSimsIn) );
2149 for ( i = 0; i < p->nDivs; i++ )
2150 VarVals[i] = (Vec_WrdEntry(p->vSimsIn, iMint) >> i) & 1;
2151 for ( i = 0; i < p->nNodes; i++ )
2152 VarVals[p->nDivs + i] = Abc_Var2Lit(iNodeVar + 3*i + 2, 0);
2153 for ( i = 0; i < p->nOuts; i++ )
2154 VarVals[p->nDivs + p->nNodes + i] = (iOutMint >> i) & 1;
2155 if ( 0 )
2156 {
2157 printf( "Adding minterm %d: ", iMint );
2158 for ( i = 0; i < p->nObjs; i++ )
2159 printf( " %d=%d", i, VarVals[i] );
2160 printf( "\n" );
2161 }
2162 for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ )
2163 {
2164 int iVarStart = 1 + 5*(i - p->nDivs);//
2165 int iBaseVarI = iNodeVar + 3*(i - p->nDivs);
2166 for ( k = 0; k < 2; k++ )
2167 for ( j = 0; j < i; j++ ) if ( p->VarMarks[i][k][j] )
2168 for ( n = 0; n < 2; n++ )
2169 Exa4_ManAddClause4( p, Abc_Var2Lit(p->VarMarks[i][k][j], 1), Abc_Var2Lit(iBaseVarI + k, n), Abc_LitNotCond(VarVals[j], !n), 0);
2170 if ( fFancy )
2171 {
2172 // Clauses for a*b = c
2173 // a + ~c
2174 // b + ~c
2175 // ~a + ~b + c
2176 Exa4_ManAddClause4( p, Abc_Var2Lit(iVarStart + 0, 1), Abc_Var2Lit(iBaseVarI + 0, 0), 0, Abc_Var2Lit(iBaseVarI + 2, 1) );
2177 Exa4_ManAddClause4( p, Abc_Var2Lit(iVarStart + 0, 1), 0, Abc_Var2Lit(iBaseVarI + 1, 0), Abc_Var2Lit(iBaseVarI + 2, 1) );
2178 Exa4_ManAddClause4( p, Abc_Var2Lit(iVarStart + 0, 1), Abc_Var2Lit(iBaseVarI + 0, 1), Abc_Var2Lit(iBaseVarI + 1, 1), Abc_Var2Lit(iBaseVarI + 2, 0) );
2179
2180 Exa4_ManAddClause4( p, Abc_Var2Lit(iVarStart + 1, 1), Abc_Var2Lit(iBaseVarI + 0, 1), 0, Abc_Var2Lit(iBaseVarI + 2, 1) );
2181 Exa4_ManAddClause4( p, Abc_Var2Lit(iVarStart + 1, 1), 0, Abc_Var2Lit(iBaseVarI + 1, 0), Abc_Var2Lit(iBaseVarI + 2, 1) );
2182 Exa4_ManAddClause4( p, Abc_Var2Lit(iVarStart + 1, 1), Abc_Var2Lit(iBaseVarI + 0, 0), Abc_Var2Lit(iBaseVarI + 1, 1), Abc_Var2Lit(iBaseVarI + 2, 0) );
2183
2184 Exa4_ManAddClause4( p, Abc_Var2Lit(iVarStart + 2, 1), Abc_Var2Lit(iBaseVarI + 0, 0), 0, Abc_Var2Lit(iBaseVarI + 2, 1) );
2185 Exa4_ManAddClause4( p, Abc_Var2Lit(iVarStart + 2, 1), 0, Abc_Var2Lit(iBaseVarI + 1, 1), Abc_Var2Lit(iBaseVarI + 2, 1) );
2186 Exa4_ManAddClause4( p, Abc_Var2Lit(iVarStart + 2, 1), Abc_Var2Lit(iBaseVarI + 0, 1), Abc_Var2Lit(iBaseVarI + 1, 0), Abc_Var2Lit(iBaseVarI + 2, 0) );
2187 // Clauses for a+b = c
2188 // ~a + c
2189 // ~b + c
2190 // a + b + ~c
2191 Exa4_ManAddClause4( p, Abc_Var2Lit(iVarStart + 3, 1), Abc_Var2Lit(iBaseVarI + 0, 1), 0, Abc_Var2Lit(iBaseVarI + 2, 0) );
2192 Exa4_ManAddClause4( p, Abc_Var2Lit(iVarStart + 3, 1), 0, Abc_Var2Lit(iBaseVarI + 1, 1), Abc_Var2Lit(iBaseVarI + 2, 0) );
2193 Exa4_ManAddClause4( p, Abc_Var2Lit(iVarStart + 3, 1), Abc_Var2Lit(iBaseVarI + 0, 0), Abc_Var2Lit(iBaseVarI + 1, 0), Abc_Var2Lit(iBaseVarI + 2, 1) );
2194 // Clauses for a^b = c
2195 // ~a + ~b + ~c
2196 // ~a + b + c
2197 // a + ~b + c
2198 // a + b + ~c
2199 if ( !fOnlyAnd )
2200 {
2201 Exa4_ManAddClause4( p, Abc_Var2Lit(iVarStart + 4, 1), Abc_Var2Lit(iBaseVarI + 0, 1), Abc_Var2Lit(iBaseVarI + 1, 1), Abc_Var2Lit(iBaseVarI + 2, 1) );
2202 Exa4_ManAddClause4( p, Abc_Var2Lit(iVarStart + 4, 1), Abc_Var2Lit(iBaseVarI + 0, 1), Abc_Var2Lit(iBaseVarI + 1, 0), Abc_Var2Lit(iBaseVarI + 2, 0) );
2203 Exa4_ManAddClause4( p, Abc_Var2Lit(iVarStart + 4, 1), Abc_Var2Lit(iBaseVarI + 0, 0), Abc_Var2Lit(iBaseVarI + 1, 1), Abc_Var2Lit(iBaseVarI + 2, 0) );
2204 Exa4_ManAddClause4( p, Abc_Var2Lit(iVarStart + 4, 1), Abc_Var2Lit(iBaseVarI + 0, 0), Abc_Var2Lit(iBaseVarI + 1, 0), Abc_Var2Lit(iBaseVarI + 2, 1) );
2205 }
2206 }
2207 else
2208 {
2209 for ( k = 0; k < 4; k++ )
2210 for ( n = 0; n < 2; n++ )
2211 Exa4_ManAddClause4( p, Abc_Var2Lit(iBaseVarI + 0, k&1), Abc_Var2Lit(iBaseVarI + 1, k>>1), Abc_Var2Lit(iBaseVarI + 2, !n), Abc_Var2Lit(k ? iVarStart + k-1 : 0, n));
2212 }
2213 }
2214 for ( i = p->nDivs + p->nNodes; i < p->nObjs; i++ )
2215 {
2216 for ( j = 0; j < p->nDivs + p->nNodes; j++ ) if ( p->VarMarks[i][0][j] )
2217 for ( n = 0; n < 2; n++ )
2218 Exa4_ManAddClause4( p, Abc_Var2Lit(p->VarMarks[i][0][j], 1), Abc_LitNotCond(VarVals[j], n), Abc_LitNotCond(VarVals[i], !n), 0);
2219 }
2220}
MAJ_NOBJS
#define MAJ_NOBJS
Definition synthesisEngine.hpp:37
Here is the caller graph for this function:

◆ Exa4_ManGenStart()

int Exa4_ManGenStart ( Exa4_Man_t * p,
int fOnlyAnd,
int fFancy,
int fOrderNodes,
int fUniqFans,
int fCard,
char * pGuide )

Definition at line 2041 of file bmcMaj.c.

2042{
2043 extern Vec_Int_t * Gia_ManKSatGenLevels( char * pGuide, int nIns, int nNodes );
2044 Vec_Int_t * vRes = pGuide ? Gia_ManKSatGenLevels( pGuide, p->nDivs, p->nNodes ) : NULL;
2045 int pLits[2*MAJ_NOBJS], i, j, k, n, m, nLits, Start, Stop;
2046 if ( vRes ) {
2047 n = p->nDivs;
2048 Vec_IntForEachEntryDoubleStart( vRes, Start, Stop, i, 2*p->nDivs ) {
2049 for ( j = 0; j < Start; j++ )
2050 if ( p->VarMarks[n][0][j] )
2051 Exa4_ManAddClause4( p, Abc_Var2Lit( p->VarMarks[n][0][j], 1 ), 0, 0, 0 );
2052 for ( k = 0; k < 2; k++ )
2053 for ( j = Stop; j < n; j++ )
2054 if ( p->VarMarks[n][k][j] )
2055 Exa4_ManAddClause4( p, Abc_Var2Lit( p->VarMarks[n][k][j], 1 ), 0, 0, 0 );
2056 n++;
2057 }
2058 assert( n == p->nDivs + p->nNodes );
2059 Vec_IntFreeP( &vRes );
2060 }
2061 for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ )
2062 {
2063 int iVarStart = 1 + 5*(i - p->nDivs);//
2064 for ( k = 0; k < 2; k++ )
2065 {
2066 nLits = 0;
2067 for ( j = 0; j < p->nObjs; j++ )
2068 if ( p->VarMarks[i][k][j] )
2069 pLits[nLits++] = Abc_Var2Lit( p->VarMarks[i][k][j], 0 );
2070 assert( nLits > 0 );
2071 Exa4_ManAddClause( p, pLits, nLits );
2072 if ( !fCard ) {
2073 for ( n = 0; n < nLits; n++ )
2074 for ( m = n+1; m < nLits; m++ )
2075 Exa4_ManAddClause4( p, Abc_LitNot(pLits[n]), Abc_LitNot(pLits[m]), 0, 0 );
2076 }
2077 else {
2078 fprintf( p->pFile, "k %d ", nLits-1 );
2079 for ( n = 0; n < nLits; n++ )
2080 pLits[n] = Abc_LitNot(pLits[n]);
2081 Exa4_ManAddClause( p, pLits, nLits );
2082 }
2083 if ( k == 1 )
2084 break;
2085 for ( j = 0; j < p->nObjs; j++ ) if ( p->VarMarks[i][0][j] )
2086 for ( n = j; n < p->nObjs; n++ ) if ( p->VarMarks[i][1][n] )
2087 Exa4_ManAddClause4( p, Abc_Var2Lit(p->VarMarks[i][0][j], 1), Abc_Var2Lit(p->VarMarks[i][1][n], 1), 0, 0 );
2088 }
2089 if ( fOrderNodes )
2090 for ( j = p->nDivs; j < i; j++ )
2091 for ( n = 0; n < p->nObjs; n++ ) if ( p->VarMarks[i][0][n] )
2092 for ( m = n+1; m < p->nObjs; m++ ) if ( p->VarMarks[j][0][m] )
2093 Exa4_ManAddClause4( p, Abc_Var2Lit(p->VarMarks[i][0][n], 1), Abc_Var2Lit(p->VarMarks[j][0][m], 1), 0, 0 );
2094 for ( j = p->nDivs; j < i; j++ )
2095 for ( k = 0; k < 2; k++ ) if ( p->VarMarks[i][k][j] )
2096 for ( n = 0; n < p->nObjs; n++ ) if ( p->VarMarks[i][!k][n] )
2097 for ( m = 0; m < 2; m++ ) if ( p->VarMarks[j][m][n] )
2098 Exa4_ManAddClause4( p, Abc_Var2Lit(p->VarMarks[i][k][j], 1), Abc_Var2Lit(p->VarMarks[i][!k][n], 1), Abc_Var2Lit(p->VarMarks[j][m][n], 1), 0 );
2099 if ( fFancy )
2100 {
2101 nLits = 0;
2102 for ( k = 0; k < 5-fOnlyAnd; k++ )
2103 pLits[nLits++] = Abc_Var2Lit( iVarStart+k, 0 );
2104 Exa4_ManAddClause( p, pLits, nLits );
2105 for ( n = 0; n < nLits; n++ )
2106 for ( m = n+1; m < nLits; m++ )
2107 Exa4_ManAddClause4( p, Abc_LitNot(pLits[n]), Abc_LitNot(pLits[m]), 0, 0 );
2108 }
2109 else
2110 {
2111 for ( k = 0; k < 3; k++ )
2112 Exa4_ManAddClause4( p, Abc_Var2Lit(iVarStart, k==1), Abc_Var2Lit(iVarStart+1, k==2), Abc_Var2Lit(iVarStart+2, k!=0), 0);
2113 if ( fOnlyAnd )
2114 Exa4_ManAddClause4( p, Abc_Var2Lit(iVarStart, 1), Abc_Var2Lit(iVarStart+1, 1), Abc_Var2Lit(iVarStart+2, 0), 0);
2115 }
2116 }
2117 for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ )
2118 {
2119 nLits = 0;
2120 for ( k = 0; k < 2; k++ )
2121 for ( j = i+1; j < p->nObjs; j++ )
2122 if ( p->VarMarks[j][k][i] )
2123 pLits[nLits++] = Abc_Var2Lit( p->VarMarks[j][k][i], 0 );
2124 Exa4_ManAddClause( p, pLits, nLits );
2125 if ( fUniqFans )
2126 for ( n = 0; n < nLits; n++ )
2127 for ( m = n+1; m < nLits; m++ )
2128 Exa4_ManAddClause4( p, Abc_LitNot(pLits[n]), Abc_LitNot(pLits[m]), 0, 0 );
2129 }
2130 for ( i = p->nDivs + p->nNodes; i < p->nObjs; i++ )
2131 {
2132 nLits = 0;
2133 for ( j = 0; j < p->nDivs + p->nNodes; j++ ) if ( p->VarMarks[i][0][j] )
2134 pLits[nLits++] = Abc_Var2Lit( p->VarMarks[i][0][j], 0 );
2135 Exa4_ManAddClause( p, pLits, nLits );
2136 for ( n = 0; n < nLits; n++ )
2137 for ( m = n+1; m < nLits; m++ )
2138 Exa4_ManAddClause4( p, Abc_LitNot(pLits[n]), Abc_LitNot(pLits[m]), 0, 0 );
2139 }
2140 return 1;
2141}
Gia_ManKSatGenLevels
Vec_Int_t * Gia_ManKSatGenLevels(char *pGuide, int nIns, int nNodes)
Definition giaSatLut.c:1686
Vec_IntForEachEntryDoubleStart
#define Vec_IntForEachEntryDoubleStart(vVec, Entry1, Entry2, i, Start)
Definition vecInt.h:74
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Exa4_ManGenTest()

Mini_Aig_t * Exa4_ManGenTest ( Vec_Wrd_t * vSimsIn,
Vec_Wrd_t * vSimsOut,
int nIns,
int nDivs,
int nOuts,
int nNodes,
int TimeOut,
int fOnlyAnd,
int fFancy,
int fOrderNodes,
int fUniqFans,
int fVerbose,
int fCard,
char * pGuide )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 2395 of file bmcMaj.c.

2396{
2397 extern Vec_Int_t * Gia_RunKadical( char * pFileNameIn, char * pFileNameOut, int Seed, int nBTLimit, int TimeOut, int fVerbose, int * pStatus );
2398 Mini_Aig_t * pMini = NULL;
2399 abctime clkTotal = Abc_Clock();
2400 Vec_Int_t * vValues = NULL;
2401 srand(time(NULL));
2402 int Status = 0, Rand = ((((unsigned)rand()) << 12) ^ ((unsigned)rand())) & 0xFFFFF;
2403 char pFileNameIn[32]; sprintf( pFileNameIn, "_%05x_.cnf", Rand );
2404 char pFileNameOut[32]; sprintf( pFileNameOut, "_%05x_.out", Rand );
2405 Exa4_Man_t * p = Exa4_ManAlloc( vSimsIn, vSimsOut, nIns, nDivs, nOuts, nNodes, fVerbose );
2406 Exa_ManIsNormalized( vSimsIn, vSimsOut );
2407 Exa4_ManGenCnf( p, pFileNameIn, fOnlyAnd, fFancy, fOrderNodes, fUniqFans, fCard, pGuide );
2408 if ( fVerbose )
2409 printf( "Timeout = %d. OnlyAnd = %d. Fancy = %d. OrderNodes = %d. UniqueFans = %d. Verbose = %d.\n", TimeOut, fOnlyAnd, fFancy, fOrderNodes, fUniqFans, fVerbose );
2410 if ( fVerbose )
2411 printf( "CNF with %d variables and %d clauses was dumped into file \"%s\".\n", p->nCnfVars, p->nCnfClauses, pFileNameIn );
2412 if ( fCard )
2413 vValues = Gia_RunKadical( pFileNameIn, pFileNameOut, 0, 0, TimeOut, fVerbose, &Status );
2414 else
2415 vValues = Exa4_ManSolve( pFileNameIn, pFileNameOut, TimeOut, fVerbose );
2416 if ( vValues ) pMini = Exa4_ManMiniAig( p, vValues, fFancy );
2417 //if ( vValues ) Exa4_ManPrintSolution( p, vValues, fFancy );
2418 if ( vValues ) Exa_ManMiniPrint( pMini, p->nIns );
2419 if ( vValues ) Exa_ManMiniVerify( pMini, vSimsIn, vSimsOut );
2420 Vec_IntFreeP( &vValues );
2421 Exa4_ManFree( p );
2422 unlink( pFileNameIn );
2423 Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
2424 return pMini;
2425}
Exa4_ManSolve
Vec_Int_t * Exa4_ManSolve(char *pFileNameIn, char *pFileNameOut, int TimeOut, int fVerbose)
Definition bmcMaj.c:1850
Exa4_ManMiniAig
Mini_Aig_t * Exa4_ManMiniAig(Exa4_Man_t *p, Vec_Int_t *vValues, int fFancy)
Definition bmcMaj.c:2320
Exa4_ManGenCnf
void Exa4_ManGenCnf(Exa4_Man_t *p, char *pFileName, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fCard, char *pGuide)
Definition bmcMaj.c:2221
Exa_ManMiniVerify
void Exa_ManMiniVerify(Mini_Aig_t *p, Vec_Wrd_t *vSimsIn, Vec_Wrd_t *vSimsOut)
Definition bmcMaj.c:1758
Exa4_ManFree
void Exa4_ManFree(Exa4_Man_t *p)
Definition bmcMaj.c:1991
Exa4_ManAlloc
Exa4_Man_t * Exa4_ManAlloc(Vec_Wrd_t *vSimsIn, Vec_Wrd_t *vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, int fVerbose)
Definition bmcMaj.c:1976
Exa_ManIsNormalized
void Exa_ManIsNormalized(Vec_Wrd_t *vSimsIn, Vec_Wrd_t *vSimsOut)
Definition bmcMaj.c:1702
Exa_ManMiniPrint
void Exa_ManMiniPrint(Mini_Aig_t *p, int nIns)
Definition bmcMaj.c:1726
Gia_RunKadical
Vec_Int_t * Gia_RunKadical(char *pFileNameIn, char *pFileNameOut, int Seed, int nBTLimit, int TimeOut, int fVerbose, int *pStatus)
Definition giaSatLut.c:1237
Mini_Aig_t
struct Mini_Aig_t_ Mini_Aig_t
BASIC TYPES ///.
Definition miniaig.h:48
sprintf
char * sprintf()
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Exa4_ManMarkup()

int Exa4_ManMarkup ( Exa4_Man_t * p)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1917 of file bmcMaj.c.

1918{
1919 int i, k, j, nVars[3] = {1 + 5*p->nNodes, 0, 3*p->nNodes*Vec_WrdSize(p->vSimsIn)};
1920 assert( p->nObjs <= MAJ_NOBJS );
1921 for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ )
1922 for ( k = 0; k < 2; k++ )
1923 for ( j = 1+!k; j < i-k; j++ )
1924 p->VarMarks[i][k][j] = nVars[0] + nVars[1]++;
1925 for ( i = p->nDivs + p->nNodes; i < p->nObjs; i++ )
1926 for ( j = p->nOuts == 1 ? p->nDivs + p->nNodes - 1 : 0; j < p->nDivs + p->nNodes; j++ )
1927 p->VarMarks[i][0][j] = nVars[0] + nVars[1]++;
1928 if ( p->fVerbose )
1929 printf( "Variables: Function = %d. Structure = %d. Internal = %d. Total = %d.\n",
1930 nVars[0], nVars[1], nVars[2], nVars[0] + nVars[1] + nVars[2] );
1931 if ( 0 )
1932 {
1933 for ( j = 0; j < 2; j++ )
1934 {
1935 printf( " : " );
1936 for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ )
1937 {
1938 for ( k = 0; k < 2; k++ )
1939 printf( "%3d ", j ? k : i );
1940 printf( " " );
1941 }
1942 printf( " " );
1943 for ( i = p->nDivs + p->nNodes; i < p->nObjs; i++ )
1944 {
1945 printf( "%3d ", j ? 0 : i );
1946 printf( " " );
1947 }
1948 printf( "\n" );
1949 }
1950 for ( j = 0; j < 5 + p->nNodes*9 + p->nOuts*5; j++ )
1951 printf( "-" );
1952 printf( "\n" );
1953 for ( j = p->nObjs - 2; j >= 0; j-- )
1954 {
1955 if ( j > 0 && j <= p->nIns )
1956 printf( " %c : ", 'a'+j-1 );
1957 else
1958 printf( "%2d : ", j );
1959 for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ )
1960 {
1961 for ( k = 0; k < 2; k++ )
1962 printf( "%3d ", p->VarMarks[i][k][j] );
1963 printf( " " );
1964 }
1965 printf( " " );
1966 for ( i = p->nDivs + p->nNodes; i < p->nObjs; i++ )
1967 {
1968 printf( "%3d ", p->VarMarks[i][0][j] );
1969 printf( " " );
1970 }
1971 printf( "\n" );
1972 }
1973 }
1974 return nVars[0] + nVars[1] + nVars[2];
1975}
Here is the caller graph for this function:

◆ Exa4_ManMiniAig()

Mini_Aig_t * Exa4_ManMiniAig ( Exa4_Man_t * p,
Vec_Int_t * vValues,
int fFancy )

Definition at line 2320 of file bmcMaj.c.

2321{
2322 int i, k, Compl[MAJ_NOBJS] = {0};
2323 Mini_Aig_t * pMini = Mini_AigStartSupport( p->nDivs-1, p->nObjs );
2324 for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ )
2325 {
2326 int iNodes[2] = {0};
2327 int iVarStart = 1 + 5*(i - p->nDivs);//
2328 if ( fFancy )
2329 {
2330 int Val1 = Vec_IntEntry(vValues, iVarStart);
2331 int Val2 = Vec_IntEntry(vValues, iVarStart+1);
2332 int Val3 = Vec_IntEntry(vValues, iVarStart+2);
2333 int Val4 = Vec_IntEntry(vValues, iVarStart+3);
2334 int Val5 = Vec_IntEntry(vValues, iVarStart+4);
2335 for ( k = 0; k < 2; k++ )
2336 {
2337 int iNode = Exa4_ManFindFanin( p, vValues, i, !k );
2338 int fComp = k ? Val1 | Val3 : Val2 | Val3;
2339 iNodes[k] = Abc_Var2Lit(iNode, fComp ^ Compl[iNode]);
2340 }
2341 if ( Val1 || Val2 || Val3 )
2342 Mini_AigAnd( pMini, iNodes[0], iNodes[1] );
2343 else
2344 {
2345 if ( Val4 )
2346 Mini_AigOr( pMini, iNodes[0], iNodes[1] );
2347 else if ( Val5 )
2348 Mini_AigXorSpecial( pMini, iNodes[0], iNodes[1] );
2349 else assert( 0 );
2350 }
2351 }
2352 else
2353 {
2354 int Val1 = Vec_IntEntry(vValues, iVarStart);
2355 int Val2 = Vec_IntEntry(vValues, iVarStart+1);
2356 int Val3 = Vec_IntEntry(vValues, iVarStart+2);
2357 Compl[i] = Val1 && Val2 && Val3;
2358 for ( k = 0; k < 2; k++ )
2359 {
2360 int iNode = Exa4_ManFindFanin( p, vValues, i, !k );
2361 int fComp = k ? !Val1 && Val2 && !Val3 : Val1 && !Val2 && !Val3;
2362 iNodes[k] = Abc_Var2Lit(iNode, fComp ^ Compl[iNode]);
2363 }
2364 if ( Val1 && Val2 )
2365 {
2366 if ( Val3 )
2367 Mini_AigOr( pMini, iNodes[0], iNodes[1] );
2368 else
2369 Mini_AigXorSpecial( pMini, iNodes[0], iNodes[1] );
2370 }
2371 else
2372 Mini_AigAnd( pMini, iNodes[0], iNodes[1] );
2373 }
2374 }
2375 for ( i = p->nDivs + p->nNodes; i < p->nObjs; i++ )
2376 {
2377 int iVar = Exa4_ManFindFanin( p, vValues, i, 0 );
2378 Mini_AigCreatePo( pMini, Abc_Var2Lit(iVar, Compl[iVar]) );
2379 }
2380 assert( p->nObjs == Mini_AigNodeNum(pMini) );
2381 return pMini;
2382}
Here is the caller graph for this function:

◆ Exa4_ManParse()

Vec_Int_t * Exa4_ManParse ( char * pFileName)

DECLARATIONS ///.

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1812 of file bmcMaj.c.

1813{
1814 Vec_Int_t * vRes = NULL;
1815 char * pToken, pBuffer[1000];
1816 FILE * pFile = fopen( pFileName, "rb" );
1817 if ( pFile == NULL )
1818 {
1819 Abc_Print( -1, "Cannot open file \"%s\".\n", pFileName );
1820 return NULL;
1821 }
1822 while ( fgets( pBuffer, 1000, pFile ) != NULL )
1823 {
1824 if ( pBuffer[0] == 's' )
1825 {
1826 if ( strncmp(pBuffer+2, "SAT", 3) )
1827 break;
1828 assert( vRes == NULL );
1829 vRes = Vec_IntAlloc( 100 );
1830 }
1831 else if ( pBuffer[0] == 'v' )
1832 {
1833 pToken = strtok( pBuffer+1, " \n\r\t" );
1834 while ( pToken )
1835 {
1836 int Token = atoi(pToken);
1837 if ( Token == 0 )
1838 break;
1839 Vec_IntSetEntryFull( vRes, Abc_AbsInt(Token), Token > 0 );
1840 pToken = strtok( NULL, " \n\r\t" );
1841 }
1842 }
1843 else if ( pBuffer[0] != 'c' )
1844 assert( 0 );
1845 }
1846 fclose( pFile );
1847 unlink( pFileName );
1848 return vRes;
1849}
strncmp
int strncmp()
strtok
char * strtok()
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Exa4_ManPrintSolution()

void Exa4_ManPrintSolution ( Exa4_Man_t * p,
Vec_Int_t * vValues,
int fFancy )

Definition at line 2271 of file bmcMaj.c.

2272{
2273 int i, k;
2274 printf( "Circuit for %d-var function with %d divisors contains %d two-input gates:\n", p->nIns, p->nDivs, p->nNodes );
2275 for ( i = p->nDivs + p->nNodes; i < p->nObjs; i++ )
2276 {
2277 int iVar = Exa4_ManFindFanin( p, vValues, i, 0 );
2278 printf( "%2d = ", i );
2279 Exa4_ManPrintFanin( p, iVar, 0 );
2280 printf( "\n" );
2281 }
2282 for ( i = p->nDivs + p->nNodes - 1; i >= p->nDivs; i-- )
2283 {
2284 int iVarStart = 1 + 5*(i - p->nDivs);//
2285 if ( fFancy )
2286 {
2287 int Val1 = Vec_IntEntry(vValues, iVarStart);
2288 int Val2 = Vec_IntEntry(vValues, iVarStart+1);
2289 int Val3 = Vec_IntEntry(vValues, iVarStart+2);
2290 int Val4 = Vec_IntEntry(vValues, iVarStart+3);
2291 //int Val5 = Vec_IntEntry(vValues, iVarStart+4);
2292 printf( "%2d = ", i );
2293 for ( k = 0; k < 2; k++ )
2294 {
2295 int iNode = Exa4_ManFindFanin( p, vValues, i, !k );
2296 int fComp = k ? Val1 | Val3 : Val2 | Val3;
2297 Exa4_ManPrintFanin( p, iNode, fComp );
2298 if ( k ) break;
2299 printf( " %c", (Val1 || Val2 || Val3) ? '&' : (Val4 ? '|' : '^') );
2300 }
2301 }
2302 else
2303 {
2304 int Val1 = Vec_IntEntry(vValues, iVarStart);
2305 int Val2 = Vec_IntEntry(vValues, iVarStart+1);
2306 int Val3 = Vec_IntEntry(vValues, iVarStart+2);
2307 printf( "%2d = ", i );
2308 for ( k = 0; k < 2; k++ )
2309 {
2310 int iNode = Exa4_ManFindFanin( p, vValues, i, !k );
2311 int fComp = k ? !Val1 && Val2 && !Val3 : Val1 && !Val2 && !Val3;
2312 Exa4_ManPrintFanin( p, iNode, fComp );
2313 if ( k ) break;
2314 printf( " %c", (Val1 && Val2) ? (Val3 ? '|' : '^') : '&' );
2315 }
2316 }
2317 printf( "\n" );
2318 }
2319}

◆ Exa4_ManSolve()

Vec_Int_t * Exa4_ManSolve ( char * pFileNameIn,
char * pFileNameOut,
int TimeOut,
int fVerbose )

Definition at line 1850 of file bmcMaj.c.

1851{
1852 int fVerboseSolver = 0;
1853 abctime clkTotal = Abc_Clock();
1854 Vec_Int_t * vRes = NULL;
1855#ifdef _WIN32
1856 char * pKissat = "kissat.exe";
1857#else
1858 char * pKissat = "kissat";
1859#endif
1860 char Command[1000], * pCommand = (char *)&Command;
1861 if ( TimeOut )
1862 sprintf( pCommand, "%s --time=%d %s %s > %s", pKissat, TimeOut, fVerboseSolver ? "": "-q", pFileNameIn, pFileNameOut );
1863 else
1864 sprintf( pCommand, "%s %s %s > %s", pKissat, fVerboseSolver ? "": "-q", pFileNameIn, pFileNameOut );
1865#ifdef __wasm
1866 if ( 1 )
1867#else
1868 if ( system( pCommand ) == -1 )
1869#endif
1870 {
1871 fprintf( stdout, "Command \"%s\" did not succeed.\n", pCommand );
1872 return 0;
1873 }
1874 vRes = Exa4_ManParse( pFileNameOut );
1875 if ( fVerbose )
1876 {
1877 if ( vRes )
1878 printf( "The problem has a solution. " );
1879 else if ( vRes == NULL && TimeOut == 0 )
1880 printf( "The problem has no solution. " );
1881 else if ( vRes == NULL )
1882 printf( "The problem has no solution or timed out after %d sec. ", TimeOut );
1883 Abc_PrintTime( 1, "SAT solver time", Abc_Clock() - clkTotal );
1884 }
1885 return vRes;
1886}
Exa4_ManParse
Vec_Int_t * Exa4_ManParse(char *pFileName)
DECLARATIONS ///.
Definition bmcMaj.c:1812
system
int system()
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Exa5_ManAlloc()

Exa5_Man_t * Exa5_ManAlloc ( Vec_Wrd_t * vSimsIn,
Vec_Wrd_t * vSimsOut,
int nIns,
int nDivs,
int nOuts,
int nNodes,
int fVerbose )

Definition at line 2568 of file bmcMaj.c.

2569{
2570 Exa5_Man_t * p = ABC_CALLOC( Exa5_Man_t, 1 );
2571 assert( Vec_WrdSize(vSimsIn) == Vec_WrdSize(vSimsOut) );
2572 p->vSimsIn = vSimsIn;
2573 p->vSimsOut = vSimsOut;
2574 p->fVerbose = fVerbose;
2575 p->nIns = nIns;
2576 p->nDivs = nDivs;
2577 p->nNodes = nNodes;
2578 p->nOuts = nOuts;
2579 p->nObjs = p->nDivs + p->nNodes + p->nOuts;
2580 p->vFans = Vec_IntAlloc( 5000 );
2581 p->nCnfVars = Exa5_ManMarkup( p );
2582 return p;
2583}
Exa5_ManMarkup
int Exa5_ManMarkup(Exa5_Man_t *p)
Definition bmcMaj.c:2505
Exa5_Man_t
struct Exa5_Man_t_ Exa5_Man_t
Definition bmcMaj.c:2475
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Exa5_ManFree()

void Exa5_ManFree ( Exa5_Man_t * p)

Definition at line 2584 of file bmcMaj.c.

2585{
2586 Vec_IntFree( p->vFans );
2587 ABC_FREE( p );
2588}
Here is the caller graph for this function:

◆ Exa5_ManGenCnf()

void Exa5_ManGenCnf ( Exa5_Man_t * p,
char * pFileName,
int fOnlyAnd,
int fFancy,
int fOrderNodes,
int fUniqFans )

Definition at line 2767 of file bmcMaj.c.

2768{
2769 int m;
2770 assert( p->pFile == NULL );
2771 p->pFile = fopen( pFileName, "wb" );
2772 fputs( "p cnf \n", p->pFile );
2773 Exa5_ManGenStart( p, fOnlyAnd, fFancy, fOrderNodes, fUniqFans );
2774 for ( m = 1; m < Vec_WrdSize(p->vSimsIn); m++ )
2775 Exa5_ManGenMint( p, m, fOnlyAnd, fFancy );
2776 rewind( p->pFile );
2777 fprintf( p->pFile, "p cnf %d %d", p->nCnfVars, p->nCnfClauses );
2778 fclose( p->pFile );
2779}
Exa5_ManGenStart
int Exa5_ManGenStart(Exa5_Man_t *p, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans)
Definition bmcMaj.c:2654
Exa5_ManGenMint
void Exa5_ManGenMint(Exa5_Man_t *p, int iMint, int fOnlyAnd, int fFancy)
Definition bmcMaj.c:2729
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Exa5_ManGenMint()

void Exa5_ManGenMint ( Exa5_Man_t * p,
int iMint,
int fOnlyAnd,
int fFancy )

Definition at line 2729 of file bmcMaj.c.

2730{
2731 int iNodeVar = p->nCnfVars + p->nNodes*(iMint - Vec_WrdSize(p->vSimsIn));
2732 int iOutMint = Abc_Tt6FirstBit( Vec_WrdEntry(p->vSimsOut, iMint) );
2733 int i, k, n, j, VarVals[MAJ_NOBJS], iNodes[3], iVarStart, iObj;
2734 assert( p->nObjs <= MAJ_NOBJS );
2735 assert( iMint < Vec_WrdSize(p->vSimsIn) );
2736 for ( i = 0; i < p->nDivs; i++ )
2737 VarVals[i] = (Vec_WrdEntry(p->vSimsIn, iMint) >> i) & 1;
2738 for ( i = 0; i < p->nNodes; i++ )
2739 VarVals[p->nDivs + i] = Abc_Var2Lit(iNodeVar + i, 0);
2740 for ( i = 0; i < p->nOuts; i++ )
2741 VarVals[p->nDivs + p->nNodes + i] = (iOutMint >> i) & 1;
2742 if ( 0 )
2743 {
2744 printf( "Adding minterm %d: ", iMint );
2745 for ( i = 0; i < p->nObjs; i++ )
2746 printf( " %d=%d", i, VarVals[i] );
2747 printf( "\n" );
2748 }
2749 Vec_IntForEachEntry( p->vFans, iObj, i )
2750 {
2751 if ( iObj == 0 ) continue;
2752 iNodes[1] = (iObj >> 0) & 0xFF;
2753 iNodes[0] = (iObj >> 8) & 0xFF;
2754 iNodes[2] = (iObj >> 16) & 0xFF;
2755 iVarStart = 1 + 3*(iNodes[2] - p->nDivs);//
2756 for ( k = 0; k < 4; k++ )
2757 for ( n = 0; n < 2; n++ )
2758 Exa5_ManAddClause4( p, Abc_Var2Lit(i, 1), Abc_LitNotCond(VarVals[iNodes[0]], k&1), Abc_LitNotCond(VarVals[iNodes[1]], k>>1), Abc_LitNotCond(VarVals[iNodes[2]], !n), Abc_Var2Lit(k ? iVarStart + k-1 : 0, n));
2759 }
2760 for ( i = p->nDivs + p->nNodes; i < p->nObjs; i++ )
2761 {
2762 for ( j = 0; j < p->nDivs + p->nNodes; j++ ) if ( p->VarMarks[i][j] )
2763 for ( n = 0; n < 2; n++ )
2764 Exa5_ManAddClause4( p, Abc_Var2Lit(p->VarMarks[i][j], 1), Abc_LitNotCond(VarVals[j], n), Abc_LitNotCond(VarVals[i], !n), 0, 0);
2765 }
2766}
Here is the caller graph for this function:

◆ Exa5_ManGenStart()

int Exa5_ManGenStart ( Exa5_Man_t * p,
int fOnlyAnd,
int fFancy,
int fOrderNodes,
int fUniqFans )

Definition at line 2654 of file bmcMaj.c.

2655{
2656 Vec_Int_t * vArray = Vec_IntAlloc( 100 );
2657 int pLits[MAJ_NOBJS], i, j, k, n, m, nLits, iObj;
2658 for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ )
2659 {
2660 int iVarStart = 1 + 3*(i - p->nDivs);//
2661 nLits = 0;
2662 for ( j = 0; j < i; j++ ) if ( p->VarMarks[i][j] )
2663 Exa5_ManAddGroup( p, p->VarMarks[i][j], j-1 ), pLits[nLits++] = Abc_Var2Lit(p->VarMarks[i][j], 0);
2664 Exa5_ManAddClause( p, pLits, nLits );
2665 Exa5_ManAddOneHot( p, pLits, nLits );
2666 if ( fOrderNodes )
2667 for ( j = p->nDivs; j < i; j++ )
2668 for ( n = 0; n < p->nObjs; n++ ) if ( p->VarMarks[i][n] )
2669 for ( m = n+1; m < p->nObjs; m++ ) if ( p->VarMarks[j][m] )
2670 Exa5_ManAddClause4( p, Abc_Var2Lit(p->VarMarks[i][n], 1), Abc_Var2Lit(p->VarMarks[j][m], 1), 0, 0, 0 );
2671 for ( j = p->nDivs; j < i; j++ ) if ( p->VarMarks[i][j] )
2672 {
2673 // go through all variables of i that point to j and k
2674 for ( n = 1; n < j; n++ )
2675 {
2676 int iVar = p->VarMarks[i][j] + n; // variable of i pointing to j
2677 int iObj = Vec_IntEntry( p->vFans, iVar );
2678 int iNode0 = (iObj >> 0) & 0xFF;
2679 int iNode1 = (iObj >> 8) & 0xFF;
2680 int iNode2 = (iObj >> 16) & 0xFF;
2681 assert( iObj > 0 );
2682 assert( iNode1 == j );
2683 assert( iNode2 == i );
2684 // go through all variables of j and block those that point to k
2685 assert( p->VarMarks[j][2] > 0 );
2686 assert( p->VarMarks[j+1][2] > 0 );
2687 for ( m = p->VarMarks[j][2]+1; m < p->VarMarks[j+1][2]; m++ )
2688 {
2689 int jObj = Vec_IntEntry( p->vFans, m );
2690 int jNode0 = (jObj >> 0) & 0xFF;
2691 int jNode1 = (jObj >> 8) & 0xFF;
2692 int jNode2 = (jObj >> 16) & 0xFF;
2693 if ( jObj == 0 )
2694 continue;
2695 assert( jNode2 == j );
2696 if ( iNode0 == jNode0 || iNode0 == jNode1 )
2697 Exa5_ManAddClause4( p, Abc_Var2Lit(iVar, 1), Abc_Var2Lit(m, 1), 0, 0, 0 );
2698 }
2699 }
2700 }
2701 for ( k = 0; k < 3; k++ )
2702 Exa5_ManAddClause4( p, Abc_Var2Lit(iVarStart, k==1), Abc_Var2Lit(iVarStart+1, k==2), Abc_Var2Lit(iVarStart+2, k!=0), 0, 0);
2703 if ( fOnlyAnd )
2704 Exa5_ManAddClause4( p, Abc_Var2Lit(iVarStart, 1), Abc_Var2Lit(iVarStart+1, 1), Abc_Var2Lit(iVarStart+2, 0), 0, 0);
2705 }
2706 for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ )
2707 {
2708 Vec_IntClear( vArray );
2709 Vec_IntForEachEntry( p->vFans, iObj, k )
2710 if ( iObj && ((iObj & 0xFF) == i || ((iObj >> 8) & 0xFF) == i) )
2711 Vec_IntPush( vArray, Abc_Var2Lit(k, 0) );
2712 for ( k = p->nDivs + p->nNodes; k < p->nObjs; k++ ) if ( p->VarMarks[k][i] )
2713 Vec_IntPush( vArray, Abc_Var2Lit(p->VarMarks[k][i], 0) );
2714 Exa5_ManAddClause( p, Vec_IntArray(vArray), Vec_IntSize(vArray) );
2715 if ( fUniqFans )
2716 Exa5_ManAddOneHot( p, Vec_IntArray(vArray), Vec_IntSize(vArray) );
2717 }
2718 Vec_IntFree( vArray );
2719 for ( i = p->nDivs + p->nNodes; i < p->nObjs; i++ )
2720 {
2721 nLits = 0;
2722 for ( j = 0; j < p->nDivs + p->nNodes; j++ ) if ( p->VarMarks[i][j] )
2723 pLits[nLits++] = Abc_Var2Lit( p->VarMarks[i][j], 0 );
2724 Exa5_ManAddClause( p, pLits, nLits );
2725 Exa5_ManAddOneHot( p, pLits, nLits );
2726 }
2727 return 1;
2728}
Here is the caller graph for this function:

◆ Exa5_ManGenTest()

Mini_Aig_t * Exa5_ManGenTest ( Vec_Wrd_t * vSimsIn,
Vec_Wrd_t * vSimsOut,
int nIns,
int nDivs,
int nOuts,
int nNodes,
int TimeOut,
int fOnlyAnd,
int fFancy,
int fOrderNodes,
int fUniqFans,
int fVerbose )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 2926 of file bmcMaj.c.

2927{
2928 abctime clkTotal = Abc_Clock();
2929 Mini_Aig_t * pMini = NULL;
2930 Vec_Int_t * vValues = NULL;
2931 srand(time(NULL));
2932 int Rand = ((((unsigned)rand()) << 12) ^ ((unsigned)rand())) & 0xFFFFF;
2933 char pFileNameIn[32]; sprintf( pFileNameIn, "_%05x_.cnf", Rand );
2934 char pFileNameOut[32]; sprintf( pFileNameOut, "_%05x_.out", Rand );
2935 Exa5_Man_t * p = Exa5_ManAlloc( vSimsIn, vSimsOut, nIns, nDivs, nOuts, nNodes, fVerbose );
2936 Exa_ManIsNormalized( vSimsIn, vSimsOut );
2937 Exa5_ManGenCnf( p, pFileNameIn, fOnlyAnd, fFancy, fOrderNodes, fUniqFans );
2938 if ( fVerbose )
2939 printf( "Timeout = %d. OnlyAnd = %d. Fancy = %d. OrderNodes = %d. UniqueFans = %d. Verbose = %d.\n", TimeOut, fOnlyAnd, fFancy, fOrderNodes, fUniqFans, fVerbose );
2940 if ( fVerbose )
2941 printf( "CNF with %d variables and %d clauses was dumped into file \"%s\".\n", p->nCnfVars, p->nCnfClauses, pFileNameIn );
2942 vValues = Exa4_ManSolve( pFileNameIn, pFileNameOut, TimeOut, fVerbose );
2943 if ( vValues ) pMini = Exa5_ManMiniAig( p, vValues );
2944 //if ( vValues ) Exa5_ManPrintSolution( p, vValues, fFancy );
2945 if ( vValues ) Exa_ManMiniPrint( pMini, p->nIns );
2946 if ( vValues ) Exa_ManMiniVerify( pMini, vSimsIn, vSimsOut );
2947 Vec_IntFreeP( &vValues );
2948 Exa5_ManFree( p );
2949 unlink( pFileNameIn );
2950 Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
2951 return pMini;
2952}
Exa5_ManAlloc
Exa5_Man_t * Exa5_ManAlloc(Vec_Wrd_t *vSimsIn, Vec_Wrd_t *vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, int fVerbose)
Definition bmcMaj.c:2568
Exa5_ManFree
void Exa5_ManFree(Exa5_Man_t *p)
Definition bmcMaj.c:2584
Exa5_ManGenCnf
void Exa5_ManGenCnf(Exa5_Man_t *p, char *pFileName, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans)
Definition bmcMaj.c:2767
Exa5_ManMiniAig
Mini_Aig_t * Exa5_ManMiniAig(Exa5_Man_t *p, Vec_Int_t *vValues)
Definition bmcMaj.c:2860
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Exa5_ManMarkup()

int Exa5_ManMarkup ( Exa5_Man_t * p)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 2505 of file bmcMaj.c.

2506{
2507 int i, j, k, nVars[3] = {1 + 3*p->nNodes, 0, p->nNodes*Vec_WrdSize(p->vSimsIn)};
2508 assert( p->nObjs <= MAJ_NOBJS );
2509 Vec_IntFill( p->vFans, 1 + 3*p->nNodes, 0 );
2510 for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ )
2511 for ( j = 2; j < i; j++ )
2512 {
2513 p->VarMarks[i][j] = nVars[0] + nVars[1];
2514 Vec_IntPush( p->vFans, 0 );
2515 for ( k = 1; k < j; k++ )
2516 Vec_IntPush( p->vFans, (i << 16) | (j << 8) | k );
2517 nVars[1] += j;
2518 }
2519 assert( Vec_IntSize(p->vFans) == nVars[0] + nVars[1] );
2520 for ( i = p->nDivs + p->nNodes; i < p->nObjs; i++ )
2521 for ( j = p->nOuts == 1 ? p->nDivs + p->nNodes - 1 : 0; j < p->nDivs + p->nNodes; j++ )
2522 p->VarMarks[i][j] = nVars[0] + nVars[1]++;
2523 if ( p->fVerbose )
2524 printf( "Variables: Function = %d. Structure = %d. Internal = %d. Total = %d.\n",
2525 nVars[0], nVars[1], nVars[2], nVars[0] + nVars[1] + nVars[2] );
2526 if ( 0 )
2527 {
2528 {
2529 printf( " : " );
2530 for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ )
2531 {
2532 printf( "%3d ", i );
2533 printf( " " );
2534 }
2535 printf( " " );
2536 for ( i = p->nDivs + p->nNodes; i < p->nObjs; i++ )
2537 {
2538 printf( "%3d ", i );
2539 printf( " " );
2540 }
2541 printf( "\n" );
2542 }
2543 for ( j = 0; j < 5 + p->nNodes*5 + p->nOuts*5; j++ )
2544 printf( "-" );
2545 printf( "\n" );
2546 for ( j = p->nObjs - 2; j >= 0; j-- )
2547 {
2548 if ( j > 0 && j <= p->nIns )
2549 printf( " %c : ", 'a'+j-1 );
2550 else
2551 printf( "%2d : ", j );
2552 for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ )
2553 {
2554 printf( "%3d ", p->VarMarks[i][j] );
2555 printf( " " );
2556 }
2557 printf( " " );
2558 for ( i = p->nDivs + p->nNodes; i < p->nObjs; i++ )
2559 {
2560 printf( "%3d ", p->VarMarks[i][j] );
2561 printf( " " );
2562 }
2563 printf( "\n" );
2564 }
2565 }
2566 return nVars[0] + nVars[1] + nVars[2];
2567}
Here is the caller graph for this function:

◆ Exa5_ManMiniAig()

Mini_Aig_t * Exa5_ManMiniAig ( Exa5_Man_t * p,
Vec_Int_t * vValues )

Definition at line 2860 of file bmcMaj.c.

2861{
2862 Mini_Aig_t * pMini = Mini_AigStartSupport( p->nDivs-1, p->nObjs );
2863 int Compl[MAJ_NOBJS] = {0};
2864 int Fan0[MAJ_NOBJS] = {0};
2865 int Fan1[MAJ_NOBJS] = {0};
2866 int Count[MAJ_NOBJS] = {0};
2867 int i, k, iObj, iNodes[3];
2868 Vec_IntForEachEntry( p->vFans, iObj, i )
2869 {
2870 if ( iObj == 0 || Vec_IntEntry(vValues, i) == 0 )
2871 continue;
2872 iNodes[0] = (iObj >> 0) & 0xFF;
2873 iNodes[1] = (iObj >> 8) & 0xFF;
2874 iNodes[2] = (iObj >> 16) & 0xFF;
2875 assert( p->nDivs <= iNodes[2] && iNodes[2] < p->nDivs + p->nNodes );
2876 Fan0[iNodes[2]] = iNodes[0];
2877 Fan1[iNodes[2]] = iNodes[1];
2878 Count[iNodes[2]]++;
2879 }
2880 assert( p->nDivs == Mini_AigNodeNum(pMini) );
2881 for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ )
2882 {
2883 int iNodes[2] = {0};
2884 int iVarStart = 1 + 3*(i - p->nDivs);//
2885 int Val1 = Vec_IntEntry(vValues, iVarStart);
2886 int Val2 = Vec_IntEntry(vValues, iVarStart+1);
2887 int Val3 = Vec_IntEntry(vValues, iVarStart+2);
2888 assert( Count[i] == 1 );
2889 Compl[i] = Val1 && Val2 && Val3;
2890 for ( k = 0; k < 2; k++ )
2891 {
2892 int iNode = k ? Fan1[i] : Fan0[i];
2893 int fComp = k ? !Val1 && Val2 && !Val3 : Val1 && !Val2 && !Val3;
2894 iNodes[k] = Abc_Var2Lit(iNode, fComp ^ Compl[iNode]);
2895 }
2896 if ( Val1 && Val2 )
2897 {
2898 if ( Val3 )
2899 Mini_AigOr( pMini, iNodes[0], iNodes[1] );
2900 else
2901 Mini_AigXorSpecial( pMini, iNodes[0], iNodes[1] );
2902 }
2903 else
2904 Mini_AigAnd( pMini, iNodes[0], iNodes[1] );
2905 }
2906 for ( i = p->nDivs + p->nNodes; i < p->nObjs; i++ )
2907 {
2908 int iVar = Exa5_ManFindFanin( p, vValues, i );
2909 Mini_AigCreatePo( pMini, Abc_Var2Lit(iVar, Compl[iVar]) );
2910 }
2911 assert( p->nObjs == Mini_AigNodeNum(pMini) );
2912 return pMini;
2913}
Here is the caller graph for this function:

◆ Exa5_ManPrintSolution()

void Exa5_ManPrintSolution ( Exa5_Man_t * p,
Vec_Int_t * vValues,
int fFancy )

Definition at line 2815 of file bmcMaj.c.

2816{
2817 int Fan0[MAJ_NOBJS] = {0};
2818 int Fan1[MAJ_NOBJS] = {0};
2819 int Count[MAJ_NOBJS] = {0};
2820 int i, k, iObj, iNodes[3];
2821 printf( "Circuit for %d-var function with %d divisors contains %d two-input gates:\n", p->nIns, p->nDivs, p->nNodes );
2822 Vec_IntForEachEntry( p->vFans, iObj, i )
2823 {
2824 if ( iObj == 0 || Vec_IntEntry(vValues, i) == 0 )
2825 continue;
2826 iNodes[0] = (iObj >> 0) & 0xFF;
2827 iNodes[1] = (iObj >> 8) & 0xFF;
2828 iNodes[2] = (iObj >> 16) & 0xFF;
2829 assert( p->nDivs <= iNodes[2] && iNodes[2] < p->nDivs + p->nNodes );
2830 Fan0[iNodes[2]] = iNodes[0];
2831 Fan1[iNodes[2]] = iNodes[1];
2832 Count[iNodes[2]]++;
2833 }
2834 for ( i = p->nDivs + p->nNodes; i < p->nObjs; i++ )
2835 {
2836 int iVar = Exa5_ManFindFanin( p, vValues, i );
2837 printf( "%2d = ", i );
2838 Exa5_ManPrintFanin( p, iVar, 0 );
2839 printf( "\n" );
2840 }
2841 for ( i = p->nDivs + p->nNodes - 1; i >= p->nDivs; i-- )
2842 {
2843 int iVarStart = 1 + 3*(i - p->nDivs);//
2844 int Val1 = Vec_IntEntry(vValues, iVarStart);
2845 int Val2 = Vec_IntEntry(vValues, iVarStart+1);
2846 int Val3 = Vec_IntEntry(vValues, iVarStart+2);
2847 assert( Count[i] == 1 );
2848 printf( "%2d = ", i );
2849 for ( k = 0; k < 2; k++ )
2850 {
2851 int iNode = k ? Fan1[i] : Fan0[i];
2852 int fComp = k ? !Val1 && Val2 && !Val3 : Val1 && !Val2 && !Val3;
2853 Exa5_ManPrintFanin( p, iNode, fComp );
2854 if ( k ) break;
2855 printf( " %c", (Val1 && Val2) ? (Val3 ? '|' : '^') : '&' );
2856 }
2857 printf( "\n" );
2858 }
2859}

◆ Exa6_GenCount()

void Exa6_GenCount ( word * pTruths,
int nVars )

Definition at line 3279 of file bmcMaj.c.

3280{
3281 int i, k;
3282 assert( nVars >= 3 && nVars <= 7 );
3283 for ( k = 0; k < 3; k++ )
3284 pTruths[k] = 0;
3285 for ( i = 0; i < (1 << nVars); i++ )
3286 {
3287 int n = Abc_TtCountOnes( (word)i );
3288 for ( k = 0; k < 3; k++ )
3289 if ( (n >> k) & 1 )
3290 Abc_TtSetBit( pTruths+k, i );
3291 }
3292}

◆ Exa6_GenProd()

void Exa6_GenProd ( word * pTruths,
int nVars )

Definition at line 3293 of file bmcMaj.c.

3294{
3295 int i, j, k;
3296 nVars /= 2;
3297 assert( nVars >= 2 && nVars <= 3 );
3298 for ( k = 0; k < 2*nVars; k++ )
3299 pTruths[k] = 0;
3300 for ( i = 0; i < (1 << nVars); i++ )
3301 for ( j = 0; j < (1 << nVars); j++ )
3302 {
3303 int n = i * j;
3304 for ( k = 0; k < 2*nVars; k++ )
3305 if ( (n >> k) & 1 )
3306 Abc_TtSetBit( pTruths+k, (i << nVars) | j );
3307 }
3308}
Here is the caller graph for this function:

◆ Exa6_ManAlloc()

Exa6_Man_t * Exa6_ManAlloc ( Vec_Wrd_t * vSimsIn,
Vec_Wrd_t * vSimsOut,
int nIns,
int nDivs,
int nOuts,
int nNodes,
int fVerbose )

Definition at line 3510 of file bmcMaj.c.

3511{
3512 Exa6_Man_t * p = ABC_CALLOC( Exa6_Man_t, 1 );
3513 assert( Vec_WrdSize(vSimsIn) == Vec_WrdSize(vSimsOut) );
3514 p->vSimsIn = vSimsIn;
3515 p->vSimsOut = vSimsOut;
3516 p->fVerbose = fVerbose;
3517 p->nIns = nIns;
3518 p->nDivs = nDivs;
3519 p->nNodes = nNodes;
3520 p->nOuts = nOuts;
3521 p->nObjs = p->nDivs + p->nNodes + p->nOuts;
3522 p->nCnfVars = Exa6_ManMarkup( p );
3523 p->nCnfVars2 = 0;
3524 assert( p->nObjs < 64 );
3525 return p;
3526}
Exa6_Man_t
struct Exa6_Man_t_ Exa6_Man_t
Definition bmcMaj.c:3420
Exa6_ManMarkup
int Exa6_ManMarkup(Exa6_Man_t *p)
Definition bmcMaj.c:3449
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Exa6_ManFindPolar()

int Exa6_ManFindPolar ( word First,
int nOuts )

Definition at line 3911 of file bmcMaj.c.

3912{
3913 int i;
3914 for ( i = 0; i < (1 << nOuts); i++ )
3915 if ( Exa6_ManPolarMinterm(First, nOuts, i) & 1 )
3916 return i;
3917 return -1;
3918}
Exa6_ManPolarMinterm
word Exa6_ManPolarMinterm(word Mint, int nOuts, int Polar)
Definition bmcMaj.c:3902
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Exa6_ManFree()

void Exa6_ManFree ( Exa6_Man_t * p)

Definition at line 3527 of file bmcMaj.c.

3528{
3529 ABC_FREE( p );
3530}
Here is the caller graph for this function:

◆ Exa6_ManGenCnf()

void Exa6_ManGenCnf ( Exa6_Man_t * p,
char * pFileName,
int fOnlyAnd,
int fFancy,
int fOrderNodes,
int fUniqFans )

Definition at line 3724 of file bmcMaj.c.

3725{
3726 int m;
3727 assert( p->pFile == NULL );
3728 p->pFile = fopen( pFileName, "wb" );
3729 fputs( "p cnf \n", p->pFile );
3730 Exa6_ManGenStart( p, fOnlyAnd, fFancy, fOrderNodes, fUniqFans );
3731 for ( m = 1; m < Vec_WrdSize(p->vSimsIn); m++ )
3732 Exa6_ManGenMint( p, m, fOnlyAnd, fFancy );
3733 rewind( p->pFile );
3734 fprintf( p->pFile, "p cnf %d %d", p->nCnfVars + p->nCnfVars2, p->nCnfClauses );
3735 fclose( p->pFile );
3736}
Exa6_ManGenStart
int Exa6_ManGenStart(Exa6_Man_t *p, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans)
Definition bmcMaj.c:3577
Exa6_ManGenMint
void Exa6_ManGenMint(Exa6_Man_t *p, int iMint, int fOnlyAnd, int fFancy)
Definition bmcMaj.c:3653
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Exa6_ManGenMint()

void Exa6_ManGenMint ( Exa6_Man_t * p,
int iMint,
int fOnlyAnd,
int fFancy )

Definition at line 3653 of file bmcMaj.c.

3654{
3655 int iNodeVar = p->nCnfVars + 3*p->nNodes*(iMint - Vec_WrdSize(p->vSimsIn));
3656 int iOutMint = Abc_Tt6FirstBit( Vec_WrdEntry(p->vSimsOut, iMint) );
3657 int fOnlyOne = Abc_TtSuppOnlyOne( (int)Vec_WrdEntry(p->vSimsOut, iMint) );
3658 int i, k, n, j, VarVals[MAJ_NOBJS];
3659 int fAllOnes = Abc_TtCountOnes( Vec_WrdEntry(p->vSimsOut, iMint) ) == (1 << p->nOuts);
3660 if ( fAllOnes )
3661 return;
3662 assert( p->nObjs <= MAJ_NOBJS );
3663 assert( iMint < Vec_WrdSize(p->vSimsIn) );
3664 assert( p->nOuts <= 6 );
3665 for ( i = 0; i < p->nDivs; i++ )
3666 VarVals[i] = (Vec_WrdEntry(p->vSimsIn, iMint) >> i) & 1;
3667 for ( i = 0; i < p->nNodes; i++ )
3668 VarVals[p->nDivs + i] = Abc_Var2Lit(iNodeVar + 3*i + 2, 0);
3669 if ( fOnlyOne )
3670 {
3671 for ( i = 0; i < p->nOuts; i++ )
3672 VarVals[p->nDivs + p->nNodes + i] = (iOutMint >> i) & 1;
3673 }
3674 else
3675 {
3676 word t = Abc_Tt6Stretch( Vec_WrdEntry(p->vSimsOut, iMint), p->nOuts );
3677 int i, c, nCubes = 0, pCover[100], pLits[10];
3678 int iOutVar = p->nCnfVars + p->nCnfVars2; p->nCnfVars2 += p->nOuts;
3679 for ( i = 0; i < p->nOuts; i++ )
3680 VarVals[p->nDivs + p->nNodes + i] = Abc_Var2Lit(iOutVar + i, 0);
3681 assert( t );
3682 if ( ~t )
3683 {
3684 Abc_Tt6IsopCover( ~t, ~t, p->nOuts, pCover, &nCubes );
3685 for ( c = 0; c < nCubes; c++ )
3686 {
3687 int nLits = 0;
3688 for ( i = 0; i < p->nOuts; i++ )
3689 {
3690 int iLit = (pCover[c] >> (2*i)) & 3;
3691 if ( iLit == 1 || iLit == 2 )
3692 pLits[nLits++] = Abc_Var2Lit(iOutVar + i, iLit != 1);
3693 }
3694 Exa6_ManAddClause( p, pLits, nLits );
3695 }
3696 }
3697 }
3698 if ( 0 )
3699 {
3700 printf( "Adding minterm %d: ", iMint );
3701 for ( i = 0; i < p->nObjs; i++ )
3702 printf( " %d=%d", i, VarVals[i] );
3703 printf( "\n" );
3704 }
3705 for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ )
3706 {
3707 int iVarStart = 1 + 3*(i - p->nDivs);//
3708 int iBaseVarI = iNodeVar + 3*(i - p->nDivs);
3709 for ( k = 0; k < 2; k++ )
3710 for ( j = 0; j < i; j++ ) if ( p->VarMarks[i][k][j] )
3711 for ( n = 0; n < 2; n++ )
3712 Exa6_ManAddClause4( p, Abc_Var2Lit(p->VarMarks[i][k][j], 1), Abc_Var2Lit(iBaseVarI + k, n), Abc_LitNotCond(VarVals[j], !n), 0);
3713 for ( k = 0; k < 4; k++ )
3714 for ( n = 0; n < 2; n++ )
3715 Exa6_ManAddClause4( p, Abc_Var2Lit(iBaseVarI + 0, k&1), Abc_Var2Lit(iBaseVarI + 1, k>>1), Abc_Var2Lit(iBaseVarI + 2, !n), Abc_Var2Lit(k ? iVarStart + k-1 : 0, n));
3716 }
3717 for ( i = p->nDivs + p->nNodes; i < p->nObjs; i++ )
3718 {
3719 for ( j = 0; j < p->nDivs + p->nNodes; j++ ) if ( p->VarMarks[i][0][j] )
3720 for ( n = 0; n < 2; n++ )
3721 Exa6_ManAddClause4( p, Abc_Var2Lit(p->VarMarks[i][0][j], 1), Abc_LitNotCond(VarVals[j], n), Abc_LitNotCond(VarVals[i], !n), 0);
3722 }
3723}
Here is the caller graph for this function:

◆ Exa6_ManGenStart()

int Exa6_ManGenStart ( Exa6_Man_t * p,
int fOnlyAnd,
int fFancy,
int fOrderNodes,
int fUniqFans )

Definition at line 3577 of file bmcMaj.c.

3578{
3579 int pLits[2*MAJ_NOBJS], i, j, k, n, m, nLits;
3580 for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ )
3581 {
3582 int iVarStart = 1 + 3*(i - p->nDivs);//
3583 for ( k = 0; k < 2; k++ )
3584 {
3585 nLits = 0;
3586 for ( j = 0; j < p->nObjs; j++ )
3587 if ( p->VarMarks[i][k][j] )
3588 pLits[nLits++] = Abc_Var2Lit( p->VarMarks[i][k][j], 0 );
3589 assert( nLits > 0 );
3590 Exa6_ManAddClause( p, pLits, nLits );
3591 for ( n = 0; n < nLits; n++ )
3592 for ( m = n+1; m < nLits; m++ )
3593 Exa6_ManAddClause4( p, Abc_LitNot(pLits[n]), Abc_LitNot(pLits[m]), 0, 0 );
3594 if ( k == 1 )
3595 break;
3596 for ( j = 0; j < p->nObjs; j++ ) if ( p->VarMarks[i][0][j] )
3597 for ( n = j; n < p->nObjs; n++ ) if ( p->VarMarks[i][1][n] )
3598 Exa6_ManAddClause4( p, Abc_Var2Lit(p->VarMarks[i][0][j], 1), Abc_Var2Lit(p->VarMarks[i][1][n], 1), 0, 0 );
3599 }
3600 if ( fOrderNodes )
3601 for ( j = p->nDivs; j < i; j++ )
3602 for ( n = 0; n < p->nObjs; n++ ) if ( p->VarMarks[i][0][n] )
3603 for ( m = n+1; m < p->nObjs; m++ ) if ( p->VarMarks[j][0][m] )
3604 Exa6_ManAddClause4( p, Abc_Var2Lit(p->VarMarks[i][0][n], 1), Abc_Var2Lit(p->VarMarks[j][0][m], 1), 0, 0 );
3605 for ( j = p->nDivs; j < i; j++ )
3606 for ( k = 0; k < 2; k++ ) if ( p->VarMarks[i][k][j] )
3607 for ( n = 0; n < p->nObjs; n++ ) if ( p->VarMarks[i][!k][n] )
3608 for ( m = 0; m < 2; m++ ) if ( p->VarMarks[j][m][n] )
3609 Exa6_ManAddClause4( p, Abc_Var2Lit(p->VarMarks[i][k][j], 1), Abc_Var2Lit(p->VarMarks[i][!k][n], 1), Abc_Var2Lit(p->VarMarks[j][m][n], 1), 0 );
3610 if ( fFancy )
3611 {
3612 nLits = 0;
3613 for ( k = 0; k < 5-fOnlyAnd; k++ )
3614 pLits[nLits++] = Abc_Var2Lit( iVarStart+k, 0 );
3615 Exa6_ManAddClause( p, pLits, nLits );
3616 for ( n = 0; n < nLits; n++ )
3617 for ( m = n+1; m < nLits; m++ )
3618 Exa6_ManAddClause4( p, Abc_LitNot(pLits[n]), Abc_LitNot(pLits[m]), 0, 0 );
3619 }
3620 else
3621 {
3622 for ( k = 0; k < 3; k++ )
3623 Exa6_ManAddClause4( p, Abc_Var2Lit(iVarStart, k==1), Abc_Var2Lit(iVarStart+1, k==2), Abc_Var2Lit(iVarStart+2, k!=0), 0);
3624 if ( fOnlyAnd )
3625 Exa6_ManAddClause4( p, Abc_Var2Lit(iVarStart, 1), Abc_Var2Lit(iVarStart+1, 1), Abc_Var2Lit(iVarStart+2, 0), 0);
3626 }
3627 }
3628 for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ )
3629 {
3630 nLits = 0;
3631 for ( k = 0; k < 2; k++ )
3632 for ( j = i+1; j < p->nObjs; j++ )
3633 if ( p->VarMarks[j][k][i] )
3634 pLits[nLits++] = Abc_Var2Lit( p->VarMarks[j][k][i], 0 );
3635 //Exa6_ManAddClause( p, pLits, nLits );
3636 if ( fUniqFans )
3637 for ( n = 0; n < nLits; n++ )
3638 for ( m = n+1; m < nLits; m++ )
3639 Exa6_ManAddClause4( p, Abc_LitNot(pLits[n]), Abc_LitNot(pLits[m]), 0, 0 );
3640 }
3641 for ( i = p->nDivs + p->nNodes; i < p->nObjs; i++ )
3642 {
3643 nLits = 0;
3644 for ( j = 0; j < p->nDivs + p->nNodes; j++ ) if ( p->VarMarks[i][0][j] )
3645 pLits[nLits++] = Abc_Var2Lit( p->VarMarks[i][0][j], 0 );
3646 Exa6_ManAddClause( p, pLits, nLits );
3647 for ( n = 0; n < nLits; n++ )
3648 for ( m = n+1; m < nLits; m++ )
3649 Exa6_ManAddClause4( p, Abc_LitNot(pLits[n]), Abc_LitNot(pLits[m]), 0, 0 );
3650 }
3651 return 1;
3652}
Here is the caller graph for this function:

◆ Exa6_ManGenTest()

Mini_Aig_t * Exa6_ManGenTest ( Vec_Wrd_t * vSimsIn,
Vec_Wrd_t * vSimsOut,
int nIns,
int nDivs,
int nOuts,
int nNodes,
int TimeOut,
int fOnlyAnd,
int fFancy,
int fOrderNodes,
int fUniqFans,
int fVerbose )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 3849 of file bmcMaj.c.

3850{
3851 Mini_Aig_t * pMini = NULL;
3852 abctime clkTotal = Abc_Clock();
3853 Vec_Int_t * vValues = NULL;
3854 int Rand = ((((unsigned)rand()) << 12) ^ ((unsigned)rand())) & 0xFFFFF;
3855 char pFileNameIn[32]; sprintf( pFileNameIn, "_%05x_.cnf", Rand );
3856 char pFileNameOut[32]; sprintf( pFileNameOut, "_%05x_.out", Rand );
3857 Exa6_Man_t * p = Exa6_ManAlloc( vSimsIn, vSimsOut, nIns, 1+nIns+nDivs, nOuts, nNodes, fVerbose );
3858 Exa_ManIsNormalized( vSimsIn, vSimsOut );
3859 Exa6_ManGenCnf( p, pFileNameIn, fOnlyAnd, fFancy, fOrderNodes, fUniqFans );
3860 if ( fVerbose )
3861 printf( "Timeout = %d. OnlyAnd = %d. Fancy = %d. OrderNodes = %d. UniqueFans = %d. Verbose = %d.\n", TimeOut, fOnlyAnd, fFancy, fOrderNodes, fUniqFans, fVerbose );
3862 if ( fVerbose )
3863 printf( "CNF with %d variables and %d clauses was dumped into file \"%s\".\n", p->nCnfVars, p->nCnfClauses, pFileNameIn );
3864 vValues = Exa4_ManSolve( pFileNameIn, pFileNameOut, TimeOut, fVerbose );
3865 if ( vValues ) pMini = Exa6_ManMiniAig( p, vValues, fFancy );
3866 //if ( vValues ) Exa6_ManPrintSolution( p, vValues, fFancy );
3867 if ( vValues ) Exa_ManMiniPrint( pMini, p->nIns );
3868 if ( vValues && nIns <= 6 ) Exa_ManMiniVerify( pMini, vSimsIn, vSimsOut );
3869 Vec_IntFreeP( &vValues );
3870 Exa6_ManFree( p );
3871 unlink( pFileNameIn );
3872 Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
3873 return pMini;
3874}
Exa6_ManMiniAig
Mini_Aig_t * Exa6_ManMiniAig(Exa6_Man_t *p, Vec_Int_t *vValues, int fFancy)
Definition bmcMaj.c:3801
Exa6_ManGenCnf
void Exa6_ManGenCnf(Exa6_Man_t *p, char *pFileName, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans)
Definition bmcMaj.c:3724
Exa6_ManAlloc
Exa6_Man_t * Exa6_ManAlloc(Vec_Wrd_t *vSimsIn, Vec_Wrd_t *vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, int fVerbose)
Definition bmcMaj.c:3510
Exa6_ManFree
void Exa6_ManFree(Exa6_Man_t *p)
Definition bmcMaj.c:3527
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Exa6_ManMarkup()

int Exa6_ManMarkup ( Exa6_Man_t * p)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 3449 of file bmcMaj.c.

3450{
3451 int i, k, j, nVars[3] = {1 + 3*p->nNodes, 0, 3*p->nNodes*Vec_WrdSize(p->vSimsIn)};
3452 assert( p->nObjs <= MAJ_NOBJS );
3453 for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ )
3454 for ( k = 0; k < 2; k++ )
3455 for ( j = 1+!k; j < i-k; j++ )
3456 p->VarMarks[i][k][j] = nVars[0] + nVars[1]++;
3457 for ( i = p->nDivs + p->nNodes; i < p->nObjs; i++ )
3458 for ( j = 0; j < p->nDivs + p->nNodes; j++ )
3459 p->VarMarks[i][0][j] = nVars[0] + nVars[1]++;
3460 if ( p->fVerbose )
3461 printf( "Variables: Function = %d. Structure = %d. Internal = %d. Total = %d.\n",
3462 nVars[0], nVars[1], nVars[2], nVars[0] + nVars[1] + nVars[2] );
3463 if ( 0 )
3464 {
3465 for ( j = 0; j < 2; j++ )
3466 {
3467 printf( " : " );
3468 for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ )
3469 {
3470 for ( k = 0; k < 2; k++ )
3471 printf( "%3d ", j ? k : i );
3472 printf( " " );
3473 }
3474 printf( " " );
3475 for ( i = p->nDivs + p->nNodes; i < p->nObjs; i++ )
3476 {
3477 printf( "%3d ", j ? 0 : i );
3478 printf( " " );
3479 }
3480 printf( "\n" );
3481 }
3482 for ( j = 0; j < 5 + p->nNodes*9 + p->nOuts*5; j++ )
3483 printf( "-" );
3484 printf( "\n" );
3485 for ( j = p->nObjs - 2; j >= 0; j-- )
3486 {
3487 if ( j > 0 && j <= p->nIns )
3488 printf( " %c : ", 'a'+j-1 );
3489 else if ( j > p->nIns && j < p->nDivs )
3490 printf( " %c : ", 'A'+j-1-p->nIns );
3491 else
3492 printf( "%2d : ", j );
3493 for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ )
3494 {
3495 for ( k = 0; k < 2; k++ )
3496 printf( "%3d ", p->VarMarks[i][k][j] );
3497 printf( " " );
3498 }
3499 printf( " " );
3500 for ( i = p->nDivs + p->nNodes; i < p->nObjs; i++ )
3501 {
3502 printf( "%3d ", p->VarMarks[i][0][j] );
3503 printf( " " );
3504 }
3505 printf( "\n" );
3506 }
3507 }
3508 return nVars[0] + nVars[1] + nVars[2];
3509}
Here is the caller graph for this function:

◆ Exa6_ManMiniAig()

Mini_Aig_t * Exa6_ManMiniAig ( Exa6_Man_t * p,
Vec_Int_t * vValues,
int fFancy )

Definition at line 3801 of file bmcMaj.c.

3802{
3803 int i, k, Compl[MAJ_NOBJS] = {0};
3804 Mini_Aig_t * pMini = Mini_AigStartSupport( p->nDivs-1, p->nObjs );
3805 for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ )
3806 {
3807 int iNodes[2] = {0};
3808 int iVarStart = 1 + 3*(i - p->nDivs);//
3809 int Val1 = Vec_IntEntry(vValues, iVarStart);
3810 int Val2 = Vec_IntEntry(vValues, iVarStart+1);
3811 int Val3 = Vec_IntEntry(vValues, iVarStart+2);
3812 Compl[i] = Val1 && Val2 && Val3;
3813 for ( k = 0; k < 2; k++ )
3814 {
3815 int iNode = Exa6_ManFindFanin( p, vValues, i, !k );
3816 int fComp = k ? !Val1 && Val2 && !Val3 : Val1 && !Val2 && !Val3;
3817 iNodes[k] = Abc_Var2Lit(iNode, fComp ^ Compl[iNode]);
3818 }
3819 if ( Val1 && Val2 )
3820 {
3821 if ( Val3 )
3822 Mini_AigOr( pMini, iNodes[0], iNodes[1] );
3823 else
3824 Mini_AigXorSpecial( pMini, iNodes[0], iNodes[1] );
3825 }
3826 else
3827 Mini_AigAnd( pMini, iNodes[0], iNodes[1] );
3828 }
3829 for ( i = p->nDivs + p->nNodes; i < p->nObjs; i++ )
3830 {
3831 int iVar = Exa6_ManFindFanin( p, vValues, i, 0 );
3832 Mini_AigCreatePo( pMini, Abc_Var2Lit(iVar, Compl[iVar]) );
3833 }
3834 assert( p->nObjs == Mini_AigNodeNum(pMini) );
3835 return pMini;
3836}
Here is the caller graph for this function:

◆ Exa6_ManPolarMinterm()

word Exa6_ManPolarMinterm ( word Mint,
int nOuts,
int Polar )

Definition at line 3902 of file bmcMaj.c.

3903{
3904 word MintNew = 0;
3905 int m, nMints = 1 << nOuts;
3906 for ( m = 0; m < nMints; m++ )
3907 if ( (Mint >> m) & 1 )
3908 MintNew |= (word)1 << (m ^ Polar);
3909 return MintNew;
3910}
Here is the caller graph for this function:

◆ Exa6_ManPrintSolution()

void Exa6_ManPrintSolution ( Exa6_Man_t * p,
Vec_Int_t * vValues,
int fFancy )

Definition at line 3772 of file bmcMaj.c.

3773{
3774 int i, k;
3775 printf( "Circuit for %d-var function with %d divisors contains %d two-input gates:\n", p->nIns, p->nDivs, p->nNodes );
3776 for ( i = p->nDivs + p->nNodes; i < p->nObjs; i++ )
3777 {
3778 int iVar = Exa6_ManFindFanin( p, vValues, i, 0 );
3779 printf( "%2d = ", i );
3780 Exa6_ManPrintFanin( p, iVar, 0 );
3781 printf( "\n" );
3782 }
3783 for ( i = p->nDivs + p->nNodes - 1; i >= p->nDivs; i-- )
3784 {
3785 int iVarStart = 1 + 3*(i - p->nDivs);//
3786 int Val1 = Vec_IntEntry(vValues, iVarStart);
3787 int Val2 = Vec_IntEntry(vValues, iVarStart+1);
3788 int Val3 = Vec_IntEntry(vValues, iVarStart+2);
3789 printf( "%2d = ", i );
3790 for ( k = 0; k < 2; k++ )
3791 {
3792 int iNode = Exa6_ManFindFanin( p, vValues, i, !k );
3793 int fComp = k ? !Val1 && Val2 && !Val3 : Val1 && !Val2 && !Val3;
3794 Exa6_ManPrintFanin( p, iNode, fComp );
3795 if ( k ) break;
3796 printf( " %c", (Val1 && Val2) ? (Val3 ? '|' : '^') : '&' );
3797 }
3798 printf( "\n" );
3799 }
3800}

◆ Exa6_ManTransformInputs()

Vec_Wrd_t * Exa6_ManTransformInputs ( Vec_Wrd_t * vIns)

Definition at line 3927 of file bmcMaj.c.

3928{
3929 Vec_Wrd_t * vRes = Vec_WrdAlloc( Vec_WrdSize(vIns) );
3930 int i; word Entry, Polar = Vec_WrdEntry( vIns, 0 );
3931 Vec_WrdForEachEntry( vIns, Entry, i )
3932 Vec_WrdPush( vRes, Entry ^ Polar );
3933 return vRes;
3934}
Vec_WrdForEachEntry
#define Vec_WrdForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecWrd.h:54
Vec_Wrd_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Wrd_t_ Vec_Wrd_t
INCLUDES ///.
Definition vecWrd.h:42
Here is the caller graph for this function:

◆ Exa6_ManTransformOutputs()

Vec_Wrd_t * Exa6_ManTransformOutputs ( Vec_Wrd_t * vOuts,
int nOuts )

Definition at line 3919 of file bmcMaj.c.

3920{
3921 Vec_Wrd_t * vRes = Vec_WrdAlloc( Vec_WrdSize(vOuts) );
3922 int i, Polar = Exa6_ManFindPolar( Vec_WrdEntry(vOuts, 0), nOuts ); word Entry;
3923 Vec_WrdForEachEntry( vOuts, Entry, i )
3924 Vec_WrdPush( vRes, Exa6_ManPolarMinterm(Entry, nOuts, Polar) );
3925 return vRes;
3926}
Exa6_ManFindPolar
int Exa6_ManFindPolar(word First, int nOuts)
Definition bmcMaj.c:3911
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Exa6_ReadFile()

int Exa6_ReadFile ( char * pFileName,
Vec_Wrd_t ** pvSimsDiv,
Vec_Wrd_t ** pvSimsOut,
int * pnDivs,
int * pnOuts )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 3164 of file bmcMaj.c.

3165{
3166 int nIns = 0, nDivs = 0, nOuts = 0, nPats = 0, iLine = 0;
3167 int iIns = 0, iDivs = 0, iOuts = 0, Value, i;
3168 char pBuffer[1000];
3169 FILE * pFile = fopen( pFileName, "rb" );
3170 if ( pFile == NULL )
3171 {
3172 Abc_Print( -1, "Cannot open file \"%s\".\n", pFileName );
3173 return 0;
3174 }
3175 while ( fgets( pBuffer, 1000, pFile ) != NULL )
3176 {
3177 if ( pBuffer[0] == 'c' )
3178 break;
3179 if ( iLine++ == 0 )
3180 {
3181 char * pLine = pBuffer;
3182 while ( (*pLine >= 'a' && *pLine <= 'z') || (*pLine >= 'A' && *pLine <= 'Z') )
3183 pLine++;
3184 Value = sscanf( pLine, "%d %d %d %d", &nIns, &nDivs, &nOuts, &nPats );
3185 if ( Value != 4 )
3186 {
3187 Abc_Print( -1, "Cannot read the parameter line in file \"%s\".\n", pFileName );
3188 fclose( pFile );
3189 return 0;
3190 }
3191 if ( nIns + nDivs >= 64 )
3192 {
3193 printf( "The number of variables and divisors should not exceed 64.\n" );
3194 return 0;
3195 }
3196 if ( nOuts > 6 )
3197 {
3198 printf( "The number of outputs should not exceed 6.\n" );
3199 return 0;
3200 }
3201 if ( nPats >= 1000 )
3202 {
3203 printf( "The number of patterns should not exceed 1000.\n" );
3204 return 0;
3205 }
3206 assert( nIns + nDivs < 64 && nOuts <= 6 && (nIns == 0 || nPats <= (1 << nIns)) && nPats < 1000 );
3207 *pvSimsDiv = Vec_WrdStart( nPats );
3208 *pvSimsOut = Vec_WrdStart( nPats );
3209 continue;
3210 }
3211 if ( pBuffer[0] == '\n' || pBuffer[0] == '\r' || pBuffer[0] == ' ' )
3212 continue;
3213 for ( i = 0; i < nPats; i++ )
3214 {
3215 if ( pBuffer[i] == '0' )
3216 continue;
3217 assert( pBuffer[i] == '1' );
3218 if ( iIns < nIns )
3219 Abc_TtSetBit( Vec_WrdEntryP(*pvSimsDiv, nPats-1-i), 1+iIns );
3220 else if ( iDivs < nDivs )
3221 Abc_TtSetBit( Vec_WrdEntryP(*pvSimsDiv, nPats-1-i), 1+nIns+iDivs );
3222 else if ( iOuts < (1 << nOuts) )
3223 Abc_TtSetBit( Vec_WrdEntryP(*pvSimsOut, nPats-1-i), iOuts );
3224 }
3225 assert( pBuffer[nPats] != '0' && pBuffer[nPats] != '1' );
3226 if ( iIns < nIns )
3227 iIns++;
3228 else if ( iDivs < nDivs )
3229 iDivs++;
3230 else if ( iOuts < (1 << nOuts) )
3231 iOuts++;
3232 }
3233 printf( "Finished reading file \"%s\" with %d inputs, %d divisors, %d outputs, and %d patterns.\n", pFileName, nIns, nDivs, nOuts, nPats );
3234 fclose( pFile );
3235 assert( iIns == nIns && iDivs == nDivs && iOuts == (1 << nOuts) );
3236 if ( pnDivs )
3237 *pnDivs = nDivs;
3238 if ( pnOuts )
3239 *pnOuts = nOuts;
3240 return nIns;
3241}
Here is the caller graph for this function:

◆ Exa6_SortSims()

void Exa6_SortSims ( Vec_Wrd_t * vSimsDiv,
Vec_Wrd_t * vSimsOut )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 3130 of file bmcMaj.c.

3131{
3132 word * pSims = Vec_WrdArray( vSimsDiv );
3133 word * pOuts = Vec_WrdArray( vSimsOut ), temp;
3134 int i, j, best_i, nSize = Vec_WrdSize(vSimsDiv);
3135 assert( Vec_WrdSize(vSimsOut) == nSize );
3136 for ( i = 0; i < nSize-1; i++ )
3137 {
3138 best_i = i;
3139 for ( j = i+1; j < nSize; j++ )
3140 if ( pSims[j] < pSims[best_i] )
3141 best_i = j;
3142 if ( i == best_i )
3143 continue;
3144 temp = pSims[i];
3145 pSims[i] = pSims[best_i];
3146 pSims[best_i] = temp;
3147 temp = pOuts[i];
3148 pOuts[i] = pOuts[best_i];
3149 pOuts[best_i] = temp;
3150 }
3151}
Here is the caller graph for this function:

◆ Exa6_WriteFile()

void Exa6_WriteFile ( char * pFileName,
int nVars,
word * pTruths,
int nTruths )

Definition at line 3242 of file bmcMaj.c.

3243{
3244 int i, o, m, nMintsI = 1 << nVars, nMintsO = 1 << nTruths;
3245 FILE * pFile = fopen( pFileName, "wb" );
3246 fprintf( pFile, "%d %d %d %d\n", nVars, 0, nTruths, nMintsI );
3247 fprintf( pFile, "\n" );
3248 for ( i = 0; i < nVars; i++, fprintf( pFile, "\n" ) )
3249 for ( m = nMintsI - 1; m >= 0; m-- )
3250 fprintf( pFile, "%d", (m >> i) & 1 );
3251 fprintf( pFile, "\n" );
3252 for ( o = 0; o < nMintsO; o++, fprintf( pFile, "\n" ) )
3253 for ( m = nMintsI - 1; m >= 0; m-- )
3254 {
3255 int oMint = 0;
3256 for ( i = 0; i < nTruths; i++ )
3257 if ( Abc_TtGetBit(pTruths+i, m) )
3258 oMint |= (word)1 << i;
3259 fprintf( pFile, "%d", oMint == o );
3260 }
3261 fclose( pFile );
3262}
Here is the caller graph for this function:

◆ Exa6_WriteFile2()

void Exa6_WriteFile2 ( char * pFileName,
int nVars,
int nDivs,
int nOuts,
Vec_Wrd_t * vSimsDiv,
Vec_Wrd_t * vSimsOut )

Definition at line 3263 of file bmcMaj.c.

3264{
3265 int i, o, m, nMintsO = 1 << nOuts;
3266 FILE * pFile = fopen( pFileName, "wb" );
3267 assert( Vec_WrdSize(vSimsDiv) == Vec_WrdSize(vSimsOut) );
3268 fprintf( pFile, "%d %d %d %d\n", nVars, nDivs, nOuts, Vec_WrdSize(vSimsOut) );
3269 fprintf( pFile, "\n" );
3270 for ( i = 0; i < nVars+nDivs; i++, fprintf( pFile, "\n%s", (i == nVars && nDivs) ? "\n":"" ) )
3271 for ( m = Vec_WrdSize(vSimsOut) - 1; m >= 0; m-- )
3272 fprintf( pFile, "%d", Abc_TtGetBit(Vec_WrdEntryP(vSimsDiv, m), 1+i) );
3273 fprintf( pFile, "\n" );
3274 for ( o = 0; o < nMintsO; o++, fprintf( pFile, "\n" ) )
3275 for ( m = Vec_WrdSize(vSimsOut) - 1; m >= 0; m-- )
3276 fprintf( pFile, "%d", Abc_TtGetBit(Vec_WrdEntryP(vSimsOut, m), o) );
3277 fclose( pFile );
3278}
Here is the caller graph for this function:

◆ Exa7_GetVar()

int Exa7_GetVar ( int n,
int i,
int j,
int m )

Definition at line 4060 of file bmcMaj.c.

4061{
4062 return 1 + n*n*m + n*i + j;
4063}
Here is the caller graph for this function:

◆ Exa7_ManGenCnf()

int Exa7_ManGenCnf ( char * pFileName,
word * pTruth,
int nVars,
int nNodes,
int GateSize )

Definition at line 4064 of file bmcMaj.c.

4065{
4066 int m, n, v, k, nV = nVars + nNodes, nMints = 1 << nVars, nClas = 0;
4067 int pVars[32] = {0}; assert( nVars + nNodes + 1 < 32 );
4068 FILE * pFile = fopen( pFileName, "wb" );
4069 fputs( "p cnf \n", pFile );
4070 for ( m = 0; m < nMints; m++ )
4071 {
4072 for ( v = 0; v < nVars; v++ )
4073 nClas += Exa7_AddClause4( pFile, Abc_Var2Lit(Exa7_GetVar(nV, v, v, m), ((m >> v)&1)==0), 0, 0, 0 );
4074 nClas += Exa7_AddClause4( pFile, Abc_Var2Lit(Exa7_GetVar(nV, nV-1, nV-1, m), ((pTruth[0] >> m)&1)==0), 0, 0, 0 );
4075 for ( n = nVars; n < nV; n++ )
4076 {
4077 int iValNode = Exa7_GetVar(nV, n, n, m);
4078 for ( v = 0; v < n; v++ )
4079 {
4080 int iParVar = Exa7_GetVar(nV, v, n, 0); // v < n
4081 int iFanVar = Exa7_GetVar(nV, n, v, m);
4082 int iValFan = Exa7_GetVar(nV, v, v, m);
4083 // iFanVar = ~iParVar | iValFan
4084 nClas += Exa7_AddClause4( pFile, Abc_Var2Lit(iFanVar, 1), Abc_Var2Lit(iParVar, 1), Abc_Var2Lit(iValFan, 0), 0 );
4085 nClas += Exa7_AddClause4( pFile, Abc_Var2Lit(iFanVar, 0), Abc_Var2Lit(iParVar, 0), 0, 0 );
4086 nClas += Exa7_AddClause4( pFile, Abc_Var2Lit(iFanVar, 0), Abc_Var2Lit(iValFan, 1), 0, 0 );
4087 // iParVar & ~iValFan => iValNode
4088 nClas += Exa7_AddClause4( pFile, Abc_Var2Lit(iParVar, 1), Abc_Var2Lit(iValFan, 0), Abc_Var2Lit(iValNode, 0), 0 );
4089 pVars[v] = Abc_Var2Lit(iFanVar, 1);
4090 }
4091 pVars[v] = Abc_Var2Lit(iValNode, 1);
4092 // (iFanVar0 & iFanVar1 & iFanVar2) => ~iValNode
4093 nClas += Exa7_AddClause( pFile, pVars, n+1 );
4094 }
4095 }
4096 for ( n = nVars; n < nV; n++ ) {
4097 for ( v = 0; v < n; v++ )
4098 pVars[v] = Abc_Var2Lit(Exa7_GetVar(nV, v, n, 0), 0); // v < n
4099 nClas += Exa7_AddClause( pFile, pVars, n );
4100 if ( GateSize ) {
4101 int Total = 1 << n, Limit = GateSize + 1;
4102 for ( m = 0; m < Total; m++ )
4103 {
4104 if ( Abc_TtCountOnes((word)m) != Limit )
4105 continue;
4106 for ( k = v = 0; v < n; v++ )
4107 if ( (m >> v) & 1 )
4108 pVars[k++] = Abc_Var2Lit(Exa7_GetVar(nV, v, n, 0), 1);
4109 assert( k == Limit );
4110 nClas += Exa7_AddClause( pFile, pVars, Limit );
4111 }
4112 }
4113 }
4114 rewind( pFile );
4115 fprintf( pFile, "p cnf %d %d", nMints * nV * nV, nClas );
4116 fclose( pFile );
4117 return nClas;
4118}
Exa7_GetVar
int Exa7_GetVar(int n, int i, int j, int m)
Definition bmcMaj.c:4060
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Exa_ManAddCnf()

int Exa_ManAddCnf ( Exa_Man_t * p,
int iMint )

Definition at line 885 of file bmcMaj.c.

886{
887 // save minterm values
888 int i, k, n, j, Value = Abc_TtGetBit(p->pTruth, iMint);
889 for ( i = 0; i < p->nVars; i++ )
890 p->VarVals[i] = (iMint >> i) & 1;
891 bmcg_sat_solver_set_nvars( p->pSat, p->iVar + 3*p->nNodes );
892 //printf( "Adding clauses for minterm %d with value %d.\n", iMint, Value );
893 for ( i = p->nVars; i < p->nObjs; i++ )
894 {
895 // fanin connectivity
896 int iVarStart = 1 + 3*(i - p->nVars);//
897 int iBaseSatVarI = p->iVar + 3*(i - p->nVars);
898 for ( k = 0; k < 2; k++ )
899 {
900 for ( j = 0; j < p->nObjs; j++ ) if ( p->VarMarks[i][k][j] )
901 {
902 int iBaseSatVarJ = p->iVar + 3*(j - p->nVars);
903 for ( n = 0; n < 2; n++ )
904 {
905 int pLits[3], nLits = 0;
906 pLits[nLits++] = Abc_Var2Lit( p->VarMarks[i][k][j], 1 );
907 pLits[nLits++] = Abc_Var2Lit( iBaseSatVarI + k, n );
908 if ( j >= p->nVars )
909 pLits[nLits++] = Abc_Var2Lit( iBaseSatVarJ + 2, !n );
910 else if ( p->VarVals[j] == n )
911 continue;
912 if ( !Exa_ManAddClause( p, pLits, nLits ) )
913 return 0;
914 }
915 }
916 }
917 // node functionality
918 for ( n = 0; n < 2; n++ )
919 {
920 if ( i == p->nObjs - 1 && n == Value )
921 continue;
922 for ( k = 0; k < 4; k++ )
923 {
924 int pLits[4], nLits = 0;
925 if ( k == 0 && n == 1 )
926 continue;
927 pLits[nLits++] = Abc_Var2Lit( iBaseSatVarI + 0, (k&1) );
928 pLits[nLits++] = Abc_Var2Lit( iBaseSatVarI + 1, (k>>1) );
929 if ( i != p->nObjs - 1 ) pLits[nLits++] = Abc_Var2Lit( iBaseSatVarI + 2, !n );
930 if ( k > 0 ) pLits[nLits++] = Abc_Var2Lit( iVarStart + k-1, n );
931 assert( nLits <= 4 );
932 if ( !Exa_ManAddClause( p, pLits, nLits ) )
933 return 0;
934 }
935 }
936 }
937 p->iVar += 3*p->nNodes;
938 return 1;
939}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Exa_ManAddCnfAdd()

int Exa_ManAddCnfAdd ( Exa_Man_t * p,
int * pnAdded )

Definition at line 710 of file bmcMaj.c.

711{
712 int pLits[MAJ_NOBJS], pLits2[2], i, j, k, n, m;
713 *pnAdded = 0;
714 for ( i = p->nVars; i < p->nObjs; i++ )
715 {
716 for ( k = 0; k < 2; k++ )
717 {
718 int nLits = 0;
719 for ( j = 0; j < p->nObjs; j++ )
720 if ( p->VarMarks[i][k][j] && bmcg_sat_solver_read_cex_varvalue(p->pSat, p->VarMarks[i][k][j]) )
721 pLits[nLits++] = Abc_Var2Lit( p->VarMarks[i][k][j], 0 );
722 assert( nLits > 0 );
723 // input uniqueness
724 for ( n = 0; n < nLits; n++ )
725 for ( m = n+1; m < nLits; m++ )
726 {
727 (*pnAdded)++;
728 pLits2[0] = Abc_LitNot(pLits[n]);
729 pLits2[1] = Abc_LitNot(pLits[m]);
730 if ( !Exa_ManAddClause( p, pLits2, 2 ) )
731 return 0;
732 }
733 if ( k == 1 )
734 break;
735 // symmetry breaking
736 for ( j = 0; j < p->nObjs; j++ ) if ( p->VarMarks[i][k][j] && bmcg_sat_solver_read_cex_varvalue(p->pSat, p->VarMarks[i][k][j]) )
737 for ( n = j; n < p->nObjs; n++ ) if ( p->VarMarks[i][k+1][n] && bmcg_sat_solver_read_cex_varvalue(p->pSat, p->VarMarks[i][k+1][j]) )
738 {
739 (*pnAdded)++;
740 pLits2[0] = Abc_Var2Lit( p->VarMarks[i][k][j], 1 );
741 pLits2[1] = Abc_Var2Lit( p->VarMarks[i][k+1][n], 1 );
742 if ( !Exa_ManAddClause( p, pLits2, 2 ) )
743 return 0;
744 }
745 }
746 }
747 return 1;
748}
bmcg_sat_solver_read_cex_varvalue
int bmcg_sat_solver_read_cex_varvalue(bmcg_sat_solver *s, int ivar)
Definition AbcGlucose.cpp:220
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Exa_ManAddCnfStart()

int Exa_ManAddCnfStart ( Exa_Man_t * p,
int fOnlyAnd )

Definition at line 764 of file bmcMaj.c.

765{
766 extern Vec_Int_t * Gia_ManKSatGenLevels( char * pGuide, int nIns, int nNodes );
767 Vec_Int_t * vRes = p->pPars->pGuide ? Gia_ManKSatGenLevels( p->pPars->pGuide, p->nVars, p->nNodes ) : NULL;
768 int pLits[MAJ_NOBJS], pLits2[3], i, j, k, n, m, Start, Stop;
769 if ( vRes ) {
770 n = p->nVars;
771 Vec_IntForEachEntryDoubleStart( vRes, Start, Stop, i, 2*p->nVars ) {
772 for ( j = 0; j < Start; j++ )
773 if ( p->VarMarks[n][0][j] ) {
774 pLits[0] = Abc_Var2Lit( p->VarMarks[n][0][j], 1 );
775 Exa_ManAddClause( p, pLits, 1 );
776 }
777 for ( k = 0; k < 2; k++ )
778 for ( j = Stop; j < n; j++ )
779 if ( p->VarMarks[n][k][j] ) {
780 pLits[0] = Abc_Var2Lit( p->VarMarks[n][k][j], 1 );
781 Exa_ManAddClause( p, pLits, 1 );
782 }
783 n++;
784 }
785 assert( n == p->nVars + p->nNodes );
786 Vec_IntFreeP( &vRes );
787 }
788 // input constraints
789 for ( i = p->nVars; i < p->nObjs; i++ )
790 {
791 int iVarStart = 1 + 3*(i - p->nVars);//
792 for ( k = 0; k < 2; k++ )
793 {
794 int nLits = 0;
795 for ( j = 0; j < p->nObjs; j++ )
796 if ( p->VarMarks[i][k][j] )
797 pLits[nLits++] = Abc_Var2Lit( p->VarMarks[i][k][j], 0 );
798 assert( nLits > 0 );
799 if ( !Exa_ManAddClause( p, pLits, nLits ) )
800 return 0;
801 // input uniqueness
802 if ( !p->pPars->fDynConstr )
803 {
804 for ( n = 0; n < nLits; n++ )
805 for ( m = n+1; m < nLits; m++ )
806 {
807 pLits2[0] = Abc_LitNot(pLits[n]);
808 pLits2[1] = Abc_LitNot(pLits[m]);
809 if ( !Exa_ManAddClause( p, pLits2, 2 ) )
810 return 0;
811 }
812 }
813 if ( k == 1 )
814 break;
815 // symmetry breaking
816 if ( !p->pPars->fDynConstr )
817 {
818 for ( j = 0; j < p->nObjs; j++ ) if ( p->VarMarks[i][k][j] )
819 for ( n = j; n < p->nObjs; n++ ) if ( p->VarMarks[i][k+1][n] )
820 {
821 pLits2[0] = Abc_Var2Lit( p->VarMarks[i][k][j], 1 );
822 pLits2[1] = Abc_Var2Lit( p->VarMarks[i][k+1][n], 1 );
823 if ( !Exa_ManAddClause( p, pLits2, 2 ) )
824 return 0;
825 }
826 }
827 }
828#ifdef USE_NODE_ORDER
829 // node ordering
830 for ( j = p->nVars; j < i; j++ )
831 for ( n = 0; n < p->nObjs; n++ ) if ( p->VarMarks[i][0][n] )
832 for ( m = n+1; m < p->nObjs; m++ ) if ( p->VarMarks[j][0][m] )
833 {
834 pLits2[0] = Abc_Var2Lit( p->VarMarks[i][0][n], 1 );
835 pLits2[1] = Abc_Var2Lit( p->VarMarks[j][0][m], 1 );
836 if ( !Exa_ManAddClause( p, pLits2, 2 ) )
837 return 0;
838 }
839#endif
840 // unique functions
841 for ( j = p->nVars; j < i; j++ )
842 for ( k = 0; k < 2; k++ ) if ( p->VarMarks[i][k][j] )
843 {
844 pLits2[0] = Abc_Var2Lit( p->VarMarks[i][k][j], 1 );
845 for ( n = 0; n < p->nObjs; n++ )
846 for ( m = 0; m < 2; m++ )
847 {
848 if ( p->VarMarks[i][!k][n] && p->VarMarks[j][m][n] )
849 {
850 pLits2[1] = Abc_Var2Lit( p->VarMarks[i][!k][n], 1 );
851 pLits2[2] = Abc_Var2Lit( p->VarMarks[j][m][n], 1 );
852 if ( !Exa_ManAddClause( p, pLits2, 3 ) )
853 return 0;
854 }
855 }
856 }
857 // two input functions
858 for ( k = 0; k < 3; k++ )
859 {
860 pLits[0] = Abc_Var2Lit( iVarStart, k==1 );
861 pLits[1] = Abc_Var2Lit( iVarStart+1, k==2 );
862 pLits[2] = Abc_Var2Lit( iVarStart+2, k!=0 );
863 if ( !Exa_ManAddClause( p, pLits, 3 ) )
864 return 0;
865 }
866 if ( fOnlyAnd )
867 {
868 pLits[0] = Abc_Var2Lit( iVarStart, 1 );
869 pLits[1] = Abc_Var2Lit( iVarStart+1, 1 );
870 pLits[2] = Abc_Var2Lit( iVarStart+2, 0 );
871 if ( !Exa_ManAddClause( p, pLits, 3 ) )
872 return 0;
873 }
874 }
875 // outputs should be used
876 for ( i = 0; i < p->nObjs - 1; i++ )
877 {
878 Vec_Int_t * vArray = Vec_WecEntry(p->vOutLits, i);
879 assert( Vec_IntSize(vArray) > 0 );
880 if ( !Exa_ManAddClause( p, Vec_IntArray(vArray), Vec_IntSize(vArray) ) )
881 return 0;
882 }
883 return 1;
884}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Exa_ManAlloc()

Exa_Man_t * Exa_ManAlloc ( Bmc_EsPar_t * pPars,
word * pTruth )

Definition at line 502 of file bmcMaj.c.

503{
504 Exa_Man_t * p = ABC_CALLOC( Exa_Man_t, 1 );
505 p->pPars = pPars;
506 p->nVars = pPars->nVars;
507 p->nNodes = pPars->nNodes;
508 p->nObjs = pPars->nVars + pPars->nNodes;
509 p->nWords = Abc_TtWordNum(pPars->nVars);
510 p->pTruth = pTruth;
511 p->vOutLits = Vec_WecStart( p->nObjs );
512 p->iVar = Exa_ManMarkup( p );
513 p->vInfo = Exa_ManTruthTables( p );
514 p->pSat = bmcg_sat_solver_start();
515 bmcg_sat_solver_set_nvars( p->pSat, p->iVar );
516 if ( pPars->RuntimeLim )
517 bmcg_sat_solver_set_runtime_limit( p->pSat, Abc_Clock() + pPars->RuntimeLim * CLOCKS_PER_SEC );
518 if ( pPars->fDumpCnf )
519 {
520 char Buffer[1000];
521 sprintf( Buffer, "%s_%d_%d.cnf", p->pPars->pTtStr, 2, p->nNodes );
522 p->pFile = fopen( Buffer, "wb" );
523 fputs( "p cnf \n", p->pFile );
524 }
525 return p;
526}
bmcg_sat_solver_set_runtime_limit
abctime bmcg_sat_solver_set_runtime_limit(bmcg_sat_solver *s, abctime Limit)
Definition AbcGlucose.cpp:230
bmcg_sat_solver_start
bmcg_sat_solver * bmcg_sat_solver_start()
MACRO DEFINITIONS ///.
Definition AbcGlucose.cpp:146
Exa_ManTruthTables
Vec_Wrd_t * Exa_ManTruthTables(Exa_Man_t *p)
Definition bmcMaj.c:454
Exa_ManMarkup
int Exa_ManMarkup(Exa_Man_t *p)
Definition bmcMaj.c:462
Exa_Man_t
struct Exa_Man_t_ Exa_Man_t
Definition bmcMaj.c:421
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Exa_ManDumpBlif()

void Exa_ManDumpBlif ( Exa_Man_t * p,
int fCompl )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 606 of file bmcMaj.c.

607{
608 char Buffer[1000];
609 char FileName[1100];
610 FILE * pFile;
611 int i, k, iVar;
612 if ( fCompl )
613 Abc_TtNot( p->pTruth, p->nWords );
614 Extra_PrintHexadecimalString( Buffer, (unsigned *)p->pTruth, p->nVars );
615 if ( fCompl )
616 Abc_TtNot( p->pTruth, p->nWords );
617 sprintf( FileName, "%s_%d_%d.blif", Buffer, 2, p->nNodes );
618 pFile = fopen( FileName, "wb" );
619 fprintf( pFile, "# Realization of the %d-input function %s using %d two-input gates:\n", p->nVars, Buffer, p->nNodes );
620 fprintf( pFile, ".model %s_%d_%d\n", Buffer, 2, p->nNodes );
621 fprintf( pFile, ".inputs" );
622 for ( i = 0; i < p->nVars; i++ )
623 fprintf( pFile, " %c", 'a'+i );
624 fprintf( pFile, "\n" );
625 fprintf( pFile, ".outputs F\n" );
626 for ( i = p->nObjs - 1; i >= p->nVars; i-- )
627 {
628 int iVarStart = 1 + 3*(i - p->nVars);//
629 int Val1 = bmcg_sat_solver_read_cex_varvalue(p->pSat, iVarStart);
630 int Val2 = bmcg_sat_solver_read_cex_varvalue(p->pSat, iVarStart+1);
631 int Val3 = bmcg_sat_solver_read_cex_varvalue(p->pSat, iVarStart+2);
632
633 fprintf( pFile, ".names" );
634 for ( k = 1; k >= 0; k-- )
635 {
636 iVar = Exa_ManFindFanin( p, i, k );
637 if ( iVar >= 0 && iVar < p->nVars )
638 fprintf( pFile, " %c", 'a'+iVar );
639 else
640 fprintf( pFile, " %02d", iVar );
641 }
642 if ( i == p->nObjs - 1 )
643 fprintf( pFile, " F\n" );
644 else
645 fprintf( pFile, " %02d\n", i );
646 if ( i == p->nObjs - 1 && fCompl )
647 fprintf( pFile, "00 1\n" );
648 if ( (i == p->nObjs - 1 && fCompl) ^ Val1 )
649 fprintf( pFile, "01 1\n" );
650 if ( (i == p->nObjs - 1 && fCompl) ^ Val2 )
651 fprintf( pFile, "10 1\n" );
652 if ( (i == p->nObjs - 1 && fCompl) ^ Val3 )
653 fprintf( pFile, "11 1\n" );
654 }
655 fprintf( pFile, ".end\n\n" );
656 fclose( pFile );
657 printf( "Solution was dumped into file \"%s\".\n", FileName );
658}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Exa_ManDumpVerilog()

void Exa_ManDumpVerilog ( Vec_Int_t * vValues,
int nVars,
int nNodes,
int GateSize,
word * pTruth )

Definition at line 4119 of file bmcMaj.c.

4120{
4121 FILE * pFile;
4122 char Buffer[1000];
4123 char FileName[1100];
4124 int v, n, k, nV = nVars+nNodes;
4125 Extra_PrintHexadecimalString( Buffer, (unsigned *)pTruth, nVars );
4126 sprintf( FileName, "func%s_%d_%d.v", Buffer, GateSize, nNodes );
4127 pFile = fopen( FileName, "wb" );
4128 fprintf( pFile, "// Realization of the %d-input function %s using %d NAND gates:\n", nVars, Buffer, nNodes );
4129 fprintf( pFile, "module func%s_%d_%d ( input", Buffer, GateSize, nNodes );
4130 for ( v = 0; v < nVars; v++ )
4131 fprintf( pFile, " %c,", 'a'+v );
4132 fprintf( pFile, " output out );\n" );
4133 for ( n = nVars; n < nV; n++ ) {
4134 int nFans = 0;
4135 for ( v = 0; v < n; v++ )
4136 nFans += Vec_IntEntry(vValues, Exa7_GetVar(nV, v, n, 0));
4137 fprintf( pFile, " wire %c = ~(", 'a'+n );
4138 for ( k = v = 0; v < n; v++ )
4139 if ( Vec_IntEntry(vValues, Exa7_GetVar(nV, v, n, 0)) )
4140 fprintf( pFile, "%c%s", 'a'+v, ++k < nFans ? " & ":"" );
4141 fprintf( pFile, ");\n" );
4142 }
4143 fprintf( pFile, " assign out = %c;\n", 'a'+nV-1 );
4144 fprintf( pFile, "endmodule\n\n" );
4145 fclose( pFile );
4146 printf( "Solution was dumped into file \"%s\".\n", FileName );
4147}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Exa_ManExactPrint()

void Exa_ManExactPrint ( Vec_Wrd_t * vSimsDiv,
Vec_Wrd_t * vSimsOut,
int nDivs,
int nOuts )

Definition at line 3935 of file bmcMaj.c.

3936{
3937 word Entry; int i;
3938 Vec_WrdForEachEntry( vSimsDiv, Entry, i )
3939 Abc_TtPrintBits( &Entry, nDivs );
3940 printf( "\n" );
3941 Vec_WrdForEachEntry( vSimsOut, Entry, i )
3942 Abc_TtPrintBits( &Entry, 1 << nOuts );
3943 printf( "\n" );
3944}
Here is the caller graph for this function:

◆ Exa_ManExactSynthesis()

void Exa_ManExactSynthesis ( Bmc_EsPar_t * pPars)

Definition at line 940 of file bmcMaj.c.

941{
942 int i, status, iMint = 1;
943 abctime clkTotal = Abc_Clock();
944 Exa_Man_t * p; int fCompl = 0;
945 word pTruth[16]; Abc_TtReadHex( pTruth, pPars->pTtStr );
946 assert( pPars->nVars <= 10 );
947 p = Exa_ManAlloc( pPars, pTruth );
948 if ( pTruth[0] & 1 ) { fCompl = 1; Abc_TtNot( pTruth, p->nWords ); }
949 status = Exa_ManAddCnfStart( p, pPars->fOnlyAnd );
950 assert( status );
951 printf( "Running exact synthesis for %d-input function with %d two-input gates...\n", p->nVars, p->nNodes );
952 for ( i = 0; iMint != -1; i++ )
953 {
954 abctime clk = Abc_Clock();
955 if ( !Exa_ManAddCnf( p, iMint ) )
956 break;
957 if ( pPars->fDynConstr )
958 status = Exa_ManSolverSolve( p );
959 else
960 status = bmcg_sat_solver_solve( p->pSat, NULL, 0 );
961 if ( pPars->fVerbose )
962 {
963 printf( "Iter %3d : ", i );
964 Extra_PrintBinary( stdout, (unsigned *)&iMint, p->nVars );
965 printf( " Var =%5d ", p->iVar );
966 printf( "Cla =%6d ", bmcg_sat_solver_clausenum(p->pSat) );
967 printf( "Conf =%9d ", bmcg_sat_solver_conflictnum(p->pSat) );
968 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
969 }
970 if ( status == GLUCOSE_UNSAT )
971 {
972 printf( "The problem has no solution.\n" );
973 break;
974 }
975 if ( status == GLUCOSE_UNDEC )
976 {
977 printf( "The solver timed out after %d sec.\n", pPars->RuntimeLim );
978 break;
979 }
980 iMint = Exa_ManEval( p );
981 }
982 if ( iMint == -1 )
983 {
984 Exa_ManPrintSolution( p, fCompl );
985 Exa_ManDumpBlif( p, fCompl );
986 }
987 Exa_ManFree( p );
988 Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
989}
Exa_ManDumpBlif
void Exa_ManDumpBlif(Exa_Man_t *p, int fCompl)
Definition bmcMaj.c:606
Exa_ManSolverSolve
int Exa_ManSolverSolve(Exa_Man_t *p)
Definition bmcMaj.c:749
Exa_ManAlloc
Exa_Man_t * Exa_ManAlloc(Bmc_EsPar_t *pPars, word *pTruth)
Definition bmcMaj.c:502
Exa_ManPrintSolution
void Exa_ManPrintSolution(Exa_Man_t *p, int fCompl)
Definition bmcMaj.c:659
Exa_ManAddCnf
int Exa_ManAddCnf(Exa_Man_t *p, int iMint)
Definition bmcMaj.c:885
Exa_ManFree
void Exa_ManFree(Exa_Man_t *p)
Definition bmcMaj.c:527
Exa_ManAddCnfStart
int Exa_ManAddCnfStart(Exa_Man_t *p, int fOnlyAnd)
Definition bmcMaj.c:764
Here is the call graph for this function:

◆ Exa_ManExactSynthesis4()

void Exa_ManExactSynthesis4 ( Bmc_EsPar_t * pPars)

Definition at line 2449 of file bmcMaj.c.

2450{
2451 Mini_Aig_t * pMini = NULL;
2452 int i, m, nMints = 1 << pPars->nVars, fCompl = 0;
2453 Vec_Wrd_t * vSimsIn = Vec_WrdStart( nMints );
2454 Vec_Wrd_t * vSimsOut = Vec_WrdStart( nMints );
2455 word pTruth[16]; Abc_TtReadHex( pTruth, pPars->pTtStr );
2456 if ( pTruth[0] & 1 ) { fCompl = 1; Abc_TtNot( pTruth, Abc_TtWordNum(pPars->nVars) ); }
2457 assert( pPars->nVars <= 10 );
2458 for ( m = 0; m < nMints; m++ )
2459 {
2460 Abc_TtSetBit( Vec_WrdEntryP(vSimsOut, m), Abc_TtGetBit(pTruth, m) );
2461 for ( i = 0; i < pPars->nVars; i++ )
2462 if ( (m >> i) & 1 )
2463 Abc_TtSetBit( Vec_WrdEntryP(vSimsIn, m), 1+i );
2464 }
2465 assert( Vec_WrdSize(vSimsIn) == (1 << pPars->nVars) );
2466 pMini = Exa4_ManGenTest( vSimsIn, vSimsOut, pPars->nVars, 1+pPars->nVars, 1, pPars->nNodes, pPars->RuntimeLim, pPars->fOnlyAnd, pPars->fFewerVars, pPars->fOrderNodes, pPars->fUniqFans, pPars->fVerbose, pPars->fCard, pPars->pGuide );
2467 if ( pMini ) Mini_AigStop( pMini );
2468 if ( fCompl ) printf( "The resulting circuit, if computed, will be complemented.\n" );
2469 Vec_WrdFree( vSimsIn );
2470 Vec_WrdFree( vSimsOut );
2471}
Exa4_ManGenTest
Mini_Aig_t * Exa4_ManGenTest(Vec_Wrd_t *vSimsIn, Vec_Wrd_t *vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, int TimeOut, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fVerbose, int fCard, char *pGuide)
Definition bmcMaj.c:2395
Here is the call graph for this function:

◆ Exa_ManExactSynthesis4_()

void Exa_ManExactSynthesis4_ ( Bmc_EsPar_t * pPars)

Definition at line 2426 of file bmcMaj.c.

2427{
2428 Mini_Aig_t * pMini = NULL;
2429 int i, m;
2430 Vec_Wrd_t * vSimsIn = Vec_WrdStart( 8 );
2431 Vec_Wrd_t * vSimsOut = Vec_WrdStart( 8 );
2432 int Truths[2] = { 0x96, 0xE8 };
2433 for ( m = 0; m < 8; m++ )
2434 {
2435 int iOutMint = 0;
2436 for ( i = 0; i < 2; i++ )
2437 if ( (Truths[i] >> m) & 1 )
2438 iOutMint |= 1 << i;
2439 Abc_TtSetBit( Vec_WrdEntryP(vSimsOut, m), iOutMint );
2440 for ( i = 0; i < 3; i++ )
2441 if ( (m >> i) & 1 )
2442 Abc_TtSetBit( Vec_WrdEntryP(vSimsIn, m), 1+i );
2443 }
2444 pMini = Exa4_ManGenTest( vSimsIn, vSimsOut, 3, 4, 2, pPars->nNodes, pPars->RuntimeLim, pPars->fOnlyAnd, pPars->fFewerVars, pPars->fOrderNodes, pPars->fUniqFans, pPars->fVerbose, 0, pPars->pGuide );
2445 if ( pMini ) Mini_AigStop( pMini );
2446 Vec_WrdFree( vSimsIn );
2447 Vec_WrdFree( vSimsOut );
2448}
Here is the call graph for this function:

◆ Exa_ManExactSynthesis4Vars()

void Exa_ManExactSynthesis4Vars ( )

Definition at line 3099 of file bmcMaj.c.

3100{
3101 int i, k, nFuncs = 1 << 15;
3102 Vec_Wrd_t * vRes = Vec_WrdAlloc( nFuncs );
3103 Vec_WrdPush( vRes, 0 );
3104 for ( i = 1; i < nFuncs; i++ )
3105 {
3106 word Res = 0;
3107 printf( "\nFunction %d:\n", i );
3108 for ( k = 1; k < 8; k++ )
3109 if ( (Res = Exa_ManExactSynthesis4VarsOne( i, i, k )) )
3110 break;
3111 assert( Res );
3112 Vec_WrdPush( vRes, Res );
3113 }
3114 Vec_WrdDumpBin( "minxaig4.data", vRes, 1 );
3115 Vec_WrdFree( vRes );
3116}
Exa_ManExactSynthesis4VarsOne
word Exa_ManExactSynthesis4VarsOne(int Index, int Truth, int nNodes)
Definition bmcMaj.c:3060
Here is the call graph for this function:

◆ Exa_ManExactSynthesis4VarsOne()

word Exa_ManExactSynthesis4VarsOne ( int Index,
int Truth,
int nNodes )

Definition at line 3060 of file bmcMaj.c.

3061{
3062 Mini_Aig_t * pMini = NULL;
3063 int i, m, nMints = 16, fCompl = 0;
3064 Vec_Wrd_t * vSimsIn = Vec_WrdStart( nMints );
3065 Vec_Wrd_t * vSimsOut = Vec_WrdStart( nMints );
3066 word pTruth[16] = { Abc_Tt6Stretch((word)Truth, 4) };
3067 if ( pTruth[0] & 1 ) { fCompl = 1; Abc_TtNot( pTruth, 1 ); }
3068 for ( m = 0; m < nMints; m++ )
3069 {
3070 Abc_TtSetBit( Vec_WrdEntryP(vSimsOut, m), Abc_TtGetBit(pTruth, m) );
3071 for ( i = 0; i < 4; i++ )
3072 if ( (m >> i) & 1 )
3073 Abc_TtSetBit( Vec_WrdEntryP(vSimsIn, m), 1+i );
3074 }
3075 assert( Vec_WrdSize(vSimsIn) == 16 );
3076 pMini = Exa5_ManGenTest( vSimsIn, vSimsOut, 4, 5, 1, nNodes, 0, 0, 0, 0, 0, 0 );
3077 if ( pMini && fCompl ) Mini_AigFlipLastPo( pMini );
3078 Vec_WrdFree( vSimsIn );
3079 Vec_WrdFree( vSimsOut );
3080 if ( pMini )
3081 {
3082 /*
3083 FILE * pTable = fopen( "min_xaig4.txt", "a+" );
3084 Mini_AigPrintArray( pTable, pMini );
3085 fprintf( pTable, ", // %d : 0x%04x (%d)\n", Index, Truth, nNodes );
3086 fclose( pTable );
3087 */
3088 word Res = Mini_AigWriteEntry( pMini );
3089 int uTruth = 0xFFFF & (int)Abc_TtConvertEntry( Res );
3090 if ( uTruth == Truth )
3091 printf( "Check ok.\n" );
3092 else
3093 printf( "Check NOT ok!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\n" );
3094 Mini_AigStop( pMini );
3095 return Res;
3096 }
3097 return 0;
3098}
Abc_TtConvertEntry
word Abc_TtConvertEntry(word Res)
Definition bmcMaj.c:3027
Mini_AigWriteEntry
word Mini_AigWriteEntry(Mini_Aig_t *p)
Definition bmcMaj.c:3000
Exa5_ManGenTest
Mini_Aig_t * Exa5_ManGenTest(Vec_Wrd_t *vSimsIn, Vec_Wrd_t *vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, int TimeOut, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fVerbose)
Definition bmcMaj.c:2926
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Exa_ManExactSynthesis5()

void Exa_ManExactSynthesis5 ( Bmc_EsPar_t * pPars)

Definition at line 2953 of file bmcMaj.c.

2954{
2955 Mini_Aig_t * pMini = NULL;
2956 int i, m, nMints = 1 << pPars->nVars, fCompl = 0;
2957 Vec_Wrd_t * vSimsIn = Vec_WrdStart( nMints );
2958 Vec_Wrd_t * vSimsOut = Vec_WrdStart( nMints );
2959 word pTruth[16]; Abc_TtReadHex( pTruth, pPars->pTtStr );
2960 if ( pTruth[0] & 1 ) { fCompl = 1; Abc_TtNot( pTruth, Abc_TtWordNum(pPars->nVars) ); }
2961 assert( pPars->nVars <= 10 );
2962 for ( m = 0; m < nMints; m++ )
2963 {
2964 Abc_TtSetBit( Vec_WrdEntryP(vSimsOut, m), Abc_TtGetBit(pTruth, m) );
2965 for ( i = 0; i < pPars->nVars; i++ )
2966 if ( (m >> i) & 1 )
2967 Abc_TtSetBit( Vec_WrdEntryP(vSimsIn, m), 1+i );
2968 }
2969 assert( Vec_WrdSize(vSimsIn) == (1 << pPars->nVars) );
2970 pMini = Exa5_ManGenTest( vSimsIn, vSimsOut, pPars->nVars, 1+pPars->nVars, 1, pPars->nNodes, pPars->RuntimeLim, pPars->fOnlyAnd, pPars->fFewerVars, pPars->fOrderNodes, pPars->fUniqFans, pPars->fVerbose );
2971 if ( pMini ) Mini_AigStop( pMini );
2972 if ( fCompl ) printf( "The resulting circuit, if computed, will be complemented.\n" );
2973 Vec_WrdFree( vSimsIn );
2974 Vec_WrdFree( vSimsOut );
2975}
Here is the call graph for this function:

◆ Exa_ManExactSynthesis6()

void Exa_ManExactSynthesis6 ( Bmc_EsPar_t * pPars,
char * pFileName )

Definition at line 3977 of file bmcMaj.c.

3978{
3979 Mini_Aig_t * pMini = NULL;
3980 Vec_Wrd_t * vSimsDiv = NULL, * vSimsOut = NULL;
3981 int i, k, nDivs, nOuts, nVars = 0;
3982 if ( !strcmp(pFileName + strlen(pFileName) - 3, "rel") )
3983 nVars = Exa6_ReadFile( pFileName, &vSimsDiv, &vSimsOut, &nDivs, &nOuts );
3984 else if ( !strcmp(pFileName + strlen(pFileName) - 3, "pla") ) {
3985 Abc_RData_t * p = Abc_ReadPla( pFileName );
3986 Abc_RData_t * p2 = p ? Abc_RData2Rel( p ) : NULL;
3987 if ( !p || !p2 ) return;
3988 nDivs = 0;
3989 nOuts = p->nOuts;
3990 nVars = p->nIns;
3991 vSimsDiv = Vec_WrdStart( p2->nPats );
3992 for ( k = 0; k < p->nIns; k++ )
3993 for ( i = 0; i < p2->nPats; i++ )
3994 if ( Abc_RDataGetIn(p2, k, i) )
3995 Abc_InfoSetBit((unsigned *)Vec_WrdEntryP(vSimsDiv, i), 1+k);
3996 vSimsOut = Vec_WrdStart( p2->nPats );
3997 for ( k = 0; k < (1 << p->nOuts); k++ )
3998 for ( i = 0; i < p2->nPats; i++ )
3999 if ( Abc_RDataGetOut(p2, k, i) )
4000 Abc_InfoSetBit((unsigned *)Vec_WrdEntryP(vSimsOut, i), k);
4001 Abc_RDataStop( p );
4002 Abc_RDataStop( p2 );
4003 }
4004 else
4005 printf( "Unknown file extension in file \"%s\".\n", pFileName );
4006 if ( nVars == 0 )
4007 return;
4008 //Vec_WrdPrintBin( vSimsDiv, 1 );
4009 //Vec_WrdPrintBin( vSimsOut, 1 );
4010 Exa6_SortSims( vSimsDiv, vSimsOut );
4011 pMini = Exa_ManExactSynthesis6Int( vSimsDiv, vSimsOut, nVars, nDivs, nOuts, pPars->nNodes, pPars->fOnlyAnd, pPars->fVerbose, pFileName );
4012 Vec_WrdFreeP( &vSimsDiv );
4013 Vec_WrdFreeP( &vSimsOut );
4014 if ( pMini ) Mini_AigStop( pMini );
4015}
Exa_ManExactSynthesis6Int
Mini_Aig_t * Exa_ManExactSynthesis6Int(Vec_Wrd_t *vSimsDiv, Vec_Wrd_t *vSimsOut, int nVars, int nDivs, int nOuts, int nNodes, int fOnlyAnd, int fVerbose, char *pFileName)
Definition bmcMaj.c:3945
Exa6_ReadFile
int Exa6_ReadFile(char *pFileName, Vec_Wrd_t **pvSimsDiv, Vec_Wrd_t **pvSimsOut, int *pnDivs, int *pnOuts)
Definition bmcMaj.c:3164
Exa6_SortSims
void Exa6_SortSims(Vec_Wrd_t *vSimsDiv, Vec_Wrd_t *vSimsOut)
Definition bmcMaj.c:3130
Abc_RData_t
typedefABC_NAMESPACE_HEADER_START struct Abc_RData_t_ Abc_RData_t
INCLUDES ///.
Definition ioResub.h:40
strlen
int strlen()
strcmp
int strcmp()
Here is the call graph for this function:

◆ Exa_ManExactSynthesis6_()

void Exa_ManExactSynthesis6_ ( Bmc_EsPar_t * pPars,
char * pFileName )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 3321 of file bmcMaj.c.

3322{
3323 Vec_Wrd_t * vSimsDiv = NULL, * vSimsOut = NULL;
3324 word Entry, Truths[100] = { 0x96, 0xE8 };
3325// int i, nVars = 3, nOuts = 2;
3326// int i, nVars = 6, nOuts = 3;
3327 int i, nVars = 4, nOuts = 4, nDivs2, nOuts2;
3328// Exa6_GenCount( Truths, nVars );
3329 Exa6_GenProd( Truths, nVars );
3330 Exa6_WriteFile( pFileName, nVars, Truths, nOuts );
3331
3332 nVars = Exa6_ReadFile( pFileName, &vSimsDiv, &vSimsOut, &nDivs2, &nOuts2 );
3333
3334 Vec_WrdForEachEntry( vSimsDiv, Entry, i )
3335 Abc_TtPrintBits( &Entry, 1 + nVars );
3336 printf( "\n" );
3337 Vec_WrdForEachEntry( vSimsOut, Entry, i )
3338 Abc_TtPrintBits( &Entry, 1 << nOuts );
3339 printf( "\n" );
3340
3341 Vec_WrdFree( vSimsDiv );
3342 Vec_WrdFree( vSimsOut );
3343}
Exa6_WriteFile
void Exa6_WriteFile(char *pFileName, int nVars, word *pTruths, int nTruths)
Definition bmcMaj.c:3242
Exa6_GenProd
void Exa6_GenProd(word *pTruths, int nVars)
Definition bmcMaj.c:3293
Here is the call graph for this function:

◆ Exa_ManExactSynthesis6Int()

Mini_Aig_t * Exa_ManExactSynthesis6Int ( Vec_Wrd_t * vSimsDiv,
Vec_Wrd_t * vSimsOut,
int nVars,
int nDivs,
int nOuts,
int nNodes,
int fOnlyAnd,
int fVerbose,
char * pFileName )

Definition at line 3945 of file bmcMaj.c.

3946{
3947 Mini_Aig_t * pTemp, * pMini;
3948 Vec_Wrd_t * vSimsDiv2, * vSimsOut2;
3949 int DivCompl, OutCompl;
3950 if ( nVars == 0 ) return NULL;
3951 assert( nVars <= 8 );
3952 DivCompl = (int)Vec_WrdEntry(vSimsDiv, 0) >> 1;
3953 OutCompl = Exa6_ManFindPolar( Vec_WrdEntry(vSimsOut, 0), nOuts );
3954 if ( fVerbose )
3955 printf( "Inputs = %d. Divisors = %d. Outputs = %d. Nodes = %d. InP = %d. OutP = %d.\n",
3956 nVars, nDivs, nOuts, nNodes, DivCompl, OutCompl );
3957 vSimsDiv2 = Exa6_ManTransformInputs( vSimsDiv );
3958 vSimsOut2 = Exa6_ManTransformOutputs( vSimsOut, nOuts );
3959 pMini = Exa6_ManGenTest( vSimsDiv2, vSimsOut2, nVars, nDivs, nOuts, nNodes, 0, fOnlyAnd, 0, 0, 0, fVerbose );
3960 if ( pMini )
3961 {
3962 if ( DivCompl || OutCompl )
3963 {
3964 pMini = Mini_AigDupCompl( pTemp = pMini, DivCompl, OutCompl );
3965 Mini_AigStop( pTemp );
3966 }
3967 Mini_AigerWrite( pFileName ? Extra_FileNameGenericAppend(pFileName, "_twoexact.aig") : (char *)"exa6.aig", pMini, 1 );
3968 //if ( nVars <= 6 )
3969 // Exa_ManMiniVerify( pMini, vSimsDiv, vSimsOut );
3970 //printf( "\n" );
3971 //Mini_AigStop( pMini );
3972 }
3973 Vec_WrdFreeP( &vSimsDiv2 );
3974 Vec_WrdFreeP( &vSimsOut2 );
3975 return pMini;
3976}
Exa6_ManTransformInputs
Vec_Wrd_t * Exa6_ManTransformInputs(Vec_Wrd_t *vIns)
Definition bmcMaj.c:3927
Exa6_ManGenTest
Mini_Aig_t * Exa6_ManGenTest(Vec_Wrd_t *vSimsIn, Vec_Wrd_t *vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, int TimeOut, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fVerbose)
Definition bmcMaj.c:3849
Exa6_ManTransformOutputs
Vec_Wrd_t * Exa6_ManTransformOutputs(Vec_Wrd_t *vOuts, int nOuts)
Definition bmcMaj.c:3919
Mini_AigDupCompl
Mini_Aig_t * Mini_AigDupCompl(Mini_Aig_t *p, int ComplIns, int ComplOuts)
Definition bmcMaj.c:3875
Extra_FileNameGenericAppend
char * Extra_FileNameGenericAppend(char *pBase, char *pSuffix)
Definition extraUtilFile.c:192
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Exa_ManExactSynthesis7()

void Exa_ManExactSynthesis7 ( Bmc_EsPar_t * pPars,
int GateSize )

Definition at line 4148 of file bmcMaj.c.

4149{
4150 abctime clkTotal = Abc_Clock();
4151 int v, n, nMints = 1 << pPars->nVars;
4152 int nV = pPars->nVars + pPars->nNodes;
4153 word pTruth[16]; Abc_TtReadHex( pTruth, pPars->pTtStr );
4154 Vec_Int_t * vValues = NULL;
4155 int Rand = ((((unsigned)rand()) << 12) ^ ((unsigned)rand())) & 0xFFFFF;
4156 char pFileNameIn[32]; sprintf( pFileNameIn, "_%05x_.cnf", Rand );
4157 char pFileNameOut[32]; sprintf( pFileNameOut, "_%05x_.out", Rand );
4158 int nClas = Exa7_ManGenCnf( pFileNameIn, pTruth, pPars->nVars, pPars->nNodes, GateSize );
4159 if ( pPars->fVerbose )
4160 printf( "CNF with %d variables and %d clauses was dumped into file \"%s\".\n", nMints * nV * nV, nClas, pFileNameIn );
4161 vValues = Exa4_ManSolve( pFileNameIn, pFileNameOut, pPars->RuntimeLim, pPars->fVerbose );
4162 if ( pPars->fVerbose && vValues ) {
4163 printf( " " );
4164 for ( n = 0; n < nV; n++ )
4165 printf( "%2d ", n );
4166 printf( "\n" );
4167 for ( n = pPars->nVars; n < nV; n++, printf("\n") ) {
4168 printf( "%2d : ", n );
4169 for ( v = 0; v < n; v++ )
4170 printf( " %c ", Vec_IntEntry(vValues, Exa7_GetVar(nV, v, n, 0)) ? '1':'.' ); // v < n
4171 }
4172 }
4173 if ( vValues )
4174 Exa_ManDumpVerilog( vValues, pPars->nVars, pPars->nNodes, GateSize, pTruth );
4175 Vec_IntFreeP( &vValues );
4176 unlink( pFileNameIn );
4177 Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
4178}
Exa7_ManGenCnf
int Exa7_ManGenCnf(char *pFileName, word *pTruth, int nVars, int nNodes, int GateSize)
Definition bmcMaj.c:4064
Exa_ManDumpVerilog
void Exa_ManDumpVerilog(Vec_Int_t *vValues, int nVars, int nNodes, int GateSize, word *pTruth)
Definition bmcMaj.c:4119
Here is the call graph for this function:

◆ Exa_ManFree()

void Exa_ManFree ( Exa_Man_t * p)

Definition at line 527 of file bmcMaj.c.

528{
529 if ( p->pFile )
530 {
531 char Buffer[1000];
532 sprintf( Buffer, "%s_%d_%d.cnf", p->pPars->pTtStr, 2, p->nNodes );
533 rewind( p->pFile );
534 fprintf( p->pFile, "p cnf %d %d", bmcg_sat_solver_varnum(p->pSat), p->nCnfClauses );
535 fclose( p->pFile );
536 printf( "CNF was dumped into file \"%s\".\n", Buffer );
537 }
538 bmcg_sat_solver_stop( p->pSat );
539 Vec_WrdFree( p->vInfo );
540 Vec_WecFree( p->vOutLits );
541 ABC_FREE( p );
542}
bmcg_sat_solver_stop
void bmcg_sat_solver_stop(bmcg_sat_solver *s)
Definition AbcGlucose.cpp:150
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Exa_ManIsNormalized()

void Exa_ManIsNormalized ( Vec_Wrd_t * vSimsIn,
Vec_Wrd_t * vSimsOut )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1702 of file bmcMaj.c.

1703{
1704 int i, Count = 0; word Temp;
1705 Vec_WrdForEachEntry( vSimsIn, Temp, i )
1706 if ( Temp & 1 )
1707 Count++;
1708 if ( Count )
1709 printf( "The data for %d divisors are not normalized.\n", Count );
1710 if ( !(Vec_WrdEntry(vSimsOut, 0) & 1) )
1711 printf( "The output data is not normalized.\n" );
1712// else if ( Count == 0 )
1713// printf( "The data is fully normalized.\n" );
1714}
Here is the caller graph for this function:

◆ Exa_ManMarkup()

int Exa_ManMarkup ( Exa_Man_t * p)

Definition at line 462 of file bmcMaj.c.

463{
464 int i, k, j;
465 assert( p->nObjs <= MAJ_NOBJS );
466 // assign functionality
467 p->iVar = 1 + 3*p->nNodes;//
468 // assign connectivity variables
469 for ( i = p->nVars; i < p->nObjs; i++ )
470 {
471 for ( k = 0; k < 2; k++ )
472 {
473 if ( p->pPars->fFewerVars && i == p->nObjs - 1 && k == 0 )
474 {
475 j = p->nObjs - 2;
476 Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) );
477 p->VarMarks[i][k][j] = p->iVar++;
478 continue;
479 }
480 for ( j = p->pPars->fFewerVars ? 1 - k : 0; j < i - k; j++ )
481 {
482 Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) );
483 p->VarMarks[i][k][j] = p->iVar++;
484 }
485 }
486 }
487 printf( "The number of parameter variables = %d.\n", p->iVar );
488 return p->iVar;
489 // printout
490 for ( i = p->nVars; i < p->nObjs; i++ )
491 {
492 printf( "Node %d\n", i );
493 for ( j = 0; j < p->nObjs; j++ )
494 {
495 for ( k = 0; k < 2; k++ )
496 printf( "%3d ", p->VarMarks[i][k][j] );
497 printf( "\n" );
498 }
499 }
500 return p->iVar;
501}
Here is the caller graph for this function:

◆ Exa_ManMiniPrint()

void Exa_ManMiniPrint ( Mini_Aig_t * p,
int nIns )

Definition at line 1726 of file bmcMaj.c.

1727{
1728 int i, nDivs = 1 + Mini_AigPiNum(p), nNodes = Mini_AigAndNum(p);
1729 printf( "This %d-var function (%d divisors) has %d gates (%d xor) and %d levels:\n",
1730 nIns, nDivs, nNodes, Mini_AigXorNum(p), Mini_AigLevelNum(p) );
1731 for ( i = nDivs + nNodes; i < Mini_AigNodeNum(p); i++ )
1732 {
1733 int Lit0 = Mini_AigNodeFanin0( p, i );
1734 printf( "%2d = ", i );
1735 Exa_ManPrintFanin( nIns, nDivs, Abc_Lit2Var(Lit0), Abc_LitIsCompl(Lit0) );
1736 printf( "\n" );
1737 }
1738 for ( i = nDivs + nNodes - 1; i >= nDivs; i-- )
1739 {
1740 int Lit0 = Mini_AigNodeFanin0( p, i );
1741 int Lit1 = Mini_AigNodeFanin1( p, i );
1742 printf( "%2d = ", i );
1743 if ( Lit0 < Lit1 )
1744 {
1745 Exa_ManPrintFanin( nIns, nDivs, Abc_Lit2Var(Lit0), Abc_LitIsCompl(Lit0) );
1746 printf( " &" );
1747 Exa_ManPrintFanin( nIns, nDivs, Abc_Lit2Var(Lit1), Abc_LitIsCompl(Lit1) );
1748 }
1749 else
1750 {
1751 Exa_ManPrintFanin( nIns, nDivs, Abc_Lit2Var(Lit1), Abc_LitIsCompl(Lit1) );
1752 printf( " ^" );
1753 Exa_ManPrintFanin( nIns, nDivs, Abc_Lit2Var(Lit0), Abc_LitIsCompl(Lit0) );
1754 }
1755 printf( "\n" );
1756 }
1757}
Here is the caller graph for this function:

◆ Exa_ManMiniVerify()

void Exa_ManMiniVerify ( Mini_Aig_t * p,
Vec_Wrd_t * vSimsIn,
Vec_Wrd_t * vSimsOut )

Definition at line 1758 of file bmcMaj.c.

1759{
1760 extern void Extra_BitMatrixTransposeP( Vec_Wrd_t * vSimsIn, int nWordsIn, Vec_Wrd_t * vSimsOut, int nWordsOut );
1761 int i, nDivs = 1 + Mini_AigPiNum(p), nNodes = Mini_AigAndNum(p);
1762 int k, nOuts = Mini_AigPoNum(p), nErrors = 0; word Outs[6] = {0};
1763 Vec_Wrd_t * vSimsIn2 = Vec_WrdStart( 64 );
1764 assert( nOuts <= 6 );
1765 assert( Vec_WrdSize(vSimsIn) <= 64 );
1766 assert( Vec_WrdSize(vSimsIn) == Vec_WrdSize(vSimsOut) );
1767 Vec_WrdFillExtra( vSimsIn, 64, 0 );
1768 Extra_BitMatrixTransposeP( vSimsIn, 1, vSimsIn2, 1 );
1769 assert( Mini_AigNodeNum(p) <= 64 );
1770 for ( i = nDivs; i < nDivs + nNodes; i++ )
1771 {
1772 int Lit0 = Mini_AigNodeFanin0( p, i );
1773 int Lit1 = Mini_AigNodeFanin1( p, i );
1774 word Sim0 = Vec_WrdEntry( vSimsIn2, Abc_Lit2Var(Lit0) );
1775 word Sim1 = Vec_WrdEntry( vSimsIn2, Abc_Lit2Var(Lit1) );
1776 Sim0 = Abc_LitIsCompl(Lit0) ? ~Sim0 : Sim0;
1777 Sim1 = Abc_LitIsCompl(Lit1) ? ~Sim1 : Sim1;
1778 Vec_WrdWriteEntry( vSimsIn2, i, Lit0 < Lit1 ? Sim0 & Sim1 : Sim0 ^ Sim1 );
1779 }
1780 for ( i = nDivs + nNodes; i < Mini_AigNodeNum(p); i++ )
1781 {
1782 int Lit0 = Mini_AigNodeFanin0( p, i );
1783 word Sim0 = Vec_WrdEntry( vSimsIn2, Abc_Lit2Var(Lit0) );
1784 Outs[i - (nDivs + nNodes)] = Abc_LitIsCompl(Lit0) ? ~Sim0 : Sim0;
1785 }
1786 Vec_WrdFree( vSimsIn2 );
1787 for ( i = 0; i < Vec_WrdSize(vSimsOut); i++ )
1788 {
1789 int iOutMint = 0;
1790 for ( k = 0; k < nOuts; k++ )
1791 if ( (Outs[k] >> i) & 1 )
1792 iOutMint |= 1 << k;
1793 nErrors += !Abc_TtGetBit(Vec_WrdEntryP(vSimsOut, i), iOutMint);
1794 }
1795 if ( nErrors == 0 )
1796 printf( "Verification successful. " );
1797 else
1798 printf( "Verification failed for %d (out of %d) minterms.\n", nErrors, Vec_WrdSize(vSimsOut) );
1799}
Extra_BitMatrixTransposeP
ABC_NAMESPACE_IMPL_START void Extra_BitMatrixTransposeP(Vec_Wrd_t *vSimsIn, int nWordsIn, Vec_Wrd_t *vSimsOut, int nWordsOut)
DECLARATIONS ///.
Definition extraUtilMisc.c:2652
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Exa_ManPrintSolution()

void Exa_ManPrintSolution ( Exa_Man_t * p,
int fCompl )

Definition at line 659 of file bmcMaj.c.

660{
661 int i, k, iVar;
662 printf( "Realization of given %d-input function using %d two-input gates:\n", p->nVars, p->nNodes );
663// for ( i = p->nVars + 2; i < p->nObjs; i++ )
664 for ( i = p->nObjs - 1; i >= p->nVars; i-- )
665 {
666 int iVarStart = 1 + 3*(i - p->nVars);//
667 int Val1 = bmcg_sat_solver_read_cex_varvalue(p->pSat, iVarStart);
668 int Val2 = bmcg_sat_solver_read_cex_varvalue(p->pSat, iVarStart+1);
669 int Val3 = bmcg_sat_solver_read_cex_varvalue(p->pSat, iVarStart+2);
670 if ( i == p->nObjs - 1 && fCompl )
671 printf( "%02d = 4\'b%d%d%d1(", i, !Val3, !Val2, !Val1 );
672 else
673 printf( "%02d = 4\'b%d%d%d0(", i, Val3, Val2, Val1 );
674 for ( k = 1; k >= 0; k-- )
675 {
676 iVar = Exa_ManFindFanin( p, i, k );
677 if ( iVar >= 0 && iVar < p->nVars )
678 printf( " %c", 'a'+iVar );
679 else
680 printf( " %02d", iVar );
681 }
682 printf( " )\n" );
683 }
684}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Exa_ManSolverSolve()

int Exa_ManSolverSolve ( Exa_Man_t * p)

Definition at line 749 of file bmcMaj.c.

750{
751 int nAdded = 1;
752 while ( nAdded )
753 {
754 int status = bmcg_sat_solver_solve( p->pSat, NULL, 0 );
755 if ( status != GLUCOSE_SAT )
756 return status;
757 status = Exa_ManAddCnfAdd( p, &nAdded );
758 //printf( "Added %d clauses.\n", nAdded );
759 if ( status != GLUCOSE_SAT )
760 return status;
761 }
762 return GLUCOSE_SAT;
763}
Exa_ManAddCnfAdd
int Exa_ManAddCnfAdd(Exa_Man_t *p, int *pnAdded)
Definition bmcMaj.c:710
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Exa_ManTruthTables()

Vec_Wrd_t * Exa_ManTruthTables ( Exa_Man_t * p)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 454 of file bmcMaj.c.

455{
456 Vec_Wrd_t * vInfo = p->vInfo = Vec_WrdStart( p->nWords * (p->nObjs+1) ); int i;
457 for ( i = 0; i < p->nVars; i++ )
458 Abc_TtIthVar( Exa_ManTruth(p, i), i, p->nVars );
459 //Dau_DsdPrintFromTruth( Exa_ManTruth(p, p->nObjs), p->nVars );
460 return vInfo;
461}
Here is the caller graph for this function:

◆ Exa_NpnCascadeTest()

void Exa_NpnCascadeTest ( )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 4191 of file bmcMaj.c.

4192{
4193 char Buffer[100];
4194 char Command[1000]; int i;
4195 FILE * pFile = fopen( "npn3.txt", "r" );
4196 for ( i = 0; i < 14; i++ )
4197// FILE * pFile = fopen( "npn4.txt", "r" );
4198// for ( i = 0; i < 222; i++ )
4199// FILE * pFile = fopen( "npn5.txt", "r" );
4200// for ( i = 0; i < 616126; i++ )
4201 {
4202 int Value = fscanf( pFile, "%s", Buffer );
4203 assert( Value == 1 );
4204 if ( i == 0 ) continue;
4205 if ( Buffer[strlen(Buffer)-1] == '\n' )
4206 Buffer[strlen(Buffer)-1] = '\0';
4207 if ( Buffer[strlen(Buffer)-1] == '\r' )
4208 Buffer[strlen(Buffer)-1] = '\0';
4209 sprintf( Command, "lutexact -I 3 -N 2 -K 2 -gvc %s", Buffer+2 );
4210 printf( "\nNPN class %6d : Command \"%s\":\n", i, Command );
4211 if ( Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), Command ) )
4212 {
4213 fprintf( stdout, "Cannot execute command \"%s\".\n", Command );
4214 return;
4215 }
4216 }
4217 fclose( pFile );
4218}
Abc_FrameGetGlobalFrame
ABC_DLL Abc_Frame_t * Abc_FrameGetGlobalFrame()
Definition mainFrame.c:643
Cmd_CommandExecute
ABC_DLL int Cmd_CommandExecute(Abc_Frame_t *pAbc, const char *sCommand)
Definition cmdApi.c:193
Here is the call graph for this function:

◆ Exa_NpnCascadeTest6()

void Exa_NpnCascadeTest6 ( )

Definition at line 4219 of file bmcMaj.c.

4220{
4221 char Command[1000]; int i;
4222 Abc_Random(1);
4223 for ( i = 0; i < 10000; i++ )
4224 {
4225 word Truth = Abc_RandomW(0);
4226 sprintf( Command, "lutexact -I 6 -N 2 -K 5 -gvc %016lx", Truth );
4227 printf( "\nIter %4d : Command \"%s\":\n", i, Command );
4228 if ( Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), Command ) )
4229 {
4230 fprintf( stdout, "Cannot execute command \"%s\".\n", Command );
4231 return;
4232 }
4233 }
4234}
Here is the call graph for this function:

◆ Gia_ManDupMini()

Gia_Man_t * Gia_ManDupMini ( Gia_Man_t * p,
Vec_Int_t * vIns,
Vec_Int_t * vDivs,
Vec_Int_t * vOuts,
Mini_Aig_t * pMini )

Definition at line 3368 of file bmcMaj.c.

3369{
3370 Gia_Man_t * pNew;
3371 Gia_Obj_t * pObj; int i, k;
3372 Vec_Int_t * vCopies = Vec_IntStartFull( Mini_AigNodeNum(pMini) );
3373 //int nPis = Mini_AigPiNum(pMini);
3374 Vec_IntWriteEntry( vCopies, 0, 0 );
3375 assert( Mini_AigPiNum(pMini) == Vec_IntSize(vIns)+Vec_IntSize(vDivs) );
3376 assert( Mini_AigPoNum(pMini) == Vec_IntSize(vOuts) );
3377 Gia_ManFillValue( p );
3378 pNew = Gia_ManStart( Gia_ManObjNum(p) );
3379 pNew->pName = Abc_UtilStrsav( p->pName );
3380 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
3381 Gia_ManConst0(p)->Value = 0;
3382 Gia_ManForEachCi( p, pObj, i )
3383 pObj->Value = Gia_ManAppendCi(pNew);
3384 Gia_ManForEachObjVec( vIns, p, pObj, i )
3385 Vec_IntWriteEntry( vCopies, 1+i, Gia_ManDupMini_rec(pNew, p, pObj) );
3386 Gia_ManForEachObjVec( vDivs, p, pObj, i )
3387 Vec_IntWriteEntry( vCopies, 1+Vec_IntSize(vIns)+i, Gia_ManDupMini_rec(pNew, p, pObj) );
3388 Mini_AigForEachAnd( pMini, k )
3389 {
3390 int iFaninLit0 = Mini_AigNodeFanin0( pMini, k );
3391 int iFaninLit1 = Mini_AigNodeFanin1( pMini, k );
3392 int iLit0 = Vec_IntEntry(vCopies, Mini_AigLit2Var(iFaninLit0)) ^ Mini_AigLitIsCompl(iFaninLit0);
3393 int iLit1 = Vec_IntEntry(vCopies, Mini_AigLit2Var(iFaninLit1)) ^ Mini_AigLitIsCompl(iFaninLit1);
3394 if ( iFaninLit0 < iFaninLit1 )
3395 Vec_IntWriteEntry( vCopies, k, Gia_ManAppendAnd(pNew, iLit0, iLit1) );
3396 else
3397 Vec_IntWriteEntry( vCopies, k, Gia_ManAppendXorReal(pNew, iLit0, iLit1) );
3398 }
3399 i = 0;
3400 Mini_AigForEachPo( pMini, k )
3401 {
3402 int iFaninLit0 = Mini_AigNodeFanin0( pMini, k );
3403 int iLit0 = Vec_IntEntry(vCopies, Mini_AigLit2Var(iFaninLit0)) ^ Mini_AigLitIsCompl(iFaninLit0);
3404 Gia_ManObj( p, Vec_IntEntry(vOuts, i++) )->Value = iLit0;
3405 }
3406 Gia_ManForEachCo( p, pObj, i )
3407 Gia_ManDupMini_rec( pNew, p, Gia_ObjFanin0(pObj) );
3408 Gia_ManForEachCo( p, pObj, i )
3409 Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
3410 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
3411 Vec_IntFree( vCopies );
3412 return pNew;
3413}
Gia_ManDupMini_rec
int Gia_ManDupMini_rec(Gia_Man_t *pNew, Gia_Man_t *p, Gia_Obj_t *pObj)
Definition bmcMaj.c:3359
Gia_ManSetRegNum
void Gia_ManSetRegNum(Gia_Man_t *p, int nRegs)
Definition giaMan.c:764
Gia_ManStart
Gia_Man_t * Gia_ManStart(int nObjsMax)
FUNCTION DEFINITIONS ///.
Definition giaMan.c:57
Gia_Obj_t
struct Gia_Obj_t_ Gia_Obj_t
Definition gia.h:76
Gia_ManFillValue
void Gia_ManFillValue(Gia_Man_t *p)
Definition giaUtil.c:369
Gia_Man_t
struct Gia_Man_t_ Gia_Man_t
Definition gia.h:96
Gia_ManForEachObjVec
#define Gia_ManForEachObjVec(vVec, p, pObj, i)
Definition gia.h:1194
Gia_ManForEachCo
#define Gia_ManForEachCo(p, pObj, i)
Definition gia.h:1236
Gia_ManForEachCi
#define Gia_ManForEachCi(p, pObj, i)
Definition gia.h:1228
Mini_AigForEachPo
#define Mini_AigForEachPo(p, i)
Definition miniaig.h:139
Mini_AigForEachAnd
#define Mini_AigForEachAnd(p, i)
Definition miniaig.h:140
Gia_Man_t_::pSpec
char * pSpec
Definition gia.h:100
Gia_Man_t_::pName
char * pName
Definition gia.h:99
Gia_Obj_t_::Value
unsigned Value
Definition gia.h:89
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Gia_ManDupMini_rec()

int Gia_ManDupMini_rec ( Gia_Man_t * pNew,
Gia_Man_t * p,
Gia_Obj_t * pObj )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 3359 of file bmcMaj.c.

3360{
3361 if ( ~pObj->Value )
3362 return pObj->Value;
3363 assert( Gia_ObjIsAnd(pObj) );
3364 Gia_ManDupMini_rec( pNew, p, Gia_ObjFanin0(pObj) );
3365 Gia_ManDupMini_rec( pNew, p, Gia_ObjFanin1(pObj) );
3366 return pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
3367}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Maj_ManAddCnf()

int Maj_ManAddCnf ( Maj_Man_t * p,
int iMint )

Definition at line 325 of file bmcMaj.c.

326{
327 // save minterm values
328 int i, k, n, j, Value = Maj_ManValue(iMint, p->nVars);
329 for ( i = 0; i < p->nVars; i++ )
330 p->VarVals[i+2] = (iMint >> i) & 1;
331 bmcg_sat_solver_set_nvars( p->pSat, p->iVar + 4*p->nNodes );
332 //printf( "Adding clauses for minterm %d.\n", iMint );
333 for ( i = p->nVars + 2; i < p->nObjs; i++ )
334 {
335 // fanin connectivity
336 int iBaseSatVarI = p->iVar + 4*(i - p->nVars - 2);
337 for ( k = 0; k < 3; k++ )
338 {
339 for ( j = 0; j < p->nObjs; j++ ) if ( p->VarMarks[i][k][j] )
340 {
341 int iBaseSatVarJ = p->iVar + 4*(j - p->nVars - 2);
342 for ( n = 0; n < 2; n++ )
343 {
344 int pLits[3], nLits = 0;
345 pLits[nLits++] = Abc_Var2Lit( p->VarMarks[i][k][j], 1 );
346 pLits[nLits++] = Abc_Var2Lit( iBaseSatVarI + k, n );
347 if ( j >= p->nVars + 2 )
348 pLits[nLits++] = Abc_Var2Lit( iBaseSatVarJ + 3, !n );
349 else if ( p->VarVals[j] == n )
350 continue;
351 if ( !bmcg_sat_solver_addclause( p->pSat, pLits, nLits ) )
352 return 0;
353 }
354 }
355 }
356 // node functionality
357 for ( n = 0; n < 2; n++ )
358 {
359 if ( i == p->nObjs - 1 && n == Value )
360 continue;
361 for ( k = 0; k < 3; k++ )
362 {
363 int pLits[3], nLits = 0;
364 if ( k != 0 ) pLits[nLits++] = Abc_Var2Lit( iBaseSatVarI + 0, n );
365 if ( k != 1 ) pLits[nLits++] = Abc_Var2Lit( iBaseSatVarI + 1, n );
366 if ( k != 2 ) pLits[nLits++] = Abc_Var2Lit( iBaseSatVarI + 2, n );
367 if ( i != p->nObjs - 1 ) pLits[nLits++] = Abc_Var2Lit( iBaseSatVarI + 3, !n );
368 assert( nLits <= 3 );
369 if ( !bmcg_sat_solver_addclause( p->pSat, pLits, nLits ) )
370 return 0;
371 }
372 }
373 }
374 p->iVar += 4*p->nNodes;
375 return 1;
376}
bmcg_sat_solver_addclause
int bmcg_sat_solver_addclause(bmcg_sat_solver *s, int *plits, int nlits)
Definition AbcGlucose.cpp:160
Maj_ManValue
int Maj_ManValue(int iMint, int nVars)
FUNCTION DEFINITIONS ///.
Definition bmcMaj.c:80
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Maj_ManAddCnfStart()

int Maj_ManAddCnfStart ( Maj_Man_t * p)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 278 of file bmcMaj.c.

279{
280 int pLits[MAJ_NOBJS], pLits2[2], i, j, k, n, m;
281 // input constraints
282 for ( i = p->nVars + 2; i < p->nObjs; i++ )
283 {
284 for ( k = 0; k < 3; k++ )
285 {
286 int nLits = 0;
287 for ( j = 0; j < p->nObjs; j++ )
288 if ( p->VarMarks[i][k][j] )
289 pLits[nLits++] = Abc_Var2Lit( p->VarMarks[i][k][j], 0 );
290 assert( nLits > 0 );
291 // input uniqueness
292 if ( !bmcg_sat_solver_addclause( p->pSat, pLits, nLits ) )
293 return 0;
294 for ( n = 0; n < nLits; n++ )
295 for ( m = n+1; m < nLits; m++ )
296 {
297 pLits2[0] = Abc_LitNot(pLits[n]);
298 pLits2[1] = Abc_LitNot(pLits[m]);
299 if ( !bmcg_sat_solver_addclause( p->pSat, pLits2, 2 ) )
300 return 0;
301 }
302 if ( k == 2 )
303 break;
304 // symmetry breaking
305 for ( j = 0; j < p->nObjs; j++ ) if ( p->VarMarks[i][k][j] )
306 for ( n = j; n < p->nObjs; n++ ) if ( p->VarMarks[i][k+1][n] )
307 {
308 pLits2[0] = Abc_Var2Lit( p->VarMarks[i][k][j], 1 );
309 pLits2[1] = Abc_Var2Lit( p->VarMarks[i][k+1][n], 1 );
310 if ( !bmcg_sat_solver_addclause( p->pSat, pLits2, 2 ) )
311 return 0;
312 }
313 }
314 }
315 // outputs should be used
316 for ( i = 2; i < p->nObjs - 1; i++ )
317 {
318 Vec_Int_t * vArray = Vec_WecEntry(p->vOutLits, i);
319 assert( Vec_IntSize(vArray) > 0 );
320 if ( !bmcg_sat_solver_addclause( p->pSat, Vec_IntArray(vArray), Vec_IntSize(vArray) ) )
321 return 0;
322 }
323 return 1;
324}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Maj_ManAlloc()

Maj_Man_t * Maj_ManAlloc ( int nVars,
int nNodes,
int fUseConst,
int fUseLine )

Definition at line 147 of file bmcMaj.c.

148{
149 Maj_Man_t * p = ABC_CALLOC( Maj_Man_t, 1 );
150 p->nVars = nVars;
151 p->nNodes = nNodes;
152 p->nObjs = 2 + nVars + nNodes;
153 p->fUseConst = fUseConst;
154 p->fUseLine = fUseLine;
155 p->nWords = Abc_TtWordNum(nVars);
156 p->vOutLits = Vec_WecStart( p->nObjs );
157 p->iVar = Maj_ManMarkup( p );
158 p->VarVals[1] = 1;
159 p->vInfo = Maj_ManTruthTables( p );
160 p->pSat = bmcg_sat_solver_start();
161 bmcg_sat_solver_set_nvars( p->pSat, p->iVar );
162 return p;
163}
Maj_Man_t
struct Maj_Man_t_ Maj_Man_t
Definition bmcMaj.c:46
Maj_ManTruthTables
Vec_Wrd_t * Maj_ManTruthTables(Maj_Man_t *p)
Definition bmcMaj.c:87
Maj_ManMarkup
int Maj_ManMarkup(Maj_Man_t *p)
Definition bmcMaj.c:100
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Maj_ManExactSynthesis()

int Maj_ManExactSynthesis ( int nVars,
int nNodes,
int fUseConst,
int fUseLine,
int fVerbose )

Definition at line 377 of file bmcMaj.c.

378{
379 int i, iMint = 0;
380 abctime clkTotal = Abc_Clock();
381 Maj_Man_t * p = Maj_ManAlloc( nVars, nNodes, fUseConst, fUseLine );
382 int status = Maj_ManAddCnfStart( p );
383 assert( status );
384 printf( "Running exact synthesis for %d-input majority with %d MAJ3 gates...\n", p->nVars, p->nNodes );
385 for ( i = 0; iMint != -1; i++ )
386 {
387 abctime clk = Abc_Clock();
388 if ( !Maj_ManAddCnf( p, iMint ) )
389 break;
390 status = bmcg_sat_solver_solve( p->pSat, NULL, 0 );
391 if ( fVerbose )
392 {
393 printf( "Iter %3d : ", i );
394 Extra_PrintBinary( stdout, (unsigned *)&iMint, p->nVars );
395 printf( " Var =%5d ", p->iVar );
396 printf( "Cla =%6d ", bmcg_sat_solver_clausenum(p->pSat) );
397 printf( "Conf =%9d ", bmcg_sat_solver_conflictnum(p->pSat) );
398 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
399 }
400 if ( status == GLUCOSE_UNSAT )
401 {
402 printf( "The problem has no solution.\n" );
403 break;
404 }
405 iMint = Maj_ManEval( p );
406 }
407 if ( iMint == -1 )
408 Maj_ManPrintSolution( p );
409 Maj_ManFree( p );
410 Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
411 return iMint == -1;
412}
Maj_ManFree
void Maj_ManFree(Maj_Man_t *p)
Definition bmcMaj.c:164
Maj_ManAddCnf
int Maj_ManAddCnf(Maj_Man_t *p, int iMint)
Definition bmcMaj.c:325
Maj_ManAlloc
Maj_Man_t * Maj_ManAlloc(int nVars, int nNodes, int fUseConst, int fUseLine)
Definition bmcMaj.c:147
Maj_ManPrintSolution
void Maj_ManPrintSolution(Maj_Man_t *p)
Definition bmcMaj.c:244
Maj_ManAddCnfStart
int Maj_ManAddCnfStart(Maj_Man_t *p)
Definition bmcMaj.c:278
Here is the call graph for this function:

◆ Maj_ManFree()

void Maj_ManFree ( Maj_Man_t * p)

Definition at line 164 of file bmcMaj.c.

165{
166 bmcg_sat_solver_stop( p->pSat );
167 Vec_WrdFree( p->vInfo );
168 Vec_WecFree( p->vOutLits );
169 ABC_FREE( p );
170}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Maj_ManMarkup()

int Maj_ManMarkup ( Maj_Man_t * p)

Definition at line 100 of file bmcMaj.c.

101{
102 int i, k, j;
103 p->iVar = 1;
104 assert( p->nObjs <= MAJ_NOBJS );
105 // make exception for the first node
106 i = p->nVars + 2;
107 for ( k = 0; k < 3; k++ )
108 {
109 j = 4-k;
110 Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) );
111 p->VarMarks[i][k][j] = p->iVar++;
112 }
113 // assign variables for other nodes
114 for ( i = p->nVars + 3; i < p->nObjs; i++ )
115 {
116 for ( k = 0; k < 3; k++ )
117 {
118 if ( p->fUseLine && k == 0 )
119 {
120 j = i-1;
121 Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) );
122 p->VarMarks[i][k][j] = p->iVar++;
123 continue;
124 }
125 for ( j = (p->fUseConst && k == 2) ? 0 : 2; j < i - k; j++ )
126 {
127 Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) );
128 p->VarMarks[i][k][j] = p->iVar++;
129 }
130 }
131 }
132 printf( "The number of parameter variables = %d.\n", p->iVar );
133 return p->iVar;
134 // printout
135 for ( i = p->nVars + 2; i < p->nObjs; i++ )
136 {
137 printf( "Node %d\n", i );
138 for ( j = 0; j < p->nObjs; j++ )
139 {
140 for ( k = 0; k < 3; k++ )
141 printf( "%3d ", p->VarMarks[i][k][j] );
142 printf( "\n" );
143 }
144 }
145 return p->iVar;
146}
Here is the caller graph for this function:

◆ Maj_ManPrintSolution()

void Maj_ManPrintSolution ( Maj_Man_t * p)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 244 of file bmcMaj.c.

245{
246 int i, k, iVar;
247 printf( "Realization of %d-input majority using %d MAJ3 gates:\n", p->nVars, p->nNodes );
248// for ( i = p->nVars + 2; i < p->nObjs; i++ )
249 for ( i = p->nObjs - 1; i >= p->nVars + 2; i-- )
250 {
251 printf( "%02d = MAJ(", i-2 );
252 for ( k = 2; k >= 0; k-- )
253 {
254 iVar = Maj_ManFindFanin( p, i, k );
255 if ( iVar >= 2 && iVar < p->nVars + 2 )
256 printf( " %c", 'a'+iVar-2 );
257 else if ( iVar < 2 )
258 printf( " %d", iVar );
259 else
260 printf( " %02d", iVar-2 );
261 }
262 printf( " )\n" );
263 }
264}
Here is the caller graph for this function:

◆ Maj_ManTruthTables()

Vec_Wrd_t * Maj_ManTruthTables ( Maj_Man_t * p)

Definition at line 87 of file bmcMaj.c.

88{
89 Vec_Wrd_t * vInfo = p->vInfo = Vec_WrdStart( p->nWords * (p->nObjs + 1) );
90 int i, nMints = Abc_MaxInt( 64, 1 << p->nVars );
91 Abc_TtFill( Maj_ManTruth(p, 1), p->nWords );
92 for ( i = 0; i < p->nVars; i++ )
93 Abc_TtIthVar( Maj_ManTruth(p, i+2), i, p->nVars );
94 for ( i = 0; i < nMints; i++ )
95 if ( Maj_ManValue(i, p->nVars) )
96 Abc_TtSetBit( Maj_ManTruth(p, p->nObjs), i );
97 //Dau_DsdPrintFromTruth( Maj_ManTruth(p, p->nObjs), p->nVars );
98 return vInfo;
99}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Maj_ManValue()

int Maj_ManValue ( int iMint,
int nVars )

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 80 of file bmcMaj.c.

81{
82 int k, Count = 0;
83 for ( k = 0; k < nVars; k++ )
84 Count += (iMint >> k) & 1;
85 return (int)(Count > nVars/2);
86}
Here is the caller graph for this function:

◆ Mini_AigDupCompl()

Mini_Aig_t * Mini_AigDupCompl ( Mini_Aig_t * p,
int ComplIns,
int ComplOuts )

Definition at line 3875 of file bmcMaj.c.

3876{
3877 Mini_Aig_t * pNew = Mini_AigStartSupport( Mini_AigPiNum(p), Mini_AigNodeNum(p) );
3878 Vec_Int_t * vCopies = Vec_IntStartFull( Mini_AigNodeNum(p) ); int k, i = 0, o = 0;
3879 Vec_IntWriteEntry( vCopies, 0, 0 );
3880 Mini_AigForEachPi( p, k )
3881 Vec_IntWriteEntry( vCopies, k, Abc_Var2Lit(k, (ComplIns>>i++) & 1) );
3882 Mini_AigForEachAnd( p, k )
3883 {
3884 int iFaninLit0 = Mini_AigNodeFanin0( p, k );
3885 int iFaninLit1 = Mini_AigNodeFanin1( p, k );
3886 int iLit0 = Vec_IntEntry(vCopies, Mini_AigLit2Var(iFaninLit0)) ^ Mini_AigLitIsCompl(iFaninLit0);
3887 int iLit1 = Vec_IntEntry(vCopies, Mini_AigLit2Var(iFaninLit1)) ^ Mini_AigLitIsCompl(iFaninLit1);
3888 if ( iFaninLit0 < iFaninLit1 )
3889 Vec_IntWriteEntry( vCopies, k, Mini_AigAnd(pNew, iLit0, iLit1) );
3890 else
3891 Vec_IntWriteEntry( vCopies, k, Mini_AigXorSpecial(pNew, iLit0, iLit1) );
3892 }
3893 Mini_AigForEachPo( p, k )
3894 {
3895 int iFaninLit0 = Mini_AigNodeFanin0( p, k );
3896 int iLit0 = Vec_IntEntry(vCopies, Mini_AigLit2Var(iFaninLit0)) ^ Mini_AigLitIsCompl(iFaninLit0);
3897 Mini_AigCreatePo( pNew, iLit0 ^ ((ComplOuts >> o++) & 1) );
3898 }
3899 Vec_IntFree( vCopies );
3900 return pNew;
3901}
Mini_AigForEachPi
#define Mini_AigForEachPi(p, i)
Definition miniaig.h:138
Here is the caller graph for this function:

◆ Mini_AigPrintArray()

void Mini_AigPrintArray ( FILE * pFile,
Mini_Aig_t * p )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 2988 of file bmcMaj.c.

2989{
2990 int i, Count = 0;
2991 fprintf( pFile, " { " );
2992 Mini_AigForEachAnd( p, i )
2993 fprintf( pFile, "%2d,%2d, ", Mini_AigNodeFanin0(p, i), Mini_AigNodeFanin1(p, i) ), Count++;
2994 Mini_AigForEachPo( p, i )
2995 fprintf( pFile, "%2d,%2d", Mini_AigNodeFanin0(p, i), Mini_AigNodeFanin0(p, i) ), Count++;
2996 for ( i = Count; i < 8; i++ )
2997 fprintf( pFile, ", %2d,%2d", 0, 0 );
2998 fprintf( pFile, " }" );
2999}

◆ Mini_AigWriteEntry()

word Mini_AigWriteEntry ( Mini_Aig_t * p)

Definition at line 3000 of file bmcMaj.c.

3001{
3002 word Res = 0; int i, k = 0;
3003 Mini_AigForEachAnd( p, i )
3004 {
3005 int iLit0 = Mini_AigNodeFanin0(p, i);
3006 int iLit1 = Mini_AigNodeFanin1(p, i);
3007 int Pair;
3008 if ( k < 4 )
3009 {
3010 assert( (iLit1 & 0xF) != (iLit0 & 0xF) );
3011 Pair = ((iLit1 & 0xF) << 4) | (iLit0 & 0xF);
3012 Res |= (word)Pair << (k*8);
3013 }
3014 else
3015 {
3016 assert( (iLit1 & 0x1F) != (iLit0 & 0x1F) );
3017 Pair = ((iLit1 & 0x1F) << 5) | (iLit0 & 0x1F);
3018 Res |= (word)Pair << (32 + (k-4)*10);
3019 }
3020 k++;
3021 }
3022 Mini_AigForEachPo( p, i )
3023 if ( Mini_AigNodeFanin0(p, i) & 1 )
3024 Res |= (word)1 << 62;
3025 return Res;
3026}
Here is the caller graph for this function: