dchSat.c File Reference

#include "dchInt.h"

Go to the source code of this file.

Functions
ABC_NAMESPACE_IMPL_START int	Dch_NodesAreEquiv (Dch_Man_t *p, Aig_Obj_t *pOld, Aig_Obj_t *pNew)
	DECLARATIONS ///. More...

Function Documentation

ABC_NAMESPACE_IMPL_START int Dch_NodesAreEquiv	(	Dch_Man_t *	p,
		Aig_Obj_t *	pOld,
		Aig_Obj_t *	pNew
	)

DECLARATIONS ///.

CFile****************************************************************

FileName [dchSat.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Choice computation for tech-mapping.]

Synopsis [Calls to the SAT solver.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 29, 2008.]

Revision [

Id:

dchSat.c,v 1.00 2008/07/29 00:00:00 alanmi Exp

]FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Runs equivalence test for the two nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file dchSat.c.

{
    int nBTLimit = p->pPars->nBTLimit;
    int pLits[2], RetValue, RetValue1, status;
    abctime clk;
    p->nSatCalls++;

    // sanity checks
    assert( !Aig_IsComplement(pNew) );
    assert( !Aig_IsComplement(pOld) );
    assert( pNew != pOld );

    p->nCallsSince++;  // experiment with this!!!
    
    // check if SAT solver needs recycling
    if ( p->pSat == NULL || 
        (p->pPars->nSatVarMax && 
         p->nSatVars > p->pPars->nSatVarMax && 
         p->nCallsSince > p->pPars->nCallsRecycle) )
        Dch_ManSatSolverRecycle( p );

    // if the nodes do not have SAT variables, allocate them
    Dch_CnfNodeAddToSolver( p, pOld );
    Dch_CnfNodeAddToSolver( p, pNew );

    // propage unit clauses
    if ( p->pSat->qtail != p->pSat->qhead )
    {
        status = sat_solver_simplify(p->pSat);
        assert( status != 0 );
        assert( p->pSat->qtail == p->pSat->qhead );
    }

    // solve under assumptions
    // A = 1; B = 0     OR     A = 1; B = 1 
    pLits[0] = toLitCond( Dch_ObjSatNum(p,pOld), 0 );
    pLits[1] = toLitCond( Dch_ObjSatNum(p,pNew), pOld->fPhase == pNew->fPhase );
    if ( p->pPars->fPolarFlip )
    {
        if ( pOld->fPhase )  pLits[0] = lit_neg( pLits[0] );
        if ( pNew->fPhase )  pLits[1] = lit_neg( pLits[1] );
    }
//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
clk = Abc_Clock();
    RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, 
        (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
p->timeSat += Abc_Clock() - clk;
    if ( RetValue1 == l_False )
    {
p->timeSatUnsat += Abc_Clock() - clk;
        pLits[0] = lit_neg( pLits[0] );
        pLits[1] = lit_neg( pLits[1] );
        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
        assert( RetValue );
        p->nSatCallsUnsat++;
    }
    else if ( RetValue1 == l_True )
    {
p->timeSatSat += Abc_Clock() - clk;
        p->nSatCallsSat++;
        return 0;
    }
    else // if ( RetValue1 == l_Undef )
    {
p->timeSatUndec += Abc_Clock() - clk;
        p->nSatFailsReal++;
        return -1;
    }

    // if the old node was constant 0, we already know the answer
    if ( pOld == Aig_ManConst1(p->pAigFraig) )
    {
        p->nSatProof++;
        return 1;
    }

    // solve under assumptions
    // A = 0; B = 1     OR     A = 0; B = 0 
    pLits[0] = toLitCond( Dch_ObjSatNum(p,pOld), 1 );
    pLits[1] = toLitCond( Dch_ObjSatNum(p,pNew), pOld->fPhase ^ pNew->fPhase );
    if ( p->pPars->fPolarFlip )
    {
        if ( pOld->fPhase )  pLits[0] = lit_neg( pLits[0] );
        if ( pNew->fPhase )  pLits[1] = lit_neg( pLits[1] );
    }
clk = Abc_Clock();
    RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, 
        (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
p->timeSat += Abc_Clock() - clk;
    if ( RetValue1 == l_False )
    {
p->timeSatUnsat += Abc_Clock() - clk;
        pLits[0] = lit_neg( pLits[0] );
        pLits[1] = lit_neg( pLits[1] );
        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
        assert( RetValue );
        p->nSatCallsUnsat++;
    }
    else if ( RetValue1 == l_True )
    {
p->timeSatSat += Abc_Clock() - clk;
        p->nSatCallsSat++;
        return 0;
    }
    else // if ( RetValue1 == l_Undef )
    {
p->timeSatUndec += Abc_Clock() - clk;
        p->nSatFailsReal++;
        return -1;
    }
    // return SAT proof
    p->nSatProof++;
    return 1;
}