summaryrefslogtreecommitdiffstats
path: root/src/aig/cnf
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/cnf')
-rw-r--r--src/aig/cnf/cnf.h3
-rw-r--r--src/aig/cnf/cnfCore.c6
-rw-r--r--src/aig/cnf/cnfMan.c13
-rw-r--r--src/aig/cnf/cnfUtil.c4
-rw-r--r--src/aig/cnf/cnfWrite.c129
5 files changed, 140 insertions, 15 deletions
diff --git a/src/aig/cnf/cnf.h b/src/aig/cnf/cnf.h
index 941ec816..5c7a594e 100644
--- a/src/aig/cnf/cnf.h
+++ b/src/aig/cnf/cnf.h
@@ -133,7 +133,7 @@ extern Cnf_Man_t * Cnf_ManStart();
extern void Cnf_ManStop( Cnf_Man_t * p );
extern Vec_Int_t * Cnf_DataCollectPiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p );
extern void Cnf_DataFree( Cnf_Dat_t * p );
-extern void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName );
+extern void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable );
void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p );
/*=== cnfMap.c ========================================================*/
extern void Cnf_DeriveMapping( Cnf_Man_t * p );
@@ -148,6 +148,7 @@ extern Vec_Ptr_t * Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect, int fPre
/*=== cnfWrite.c ========================================================*/
extern void Cnf_SopConvertToVector( char * pSop, int nCubes, Vec_Int_t * vCover );
extern Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs );
+extern Cnf_Dat_t * Cnf_DeriveSimple( Aig_Man_t * p, int nOutputs );
#ifdef __cplusplus
}
diff --git a/src/aig/cnf/cnfCore.c b/src/aig/cnf/cnfCore.c
index 88a55c22..13de745b 100644
--- a/src/aig/cnf/cnfCore.c
+++ b/src/aig/cnf/cnfCore.c
@@ -75,9 +75,9 @@ clk = clock();
Aig_MmFixedStop( pMemCuts, 0 );
p->timeSave = clock() - clk;
-PRT( "Cuts ", p->timeCuts );
-PRT( "Map ", p->timeMap );
-PRT( "Saving ", p->timeSave );
+//PRT( "Cuts ", p->timeCuts );
+//PRT( "Map ", p->timeMap );
+//PRT( "Saving ", p->timeSave );
return pCnf;
}
diff --git a/src/aig/cnf/cnfMan.c b/src/aig/cnf/cnfMan.c
index 77bf8650..1edc012a 100644
--- a/src/aig/cnf/cnfMan.c
+++ b/src/aig/cnf/cnfMan.c
@@ -26,6 +26,7 @@
////////////////////////////////////////////////////////////////////////
static inline int Cnf_Lit2Var( int Lit ) { return (Lit & 1)? -(Lit >> 1)-1 : (Lit >> 1)+1; }
+static inline int Cnf_Lit2Var2( int Lit ) { return (Lit & 1)? -(Lit >> 1) : (Lit >> 1); }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@@ -138,7 +139,7 @@ void Cnf_DataFree( Cnf_Dat_t * p )
SeeAlso []
***********************************************************************/
-void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName )
+void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable )
{
FILE * pFile;
int * pLit, * pStop, i;
@@ -153,7 +154,7 @@ void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName )
for ( i = 0; i < p->nClauses; i++ )
{
for ( pLit = p->pClauses[i], pStop = p->pClauses[i+1]; pLit < pStop; pLit++ )
- fprintf( pFile, "%d ", Cnf_Lit2Var(*pLit) );
+ fprintf( pFile, "%d ", fReadable? Cnf_Lit2Var2(*pLit) : Cnf_Lit2Var(*pLit) );
fprintf( pFile, "0\n" );
}
fprintf( pFile, "\n" );
@@ -174,7 +175,7 @@ void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName )
void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p )
{
sat_solver * pSat;
- int i;
+ int i, status;
pSat = sat_solver_new();
sat_solver_setnvars( pSat, p->nVars );
for ( i = 0; i < p->nClauses; i++ )
@@ -185,6 +186,12 @@ void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p )
return NULL;
}
}
+ status = sat_solver_simplify(pSat);
+ if ( status == 0 )
+ {
+ sat_solver_delete( pSat );
+ return NULL;
+ }
return pSat;
}
diff --git a/src/aig/cnf/cnfUtil.c b/src/aig/cnf/cnfUtil.c
index 22b30262..cd47cb58 100644
--- a/src/aig/cnf/cnfUtil.c
+++ b/src/aig/cnf/cnfUtil.c
@@ -98,7 +98,7 @@ Vec_Ptr_t * Aig_ManScanMapping( Cnf_Man_t * p, int fCollect )
p->aArea = 0;
Aig_ManForEachPo( p->pManAig, pObj, i )
p->aArea += Aig_ManScanMapping_rec( p, Aig_ObjFanin0(pObj), vMapped );
- printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) + Aig_ManPiNum(p->pManAig) + 1 : 0, p->aArea + 2 );
+// printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) + Aig_ManPiNum(p->pManAig) + 1 : 0, p->aArea + 2 );
return vMapped;
}
@@ -177,7 +177,7 @@ Vec_Ptr_t * Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect, int fPreorder )
p->aArea = 0;
Aig_ManForEachPo( p->pManAig, pObj, i )
p->aArea += Cnf_ManScanMapping_rec( p, Aig_ObjFanin0(pObj), vMapped, fPreorder );
- printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) + Aig_ManPiNum(p->pManAig) + 1 : 0, p->aArea + 2 );
+// printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) + Aig_ManPiNum(p->pManAig) + 1 : 0, p->aArea + 2 );
return vMapped;
}
diff --git a/src/aig/cnf/cnfWrite.c b/src/aig/cnf/cnfWrite.c
index fa5be801..6faa08d2 100644
--- a/src/aig/cnf/cnfWrite.c
+++ b/src/aig/cnf/cnfWrite.c
@@ -217,11 +217,12 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs )
pCnf->pVarNums = ALLOC( int, 1+Aig_ManObjIdMax(p->pManAig) );
memset( pCnf->pVarNums, 0xff, sizeof(int) * (1+Aig_ManObjIdMax(p->pManAig)) );
// assign variables to the last (nOutputs) POs
- Number = 0;
- for ( i = 0; i < nOutputs; i++ )
+ Number = 1;
+ if ( nOutputs )
{
- pObj = Aig_ManPo( p->pManAig, Aig_ManPoNum(p->pManAig) - nOutputs + i );
- pCnf->pVarNums[pObj->Id] = Number++;
+ assert( nOutputs == Aig_ManRegNum(p->pManAig) );
+ Aig_ManForEachLiSeq( p->pManAig, pObj, i )
+ pCnf->pVarNums[pObj->Id] = Number++;
}
// assign variables to the internal nodes
Vec_PtrForEachEntry( vMapped, pObj, i )
@@ -291,16 +292,15 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs )
// write the output literals
Aig_ManForEachPo( p->pManAig, pObj, i )
{
+ OutVar = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
if ( i < Aig_ManPoNum(p->pManAig) - nOutputs )
{
- OutVar = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
*pClas++ = pLits;
*pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj);
}
else
{
PoVar = pCnf->pVarNums[ pObj->Id ];
- OutVar = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
// first clause
*pClas++ = pLits;
*pLits++ = 2 * PoVar;
@@ -319,6 +319,123 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs )
}
+/**Function*************************************************************
+
+ Synopsis [Derives a simple CNF for the AIG.]
+
+ 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 []
+
+***********************************************************************/
+Cnf_Dat_t * Cnf_DeriveSimple( Aig_Man_t * p, int nOutputs )
+{
+ Aig_Obj_t * pObj;
+ Cnf_Dat_t * pCnf;
+ int OutVar, PoVar, pVars[32], * pLits, ** pClas;
+ int i, nLiterals, nClauses, Number;
+
+ // count the number of literals and clauses
+ nLiterals = 1 + 7 * Aig_ManNodeNum(p) + Aig_ManPoNum( p ) + 3 * nOutputs;
+ nClauses = 1 + 3 * Aig_ManNodeNum(p) + Aig_ManPoNum( p ) + nOutputs;
+
+ // allocate CNF
+ pCnf = ALLOC( Cnf_Dat_t, 1 );
+ memset( pCnf, 0, sizeof(Cnf_Dat_t) );
+ pCnf->nLiterals = nLiterals;
+ pCnf->nClauses = nClauses;
+ pCnf->pClauses = ALLOC( int *, nClauses + 1 );
+ pCnf->pClauses[0] = ALLOC( int, nLiterals );
+ pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals;
+
+ // create room for variable numbers
+ pCnf->pVarNums = ALLOC( int, 1+Aig_ManObjIdMax(p) );
+ memset( pCnf->pVarNums, 0xff, sizeof(int) * (1+Aig_ManObjIdMax(p)) );
+ // assign variables to the last (nOutputs) POs
+ Number = 1;
+ if ( nOutputs )
+ {
+ assert( nOutputs == Aig_ManRegNum(p) );
+ Aig_ManForEachLiSeq( p, pObj, i )
+ pCnf->pVarNums[pObj->Id] = Number++;
+ }
+ // assign variables to the internal nodes
+ Aig_ManForEachNode( p, pObj, i )
+ pCnf->pVarNums[pObj->Id] = Number++;
+ // assign variables to the PIs and constant node
+ Aig_ManForEachPi( p, pObj, i )
+ pCnf->pVarNums[pObj->Id] = Number++;
+ pCnf->pVarNums[Aig_ManConst1(p)->Id] = Number++;
+ pCnf->nVars = Number;
+/*
+ // print CNF numbers
+ printf( "SAT numbers of each node:\n" );
+ Aig_ManForEachObj( p, pObj, i )
+ printf( "%d=%d ", pObj->Id, pCnf->pVarNums[pObj->Id] );
+ printf( "\n" );
+*/
+ // assign the clauses
+ pLits = pCnf->pClauses[0];
+ pClas = pCnf->pClauses;
+ Aig_ManForEachNode( p, pObj, i )
+ {
+ OutVar = pCnf->pVarNums[ pObj->Id ];
+ pVars[0] = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
+ pVars[1] = pCnf->pVarNums[ Aig_ObjFanin1(pObj)->Id ];
+
+ // positive phase
+ *pClas++ = pLits;
+ *pLits++ = 2 * OutVar;
+ *pLits++ = 2 * pVars[0] + !Aig_ObjFaninC0(pObj);
+ *pLits++ = 2 * pVars[1] + !Aig_ObjFaninC1(pObj);
+ // negative phase
+ *pClas++ = pLits;
+ *pLits++ = 2 * OutVar + 1;
+ *pLits++ = 2 * pVars[0] + Aig_ObjFaninC0(pObj);
+ *pClas++ = pLits;
+ *pLits++ = 2 * OutVar + 1;
+ *pLits++ = 2 * pVars[1] + Aig_ObjFaninC1(pObj);
+ }
+
+ // write the constant literal
+ OutVar = pCnf->pVarNums[ Aig_ManConst1(p)->Id ];
+ assert( OutVar <= Aig_ManObjIdMax(p) );
+ *pClas++ = pLits;
+ *pLits++ = 2 * OutVar;
+
+ // write the output literals
+ Aig_ManForEachPo( p, pObj, i )
+ {
+ OutVar = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
+ if ( i < Aig_ManPoNum(p) - nOutputs )
+ {
+ *pClas++ = pLits;
+ *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj);
+ }
+ else
+ {
+ PoVar = pCnf->pVarNums[ pObj->Id ];
+ // first clause
+ *pClas++ = pLits;
+ *pLits++ = 2 * PoVar;
+ *pLits++ = 2 * OutVar + !Aig_ObjFaninC0(pObj);
+ // second clause
+ *pClas++ = pLits;
+ *pLits++ = 2 * PoVar + 1;
+ *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj);
+ }
+ }
+
+ // verify that the correct number of literals and clauses was written
+ assert( pLits - pCnf->pClauses[0] == nLiterals );
+ assert( pClas - pCnf->pClauses == nClauses );
+ return pCnf;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
generated by cgit v1.2.3 (git 2.25.1) at 2025-01-04 09:50:33 +0000