Home
last modified time | relevance | path

Searched refs:pAssigns (Results 1 – 13 of 13) sorted by relevance

/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/msat/
H A DmsatClause.c60 int * pAssigns = Msat_SolverReadAssignsArray(p); in Msat_ClauseCreate() local
107 if ( pAssigns[Var] != MSAT_VAR_UNASSIGNED ) in Msat_ClauseCreate()
109 if ( pAssigns[Var] == pLits[i] ) in Msat_ClauseCreate()
335 int Msat_ClausePropagate( Msat_Clause_t * pC, Msat_Lit_t Lit, int * pAssigns, Msat_Lit_t * pLit_ou… in Msat_ClausePropagate() argument
343 if ( pAssigns[MSAT_LIT2VAR(pC->pData[0])] == pC->pData[0] ) in Msat_ClausePropagate()
350 if ( pAssigns[MSAT_LIT2VAR(pC->pData[i])] != MSAT_LITNOT(pC->pData[i]) ) in Msat_ClausePropagate()
374 int Msat_ClauseSimplify( Msat_Clause_t * pC, int * pAssigns ) in Msat_ClauseSimplify() argument
381 if ( pAssigns[Var] == MSAT_VAR_UNASSIGNED ) in Msat_ClauseSimplify()
386 if ( pAssigns[Var] == pC->pData[i] ) in Msat_ClauseSimplify()
H A DmsatSolverIo.c55 if ( p->pAssigns[i] == MSAT_VAR_UNASSIGNED ) in Msat_SolverPrintAssignment()
59 assert( i == MSAT_LIT2VAR(p->pAssigns[i]) ); in Msat_SolverPrintAssignment()
60 if ( MSAT_LITSIGN(p->pAssigns[i]) ) in Msat_SolverPrintAssignment()
145 fprintf( pFile, "%s%d 0\n", ((p->pAssigns[i]&1)? "-": ""), i + 1 ); in Msat_SolverWriteDimacs()
H A DmsatSolverApi.c53 …t_SolverReadVarValue( Msat_Solver_t * p, Msat_Var_t Var ) { return (Msat_Type_t)p->pAssigns[Var]; } in Msat_SolverReadVarValue()
56 int * Msat_SolverReadAssignsArray( Msat_Solver_t * p ) { return p->pAssigns… in Msat_SolverReadAssignsArray()
188 p->pAssigns = ABC_ALLOC( int, p->nVarsAlloc ); in Msat_SolverAlloc()
191 p->pAssigns[i] = MSAT_VAR_UNASSIGNED; in Msat_SolverAlloc()
257 p->pAssigns = ABC_REALLOC( int, p->pAssigns, p->nVarsAlloc ); in Msat_SolverResize()
260 p->pAssigns[i] = MSAT_VAR_UNASSIGNED; in Msat_SolverResize()
349 p->pAssigns[i] = MSAT_VAR_UNASSIGNED; in Msat_SolverClean()
417 ABC_FREE( p->pAssigns ); in Msat_SolverFree()
458 p->pAssigns[i] = MSAT_VAR_UNASSIGNED; in Msat_SolverPrepare()
H A DmsatSolverSearch.c79 p->pAssigns[Var] = MSAT_VAR_UNASSIGNED; in Msat_SolverUndoOne()
185 if ( p->pAssigns[Var] != MSAT_VAR_UNASSIGNED ) in Msat_SolverEnqueue()
186 return p->pAssigns[Var] == Lit; in Msat_SolverEnqueue()
194 p->pAssigns[Var] = Lit; in Msat_SolverEnqueue()
239 if ( !Msat_ClausePropagate( pClauses[i], Lit, p->pAssigns, &Lit_out ) ) in Msat_SolverPropagate()
287 int * pAssigns; in Msat_SolverSimplifyDB() local
299 pAssigns = Msat_SolverReadAssignsArray( p ); in Msat_SolverSimplifyDB()
306 if ( Msat_ClauseSimplify( pClauses[i], pAssigns ) ) in Msat_SolverSimplifyDB()
599 memcpy( p->pModel, p->pAssigns, sizeof(int) * p->nVars ); in Msat_SolverSearch()
H A DmsatInt.h117 int * pAssigns; // The current assignments (literals or MSAT_VAR_UNKOWN) member
245 extern int Msat_ClausePropagate( Msat_Clause_t * pC, Msat_Lit_t Lit, int * pAssigns…
246 extern int Msat_ClauseSimplify( Msat_Clause_t * pC, int * pAssigns );
H A DmsatSolverCore.c94 if ( p->pAssigns[i] != MSAT_VAR_UNASSIGNED ) in Msat_SolverProgressEstimate()
H A DmsatOrderH.c199 if ( (p)->pSat->pAssigns[Var] == MSAT_VAR_UNASSIGNED ) in Msat_OrderVarSelect()
H A DmsatOrderJ.c70 #define Msat_OrderVarIsAssigned( p, i ) ((p)->pSat->pAssigns[i] != MSAT_VAR_UNASSIGNED)
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/bsat/
H A DsatInterP.c54 lit * pAssigns; // assignments by variable (size nVars) member
139 p->pAssigns = ABC_REALLOC(lit, p->pAssigns, p->nVarsAlloc ); in Intp_ManResize()
147 memset( p->pAssigns , 0xff, sizeof(lit) * p->pCnf->nVars ); in Intp_ManResize()
192 ABC_FREE( p->pAssigns ); in Intp_ManFree()
303 if ( p->pAssigns[Var] != LIT_UNDEF ) in Intp_ManEnqueue()
304 return p->pAssigns[Var] == Lit; in Intp_ManEnqueue()
305 p->pAssigns[Var] = Lit; in Intp_ManEnqueue()
332 p->pAssigns[Var] = LIT_UNDEF; in Intp_ManCancelUntil()
370 if ( pCur->pLits[0] == p->pAssigns[lit_var(pCur->pLits[0])] ) in Intp_ManPropagateOne()
380 if ( lit_neg(pCur->pLits[i]) == p->pAssigns[lit_var(pCur->pLits[i])] ) in Intp_ManPropagateOne()
[all …]
H A DsatInter.c55 lit * pAssigns; // assignments by variable (size nVars) member
221 p->pAssigns = ABC_REALLOC(lit, p->pAssigns, p->nVarsAlloc ); in Int_ManResize()
229 memset( p->pAssigns , 0xff, sizeof(lit) * p->pCnf->nVars ); in Int_ManResize()
284 ABC_FREE( p->pAssigns ); in Int_ManFree()
419 if ( p->pAssigns[Var] != LIT_UNDEF ) in Int_ManEnqueue()
420 return p->pAssigns[Var] == Lit; in Int_ManEnqueue()
421 p->pAssigns[Var] = Lit; in Int_ManEnqueue()
448 p->pAssigns[Var] = LIT_UNDEF; in Int_ManCancelUntil()
486 if ( pCur->pLits[0] == p->pAssigns[lit_var(pCur->pLits[0])] ) in Int_ManPropagateOne()
496 if ( lit_neg(pCur->pLits[i]) == p->pAssigns[lit_var(pCur->pLits[i])] ) in Int_ManPropagateOne()
[all …]
H A DsatInterA.c55 lit * pAssigns; // assignments by variable (size nVars) member
200 p->pAssigns = ABC_REALLOC(lit, p->pAssigns, p->nVarsAlloc ); in Inta_ManResize()
208 memset( p->pAssigns , 0xff, sizeof(lit) * p->pCnf->nVars ); in Inta_ManResize()
261 ABC_FREE( p->pAssigns ); in Inta_ManFree()
372 if ( p->pAssigns[Var] != LIT_UNDEF ) in Inta_ManEnqueue()
373 return p->pAssigns[Var] == Lit; in Inta_ManEnqueue()
374 p->pAssigns[Var] = Lit; in Inta_ManEnqueue()
401 p->pAssigns[Var] = LIT_UNDEF; in Inta_ManCancelUntil()
439 if ( pCur->pLits[0] == p->pAssigns[lit_var(pCur->pLits[0])] ) in Inta_ManPropagateOne()
449 if ( lit_neg(pCur->pLits[i]) == p->pAssigns[lit_var(pCur->pLits[i])] ) in Inta_ManPropagateOne()
[all …]
H A DsatInterB.c55 lit * pAssigns; // assignments by variable (size nVars) member
205 p->pAssigns = ABC_REALLOC(lit, p->pAssigns, p->nVarsAlloc ); in Intb_ManResize()
213 memset( p->pAssigns , 0xff, sizeof(lit) * p->pCnf->nVars ); in Intb_ManResize()
266 ABC_FREE( p->pAssigns ); in Intb_ManFree()
377 if ( p->pAssigns[Var] != LIT_UNDEF ) in Intb_ManEnqueue()
378 return p->pAssigns[Var] == Lit; in Intb_ManEnqueue()
379 p->pAssigns[Var] = Lit; in Intb_ManEnqueue()
406 p->pAssigns[Var] = LIT_UNDEF; in Intb_ManCancelUntil()
444 if ( pCur->pLits[0] == p->pAssigns[lit_var(pCur->pLits[0])] ) in Intb_ManPropagateOne()
454 if ( lit_neg(pCur->pLits[i]) == p->pAssigns[lit_var(pCur->pLits[i])] ) in Intb_ManPropagateOne()
[all …]
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/proof/
H A Dpr.c73 lit * pAssigns; // assignments by variable (size nVars) member
186 p->pAssigns = ABC_REALLOC(lit, p->pAssigns, p->nVarsAlloc ); in Pr_ManResize()
192 memset( p->pAssigns + nVarsAllocOld, 0xff, sizeof(lit) * (p->nVarsAlloc - nVarsAllocOld) ); in Pr_ManResize()
224 ABC_FREE( p->pAssigns ); in Pr_ManFree()
462 if ( p->pAssigns[Var] != LIT_UNDEF ) in Pr_ManEnqueue()
463 return p->pAssigns[Var] == Lit; in Pr_ManEnqueue()
464 p->pAssigns[Var] = Lit; in Pr_ManEnqueue()
491 p->pAssigns[Var] = LIT_UNDEF; in Pr_ManCancelUntil()
529 if ( pCur->pLits[0] == p->pAssigns[lit_var(pCur->pLits[0])] ) in Pr_ManPropagateOne()
539 if ( lit_neg(pCur->pLits[i]) == p->pAssigns[lit_var(pCur->pLits[i])] ) in Pr_ManPropagateOne()