summaryrefslogtreecommitdiffstats
path: root/src/sat/msat
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat/msat')
-rw-r--r--src/sat/msat/msat.h20
-rw-r--r--src/sat/msat/msatActivity.c6
-rw-r--r--src/sat/msat/msatClause.c7
-rw-r--r--src/sat/msat/msatClauseVec.c2
-rw-r--r--src/sat/msat/msatInt.h10
-rw-r--r--src/sat/msat/msatMem.c4
-rw-r--r--src/sat/msat/msatOrderH.c2
-rw-r--r--src/sat/msat/msatOrderJ.c46
-rw-r--r--src/sat/msat/msatQueue.c2
-rw-r--r--src/sat/msat/msatRead.c2
-rw-r--r--src/sat/msat/msatSolverApi.c50
-rw-r--r--src/sat/msat/msatSolverCore.c33
-rw-r--r--src/sat/msat/msatSolverIo.c2
-rw-r--r--src/sat/msat/msatSolverSearch.c10
-rw-r--r--src/sat/msat/msatSort.c2
-rw-r--r--src/sat/msat/msatVec.c2
16 files changed, 65 insertions, 135 deletions
diff --git a/src/sat/msat/msat.h b/src/sat/msat/msat.h
index 53353ba6..21ddcb81 100644
--- a/src/sat/msat/msat.h
+++ b/src/sat/msat/msat.h
@@ -21,10 +21,6 @@
#ifndef __MSAT_H__
#define __MSAT_H__
-#ifdef __cplusplus
-extern "C" {
-#endif
-
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
@@ -69,7 +65,7 @@ typedef enum { MSAT_FALSE = -1, MSAT_UNKNOWN = 0, MSAT_TRUE = 1 } Msat_Type_t;
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
-/// MACRO DEFINITIONS ///
+/// MACRO DEFITIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
@@ -80,10 +76,10 @@ typedef enum { MSAT_FALSE = -1, MSAT_UNKNOWN = 0, MSAT_TRUE = 1 } Msat_Type_t;
extern bool Msat_SolverParseDimacs( FILE * pFile, Msat_Solver_t ** p, int fVerbose );
/*=== satSolver.c ===========================================================*/
// adding vars, clauses, simplifying the database, and solving
-extern bool Msat_SolverAddVar( Msat_Solver_t * p, int Level );
+extern bool Msat_SolverAddVar( Msat_Solver_t * p );
extern bool Msat_SolverAddClause( Msat_Solver_t * p, Msat_IntVec_t * pLits );
extern bool Msat_SolverSimplifyDB( Msat_Solver_t * p );
-extern bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * pVecAssumps, int nBackTrackLimit, int nTimeLimit );
+extern bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * pVecAssumps, int nBackTrackLimit );
// printing stats, assignments, and clauses
extern void Msat_SolverPrintStats( Msat_Solver_t * p );
extern void Msat_SolverPrintAssignment( Msat_Solver_t * p );
@@ -91,20 +87,17 @@ 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 );
extern unsigned Msat_SolverReadTruth( Msat_Solver_t * p );
extern int Msat_SolverReadBackTracks( Msat_Solver_t * p );
-extern int Msat_SolverReadInspects( Msat_Solver_t * p );
extern void Msat_SolverSetVerbosity( Msat_Solver_t * p, int fVerbose );
extern void Msat_SolverSetProofWriting( Msat_Solver_t * p, int fProof );
extern void Msat_SolverSetVarTypeA( Msat_Solver_t * p, int Var );
extern void Msat_SolverSetVarMap( Msat_Solver_t * p, Msat_IntVec_t * vVarMap );
extern void Msat_SolverMarkLastClauseTypeA( Msat_Solver_t * p );
extern void Msat_SolverMarkClausesStart( Msat_Solver_t * p );
-extern float * Msat_SolverReadFactors( Msat_Solver_t * p );
// returns the solution after incremental solving
extern int Msat_SolverReadSolutions( Msat_Solver_t * p );
extern int * Msat_SolverReadSolutionsArray( Msat_Solver_t * p );
@@ -160,13 +153,8 @@ extern double Msat_VarHeapReadMaxWeight( Msat_VarHeap_t * p );
extern int Msat_VarHeapCountNodes( Msat_VarHeap_t * p, double WeightLimit );
extern int Msat_VarHeapReadMax( Msat_VarHeap_t * p );
extern int Msat_VarHeapGetMax( Msat_VarHeap_t * p );
-
-#ifdef __cplusplus
-}
-#endif
-
-#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
+#endif
diff --git a/src/sat/msat/msatActivity.c b/src/sat/msat/msatActivity.c
index 1cd795bd..c9a518ce 100644
--- a/src/sat/msat/msatActivity.c
+++ b/src/sat/msat/msatActivity.c
@@ -25,7 +25,7 @@
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
+/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
@@ -45,9 +45,7 @@ void Msat_SolverVarBumpActivity( Msat_Solver_t * p, Msat_Lit_t Lit )
if ( p->dVarDecay < 0 ) // (negative decay means static variable order -- don't bump)
return;
Var = MSAT_LIT2VAR(Lit);
- p->pdActivity[Var] += p->dVarInc;
-// p->pdActivity[Var] += p->dVarInc * p->pFactors[Var];
- if ( p->pdActivity[Var] > 1e100 )
+ if ( (p->pdActivity[Var] += p->dVarInc) > 1e100 )
Msat_SolverVarRescaleActivity( p );
Msat_OrderUpdate( p->pOrder, Var );
}
diff --git a/src/sat/msat/msatClause.c b/src/sat/msat/msatClause.c
index 2ba8cd32..dc39bee6 100644
--- a/src/sat/msat/msatClause.c
+++ b/src/sat/msat/msatClause.c
@@ -36,7 +36,7 @@ struct Msat_Clause_t_
};
////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
+/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
@@ -82,10 +82,6 @@ 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]);
@@ -194,7 +190,6 @@ 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/msatClauseVec.c b/src/sat/msat/msatClauseVec.c
index 04691cf2..7c24619f 100644
--- a/src/sat/msat/msatClauseVec.c
+++ b/src/sat/msat/msatClauseVec.c
@@ -25,7 +25,7 @@
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
+/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
diff --git a/src/sat/msat/msatInt.h b/src/sat/msat/msatInt.h
index 03903abe..037616f6 100644
--- a/src/sat/msat/msatInt.h
+++ b/src/sat/msat/msatInt.h
@@ -56,10 +56,10 @@ typedef long long int64;
#define ALLOC(type, num) \
((type *) malloc(sizeof(type) * (num)))
#define REALLOC(type, obj, num) \
- ((obj) ? ((type *) realloc((char *)(obj), sizeof(type) * (num))) : \
- ((type *) malloc(sizeof(type) * (num))))
+ (obj) ? ((type *) realloc((char *) obj, sizeof(type) * (num))) : \
+ ((type *) malloc(sizeof(type) * (num)))
#define FREE(obj) \
- ((obj) ? (free((char *)(obj)), (obj) = 0) : 0)
+ ((obj) ? (free((char *) (obj)), (obj) = 0) : 0)
// By default, custom memory management is used
// which guarantees constant time allocation/deallocation
@@ -119,7 +119,6 @@ struct Msat_Solver_t_
double dClaDecay; // INVERSE decay factor for clause activity: stores 1/decay.
double * pdActivity; // A heuristic measurement of the activity of a variable.
- float * pFactors; // the multiplicative factors of variable activity
double dVarInc; // Amount to bump next variable with.
double dVarDecay; // INVERSE decay factor for variable activity: stores 1/decay. Use negative value for static variable order.
Msat_Order_t * pOrder; // Keeps track of the decision variable order.
@@ -152,7 +151,6 @@ 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;
@@ -186,7 +184,7 @@ struct Msat_IntVec_t_
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
-/// MACRO DEFINITIONS ///
+/// MACRO DEFITIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/msat/msatMem.c b/src/sat/msat/msatMem.c
index 30bf4a96..2d178094 100644
--- a/src/sat/msat/msatMem.c
+++ b/src/sat/msat/msatMem.c
@@ -72,7 +72,7 @@ struct Msat_MmStep_t_
};
////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
+/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
@@ -231,7 +231,7 @@ void Msat_MmFixedRestart( Msat_MmFixed_t * p )
int i;
char * pTemp;
- // deallocate all chunks except the first one
+ // delocate all chunks except the first one
for ( i = 1; i < p->nChunks; i++ )
free( p->pChunks[i] );
p->nChunks = 1;
diff --git a/src/sat/msat/msatOrderH.c b/src/sat/msat/msatOrderH.c
index 956e7fc6..ca034233 100644
--- a/src/sat/msat/msatOrderH.c
+++ b/src/sat/msat/msatOrderH.c
@@ -58,7 +58,7 @@ static void Msat_HeapPercolateDown( Msat_Order_t * p, int i );
extern int timeSelect;
////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
+/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
diff --git a/src/sat/msat/msatOrderJ.c b/src/sat/msat/msatOrderJ.c
index 4db7ff7b..6067b40f 100644
--- a/src/sat/msat/msatOrderJ.c
+++ b/src/sat/msat/msatOrderJ.c
@@ -38,7 +38,7 @@ struct Msat_OrderVar_t_
{
Msat_OrderVar_t * pNext;
Msat_OrderVar_t * pPrev;
- int Num;
+ int Num;
};
// the ring of variables data structure (J-boundary)
@@ -82,7 +82,7 @@ extern int timeSelect;
extern int timeAssign;
////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
+/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
@@ -170,8 +170,7 @@ int Msat_OrderCheck( Msat_Order_t * p )
Msat_OrderVar_t * pVar, * pNext;
Msat_IntVec_t * vRound;
int * pRound, nRound;
- int * pVars, nVars, i, k;
- int Counter = 0;
+ int * pVars, nVars, i;
// go through all the variables in the boundary
Msat_OrderRingForEachEntry( p->rVars.pRoot, pVar, pNext )
@@ -189,14 +188,10 @@ int Msat_OrderCheck( Msat_Order_t * p )
if ( Msat_OrderVarIsAssigned(p, pRound[i]) )
break;
}
-// assert( i != nRound );
-// if ( i == nRound )
-// return 0;
- if ( i == nRound )
- Counter++;
+ assert( i != nRound );
+ if ( i != nRound )
+ return 0;
}
- if ( Counter > 0 )
- printf( "%d(%d) ", Counter, p->rVars.nItems );
// we may also check other unassigned variables in the cone
// to make sure that if they are not in J-boundary,
@@ -214,16 +209,16 @@ int Msat_OrderCheck( Msat_Order_t * p )
vRound = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( p->pSat->vAdjacents, pVars[i] );
nRound = Msat_IntVecReadSize( vRound );
pRound = Msat_IntVecReadArray( vRound );
- for ( k = 0; k < nRound; k++ )
+ for ( i = 0; i < nRound; i++ )
{
- if ( !Msat_OrderVarIsUsedInCone(p, pRound[k]) )
+ if ( !Msat_OrderVarIsUsedInCone(p, pRound[i]) )
continue;
- if ( Msat_OrderVarIsAssigned(p, pRound[k]) )
+ if ( Msat_OrderVarIsAssigned(p, pRound[i]) )
break;
}
-// assert( k == nRound );
-// if ( k != nRound )
-// return 0;
+ assert( i == nRound );
+ if ( i == nRound )
+ return 0;
}
return 1;
}
@@ -261,7 +256,7 @@ int Msat_OrderVarSelect( Msat_Order_t * p )
Msat_OrderVar_t * pVar, * pNext, * pVarBest;
double * pdActs = p->pSat->pdActivity;
double dfActBest;
-// int clk = clock();
+ int clk = clock();
pVarBest = NULL;
dfActBest = -1.0;
@@ -273,13 +268,12 @@ int Msat_OrderVarSelect( Msat_Order_t * p )
pVarBest = pVar;
}
}
-//timeSelect += clock() - clk;
-//timeAssign += clock() - clk;
+timeSelect += clock() - clk;
+timeAssign += clock() - clk;
//if ( pVarBest && pVarBest->Num % 1000 == 0 )
//printf( "%d ", p->rVars.nItems );
-// Msat_OrderCheck( p );
if ( pVarBest )
{
assert( Msat_OrderVarIsUsedInCone(p, pVarBest->Num) );
@@ -302,7 +296,7 @@ int Msat_OrderVarSelect( Msat_Order_t * p )
void Msat_OrderVarAssigned( Msat_Order_t * p, int Var )
{
Msat_IntVec_t * vRound;
- int i;//, clk = clock();
+ int i, clk = clock();
// make sure the variable is in the boundary
assert( Var < p->nVarsAlloc );
@@ -322,7 +316,7 @@ void Msat_OrderVarAssigned( Msat_Order_t * p, int Var )
continue;
Msat_OrderRingAddLast( &p->rVars, &p->pVars[vRound->pArray[i]] );
}
-//timeSelect += clock() - clk;
+timeSelect += clock() - clk;
// Msat_OrderCheck( p );
}
@@ -340,7 +334,7 @@ void Msat_OrderVarAssigned( Msat_Order_t * p, int Var )
void Msat_OrderVarUnassigned( Msat_Order_t * p, int Var )
{
Msat_IntVec_t * vRound, * vRound2;
- int i, k;//, clk = clock();
+ int i, k, clk = clock();
// make sure the variable is not in the boundary
assert( Var < p->nVarsAlloc );
@@ -369,7 +363,7 @@ void Msat_OrderVarUnassigned( Msat_Order_t * p, int Var )
if ( k == vRound2->nSize ) // there is no assigned vars, delete this one
Msat_OrderRingRemove( &p->rVars, &p->pVars[vRound->pArray[i]] );
}
-//timeSelect += clock() - clk;
+timeSelect += clock() - clk;
// Msat_OrderCheck( p );
}
@@ -456,7 +450,7 @@ void Msat_OrderRingRemove( Msat_OrderRing_t * pRing, Msat_OrderVar_t * pVar )
pRing->pRoot = pVar->pNext;
// move the root to the next entry after pVar
// this way all the additions to the list will be traversed first
-// pRing->pRoot = pVar->pPrev;
+// pRing->pRoot = pVar->pNext;
// delete the node
pVar->pPrev->pNext = pVar->pNext;
pVar->pNext->pPrev = pVar->pPrev;
diff --git a/src/sat/msat/msatQueue.c b/src/sat/msat/msatQueue.c
index 5938e042..c12cc75d 100644
--- a/src/sat/msat/msatQueue.c
+++ b/src/sat/msat/msatQueue.c
@@ -33,7 +33,7 @@ struct Msat_Queue_t_
};
////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
+/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
diff --git a/src/sat/msat/msatRead.c b/src/sat/msat/msatRead.c
index 738562ef..b8e585a4 100644
--- a/src/sat/msat/msatRead.c
+++ b/src/sat/msat/msatRead.c
@@ -27,7 +27,7 @@
static char * Msat_FileRead( FILE * pFile );
////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
+/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
diff --git a/src/sat/msat/msatSolverApi.c b/src/sat/msat/msatSolverApi.c
index ee3507a6..ba506993 100644
--- a/src/sat/msat/msatSolverApi.c
+++ b/src/sat/msat/msatSolverApi.c
@@ -27,7 +27,7 @@
static void Msat_SolverSetupTruthTables( unsigned uTruths[][2] );
////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
+/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
@@ -41,30 +41,27 @@ static void Msat_SolverSetupTruthTables( unsigned uTruths[][2] );
SeeAlso []
***********************************************************************/
-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_SolverReadVarNum( Msat_Solver_t * p ) { return p->nVars; }
+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; }
-Msat_Clause_t ** Msat_SolverReadReasonArray( Msat_Solver_t * p ) { return p->pReasons; }
+int * Msat_SolverReadDecisionLevelArray( Msat_Solver_t * p ) { return p->pLevel; }
+Msat_Clause_t ** Msat_SolverReadReasonArray( Msat_Solver_t * p ) { return p->pReasons; }
Msat_Lit_t Msat_SolverReadVarValue( Msat_Solver_t * p, Msat_Var_t Var ) { return p->pAssigns[Var]; }
-Msat_ClauseVec_t * Msat_SolverReadLearned( Msat_Solver_t * p ) { return p->vLearned; }
-Msat_ClauseVec_t ** Msat_SolverReadWatchedArray( Msat_Solver_t * p ) { return p->pvWatched; }
-int * Msat_SolverReadAssignsArray( Msat_Solver_t * p ) { return p->pAssigns; }
-int * Msat_SolverReadModelArray( Msat_Solver_t * p ) { return p->pModel; }
-int Msat_SolverReadBackTracks( Msat_Solver_t * p ) { return (int)p->Stats.nConflicts; }
-int Msat_SolverReadInspects( Msat_Solver_t * p ) { return (int)p->Stats.nInspects; }
-Msat_MmStep_t * Msat_SolverReadMem( Msat_Solver_t * p ) { return p->pMem; }
-int * Msat_SolverReadSeenArray( Msat_Solver_t * p ) { return p->pSeen; }
-int Msat_SolverIncrementSeenId( Msat_Solver_t * p ) { return ++p->nSeenId; }
+Msat_ClauseVec_t * Msat_SolverReadLearned( Msat_Solver_t * p ) { return p->vLearned; }
+Msat_ClauseVec_t ** Msat_SolverReadWatchedArray( Msat_Solver_t * p ) { return p->pvWatched; }
+int * Msat_SolverReadAssignsArray( Msat_Solver_t * p ) { return p->pAssigns; }
+int * Msat_SolverReadModelArray( Msat_Solver_t * p ) { return p->pModel; }
+int Msat_SolverReadBackTracks( Msat_Solver_t * p ) { return p->nBackTracks; }
+Msat_MmStep_t * Msat_SolverReadMem( Msat_Solver_t * p ) { return p->pMem; }
+int * Msat_SolverReadSeenArray( Msat_Solver_t * p ) { return p->pSeen; }
+int Msat_SolverIncrementSeenId( Msat_Solver_t * p ) { return ++p->nSeenId; }
void Msat_SolverSetVerbosity( Msat_Solver_t * p, int fVerbose ) { p->fVerbose = fVerbose; }
-void Msat_SolverClausesIncrement( Msat_Solver_t * p ) { p->nClausesAlloc++; }
-void Msat_SolverClausesDecrement( Msat_Solver_t * p ) { p->nClausesAlloc--; }
-void Msat_SolverClausesIncrementL( Msat_Solver_t * p ) { p->nClausesAllocL++; }
-void Msat_SolverClausesDecrementL( Msat_Solver_t * p ) { p->nClausesAllocL--; }
+void Msat_SolverClausesIncrement( Msat_Solver_t * p ) { p->nClausesAlloc++; }
+void Msat_SolverClausesDecrement( Msat_Solver_t * p ) { p->nClausesAlloc--; }
+void Msat_SolverClausesIncrementL( Msat_Solver_t * p ) { p->nClausesAllocL++; }
+void Msat_SolverClausesDecrementL( Msat_Solver_t * p ) { p->nClausesAllocL--; }
void Msat_SolverMarkLastClauseTypeA( Msat_Solver_t * p ) { Msat_ClauseSetTypeA( Msat_ClauseVecReadEntry( p->vClauses, Msat_ClauseVecReadSize(p->vClauses)-1 ), 1 ); }
void Msat_SolverMarkClausesStart( Msat_Solver_t * p ) { p->nClausesStart = Msat_ClauseVecReadSize(p->vClauses); }
-float * Msat_SolverReadFactors( Msat_Solver_t * p ) { return p->pFactors; }
/**Function*************************************************************
@@ -175,12 +172,8 @@ Msat_Solver_t * Msat_SolverAlloc( int nVarsAlloc,
p->dVarDecay = dVarDecay;
p->pdActivity = ALLOC( double, p->nVarsAlloc );
- p->pFactors = ALLOC( float, p->nVarsAlloc );
for ( i = 0; i < p->nVarsAlloc; i++ )
- {
- p->pdActivity[i] = 0.0;
- p->pFactors[i] = 1.0;
- }
+ p->pdActivity[i] = 0;
p->pAssigns = ALLOC( int, p->nVarsAlloc );
p->pModel = ALLOC( int, p->nVarsAlloc );
@@ -244,12 +237,8 @@ void Msat_SolverResize( Msat_Solver_t * p, int nVarsAlloc )
p->nVarsAlloc = nVarsAlloc;
p->pdActivity = REALLOC( double, p->pdActivity, p->nVarsAlloc );
- p->pFactors = REALLOC( float, p->pFactors, p->nVarsAlloc );
for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ )
- {
- p->pdActivity[i] = 0.0;
- p->pFactors[i] = 1.0;
- }
+ p->pdActivity[i] = 0;
p->pAssigns = REALLOC( int, p->pAssigns, p->nVarsAlloc );
p->pModel = REALLOC( int, p->pModel, p->nVarsAlloc );
@@ -403,7 +392,6 @@ void Msat_SolverFree( Msat_Solver_t * p )
Msat_ClauseVecFree( p->vLearned );
FREE( p->pdActivity );
- FREE( p->pFactors );
Msat_OrderFree( p->pOrder );
for ( i = 0; i < 2 * p->nVarsAlloc; i++ )
diff --git a/src/sat/msat/msatSolverCore.c b/src/sat/msat/msatSolverCore.c
index f9fee73c..b8d9f328 100644
--- a/src/sat/msat/msatSolverCore.c
+++ b/src/sat/msat/msatSolverCore.c
@@ -25,7 +25,7 @@
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
+/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
@@ -39,11 +39,10 @@
SeeAlso []
***********************************************************************/
-bool Msat_SolverAddVar( Msat_Solver_t * p, int Level )
+bool Msat_SolverAddVar( Msat_Solver_t * p )
{
if ( p->nVars == p->nVarsAlloc )
Msat_SolverResize( p, 2 * p->nVarsAlloc );
- p->pLevel[p->nVars] = Level;
p->nVars++;
return 1;
}
@@ -132,18 +131,14 @@ void Msat_SolverPrintStats( Msat_Solver_t * p )
SeeAlso []
***********************************************************************/
-bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTrackLimit, int nTimeLimit )
+bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTrackLimit )
{
Msat_SearchParams_t Params = { 0.95, 0.999 };
double nConflictsLimit, nLearnedLimit;
Msat_Type_t Status;
- int timeStart = clock();
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;
@@ -177,31 +172,11 @@ bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTra
nConflictsLimit *= 1.5;
nLearnedLimit *= 1.1;
// if the limit on the number of backtracks is given, quit the restart loop
- if ( nBackTrackLimit > 0 && (int)p->Stats.nConflicts - p->nBackTracks > nBackTrackLimit )
- break;
- // if the runtime limit is exceeded, quit the restart loop
- if ( nTimeLimit > 0 && clock() - timeStart >= nTimeLimit * CLOCKS_PER_SEC )
+ if ( nBackTrackLimit > 0 )
break;
}
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;
}
diff --git a/src/sat/msat/msatSolverIo.c b/src/sat/msat/msatSolverIo.c
index 05b7f6a9..f17595a7 100644
--- a/src/sat/msat/msatSolverIo.c
+++ b/src/sat/msat/msatSolverIo.c
@@ -27,7 +27,7 @@
static char * Msat_TimeStamp();
////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
+/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
diff --git a/src/sat/msat/msatSolverSearch.c b/src/sat/msat/msatSolverSearch.c
index 11a6540c..13a0c403 100644
--- a/src/sat/msat/msatSolverSearch.c
+++ b/src/sat/msat/msatSolverSearch.c
@@ -31,7 +31,7 @@ static void Msat_SolverAnalyze( Msat_Solver_t * p, Msat_Clause_t * pC
static void Msat_SolverReduceDB( Msat_Solver_t * p );
////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
+/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
@@ -534,18 +534,12 @@ Msat_Type_t Msat_SolverSearch( Msat_Solver_t * p, int nConfLimit, int nLearnedLi
Msat_Clause_t * pConf;
Msat_Var_t Var;
int nLevelBack, nConfs, nAssigns, Value;
- int i;
assert( Msat_SolverReadDecisionLevel(p) == p->nLevelRoot );
p->Stats.nStarts++;
p->dVarDecay = 1 / pPars->dVarDecay;
p->dClaDecay = 1 / pPars->dClaDecay;
- // reset the activities
- for ( i = 0; i < p->nVars; i++ )
- p->pdActivity[i] = (double)p->pFactors[i];
-// p->pdActivity[i] = 0.0;
-
nConfs = 0;
while ( 1 )
{
@@ -605,7 +599,7 @@ Msat_Type_t Msat_SolverSearch( Msat_Solver_t * p, int nConfLimit, int nLearnedLi
Msat_SolverCancelUntil( p, p->nLevelRoot );
return MSAT_UNKNOWN;
}
- else if ( nBackTrackLimit > 0 && (int)p->Stats.nConflicts - p->nBackTracks > nBackTrackLimit ) {
+ else if ( nBackTrackLimit > 0 && nConfs > nBackTrackLimit ) {
// Reached bound on number of conflicts:
Msat_QueueClear( p->pQueue );
Msat_SolverCancelUntil( p, p->nLevelRoot );
diff --git a/src/sat/msat/msatSort.c b/src/sat/msat/msatSort.c
index 3b89d102..2198d303 100644
--- a/src/sat/msat/msatSort.c
+++ b/src/sat/msat/msatSort.c
@@ -41,7 +41,7 @@ static int irand(double seed, int size) {
static void Msat_SolverSort( Msat_Clause_t ** array, int size, double seed );
////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
+/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
diff --git a/src/sat/msat/msatVec.c b/src/sat/msat/msatVec.c
index 75f53047..951969cf 100644
--- a/src/sat/msat/msatVec.c
+++ b/src/sat/msat/msatVec.c
@@ -28,7 +28,7 @@ static int Msat_IntVecSortCompare1( int * pp1, int * pp2 );
static int Msat_IntVecSortCompare2( int * pp1, int * pp2 );
////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
+/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-05 00:45:41 +0000