ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Classes | Macros | Typedefs | Functions
cnf.h File Reference
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include "misc/vec/vec.h"
#include "aig/aig/aig.h"
#include "opt/dar/darInt.h"
Include dependency graph for cnf.h:

Go to the source code of this file.

Classes

struct  Cnf_Dat_t_
 
struct  Cnf_Cut_t_
 
struct  Cnf_Man_t_
 

Macros

#define Cnf_CnfForClause(p, pBeg, pEnd, i)
 MACRO DEFINITIONS ///.
 
#define Cnf_CutForEachLeaf(p, pCut, pLeaf, i)
 

Typedefs

typedef typedefABC_NAMESPACE_HEADER_START struct Cnf_Man_t_ Cnf_Man_t
 INCLUDES ///.
 
typedef struct Cnf_Dat_t_ Cnf_Dat_t
 
typedef struct Cnf_Cut_t_ Cnf_Cut_t
 

Functions

Vec_Int_t * Cnf_DeriveMappingArray (Aig_Man_t *pAig)
 FUNCTION DECLARATIONS ///.
 
Cnf_Dat_t * Cnf_Derive (Aig_Man_t *pAig, int nOutputs)
 
Cnf_Dat_t * Cnf_DeriveWithMan (Cnf_Man_t *p, Aig_Man_t *pAig, int nOutputs)
 
Cnf_Dat_t * Cnf_DeriveOther (Aig_Man_t *pAig, int fSkipTtMin)
 
Cnf_Dat_t * Cnf_DeriveOtherWithMan (Cnf_Man_t *p, Aig_Man_t *pAig, int fSkipTtMin)
 
void Cnf_ManPrepare ()
 FUNCTION DEFINITIONS ///.
 
Cnf_Man_t * Cnf_ManRead ()
 
void Cnf_ManFree ()
 
Cnf_Cut_t * Cnf_CutCreate (Cnf_Man_t *p, Aig_Obj_t *pObj)
 
void Cnf_CutPrint (Cnf_Cut_t *pCut)
 
void Cnf_CutFree (Cnf_Cut_t *pCut)
 
void Cnf_CutUpdateRefs (Cnf_Man_t *p, Cnf_Cut_t *pCut, Cnf_Cut_t *pCutFan, Cnf_Cut_t *pCutRes)
 
Cnf_Cut_t * Cnf_CutCompose (Cnf_Man_t *p, Cnf_Cut_t *pCut, Cnf_Cut_t *pCutFan, int iFan)
 
void Cnf_ReadMsops (char **ppSopSizes, char ***ppSops)
 FUNCTION DEFINITIONS ///.
 
void Cnf_CollectLeaves (Aig_Obj_t *pRoot, Vec_Ptr_t *vSuper, int fStopCompl)
 
void Cnf_ComputeClauses (Aig_Man_t *p, Aig_Obj_t *pRoot, Vec_Ptr_t *vLeaves, Vec_Ptr_t *vNodes, Vec_Int_t *vMap, Vec_Int_t *vCover, Vec_Int_t *vClauses)
 
void Cnf_DeriveFastMark (Aig_Man_t *p)
 
Cnf_Dat_t * Cnf_DeriveFast (Aig_Man_t *p, int nOutputs)
 
Cnf_Man_t * Cnf_ManStart ()
 FUNCTION DEFINITIONS ///.
 
void Cnf_ManStop (Cnf_Man_t *p)
 
Vec_Int_t * Cnf_DataCollectPiSatNums (Cnf_Dat_t *pCnf, Aig_Man_t *p)
 
Cnf_Dat_t * Cnf_DataAlloc (Aig_Man_t *pAig, int nVars, int nClauses, int nLiterals)
 
Cnf_Dat_t * Cnf_DataDup (Cnf_Dat_t *p)
 
Cnf_Dat_t * Cnf_DataDupCof (Cnf_Dat_t *p, int Lit)
 
Cnf_Dat_t * Cnf_DataDupCofArray (Cnf_Dat_t *p, Vec_Int_t *vLits)
 
void Cnf_DataFree (Cnf_Dat_t *p)
 
void Cnf_DataLift (Cnf_Dat_t *p, int nVarsPlus)
 
void Cnf_DataCollectFlipLits (Cnf_Dat_t *p, int iFlipVar, Vec_Int_t *vFlips)
 
void Cnf_DataLiftAndFlipLits (Cnf_Dat_t *p, int nVarsPlus, Vec_Int_t *vLits)
 
void Cnf_DataPrint (Cnf_Dat_t *p, int fReadable)
 
void Cnf_DataWriteIntoFile (Cnf_Dat_t *p, char *pFileName, int fReadable, Vec_Int_t *vForAlls, Vec_Int_t *vExists)
 
void Cnf_DataWriteIntoFileInv (Cnf_Dat_t *p, char *pFileName, int fReadable, Vec_Int_t *vExists1, Vec_Int_t *vForAlls, Vec_Int_t *vExists2)
 
void * Cnf_DataWriteIntoSolver (Cnf_Dat_t *p, int nFrames, int fInit)
 
void * Cnf_DataWriteIntoSolverInt (void *pSat, Cnf_Dat_t *p, int nFrames, int fInit)
 
int Cnf_DataWriteOrClause (void *pSat, Cnf_Dat_t *pCnf)
 
int Cnf_DataWriteAndClauses (void *p, Cnf_Dat_t *pCnf)
 
void Cnf_DataTranformPolarity (Cnf_Dat_t *pCnf, int fTransformPos)
 
int Cnf_DataAddXorClause (void *pSat, int iVarA, int iVarB, int iVarC)
 
void Cnf_DeriveMapping (Cnf_Man_t *p)
 
int Cnf_ManMapForCnf (Cnf_Man_t *p)
 
void Cnf_ManTransferCuts (Cnf_Man_t *p)
 
void Cnf_ManFreeCuts (Cnf_Man_t *p)
 
void Cnf_ManPostprocess (Cnf_Man_t *p)
 
Vec_Ptr_t * Aig_ManScanMapping (Cnf_Man_t *p, int fCollect)
 
Vec_Ptr_t * Cnf_ManScanMapping (Cnf_Man_t *p, int fCollect, int fPreorder)
 
Vec_Int_t * Cnf_DataCollectCiSatNums (Cnf_Dat_t *pCnf, Aig_Man_t *p)
 
Vec_Int_t * Cnf_DataCollectCoSatNums (Cnf_Dat_t *pCnf, Aig_Man_t *p)
 
unsigned char * Cnf_DataDeriveLitPolarities (Cnf_Dat_t *p)
 
Cnf_Dat_t * Cnf_DataReadFromFile (char *pFileName)
 
Vec_Int_t * Cnf_ManWriteCnfMapping (Cnf_Man_t *p, Vec_Ptr_t *vMapped)
 DECLARATIONS ///.
 
void Cnf_SopConvertToVector (char *pSop, int nCubes, Vec_Int_t *vCover)
 
Cnf_Dat_t * Cnf_ManWriteCnf (Cnf_Man_t *p, Vec_Ptr_t *vMapped, int nOutputs)
 
Cnf_Dat_t * Cnf_ManWriteCnfOther (Cnf_Man_t *p, Vec_Ptr_t *vMapped)
 
Cnf_Dat_t * Cnf_DeriveSimple (Aig_Man_t *p, int nOutputs)
 
Cnf_Dat_t * Cnf_DeriveSimpleForRetiming (Aig_Man_t *p)
 

Macro Definition Documentation

◆ Cnf_CnfForClause

#define Cnf_CnfForClause ( p,
pBeg,
pEnd,
i )
Value:
for ( i = 0; i < p->nClauses && (pBeg = p->pClauses[i]) && (pEnd = p->pClauses[i+1]); i++ )
p
Cube * p
Definition exorList.c:222

MACRO DEFINITIONS ///.

ITERATORS ///

Definition at line 117 of file cnf.h.

117#define Cnf_CnfForClause( p, pBeg, pEnd, i ) \
118 for ( i = 0; i < p->nClauses && (pBeg = p->pClauses[i]) && (pEnd = p->pClauses[i+1]); i++ )

◆ Cnf_CutForEachLeaf

#define Cnf_CutForEachLeaf ( p,
pCut,
pLeaf,
i )
Value:
for ( i = 0; (i < (int)(pCut)->nFanins) && ((pLeaf) = Aig_ManObj(p, (pCut)->pFanins[i])); i++ )

Definition at line 121 of file cnf.h.

121#define Cnf_CutForEachLeaf( p, pCut, pLeaf, i ) \
122 for ( i = 0; (i < (int)(pCut)->nFanins) && ((pLeaf) = Aig_ManObj(p, (pCut)->pFanins[i])); i++ )

Typedef Documentation

◆ Cnf_Cut_t

typedef struct Cnf_Cut_t_ Cnf_Cut_t

Definition at line 53 of file cnf.h.

◆ Cnf_Dat_t

typedef struct Cnf_Dat_t_ Cnf_Dat_t

Definition at line 52 of file cnf.h.

◆ Cnf_Man_t

typedef typedefABC_NAMESPACE_HEADER_START struct Cnf_Man_t_ Cnf_Man_t

INCLUDES ///.

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

FileName [cnf.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [DAG-aware AIG rewriting.]

Synopsis [External declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - April 28, 2007.]

Revision [

Id
cnf.h,v 1.00 2007/04/28 00:00:00 alanmi Exp

] PARAMETERS /// BASIC TYPES ///

Definition at line 51 of file cnf.h.

Function Documentation

◆ Aig_ManScanMapping()

Vec_Ptr_t * Aig_ManScanMapping ( Cnf_Man_t * p,
int fCollect )
extern

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

Synopsis [Computes area, references, and nodes used in the mapping.]

Description [Collects the nodes in reverse topological order.]

SideEffects []

SeeAlso []

Definition at line 297 of file cnfUtil.c.

298{
299 Vec_Ptr_t *vMapped = NULL;
300 Aig_Obj_t *pObj;
301 int i;
302 // clean all references
303 Aig_ManForEachObj(p->pManAig, pObj, i)
304 pObj->nRefs = 0;
305 // allocate the array
306 if (fCollect)
307 vMapped = Vec_PtrAlloc(1000);
308 // collect nodes reachable from POs in the DFS order through the best cuts
309 p->aArea = 0;
310 Aig_ManForEachCo(p->pManAig, pObj, i)
311 p->aArea += Aig_ManScanMapping_rec(p, Aig_ObjFanin0(pObj), vMapped);
312 // printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) + Aig_ManCiNum(p->pManAig) + 1 : 0, p->aArea + 2 );
313 return vMapped;
314}
Aig_ManForEachObj
#define Aig_ManForEachObj(p, pObj, i)
Definition aig.h:403
Aig_Obj_t
struct Aig_Obj_t_ Aig_Obj_t
Definition aig.h:51
Aig_ManForEachCo
#define Aig_ManForEachCo(p, pObj, i)
Definition aig.h:398
Aig_ManScanMapping_rec
int Aig_ManScanMapping_rec(Cnf_Man_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vMapped)
Definition cnfUtil.c:253
Aig_Obj_t_::nRefs
unsigned int nRefs
Definition aig.h:81
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
Here is the call graph for this function:

◆ Cnf_CollectLeaves()

void Cnf_CollectLeaves ( Aig_Obj_t * pRoot,
Vec_Ptr_t * vSuper,
int fStopCompl )
extern

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

Synopsis [Detects multi-input gate rooted at this node.]

Description []

SideEffects []

SeeAlso []

Definition at line 76 of file cnfFast.c.

77{
78 assert( !Aig_IsComplement(pRoot) );
79 Vec_PtrClear( vSuper );
80 Cnf_CollectLeaves_rec( pRoot, pRoot, vSuper, fStopCompl );
81}
Cnf_CollectLeaves_rec
ABC_NAMESPACE_IMPL_START void Cnf_CollectLeaves_rec(Aig_Obj_t *pRoot, Aig_Obj_t *pObj, Vec_Ptr_t *vSuper, int fStopCompl)
DECLARATIONS ///.
Definition cnfFast.c:45
assert
#define assert(ex)
Definition util_old.h:213
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Cnf_ComputeClauses()

void Cnf_ComputeClauses ( Aig_Man_t * p,
Aig_Obj_t * pRoot,
Vec_Ptr_t * vLeaves,
Vec_Ptr_t * vNodes,
Vec_Int_t * vMap,
Vec_Int_t * vCover,
Vec_Int_t * vClauses )
extern

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

Synopsis [Collects nodes inside the cone.]

Description []

SideEffects []

SeeAlso []

Definition at line 198 of file cnfFast.c.

200{
201 Aig_Obj_t * pLeaf;
202 int c, k, Cube, OutLit, RetValue;
203 word Truth;
204 assert( pRoot->fMarkA );
205
206 Vec_IntClear( vClauses );
207
208 OutLit = Cnf_ObjGetLit( vMap, pRoot, 0 );
209 // detect cone
210 Cnf_CollectLeaves( pRoot, vLeaves, 0 );
211 Cnf_CollectVolume( p, pRoot, vLeaves, vNodes );
212 assert( pRoot == Vec_PtrEntryLast(vNodes) );
213 // check if this is an AND-gate
214 Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pLeaf, k )
215 {
216 if ( Aig_ObjFaninC0(pLeaf) && !Aig_ObjFanin0(pLeaf)->fMarkA )
217 break;
218 if ( Aig_ObjFaninC1(pLeaf) && !Aig_ObjFanin1(pLeaf)->fMarkA )
219 break;
220 }
221 if ( k == Vec_PtrSize(vNodes) )
222 {
223 Cnf_CollectLeaves( pRoot, vLeaves, 1 );
224 // write big clause
225 Vec_IntPush( vClauses, 0 );
226 Vec_IntPush( vClauses, OutLit );
227 Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pLeaf, k )
228 Vec_IntPush( vClauses, Cnf_ObjGetLit(vMap, Aig_Regular(pLeaf), !Aig_IsComplement(pLeaf)) );
229 // write small clauses
230 Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pLeaf, k )
231 {
232 Vec_IntPush( vClauses, 0 );
233 Vec_IntPush( vClauses, OutLit ^ 1 );
234 Vec_IntPush( vClauses, Cnf_ObjGetLit(vMap, Aig_Regular(pLeaf), Aig_IsComplement(pLeaf)) );
235 }
236 return;
237 }
238 if ( Vec_PtrSize(vLeaves) > 6 )
239 printf( "FastCnfGeneration: Internal error!!!\n" );
240 assert( Vec_PtrSize(vLeaves) <= 6 );
241
242 Truth = Cnf_CutDeriveTruth( p, vLeaves, vNodes );
243 if ( Truth == 0 || Truth == ~(word)0 )
244 {
245 Vec_IntPush( vClauses, 0 );
246 Vec_IntPush( vClauses, (Truth == 0) ? (OutLit ^ 1) : OutLit );
247 return;
248 }
249
250 RetValue = Kit_TruthIsop( (unsigned *)&Truth, Vec_PtrSize(vLeaves), vCover, 0 );
251 assert( RetValue >= 0 );
252
253 Vec_IntForEachEntry( vCover, Cube, c )
254 {
255 Vec_IntPush( vClauses, 0 );
256 Vec_IntPush( vClauses, OutLit );
257 for ( k = 0; k < Vec_PtrSize(vLeaves); k++, Cube >>= 2 )
258 {
259 if ( (Cube & 3) == 0 )
260 continue;
261 assert( (Cube & 3) != 3 );
262 Vec_IntPush( vClauses, Cnf_ObjGetLit(vMap, (Aig_Obj_t *)Vec_PtrEntry(vLeaves,k), (Cube&3)!=1) );
263 }
264 }
265
266 Truth = ~Truth;
267
268 RetValue = Kit_TruthIsop( (unsigned *)&Truth, Vec_PtrSize(vLeaves), vCover, 0 );
269 assert( RetValue >= 0 );
270 Vec_IntForEachEntry( vCover, Cube, c )
271 {
272 Vec_IntPush( vClauses, 0 );
273 Vec_IntPush( vClauses, OutLit ^ 1 );
274 for ( k = 0; k < Vec_PtrSize(vLeaves); k++, Cube >>= 2 )
275 {
276 if ( (Cube & 3) == 0 )
277 continue;
278 assert( (Cube & 3) != 3 );
279 Vec_IntPush( vClauses, Cnf_ObjGetLit(vMap, (Aig_Obj_t *)Vec_PtrEntry(vLeaves,k), (Cube&3)!=1) );
280 }
281 }
282}
Cnf_CutDeriveTruth
word Cnf_CutDeriveTruth(Aig_Man_t *p, Vec_Ptr_t *vLeaves, Vec_Ptr_t *vNodes)
Definition cnfFast.c:138
Cnf_CollectVolume
void Cnf_CollectVolume(Aig_Man_t *p, Aig_Obj_t *pRoot, Vec_Ptr_t *vLeaves, Vec_Ptr_t *vNodes)
Definition cnfFast.c:116
Cnf_CollectLeaves
void Cnf_CollectLeaves(Aig_Obj_t *pRoot, Vec_Ptr_t *vSuper, int fStopCompl)
Definition cnfFast.c:76
Cube
struct cube Cube
word
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
Kit_TruthIsop
int Kit_TruthIsop(unsigned *puTruth, int nVars, Vec_Int_t *vMemory, int fTryBoth)
Definition kitIsop.c:134
Aig_Obj_t_::fMarkA
unsigned int fMarkA
Definition aig.h:79
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecPtr.h:55
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Cnf_CutCompose()

