diff options
| -rw-r--r-- | src/aig/gia/giaAbsGla2.c | 9 | ||||
| -rw-r--r-- | src/sat/bsat/satProof2.h | 1 | ||||
| -rw-r--r-- | src/sat/bsat/satSolver2.c | 15 | ||||
| -rw-r--r-- | src/sat/bsat/satSolver2.h | 5 |
4 files changed, 25 insertions, 5 deletions
diff --git a/src/aig/gia/giaAbsGla2.c b/src/aig/gia/giaAbsGla2.c index 2c628ea8..fe8c7e3d 100644 --- a/src/aig/gia/giaAbsGla2.c +++ b/src/aig/gia/giaAbsGla2.c @@ -1484,6 +1484,15 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) nVarsOld = p->nSatVars; for ( c = 0; ; c++ ) { + // consider the special case when the target literal is implied false + // by implications which happened as a result of previous refinements + // note that incremental UNSAT core cannot be computed because there is no learned clauses + // in this case, we will assume that UNSAT core cannot reduce the problem + if ( var_is_assigned(p->pSat, Abc_Lit2Var(Lit)) ) + { + Prf_ManStopP( &p->pSat->pPrf2 ); + break; + } // perform SAT solving clk2 = clock(); Status = sat_solver2_solve( p->pSat, &Lit, &Lit+1, (ABC_INT64_T)pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); diff --git a/src/sat/bsat/satProof2.h b/src/sat/bsat/satProof2.h index 25ad0d07..b82d9590 100644 --- a/src/sat/bsat/satProof2.h +++ b/src/sat/bsat/satProof2.h @@ -290,6 +290,7 @@ static inline Vec_Int_t * Prf_ManUnsatCore( Prf_Man_t * p ) int i, Entry; assert( p->iFirst >= 0 ); assert( p->pInfo == NULL ); + assert( Prf_ManSize(p) > 0 ); vCore = Vec_IntAlloc( 64 * p->nWords ); p->pInfo = Prf_ManClauseInfo( p, Prf_ManSize(p)-1 ); if ( p->vId2Pr == NULL ) diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c index dfe01a23..2b65170a 100644 --- a/src/sat/bsat/satSolver2.c +++ b/src/sat/bsat/satSolver2.c @@ -80,8 +80,9 @@ struct varinfo2_t // unsigned lev : 24; // variable level }; -int var_is_partA (sat_solver2* s, int v) { return s->vi[v].partA; } -void var_set_partA(sat_solver2* s, int v, int partA) { s->vi[v].partA = partA; } +int var_is_assigned(sat_solver2* s, int v) { return s->assigns[v] != varX; } +int var_is_partA (sat_solver2* s, int v) { return s->vi[v].partA; } +void var_set_partA(sat_solver2* s, int v, int partA) { s->vi[v].partA = partA; } //static inline int var_level (sat_solver2* s, int v) { return s->vi[v].lev; } static inline int var_level (sat_solver2* s, int v) { return s->levels[v]; } @@ -95,6 +96,11 @@ static inline void var_set_level (sat_solver2* s, int v, int lev) { s->leve static inline void var_set_value (sat_solver2* s, int v, int val) { s->assigns[v] = val; } static inline void var_set_polar (sat_solver2* s, int v, int pol) { s->vi[v].pol = pol; } +// check if the literal is false under current assumptions +static inline int solver2_lit_is_false( sat_solver2* s, int Lit ) { return var_value(s, lit_var(Lit)) == !lit_sign(Lit); } + + + // variable tags static inline int var_tag (sat_solver2* s, int v) { return s->vi[v].tag; } static inline void var_set_tag (sat_solver2* s, int v, int tag) { @@ -1884,7 +1890,10 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim } else { - assert( 0 ); +// assert( 0 ); +// r = var_unit_clause( s, lit_var(p) ); +// assert( r != NULL ); +// proof_id = clause2_proofid(s, r, 0); proof_id = -1; // the only case when ProofId is not assigned (conflicting assumptions) veci_resize(&s->conf_final,0); veci_push(&s->conf_final, lit_neg(p)); diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h index bed774ef..a1539637 100644 --- a/src/sat/bsat/satSolver2.h +++ b/src/sat/bsat/satSolver2.h @@ -62,8 +62,9 @@ extern int * Sat_Solver2GetModel( sat_solver2 * p, int * pVars, int nVars extern void Sat_Solver2DoubleClauses( sat_solver2 * p, int iVar ); // global variables -extern int var_is_partA (sat_solver2* s, int v); -extern void var_set_partA(sat_solver2* s, int v, int partA); +extern int var_is_assigned(sat_solver2* s, int v); +extern int var_is_partA (sat_solver2* s, int v); +extern void var_set_partA (sat_solver2* s, int v, int partA); // proof-based APIs extern void * Sat_ProofCore( sat_solver2 * s ); |