80 p->pReasons[
Var] = NULL;
186 return p->pAssigns[
Var] == Lit;
194 p->pAssigns[
Var] = Lit;
197 p->pReasons[
Var] = pC;
228 p->Stats.nPropagations++;
233 for ( i = j = 0; i < nClauses; i++ )
235 p->Stats.nInspects++;
245 pClauses[j++] = pClauses[i];
249 pConflict = pClauses[i];
251 for ( ; i < nClauses; i++ )
252 pClauses[j++] = pClauses[i];
263 pClauses[j++] = pClauses[i];
286 int nClauses, Type, i, j;
300 for ( Type = 0; Type < 2; Type++ )
302 vClauses = Type? p->vLearned : p->vClauses;
305 for ( i = j = 0; i < nClauses; i++ )
310 pClauses[j++] = pClauses[i];
345 for ( i = j = 0; i < nLearned / 2; i++ )
349 pLearned[j++] = pLearned[i];
351 for ( ; i < nLearned; i++ )
356 pLearned[j++] = pLearned[i];
379 for ( i = 0; i < nLearned; i++ )
388 for ( i = 0; i < p->nVarsAlloc; i++ )
389 p->pReasons[i] = NULL;
406 int nLearned, nClauses, i;
411 for ( i = p->nClausesStart; i < nClauses; i++ )
421 for ( i = 0; i < nLearned; i++ )
459 int * pReasonArray, nReasonSize;
475 for ( j = 0; j < nReasonSize; j++ ) {
476 LitQ = pReasonArray[j];
478 if ( p->pSeen[VarQ] != p->nSeenId ) {
479 p->pSeen[VarQ] = p->nSeenId;
485 if ( p->pLevel[VarQ] == nLevelCur )
487 else if ( p->pLevel[VarQ] > 0 ) {
491 if ( *pLevel_out < p->pLevel[VarQ] )
492 *pLevel_out = p->pLevel[VarQ];
501 pC = p->pReasons[
Var];
503 }
while ( p->pSeen[Var] != p->nSeenId );
505 }
while ( pathC > 0 );
515 for ( j = 0; j < nReasonSize; j++ )
517 printf(
" } at level %d\n", *pLevel_out);
539 int nLevelBack, nConfs, nAssigns, Value;
548 for ( i = 0; i < p->nVars; i++ )
549 p->pdActivity[i] = (
double)p->pFactors[i];
556 if ( pConf != NULL ){
565 p->Stats.nConflicts++;
599 memcpy( p->pModel, p->pAssigns,
sizeof(
int) * p->nVars );
604 if ( nConfLimit > 0 && nConfs > nConfLimit ) {
611 else if ( nBackTrackLimit > 0 && (
int)p->Stats.nConflicts - p->nBackTracks > nBackTrackLimit ) {
619 p->Stats.nDecisions++;
int Msat_SolverReadDecisionLevel(Msat_Solver_t *p)
#define MSAT_LIT_UNASSIGNED
void Msat_SolverClaDecayActivity(Msat_Solver_t *p)
void Msat_ClauseFree(Msat_Solver_t *p, Msat_Clause_t *pC, int fRemoveWatched)
void Msat_OrderVarAssigned(Msat_Order_t *p, int Var)
#define MSAT_VAR_UNASSIGNED
#define MSAT_ORDER_UNKNOWN
void Msat_QueueClear(Msat_Queue_t *p)
void Msat_ClauseCalcReason(Msat_Solver_t *p, Msat_Clause_t *pC, Msat_Lit_t Lit, Msat_IntVec_t *vLits_out)
int Msat_ClausePropagate(Msat_Clause_t *pC, Msat_Lit_t Lit, int *pAssigns, Msat_Lit_t *pLit_out)
int Msat_IntVecReadEntryLast(Msat_IntVec_t *p)
void Msat_QueueInsert(Msat_Queue_t *p, int Lit)
Msat_Clause_t * Msat_SolverPropagate(Msat_Solver_t *p)
void Msat_IntVecClear(Msat_IntVec_t *p)
Msat_Type_t Msat_SolverSearch(Msat_Solver_t *p, int nConfLimit, int nLearnedLimit, int nBackTrackLimit, Msat_SearchParams_t *pPars)
int Msat_QueueReadSize(Msat_Queue_t *p)
int Msat_ClauseIsLocked(Msat_Solver_t *p, Msat_Clause_t *pC)
typedefABC_NAMESPACE_HEADER_START struct Msat_Clause_t_ Msat_Clause_t
INCLUDES ///.
int Msat_ClauseVecReadSize(Msat_ClauseVec_t *p)
void Msat_ClauseVecShrink(Msat_ClauseVec_t *p, int nSizeNew)
ABC_NAMESPACE_IMPL_START void Msat_SolverVarBumpActivity(Msat_Solver_t *p, Msat_Lit_t Lit)
DECLARATIONS ///.
int Msat_OrderVarSelect(Msat_Order_t *p)
void Msat_ClauseSetNum(Msat_Clause_t *pC, int Num)
void Msat_SolverVarDecayActivity(Msat_Solver_t *p)
GLOBAL VARIABLES ///.
static ABC_NAMESPACE_IMPL_START void Msat_SolverUndoOne(Msat_Solver_t *p)
DECLARATIONS ///.
int Msat_IntVecReadSize(Msat_IntVec_t *p)
static void Msat_SolverAnalyze(Msat_Solver_t *p, Msat_Clause_t *pC, Msat_IntVec_t *vLits_out, int *pLevel_out)
void Msat_IntVecPush(Msat_IntVec_t *p, int Entry)
int * Msat_SolverReadAssignsArray(Msat_Solver_t *p)
void Msat_SolverSortDB(Msat_Solver_t *p)
FUNCTION DEFINITIONS ///.
void Msat_SolverRemoveLearned(Msat_Solver_t *p)
int Msat_ClauseSimplify(Msat_Clause_t *pC, int *pAssigns)
Msat_Clause_t ** Msat_ClauseVecReadArray(Msat_ClauseVec_t *p)
static void Msat_SolverCancel(Msat_Solver_t *p)
int Msat_IntVecPop(Msat_IntVec_t *p)
void Msat_SolverRemoveMarked(Msat_Solver_t *p)
void Msat_ClauseVecPush(Msat_ClauseVec_t *p, Msat_Clause_t *Entry)
void Msat_SolverCancelUntil(Msat_Solver_t *p, int Level)
#define ABC_NAMESPACE_IMPL_END
int Msat_IntVecReadEntry(Msat_IntVec_t *p, int i)
int Msat_SolverAssume(Msat_Solver_t *p, Msat_Lit_t Lit)
FUNCTION DEFINITIONS ///.
int Msat_SolverSimplifyDB(Msat_Solver_t *p)
#define ABC_NAMESPACE_IMPL_START
static Msat_Clause_t * Msat_SolverRecord(Msat_Solver_t *p, Msat_IntVec_t *vLits)
int * Msat_IntVecReadArray(Msat_IntVec_t *p)
static void Msat_SolverReduceDB(Msat_Solver_t *p)
#define MSAT_VAR2LIT(v, s)
void Msat_IntVecWriteEntry(Msat_IntVec_t *p, int i, int Entry)
void Msat_ClausePrintSymbols(Msat_Clause_t *pC)
void Msat_OrderVarUnassigned(Msat_Order_t *p, int Var)
int Msat_QueueExtract(Msat_Queue_t *p)
double Msat_SolverProgressEstimate(Msat_Solver_t *p)
int Msat_SolverEnqueue(Msat_Solver_t *p, Msat_Lit_t Lit, Msat_Clause_t *pC)
int Msat_ClauseCreate(Msat_Solver_t *p, Msat_IntVec_t *vLits, int fLearned, Msat_Clause_t **pClause_out)
FUNCTION DEFINITIONS ///.
typedefABC_NAMESPACE_HEADER_START struct Msat_Solver_t_ Msat_Solver_t
INCLUDES ///.
float Msat_ClauseReadActivity(Msat_Clause_t *pC)