Cnf_Cut_t * Cnf_CutCompose ( Cnf_Man_t * p,
Cnf_Cut_t * pCut,
Cnf_Cut_t * pCutFan,
int iFan )
extern

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

Synopsis [Merges two cuts.]

Description [Returns NULL of the cuts cannot be merged.]

SideEffects []

SeeAlso []

Definition at line 294 of file cnfCut.c.

295{
296 Cnf_Cut_t * pCutRes;
297 static int pFanins[32];
298 unsigned * pTruth, * pTruthFan, * pTruthRes;
299 unsigned * pTop = p->pTruths[0], * pFan = p->pTruths[2], * pTemp = p->pTruths[3];
300 unsigned uPhase, uPhaseFan;
301 int i, iVar, nFanins, RetValue;
302
303 // make sure the second cut is the fanin of the first
304 for ( iVar = 0; iVar < pCut->nFanins; iVar++ )
305 if ( pCut->pFanins[iVar] == iFan )
306 break;
307 assert( iVar < pCut->nFanins );
308 // remove this variable
309 Cnf_CutRemoveIthVar( pCut, iVar, iFan );
310 // merge leaves of the cuts
311 nFanins = Cnf_CutMergeLeaves( pCut, pCutFan, pFanins );
312 if ( nFanins+1 > p->nMergeLimit )
313 {
314 Cnf_CutInsertIthVar( pCut, iVar, iFan );
315 return NULL;
316 }
317 // create new cut
318 pCutRes = Cnf_CutAlloc( p, nFanins );
319 memcpy( pCutRes->pFanins, pFanins, sizeof(int) * nFanins );
320 assert( pCutRes->nFanins <= pCut->nFanins + pCutFan->nFanins );
321
322 // derive its truth table
323 // get the truth tables in the composition space
324 pTruth = Cnf_CutTruth(pCut);
325 pTruthFan = Cnf_CutTruth(pCutFan);
326 pTruthRes = Cnf_CutTruth(pCutRes);
327 for ( i = 0; i < 2*pCutRes->nWords; i++ )
328 pTop[i] = pTruth[i % pCut->nWords];
329 for ( i = 0; i < pCutRes->nWords; i++ )
330 pFan[i] = pTruthFan[i % pCutFan->nWords];
331 // move the variable to the end
332 uPhase = Kit_BitMask( pCutRes->nFanins+1 ) & ~(1 << iVar);
333 Kit_TruthShrink( pTemp, pTop, pCutRes->nFanins, pCutRes->nFanins+1, uPhase, 1 );
334 // compute the phases
335 uPhase = Cnf_TruthPhase( pCutRes, pCut ) | (1 << pCutRes->nFanins);
336 uPhaseFan = Cnf_TruthPhase( pCutRes, pCutFan );
337 // permute truth-tables to the common support
338 Kit_TruthStretch( pTemp, pTop, pCut->nFanins+1, pCutRes->nFanins+1, uPhase, 1 );
339 Kit_TruthStretch( pTemp, pFan, pCutFan->nFanins, pCutRes->nFanins, uPhaseFan, 1 );
340 // perform Boolean operation
341 Kit_TruthMux( pTruthRes, pTop, pTop+pCutRes->nWords, pFan, pCutRes->nFanins );
342 // return the cut to its original condition
343 Cnf_CutInsertIthVar( pCut, iVar, iFan );
344 // consider the simple case
345 if ( pCutRes->nFanins < 5 )
346 {
347 pCutRes->Cost = p->pSopSizes[0xFFFF & *pTruthRes] + p->pSopSizes[0xFFFF & ~*pTruthRes];
348 return pCutRes;
349 }
350
351 // derive ISOP for positive phase
352 RetValue = Kit_TruthIsop( pTruthRes, pCutRes->nFanins, p->vMemory, 0 );
353 pCutRes->vIsop[1] = (RetValue == -1)? NULL : Vec_IntDup( p->vMemory );
354 // derive ISOP for negative phase
355 Kit_TruthNot( pTruthRes, pTruthRes, pCutRes->nFanins );
356 RetValue = Kit_TruthIsop( pTruthRes, pCutRes->nFanins, p->vMemory, 0 );
357 pCutRes->vIsop[0] = (RetValue == -1)? NULL : Vec_IntDup( p->vMemory );
358 Kit_TruthNot( pTruthRes, pTruthRes, pCutRes->nFanins );
359
360 // compute the cut cost
361 if ( pCutRes->vIsop[0] == NULL || pCutRes->vIsop[1] == NULL )
362 pCutRes->Cost = 127;
363 else if ( Vec_IntSize(pCutRes->vIsop[0]) + Vec_IntSize(pCutRes->vIsop[1]) > 127 )
364 pCutRes->Cost = 127;
365 else
366 pCutRes->Cost = Vec_IntSize(pCutRes->vIsop[0]) + Vec_IntSize(pCutRes->vIsop[1]);
367 return pCutRes;
368}
Cnf_CutRemoveIthVar
void Cnf_CutRemoveIthVar(Cnf_Cut_t *pCut, int iVar, int iFan)
Definition cnfCut.c:254
Cnf_CutAlloc
ABC_NAMESPACE_IMPL_START Cnf_Cut_t * Cnf_CutAlloc(Cnf_Man_t *p, int nLeaves)
DECLARATIONS ///.
Definition cnfCut.c:46
Cnf_CutInsertIthVar
void Cnf_CutInsertIthVar(Cnf_Cut_t *pCut, int iVar, int iFan)
Definition cnfCut.c:274
Cnf_Cut_t
struct Cnf_Cut_t_ Cnf_Cut_t
Definition cnf.h:53
Kit_TruthShrink
void Kit_TruthShrink(unsigned *pOut, unsigned *pIn, int nVars, int nVarsAll, unsigned Phase, int fReturnIn)
Definition kitTruth.c:200
Kit_TruthStretch
void Kit_TruthStretch(unsigned *pOut, unsigned *pIn, int nVars, int nVarsAll, unsigned Phase, int fReturnIn)
Definition kitTruth.c:166
Cnf_Cut_t_::vIsop
Vec_Int_t * vIsop[2]
Definition cnf.h:76
Cnf_Cut_t_::nFanins
char nFanins
Definition cnf.h:73
Cnf_Cut_t_::pFanins
int pFanins[0]
Definition cnf.h:77
Cnf_Cut_t_::Cost
char Cost
Definition cnf.h:74
Cnf_Cut_t_::nWords
short nWords
Definition cnf.h:75
memcpy
char * memcpy()
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Cnf_CutCreate()

Cnf_Cut_t * Cnf_CutCreate ( Cnf_Man_t * p,
Aig_Obj_t * pObj )
extern

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

Synopsis [Creates cut for the given node.]

Description []

SideEffects []

SeeAlso []

Definition at line 87 of file cnfCut.c.

88{
89 Dar_Cut_t * pCutBest;
90 Cnf_Cut_t * pCut;
91 unsigned * pTruth;
92 assert( Aig_ObjIsNode(pObj) );
93 pCutBest = Dar_ObjBestCut( pObj );
94 assert( pCutBest != NULL );
95 assert( pCutBest->nLeaves <= 4 );
96 pCut = Cnf_CutAlloc( p, pCutBest->nLeaves );
97 memcpy( pCut->pFanins, pCutBest->pLeaves, sizeof(int) * pCutBest->nLeaves );
98 pTruth = Cnf_CutTruth(pCut);
99 *pTruth = (pCutBest->uTruth << 16) | pCutBest->uTruth;
100 pCut->Cost = Cnf_CutSopCost( p, pCutBest );
101 return pCut;
102}
Dar_Cut_t
struct Dar_Cut_t_ Dar_Cut_t
Definition darInt.h:52
Dar_Cut_t_::nLeaves
unsigned nLeaves
Definition darInt.h:62
Dar_Cut_t_::pLeaves
int pLeaves[4]
Definition darInt.h:63
Dar_Cut_t_::uTruth
unsigned uTruth
Definition darInt.h:58
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Cnf_CutFree()

void Cnf_CutFree ( Cnf_Cut_t * pCut)
extern

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

