From a40c13a93cc19ec33a56995619a8acc442ad548c Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 22 Jul 2012 22:28:24 -0700 Subject: Recording and reusing learned util clauses in bmc2. --- src/aig/saig/saigBmc2.c | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) (limited to 'src/aig/saig') 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 -- cgit v1.2.3