diff options
Diffstat (limited to 'src/sat')
-rw-r--r-- | src/sat/bsat/satProof.c | 5 | ||||
-rw-r--r-- | src/sat/bsat/satSolver.h | 1 | ||||
-rw-r--r-- | src/sat/bsat/satSolver2.c | 10 |
3 files changed, 11 insertions, 5 deletions
diff --git a/src/sat/bsat/satProof.c b/src/sat/bsat/satProof.c index 680b1996..eeadf09e 100644 --- a/src/sat/bsat/satProof.c +++ b/src/sat/bsat/satProof.c @@ -396,11 +396,15 @@ int Sat_ProofReduce( Vec_Set_t * vProof, void * pRoots, int hProofPivot ) if ( pNode->Id == 0 ) continue; pNode->Id = Vec_SetAppendS( vProof, 2 + pNode->nEnts ); + assert( pNode->Id > 0 ); Vec_PtrPush( vUsed, pNode ); // update fanins Proof_NodeForeachFanin( vProof, pNode, pFanin, k ) if ( (pNode->pEnts[k] & 1) == 0 ) // proof node + { + assert( pFanin->Id > 0 ); pNode->pEnts[k] = (pFanin->Id << 2) | (pNode->pEnts[k] & 2); + } // else // problem clause // assert( (int*)pFanin >= Vec_IntArray(vClauses) && (int*)pFanin < Vec_IntArray(vClauses)+Vec_IntSize(vClauses) ); } @@ -420,7 +424,6 @@ int Sat_ProofReduce( Vec_Set_t * vProof, void * pRoots, int hProofPivot ) if ( pPivot && pPivot <= pNode ) { RetValue = hTemp; -// s->iProofPivot = i; pPivot = NULL; } } diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h index 520e8284..eace9eea 100644 --- a/src/sat/bsat/satSolver.h +++ b/src/sat/bsat/satSolver.h @@ -30,7 +30,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "satVec.h" #include "satClause.h" -#include "misc/vec/vecSet.h" ABC_NAMESPACE_HEADER_START diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c index cb6199ec..2cd825b7 100644 --- a/src/sat/bsat/satSolver2.c +++ b/src/sat/bsat/satSolver2.c @@ -164,7 +164,7 @@ static inline void proof_chain_start( sat_solver2* s, clause* c ) if ( s->fProofLogging ) { int ProofId = clause2_proofid(s, c, 0); - assert( ProofId > 0 ); + assert( (ProofId >> 2) > 0 ); veci_resize( &s->temp_proof, 0 ); veci_push( &s->temp_proof, 0 ); veci_push( &s->temp_proof, 0 ); @@ -178,7 +178,7 @@ static inline void proof_chain_resolve( sat_solver2* s, clause* cls, int Var ) { clause* c = cls ? cls : var_unit_clause( s, Var ); int ProofId = clause2_proofid(s, c, var_is_partA(s,Var)); - assert( ProofId > 0 ); + assert( (ProofId >> 2) > 0 ); veci_push( &s->temp_proof, ProofId ); } } @@ -1417,7 +1417,10 @@ void sat_solver2_reducedb(sat_solver2* s) break; } if ( j < nLearnedOld / 6 ) + { + ABC_FREE( pSortValues ); return; + } // mark learned clauses to remove Counter = j = 0; @@ -1439,6 +1442,7 @@ void sat_solver2_reducedb(sat_solver2* s) s->stats.learnts--; } } + ABC_FREE( pSortValues ); // if ( j == nLearnedOld ) // return; @@ -1717,6 +1721,7 @@ void sat_solver2_verify( sat_solver2* s ) // Abc_Print(1, "Verification passed.\n" ); } */ + // checks how many watched clauses are satisfied by 0-level assignments // (this procedure may be called before setting up a new bookmark for rollback) int sat_solver2_check_watched( sat_solver2* s ) @@ -1754,7 +1759,6 @@ int sat_solver2_check_watched( sat_solver2* s ) return 0; } - int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal) { int restart_iter = 0; |