Synopsis [Deallocates cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 68 of file cnfCut.c.

69{
70 if ( pCut->vIsop[0] )
71 Vec_IntFree( pCut->vIsop[0] );
72 if ( pCut->vIsop[1] )
73 Vec_IntFree( pCut->vIsop[1] );
74}
Here is the caller graph for this function:

◆ Cnf_CutPrint()

void Cnf_CutPrint ( Cnf_Cut_t * pCut)
extern

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

Synopsis [Deallocates cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 115 of file cnfCut.c.

116{
117 int i;
118 printf( "{" );
119 for ( i = 0; i < pCut->nFanins; i++ )
120 printf( "%d ", pCut->pFanins[i] );
121 printf( " } " );
122}

◆ Cnf_CutUpdateRefs()

void Cnf_CutUpdateRefs ( Cnf_Man_t * p,
Cnf_Cut_t * pCut,
Cnf_Cut_t * pCutFan,
Cnf_Cut_t * pCutRes )
extern

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

Synopsis [Allocates cut of the given size.]

Description []

SideEffects []

SeeAlso []

Definition at line 178 of file cnfCut.c.

179{
180 Cnf_CutDeref( p, pCut );
181 Cnf_CutDeref( p, pCutFan );
182 Cnf_CutRef( p, pCutRes );
183}
Cnf_CutDeref
void Cnf_CutDeref(Cnf_Man_t *p, Cnf_Cut_t *pCut)
Definition cnfCut.c:135
Cnf_CutRef
void Cnf_CutRef(Cnf_Man_t *p, Cnf_Cut_t *pCut)
Definition cnfCut.c:157
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Cnf_DataAddXorClause()

int Cnf_DataAddXorClause ( void * pSat,
int iVarA,
int iVarB,
int iVarC )
extern

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

Synopsis [Adds constraints for the two-input AND-gate.]

Description []

SideEffects []

SeeAlso []

Definition at line 804 of file cnfMan.c.

805{
806 lit Lits[3];
807 assert( iVarA > 0 && iVarB > 0 && iVarC > 0 );
808
809 Lits[0] = toLitCond( iVarA, 1 );
810 Lits[1] = toLitCond( iVarB, 1 );
811 Lits[2] = toLitCond( iVarC, 1 );
812 if ( !sat_solver_addclause( (sat_solver *)pSat, Lits, Lits + 3 ) )
813 return 0;
814
815 Lits[0] = toLitCond( iVarA, 1 );
816 Lits[1] = toLitCond( iVarB, 0 );
817 Lits[2] = toLitCond( iVarC, 0 );
818 if ( !sat_solver_addclause( (sat_solver *)pSat, Lits, Lits + 3 ) )
819 return 0;
820
821 Lits[0] = toLitCond( iVarA, 0 );
822 Lits[1] = toLitCond( iVarB, 1 );
823 Lits[2] = toLitCond( iVarC, 0 );
824 if ( !sat_solver_addclause( (sat_solver *)pSat, Lits, Lits + 3 ) )
825 return 0;
826
827 Lits[0] = toLitCond( iVarA, 0 );
828 Lits[1] = toLitCond( iVarB, 0 );
829 Lits[2] = toLitCond( iVarC, 1 );
830 if ( !sat_solver_addclause( (sat_solver *)pSat, Lits, Lits + 3 ) )
831 return 0;
832
833 return 1;
834}
sat_solver_addclause
#define sat_solver_addclause
Definition cecSatG2.c:37
sat_solver
#define sat_solver
Definition cecSatG2.c:34
lit
int lit
Definition satVec.h:130
Here is the caller graph for this function:

◆ Cnf_DataAlloc()

Cnf_Dat_t * Cnf_DataAlloc ( Aig_Man_t * pAig,
int nVars,
int nClauses,
int nLiterals )
extern

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

Synopsis [Allocates the new CNF.]

Description []

SideEffects []

SeeAlso []

Definition at line 124 of file cnfMan.c.

125{
126 Cnf_Dat_t * pCnf;
127 pCnf = ABC_CALLOC( Cnf_Dat_t, 1 );
128 pCnf->pMan = pAig;
129 pCnf->nVars = nVars;
130 pCnf->nClauses = nClauses;
131 pCnf->nLiterals = nLiterals;
132 pCnf->pClauses = ABC_ALLOC( int *, nClauses + 1 );
133 pCnf->pClauses[0] = ABC_ALLOC( int, nLiterals );
134 pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals;
135 if ( pCnf->pVarNums )
136 pCnf->pVarNums = ABC_FALLOC( int, Aig_ManObjNumMax(pAig) );
137 return pCnf;
138}
ABC_FALLOC
#define ABC_FALLOC(type, num)
Definition abc_global.h:266
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition abc_global.h:265
Cnf_Dat_t
struct Cnf_Dat_t_ Cnf_Dat_t
Definition cnf.h:52
Cnf_Dat_t_::nVars
int nVars
Definition cnf.h:59
Cnf_Dat_t_::nLiterals
int nLiterals
Definition cnf.h:60
Cnf_Dat_t_::pVarNums
int * pVarNums
Definition cnf.h:63
Cnf_Dat_t_::pClauses
int ** pClauses
Definition cnf.h:62
Cnf_Dat_t_::nClauses
int nClauses
Definition cnf.h:61
Cnf_Dat_t_::pMan
Aig_Man_t * pMan
Definition cnf.h:58
Here is the caller graph for this function:

◆ Cnf_DataCollectCiSatNums()

Vec_Int_t * Cnf_DataCollectCiSatNums ( Cnf_Dat_t * pCnf,
Aig_Man_t * p )
extern

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

Synopsis [Returns the array of CI IDs.]

Description []

SideEffects []

SeeAlso []

Definition at line 407 of file cnfUtil.c.

408{
409 Vec_Int_t *vCiIds;
410 Aig_Obj_t *pObj;
411 int i;
412 vCiIds = Vec_IntAlloc(Aig_ManCiNum(p));
413 Aig_ManForEachCi(p, pObj, i)
414 Vec_IntPush(vCiIds, pCnf->pVarNums[pObj->Id]);
415 return vCiIds;
416}
Aig_ManForEachCi
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition aig.h:393
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Aig_Obj_t_::Id
int Id
Definition aig.h:85
Here is the caller graph for this function:

◆ Cnf_DataCollectCoSatNums()

Vec_Int_t * Cnf_DataCollectCoSatNums ( Cnf_Dat_t * pCnf,
Aig_Man_t * p )
extern

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

Synopsis [Returns the array of CI IDs.]

Description []

SideEffects []

SeeAlso []

Definition at line 429 of file cnfUtil.c.

430{
431 Vec_Int_t *vCoIds;
432 Aig_Obj_t *pObj;
433 int i;
434 vCoIds = Vec_IntAlloc(Aig_ManCoNum(p));
435 Aig_ManForEachCo(p, pObj, i)
436 Vec_IntPush(vCoIds, pCnf->pVarNums[pObj->Id]);
437 return vCoIds;
438}
Here is the caller graph for this function:

◆ Cnf_DataCollectFlipLits()

void Cnf_DataCollectFlipLits ( Cnf_Dat_t * p,
int iFlipVar,
Vec_Int_t * vFlips )
extern

Definition at line 245 of file cnfMan.c.

246{
247 int v;
248 assert( p->pMan == NULL );
249 Vec_IntClear( vFlips );
250 for ( v = 0; v < p->nLiterals; v++ )
251 if ( Abc_Lit2Var(p->pClauses[0][v]) == iFlipVar )
252 Vec_IntPush( vFlips, v );
253}
Here is the caller graph for this function:

◆ Cnf_DataCollectPiSatNums()

Vec_Int_t * Cnf_DataCollectPiSatNums ( Cnf_Dat_t * pCnf,
Aig_Man_t * p )
extern

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

Synopsis [Returns the array of CI IDs.]

Description []

SideEffects []

SeeAlso []

Definition at line 104 of file cnfMan.c.

105{
106 Aig_Obj_t * pObj; int i;
107 Vec_Int_t * vCiIds = Vec_IntAlloc( Aig_ManCiNum(p) );
108 Aig_ManForEachCi( p, pObj, i )
109 Vec_IntPush( vCiIds, pCnf->pVarNums[pObj->Id] );
110 return vCiIds;
111}
Here is the caller graph for this function:

◆ Cnf_DataDeriveLitPolarities()

unsigned char * Cnf_DataDeriveLitPolarities ( Cnf_Dat_t * p)
extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 451 of file cnfUtil.c.

452{
453 int i, c, iClaBeg, iClaEnd, *pLit;
454 unsigned *pPols0 = ABC_CALLOC(unsigned, Aig_ManObjNumMax(p->pMan));
455 unsigned *pPols1 = ABC_CALLOC(unsigned, Aig_ManObjNumMax(p->pMan));
456 unsigned char *pPres = ABC_CALLOC(unsigned char, p->nClauses);
457 for (i = 0; i < Aig_ManObjNumMax(p->pMan); i++)
458 {
459 if (p->pObj2Count[i] == 0)
460 continue;
461 iClaBeg = p->pObj2Clause[i];
462 iClaEnd = p->pObj2Clause[i] + p->pObj2Count[i];
463 // go through the negative polarity clauses
464 for (c = iClaBeg; c < iClaEnd; c++)
465 for (pLit = p->pClauses[c] + 1; pLit < p->pClauses[c + 1]; pLit++)
466 if (Abc_LitIsCompl(p->pClauses[c][0]))
467 pPols0[Abc_Lit2Var(*pLit)] |= (unsigned)(2 - Abc_LitIsCompl(*pLit)); // taking the opposite (!) -- not the case
468 else
469 pPols1[Abc_Lit2Var(*pLit)] |= (unsigned)(2 - Abc_LitIsCompl(*pLit)); // taking the opposite (!) -- not the case
470 // record these clauses
471 for (c = iClaBeg; c < iClaEnd; c++)
472 for (pLit = p->pClauses[c] + 1; pLit < p->pClauses[c + 1]; pLit++)
473 if (Abc_LitIsCompl(p->pClauses[c][0]))
474 pPres[c] = (unsigned char)((unsigned)pPres[c] | (pPols0[Abc_Lit2Var(*pLit)] << (2 * (pLit - p->pClauses[c] - 1))));
475 else
476 pPres[c] = (unsigned char)((unsigned)pPres[c] | (pPols1[Abc_Lit2Var(*pLit)] << (2 * (pLit - p->pClauses[c] - 1))));
477 // clean negative polarity
478 for (c = iClaBeg; c < iClaEnd; c++)
479 for (pLit = p->pClauses[c] + 1; pLit < p->pClauses[c + 1]; pLit++)
480 pPols0[Abc_Lit2Var(*pLit)] = pPols1[Abc_Lit2Var(*pLit)] = 0;
481 }
482 ABC_FREE(pPols0);
483 ABC_FREE(pPols1);
484 /*
485 // for ( c = 0; c < p->nClauses; c++ )
486 for ( c = 0; c < 100; c++ )
487 {
488 printf( "Clause %6d : ", c );
489 for ( i = 0; i < 4; i++ )
490 printf( "%d ", ((unsigned)pPres[c] >> (2*i)) & 3 );
491 printf( " " );
492 for ( pLit = p->pClauses[c]; pLit < p->pClauses[c+1]; pLit++ )
493 printf( "%6d ", *pLit );
494 printf( "\n" );
495 }
496 */
497 return pPres;
498}
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267

◆ Cnf_DataDup()

Cnf_Dat_t * Cnf_DataDup ( Cnf_Dat_t * p)
extern

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

Synopsis [Allocates the new CNF.]

Description []

SideEffects []

SeeAlso []

Definition at line 151 of file cnfMan.c.

152{
153 Cnf_Dat_t * pCnf;
154 int i;
155 pCnf = Cnf_DataAlloc( p->pMan, p->nVars, p->nClauses, p->nLiterals );
156 memcpy( pCnf->pClauses[0], p->pClauses[0], sizeof(int) * p->nLiterals );
157 if ( p->pVarNums )
158 memcpy( pCnf->pVarNums, p->pVarNums, sizeof(int) * Aig_ManObjNumMax(p->pMan) );
159 for ( i = 1; i < p->nClauses; i++ )
160 pCnf->pClauses[i] = pCnf->pClauses[0] + (p->pClauses[i] - p->pClauses[0]);
161 return pCnf;
162}
Cnf_DataAlloc
Cnf_Dat_t * Cnf_DataAlloc(Aig_Man_t *pAig, int nVars, int nClauses, int nLiterals)
Definition cnfMan.c:124
Here is the call graph for this function:

◆ Cnf_DataDupCof()

Cnf_Dat_t * Cnf_DataDupCof ( Cnf_Dat_t * p,
int Lit )
extern

Definition at line 163 of file cnfMan.c.

164{
165 Cnf_Dat_t * pCnf;
166 int i;
167 pCnf = Cnf_DataAlloc( p->pMan, p->nVars, p->nClauses+1, p->nLiterals+1 );
168 memcpy( pCnf->pClauses[0], p->pClauses[0], sizeof(int) * p->nLiterals );
169 if ( pCnf->pVarNums )
170 memcpy( pCnf->pVarNums, p->pVarNums, sizeof(int) * Aig_ManObjNumMax(p->pMan) );
171 for ( i = 1; i < p->nClauses; i++ )
172 pCnf->pClauses[i] = pCnf->pClauses[0] + (p->pClauses[i] - p->pClauses[0]);
173 pCnf->pClauses[p->nClauses] = pCnf->pClauses[0] + p->nLiterals;
174 pCnf->pClauses[p->nClauses][0] = Lit;
175 assert( pCnf->pClauses[p->nClauses+1] == pCnf->pClauses[0] + p->nLiterals+1 );
176 return pCnf;
177}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Cnf_DataDupCofArray()

Cnf_Dat_t * Cnf_DataDupCofArray ( Cnf_Dat_t * p,
Vec_Int_t * vLits )
extern

Definition at line 178 of file cnfMan.c.

179{
180 Cnf_Dat_t * pCnf;
181 int i, iLit;
182 pCnf = Cnf_DataAlloc( p->pMan, p->nVars, p->nClauses+Vec_IntSize(vLits), p->nLiterals+Vec_IntSize(vLits) );
183 memcpy( pCnf->pClauses[0], p->pClauses[0], sizeof(int) * p->nLiterals );
184 if ( pCnf->pVarNums )
185 memcpy( pCnf->pVarNums, p->pVarNums, sizeof(int) * Aig_ManObjNumMax(p->pMan) );
186 for ( i = 1; i < p->nClauses; i++ )
187 pCnf->pClauses[i] = pCnf->pClauses[0] + (p->pClauses[i] - p->pClauses[0]);
188 Vec_IntForEachEntry( vLits, iLit, i ) {
189 pCnf->pClauses[p->nClauses+i] = pCnf->pClauses[0] + p->nLiterals+i;
190 pCnf->pClauses[p->nClauses+i][0] = iLit;
191 }
192 assert( pCnf->pClauses[p->nClauses+Vec_IntSize(vLits)] == pCnf->pClauses[0] + p->nLiterals+Vec_IntSize(vLits) );
193 return pCnf;
194}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Cnf_DataFree()

void Cnf_DataFree ( Cnf_Dat_t * p)
extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 207 of file cnfMan.c.

208{
209 if ( p == NULL )
210 return;
211 Vec_IntFreeP( &p->vMapping );
212 ABC_FREE( p->pClaPols );
213 ABC_FREE( p->pObj2Clause );
214 ABC_FREE( p->pObj2Count );
215 ABC_FREE( p->pClauses[0] );
216 ABC_FREE( p->pClauses );
217 ABC_FREE( p->pVarNums );
218 ABC_FREE( p );
219}

◆ Cnf_DataLift()

void Cnf_DataLift ( Cnf_Dat_t * p,
int nVarsPlus )
extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 232 of file cnfMan.c.

233{
234 Aig_Obj_t * pObj;
235 int v;
236 if ( p->pMan )
237 {
238 Aig_ManForEachObj( p->pMan, pObj, v )
239 if ( p->pVarNums[pObj->Id] >= 0 )
240 p->pVarNums[pObj->Id] += nVarsPlus;
241 }
242 for ( v = 0; v < p->nLiterals; v++ )
243 p->pClauses[0][v] += 2*nVarsPlus;
244}
Here is the caller graph for this function:

◆ Cnf_DataLiftAndFlipLits()

void Cnf_DataLiftAndFlipLits ( Cnf_Dat_t * p,
int nVarsPlus,
Vec_Int_t * vLits )
extern

Definition at line 254 of file cnfMan.c.

255{
256 int i, iLit;
257 assert( p->pMan == NULL );
258 Vec_IntForEachEntry( vLits, iLit, i )
259 p->pClauses[0][iLit] = Abc_LitNot(p->pClauses[0][iLit]) + 2*nVarsPlus;
260}
Here is the caller graph for this function:

◆ Cnf_DataPrint()

void Cnf_DataPrint ( Cnf_Dat_t * p,
int fReadable )
extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 273 of file cnfMan.c.

274{
275 FILE * pFile = stdout;
276 int * pLit, * pStop, i;
277 fprintf( pFile, "p cnf %d %d\n", p->nVars, p->nClauses );
278 for ( i = 0; i < p->nClauses; i++ )
279 {
280 for ( pLit = p->pClauses[i], pStop = p->pClauses[i+1]; pLit < pStop; pLit++ )
281 fprintf( pFile, "%s%d ", Abc_LitIsCompl(*pLit) ? "-":"", fReadable? Abc_Lit2Var(*pLit) : Abc_Lit2Var(*pLit)+1 );
282 fprintf( pFile, "\n" );
283 }
284 fprintf( pFile, "\n" );
285}

◆ Cnf_DataReadFromFile()

Cnf_Dat_t * Cnf_DataReadFromFile ( char * pFileName)
extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 511 of file cnfUtil.c.

512{
513 int MaxLine = 1000000;
514 int Var, Lit, nVars = -1, nClas = -1, i, Entry, iLine = 0;
515 Cnf_Dat_t *pCnf = NULL;
516 Vec_Int_t *vClas = NULL;
517 Vec_Int_t *vLits = NULL;
518 char *pBuffer, *pToken;
519 FILE *pFile = fopen(pFileName, "rb");
520 if (pFile == NULL)
521 {
522 printf("Cannot open file \"%s\" for writing.\n", pFileName);
523 return NULL;
524 }
525 pBuffer = ABC_ALLOC(char, MaxLine);
526 while (fgets(pBuffer, MaxLine, pFile) != NULL)
527 {
528 iLine++;
529 if (pBuffer[0] == 'c')
530 continue;
531 if (pBuffer[0] == 'p')
532 {
533 pToken = strtok(pBuffer + 1, " \t");
534 if (strcmp(pToken, "cnf"))
535 {
536 printf("Incorrect input file.\n");
537 goto finish;
538 }
539 pToken = strtok(NULL, " \t");
540 nVars = atoi(pToken);
541 pToken = strtok(NULL, " \t");
542 nClas = atoi(pToken);
543 if (nVars <= 0 || nClas <= 0)
544 {
545 printf("Incorrect parameters.\n");
546 goto finish;
547 }
548 // temp storage
549 vClas = Vec_IntAlloc(nClas + 1);
550 vLits = Vec_IntAlloc(nClas * 8);
551 continue;
552 }
553 pToken = strtok(pBuffer, " \t\r\n");
554 if (pToken == NULL)
555 continue;
556 Vec_IntPush(vClas, Vec_IntSize(vLits));
557 while (pToken)
558 {
559 Var = atoi(pToken);
560 if (Var == 0)
561 break;
562 Lit = (Var > 0) ? Abc_Var2Lit(Var - 1, 0) : Abc_Var2Lit(-Var - 1, 1);
563 if (Lit >= 2 * nVars)
564 {
565 printf("Literal %d is out-of-bound for %d variables.\n", Lit, nVars);
566 goto finish;
567 }
568 Vec_IntPush(vLits, Lit);
569 pToken = strtok(NULL, " \t\r\n");
570 }
571 if (Var != 0)
572 {
573 printf("There is no zero-terminator in line %d.\n", iLine);
574 goto finish;
575 }
576 }
577 // finalize
578 if (Vec_IntSize(vClas) != nClas)
579 printf("Warning! The number of clauses (%d) is different from declaration (%d).\n", Vec_IntSize(vClas), nClas);
580 Vec_IntPush(vClas, Vec_IntSize(vLits));
581 // create
582 pCnf = ABC_CALLOC(Cnf_Dat_t, 1);
583 pCnf->nVars = nVars;
584 pCnf->nClauses = Vec_IntSize(vClas) - 1;
585 pCnf->nLiterals = Vec_IntSize(vLits);
586 pCnf->pClauses = ABC_ALLOC(int *, Vec_IntSize(vClas));
587 pCnf->pClauses[0] = Vec_IntReleaseArray(vLits);
588 Vec_IntForEachEntry(vClas, Entry, i)
589 pCnf->pClauses[i] = pCnf->pClauses[0] + Entry;
590finish:
591 fclose(pFile);
592 Vec_IntFreeP(&vClas);
593 Vec_IntFreeP(&vLits);
594 ABC_FREE(pBuffer);
595 return pCnf;
596}
Var
int Var
Definition exorList.c:228
strcmp
int strcmp()
strtok
char * strtok()
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Cnf_DataTranformPolarity()

void Cnf_DataTranformPolarity ( Cnf_Dat_t * pCnf,
int fTransformPos )
extern

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

Synopsis [Transforms polarity of the internal veriables.]

Description []

SideEffects []

SeeAlso []

Definition at line 768 of file cnfMan.c.

769{
770 Aig_Obj_t * pObj;
771 int * pVarToPol;
772 int i, iVar;
773 // create map from the variable number to its polarity
774 pVarToPol = ABC_CALLOC( int, pCnf->nVars );
775 Aig_ManForEachObj( pCnf->pMan, pObj, i )
776 {
777 if ( !fTransformPos && Aig_ObjIsCo(pObj) )
778 continue;
779 if ( pCnf->pVarNums[pObj->Id] >= 0 )
780 pVarToPol[ pCnf->pVarNums[pObj->Id] ] = pObj->fPhase;
781 }
782 // transform literals
783 for ( i = 0; i < pCnf->nLiterals; i++ )
784 {
785 iVar = lit_var(pCnf->pClauses[0][i]);
786 assert( iVar < pCnf->nVars );
787 if ( pVarToPol[iVar] )
788 pCnf->pClauses[0][i] = lit_neg( pCnf->pClauses[0][i] );
789 }
790 ABC_FREE( pVarToPol );
791}
Aig_Obj_t_::fPhase
unsigned int fPhase
Definition aig.h:78
Here is the caller graph for this function:

◆ Cnf_DataWriteAndClauses()

int Cnf_DataWriteAndClauses ( void * p,
Cnf_Dat_t * pCnf )
extern

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

Synopsis [Adds the OR-clause.]

Description []

SideEffects []

SeeAlso []

Definition at line 743 of file cnfMan.c.

744{
745 sat_solver * pSat = (sat_solver *)p;
746 Aig_Obj_t * pObj;
747 int i, Lit;
748 Aig_ManForEachCo( pCnf->pMan, pObj, i )
749 {
750 Lit = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
751 if ( !sat_solver_addclause( pSat, &Lit, &Lit+1 ) )
752 return 0;
753 }
754 return 1;
755}
Here is the caller graph for this function:

◆ Cnf_DataWriteIntoFile()

void Cnf_DataWriteIntoFile ( Cnf_Dat_t * p,
char * pFileName,
int fReadable,
Vec_Int_t * vForAlls,
Vec_Int_t * vExists )
extern

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

Synopsis [Writes CNF into a file.]

Description []

SideEffects []

SeeAlso []

Definition at line 387 of file cnfMan.c.

388{
389 FILE * pFile;
390 int * pLit, * pStop, i, VarId;
391 if ( !strncmp(pFileName+strlen(pFileName)-3,".gz",3) )
392 {
393 Cnf_DataWriteIntoFileGz( p, pFileName, fReadable, vForAlls, vExists );
394 return;
395 }
396 pFile = fopen( pFileName, "w" );
397 if ( pFile == NULL )
398 {
399 printf( "Cnf_WriteIntoFile(): Output file cannot be opened.\n" );
400 return;
401 }
402 fprintf( pFile, "c Result of efficient AIG-to-CNF conversion using package CNF\n" );
403 fprintf( pFile, "p cnf %d %d\n", p->nVars, p->nClauses );
404 if ( vForAlls )
405 {
406 fprintf( pFile, "a " );
407 Vec_IntForEachEntry( vForAlls, VarId, i )
408 fprintf( pFile, "%d ", fReadable? VarId : VarId+1 );
409 fprintf( pFile, "0\n" );
410 }
411 if ( vExists )
412 {
413 fprintf( pFile, "e " );
414 Vec_IntForEachEntry( vExists, VarId, i )
415 fprintf( pFile, "%d ", fReadable? VarId : VarId+1 );
416 fprintf( pFile, "0\n" );
417 }
418 for ( i = 0; i < p->nClauses; i++ )
419 {
420 for ( pLit = p->pClauses[i], pStop = p->pClauses[i+1]; pLit < pStop; pLit++ )
421 fprintf( pFile, "%d ", fReadable? Cnf_Lit2Var2(*pLit) : Cnf_Lit2Var(*pLit) );
422 fprintf( pFile, "0\n" );
423 }
424 fprintf( pFile, "\n" );
425 fclose( pFile );
426}
Cnf_DataWriteIntoFileGz
void Cnf_DataWriteIntoFileGz(Cnf_Dat_t *p, char *pFileName, int fReadable, Vec_Int_t *vForAlls, Vec_Int_t *vExists)
Definition cnfMan.c:298
strncmp
int strncmp()
strlen
int strlen()
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Cnf_DataWriteIntoFileInv()

void Cnf_DataWriteIntoFileInv ( Cnf_Dat_t * p,
char * pFileName,
int fReadable,
Vec_Int_t * vExists1,
Vec_Int_t * vForAlls,
Vec_Int_t * vExists2 )
extern

Definition at line 427 of file cnfMan.c.

428{
429 FILE * pFile;
430 int * pLit, * pStop, i, VarId;
431 if ( !strncmp(pFileName+strlen(pFileName)-3,".gz",3) )
432 {
433 Cnf_DataWriteIntoFileInvGz( p, pFileName, fReadable, vExists1, vForAlls, vExists2 );
434 return;
435 }
436 pFile = fopen( pFileName, "w" );
437 if ( pFile == NULL )
438 {
439 printf( "Cnf_WriteIntoFile(): Output file cannot be opened.\n" );
440 return;
441 }
442 fprintf( pFile, "c Result of efficient AIG-to-CNF conversion using package CNF\n" );
443 fprintf( pFile, "p cnf %d %d\n", p->nVars, p->nClauses );
444 if ( vExists1 )
445 {
446 fprintf( pFile, "e " );
447 Vec_IntForEachEntry( vExists1, VarId, i )
448 fprintf( pFile, "%d ", fReadable? VarId : VarId+1 );
449 fprintf( pFile, "0\n" );
450 }
451 if ( vForAlls )
452 {
453 fprintf( pFile, "a " );
454 Vec_IntForEachEntry( vForAlls, VarId, i )
455 fprintf( pFile, "%d ", fReadable? VarId : VarId+1 );
456 fprintf( pFile, "0\n" );
457 }
458 if ( vExists2 )
459 {
460 fprintf( pFile, "e " );
461 Vec_IntForEachEntry( vExists2, VarId, i )
462 fprintf( pFile, "%d ", fReadable? VarId : VarId+1 );
463 fprintf( pFile, "0\n" );
464 }
465 for ( i = 0; i < p->nClauses; i++ )
466 {
467 for ( pLit = p->pClauses[i], pStop = p->pClauses[i+1]; pLit < pStop; pLit++ )
468 fprintf( pFile, "%d ", fReadable? Cnf_Lit2Var2(*pLit) : Cnf_Lit2Var(*pLit) );
469 fprintf( pFile, "0\n" );
470 }
471 fprintf( pFile, "\n" );
472 fclose( pFile );
473}
Cnf_DataWriteIntoFileInvGz
void Cnf_DataWriteIntoFileInvGz(Cnf_Dat_t *p, char *pFileName, int fReadable, Vec_Int_t *vExists1, Vec_Int_t *vForAlls, Vec_Int_t *vExists2)
Definition cnfMan.c:333
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Cnf_DataWriteIntoSolver()

void * Cnf_DataWriteIntoSolver ( Cnf_Dat_t * p,
int nFrames,
int fInit )
extern

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

Synopsis [Writes CNF into a file.]

Description []

SideEffects []

SeeAlso []

Definition at line 579 of file cnfMan.c.

580{
581 return Cnf_DataWriteIntoSolverInt( sat_solver_new(), p, nFrames, fInit );
582}
Cnf_DataWriteIntoSolverInt
void * Cnf_DataWriteIntoSolverInt(void *pSolver, Cnf_Dat_t *p, int nFrames, int fInit)
Definition cnfMan.c:486
sat_solver_new
sat_solver * sat_solver_new(void)
Definition satSolver.c:1137

◆ Cnf_DataWriteIntoSolverInt()

void * Cnf_DataWriteIntoSolverInt ( void * pSolver,
Cnf_Dat_t * p,
int nFrames,
int fInit )
extern

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

Synopsis [Writes CNF into a file.]

Description []

SideEffects []

SeeAlso []

Definition at line 486 of file cnfMan.c.

487{
488 sat_solver * pSat = (sat_solver *)pSolver;
489 int i, f, status;
490 assert( nFrames > 0 );
491 assert( pSat );
492// pSat = sat_solver_new();
493 sat_solver_setnvars( pSat, p->nVars * nFrames );
494 for ( i = 0; i < p->nClauses; i++ )
495 {
496 if ( !sat_solver_addclause( pSat, p->pClauses[i], p->pClauses[i+1] ) )
497 {
498 sat_solver_delete( pSat );
499 return NULL;
500 }
501 }
502 if ( nFrames > 1 )
503 {
504 Aig_Obj_t * pObjLo, * pObjLi;
505 int nLitsAll, * pLits, Lits[2];
506 nLitsAll = 2 * p->nVars;
507 pLits = p->pClauses[0];
508 for ( f = 1; f < nFrames; f++ )
509 {
510 // add equality of register inputs/outputs for different timeframes
511 Aig_ManForEachLiLoSeq( p->pMan, pObjLi, pObjLo, i )
512 {
513 Lits[0] = (f-1)*nLitsAll + toLitCond( p->pVarNums[pObjLi->Id], 0 );
514 Lits[1] = f *nLitsAll + toLitCond( p->pVarNums[pObjLo->Id], 1 );
515 if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
516 {
517 sat_solver_delete( pSat );
518 return NULL;
519 }
520 Lits[0]++;
521 Lits[1]--;
522 if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
523 {
524 sat_solver_delete( pSat );
525 return NULL;
526 }
527 }
528 // add clauses for the next timeframe
529 for ( i = 0; i < p->nLiterals; i++ )
530 pLits[i] += nLitsAll;
531 for ( i = 0; i < p->nClauses; i++ )
532 {
533 if ( !sat_solver_addclause( pSat, p->pClauses[i], p->pClauses[i+1] ) )
534 {
535 sat_solver_delete( pSat );
536 return NULL;
537 }
538 }
539 }
540 // return literals to their original state
541 nLitsAll = (f-1) * nLitsAll;
542 for ( i = 0; i < p->nLiterals; i++ )
543 pLits[i] -= nLitsAll;
544 }
545 if ( fInit )
546 {
547 Aig_Obj_t * pObjLo;
548 int Lits[1];
549 Aig_ManForEachLoSeq( p->pMan, pObjLo, i )
550 {
551 Lits[0] = toLitCond( p->pVarNums[pObjLo->Id], 1 );
552 if ( !sat_solver_addclause( pSat, Lits, Lits + 1 ) )
553 {
554 sat_solver_delete( pSat );
555 return NULL;
556 }
557 }
558 }
559 status = sat_solver_simplify(pSat);
560 if ( status == 0 )
561 {
562 sat_solver_delete( pSat );
563 return NULL;
564 }
565 return pSat;
566}
Aig_ManForEachLoSeq
#define Aig_ManForEachLoSeq(p, pObj, i)
Definition aig.h:441
Aig_ManForEachLiLoSeq
#define Aig_ManForEachLiLoSeq(p, pObjLi, pObjLo, k)
Definition aig.h:450
sat_solver_simplify
int sat_solver_simplify(sat_solver *s)
Definition satSolver.c:1515
sat_solver_setnvars
void sat_solver_setnvars(sat_solver *s, int n)
Definition satSolver.c:1272
sat_solver_delete
void sat_solver_delete(sat_solver *s)
Definition satSolver.c:1341
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Cnf_DataWriteOrClause()

int Cnf_DataWriteOrClause ( void * p,
Cnf_Dat_t * pCnf )
extern

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

Synopsis [Adds the OR-clause.]

Description []

SideEffects []

SeeAlso []

Definition at line 687 of file cnfMan.c.

688{
689 sat_solver * pSat = (sat_solver *)p;
690 Aig_Obj_t * pObj;
691 int i, * pLits;
692 pLits = ABC_ALLOC( int, Aig_ManCoNum(pCnf->pMan) );
693 Aig_ManForEachCo( pCnf->pMan, pObj, i )
694 pLits[i] = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
695 if ( !sat_solver_addclause( pSat, pLits, pLits + Aig_ManCoNum(pCnf->pMan) ) )
696 {
697 ABC_FREE( pLits );
698 return 0;
699 }
700 ABC_FREE( pLits );
701 return 1;
702}
Here is the caller graph for this function:

◆ Cnf_Derive()

Cnf_Dat_t * Cnf_Derive ( Aig_Man_t * pAig,
int nOutputs )
extern

Definition at line 165 of file cnfCore.c.

166{
167 Cnf_ManPrepare();
168 return Cnf_DeriveWithMan( s_pManCnf, pAig, nOutputs );
169}
Cnf_ManPrepare
void Cnf_ManPrepare()
FUNCTION DEFINITIONS ///.
Definition cnfCore.c:46
Cnf_DeriveWithMan
Cnf_Dat_t * Cnf_DeriveWithMan(Cnf_Man_t *p, Aig_Man_t *pAig, int nOutputs)
Definition cnfCore.c:129
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Cnf_DeriveFast()

Cnf_Dat_t * Cnf_DeriveFast ( Aig_Man_t * p,
int nOutputs )
extern

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

Synopsis [Fast CNF computation.]

Description []

SideEffects []

SeeAlso []

Definition at line 666 of file cnfFast.c.

667{
668 Cnf_Dat_t * pCnf = NULL;
669 abctime clk;//, clkTotal = Abc_Clock();
670// printf( "\n" );
671 Aig_ManCleanMarkAB( p );
672 // create initial marking
673 clk = Abc_Clock();
674 Cnf_DeriveFastMark( p );
675// Abc_PrintTime( 1, "Marking", Abc_Clock() - clk );
676 // compute CNF size
677 clk = Abc_Clock();
678 pCnf = Cnf_DeriveFastClauses( p, nOutputs );
679// Abc_PrintTime( 1, "Clauses", Abc_Clock() - clk );
680 // derive the resulting CNF
681 Aig_ManCleanMarkA( p );
682// Abc_PrintTime( 1, "TOTAL ", Abc_Clock() - clkTotal );
683
684// printf( "CNF stats: Vars = %6d. Clauses = %7d. Literals = %8d. \n", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
685
686// Cnf_DataFree( pCnf );
687// pCnf = NULL;
688 return pCnf;
689}
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
Aig_ManCleanMarkA
void Aig_ManCleanMarkA(Aig_Man_t *p)
Definition aigUtil.c:148
Aig_ManCleanMarkAB
void Aig_ManCleanMarkAB(Aig_Man_t *p)
Definition aigUtil.c:186
Cnf_DeriveFastClauses
Cnf_Dat_t * Cnf_DeriveFastClauses(Aig_Man_t *p, int nOutputs)
Definition cnfFast.c:545
Cnf_DeriveFastMark
void Cnf_DeriveFastMark(Aig_Man_t *p)
Definition cnfFast.c:297
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Cnf_DeriveFastMark()

void Cnf_DeriveFastMark ( Aig_Man_t * p)
extern

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

Synopsis [Marks AIG for CNF computation.]

Description []

SideEffects []

SeeAlso []

Definition at line 297 of file cnfFast.c.

298{
299 Vec_Int_t * vSupps;
300 Vec_Ptr_t * vLeaves, * vNodes;
301 Aig_Obj_t * pObj, * pTemp, * pObjC, * pObj0, * pObj1;
302 int i, k, nFans, Counter;
303
304 vLeaves = Vec_PtrAlloc( 100 );
305 vNodes = Vec_PtrAlloc( 100 );
306 vSupps = Vec_IntStart( Aig_ManObjNumMax(p) );
307
308 // mark CIs
309 Aig_ManForEachCi( p, pObj, i )
310 pObj->fMarkA = 1;
311
312 // mark CO drivers
313 Aig_ManForEachCo( p, pObj, i )
314 Aig_ObjFanin0(pObj)->fMarkA = 1;
315
316 // mark MUX/XOR nodes
317 Aig_ManForEachNode( p, pObj, i )
318 {
319 assert( !pObj->fMarkB );
320 if ( !Aig_ObjIsMuxType(pObj) )
321 continue;
322 pObj0 = Aig_ObjFanin0(pObj);
323 if ( pObj0->fMarkB || Aig_ObjRefs(pObj0) > 1 )
324 continue;
325 pObj1 = Aig_ObjFanin1(pObj);
326 if ( pObj1->fMarkB || Aig_ObjRefs(pObj1) > 1 )
327 continue;
328 // mark nodes
329 pObj->fMarkB = 1;
330 pObj0->fMarkB = 1;
331 pObj1->fMarkB = 1;
332 // mark inputs and outputs
333 pObj->fMarkA = 1;
334 Aig_ObjFanin0(pObj0)->fMarkA = 1;
335 Aig_ObjFanin1(pObj0)->fMarkA = 1;
336 Aig_ObjFanin0(pObj1)->fMarkA = 1;
337 Aig_ObjFanin1(pObj1)->fMarkA = 1;
338 }
339
340 // mark nodes with multiple fanouts and pointed to by complemented edges
341 Aig_ManForEachNode( p, pObj, i )
342 {
343 // mark nodes with many fanouts
344 if ( Aig_ObjRefs(pObj) > 1 )
345 pObj->fMarkA = 1;
346 // mark nodes pointed to by a complemented edge
347 if ( Aig_ObjFaninC0(pObj) && !Aig_ObjFanin0(pObj)->fMarkB )
348 Aig_ObjFanin0(pObj)->fMarkA = 1;
349 if ( Aig_ObjFaninC1(pObj) && !Aig_ObjFanin1(pObj)->fMarkB )
350 Aig_ObjFanin1(pObj)->fMarkA = 1;
351 }
352
353 // compute supergate size for internal marked nodes
354 Aig_ManForEachNode( p, pObj, i )
355 {
356 if ( !pObj->fMarkA )
357 continue;
358 if ( pObj->fMarkB )
359 {
360 if ( !Aig_ObjIsMuxType(pObj) )
361 continue;
362 pObjC = Aig_ObjRecognizeMux( pObj, &pObj1, &pObj0 );
363 pObj0 = Aig_Regular(pObj0);
364 pObj1 = Aig_Regular(pObj1);
365 assert( pObj0->fMarkA );
366 assert( pObj1->fMarkA );
367// if ( pObj0 == pObj1 )
368// continue;
369 nFans = 1 + (pObj0 == pObj1);
370 if ( !pObj0->fMarkB && !Aig_ObjIsCi(pObj0) && Aig_ObjRefs(pObj0) == nFans && Vec_IntEntry(vSupps, Aig_ObjId(pObj0)) < 3 )
371 {
372 pObj0->fMarkA = 0;
373 continue;
374 }
375 if ( !pObj1->fMarkB && !Aig_ObjIsCi(pObj1) && Aig_ObjRefs(pObj1) == nFans && Vec_IntEntry(vSupps, Aig_ObjId(pObj1)) < 3 )
376 {
377 pObj1->fMarkA = 0;
378 continue;
379 }
380 continue;
381 }
382
383 Cnf_CollectLeaves( pObj, vLeaves, 1 );
384 Vec_IntWriteEntry( vSupps, Aig_ObjId(pObj), Vec_PtrSize(vLeaves) );
385 if ( Vec_PtrSize(vLeaves) >= 6 )
386 continue;
387 Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pTemp, k )
388 {
389 pTemp = Aig_Regular(pTemp);
390 assert( pTemp->fMarkA );
391 if ( pTemp->fMarkB || Aig_ObjIsCi(pTemp) || Aig_ObjRefs(pTemp) > 1 )
392 continue;
393 assert( Vec_IntEntry(vSupps, Aig_ObjId(pTemp)) > 0 );
394 if ( Vec_PtrSize(vLeaves) - 1 + Vec_IntEntry(vSupps, Aig_ObjId(pTemp)) > 6 )
395 continue;
396 pTemp->fMarkA = 0;
397 Vec_IntWriteEntry( vSupps, Aig_ObjId(pObj), 6 );
398//printf( "%d %d ", Vec_PtrSize(vLeaves), Vec_IntEntry(vSupps, Aig_ObjId(pTemp)) );
399 break;
400 }
401 }
402 Aig_ManCleanMarkB( p );
403
404 // check CO drivers
405 Counter = 0;
406 Aig_ManForEachCo( p, pObj, i )
407 Counter += !Aig_ObjFanin0(pObj)->fMarkA;
408 if ( Counter )
409 printf( "PO-driver rule is violated %d times.\n", Counter );
410
411 // check that the AND-gates are fine
412 Counter = 0;
413 Aig_ManForEachNode( p, pObj, i )
414 {
415 assert( pObj->fMarkB == 0 );
416 if ( !pObj->fMarkA )
417 continue;
418 Cnf_CollectLeaves( pObj, vLeaves, 0 );
419 if ( Vec_PtrSize(vLeaves) <= 6 )
420 continue;
421 Cnf_CollectVolume( p, pObj, vLeaves, vNodes );
422 Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pTemp, k )
423 {
424 if ( Aig_ObjFaninC0(pTemp) && !Aig_ObjFanin0(pTemp)->fMarkA )
425 Counter++;
426 if ( Aig_ObjFaninC1(pTemp) && !Aig_ObjFanin1(pTemp)->fMarkA )
427 Counter++;
428 }
429 }
430 if ( Counter )
431 printf( "AND-gate rule is violated %d times.\n", Counter );
432
433 Vec_PtrFree( vLeaves );
434 Vec_PtrFree( vNodes );
435 Vec_IntFree( vSupps );
436}
Aig_ObjRecognizeMux
Aig_Obj_t * Aig_ObjRecognizeMux(Aig_Obj_t *pObj, Aig_Obj_t **ppObjT, Aig_Obj_t **ppObjE)
Definition aigUtil.c:387
Aig_ManCleanMarkB
void Aig_ManCleanMarkB(Aig_Man_t *p)
Definition aigUtil.c:167
Aig_ManForEachNode
#define Aig_ManForEachNode(p, pObj, i)
Definition aig.h:413
Aig_ObjIsMuxType
int Aig_ObjIsMuxType(Aig_Obj_t *pObj)
Definition aigUtil.c:307
Aig_Obj_t_::fMarkB
unsigned int fMarkB
Definition aig.h:80
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Cnf_DeriveMapping()

