From a6aec18afb8cf503d9168a22197867c5f431fbb8 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 25 Dec 2005 08:01:00 -0800 Subject: Version abc51225 --- src/sat/asat/solver.h | 5 +++-- src/sat/fraig/fraigCanon.c | 4 ++-- src/sat/fraig/fraigSat.c | 22 +++++++++++++++++++++- src/sat/msat/msat.h | 1 + src/sat/msat/msatClause.c | 5 +++++ src/sat/msat/msatInt.h | 1 + src/sat/msat/msatSolverApi.c | 1 + src/sat/msat/msatSolverCore.c | 20 ++++++++++++++++++++ 8 files changed, 54 insertions(+), 5 deletions(-) (limited to 'src/sat') diff --git a/src/sat/asat/solver.h b/src/sat/asat/solver.h index b82601c4..9618603c 100644 --- a/src/sat/asat/solver.h +++ b/src/sat/asat/solver.h @@ -52,8 +52,9 @@ static const lbool l_Undef = 0; static const lbool l_True = 1; static const lbool l_False = -1; -static inline lit neg (lit l) { return l ^ 1; } -static inline lit toLit (int v) { return v + v; } +static inline lit neg (lit l) { return l ^ 1; } +static inline lit toLit (int v) { return v + v; } +static inline lit toLitCond (int v, int c) { return v + v + (int)(c != 0); } //================================================================================================= // Public interface: diff --git a/src/sat/fraig/fraigCanon.c b/src/sat/fraig/fraigCanon.c index 97da413d..fab01368 100644 --- a/src/sat/fraig/fraigCanon.c +++ b/src/sat/fraig/fraigCanon.c @@ -68,7 +68,7 @@ Fraig_Node_t * Fraig_NodeAndCanon( Fraig_Man_t * pMan, Fraig_Node_t * p1, Fraig_ return p1; return Fraig_Not(pMan->pConst1); } - +/* // check for less trivial cases if ( Fraig_IsComplement(p1) ) { @@ -125,7 +125,7 @@ Fraig_Node_t * Fraig_NodeAndCanon( Fraig_Man_t * pMan, Fraig_Node_t * p1, Fraig_ return Fraig_Not(pMan->pConst1); } } - +*/ // perform level-one structural hashing if ( Fraig_HashTableLookupS( pMan, p1, p2, &pNodeNew ) ) // the node with these children is found { diff --git a/src/sat/fraig/fraigSat.c b/src/sat/fraig/fraigSat.c index bc60e4e9..13f6b50b 100644 --- a/src/sat/fraig/fraigSat.c +++ b/src/sat/fraig/fraigSat.c @@ -41,6 +41,8 @@ extern void * Msat_ClauseVecReadEntry( void * p, int i ); // The best way seems to be fanins followed by fanouts. Slight changes to this order // leads to big degradation in quality. +static int nMuxes; + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -105,7 +107,7 @@ void Fraig_ManProveMiter( Fraig_Man_t * p ) } if ( p->fVerboseP ) { - PRT( "Final miter proof time", clock() - clk ); +// PRT( "Final miter proof time", clock() - clk ); } } @@ -195,6 +197,8 @@ int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * } */ + nMuxes = 0; + // get the logic cone clk = clock(); @@ -202,6 +206,9 @@ clk = clock(); // Fraig_PrepareCones( p, pOld, pNew ); p->timeTrav += clock() - clk; +// printf( "The number of MUXes detected = %d (%5.2f %% of logic). ", nMuxes, 300.0*nMuxes/(p->vNodes->nSize - p->vInputs->nSize) ); +// PRT( "Time", clock() - clk ); + if ( fVerbose ) printf( "%d(%d) - ", Fraig_CountPis(p,p->vVarsInt), Msat_IntVecReadSize(p->vVarsInt) ); @@ -226,6 +233,8 @@ clk = clock(); RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, nTimeLimit ); p->timeSat += clock() - clk; +Msat_SolverWriteDimacs( p->pSat, "temp_fraig.cnf" ); + if ( RetValue1 == MSAT_FALSE ) { //p->time1 += clock() - clk; @@ -284,6 +293,7 @@ p->time3 += clock() - clk; clk = clock(); RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, nTimeLimit ); p->timeSat += clock() - clk; + if ( RetValue1 == MSAT_FALSE ) { //p->time1 += clock() - clk; @@ -552,6 +562,7 @@ void Fraig_PrepareCones( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t * Fraig_PrepareCones_rec( pMan, pNew ); Fraig_PrepareCones_rec( pMan, pOld ); + /* nVars = Msat_IntVecReadSize( pMan->vVarsInt ); pVars = Msat_IntVecReadArray( pMan->vVarsInt ); @@ -715,6 +726,8 @@ void Fraig_OrderVariables( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t Fraig_NodeVecPushUnique( pNode->vFanins, Fraig_Regular(Fraig_Regular(pNode->p2)->p2) ); Fraig_SupergateAddClausesMux( pMan, pNode ); // Fraig_DetectFanoutFreeConeMux( pMan, pNode ); + + nMuxes++; } else { @@ -1057,6 +1070,12 @@ void Fraig_SupergateAddClausesMux( Fraig_Man_t * p, Fraig_Node_t * pNode ) // t + e + f' // t' + e' + f + if ( VarT == VarE ) + { +// assert( fCompT == !fCompE ); + return; + } + Msat_IntVecClear( p->vProj ); Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarT, 0^fCompT) ); Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarE, 0^fCompE) ); @@ -1069,6 +1088,7 @@ void Fraig_SupergateAddClausesMux( Fraig_Man_t * p, Fraig_Node_t * pNode ) Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarF, 0) ); RetValue = Msat_SolverAddClause( p->pSat, p->vProj ); assert( RetValue ); + } diff --git a/src/sat/msat/msat.h b/src/sat/msat/msat.h index 37e0bbeb..40028784 100644 --- a/src/sat/msat/msat.h +++ b/src/sat/msat/msat.h @@ -87,6 +87,7 @@ extern void Msat_SolverPrintClauses( Msat_Solver_t * p ); extern void Msat_SolverWriteDimacs( Msat_Solver_t * p, char * pFileName ); // access to the solver internal data extern int Msat_SolverReadVarNum( Msat_Solver_t * p ); +extern int Msat_SolverReadClauseNum( Msat_Solver_t * p ); extern int Msat_SolverReadVarAllocNum( Msat_Solver_t * p ); extern int * Msat_SolverReadAssignsArray( Msat_Solver_t * p ); extern int * Msat_SolverReadModelArray( Msat_Solver_t * p ); diff --git a/src/sat/msat/msatClause.c b/src/sat/msat/msatClause.c index f944ed81..62b9ecad 100644 --- a/src/sat/msat/msatClause.c +++ b/src/sat/msat/msatClause.c @@ -82,6 +82,10 @@ bool Msat_ClauseCreate( Msat_Solver_t * p, Msat_IntVec_t * vLits, bool fLearned, // nSeenId - 1 stands for negative // nSeenId stands for positive // Remove false literals + + // there is a bug here!!!! + // when the same var in opposite polarities is given, it drops one polarity!!! + for ( i = j = 0; i < nLits; i++ ) { // get the corresponding variable Var = MSAT_LIT2VAR(pLits[i]); @@ -190,6 +194,7 @@ bool Msat_ClauseCreate( Msat_Solver_t * p, Msat_IntVec_t * vLits, bool fLearned, { Msat_SolverVarBumpActivity( p, pLits[i] ); // Msat_SolverVarBumpActivity( p, pLits[i] ); + p->pFreq[ MSAT_LIT2VAR(pLits[i]) ]++; } } diff --git a/src/sat/msat/msatInt.h b/src/sat/msat/msatInt.h index ef2375a7..3dfe2109 100644 --- a/src/sat/msat/msatInt.h +++ b/src/sat/msat/msatInt.h @@ -151,6 +151,7 @@ struct Msat_Solver_t_ int nSeenId; // the id of current seeing Msat_IntVec_t * vReason; // the temporary array of literals Msat_IntVec_t * vTemp; // the temporary array of literals + int * pFreq; // the number of times each var participated in conflicts // the memory manager Msat_MmStep_t * pMem; diff --git a/src/sat/msat/msatSolverApi.c b/src/sat/msat/msatSolverApi.c index dd3a5a43..4a721487 100644 --- a/src/sat/msat/msatSolverApi.c +++ b/src/sat/msat/msatSolverApi.c @@ -42,6 +42,7 @@ static void Msat_SolverSetupTruthTables( unsigned uTruths[][2] ); ***********************************************************************/ int Msat_SolverReadVarNum( Msat_Solver_t * p ) { return p->nVars; } +int Msat_SolverReadClauseNum( Msat_Solver_t * p ) { return p->nClauses; } int Msat_SolverReadVarAllocNum( Msat_Solver_t * p ) { return p->nVarsAlloc;} int Msat_SolverReadDecisionLevel( Msat_Solver_t * p ) { return Msat_IntVecReadSize(p->vTrailLim); } int * Msat_SolverReadDecisionLevelArray( Msat_Solver_t * p ) { return p->pLevel; } diff --git a/src/sat/msat/msatSolverCore.c b/src/sat/msat/msatSolverCore.c index ed228b33..5f13694b 100644 --- a/src/sat/msat/msatSolverCore.c +++ b/src/sat/msat/msatSolverCore.c @@ -140,6 +140,9 @@ bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTra int64 nConflictsOld = p->Stats.nConflicts; int64 nDecisionsOld = p->Stats.nDecisions; + p->pFreq = ALLOC( int, p->nVarsAlloc ); + memset( p->pFreq, 0, sizeof(int) * p->nVarsAlloc ); + if ( vAssumps ) { int * pAssumps, nAssumps, i; @@ -181,6 +184,23 @@ bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTra } Msat_SolverCancelUntil( p, 0 ); p->nBackTracks = (int)p->Stats.nConflicts - p->nBackTracks; +/* + PRT( "True solver runtime", clock() - timeStart ); + // print the statistics + { + int i, Counter = 0; + for ( i = 0; i < p->nVars; i++ ) + if ( p->pFreq[i] > 0 ) + { + printf( "%d ", p->pFreq[i] ); + Counter++; + } + if ( Counter ) + printf( "\n" ); + printf( "Total = %d. Used = %d. Decisions = %d. Imps = %d. Conflicts = %d. ", p->nVars, Counter, (int)p->Stats.nDecisions, (int)p->Stats.nPropagations, (int)p->Stats.nConflicts ); + PRT( "Time", clock() - timeStart ); + } +*/ return Status; } -- cgit v1.2.3