summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/aig/gia/gia.c159
-rw-r--r--src/aig/gia/giaCSat.c1
-rw-r--r--src/aig/gia/giaCSat2.c1132
-rw-r--r--src/aig/gia/module.make1
-rw-r--r--src/base/abci/abc.c19
-rw-r--r--src/proof/cec/cecCore.c2
6 files changed, 1309 insertions, 5 deletions
diff --git a/src/aig/gia/gia.c b/src/aig/gia/gia.c
index 4fb33a9b..8f18f69c 100644
--- a/src/aig/gia/gia.c
+++ b/src/aig/gia/gia.c
@@ -26,6 +26,43 @@ ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
+
+typedef struct Slv_Man_t_ Slv_Man_t;
+struct Slv_Man_t_
+{
+ Vec_Int_t vCis;
+ Vec_Int_t vCos;
+ Vec_Int_t vFanins;
+ Vec_Int_t vFanoutN;
+ Vec_Int_t vFanout0;
+ Vec_Str_t vValues;
+ Vec_Int_t vCopies;
+};
+
+static inline int Slv_ManObjNum ( Slv_Man_t * p ) { return Vec_IntSize(&p->vFanins)/2; }
+
+static inline int Slv_ObjFaninLit ( Slv_Man_t * p, int iObj, int f ) { return Vec_IntEntry(&p->vFanins, Abc_Var2Lit(iObj, f)); }
+static inline int Slv_ObjFanin ( Slv_Man_t * p, int iObj, int f ) { return Abc_Lit2Var(Slv_ObjFaninLit(p, iObj, f)); }
+static inline int Slv_ObjFaninC ( Slv_Man_t * p, int iObj, int f ) { return Abc_LitIsCompl(Slv_ObjFaninLit(p, iObj, f)); }
+
+static inline int Slv_ObjIsCi ( Slv_Man_t * p, int iObj ) { return !Slv_ObjFaninLit(p, iObj, 0) && Slv_ObjFaninLit(p, iObj, 1); }
+static inline int Slv_ObjIsCo ( Slv_Man_t * p, int iObj ) { return Slv_ObjFaninLit(p, iObj, 0) && !Slv_ObjFaninLit(p, iObj, 1); }
+static inline int Slv_ObjIsAnd ( Slv_Man_t * p, int iObj ) { return Slv_ObjFaninLit(p, iObj, 0) && Slv_ObjFaninLit(p, iObj, 1); }
+
+static inline int Slv_ObjFanout0 ( Slv_Man_t * p, int iObj ) { return Vec_IntEntry(&p->vFanout0, iObj); }
+static inline void Slv_ObjSetFanout0 ( Slv_Man_t * p, int iObj, int iLit ) { Vec_IntWriteEntry(&p->vFanout0, iObj, iLit); }
+
+static inline int Slv_ObjNextFanout ( Slv_Man_t * p, int iLit ) { return Vec_IntEntry(&p->vFanoutN, iLit); }
+static inline void Slv_ObjSetNextFanout( Slv_Man_t * p, int iLit, int iLitF ) { Vec_IntWriteEntry(&p->vFanoutN, iLit, iLitF); }
+
+static inline int Slv_ObjCopyLit ( Slv_Man_t * p, int iObj ) { return Vec_IntEntry(&p->vCopies, iObj); }
+static inline void Slv_ObjSetCopyLit ( Slv_Man_t * p, int iObj, int iLit ) { Vec_IntWriteEntry(&p->vCopies, iObj, iLit); }
+
+#define Slv_ManForEachObj( p, iObj ) \
+ for ( iObj = 1; iObj < Slv_ManObjNum(p); iObj++ )
+
+#define Slv_ObjForEachFanout( p, iObj, iFanLit ) \
+ for ( iFanLit = Slv_ObjFanout0(p, iObj); iFanLit; iFanLit = Slv_ObjNextFanout(p, iFanLit) )
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@@ -42,6 +79,128 @@ ABC_NAMESPACE_IMPL_START
SeeAlso []
***********************************************************************/
+Slv_Man_t * Slv_ManAlloc( int nObjs )
+{
+ Slv_Man_t * p = ABC_CALLOC( Slv_Man_t, 1 );
+ Vec_IntGrow( &p->vCis, 100 );
+ Vec_IntGrow( &p->vCos, 100 );
+ Vec_IntGrow( &p->vFanins, 2*nObjs );
+ Vec_IntGrow( &p->vFanoutN, 2*nObjs );
+ Vec_IntGrow( &p->vFanout0, nObjs );
+ Vec_StrGrow( &p->vValues, nObjs );
+ // constant node
+ Vec_IntFill( &p->vFanins, 2, 0 );
+ Vec_IntFill( &p->vFanoutN, 2, 0 );
+ Vec_IntFill( &p->vFanout0, 1, 0 );
+ return p;
+}
+void Slv_ManFree( Slv_Man_t * p )
+{
+ Vec_IntErase( &p->vCis );
+ Vec_IntErase( &p->vCos );
+ Vec_IntErase( &p->vFanins );
+ Vec_IntErase( &p->vFanoutN );
+ Vec_IntErase( &p->vFanout0 );
+ Vec_StrErase( &p->vValues );
+ Vec_IntErase( &p->vCopies );
+ ABC_FREE( p );
+}
+void Slv_ManPrintFanouts( Slv_Man_t * p )
+{
+ int iObj, iFanLit;
+ Slv_ManForEachObj( p, iObj )
+ {
+ printf( "Fanouts of node %d: ", iObj );
+ Slv_ObjForEachFanout( p, iObj, iFanLit )
+ printf( "%d ", Abc_Lit2Var(iFanLit) );
+ printf( "\n" );
+ }
+}
+static inline int Slv_ManAppendObj( Slv_Man_t * p, int iLit0, int iLit1 )
+{
+ int iObj = Slv_ManObjNum(p);
+ Vec_StrPush( &p->vValues, 0 );
+ Vec_IntPush( &p->vFanout0, 0 );
+ Vec_IntPushTwo( &p->vFanoutN, 0, 0 );
+ if ( !iLit0 ) // primary input
+ assert(!iLit1), iLit1 = Vec_IntSize(&p->vCis)+1, Vec_IntPush(&p->vCis, iObj);
+ else if ( !iLit1 ) // primary output
+ assert(iLit0), Vec_IntPush(&p->vCos, iObj);
+ else
+ {
+ Slv_ObjSetNextFanout( p, Abc_Var2Lit(iObj, 0), Slv_ObjFanout0(p, Abc_Lit2Var(iLit0)) );
+ Slv_ObjSetNextFanout( p, Abc_Var2Lit(iObj, 1), Slv_ObjFanout0(p, Abc_Lit2Var(iLit1)) );
+ Slv_ObjSetFanout0( p, Abc_Lit2Var(iLit0), Abc_Var2Lit(iObj, 0) );
+ Slv_ObjSetFanout0( p, Abc_Lit2Var(iLit1), Abc_Var2Lit(iObj, 1) );
+ }
+ Vec_IntPushTwo( &p->vFanins, iLit0, iLit1 );
+ return Abc_Var2Lit( iObj, 0 );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Slv_Man_t * Slv_ManFromGia( Gia_Man_t * p )
+{
+ Gia_Obj_t * pObj; int i;
+ Slv_Man_t * pNew = Slv_ManAlloc( Gia_ManObjNum(p) );
+ Gia_ManConst0(p)->Value = 0;
+ Gia_ManForEachObj1( p, pObj, i )
+ {
+ if ( Gia_ObjIsAnd(pObj) )
+ pObj->Value = Slv_ManAppendObj( pNew, Abc_LitNotCond(Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj)), Abc_LitNotCond(Gia_ObjFanin1(pObj)->Value, Gia_ObjFaninC1(pObj)) );
+ else if ( Gia_ObjIsCo(pObj) )
+ pObj->Value = Slv_ManAppendObj( pNew, Abc_LitNotCond(Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj)), 0 );
+ else if ( Gia_ObjIsCi(pObj) )
+ pObj->Value = Slv_ManAppendObj( pNew, 0, 0 );
+ else
+ assert( 0 );
+ }
+ assert( Gia_ManObjNum(p) == Slv_ManObjNum(pNew) );
+ return pNew;
+}
+Gia_Man_t * Slv_ManToGia( Slv_Man_t * p )
+{
+ int iObj;
+ Gia_Man_t * pNew = Gia_ManStart( Slv_ManObjNum(p) );
+ Vec_IntFill( &p->vCopies, Slv_ManObjNum(p), 0 );
+ Slv_ManForEachObj( p, iObj )
+ if ( Slv_ObjIsCi(p, iObj) )
+ Slv_ObjSetCopyLit( p, iObj, Gia_ManAppendCi(pNew) );
+ else if ( Slv_ObjIsCo(p, iObj) )
+ {
+ int iLit0 = Abc_LitNotCond( Slv_ObjCopyLit(p, Slv_ObjFanin(p, iObj, 0)), Slv_ObjFaninC(p, iObj, 0) );
+ Slv_ObjSetCopyLit( p, iObj, Gia_ManAppendCo(pNew, iLit0) );
+ }
+ else if ( Slv_ObjIsAnd(p, iObj) )
+ {
+ int iLit0 = Abc_LitNotCond( Slv_ObjCopyLit(p, Slv_ObjFanin(p, iObj, 0)), Slv_ObjFaninC(p, iObj, 0) );
+ int iLit1 = Abc_LitNotCond( Slv_ObjCopyLit(p, Slv_ObjFanin(p, iObj, 1)), Slv_ObjFaninC(p, iObj, 1) );
+ Slv_ObjSetCopyLit( p, iObj, Gia_ManAppendAnd(pNew, iLit0, iLit1) );
+ }
+ else assert(0);
+ assert( Gia_ManObjNum(pNew) == Slv_ManObjNum(p) );
+ return pNew;
+}
+
+Gia_Man_t * Slv_ManToAig( Gia_Man_t * pGia )
+{
+ Slv_Man_t * p = Slv_ManFromGia( pGia );
+ Gia_Man_t * pNew = Slv_ManToGia( p );
+ pNew->pName = Abc_UtilStrsav( pGia->pName );
+ pNew->pSpec = Abc_UtilStrsav( pGia->pSpec );
+ Slv_ManPrintFanouts( p );
+ Slv_ManFree( p );
+ return pNew;
+}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
diff --git a/src/aig/gia/giaCSat.c b/src/aig/gia/giaCSat.c
index baf1b418..503961d4 100644
--- a/src/aig/gia/giaCSat.c
+++ b/src/aig/gia/giaCSat.c
@@ -285,6 +285,7 @@ static inline int Cbs_QueIsEmpty( Cbs_Que_t * p )
***********************************************************************/
static inline void Cbs_QuePush( Cbs_Que_t * p, Gia_Obj_t * pObj )
{
+ assert( !Gia_IsComplement(pObj) );
if ( p->iTail == p->nSize )
{
p->nSize *= 2;
diff --git a/src/aig/gia/giaCSat2.c b/src/aig/gia/giaCSat2.c
new file mode 100644
index 00000000..14633b08
--- /dev/null
+++ b/src/aig/gia/giaCSat2.c
@@ -0,0 +1,1132 @@
+/**CFile****************************************************************
+
+ FileName [giaCSat.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Scalable AIG package.]
+
+ Synopsis [A simple circuit-based solver.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: giaCSat.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "gia.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+//#define gia_assert(exp) ((void)0)
+//#define gia_assert(exp) (assert(exp))
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Cbs2_Par_t_ Cbs2_Par_t;
+struct Cbs2_Par_t_
+{
+ // conflict limits
+ int nBTLimit; // limit on the number of conflicts
+ int nJustLimit; // limit on the size of justification queue
+ // current parameters
+ int nBTThis; // number of conflicts
+ int nBTThisNc; // number of conflicts
+ int nJustThis; // max size of the frontier
+ int nBTTotal; // total number of conflicts
+ int nJustTotal; // total size of the frontier
+ // decision heuristics
+ int fUseHighest; // use node with the highest ID
+ int fUseLowest; // use node with the highest ID
+ int fUseMaxFF; // use node with the largest fanin fanout
+ // other
+ int fVerbose;
+};
+
+typedef struct Cbs2_Que_t_ Cbs2_Que_t;
+struct Cbs2_Que_t_
+{
+ int iHead; // beginning of the queue
+ int iTail; // end of the queue
+ int nSize; // allocated size
+ Gia_Obj_t ** pData; // nodes stored in the queue
+};
+
+typedef struct Cbs2_Man_t_ Cbs2_Man_t;
+struct Cbs2_Man_t_
+{
+ Cbs2_Par_t Pars; // parameters
+ Gia_Man_t * pAig; // AIG manager
+ Cbs2_Que_t pProp; // propagation queue
+ Cbs2_Que_t pJust; // justification queue
+ Cbs2_Que_t pClauses; // clause queue
+ Gia_Obj_t ** pIter; // iterator through clause vars
+ Vec_Int_t * vLevReas; // levels and decisions
+ Vec_Int_t * vModel; // satisfying assignment
+ Vec_Ptr_t * vTemp; // temporary storage
+ // SAT calls statistics
+ int nSatUnsat; // the number of proofs
+ int nSatSat; // the number of failure
+ int nSatUndec; // the number of timeouts
+ int nSatTotal; // the number of calls
+ // conflicts
+ int nConfUnsat; // conflicts in unsat problems
+ int nConfSat; // conflicts in sat problems
+ int nConfUndec; // conflicts in undec problems
+ // runtime stats
+ abctime timeSatUnsat; // unsat
+ abctime timeSatSat; // sat
+ abctime timeSatUndec; // undecided
+ abctime timeTotal; // total runtime
+};
+
+static inline int Cbs2_VarIsAssigned( Gia_Obj_t * pVar ) { return pVar->fMark0; }
+static inline void Cbs2_VarAssign( Gia_Obj_t * pVar ) { assert(!pVar->fMark0); pVar->fMark0 = 1; }
+static inline void Cbs2_VarUnassign( Gia_Obj_t * pVar ) { assert(pVar->fMark0); pVar->fMark0 = 0; pVar->fMark1 = 0; pVar->Value = ~0; }
+static inline int Cbs2_VarValue( Gia_Obj_t * pVar ) { assert(pVar->fMark0); return pVar->fMark1; }
+static inline void Cbs2_VarSetValue( Gia_Obj_t * pVar, int v ) { assert(pVar->fMark0); pVar->fMark1 = v; }
+static inline int Cbs2_VarIsJust( Gia_Obj_t * pVar ) { return Gia_ObjIsAnd(pVar) && !Cbs2_VarIsAssigned(Gia_ObjFanin0(pVar)) && !Cbs2_VarIsAssigned(Gia_ObjFanin1(pVar)); }
+static inline int Cbs2_VarFanin0Value( Gia_Obj_t * pVar ) { return !Cbs2_VarIsAssigned(Gia_ObjFanin0(pVar)) ? 2 : (Cbs2_VarValue(Gia_ObjFanin0(pVar)) ^ Gia_ObjFaninC0(pVar)); }
+static inline int Cbs2_VarFanin1Value( Gia_Obj_t * pVar ) { return !Cbs2_VarIsAssigned(Gia_ObjFanin1(pVar)) ? 2 : (Cbs2_VarValue(Gia_ObjFanin1(pVar)) ^ Gia_ObjFaninC1(pVar)); }
+
+static inline int Cbs2_VarDecLevel( Cbs2_Man_t * p, Gia_Obj_t * pVar ) { assert( pVar->Value != ~0 ); return Vec_IntEntry(p->vLevReas, 3*pVar->Value); }
+static inline Gia_Obj_t * Cbs2_VarReason0( Cbs2_Man_t * p, Gia_Obj_t * pVar ) { assert( pVar->Value != ~0 ); return pVar + Vec_IntEntry(p->vLevReas, 3*pVar->Value+1); }
+static inline Gia_Obj_t * Cbs2_VarReason1( Cbs2_Man_t * p, Gia_Obj_t * pVar ) { assert( pVar->Value != ~0 ); return pVar + Vec_IntEntry(p->vLevReas, 3*pVar->Value+2); }
+static inline int Cbs2_ClauseDecLevel( Cbs2_Man_t * p, int hClause ) { return Cbs2_VarDecLevel( p, p->pClauses.pData[hClause] ); }
+
+#define Cbs2_QueForEachEntry( Que, pObj, i ) \
+ for ( i = (Que).iHead; (i < (Que).iTail) && ((pObj) = (Que).pData[i]); i++ )
+
+#define Cbs2_ClauseForEachVar( p, hClause, pObj ) \
+ for ( (p)->pIter = (p)->pClauses.pData + hClause; (pObj = *pIter); (p)->pIter++ )
+#define Cbs2_ClauseForEachVar1( p, hClause, pObj ) \
+ for ( (p)->pIter = (p)->pClauses.pData+hClause+1; (pObj = *pIter); (p)->pIter++ )
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Sets default values of the parameters.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cbs2_SetDefaultParams( Cbs2_Par_t * pPars )
+{
+ memset( pPars, 0, sizeof(Cbs2_Par_t) );
+ pPars->nBTLimit = 1000; // limit on the number of conflicts
+ pPars->nJustLimit = 100; // limit on the size of justification queue
+ pPars->fUseHighest = 1; // use node with the highest ID
+ pPars->fUseLowest = 0; // use node with the highest ID
+ pPars->fUseMaxFF = 0; // use node with the largest fanin fanout
+ pPars->fVerbose = 1; // print detailed statistics
+}
+void Cbs2_ManSetConflictNum( Cbs2_Man_t * p, int Num )
+{
+ p->Pars.nBTLimit = Num;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Cbs2_Man_t * Cbs2_ManAlloc( Gia_Man_t * pGia )
+{
+ Cbs2_Man_t * p;
+ p = ABC_CALLOC( Cbs2_Man_t, 1 );
+ p->pProp.nSize = p->pJust.nSize = p->pClauses.nSize = 10000;
+ p->pProp.pData = ABC_ALLOC( Gia_Obj_t *, p->pProp.nSize );
+ p->pJust.pData = ABC_ALLOC( Gia_Obj_t *, p->pJust.nSize );
+ p->pClauses.pData = ABC_ALLOC( Gia_Obj_t *, p->pClauses.nSize );
+ p->pClauses.iHead = p->pClauses.iTail = 1;
+ p->vModel = Vec_IntAlloc( 1000 );
+ p->vLevReas = Vec_IntAlloc( 1000 );
+ p->vTemp = Vec_PtrAlloc( 1000 );
+ p->pAig = pGia;
+ Cbs2_SetDefaultParams( &p->Pars );
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cbs2_ManStop( Cbs2_Man_t * p )
+{
+ Vec_IntFree( p->vLevReas );
+ Vec_IntFree( p->vModel );
+ Vec_PtrFree( p->vTemp );
+ ABC_FREE( p->pClauses.pData );
+ ABC_FREE( p->pProp.pData );
+ ABC_FREE( p->pJust.pData );
+ ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns satisfying assignment.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Cbs2_ReadModel( Cbs2_Man_t * p )
+{
+ return p->vModel;
+}
+
+
+
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if the solver is out of limits.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Cbs2_ManCheckLimits( Cbs2_Man_t * p )
+{
+ return p->Pars.nJustThis > p->Pars.nJustLimit || p->Pars.nBTThis > p->Pars.nBTLimit;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Saves the satisfying assignment as an array of literals.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Cbs2_ManSaveModel( Cbs2_Man_t * p, Vec_Int_t * vCex )
+{
+ Gia_Obj_t * pVar;
+ int i;
+ Vec_IntClear( vCex );
+ p->pProp.iHead = 0;
+ Cbs2_QueForEachEntry( p->pProp, pVar, i )
+ if ( Gia_ObjIsCi(pVar) )
+// Vec_IntPush( vCex, Abc_Var2Lit(Gia_ObjId(p->pAig,pVar), !Cbs2_VarValue(pVar)) );
+ Vec_IntPush( vCex, Abc_Var2Lit(Gia_ObjCioId(pVar), !Cbs2_VarValue(pVar)) );
+}
+static inline void Cbs2_ManSaveModelAll( Cbs2_Man_t * p, Vec_Int_t * vCex )
+{
+ Gia_Obj_t * pVar;
+ int i;
+ Vec_IntClear( vCex );
+ p->pProp.iHead = 0;
+ Cbs2_QueForEachEntry( p->pProp, pVar, i )
+ Vec_IntPush( vCex, Abc_Var2Lit(Gia_ObjId(p->pAig,pVar), !Cbs2_VarValue(pVar)) );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Cbs2_QueIsEmpty( Cbs2_Que_t * p )
+{
+ return p->iHead == p->iTail;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Cbs2_QuePush( Cbs2_Que_t * p, Gia_Obj_t * pObj )
+{
+ if ( p->iTail == p->nSize )
+ {
+ p->nSize *= 2;
+ p->pData = ABC_REALLOC( Gia_Obj_t *, p->pData, p->nSize );
+ }
+ p->pData[p->iTail++] = pObj;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if the object in the queue.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Cbs2_QueHasNode( Cbs2_Que_t * p, Gia_Obj_t * pObj )
+{
+ Gia_Obj_t * pTemp;
+ int i;
+ Cbs2_QueForEachEntry( *p, pTemp, i )
+ if ( pTemp == pObj )
+ return 1;
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Cbs2_QueStore( Cbs2_Que_t * p, int * piHeadOld, int * piTailOld )
+{
+ int i;
+ *piHeadOld = p->iHead;
+ *piTailOld = p->iTail;
+ for ( i = *piHeadOld; i < *piTailOld; i++ )
+ Cbs2_QuePush( p, p->pData[i] );
+ p->iHead = *piTailOld;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Cbs2_QueRestore( Cbs2_Que_t * p, int iHeadOld, int iTailOld )
+{
+ p->iHead = iHeadOld;
+ p->iTail = iTailOld;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Finalized the clause.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Cbs2_QueFinish( Cbs2_Que_t * p )
+{
+ int iHeadOld = p->iHead;
+ assert( p->iHead < p->iTail );
+ Cbs2_QuePush( p, NULL );
+ p->iHead = p->iTail;
+ return iHeadOld;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Max number of fanins fanouts.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Cbs2_VarFaninFanoutMax( Cbs2_Man_t * p, Gia_Obj_t * pObj )
+{
+ int Count0, Count1;
+ assert( !Gia_IsComplement(pObj) );
+ assert( Gia_ObjIsAnd(pObj) );
+ Count0 = Gia_ObjRefNum( p->pAig, Gia_ObjFanin0(pObj) );
+ Count1 = Gia_ObjRefNum( p->pAig, Gia_ObjFanin1(pObj) );
+ return Abc_MaxInt( Count0, Count1 );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Find variable with the highest ID.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline Gia_Obj_t * Cbs2_ManDecideHighest( Cbs2_Man_t * p )
+{
+ Gia_Obj_t * pObj, * pObjMax = NULL;
+ int i;
+ Cbs2_QueForEachEntry( p->pJust, pObj, i )
+ if ( pObjMax == NULL || pObjMax < pObj )
+ pObjMax = pObj;
+ return pObjMax;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Find variable with the lowest ID.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline Gia_Obj_t * Cbs2_ManDecideLowest( Cbs2_Man_t * p )
+{
+ Gia_Obj_t * pObj, * pObjMin = NULL;
+ int i;
+ Cbs2_QueForEachEntry( p->pJust, pObj, i )
+ if ( pObjMin == NULL || pObjMin > pObj )
+ pObjMin = pObj;
+ return pObjMin;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Find variable with the maximum number of fanin fanouts.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline Gia_Obj_t * Cbs2_ManDecideMaxFF( Cbs2_Man_t * p )
+{
+ Gia_Obj_t * pObj, * pObjMax = NULL;
+ int i, iMaxFF = 0, iCurFF;
+ assert( p->pAig->pRefs != NULL );
+ Cbs2_QueForEachEntry( p->pJust, pObj, i )
+ {
+ iCurFF = Cbs2_VarFaninFanoutMax( p, pObj );
+ assert( iCurFF > 0 );
+ if ( iMaxFF < iCurFF )
+ {
+ iMaxFF = iCurFF;
+ pObjMax = pObj;
+ }
+ }
+ return pObjMax;
+}
+
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Cbs2_ManCancelUntil( Cbs2_Man_t * p, int iBound )
+{
+ Gia_Obj_t * pVar;
+ int i;
+ assert( iBound <= p->pProp.iTail );
+ p->pProp.iHead = iBound;
+ Cbs2_QueForEachEntry( p->pProp, pVar, i )
+ Cbs2_VarUnassign( pVar );
+ p->pProp.iTail = iBound;
+ Vec_IntShrink( p->vLevReas, 3*iBound );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Assigns the variables a value.]
+
+ Description [Returns 1 if conflict; 0 if no conflict.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Cbs2_ManAssign( Cbs2_Man_t * p, Gia_Obj_t * pObj, int Level, Gia_Obj_t * pRes0, Gia_Obj_t * pRes1 )
+{
+ Gia_Obj_t * pObjR = Gia_Regular(pObj);
+ assert( Gia_ObjIsCand(pObjR) );
+ assert( !Cbs2_VarIsAssigned(pObjR) );
+ Cbs2_VarAssign( pObjR );
+ Cbs2_VarSetValue( pObjR, !Gia_IsComplement(pObj) );
+ assert( pObjR->Value == ~0 );
+ pObjR->Value = p->pProp.iTail;
+ Cbs2_QuePush( &p->pProp, pObjR );
+ Vec_IntPush( p->vLevReas, Level );
+ Vec_IntPush( p->vLevReas, pRes0 ? pRes0-pObjR : 0 );
+ Vec_IntPush( p->vLevReas, pRes1 ? pRes1-pObjR : 0 );
+ assert( Vec_IntSize(p->vLevReas) == 3 * p->pProp.iTail );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Returns clause size.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Cbs2_ManClauseSize( Cbs2_Man_t * p, int hClause )
+{
+ Cbs2_Que_t * pQue = &(p->pClauses);
+ Gia_Obj_t ** pIter;
+ for ( pIter = pQue->pData + hClause; *pIter; pIter++ );
+ return pIter - pQue->pData - hClause ;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prints conflict clause.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Cbs2_ManPrintClause( Cbs2_Man_t * p, int Level, int hClause )
+{
+ Cbs2_Que_t * pQue = &(p->pClauses);
+ Gia_Obj_t * pObj;
+ int i;
+ assert( Cbs2_QueIsEmpty( pQue ) );
+ printf( "Level %2d : ", Level );
+ for ( i = hClause; (pObj = pQue->pData[i]); i++ )
+ printf( "%d=%d(%d) ", Gia_ObjId(p->pAig, pObj), Cbs2_VarValue(pObj), Cbs2_VarDecLevel(p, pObj) );
+ printf( "\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prints conflict clause.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Cbs2_ManPrintClauseNew( Cbs2_Man_t * p, int Level, int hClause )
+{
+ Cbs2_Que_t * pQue = &(p->pClauses);
+ Gia_Obj_t * pObj;
+ int i;
+ assert( Cbs2_QueIsEmpty( pQue ) );
+ printf( "Level %2d : ", Level );
+ for ( i = hClause; (pObj = pQue->pData[i]); i++ )
+ printf( "%c%d ", Cbs2_VarValue(pObj)? '+':'-', Gia_ObjId(p->pAig, pObj) );
+ printf( "\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns conflict clause.]
+
+ Description [Performs conflict analysis.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Cbs2_ManDeriveReason( Cbs2_Man_t * p, int Level )
+{
+ Cbs2_Que_t * pQue = &(p->pClauses);
+ Gia_Obj_t * pObj, * pReason;
+ int i, k, iLitLevel;
+ assert( pQue->pData[pQue->iHead] == NULL );
+ assert( pQue->iHead + 1 < pQue->iTail );
+/*
+ for ( i = pQue->iHead + 1; i < pQue->iTail; i++ )
+ {
+ pObj = pQue->pData[i];
+ assert( pObj->fMark0 == 1 );
+ }
+*/
+ // compact literals
+ Vec_PtrClear( p->vTemp );
+ for ( i = k = pQue->iHead + 1; i < pQue->iTail; i++ )
+ {
+ pObj = pQue->pData[i];
+ if ( !pObj->fMark0 ) // unassigned - seen again
+ continue;
+ // assigned - seen first time
+ pObj->fMark0 = 0;
+ Vec_PtrPush( p->vTemp, pObj );
+ // check decision level
+ iLitLevel = Cbs2_VarDecLevel( p, pObj );
+ if ( iLitLevel < Level )
+ {
+ pQue->pData[k++] = pObj;
+ continue;
+ }
+ assert( iLitLevel == Level );
+ pReason = Cbs2_VarReason0( p, pObj );
+ if ( pReason == pObj ) // no reason
+ {
+ //assert( pQue->pData[pQue->iHead] == NULL );
+ pQue->pData[pQue->iHead] = pObj;
+ continue;
+ }
+ Cbs2_QuePush( pQue, pReason );
+ pReason = Cbs2_VarReason1( p, pObj );
+ if ( pReason != pObj ) // second reason
+ Cbs2_QuePush( pQue, pReason );
+ }
+ assert( pQue->pData[pQue->iHead] != NULL );
+ pQue->iTail = k;
+ // clear the marks
+ Vec_PtrForEachEntry( Gia_Obj_t *, p->vTemp, pObj, i )
+ pObj->fMark0 = 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns conflict clause.]
+
+ Description [Performs conflict analysis.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Cbs2_ManAnalyze( Cbs2_Man_t * p, int Level, Gia_Obj_t * pVar, Gia_Obj_t * pFan0, Gia_Obj_t * pFan1 )
+{
+ Cbs2_Que_t * pQue = &(p->pClauses);
+ assert( Cbs2_VarIsAssigned(pVar) );
+ assert( Cbs2_VarIsAssigned(pFan0) );
+ assert( pFan1 == NULL || Cbs2_VarIsAssigned(pFan1) );
+ assert( Cbs2_QueIsEmpty( pQue ) );
+ Cbs2_QuePush( pQue, NULL );
+ Cbs2_QuePush( pQue, pVar );
+ Cbs2_QuePush( pQue, pFan0 );
+ if ( pFan1 )
+ Cbs2_QuePush( pQue, pFan1 );
+ Cbs2_ManDeriveReason( p, Level );
+ return Cbs2_QueFinish( pQue );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Performs resolution of two clauses.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Cbs2_ManResolve( Cbs2_Man_t * p, int Level, int hClause0, int hClause1 )
+{
+ Cbs2_Que_t * pQue = &(p->pClauses);
+ Gia_Obj_t * pObj;
+ int i, LevelMax = -1, LevelCur;
+ assert( pQue->pData[hClause0] != NULL );
+ assert( pQue->pData[hClause0] == pQue->pData[hClause1] );
+/*
+ for ( i = hClause0 + 1; (pObj = pQue->pData[i]); i++ )
+ assert( pObj->fMark0 == 1 );
+ for ( i = hClause1 + 1; (pObj = pQue->pData[i]); i++ )
+ assert( pObj->fMark0 == 1 );
+*/
+ assert( Cbs2_QueIsEmpty( pQue ) );
+ Cbs2_QuePush( pQue, NULL );
+ for ( i = hClause0 + 1; (pObj = pQue->pData[i]); i++ )
+ {
+ if ( !pObj->fMark0 ) // unassigned - seen again
+ continue;
+ // assigned - seen first time
+ pObj->fMark0 = 0;
+ Cbs2_QuePush( pQue, pObj );
+ LevelCur = Cbs2_VarDecLevel( p, pObj );
+ if ( LevelMax < LevelCur )
+ LevelMax = LevelCur;
+ }
+ for ( i = hClause1 + 1; (pObj = pQue->pData[i]); i++ )
+ {
+ if ( !pObj->fMark0 ) // unassigned - seen again
+ continue;
+ // assigned - seen first time
+ pObj->fMark0 = 0;
+ Cbs2_QuePush( pQue, pObj );
+ LevelCur = Cbs2_VarDecLevel( p, pObj );
+ if ( LevelMax < LevelCur )
+ LevelMax = LevelCur;
+ }
+ for ( i = pQue->iHead + 1; i < pQue->iTail; i++ )
+ pQue->pData[i]->fMark0 = 1;
+ Cbs2_ManDeriveReason( p, LevelMax );
+ return Cbs2_QueFinish( pQue );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Propagates a variable.]
+
+ Description [Returns clause handle if conflict; 0 if no conflict.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Cbs2_ManPropagateOne( Cbs2_Man_t * p, Gia_Obj_t * pVar, int Level )
+{
+ int Value0, Value1;
+ assert( !Gia_IsComplement(pVar) );
+ assert( Cbs2_VarIsAssigned(pVar) );
+ if ( Gia_ObjIsCi(pVar) )
+ return 0;
+ assert( Gia_ObjIsAnd(pVar) );
+ Value0 = Cbs2_VarFanin0Value(pVar);
+ Value1 = Cbs2_VarFanin1Value(pVar);
+ if ( Cbs2_VarValue(pVar) )
+ { // value is 1
+ if ( Value0 == 0 || Value1 == 0 ) // one is 0
+ {
+ if ( Value0 == 0 && Value1 != 0 )
+ return Cbs2_ManAnalyze( p, Level, pVar, Gia_ObjFanin0(pVar), NULL );
+ if ( Value0 != 0 && Value1 == 0 )
+ return Cbs2_ManAnalyze( p, Level, pVar, Gia_ObjFanin1(pVar), NULL );
+ assert( Value0 == 0 && Value1 == 0 );
+ return Cbs2_ManAnalyze( p, Level, pVar, Gia_ObjFanin0(pVar), Gia_ObjFanin1(pVar) );
+ }
+ if ( Value0 == 2 ) // first is unassigned
+ Cbs2_ManAssign( p, Gia_ObjChild0(pVar), Level, pVar, NULL );
+ if ( Value1 == 2 ) // first is unassigned
+ Cbs2_ManAssign( p, Gia_ObjChild1(pVar), Level, pVar, NULL );
+ return 0;
+ }
+ // value is 0
+ if ( Value0 == 0 || Value1 == 0 ) // one is 0
+ return 0;
+ if ( Value0 == 1 && Value1 == 1 ) // both are 1
+ return Cbs2_ManAnalyze( p, Level, pVar, Gia_ObjFanin0(pVar), Gia_ObjFanin1(pVar) );
+ if ( Value0 == 1 || Value1 == 1 ) // one is 1
+ {
+ if ( Value0 == 2 ) // first is unassigned
+ Cbs2_ManAssign( p, Gia_Not(Gia_ObjChild0(pVar)), Level, pVar, Gia_ObjFanin1(pVar) );
+ if ( Value1 == 2 ) // second is unassigned
+ Cbs2_ManAssign( p, Gia_Not(Gia_ObjChild1(pVar)), Level, pVar, Gia_ObjFanin0(pVar) );
+ return 0;
+ }
+ assert( Cbs2_VarIsJust(pVar) );
+ assert( !Cbs2_QueHasNode( &p->pJust, pVar ) );
+ Cbs2_QuePush( &p->pJust, pVar );
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Propagates a variable.]
+
+ Description [Returns 1 if conflict; 0 if no conflict.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Cbs2_ManPropagateTwo( Cbs2_Man_t * p, Gia_Obj_t * pVar, int Level )
+{
+ int Value0, Value1;
+ assert( !Gia_IsComplement(pVar) );
+ assert( Gia_ObjIsAnd(pVar) );
+ assert( Cbs2_VarIsAssigned(pVar) );
+ assert( !Cbs2_VarValue(pVar) );
+ Value0 = Cbs2_VarFanin0Value(pVar);
+ Value1 = Cbs2_VarFanin1Value(pVar);
+ // value is 0
+ if ( Value0 == 0 || Value1 == 0 ) // one is 0
+ return 0;
+ if ( Value0 == 1 && Value1 == 1 ) // both are 1
+ return Cbs2_ManAnalyze( p, Level, pVar, Gia_ObjFanin0(pVar), Gia_ObjFanin1(pVar) );
+ assert( Value0 == 1 || Value1 == 1 );
+ if ( Value0 == 2 ) // first is unassigned
+ Cbs2_ManAssign( p, Gia_Not(Gia_ObjChild0(pVar)), Level, pVar, Gia_ObjFanin1(pVar) );
+ if ( Value1 == 2 ) // first is unassigned
+ Cbs2_ManAssign( p, Gia_Not(Gia_ObjChild1(pVar)), Level, pVar, Gia_ObjFanin0(pVar) );
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Propagates all variables.]
+
+ Description [Returns 1 if conflict; 0 if no conflict.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Cbs2_ManPropagate( Cbs2_Man_t * p, int Level )
+{
+ int hClause;
+ Gia_Obj_t * pVar;
+ int i, k;
+ while ( 1 )
+ {
+ Cbs2_QueForEachEntry( p->pProp, pVar, i )
+ {
+ if ( (hClause = Cbs2_ManPropagateOne( p, pVar, Level )) )
+ return hClause;
+ }
+ p->pProp.iHead = p->pProp.iTail;
+ k = p->pJust.iHead;
+ Cbs2_QueForEachEntry( p->pJust, pVar, i )
+ {
+ if ( Cbs2_VarIsJust( pVar ) )
+ p->pJust.pData[k++] = pVar;
+ else if ( (hClause = Cbs2_ManPropagateTwo( p, pVar, Level )) )
+ return hClause;
+ }
+ if ( k == p->pJust.iTail )
+ break;
+ p->pJust.iTail = k;
+ }
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Solve the problem recursively.]
+
+ Description [Returns learnt clause if unsat, NULL if sat or undecided.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Cbs2_ManSolve_rec( Cbs2_Man_t * p, int Level )
+{
+ Cbs2_Que_t * pQue = &(p->pClauses);
+ Gia_Obj_t * pVar = NULL, * pDecVar;
+ int hClause, hLearn0, hLearn1;
+ int iPropHead, iJustHead, iJustTail;
+ // propagate assignments
+ assert( !Cbs2_QueIsEmpty(&p->pProp) );
+ if ( (hClause = Cbs2_ManPropagate( p, Level )) )
+ return hClause;
+ // check for satisfying assignment
+ assert( Cbs2_QueIsEmpty(&p->pProp) );
+ if ( Cbs2_QueIsEmpty(&p->pJust) )
+ return 0;
+ // quit using resource limits
+ p->Pars.nJustThis = Abc_MaxInt( p->Pars.nJustThis, p->pJust.iTail - p->pJust.iHead );
+ if ( Cbs2_ManCheckLimits( p ) )
+ return 0;
+ // remember the state before branching
+ iPropHead = p->pProp.iHead;
+ Cbs2_QueStore( &p->pJust, &iJustHead, &iJustTail );
+ // find the decision variable
+ if ( p->Pars.fUseHighest )
+ pVar = Cbs2_ManDecideHighest( p );
+ else if ( p->Pars.fUseLowest )
+ pVar = Cbs2_ManDecideLowest( p );
+ else if ( p->Pars.fUseMaxFF )
+ pVar = Cbs2_ManDecideMaxFF( p );
+ else assert( 0 );
+ assert( Cbs2_VarIsJust( pVar ) );
+ // chose decision variable using fanout count
+ if ( Gia_ObjRefNum(p->pAig, Gia_ObjFanin0(pVar)) > Gia_ObjRefNum(p->pAig, Gia_ObjFanin1(pVar)) )
+ pDecVar = Gia_Not(Gia_ObjChild0(pVar));
+ else
+ pDecVar = Gia_Not(Gia_ObjChild1(pVar));
+// pDecVar = Gia_NotCond( Gia_Regular(pDecVar), Gia_Regular(pDecVar)->fPhase );
+// pDecVar = Gia_Not(pDecVar);
+ // decide on first fanin
+ Cbs2_ManAssign( p, pDecVar, Level+1, NULL, NULL );
+ if ( !(hLearn0 = Cbs2_ManSolve_rec( p, Level+1 )) )
+ return 0;
+ if ( pQue->pData[hLearn0] != Gia_Regular(pDecVar) )
+ return hLearn0;
+ Cbs2_ManCancelUntil( p, iPropHead );
+ Cbs2_QueRestore( &p->pJust, iJustHead, iJustTail );
+ // decide on second fanin
+ Cbs2_ManAssign( p, Gia_Not(pDecVar), Level+1, NULL, NULL );
+ if ( !(hLearn1 = Cbs2_ManSolve_rec( p, Level+1 )) )
+ return 0;
+ if ( pQue->pData[hLearn1] != Gia_Regular(pDecVar) )
+ return hLearn1;
+ hClause = Cbs2_ManResolve( p, Level, hLearn0, hLearn1 );
+// Cbs2_ManPrintClauseNew( p, Level, hClause );
+// if ( Level > Cbs2_ClauseDecLevel(p, hClause) )
+// p->Pars.nBTThisNc++;
+ p->Pars.nBTThis++;
+ return hClause;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Looking for a satisfying assignment of the node.]
+
+ Description [Assumes that each node has flag pObj->fMark0 set to 0.
+ Returns 1 if unsatisfiable, 0 if satisfiable, and -1 if undecided.
+ The node may be complemented. ]
+
+ SideEffects [The two procedures differ in the CEX format.]
+
+ SeeAlso []
+
+***********************************************************************/
+int Cbs2_ManSolve( Cbs2_Man_t * p, Gia_Obj_t * pObj )
+{
+ int RetValue = 0;
+ assert( !p->pProp.iHead && !p->pProp.iTail );
+ assert( !p->pJust.iHead && !p->pJust.iTail );
+ assert( p->pClauses.iHead == 1 && p->pClauses.iTail == 1 );
+ p->Pars.nBTThis = p->Pars.nJustThis = p->Pars.nBTThisNc = 0;
+ Cbs2_ManAssign( p, pObj, 0, NULL, NULL );
+ if ( !Cbs2_ManSolve_rec(p, 0) && !Cbs2_ManCheckLimits(p) )
+ Cbs2_ManSaveModel( p, p->vModel );
+ else
+ RetValue = 1;
+ Cbs2_ManCancelUntil( p, 0 );
+ p->pJust.iHead = p->pJust.iTail = 0;
+ p->pClauses.iHead = p->pClauses.iTail = 1;
+ p->Pars.nBTTotal += p->Pars.nBTThis;
+ p->Pars.nJustTotal = Abc_MaxInt( p->Pars.nJustTotal, p->Pars.nJustThis );
+ if ( Cbs2_ManCheckLimits( p ) )
+ RetValue = -1;
+ return RetValue;
+}
+int Cbs2_ManSolve2( Cbs2_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 )
+{
+ int RetValue = 0;
+ assert( !p->pProp.iHead && !p->pProp.iTail );
+ assert( !p->pJust.iHead && !p->pJust.iTail );
+ assert( p->pClauses.iHead == 1 && p->pClauses.iTail == 1 );
+ p->Pars.nBTThis = p->Pars.nJustThis = p->Pars.nBTThisNc = 0;
+ Cbs2_ManAssign( p, pObj, 0, NULL, NULL );
+ if ( pObj2 )
+ Cbs2_ManAssign( p, pObj2, 0, NULL, NULL );
+ if ( !Cbs2_ManSolve_rec(p, 0) && !Cbs2_ManCheckLimits(p) )
+ Cbs2_ManSaveModelAll( p, p->vModel );
+ else
+ RetValue = 1;
+ Cbs2_ManCancelUntil( p, 0 );
+ p->pJust.iHead = p->pJust.iTail = 0;
+ p->pClauses.iHead = p->pClauses.iTail = 1;
+ p->Pars.nBTTotal += p->Pars.nBTThis;
+ p->Pars.nJustTotal = Abc_MaxInt( p->Pars.nJustTotal, p->Pars.nJustThis );
+ if ( Cbs2_ManCheckLimits( p ) )
+ RetValue = -1;
+ return RetValue;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prints statistics of the manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cbs2_ManSatPrintStats( Cbs2_Man_t * p )
+{
+ printf( "CO = %8d ", Gia_ManCoNum(p->pAig) );
+ printf( "AND = %8d ", Gia_ManAndNum(p->pAig) );
+ printf( "Conf = %6d ", p->Pars.nBTLimit );
+ printf( "JustMax = %5d ", p->Pars.nJustLimit );
+ printf( "\n" );
+ printf( "Unsat calls %6d (%6.2f %%) Ave conf = %8.1f ",
+ p->nSatUnsat, p->nSatTotal? 100.0*p->nSatUnsat/p->nSatTotal :0.0, p->nSatUnsat? 1.0*p->nConfUnsat/p->nSatUnsat :0.0 );
+ ABC_PRTP( "Time", p->timeSatUnsat, p->timeTotal );
+ printf( "Sat calls %6d (%6.2f %%) Ave conf = %8.1f ",
+ p->nSatSat, p->nSatTotal? 100.0*p->nSatSat/p->nSatTotal :0.0, p->nSatSat? 1.0*p->nConfSat/p->nSatSat : 0.0 );
+ ABC_PRTP( "Time", p->timeSatSat, p->timeTotal );
+ printf( "Undef calls %6d (%6.2f %%) Ave conf = %8.1f ",
+ p->nSatUndec, p->nSatTotal? 100.0*p->nSatUndec/p->nSatTotal :0.0, p->nSatUndec? 1.0*p->nConfUndec/p->nSatUndec : 0.0 );
+ ABC_PRTP( "Time", p->timeSatUndec, p->timeTotal );
+ ABC_PRT( "Total time", p->timeTotal );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Procedure to test the new SAT solver.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Cbs2_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStatus, int fVerbose )
+{
+ extern void Gia_ManCollectTest( Gia_Man_t * pAig );
+ extern void Cec_ManSatAddToStore( Vec_Int_t * vCexStore, Vec_Int_t * vCex, int Out );
+ Cbs2_Man_t * p;
+ Vec_Int_t * vCex, * vVisit, * vCexStore;
+ Vec_Str_t * vStatus;
+ Gia_Obj_t * pRoot;
+ int i, status;
+ abctime clk, clkTotal = Abc_Clock();
+ assert( Gia_ManRegNum(pAig) == 0 );
+// Gia_ManCollectTest( pAig );
+ // prepare AIG
+ Gia_ManCreateRefs( pAig );
+ Gia_ManCleanMark0( pAig );
+ Gia_ManCleanMark1( pAig );
+ Gia_ManFillValue( pAig ); // maps nodes into trail ids
+ Gia_ManSetPhase( pAig ); // maps nodes into trail ids
+ // create logic network
+ p = Cbs2_ManAlloc( pAig );
+ p->Pars.nBTLimit = nConfs;
+ // create resulting data-structures
+ vStatus = Vec_StrAlloc( Gia_ManPoNum(pAig) );
+ vCexStore = Vec_IntAlloc( 10000 );
+ vVisit = Vec_IntAlloc( 100 );
+ vCex = Cbs2_ReadModel( p );
+ // solve for each output
+ Gia_ManForEachCo( pAig, pRoot, i )
+ {
+// printf( "\n" );
+
+ Vec_IntClear( vCex );
+ if ( Gia_ObjIsConst0(Gia_ObjFanin0(pRoot)) )
+ {
+ if ( Gia_ObjFaninC0(pRoot) )
+ {
+// printf( "Constant 1 output of SRM!!!\n" );
+ Cec_ManSatAddToStore( vCexStore, vCex, i ); // trivial counter-example
+ Vec_StrPush( vStatus, 0 );
+ }
+ else
+ {
+// printf( "Constant 0 output of SRM!!!\n" );
+ Vec_StrPush( vStatus, 1 );
+ }
+ continue;
+ }
+ clk = Abc_Clock();
+ p->Pars.fUseHighest = 1;
+ p->Pars.fUseLowest = 0;
+ status = Cbs2_ManSolve( p, Gia_ObjChild0(pRoot) );
+// printf( "\n" );
+/*
+ if ( status == -1 )
+ {
+ p->Pars.fUseHighest = 0;
+ p->Pars.fUseLowest = 1;
+ status = Cbs2_ManSolve( p, Gia_ObjChild0(pRoot) );
+ }
+*/
+ Vec_StrPush( vStatus, (char)status );
+ if ( status == -1 )
+ {
+ p->nSatUndec++;
+ p->nConfUndec += p->Pars.nBTThis;
+ Cec_ManSatAddToStore( vCexStore, NULL, i ); // timeout
+ p->timeSatUndec += Abc_Clock() - clk;
+ continue;
+ }
+ if ( status == 1 )
+ {
+ p->nSatUnsat++;
+ p->nConfUnsat += p->Pars.nBTThis;
+ p->timeSatUnsat += Abc_Clock() - clk;
+ continue;
+ }
+ p->nSatSat++;
+ p->nConfSat += p->Pars.nBTThis;
+// Gia_SatVerifyPattern( pAig, pRoot, vCex, vVisit );
+ Cec_ManSatAddToStore( vCexStore, vCex, i );
+ p->timeSatSat += Abc_Clock() - clk;
+ }
+ Vec_IntFree( vVisit );
+ p->nSatTotal = Gia_ManPoNum(pAig);
+ p->timeTotal = Abc_Clock() - clkTotal;
+ if ( fVerbose )
+ Cbs2_ManSatPrintStats( p );
+// printf( "RecCalls = %8d. RecClause = %8d. RecNonChro = %8d.\n", p->nRecCall, p->nRecClause, p->nRecNonChro );
+ Cbs2_ManStop( p );
+ *pvStatus = vStatus;
+
+// printf( "Total number of cex literals = %d. (Ave = %d)\n",
+// Vec_IntSize(vCexStore)-2*p->nSatUndec-2*p->nSatSat,
+// (Vec_IntSize(vCexStore)-2*p->nSatUndec-2*p->nSatSat)/p->nSatSat );
+ return vCexStore;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make
index 7a0e1617..3fc41108 100644
--- a/src/aig/gia/module.make
+++ b/src/aig/gia/module.make
@@ -13,6 +13,7 @@ SRC += src/aig/gia/giaAig.c \
src/aig/gia/giaCone.c \
src/aig/gia/giaCSatOld.c \
src/aig/gia/giaCSat.c \
+ src/aig/gia/giaCSat2.c \
src/aig/gia/giaCTas.c \
src/aig/gia/giaCut.c \
src/aig/gia/giaDfs.c \
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 0c2b72ec..67854f1a 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -33640,13 +33640,14 @@ usage:
***********************************************************************/
int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
{
+ extern Vec_Int_t * Cbs2_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStatus, int fVerbose );
Cec_ParSat_t ParsSat, * pPars = &ParsSat;
Gia_Man_t * pTemp;
int c;
- int fCSat = 0;
+ int fNewSolver = 0, fCSat = 0;
Cec_ManSatSetDefaultParams( pPars );
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "CSNnmtcvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "CSNanmtcvh" ) ) != EOF )
{
switch ( c )
{
@@ -33683,6 +33684,9 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nCallsRecycle < 0 )
goto usage;
break;
+ case 'a':
+ fNewSolver ^= 1;
+ break;
case 'n':
pPars->fNonChrono ^= 1;
break;
@@ -33711,7 +33715,9 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Vec_Int_t * vCounters;
Vec_Str_t * vStatus;
- if ( pPars->fLearnCls )
+ if ( fNewSolver )
+ vCounters = Cbs2_ManSolveMiterNc( pAbc->pGia, pPars->nBTLimit, &vStatus, pPars->fVerbose );
+ else if ( pPars->fLearnCls )
vCounters = Tas_ManSolveMiterNc( pAbc->pGia, pPars->nBTLimit, &vStatus, pPars->fVerbose );
else if ( pPars->fNonChrono )
vCounters = Cbs_ManSolveMiterNc( pAbc->pGia, pPars->nBTLimit, &vStatus, pPars->fVerbose );
@@ -33728,11 +33734,12 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- Abc_Print( -2, "usage: &sat [-CSN <num>] [-nmctvh]\n" );
+ Abc_Print( -2, "usage: &sat [-CSN <num>] [-anmctvh]\n" );
Abc_Print( -2, "\t performs SAT solving for the combinational outputs\n" );
Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
Abc_Print( -2, "\t-S num : the min number of variables to recycle the solver [default = %d]\n", pPars->nSatVarMax );
Abc_Print( -2, "\t-N num : the min number of calls to recycle the solver [default = %d]\n", pPars->nCallsRecycle );
+ Abc_Print( -2, "\t-a : toggle using new solver [default = %s]\n", fNewSolver? "yes": "no" );
Abc_Print( -2, "\t-n : toggle using non-chronological backtracking [default = %s]\n", pPars->fNonChrono? "yes": "no" );
Abc_Print( -2, "\t-m : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "miter": "circuit" );
Abc_Print( -2, "\t-c : toggle using circuit-based SAT solver [default = %s]\n", fCSat? "yes": "no" );
@@ -44856,6 +44863,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
// Gia_ParTest( pAbc->pGia, nWords, nProcs );
// Gia_StoComputeCuts( pAbc->pGia );
// printf( "\nThis command is currently disabled.\n\n" );
+/*
{
char Buffer[10];
extern void Gia_DumpLutSizeDistrib( Gia_Man_t * p, char * pFileName );
@@ -44863,6 +44871,9 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pAbc->pGia )
Gia_DumpLutSizeDistrib( pAbc->pGia, Buffer );
}
+*/
+// pTemp = Slv_ManToAig( pAbc->pGia );
+// Abc_FrameUpdateGia( pAbc, pTemp );
return 0;
usage:
Abc_Print( -2, "usage: &test [-FW num] [-svh]\n" );
diff --git a/src/proof/cec/cecCore.c b/src/proof/cec/cecCore.c
index ccc5a8e6..85fcfa26 100644
--- a/src/proof/cec/cecCore.c
+++ b/src/proof/cec/cecCore.c
@@ -48,7 +48,7 @@ void Cec_ManSatSetDefaultParams( Cec_ParSat_t * p )
p->nBTLimit = 100; // conflict limit at a node
p->nSatVarMax = 2000; // the max number of SAT variables
p->nCallsRecycle = 200; // calls to perform before recycling SAT solver
- p->fNonChrono = 0; // use non-chronological backtracling (for circuit SAT only)
+ p->fNonChrono = 1; // use non-chronological backtracling (for circuit SAT only)
p->fPolarFlip = 1; // flops polarity of variables
p->fCheckMiter = 0; // the circuit is the miter
// p->fFirstStop = 0; // stop on the first sat output
generated by cgit v1.2.3 (git 2.25.1) at 2025-10-31 14:13:32 +0000