Searched refs:hProofPivot (Results 1 – 7 of 7) sorted by relevance
383 int Sat_ProofReduce( Vec_Set_t * vProof, void * pRoots, int hProofPivot ) in Sat_ProofReduce() argument427 assert( hProofPivot >= 1 && hProofPivot <= Vec_SetHandCurrent(vProof) ); in Sat_ProofReduce()428 pPivot = Proof_NodeRead( vProof, hProofPivot ); in Sat_ProofReduce()
137 int hProofPivot; // the pivot for proof records member254 s->hProofPivot = Vec_SetHandCurrent(s->pPrf1); in sat_solver2_bookmark()
1165 s->hProofPivot = 1; // the pivot for proof records in sat_solver2_new()1571 extern int Sat_ProofReduce( Vec_Set_t * vProof, void * pRoots, int hProofPivot ); in sat_solver2_reducedb()1572 s->hProofPivot = Sat_ProofReduce( s->pPrf1, &s->claProofs, s->hProofPivot ); in sat_solver2_reducedb()1594 …assert( s->pPrf1 == NULL || (s->hProofPivot >= 1 && s->hProofPivot <= Vec_SetHandCurrent(s->pPrf1)… in sat_solver2_rollback()1639 Vec_SetShrink(s->pPrf1, s->hProofPivot); in sat_solver2_rollback()1687 s->hProofPivot = 1; // the pivot for proof records in sat_solver2_rollback()
116 int hProofPivot; // the pivot for proof records member
117 int hProofPivot; // the pivot for proof records member
1693 s->hProofPivot = 1; // the pivot for proof records in sat_solver3_rollback()
1728 s->hProofPivot = 1; // the pivot for proof records in sat_solver_rollback()