void Cnf_DeriveMapping ( Cnf_Man_t * p)
extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 100 of file cnfMap.c.

101{
102 Vec_Ptr_t * vSuper;
103 Aig_Obj_t * pObj;
104 Dar_Cut_t * pCut, * pCutBest;
105 int i, k, AreaFlow, * pAreaFlows;
106 // allocate area flows
107 pAreaFlows = ABC_ALLOC( int, Aig_ManObjNumMax(p->pManAig) );
108 memset( pAreaFlows, 0, sizeof(int) * Aig_ManObjNumMax(p->pManAig) );
109 // visit the nodes in the topological order and update their best cuts
110 vSuper = Vec_PtrAlloc( 100 );
111 Aig_ManForEachNode( p->pManAig, pObj, i )
112 {
113 // go through the cuts
114 pCutBest = NULL;
115 Dar_ObjForEachCut( pObj, pCut, k )
116 {
117 pCut->fBest = 0;
118 if ( k == 0 )
119 continue;
120 Cnf_CutAssignAreaFlow( p, pCut, pAreaFlows );
121 if ( pCutBest == NULL || pCutBest->uSign > pCut->uSign ||
122 (pCutBest->uSign == pCut->uSign && pCutBest->Value < pCut->Value) )
123 pCutBest = pCut;
124 }
125 // check the big cut
126// Aig_ObjCollectSuper( pObj, vSuper );
127 // get the area flow of this cut
128// AreaFlow = Cnf_CutSuperAreaFlow( vSuper, pAreaFlows );
129 AreaFlow = ABC_INFINITY;
130 if ( AreaFlow >= (int)pCutBest->uSign )
131 {
132 pAreaFlows[pObj->Id] = pCutBest->uSign;
133 pCutBest->fBest = 1;
134 }
135 else
136 {
137 pAreaFlows[pObj->Id] = AreaFlow;
138 pObj->fMarkB = 1; // mark the special node
139 }
140 }
141 Vec_PtrFree( vSuper );
142 ABC_FREE( pAreaFlows );
143
144/*
145 // compute the area of mapping
146 AreaFlow = 0;
147 Aig_ManForEachCo( p->pManAig, pObj, i )
148 AreaFlow += Dar_ObjBestCut(Aig_ObjFanin0(pObj))->uSign / 100 / Aig_ObjFanin0(pObj)->nRefs;
149 printf( "Area of the network = %d.\n", AreaFlow );
150*/
151}
ABC_INFINITY
#define ABC_INFINITY
MACRO DEFINITIONS ///.
Definition abc_global.h:250
Cnf_CutAssignAreaFlow
ABC_NAMESPACE_IMPL_START void Cnf_CutAssignAreaFlow(Cnf_Man_t *p, Dar_Cut_t *pCut, int *pAreaFlows)
DECLARATIONS ///.
Definition cnfMap.c:45
Dar_ObjForEachCut
#define Dar_ObjForEachCut(pObj, pCut, i)
Definition darInt.h:121
Dar_Cut_t_::fBest
unsigned fBest
Definition darInt.h:60
Dar_Cut_t_::Value
unsigned Value
Definition darInt.h:59
Dar_Cut_t_::uSign
unsigned uSign
Definition darInt.h:57
memset
char * memset()
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Cnf_DeriveMappingArray()

