summaryrefslogtreecommitdiffstats
path: root/src/aig
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig')
-rw-r--r--src/aig/aig/aigInter.c174
-rw-r--r--src/aig/aig/module.make1
-rw-r--r--src/aig/cnf/cnf.h1
-rw-r--r--src/aig/cnf/cnfMan.c22
4 files changed, 198 insertions, 0 deletions
diff --git a/src/aig/aig/aigInter.c b/src/aig/aig/aigInter.c
new file mode 100644
index 00000000..b3bc28b2
--- /dev/null
+++ b/src/aig/aig/aigInter.c
@@ -0,0 +1,174 @@
+/**CFile****************************************************************
+
+ FileName [aigInter.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [AIG package.]
+
+ Synopsis [Interpolate two AIGs.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - April 28, 2007.]
+
+ Revision [$Id: aigInter.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+#include "cnf.h"
+#include "satStore.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManInter( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fVerbose )
+{
+ void * pSatCnf = NULL;
+ Inta_Man_t * pManInter;
+ Aig_Man_t * pRes;
+ sat_solver * pSat;
+ Cnf_Dat_t * pCnfOn, * pCnfOff;
+ Vec_Int_t * vVarsAB;
+ Aig_Obj_t * pObj, * pObj2;
+ int Lits[3], status, i;
+ int clk = clock();
+
+ assert( Aig_ManPiNum(pManOn) == Aig_ManPiNum(pManOff) );
+
+ // derive CNFs
+ pCnfOn = Cnf_Derive( pManOn, 0 );
+ pCnfOff = Cnf_Derive( pManOff, 0 );
+// pCnfOn = Cnf_DeriveSimple( pManOn, 0 );
+// pCnfOff = Cnf_DeriveSimple( pManOff, 0 );
+ Cnf_DataLift( pCnfOff, pCnfOn->nVars );
+
+ // start the solver
+ pSat = sat_solver_new();
+ sat_solver_store_alloc( pSat );
+ sat_solver_setnvars( pSat, pCnfOn->nVars + pCnfOff->nVars );
+
+ // add clauses of A
+ for ( i = 0; i < pCnfOn->nClauses; i++ )
+ {
+ if ( !sat_solver_addclause( pSat, pCnfOn->pClauses[i], pCnfOn->pClauses[i+1] ) )
+ {
+ Cnf_DataFree( pCnfOn );
+ Cnf_DataFree( pCnfOff );
+ sat_solver_delete( pSat );
+ return NULL;
+ }
+ }
+ sat_solver_store_mark_clauses_a( pSat );
+
+ // add clauses of B
+ for ( i = 0; i < pCnfOff->nClauses; i++ )
+ {
+ if ( !sat_solver_addclause( pSat, pCnfOff->pClauses[i], pCnfOff->pClauses[i+1] ) )
+ {
+ Cnf_DataFree( pCnfOn );
+ Cnf_DataFree( pCnfOff );
+ sat_solver_delete( pSat );
+ return NULL;
+ }
+ }
+
+ // add PI clauses
+ // collect the common variables
+ vVarsAB = Vec_IntAlloc( Aig_ManPiNum(pManOn) );
+ Aig_ManForEachPi( pManOn, pObj, i )
+ {
+ Vec_IntPush( vVarsAB, pCnfOn->pVarNums[pObj->Id] );
+ pObj2 = Aig_ManPi( pManOff, i );
+
+ Lits[0] = toLitCond( pCnfOn->pVarNums[pObj->Id], 0 );
+ Lits[1] = toLitCond( pCnfOff->pVarNums[pObj2->Id], 1 );
+ if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
+ assert( 0 );
+ Lits[0] = toLitCond( pCnfOn->pVarNums[pObj->Id], 1 );
+ Lits[1] = toLitCond( pCnfOff->pVarNums[pObj2->Id], 0 );
+ if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
+ assert( 0 );
+ }
+ Cnf_DataFree( pCnfOn );
+ Cnf_DataFree( pCnfOff );
+ sat_solver_store_mark_roots( pSat );
+ if ( fVerbose )
+ {
+ PRT( "Prepare", clock() - clk );
+ }
+
+/*
+ status = sat_solver_simplify(pSat);
+ if ( status == 0 )
+ {
+ Vec_IntFree( vVarsAB );
+ Cnf_DataFree( pCnfOn );
+ Cnf_DataFree( pCnfOff );
+ sat_solver_delete( pSat );
+ return NULL;
+ }
+*/
+
+ // solve the problem
+ clk = clock();
+ status = sat_solver_solve( pSat, NULL, NULL, (sint64)0, (sint64)0, (sint64)0, (sint64)0 );
+ if ( fVerbose )
+ {
+ PRT( "Solving", clock() - clk );
+ }
+ if ( status == l_False )
+ {
+ pSatCnf = sat_solver_store_release( pSat );
+// printf( "unsat\n" );
+ }
+ else if ( status == l_True )
+ {
+// printf( "sat\n" );
+ }
+ else
+ {
+// printf( "undef\n" );
+ }
+ sat_solver_delete( pSat );
+ if ( pSatCnf == NULL )
+ {
+ printf( "The SAT problem is not unsat.\n" );
+ Vec_IntFree( vVarsAB );
+ return NULL;
+ }
+
+ // create the resulting manager
+ pManInter = Inta_ManAlloc();
+ pRes = Inta_ManInterpolate( pManInter, pSatCnf, vVarsAB, fVerbose );
+ Inta_ManFree( pManInter );
+
+ Vec_IntFree( vVarsAB );
+ Sto_ManFree( pSatCnf );
+ return pRes;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/aig/module.make b/src/aig/aig/module.make
index 667ceec1..ffe6141c 100644
--- a/src/aig/aig/module.make
+++ b/src/aig/aig/module.make
@@ -3,6 +3,7 @@ SRC += src/aig/aig/aigCheck.c \
src/aig/aig/aigFanout.c \
src/aig/aig/aigFrames.c \
src/aig/aig/aigHaig.c \
+ src/aig/aig/aigInter.c \
src/aig/aig/aigMan.c \
src/aig/aig/aigMem.c \
src/aig/aig/aigMffc.c \
diff --git a/src/aig/cnf/cnf.h b/src/aig/cnf/cnf.h
index 77c87f3f..5726469f 100644
--- a/src/aig/cnf/cnf.h
+++ b/src/aig/cnf/cnf.h
@@ -133,6 +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_DataLift( Cnf_Dat_t * p, int nVarsPlus );
extern void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable );
void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit );
/*=== cnfMap.c ========================================================*/
diff --git a/src/aig/cnf/cnfMan.c b/src/aig/cnf/cnfMan.c
index 4ac06b48..47bc0b67 100644
--- a/src/aig/cnf/cnfMan.c
+++ b/src/aig/cnf/cnfMan.c
@@ -139,6 +139,28 @@ void Cnf_DataFree( Cnf_Dat_t * p )
SeeAlso []
***********************************************************************/
+void Cnf_DataLift( Cnf_Dat_t * p, int nVarsPlus )
+{
+ Aig_Obj_t * pObj;
+ int v;
+ Aig_ManForEachObj( p->pMan, pObj, v )
+ if ( p->pVarNums[pObj->Id] )
+ p->pVarNums[pObj->Id] += nVarsPlus;
+ for ( v = 0; v < p->nLiterals; v++ )
+ p->pClauses[0][v] += 2*nVarsPlus;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Writes CNF into a file.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable )
{
FILE * pFile;
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-19 01:53:33 +0000