21 #ifndef ABC__sat__msat__msatInt_h
22 #define ABC__sat__msat__msatInt_h
68 #define MSAT_VAR_UNASSIGNED (-1)
69 #define MSAT_LIT_UNASSIGNED (-2)
70 #define MSAT_ORDER_UNKNOWN (-3)
74 #define L_ind Msat_SolverReadDecisionLevel(p)*3+3,Msat_SolverReadDecisionLevel(p)
76 #define L_lit(Lit) MSAT_LITSIGN(Lit)?"-":"", MSAT_LIT2VAR(Lit)+1
void Msat_SolverClausesDecrement(Msat_Solver_t *p)
int * Msat_ClauseReadLits(Msat_Clause_t *pC)
int Msat_SolverReadDecisionLevel(Msat_Solver_t *p)
void Msat_ClauseSetMark(Msat_Clause_t *pC, int fMark)
void Msat_ClauseWriteDimacs(FILE *pFile, Msat_Clause_t *pC, int fIncrement)
void Msat_OrderVarAssigned(Msat_Order_t *p, int Var)
int Msat_MmFixedReadMemUsage(Msat_MmFixed_t *p)
Msat_Clause_t * Msat_ClauseVecPop(Msat_ClauseVec_t *p)
void Msat_MmStepEntryRecycle(Msat_MmStep_t *p, char *pEntry, int nBytes)
void Msat_QueueFree(Msat_Queue_t *p)
int Msat_OrderCheck(Msat_Order_t *p)
int * Msat_SolverReadSeenArray(Msat_Solver_t *p)
char * Msat_MmFlexEntryFetch(Msat_MmFlex_t *p, int nBytes)
void Msat_QueueClear(Msat_Queue_t *p)
void Msat_ClauseVecGrow(Msat_ClauseVec_t *p, int nCapMin)
Msat_ClauseVec_t * vAdjacents
Msat_Clause_t * Msat_ClauseVecReadEntry(Msat_ClauseVec_t *p, int i)
char * Msat_MmStepEntryFetch(Msat_MmStep_t *p, int nBytes)
Msat_Clause_t * Msat_ClauseCreateFake(Msat_Solver_t *p, Msat_IntVec_t *vLits)
void Msat_ClauseVecFree(Msat_ClauseVec_t *p)
void Msat_QueueInsert(Msat_Queue_t *p, int Lit)
void Msat_OrderSetBounds(Msat_Order_t *p, int nVarsMax)
Msat_ClauseVec_t * Msat_SolverReadLearned(Msat_Solver_t *p)
Msat_Clause_t ** Msat_ClauseVecReadArray(Msat_ClauseVec_t *p)
void Msat_MmFixedRestart(Msat_MmFixed_t *p)
Msat_Clause_t * Msat_ClauseCreateFakeLit(Msat_Solver_t *p, Msat_Lit_t Lit)
int Msat_ClauseCreate(Msat_Solver_t *p, Msat_IntVec_t *vLits, int fLearnt, Msat_Clause_t **pClause_out)
FUNCTION DEFINITIONS ///.
Msat_Type_t Msat_SolverSearch(Msat_Solver_t *p, int nConfLimit, int nLearnedLimit, int nBackTrackLimit, Msat_SearchParams_t *pPars)
int Msat_SolverIncrementSeenId(Msat_Solver_t *p)
int Msat_ClauseReadTypeA(Msat_Clause_t *pC)
void Msat_ClausePrint(Msat_Clause_t *pC)
int Msat_QueueReadSize(Msat_Queue_t *p)
void Msat_SolverClaDecayActivity(Msat_Solver_t *p)
void Msat_MmFlexStop(Msat_MmFlex_t *p, int fVerbose)
void Msat_MmFixedEntryRecycle(Msat_MmFixed_t *p, char *pEntry)
typedefABC_NAMESPACE_HEADER_START struct Msat_Clause_t_ Msat_Clause_t
INCLUDES ///.
int Msat_SolverEnqueue(Msat_Solver_t *p, Msat_Lit_t Lit, Msat_Clause_t *pC)
void Msat_ClauseRemoveWatch(Msat_ClauseVec_t *vClauses, Msat_Clause_t *pC)
void Msat_SolverVarRescaleActivity(Msat_Solver_t *p)
float Msat_ClauseReadActivity(Msat_Clause_t *pC)
Msat_ClauseVec_t ** pvWatched
unsigned Msat_ClauseComputeTruth(Msat_Solver_t *p, Msat_Clause_t *pC)
int Msat_ClauseSimplify(Msat_Clause_t *pC, int *pAssigns)
int Msat_ClauseReadNum(Msat_Clause_t *pC)
int Msat_OrderVarSelect(Msat_Order_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)
Msat_Clause_t * Msat_SolverReadClause(Msat_Solver_t *p, int Num)
Msat_ClauseVec_t * vClauses
int Msat_MmStepReadMemUsage(Msat_MmStep_t *p)
Msat_ClauseVec_t * Msat_ClauseVecAlloc(int nCap)
DECLARATIONS ///.
void Msat_SolverSortDB(Msat_Solver_t *p)
FUNCTION DEFINITIONS ///.
void Msat_ClauseVecWriteEntry(Msat_ClauseVec_t *p, int i, Msat_Clause_t *Entry)
void Msat_SolverVarBumpActivity(Msat_Solver_t *p, Msat_Lit_t Lit)
DECLARATIONS ///.
void Msat_ClauseVecClear(Msat_ClauseVec_t *p)
int Msat_ClauseReadMark(Msat_Clause_t *pC)
void Msat_SolverCancelUntil(Msat_Solver_t *p, int Level)
void Msat_ClauseVecPush(Msat_ClauseVec_t *p, Msat_Clause_t *Entry)
void Msat_OrderFree(Msat_Order_t *p)
void Msat_ClauseSetTypeA(Msat_Clause_t *pC, int fTypeA)
void Msat_SolverVarDecayActivity(Msat_Solver_t *p)
GLOBAL VARIABLES ///.
void Msat_SolverClaBumpActivity(Msat_Solver_t *p, Msat_Clause_t *pC)
Msat_IntVec_t * vTrailLim
void Msat_ClauseFree(Msat_Solver_t *p, Msat_Clause_t *pC, int fRemoveWatched)
#define ABC_NAMESPACE_HEADER_START
NAMESPACES ///.
void Msat_SolverClausesIncrement(Msat_Solver_t *p)
Msat_MmStep_t * Msat_SolverReadMem(Msat_Solver_t *p)
ABC_INT64_T nPropagations
#define ABC_NAMESPACE_HEADER_END
int Msat_ClauseIsLocked(Msat_Solver_t *p, Msat_Clause_t *pC)
Msat_MmFlex_t * Msat_MmFlexStart()
Msat_Order_t * Msat_OrderAlloc(Msat_Solver_t *pSat)
FUNCTION DEFINITIONS ///.
void Msat_SolverClaRescaleActivity(Msat_Solver_t *p)
int Msat_MmFlexReadMemUsage(Msat_MmFlex_t *p)
void Msat_SolverClausesIncrementL(Msat_Solver_t *p)
Msat_Clause_t ** pReasons
void Msat_ClausePrintSymbols(Msat_Clause_t *pC)
Msat_ClauseVec_t ** Msat_SolverReadWatchedArray(Msat_Solver_t *p)
Msat_Clause_t ** Msat_SolverReadReasonArray(Msat_Solver_t *p)
Msat_IntVec_t * vVarsUsed
Msat_Type_t Msat_SolverReadVarValue(Msat_Solver_t *p, Msat_Var_t Var)
Msat_ClauseVec_t * vLearned
Msat_IntVec_t * vConeVars
void Msat_MmFixedStop(Msat_MmFixed_t *p, int fVerbose)
Msat_Clause_t * Msat_SolverPropagate(Msat_Solver_t *p)
int Msat_SolverAssume(Msat_Solver_t *p, Msat_Lit_t Lit)
FUNCTION DEFINITIONS ///.
void Msat_OrderClean(Msat_Order_t *p, Msat_IntVec_t *vCone)
void Msat_OrderUpdate(Msat_Order_t *p, int Var)
int Msat_ClauseReadSize(Msat_Clause_t *pC)
Msat_MmFixed_t * Msat_MmFixedStart(int nEntrySize)
FUNCTION DEFINITIONS ///.
Msat_Queue_t * Msat_QueueAlloc(int nVars)
FUNCTION DEFINITIONS ///.
char * Msat_MmFixedEntryFetch(Msat_MmFixed_t *p)
int * Msat_SolverReadDecisionLevelArray(Msat_Solver_t *p)
void Msat_OrderVarUnassigned(Msat_Order_t *p, int Var)
Msat_MmStep_t * Msat_MmStepStart(int nSteps)
int Msat_QueueExtract(Msat_Queue_t *p)
double Msat_SolverProgressEstimate(Msat_Solver_t *p)
void Msat_MmStepStop(Msat_MmStep_t *p, int fVerbose)
int Msat_ClauseReadLearned(Msat_Clause_t *pC)
void Msat_ClauseVecShrink(Msat_ClauseVec_t *p, int nSizeNew)
int Msat_ClauseVecReadSize(Msat_ClauseVec_t *p)
void Msat_ClauseSetNum(Msat_Clause_t *pC, int Num)
void Msat_ClauseWriteActivity(Msat_Clause_t *pC, float Num)
typedefABC_NAMESPACE_HEADER_START struct Msat_Solver_t_ Msat_Solver_t
INCLUDES ///.
void Msat_SolverClausesDecrementL(Msat_Solver_t *p)