Vec_Int_t * Cnf_DeriveMappingArray ( Aig_Man_t * pAig)
extern

FUNCTION DECLARATIONS ///.

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

Synopsis [Converts AIG into the SAT solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 78 of file cnfCore.c.

79{
80 Vec_Int_t * vResult;
81 Cnf_Man_t * p;
82 Vec_Ptr_t * vMapped;
83 Aig_MmFixed_t * pMemCuts;
84 abctime clk;
85 // allocate the CNF manager
86 p = Cnf_ManStart();
87 p->pManAig = pAig;
88
89 // generate cuts for all nodes, assign cost, and find best cuts
90clk = Abc_Clock();
91 pMemCuts = Dar_ManComputeCuts( pAig, 10, 0, 0 );
92p->timeCuts = Abc_Clock() - clk;
93
94 // find the mapping
95clk = Abc_Clock();
96 Cnf_DeriveMapping( p );
97p->timeMap = Abc_Clock() - clk;
98// Aig_ManScanMapping( p, 1 );
99
100 // convert it into CNF
101clk = Abc_Clock();
102 Cnf_ManTransferCuts( p );
103 vMapped = Cnf_ManScanMapping( p, 1, 0 );
104 vResult = Cnf_ManWriteCnfMapping( p, vMapped );
105 Vec_PtrFree( vMapped );
106 Aig_MmFixedStop( pMemCuts, 0 );
107p->timeSave = Abc_Clock() - clk;
108
109 // reset reference counters
110 Aig_ManResetRefs( pAig );
111//ABC_PRT( "Cuts ", p->timeCuts );
112//ABC_PRT( "Map ", p->timeMap );
113//ABC_PRT( "Saving ", p->timeSave );
114 Cnf_ManStop( p );
115 return vResult;
116}
Aig_ManResetRefs
void Aig_ManResetRefs(Aig_Man_t *p)
Definition aigUtil.c:122
Aig_MmFixed_t
struct Aig_MmFixed_t_ Aig_MmFixed_t
Definition aig.h:52
Aig_MmFixedStop
void Aig_MmFixedStop(Aig_MmFixed_t *p, int fVerbose)
Definition aigMem.c:132
Cnf_ManTransferCuts
void Cnf_ManTransferCuts(Cnf_Man_t *p)
Definition cnfPost.c:117
Cnf_Man_t
typedefABC_NAMESPACE_HEADER_START struct Cnf_Man_t_ Cnf_Man_t
INCLUDES ///.
Definition cnf.h:51
Cnf_ManStart
Cnf_Man_t * Cnf_ManStart()
FUNCTION DEFINITIONS ///.
Definition cnfMan.c:51
Cnf_DeriveMapping
void Cnf_DeriveMapping(Cnf_Man_t *p)
Definition cnfMap.c:100
Cnf_ManScanMapping
Vec_Ptr_t * Cnf_ManScanMapping(Cnf_Man_t *p, int fCollect, int fPreorder)
Definition cnfUtil.c:377
Cnf_ManStop
void Cnf_ManStop(Cnf_Man_t *p)
Definition cnfMan.c:82
Cnf_ManWriteCnfMapping
Vec_Int_t * Cnf_ManWriteCnfMapping(Cnf_Man_t *p, Vec_Ptr_t *vMapped)
DECLARATIONS ///.
Definition cnfWrite.c:45
Dar_ManComputeCuts
Aig_MmFixed_t * Dar_ManComputeCuts(Aig_Man_t *pAig, int nCutsMax, int fSkipTtMin, int fVerbose)
Definition darCore.c:291
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Cnf_DeriveOther()

Cnf_Dat_t * Cnf_DeriveOther ( Aig_Man_t * pAig,
int fSkipTtMin )
extern

Definition at line 219 of file cnfCore.c.

220{
221 Cnf_ManPrepare();
222 return Cnf_DeriveOtherWithMan( s_pManCnf, pAig, fSkipTtMin );
223}
Cnf_DeriveOtherWithMan
Cnf_Dat_t * Cnf_DeriveOtherWithMan(Cnf_Man_t *p, Aig_Man_t *pAig, int fSkipTtMin)
Definition cnfCore.c:182
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Cnf_DeriveOtherWithMan()

Cnf_Dat_t * Cnf_DeriveOtherWithMan ( Cnf_Man_t * p,
Aig_Man_t * pAig,
int fSkipTtMin )
extern

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

Synopsis [Converts AIG into the SAT solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 182 of file cnfCore.c.

183{
184 Cnf_Dat_t * pCnf;
185 Vec_Ptr_t * vMapped;
186 Aig_MmFixed_t * pMemCuts;
187 abctime clk;
188 // connect the managers
189 p->pManAig = pAig;
190
191 // generate cuts for all nodes, assign cost, and find best cuts
192clk = Abc_Clock();
193 pMemCuts = Dar_ManComputeCuts( pAig, 10, fSkipTtMin, 0 );
194p->timeCuts = Abc_Clock() - clk;
195
196 // find the mapping
197clk = Abc_Clock();
198 Cnf_DeriveMapping( p );
199p->timeMap = Abc_Clock() - clk;
200// Aig_ManScanMapping( p, 1 );
201
202 // convert it into CNF
203clk = Abc_Clock();
204 Cnf_ManTransferCuts( p );
205 vMapped = Cnf_ManScanMapping( p, 1, 1 );
206 pCnf = Cnf_ManWriteCnfOther( p, vMapped );
207 pCnf->vMapping = Cnf_ManWriteCnfMapping( p, vMapped );
208 Vec_PtrFree( vMapped );
209 Aig_MmFixedStop( pMemCuts, 0 );
210p->timeSave = Abc_Clock() - clk;
211
212 // reset reference counters
213 Aig_ManResetRefs( pAig );
214//ABC_PRT( "Cuts ", p->timeCuts );
215//ABC_PRT( "Map ", p->timeMap );
216//ABC_PRT( "Saving ", p->timeSave );
217 return pCnf;
218}
Cnf_ManWriteCnfOther
Cnf_Dat_t * Cnf_ManWriteCnfOther(Cnf_Man_t *p, Vec_Ptr_t *vMapped)
Definition cnfWrite.c:419
Cnf_Dat_t_::vMapping
Vec_Int_t * vMapping
Definition cnf.h:67
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Cnf_DeriveSimple()

Cnf_Dat_t * Cnf_DeriveSimple ( Aig_Man_t * p,
int nOutputs )
extern

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

Synopsis [Derives a simple CNF for the AIG.]

Description [The last argument lists the number of last outputs of the manager, which will not be converted into clauses. New variables will be introduced for these outputs.]

SideEffects []

SeeAlso []

Definition at line 587 of file cnfWrite.c.

588{
589 Aig_Obj_t * pObj;
590 Cnf_Dat_t * pCnf;
591 int OutVar, PoVar, pVars[32], * pLits, ** pClas;
592 int i, nLiterals, nClauses, Number;
593
594 // count the number of literals and clauses
595 nLiterals = 1 + 7 * Aig_ManNodeNum(p) + Aig_ManCoNum( p ) + 3 * nOutputs;
596 nClauses = 1 + 3 * Aig_ManNodeNum(p) + Aig_ManCoNum( p ) + nOutputs;
597
598 // allocate CNF
599 pCnf = ABC_ALLOC( Cnf_Dat_t, 1 );
600 memset( pCnf, 0, sizeof(Cnf_Dat_t) );
601 pCnf->pMan = p;
602 pCnf->nLiterals = nLiterals;
603 pCnf->nClauses = nClauses;
604 pCnf->pClauses = ABC_ALLOC( int *, nClauses + 1 );
605 pCnf->pClauses[0] = ABC_ALLOC( int, nLiterals );
606 pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals;
607
608 // create room for variable numbers
609 pCnf->pVarNums = ABC_ALLOC( int, Aig_ManObjNumMax(p) );
610// memset( pCnf->pVarNums, 0xff, sizeof(int) * Aig_ManObjNumMax(p) );
611 for ( i = 0; i < Aig_ManObjNumMax(p); i++ )
612 pCnf->pVarNums[i] = -1;
613 // assign variables to the last (nOutputs) POs
614 Number = 1;
615 if ( nOutputs )
616 {
617// assert( nOutputs == Aig_ManRegNum(p) );
618// Aig_ManForEachLiSeq( p, pObj, i )
619// pCnf->pVarNums[pObj->Id] = Number++;
620 Aig_ManForEachCo( p, pObj, i )
621 pCnf->pVarNums[pObj->Id] = Number++;
622 }
623 // assign variables to the internal nodes
624 Aig_ManForEachNode( p, pObj, i )
625 pCnf->pVarNums[pObj->Id] = Number++;
626 // assign variables to the PIs and constant node
627 Aig_ManForEachCi( p, pObj, i )
628 pCnf->pVarNums[pObj->Id] = Number++;
629 pCnf->pVarNums[Aig_ManConst1(p)->Id] = Number++;
630 pCnf->nVars = Number;
631/*
632 // print CNF numbers
633 printf( "SAT numbers of each node:\n" );
634 Aig_ManForEachObj( p, pObj, i )
635 printf( "%d=%d ", pObj->Id, pCnf->pVarNums[pObj->Id] );
636 printf( "\n" );
637*/
638 // assign the clauses
639 pLits = pCnf->pClauses[0];
640 pClas = pCnf->pClauses;
641 Aig_ManForEachNode( p, pObj, i )
642 {
643 OutVar = pCnf->pVarNums[ pObj->Id ];
644 pVars[0] = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
645 pVars[1] = pCnf->pVarNums[ Aig_ObjFanin1(pObj)->Id ];
646
647 // positive phase
648 *pClas++ = pLits;
649 *pLits++ = 2 * OutVar;
650 *pLits++ = 2 * pVars[0] + !Aig_ObjFaninC0(pObj);
651 *pLits++ = 2 * pVars[1] + !Aig_ObjFaninC1(pObj);
652 // negative phase
653 *pClas++ = pLits;
654 *pLits++ = 2 * OutVar + 1;
655 *pLits++ = 2 * pVars[0] + Aig_ObjFaninC0(pObj);
656 *pClas++ = pLits;
657 *pLits++ = 2 * OutVar + 1;
658 *pLits++ = 2 * pVars[1] + Aig_ObjFaninC1(pObj);
659 }
660
661 // write the constant literal
662 OutVar = pCnf->pVarNums[ Aig_ManConst1(p)->Id ];
663 assert( OutVar <= Aig_ManObjNumMax(p) );
664 *pClas++ = pLits;
665 *pLits++ = 2 * OutVar;
666
667 // write the output literals
668 Aig_ManForEachCo( p, pObj, i )
669 {
670 OutVar = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
671 if ( i < Aig_ManCoNum(p) - nOutputs )
672 {
673 *pClas++ = pLits;
674 *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj);
675 }
676 else
677 {
678 PoVar = pCnf->pVarNums[ pObj->Id ];
679 // first clause
680 *pClas++ = pLits;
681 *pLits++ = 2 * PoVar;
682 *pLits++ = 2 * OutVar + !Aig_ObjFaninC0(pObj);
683 // second clause
684 *pClas++ = pLits;
685 *pLits++ = 2 * PoVar + 1;
686 *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj);
687 }
688 }
689
690 // verify that the correct number of literals and clauses was written
691 assert( pLits - pCnf->pClauses[0] == nLiterals );
692 assert( pClas - pCnf->pClauses == nClauses );
693 return pCnf;
694}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Cnf_DeriveSimpleForRetiming()

