Version abc51225

5 files changed, 28 insertions, 0 deletions

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;
 }