abc/src/sat/bsat/satInterP.c
/**Function*************************************************************

  Synopsis    [Computes UNSAT core of the satisfiablity problem.]

  Description [Takes the interpolation manager, the CNF derived by the SAT
  solver, which includes the root clauses and the learned clauses. Returns
  the array of integers representing the number of root clauses that are in
  the UNSAT core.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Function
Synopsis    [Computes UNSAT core of the satisfiablity problem.]

Description [Takes the interpolation manager, the CNF derived by the SAT
solver, which includes the root clauses and the learned clauses. Returns
the array of integers representing the number of root clauses that are in
the UNSAT core.]




Function Synopsis [ Computes UNSAT core of the satisfiablity problem . ] Description [ Takes the interpolation manager the CNF derived by the SAT solver which includes the root clauses and the learned clauses . Returns the array of integers representing the number of root clauses that are in the UNSAT core . ]
void * Intp_ManUnsatCore( Intp_Man_t * p, Sto_Man_t * pCnf, int fLearned, int fVerbose )
{
    Vec_Int_t * vCore;
    Vec_Str_t * vVisited;
    Sto_Cls_t * pClause;
    int RetValue = 1;
    abctime clkTotal = Abc_Clock();
    assert( pCnf->nVars > 0 && pCnf->nClauses > 0 );
    p->pCnf = pCnf;
    p->fVerbose = fVerbose;
    Intp_ManResize( p ); 
    if ( p->fProofWrite )
    {
        p->pFile = fopen( "proof.cnf_", "w" );
        p->Counter = 0;
    }
    Vec_PtrClear( p->vAntClas );
    p->nAntStart = p->pCnf->nRoots;
    Sto_ManForEachClauseRoot( p->pCnf, pClause )
        Intp_ManProofWriteOne( p, pClause );
    if ( Intp_ManProcessRoots( p ) )
    {
        Sto_ManForEachClause( p->pCnf, pClause )
        {
            if ( pClause->fRoot )
                continue;
            if ( !Intp_ManProofRecordOne( p, pClause ) )
            {
                RetValue = 0;
                break;
            }
        }
    }
    assert( p->pCnf->pEmpty->Id - p->nAntStart == Vec_PtrSize(p->vAntClas) - 1 );
    Vec_PtrPush( p->vAntClas, Vec_IntAlloc(0) );
    if ( p->fProofWrite )
    {
        fclose( p->pFile );
        p->pFile = NULL;    
    }
    if ( fVerbose )
    {
    printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d.  Ave = %.2f.  Mem = %.2f MB\n", 
        p->pCnf->nVars, p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, p->Counter,  
        1.0*(p->Counter-p->pCnf->nRoots)/(p->pCnf->nClauses-p->pCnf->nRoots), 
        1.0*Sto_ManMemoryReport(p->pCnf)/(1<<20) );
p->timeTotal += Abc_Clock() - clkTotal;
    }
    vCore = Vec_IntAlloc( 1000 );
    vVisited = Vec_StrStart( p->pCnf->pEmpty->Id+1 );
    Intp_ManUnsatCore_rec( p->vAntClas, p->pCnf->pEmpty->Id, vCore, p->pCnf->nRoots, vVisited, fLearned );
    Vec_StrFree( vVisited );
    if ( fVerbose )
        printf( "Root clauses = %d. Learned clauses = %d. UNSAT core size = %d.\n", 
            p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, Vec_IntSize(vCore) );
    return vCore;   
}
void * Intp_ManUnsatCore ( Intp_Man_t * p , Sto_Man_t * pCnf , int fLearned , int fVerbose ) { Vec_Int_t * vCore ; Vec_Str_t * vVisited ; Sto_Cls_t * pClause ; int RetValue = 1 ; abctime clkTotal = Abc_Clock ( ) ; assert ( pCnf -> nVars > 0 && pCnf -> nClauses > 0 ) ; p -> pCnf = pCnf ; p -> fVerbose = fVerbose ; Intp_ManResize ( p ) ; if ( p -> fProofWrite ) { p -> pFile = fopen ( " " , " " ) ; p -> Counter = 0 ; } Vec_PtrClear ( p -> vAntClas ) ; p -> nAntStart = p -> pCnf -> nRoots ; Sto_ManForEachClauseRoot ( p -> pCnf , pClause ) Intp_ManProofWriteOne ( p , pClause ) ; if ( Intp_ManProcessRoots ( p ) ) { Sto_ManForEachClause ( p -> pCnf , pClause ) { if ( pClause -> fRoot ) continue ; if ( ! Intp_ManProofRecordOne ( p , pClause ) ) { RetValue = 0 ; break ; } } } assert ( p -> pCnf -> pEmpty -> Id - p -> nAntStart == Vec_PtrSize ( p -> vAntClas ) - 1 ) ; Vec_PtrPush ( p -> vAntClas , Vec_IntAlloc ( 0 ) ) ; if ( p -> fProofWrite ) { fclose ( p -> pFile ) ; p -> pFile = NULL ; } if ( fVerbose ) { printf ( " \n " , p -> pCnf -> nVars , p -> pCnf -> nRoots , p -> pCnf -> nClauses - p -> pCnf -> nRoots , p -> Counter , 1.0 * ( p -> Counter - p -> pCnf -> nRoots ) / ( p -> pCnf -> nClauses - p -> pCnf -> nRoots ) , 1.0 * Sto_ManMemoryReport ( p -> pCnf ) / ( 1 << 20 ) ) ; p -> timeTotal += Abc_Clock ( ) - clkTotal ; } vCore = Vec_IntAlloc ( 1000 ) ; vVisited = Vec_StrStart ( p -> pCnf -> pEmpty -> Id + 1 ) ; Intp_ManUnsatCore_rec ( p -> vAntClas , p -> pCnf -> pEmpty -> Id , vCore , p -> pCnf -> nRoots , vVisited , fLearned ) ; Vec_StrFree ( vVisited ) ; if ( fVerbose ) printf ( " \n " , p -> pCnf -> nRoots , p -> pCnf -> nClauses - p -> pCnf -> nRoots , Vec_IntSize ( vCore ) ) ; return vCore ; }
Function
Synopsis    [Computes UNSAT core of the satisfiablity problem.]
Function Synopsis [ Computes UNSAT core of the satisfiablity problem . ]
// check that the CNF makes sense // adjust the manager // construct proof for each clause // start the proof // write the root clauses //    Vec_IntClear( p->vAnties ); //    Vec_IntFill( p->vBreaks, p->pCnf->nRoots, 0 ); // propagate root level assignments // if there is no conflict, consider learned clauses // add the last breaker //    assert( p->pCnf->pEmpty->Id == Vec_IntSize(p->vBreaks) - 1 ); //    Vec_IntPush( p->vBreaks, Vec_IntSize(p->vAnties) ); // stop the proof //        Sat_ProofChecker( "proof.cnf_" ); //        ABC_PRT( "Core", Abc_Clock() - clkTotal ); // derive the UNSAT core //    Intp_ManUnsatCoreVerify( p->pCnf, vCore );