Cnf_Dat_t * Cnf_DeriveSimpleForRetiming ( Aig_Man_t * p)
extern

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

Synopsis [Derives a simple CNF for backward retiming computation.]

Description [The last argument shows the number of last outputs of the manager, which will not be converted into clauses. New variables will be introduced for these outputs.]

SideEffects []

SeeAlso []

Definition at line 709 of file cnfWrite.c.

710{
711 Aig_Obj_t * pObj;
712 Cnf_Dat_t * pCnf;
713 int OutVar, PoVar, pVars[32], * pLits, ** pClas;
714 int i, nLiterals, nClauses, Number;
715
716 // count the number of literals and clauses
717 nLiterals = 1 + 7 * Aig_ManNodeNum(p) + 5 * Aig_ManCoNum(p);
718 nClauses = 1 + 3 * Aig_ManNodeNum(p) + 3 * Aig_ManCoNum(p);
719
720 // allocate CNF
721 pCnf = ABC_ALLOC( Cnf_Dat_t, 1 );
722 memset( pCnf, 0, sizeof(Cnf_Dat_t) );
723 pCnf->pMan = p;
724 pCnf->nLiterals = nLiterals;
725 pCnf->nClauses = nClauses;
726 pCnf->pClauses = ABC_ALLOC( int *, nClauses + 1 );
727 pCnf->pClauses[0] = ABC_ALLOC( int, nLiterals );
728 pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals;
729
730 // create room for variable numbers
731 pCnf->pVarNums = ABC_ALLOC( int, Aig_ManObjNumMax(p) );
732// memset( pCnf->pVarNums, 0xff, sizeof(int) * Aig_ManObjNumMax(p) );
733 for ( i = 0; i < Aig_ManObjNumMax(p); i++ )
734 pCnf->pVarNums[i] = -1;
735 // assign variables to the last (nOutputs) POs
736 Number = 1;
737 Aig_ManForEachCo( p, pObj, i )
738 pCnf->pVarNums[pObj->Id] = Number++;
739 // assign variables to the internal nodes
740 Aig_ManForEachNode( p, pObj, i )
741 pCnf->pVarNums[pObj->Id] = Number++;
742 // assign variables to the PIs and constant node
743 Aig_ManForEachCi( p, pObj, i )
744 pCnf->pVarNums[pObj->Id] = Number++;
745 pCnf->pVarNums[Aig_ManConst1(p)->Id] = Number++;
746 pCnf->nVars = Number;
747 // assign the clauses
748 pLits = pCnf->pClauses[0];
749 pClas = pCnf->pClauses;
750 Aig_ManForEachNode( p, pObj, i )
751 {
752 OutVar = pCnf->pVarNums[ pObj->Id ];
753 pVars[0] = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
754 pVars[1] = pCnf->pVarNums[ Aig_ObjFanin1(pObj)->Id ];
755
756 // positive phase
757 *pClas++ = pLits;
758 *pLits++ = 2 * OutVar;
759 *pLits++ = 2 * pVars[0] + !Aig_ObjFaninC0(pObj);
760 *pLits++ = 2 * pVars[1] + !Aig_ObjFaninC1(pObj);
761 // negative phase
762 *pClas++ = pLits;
763 *pLits++ = 2 * OutVar + 1;
764 *pLits++ = 2 * pVars[0] + Aig_ObjFaninC0(pObj);
765 *pClas++ = pLits;
766 *pLits++ = 2 * OutVar + 1;
767 *pLits++ = 2 * pVars[1] + Aig_ObjFaninC1(pObj);
768 }
769
770 // write the constant literal
771 OutVar = pCnf->pVarNums[ Aig_ManConst1(p)->Id ];
772 assert( OutVar <= Aig_ManObjNumMax(p) );
773 *pClas++ = pLits;
774 *pLits++ = 2 * OutVar;
775
776 // write the output literals
777 Aig_ManForEachCo( p, pObj, i )
778 {
779 OutVar = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
780 PoVar = pCnf->pVarNums[ pObj->Id ];
781 // first clause
782 *pClas++ = pLits;
783 *pLits++ = 2 * PoVar;
784 *pLits++ = 2 * OutVar + !Aig_ObjFaninC0(pObj);
785 // second clause
786 *pClas++ = pLits;
787 *pLits++ = 2 * PoVar + 1;
788 *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj);
789 // final clause (init-state is always 0 -> set the output to 0)
790 *pClas++ = pLits;
791 *pLits++ = 2 * PoVar + 1;
792 }
793
794 // verify that the correct number of literals and clauses was written
795 assert( pLits - pCnf->pClauses[0] == nLiterals );
796 assert( pClas - pCnf->pClauses == nClauses );
797 return pCnf;
798}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Cnf_DeriveWithMan()

Cnf_Dat_t * Cnf_DeriveWithMan ( Cnf_Man_t * p,
Aig_Man_t * pAig,
int nOutputs )
extern

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

