diff options
| -rw-r--r-- | src/aig/gia/giaAbsRef.c | 2 | ||||
| -rw-r--r-- | src/aig/gia/giaUtil.c | 2 | ||||
| -rw-r--r-- | src/aig/saig/saigBmc2.c | 18 | ||||
| -rw-r--r-- | src/misc/extra/extraUtilMisc.c | 2 | ||||
| -rw-r--r-- | src/sat/bsat/satSolver.c | 1 |
5 files changed, 22 insertions, 3 deletions
diff --git a/src/aig/gia/giaAbsRef.c b/src/aig/gia/giaAbsRef.c index 4532a90b..e982ced3 100644 --- a/src/aig/gia/giaAbsRef.c +++ b/src/aig/gia/giaAbsRef.c @@ -207,7 +207,7 @@ void Rnm_ManCollect_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vObjs, int } void Rnm_ManCollect( Rnm_Man_t * p ) { - Gia_Obj_t * pObj; + Gia_Obj_t * pObj = NULL; int i; // mark const/PIs/PPIs Gia_ManIncrementTravId( p->pGia ); diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c index c212fe64..01e2b1bd 100644 --- a/src/aig/gia/giaUtil.c +++ b/src/aig/gia/giaUtil.c @@ -1461,6 +1461,8 @@ unsigned * Gia_ObjComputeTruthTable( Gia_Man_t * p, Gia_Obj_t * pObj ) pTruth = Gla_ObjTruthElem( p, Gia_ObjCioId(pRoot) ); else if ( Gia_ObjIsAnd(pRoot) ) pTruth = Gla_ObjTruthNode( p, pRoot ); + else + pTruth = NULL; return (unsigned *)Gla_ObjTruthDup( p, Gla_ObjTruthFree2(p), pTruth, Gia_ObjIsCo(pObj) && Gia_ObjFaninC0(pObj) ); } diff --git a/src/aig/saig/saigBmc2.c b/src/aig/saig/saigBmc2.c index 7533c952..94c8d2c0 100644 --- a/src/aig/saig/saigBmc2.c +++ b/src/aig/saig/saigBmc2.c @@ -671,7 +671,7 @@ Abc_Cex_t * Saig_BmcGenerateCounterExample( Saig_Bmc_t * p ) int Saig_BmcSolveTargets( Saig_Bmc_t * p, int nStart, int * pnOutsSolved ) { Aig_Obj_t * pObj; - int i, VarNum, Lit, RetValue; + int i, k, VarNum, Lit, status, RetValue; assert( Vec_PtrSize(p->vTargets) > 0 ); if ( p->pSat->qtail != p->pSat->qhead ) { @@ -688,7 +688,23 @@ int Saig_BmcSolveTargets( Saig_Bmc_t * p, int nStart, int * pnOutsSolved ) Lit = toLitCond( VarNum, Aig_IsComplement(pObj) ); RetValue = sat_solver_solve( p->pSat, &Lit, &Lit + 1, (ABC_INT64_T)p->nConfMaxOne, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); if ( RetValue == l_False ) // unsat + { + // add final unit clause + Lit = lit_neg( Lit ); + status = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 ); + assert( status ); + // add learned units + for ( k = 0; k < veci_size(&p->pSat->unit_lits); k++ ) + { + Lit = veci_begin(&p->pSat->unit_lits)[k]; + status = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 ); + assert( status ); + } + veci_resize(&p->pSat->unit_lits, 0); + // propagate units + sat_solver_compress( p->pSat ); continue; + } if ( RetValue == l_Undef ) // undecided return l_Undef; // generate counter-example diff --git a/src/misc/extra/extraUtilMisc.c b/src/misc/extra/extraUtilMisc.c index c490b14a..729d0c04 100644 --- a/src/misc/extra/extraUtilMisc.c +++ b/src/misc/extra/extraUtilMisc.c @@ -2402,7 +2402,7 @@ void Extra_NpnTest() clock_t clk = clock(); word * pFuncs; int * pComp, * pPerm; - int i, k, nUnique = 0; + int i;//, k, nUnique = 0; /* // read functions pFuncs = Extra_NpnRead( "C:\\_projects\\abc\\_TEST\\allan\\lib6var5M.txt", nFuncs ); diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index b2014404..fa17f41c 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -1526,6 +1526,7 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit return l_False; } //////////////////////////////////////////////// + veci_resize(&s->unit_lits, 0); // set the external limits s->nCalls++; |