summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/gia/gia.h3
-rw-r--r--src/aig/gia/giaDup.c15
-rw-r--r--src/aig/gia/giaMan.c1
-rw-r--r--src/proof/cec/cecSplit.c154
4 files changed, 120 insertions, 53 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 870ac85c..bdb07c4c 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -156,6 +156,7 @@ struct Gia_Man_t_
Vec_Int_t * vUserFfIds; // numbers assigned to FFs by the user
Vec_Int_t * vCiNumsOrig; // original CI names
Vec_Int_t * vCoNumsOrig; // original CO names
+ Vec_Int_t * vCofVars; // cofactoring variables
Vec_Vec_t * vClockDoms; // clock domains
Vec_Flt_t * vTiming; // arrival/required/slack
void * pManTime; // the timing manager
@@ -1013,7 +1014,7 @@ extern Gia_Man_t * Gia_ManDupFlopClass( Gia_Man_t * p, int iClass );
extern Gia_Man_t * Gia_ManDupMarked( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupTimes( Gia_Man_t * p, int nTimes );
extern Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p );
-extern Gia_Man_t * Gia_ManDupDfsRehash( Gia_Man_t * p, int nSteps, int Value );
+extern Gia_Man_t * Gia_ManDupCofactor( Gia_Man_t * p, int iVar, int Value );
extern Gia_Man_t * Gia_ManDupDfsSkip( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupDfsCone( Gia_Man_t * p, Gia_Obj_t * pObj );
extern Gia_Man_t * Gia_ManDupDfsLitArray( Gia_Man_t * p, Vec_Int_t * vLits );
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 2d294433..0939c091 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -1201,30 +1201,33 @@ Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p )
SeeAlso []
***********************************************************************/
-void Gia_ManDupDfsRehash_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
+void Gia_ManDupCofactor_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
{
if ( ~pObj->Value )
return;
assert( Gia_ObjIsAnd(pObj) );
- Gia_ManDupDfsRehash_rec( pNew, p, Gia_ObjFanin0(pObj) );
- Gia_ManDupDfsRehash_rec( pNew, p, Gia_ObjFanin1(pObj) );
+ Gia_ManDupCofactor_rec( pNew, p, Gia_ObjFanin0(pObj) );
+ Gia_ManDupCofactor_rec( pNew, p, Gia_ObjFanin1(pObj) );
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
}
-Gia_Man_t * Gia_ManDupDfsRehash( Gia_Man_t * p, int nSteps, int Value )
+Gia_Man_t * Gia_ManDupCofactor( Gia_Man_t * p, int iVar, int Value )
{
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj;
int i;
+ assert( iVar >= 0 && iVar < Gia_ManPiNum(p) );
+ assert( Value == 0 || Value == 1 );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
Gia_ManFillValue( p );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
- pObj->Value = i < nSteps ? Value : Gia_ManAppendCi(pNew);
+ pObj->Value = Gia_ManAppendCi(pNew);
+ Gia_ManPi( p, iVar )->Value = Value; // modification!
Gia_ManHashAlloc( pNew );
Gia_ManForEachCo( p, pObj, i )
- Gia_ManDupDfsRehash_rec( pNew, p, Gia_ObjFanin0(pObj) );
+ Gia_ManDupCofactor_rec( pNew, p, Gia_ObjFanin0(pObj) );
Gia_ManForEachCo( p, pObj, i )
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index 710886ae..6d5a8e92 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -92,6 +92,7 @@ void Gia_ManStop( Gia_Man_t * p )
Vec_WrdFreeP( &p->vSimsPi );
Vec_FltFreeP( &p->vTiming );
Vec_VecFreeP( &p->vClockDoms );
+ Vec_IntFreeP( &p->vCofVars );
Vec_IntFreeP( &p->vLutConfigs );
Vec_IntFreeP( &p->vUserPiIds );
Vec_IntFreeP( &p->vUserPoIds );
diff --git a/src/proof/cec/cecSplit.c b/src/proof/cec/cecSplit.c
index 6046df37..352b94e4 100644
--- a/src/proof/cec/cecSplit.c
+++ b/src/proof/cec/cecSplit.c
@@ -18,11 +18,13 @@
***********************************************************************/
+#include <math.h>
#include "aig/gia/gia.h"
#include "aig/gia/giaAig.h"
-#include "bdd/cudd/cuddInt.h"
+//#include "bdd/cudd/cuddInt.h"
#include "sat/cnf/cnf.h"
-#include "sat/bsat/satStore.h"
+#include "sat/bsat/satSolver.h"
+#include "misc/util/utilTruth.h"
ABC_NAMESPACE_IMPL_START
@@ -35,6 +37,8 @@ ABC_NAMESPACE_IMPL_START
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
+#if 0 // BDD code
+
/**Function*************************************************************
Synopsis [Permute primary inputs.]
@@ -109,6 +113,8 @@ void Gia_ManBuildBddTest( Gia_Man_t * p )
Gia_ManDerefBdd( dd, vNodes );
}
+#endif // BDD code
+
/**Function*************************************************************
Synopsis [Permute primary inputs.]
@@ -120,10 +126,9 @@ void Gia_ManBuildBddTest( Gia_Man_t * p )
SeeAlso []
***********************************************************************/
-Gia_Man_t * Gia_PermuteSpecial( Gia_Man_t * p )
+int * Gia_PermuteSpecialOrder( Gia_Man_t * p )
{
Vec_Int_t * vPerm;
- Gia_Man_t * pNew;
Gia_Obj_t * pObj;
int i, * pOrder;
Gia_ManCreateRefs( p );
@@ -132,6 +137,13 @@ Gia_Man_t * Gia_PermuteSpecial( Gia_Man_t * p )
Vec_IntPush( vPerm, Gia_ObjRefNum(p, pObj) );
pOrder = Abc_QuickSortCost( Vec_IntArray(vPerm), Vec_IntSize(vPerm), 1 );
Vec_IntFree( vPerm );
+ return pOrder;
+}
+Gia_Man_t * Gia_PermuteSpecial( Gia_Man_t * p )
+{
+ Gia_Man_t * pNew;
+ Vec_Int_t * vPerm;
+ int * pOrder = Gia_PermuteSpecialOrder( p );
vPerm = Vec_IntAllocArray( pOrder, Gia_ManPiNum(p) );
pNew = Gia_ManDupPerm( p, vPerm );
Vec_IntFree( vPerm );
@@ -207,29 +219,13 @@ static inline sat_solver * Cec_GiaDeriveSolver( Gia_Man_t * p, int nTimeOut )
Cnf_DataFree( pCnf );
return pSat;
}
-static inline int Cnf_GiaSolveOne( Gia_Man_t * p, int nTimeOut, int nSize, int fVerbose )
+static inline int Cnf_GiaSolveOne( Gia_Man_t * p, int nTimeOut, int fVerbose, int * pnVars, int * pnConfs )
{
static int Counter = 0;
- abctime clk = Abc_Clock();
sat_solver * pSat = Cec_GiaDeriveSolver( p, nTimeOut );
int status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
- if ( fVerbose )
- {
- printf( "Iter%6d : ", Counter++ );
- printf( "Size =%7d ", nSize );
- printf( "Input = %3d ", Gia_ManPiNum(p) );
- printf( "Var =%10d ", sat_solver_nvars(pSat) );
- printf( "Clause =%10d ", sat_solver_nclauses(pSat) );
- printf( "Conflict =%10d ", sat_solver_nconflicts(pSat) );
- if ( status == l_Undef )
- printf( "UNDECIDED " );
- else if ( status == l_False )
- printf( "UNSAT " );
- else
- printf( "SAT " );
- Abc_PrintTime( 1, "Time", Abc_Clock()-clk );
- //ABC_PRTr( "Time", Abc_Clock()-clk );
- }
+ *pnVars = sat_solver_nvars( pSat );
+ *pnConfs = sat_solver_nconflicts( pSat );
sat_solver_delete( pSat );
if ( status == l_Undef )
return -1;
@@ -253,9 +249,9 @@ static inline int Cnf_GiaSolveOne( Gia_Man_t * p, int nTimeOut, int nSize, int f
}
*/
}
-static inline int Cnf_GiaCheckOne( Vec_Ptr_t * vStack, Gia_Man_t * p, int nTimeOut, int nSize, int fVerbose )
+static inline int Cnf_GiaCheckOne( Vec_Ptr_t * vStack, Gia_Man_t * p, int nTimeOut, int fVerbose, int * pnVars, int * pnConfs )
{
- int status = Cnf_GiaSolveOne( p, nTimeOut, nSize, fVerbose );
+ int status = Cnf_GiaSolveOne( p, nTimeOut, fVerbose, pnVars, pnConfs );
if ( status == -1 )
{
Vec_PtrPush( vStack, p );
@@ -287,47 +283,111 @@ static inline void Cec_GiaSplitClean( Vec_Ptr_t * vStack )
SeeAlso []
***********************************************************************/
+void Cec_GiaSplitPrint( int nIter, int Depth, int nVars, int nConfs, int fSatUnsat, double Prog, abctime clk )
+{
+ printf( "%6d : ", nIter );
+ printf( "Depth =%3d ", Depth );
+ printf( "SatVar =%10d ", nVars );
+ printf( "SatConf =%7d ", nConfs );
+ printf( "%s ", fSatUnsat ? "UNSAT " : "UNDECIDED" );
+ printf( "Progress = %.9f ", Prog );
+ Abc_PrintTime( 1, "Time", clk );
+ //ABC_PRTr( "Time", Abc_Clock()-clk );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int fVerbose )
{
- Gia_Man_t * pNew;
- Vec_Ptr_t * vStack;
- Gia_Man_t * pPart0, * pPart1;
+ abctime clk, clkTotal = Abc_Clock();
+ Gia_Man_t * pPart0, * pPart1, * pLast;
Gia_Obj_t * pObj;
- int i, RetValue = -1;
+ Vec_Ptr_t * vStack;
+ int * pOrder, RetValue = -1;
+ int nSatVars, nSatConfs, fSatUnsat;
+ int i, nIter, iVar, Depth;
+ double Progress = 0;
+ // create local copy
+ p = Gia_ManDup( p );
// reorder variables
- pNew = Gia_PermuteSpecial( p );
- if ( fVerbose )
+ pOrder = Gia_PermuteSpecialOrder( p );
+ if ( fVerbose )
{
- Gia_ManCreateRefs( pNew );
- Gia_ManForEachPi( pNew, pObj, i )
- printf( "%d ", Gia_ObjRefNum(pNew, pObj) );
+ Gia_ManForEachPi( p, pObj, i )
+ printf( "%d ", Gia_ObjRefNum(p, pObj) );
+ printf( "\n" );
+ Gia_ManForEachPi( p, pObj, i )
+ printf( "%d ", Gia_ObjRefNum(p, Gia_ManPi(p, pOrder[i])) );
printf( "\n" );
}
+ // start cofactored variables
+ assert( p->vCofVars == NULL );
+ p->vCofVars = Vec_IntAlloc( 100 );
// start with the current problem
vStack = Vec_PtrAlloc( 1000 );
- if ( !Cnf_GiaCheckOne(vStack, pNew, nTimeOut, Vec_PtrSize(vStack), fVerbose) )
+ clk = Abc_Clock();
+ if ( !Cnf_GiaCheckOne(vStack, p, nTimeOut, fVerbose, &nSatVars, &nSatConfs) )
RetValue = 0;
else
{
- while ( Vec_PtrSize(vStack) > 0 )
+ if ( fVerbose )
+ Cec_GiaSplitPrint( 0, 0, nSatVars, nSatConfs, 0, 0, Abc_Clock() - clk );
+ for ( nIter = 1; Vec_PtrSize(vStack) > 0; nIter++ )
{
- pNew = (Gia_Man_t *)Vec_PtrPop( vStack );
+ // get the last AIG
+ pLast = (Gia_Man_t *)Vec_PtrPop( vStack );
+ // determine cofactoring variable
+ Depth = Vec_IntSize(pLast->vCofVars);
+ iVar = pOrder[Depth];
// cofactor
- pPart0 = Gia_ManDupDfsRehash( pNew, 1, 0 );
- if ( !Cnf_GiaCheckOne(vStack, pPart0, nTimeOut, Vec_PtrSize(vStack), fVerbose) )
+ pPart0 = Gia_ManDupCofactor( pLast, iVar, 0 );
+ // create variable
+ pPart0->vCofVars = Vec_IntAlloc( Vec_IntSize(pLast->vCofVars) + 1 );
+ Vec_IntAppend( pPart0->vCofVars, pLast->vCofVars );
+ Vec_IntPush( pPart0->vCofVars, Abc_Var2Lit(iVar, 1) );
+ // check this AIG
+ fSatUnsat = Vec_PtrSize(vStack);
+ clk = Abc_Clock();
+ if ( !Cnf_GiaCheckOne(vStack, pPart0, nTimeOut, fVerbose, &nSatVars, &nSatConfs) )
{
- Gia_ManStop( pNew );
+ Gia_ManStop( pLast );
RetValue = 0;
break;
}
+ fSatUnsat = (fSatUnsat == Vec_PtrSize(vStack));
+ if ( fSatUnsat )
+ Progress += 1.0 / pow(0.5, Depth + 1);
+ if ( fVerbose )
+ Cec_GiaSplitPrint( nIter, Depth, nSatVars, nSatConfs, fSatUnsat, Progress, Abc_Clock() - clk );
// cofactor
- pPart1 = Gia_ManDupDfsRehash( pNew, 1, 1 );
- Gia_ManStop( pNew );
- if ( !Cnf_GiaCheckOne(vStack, pPart1, nTimeOut, Vec_PtrSize(vStack), fVerbose) )
+ pPart1 = Gia_ManDupCofactor( pLast, iVar, 1 );
+ // create variable
+ pPart1->vCofVars = Vec_IntAlloc( Vec_IntSize(pLast->vCofVars) + 1 );
+ Vec_IntAppend( pPart1->vCofVars, pLast->vCofVars );
+ Vec_IntPush( pPart1->vCofVars, Abc_Var2Lit(iVar, 0) );
+ Gia_ManStop( pLast );
+ // check this AIG
+ fSatUnsat = Vec_PtrSize(vStack);
+ clk = Abc_Clock();
+ if ( !Cnf_GiaCheckOne(vStack, pPart1, nTimeOut, fVerbose, &nSatVars, &nSatConfs) )
{
RetValue = 0;
break;
}
+ fSatUnsat = (fSatUnsat == Vec_PtrSize(vStack));
+ if ( fSatUnsat )
+ Progress += 1.0 / (Depth + 1);
+ if ( fVerbose )
+ Cec_GiaSplitPrint( nIter, Depth, nSatVars, nSatConfs, fSatUnsat, Progress, Abc_Clock() - clk );
// if ( Vec_PtrSize(vStack) > 2 )
// break;
}
@@ -336,12 +396,14 @@ int Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int fVerbose )
}
Cec_GiaSplitClean( vStack );
if ( RetValue == 0 )
- printf( "Problem is SAT\n" );
+ printf( "Problem is SAT " );
else if ( RetValue == 1 )
- printf( "Problem is UNSAT\n" );
+ printf( "Problem is UNSAT " );
else if ( RetValue == -1 )
- printf( "Problem is UNDECIDED\n" );
+ printf( "Problem is UNDECIDED " );
else assert( 0 );
+ ABC_FREE( pOrder );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
return RetValue;
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-06 05:14:58 +0000