Synopsis [Converts AIG into the SAT solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 129 of file cnfCore.c.

130{
131 Cnf_Dat_t * pCnf;
132 Vec_Ptr_t * vMapped;
133 Aig_MmFixed_t * pMemCuts;
134 abctime clk;
135 // connect the managers
136 p->pManAig = pAig;
137
138 // generate cuts for all nodes, assign cost, and find best cuts
139clk = Abc_Clock();
140 pMemCuts = Dar_ManComputeCuts( pAig, 10, 0, 0 );
141p->timeCuts = Abc_Clock() - clk;
142
143 // find the mapping
144clk = Abc_Clock();
145 Cnf_DeriveMapping( p );
146p->timeMap = Abc_Clock() - clk;
147// Aig_ManScanMapping( p, 1 );
148
149 // convert it into CNF
150clk = Abc_Clock();
151 Cnf_ManTransferCuts( p );
152 vMapped = Cnf_ManScanMapping( p, 1, 1 );
153 pCnf = Cnf_ManWriteCnf( p, vMapped, nOutputs );
154 Vec_PtrFree( vMapped );
155 Aig_MmFixedStop( pMemCuts, 0 );
156p->timeSave = Abc_Clock() - clk;
157
158 // reset reference counters
159 Aig_ManResetRefs( pAig );
160//ABC_PRT( "Cuts ", p->timeCuts );
161//ABC_PRT( "Map ", p->timeMap );
162//ABC_PRT( "Saving ", p->timeSave );
163 return pCnf;
164}
Cnf_ManWriteCnf
Cnf_Dat_t * Cnf_ManWriteCnf(Cnf_Man_t *p, Vec_Ptr_t *vMapped, int nOutputs)
Definition cnfWrite.c:199
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Cnf_ManFree()

void Cnf_ManFree ( )
extern

Definition at line 58 of file cnfCore.c.

59{
60 if ( s_pManCnf == NULL )
61 return;
62 Cnf_ManStop( s_pManCnf );
63 s_pManCnf = NULL;
64}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Cnf_ManFreeCuts()

void Cnf_ManFreeCuts ( Cnf_Man_t * p)
extern

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

Synopsis [Transfers cuts of the mapped nodes into internal representation.]

Description []

SideEffects []

SeeAlso []

Definition at line 142 of file cnfPost.c.

143{
144 Aig_Obj_t * pObj;
145 int i;
146 Aig_ManForEachObj( p->pManAig, pObj, i )
147 if ( pObj->pData )
148 {
149 Cnf_CutFree( (Cnf_Cut_t *)pObj->pData );
150 pObj->pData = NULL;
151 }
152}
Cnf_CutFree
void Cnf_CutFree(Cnf_Cut_t *pCut)
Definition cnfCut.c:68
Aig_Obj_t_::pData
void * pData
Definition aig.h:87
Here is the call graph for this function:

◆ Cnf_ManMapForCnf()

int Cnf_ManMapForCnf ( Cnf_Man_t * p)
extern

◆ Cnf_ManPostprocess()

void Cnf_ManPostprocess ( Cnf_Man_t * p)
extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 165 of file cnfPost.c.

166{
167 Cnf_Cut_t * pCut, * pCutFan, * pCutRes;
168 Aig_Obj_t * pObj, * pFan;
169 int Order[16], Costs[16];
170 int i, k, fChanges;
171 Aig_ManForEachNode( p->pManAig, pObj, i )
172 {
173 if ( pObj->nRefs == 0 )
174 continue;
175 pCut = Cnf_ObjBestCut(pObj);
176
177 // sort fanins according to their size
178 Cnf_CutForEachLeaf( p->pManAig, pCut, pFan, k )
179 {
180 Order[k] = k;
181 Costs[k] = Aig_ObjIsNode(pFan)? Cnf_ObjBestCut(pFan)->Cost : 0;
182 }
183 // sort the cuts by Weight
184 do {
185 int Temp;
186 fChanges = 0;
187 for ( k = 0; k < pCut->nFanins - 1; k++ )
188 {
189 if ( Costs[Order[k]] <= Costs[Order[k+1]] )
190 continue;
191 Temp = Order[k];
192 Order[k] = Order[k+1];
193 Order[k+1] = Temp;
194 fChanges = 1;
195 }
196 } while ( fChanges );
197
198
199// Cnf_CutForEachLeaf( p->pManAig, pCut, pFan, k )
200 for ( k = 0; (k < (int)(pCut)->nFanins) && ((pFan) = Aig_ManObj(p->pManAig, (pCut)->pFanins[Order[k]])); k++ )
201 {
202 if ( !Aig_ObjIsNode(pFan) )
203 continue;
204 assert( pFan->nRefs != 0 );
205 if ( pFan->nRefs != 1 )
206 continue;
207 pCutFan = Cnf_ObjBestCut(pFan);
208 // try composing these two cuts
209// Cnf_CutPrint( pCut );
210 pCutRes = Cnf_CutCompose( p, pCut, pCutFan, pFan->Id );
211// Cnf_CutPrint( pCut );
212// printf( "\n" );
213 // check if the cost if reduced
214 if ( pCutRes == NULL || pCutRes->Cost == 127 || pCutRes->Cost > pCut->Cost + pCutFan->Cost )
215 {
216 if ( pCutRes )
217 Cnf_CutFree( pCutRes );
218 continue;
219 }
220 // update the cut
221 Cnf_ObjSetBestCut( pObj, pCutRes );
222 Cnf_ObjSetBestCut( pFan, NULL );
223 Cnf_CutUpdateRefs( p, pCut, pCutFan, pCutRes );
224 assert( pFan->nRefs == 0 );
225 Cnf_CutFree( pCut );
226 Cnf_CutFree( pCutFan );
227 break;
228 }
229 }
230}
Cnf_CutUpdateRefs
void Cnf_CutUpdateRefs(Cnf_Man_t *p, Cnf_Cut_t *pCut, Cnf_Cut_t *pCutFan, Cnf_Cut_t *pCutRes)
Definition cnfCut.c:178
Cnf_CutCompose
Cnf_Cut_t * Cnf_CutCompose(Cnf_Man_t *p, Cnf_Cut_t *pCut, Cnf_Cut_t *pCutFan, int iFan)
Definition cnfCut.c:294
Cnf_CutForEachLeaf
#define Cnf_CutForEachLeaf(p, pCut, pLeaf, i)
Definition cnf.h:121
Here is the call graph for this function:

◆ Cnf_ManPrepare()

void Cnf_ManPrepare ( )
extern

FUNCTION DEFINITIONS ///.

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file cnfCore.c.

47{
48 if ( s_pManCnf == NULL )
49 {
50// printf( "\n\nCreating CNF manager!!!!!\n\n" );
51 s_pManCnf = Cnf_ManStart();
52 }
53}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Cnf_ManRead()

Cnf_Man_t * Cnf_ManRead ( )
extern

Definition at line 54 of file cnfCore.c.

55{
56 return s_pManCnf;
57}

◆ Cnf_ManScanMapping()

Vec_Ptr_t * Cnf_ManScanMapping ( Cnf_Man_t * p,
int fCollect,
int fPreorder )
extern

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

Synopsis [Computes area, references, and nodes used in the mapping.]

Description [Collects the nodes in reverse topological order.]

SideEffects []

SeeAlso []

Definition at line 377 of file cnfUtil.c.

378{
379 Vec_Ptr_t *vMapped = NULL;
380 Aig_Obj_t *pObj;
381 int i;
382 // clean all references
383 Aig_ManForEachObj(p->pManAig, pObj, i)
384 pObj->nRefs = 0;
385 // allocate the array
386 if (fCollect)
387 vMapped = Vec_PtrAlloc(1000);
388 // collect nodes reachable from POs in the DFS order through the best cuts
389 p->aArea = 0;
390 Aig_ManForEachCo(p->pManAig, pObj, i)
391 p->aArea += Cnf_ManScanMapping_rec(p, Aig_ObjFanin0(pObj), vMapped, fPreorder);
392 // printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) + Aig_ManCiNum(p->pManAig) + 1 : 0, p->aArea + 2 );
393 return vMapped;
394}
Cnf_ManScanMapping_rec
int Cnf_ManScanMapping_rec(Cnf_Man_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vMapped, int fPreorder)
Definition cnfUtil.c:327
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Cnf_ManStart()

Cnf_Man_t * Cnf_ManStart ( )
extern

FUNCTION DEFINITIONS ///.

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

Synopsis [Starts the fraiging manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 51 of file cnfMan.c.

52{
53 Cnf_Man_t * p;
54 int i;
55 // allocate the manager
56 p = ABC_ALLOC( Cnf_Man_t, 1 );
57 memset( p, 0, sizeof(Cnf_Man_t) );
58 // derive internal data structures
59 Cnf_ReadMsops( &p->pSopSizes, &p->pSops );
60 // allocate memory manager for cuts
61 p->pMemCuts = Aig_MmFlexStart();
62 p->nMergeLimit = 10;
63 // allocate temporary truth tables
64 p->pTruths[0] = ABC_ALLOC( unsigned, 4 * Abc_TruthWordNum(p->nMergeLimit) );
65 for ( i = 1; i < 4; i++ )
66 p->pTruths[i] = p->pTruths[i-1] + Abc_TruthWordNum(p->nMergeLimit);
67 p->vMemory = Vec_IntAlloc( 1 << 18 );
68 return p;
69}
Aig_MmFlexStart
Aig_MmFlex_t * Aig_MmFlexStart()
Definition aigMem.c:305
Cnf_ReadMsops
void Cnf_ReadMsops(char **ppSopSizes, char ***ppSops)
FUNCTION DEFINITIONS ///.
Definition cnfData.c:4537
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Cnf_ManStop()

void Cnf_ManStop ( Cnf_Man_t * p)
extern

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

Synopsis [Stops the fraiging manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 82 of file cnfMan.c.

83{
84 Vec_IntFree( p->vMemory );
85 ABC_FREE( p->pTruths[0] );
86 Aig_MmFlexStop( p->pMemCuts, 0 );
87 ABC_FREE( p->pSopSizes );
88 ABC_FREE( p->pSops[1] );
89 ABC_FREE( p->pSops );
90 ABC_FREE( p );
91}
Aig_MmFlexStop
void Aig_MmFlexStop(Aig_MmFlex_t *p, int fVerbose)
Definition aigMem.c:337
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Cnf_ManTransferCuts()

void Cnf_ManTransferCuts ( Cnf_Man_t * p)
extern

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

Synopsis [Transfers cuts of the mapped nodes into internal representation.]

Description []

SideEffects []

SeeAlso []

Definition at line 117 of file cnfPost.c.

118{
119 Aig_Obj_t * pObj;
120 int i;
121 Aig_MmFlexRestart( p->pMemCuts );
122 Aig_ManForEachObj( p->pManAig, pObj, i )
123 {
124 if ( Aig_ObjIsNode(pObj) && pObj->nRefs > 0 )
125 pObj->pData = Cnf_CutCreate( p, pObj );
126 else
127 pObj->pData = NULL;
128 }
129}
Aig_MmFlexRestart
void Aig_MmFlexRestart(Aig_MmFlex_t *p)
Definition aigMem.c:415
Cnf_CutCreate
Cnf_Cut_t * Cnf_CutCreate(Cnf_Man_t *p, Aig_Obj_t *pObj)
Definition cnfCut.c:87
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Cnf_ManWriteCnf()

Cnf_Dat_t * Cnf_ManWriteCnf ( Cnf_Man_t * p,
Vec_Ptr_t * vMapped,
int nOutputs )
extern

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

Synopsis [Derives CNF for the mapping.]

Description [The last argument shows the number of last outputs of the manager, which will not be converted into clauses but the new variables for which will be introduced.]

SideEffects []

SeeAlso []

Definition at line 199 of file cnfWrite.c.

200{
201 int fChangeVariableOrder = 0; // should be set to 0 to improve performance
202 Aig_Obj_t * pObj;
203 Cnf_Dat_t * pCnf;
204 Cnf_Cut_t * pCut;
205 Vec_Int_t * vCover, * vSopTemp;
206 int OutVar, PoVar, pVars[32], * pLits, ** pClas;
207 unsigned uTruth;
208 int i, k, nLiterals, nClauses, Cube, Number;
209
210 // count the number of literals and clauses
211 nLiterals = 1 + Aig_ManCoNum( p->pManAig ) + 3 * nOutputs;
212 nClauses = 1 + Aig_ManCoNum( p->pManAig ) + nOutputs;
213 Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i )
214 {
215 assert( Aig_ObjIsNode(pObj) );
216 pCut = Cnf_ObjBestCut( pObj );
217
218 // positive polarity of the cut
219 if ( pCut->nFanins < 5 )
220 {
221 uTruth = 0xFFFF & *Cnf_CutTruth(pCut);
222 nLiterals += Cnf_SopCountLiterals( p->pSops[uTruth], p->pSopSizes[uTruth] ) + p->pSopSizes[uTruth];
223 assert( p->pSopSizes[uTruth] >= 0 );
224 nClauses += p->pSopSizes[uTruth];
225 }
226 else
227 {
228 nLiterals += Cnf_IsopCountLiterals( pCut->vIsop[1], pCut->nFanins ) + Vec_IntSize(pCut->vIsop[1]);
229 nClauses += Vec_IntSize(pCut->vIsop[1]);
230 }
231 // negative polarity of the cut
232 if ( pCut->nFanins < 5 )
233 {
234 uTruth = 0xFFFF & ~*Cnf_CutTruth(pCut);
235 nLiterals += Cnf_SopCountLiterals( p->pSops[uTruth], p->pSopSizes[uTruth] ) + p->pSopSizes[uTruth];
236 assert( p->pSopSizes[uTruth] >= 0 );
237 nClauses += p->pSopSizes[uTruth];
238 }
239 else
240 {
241 nLiterals += Cnf_IsopCountLiterals( pCut->vIsop[0], pCut->nFanins ) + Vec_IntSize(pCut->vIsop[0]);
242 nClauses += Vec_IntSize(pCut->vIsop[0]);
243 }
244//printf( "%d ", nClauses-(1 + Aig_ManCoNum( p->pManAig )) );
245 }
246//printf( "\n" );
247
248 // allocate CNF
249 pCnf = ABC_CALLOC( Cnf_Dat_t, 1 );
250 pCnf->pMan = p->pManAig;
251 pCnf->nLiterals = nLiterals;
252 pCnf->nClauses = nClauses;
253 pCnf->pClauses = ABC_ALLOC( int *, nClauses + 1 );
254 pCnf->pClauses[0] = ABC_ALLOC( int, nLiterals );
255 pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals;
256 // create room for variable numbers
257 pCnf->pVarNums = ABC_ALLOC( int, Aig_ManObjNumMax(p->pManAig) );
258// memset( pCnf->pVarNums, 0xff, sizeof(int) * Aig_ManObjNumMax(p->pManAig) );
259 for ( i = 0; i < Aig_ManObjNumMax(p->pManAig); i++ )
260 pCnf->pVarNums[i] = -1;
261
262 if ( !fChangeVariableOrder )
263 {
264 // assign variables to the last (nOutputs) POs
265 Number = 1;
266 if ( nOutputs )
267 {
268 if ( Aig_ManRegNum(p->pManAig) == 0 )
269 {
270 assert( nOutputs == Aig_ManCoNum(p->pManAig) );
271 Aig_ManForEachCo( p->pManAig, pObj, i )
272 pCnf->pVarNums[pObj->Id] = Number++;
273 }
274 else
275 {
276 assert( nOutputs == Aig_ManRegNum(p->pManAig) );
277 Aig_ManForEachLiSeq( p->pManAig, pObj, i )
278 pCnf->pVarNums[pObj->Id] = Number++;
279 }
280 }
281 // assign variables to the internal nodes
282 Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i )
283 pCnf->pVarNums[pObj->Id] = Number++;
284 // assign variables to the PIs and constant node
285 Aig_ManForEachCi( p->pManAig, pObj, i )
286 pCnf->pVarNums[pObj->Id] = Number++;
287 pCnf->pVarNums[Aig_ManConst1(p->pManAig)->Id] = Number++;
288 pCnf->nVars = Number;
289 }
290 else
291 {
292 // assign variables to the last (nOutputs) POs
293 Number = Aig_ManObjNumMax(p->pManAig) + 1;
294 pCnf->nVars = Number + 1;
295 if ( nOutputs )
296 {
297 if ( Aig_ManRegNum(p->pManAig) == 0 )
298 {
299 assert( nOutputs == Aig_ManCoNum(p->pManAig) );
300 Aig_ManForEachCo( p->pManAig, pObj, i )
301 pCnf->pVarNums[pObj->Id] = Number--;
302 }
303 else
304 {
305 assert( nOutputs == Aig_ManRegNum(p->pManAig) );
306 Aig_ManForEachLiSeq( p->pManAig, pObj, i )
307 pCnf->pVarNums[pObj->Id] = Number--;
308 }
309 }
310 // assign variables to the internal nodes
311 Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i )
312 pCnf->pVarNums[pObj->Id] = Number--;
313 // assign variables to the PIs and constant node
314 Aig_ManForEachCi( p->pManAig, pObj, i )
315 pCnf->pVarNums[pObj->Id] = Number--;
316 pCnf->pVarNums[Aig_ManConst1(p->pManAig)->Id] = Number--;
317 assert( Number >= 0 );
318 }
319
320 // assign the clauses
321 vSopTemp = Vec_IntAlloc( 1 << 16 );
322 pLits = pCnf->pClauses[0];
323 pClas = pCnf->pClauses;
324 Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i )
325 {
326 pCut = Cnf_ObjBestCut( pObj );
327
328 // save variables of this cut
329 OutVar = pCnf->pVarNums[ pObj->Id ];
330 for ( k = 0; k < (int)pCut->nFanins; k++ )
331 {
332 pVars[k] = pCnf->pVarNums[ pCut->pFanins[k] ];
333 assert( pVars[k] <= Aig_ManObjNumMax(p->pManAig) );
334 }
335
336 // positive polarity of the cut
337 if ( pCut->nFanins < 5 )
338 {
339 uTruth = 0xFFFF & *Cnf_CutTruth(pCut);
340 Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vSopTemp );
341 vCover = vSopTemp;
342 }
343 else
344 vCover = pCut->vIsop[1];
345 Vec_IntForEachEntry( vCover, Cube, k )
346 {
347 *pClas++ = pLits;
348 *pLits++ = 2 * OutVar;
349 pLits += Cnf_IsopWriteCube( Cube, pCut->nFanins, pVars, pLits );
350 }
351
352 // negative polarity of the cut
353 if ( pCut->nFanins < 5 )
354 {
355 uTruth = 0xFFFF & ~*Cnf_CutTruth(pCut);
356 Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vSopTemp );
357 vCover = vSopTemp;
358 }
359 else
360 vCover = pCut->vIsop[0];
361 Vec_IntForEachEntry( vCover, Cube, k )
362 {
363 *pClas++ = pLits;
364 *pLits++ = 2 * OutVar + 1;
365 pLits += Cnf_IsopWriteCube( Cube, pCut->nFanins, pVars, pLits );
366 }
367 }
368 Vec_IntFree( vSopTemp );
369
370 // write the constant literal
371 OutVar = pCnf->pVarNums[ Aig_ManConst1(p->pManAig)->Id ];
372 assert( OutVar <= Aig_ManObjNumMax(p->pManAig) );
373 *pClas++ = pLits;
374 *pLits++ = 2 * OutVar;
375
376 // write the output literals
377 Aig_ManForEachCo( p->pManAig, pObj, i )
378 {
379 OutVar = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
380 if ( i < Aig_ManCoNum(p->pManAig) - nOutputs )
381 {
382 *pClas++ = pLits;
383 *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj);
384 }
385 else
386 {
387 PoVar = pCnf->pVarNums[ pObj->Id ];
388 // first clause
389 *pClas++ = pLits;
390 *pLits++ = 2 * PoVar;
391 *pLits++ = 2 * OutVar + !Aig_ObjFaninC0(pObj);
392 // second clause
393 *pClas++ = pLits;
394 *pLits++ = 2 * PoVar + 1;
395 *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj);
396 }
397 }
398
399 // verify that the correct number of literals and clauses was written
400 assert( pLits - pCnf->pClauses[0] == nLiterals );
401 assert( pClas - pCnf->pClauses == nClauses );
402//Cnf_DataPrint( pCnf, 1 );
403 return pCnf;
404}
Aig_ManForEachLiSeq
#define Aig_ManForEachLiSeq(p, pObj, i)
Definition aig.h:447
Cnf_IsopWriteCube
int Cnf_IsopWriteCube(int Cube, int nVars, int *pVars, int *pLiterals)
Definition cnfWrite.c:170
Cnf_IsopCountLiterals
int Cnf_IsopCountLiterals(Vec_Int_t *vIsop, int nVars)
Definition cnfWrite.c:144
Cnf_SopConvertToVector
void Cnf_SopConvertToVector(char *pSop, int nCubes, Vec_Int_t *vCover)
Definition cnfWrite.c:82
Cnf_SopCountLiterals
int Cnf_SopCountLiterals(char *pSop, int nCubes)
Definition cnfWrite.c:117
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Cnf_ManWriteCnfMapping()

Vec_Int_t * Cnf_ManWriteCnfMapping ( Cnf_Man_t * p,
Vec_Ptr_t * vMapped )
extern

DECLARATIONS ///.

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

FileName [cnfWrite.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [AIG-to-CNF conversion.]

Synopsis []

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - April 28, 2007.]

Revision [

Id
cnfWrite.c,v 1.00 2007/04/28 00:00:00 alanmi Exp

] FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Derives CNF mapping.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file cnfWrite.c.

46{
47 Vec_Int_t * vResult;
48 Aig_Obj_t * pObj;
49 Cnf_Cut_t * pCut;
50 int i, k, nOffset;
51 nOffset = Aig_ManObjNumMax(p->pManAig);
52 vResult = Vec_IntStart( nOffset );
53 Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i )
54 {
55 assert( Aig_ObjIsNode(pObj) );
56 pCut = Cnf_ObjBestCut( pObj );
57 assert( pCut->nFanins < 5 );
58 Vec_IntWriteEntry( vResult, Aig_ObjId(pObj), nOffset );
59 Vec_IntPush( vResult, *Cnf_CutTruth(pCut) );
60 for ( k = 0; k < pCut->nFanins; k++ )
61 Vec_IntPush( vResult, pCut->pFanins[k] );
62 for ( ; k < 4; k++ )
63 Vec_IntPush( vResult, -1 );
64 nOffset += 5;
65 }
66 return vResult;
67}
Here is the caller graph for this function:

◆ Cnf_ManWriteCnfOther()

Cnf_Dat_t * Cnf_ManWriteCnfOther ( Cnf_Man_t * p,
Vec_Ptr_t * vMapped )
extern

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

Synopsis [Derives CNF for the mapping.]

Description [Derives CNF with obj IDs as SAT vars and mapping of objects into clauses (pObj2Clause and pObj2Count).]

SideEffects []

SeeAlso []

Definition at line 419 of file cnfWrite.c.

420{
421 Aig_Obj_t * pObj;
422 Cnf_Dat_t * pCnf;
423 Cnf_Cut_t * pCut;
424 Vec_Int_t * vCover, * vSopTemp;
425 int OutVar, PoVar, pVars[32], * pLits, ** pClas;
426 unsigned uTruth;
427 int i, k, nLiterals, nClauses, Cube;
428
429 // count the number of literals and clauses
430 nLiterals = 1 + 4 * Aig_ManCoNum( p->pManAig );
431 nClauses = 1 + 2 * Aig_ManCoNum( p->pManAig );
432 Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i )
433 {
434 assert( Aig_ObjIsNode(pObj) );
435 pCut = Cnf_ObjBestCut( pObj );
436 // positive polarity of the cut
437 if ( pCut->nFanins < 5 )
438 {
439 uTruth = 0xFFFF & *Cnf_CutTruth(pCut);
440 nLiterals += Cnf_SopCountLiterals( p->pSops[uTruth], p->pSopSizes[uTruth] ) + p->pSopSizes[uTruth];
441 assert( p->pSopSizes[uTruth] >= 0 );
442 nClauses += p->pSopSizes[uTruth];
443 }
444 else
445 {
446 nLiterals += Cnf_IsopCountLiterals( pCut->vIsop[1], pCut->nFanins ) + Vec_IntSize(pCut->vIsop[1]);
447 nClauses += Vec_IntSize(pCut->vIsop[1]);
448 }
449 // negative polarity of the cut
450 if ( pCut->nFanins < 5 )
451 {
452 uTruth = 0xFFFF & ~*Cnf_CutTruth(pCut);
453 nLiterals += Cnf_SopCountLiterals( p->pSops[uTruth], p->pSopSizes[uTruth] ) + p->pSopSizes[uTruth];
454 assert( p->pSopSizes[uTruth] >= 0 );
455 nClauses += p->pSopSizes[uTruth];
456 }
457 else
458 {
459 nLiterals += Cnf_IsopCountLiterals( pCut->vIsop[0], pCut->nFanins ) + Vec_IntSize(pCut->vIsop[0]);
460 nClauses += Vec_IntSize(pCut->vIsop[0]);
461 }
462 }
463
464 // allocate CNF
465 pCnf = ABC_CALLOC( Cnf_Dat_t, 1 );
466 pCnf->pMan = p->pManAig;
467 pCnf->nLiterals = nLiterals;
468 pCnf->nClauses = nClauses;
469 pCnf->pClauses = ABC_ALLOC( int *, nClauses + 1 );
470 pCnf->pClauses[0] = ABC_ALLOC( int, nLiterals );
471 pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals;
472 // create room for variable numbers
473 pCnf->pObj2Clause = ABC_ALLOC( int, Aig_ManObjNumMax(p->pManAig) );
474 pCnf->pObj2Count = ABC_ALLOC( int, Aig_ManObjNumMax(p->pManAig) );
475 for ( i = 0; i < Aig_ManObjNumMax(p->pManAig); i++ )
476 pCnf->pObj2Clause[i] = pCnf->pObj2Count[i] = -1;
477 pCnf->nVars = Aig_ManObjNumMax(p->pManAig);
478
479 // clear the PI counters
480 Aig_ManForEachCi( p->pManAig, pObj, i )
481 pCnf->pObj2Count[pObj->Id] = 0;
482
483 // assign the clauses
484 vSopTemp = Vec_IntAlloc( 1 << 16 );
485 pLits = pCnf->pClauses[0];
486 pClas = pCnf->pClauses;
487 Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i )
488 {
489 // remember the starting clause
490 pCnf->pObj2Clause[pObj->Id] = pClas - pCnf->pClauses;
491 pCnf->pObj2Count[pObj->Id] = 0;
492
493 // get the best cut
494 pCut = Cnf_ObjBestCut( pObj );
495 // save variables of this cut
496 OutVar = pObj->Id;
497 for ( k = 0; k < (int)pCut->nFanins; k++ )
498 {
499 pVars[k] = pCut->pFanins[k];
500 assert( pVars[k] <= Aig_ManObjNumMax(p->pManAig) );
501 }
502
503 // positive polarity of the cut
504 if ( pCut->nFanins < 5 )
505 {
506 uTruth = 0xFFFF & *Cnf_CutTruth(pCut);
507 Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vSopTemp );
508 vCover = vSopTemp;
509 }
510 else
511 vCover = pCut->vIsop[1];
512 Vec_IntForEachEntry( vCover, Cube, k )
513 {
514 *pClas++ = pLits;
515 *pLits++ = 2 * OutVar;
516 pLits += Cnf_IsopWriteCube( Cube, pCut->nFanins, pVars, pLits );
517 }
518 pCnf->pObj2Count[pObj->Id] += Vec_IntSize(vCover);
519
520 // negative polarity of the cut
521 if ( pCut->nFanins < 5 )
522 {
523 uTruth = 0xFFFF & ~*Cnf_CutTruth(pCut);
524 Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vSopTemp );
525 vCover = vSopTemp;
526 }
527 else
528 vCover = pCut->vIsop[0];
529 Vec_IntForEachEntry( vCover, Cube, k )
530 {
531 *pClas++ = pLits;
532 *pLits++ = 2 * OutVar + 1;
533 pLits += Cnf_IsopWriteCube( Cube, pCut->nFanins, pVars, pLits );
534 }
535 pCnf->pObj2Count[pObj->Id] += Vec_IntSize(vCover);
536 }
537 Vec_IntFree( vSopTemp );
538
539 // write the output literals
540 Aig_ManForEachCo( p->pManAig, pObj, i )
541 {
542 // remember the starting clause
543 pCnf->pObj2Clause[pObj->Id] = pClas - pCnf->pClauses;
544 pCnf->pObj2Count[pObj->Id] = 2;
545 // get variables
546 OutVar = Aig_ObjFanin0(pObj)->Id;
547 PoVar = pObj->Id;
548 // first clause
549 *pClas++ = pLits;
550 *pLits++ = 2 * PoVar;
551 *pLits++ = 2 * OutVar + !Aig_ObjFaninC0(pObj);
552 // second clause
553 *pClas++ = pLits;
554 *pLits++ = 2 * PoVar + 1;
555 *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj);
556 }
557
558 // remember the starting clause
559 pCnf->pObj2Clause[Aig_ManConst1(p->pManAig)->Id] = pClas - pCnf->pClauses;
560 pCnf->pObj2Count[Aig_ManConst1(p->pManAig)->Id] = 1;
561 // write the constant literal
562 OutVar = Aig_ManConst1(p->pManAig)->Id;
563 *pClas++ = pLits;
564 *pLits++ = 2 * OutVar;
565
566 // verify that the correct number of literals and clauses was written
567 assert( pLits - pCnf->pClauses[0] == nLiterals );
568 assert( pClas - pCnf->pClauses == nClauses );
569//Cnf_DataPrint( pCnf, 1 );
570 return pCnf;
571}
Cnf_Dat_t_::pObj2Count
int * pObj2Count
Definition cnf.h:65
Cnf_Dat_t_::pObj2Clause
int * pObj2Clause
Definition cnf.h:64
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Cnf_ReadMsops()

void Cnf_ReadMsops ( char ** ppSopSizes,
char *** ppSops )
extern

FUNCTION DEFINITIONS ///.

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

Synopsis [Prepares the data for MSOPs of 4-variable functions.]

Description []

SideEffects []

SeeAlso []

Definition at line 4537 of file cnfData.c.

4538{
4539 unsigned uMasks[4][2] = {
4540 { 0x5555, 0xAAAA },
4541 { 0x3333, 0xCCCC },
4542 { 0x0F0F, 0xF0F0 },
4543 { 0x00FF, 0xFF00 }
4544 };
4545 char Map[256], * pPrev, * pMemory;
4546 char * pSopSizes, ** pSops;
4547 int i, k, b, Size;
4548
4549 // map chars into their numbers
4550 for ( i = 0; i < 256; i++ )
4551 Map[i] = (char)(-1);
4552 for ( i = 0; i < 81; i++ )
4553 Map[(int)s_Data3[i]] = (char)i;
4554
4555 // count the number of strings
4556 for ( Size = 0; s_Data4[Size] && Size < 100000; Size++ );
4557 assert( Size < 100000 );
4558
4559 // allocate memory
4560 pMemory = ABC_ALLOC( char, Size * 75 );
4561 // copy the array into memory
4562 for ( i = 0; i < Size; i++ )
4563 for ( k = 0; k < 75; k++ )
4564 if ( s_Data4[i][k] == ' ' )
4565 pMemory[i*75+k] = (char)(-1);
4566 else
4567 pMemory[i*75+k] = Map[(int)s_Data4[i][k]];
4568
4569 // set pointers and compute SOP sizes
4570 pSopSizes = ABC_ALLOC( char, 65536 );
4571 pSops = ABC_ALLOC( char *, 65536 );
4572 pSopSizes[0] = 0;
4573 pSops[0] = NULL;
4574 pPrev = pMemory;
4575 for ( k = 0, i = 1; i < 65536; k++ )
4576 if ( pMemory[k] == (char)(-1) )
4577 {
4578 pSopSizes[i] = pMemory + k - pPrev;
4579 pSops[i++] = pPrev;
4580 pPrev = pMemory + k + 1;
4581 }
4582 *ppSopSizes = pSopSizes;
4583 *ppSops = pSops;
4584
4585 // verify the results - derive truth table from SOP
4586 for ( i = 1; i < 65536; i++ )
4587 {
4588 int uTruth = 0, uCube, Lit;
4589 for ( k = 0; k < pSopSizes[i]; k++ )
4590 {
4591 uCube = 0xFFFF;
4592 Lit = pSops[i][k];
4593 for ( b = 3; b >= 0; b-- )
4594 {
4595 if ( Lit % 3 == 0 )
4596 uCube &= uMasks[b][0];
4597 else if ( Lit % 3 == 1 )
4598 uCube &= uMasks[b][1];
4599 Lit = Lit / 3;
4600 }
4601 uTruth |= uCube;
4602 }
4603 assert( uTruth == i );
4604 }
4605}
s_Data3
unsigned int s_Data3[24772]
Definition darData.c:9426
Here is the caller graph for this function:

◆ Cnf_SopConvertToVector()

void Cnf_SopConvertToVector ( char * pSop,
int nCubes,
Vec_Int_t * vCover )
extern

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

Synopsis [Writes the cover into the array.]

Description []

SideEffects []

SeeAlso []

Definition at line 82 of file cnfWrite.c.

83{
84 int Lits[4], Cube, iCube, i, b;
85 Vec_IntClear( vCover );
86 for ( i = 0; i < nCubes; i++ )
87 {
88 Cube = pSop[i];
89 for ( b = 0; b < 4; b++ )
90 {
91 if ( Cube % 3 == 0 )
92 Lits[b] = 1;
93 else if ( Cube % 3 == 1 )
94 Lits[b] = 2;
95 else
96 Lits[b] = 0;
97 Cube = Cube / 3;
98 }
99 iCube = 0;
100 for ( b = 0; b < 4; b++ )
101 iCube = (iCube << 2) | Lits[b];
102 Vec_IntPush( vCover, iCube );
103 }
104}
Here is the caller graph for this function: