sfmSat.c 9.82 KB
Newer Older
Alan Mishchenko committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29
/**CFile****************************************************************

  FileName    [sfmSat.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [SAT-based optimization using internal don't-cares.]

  Synopsis    [SAT-based procedures.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - June 20, 2005.]

  Revision    [$Id: sfmSat.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]

***********************************************************************/

#include "sfmInt.h"

ABC_NAMESPACE_IMPL_START


////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

Alan Mishchenko committed
30 31 32 33 34 35 36 37 38
static word s_Truths6[6] = {
    ABC_CONST(0xAAAAAAAAAAAAAAAA),
    ABC_CONST(0xCCCCCCCCCCCCCCCC),
    ABC_CONST(0xF0F0F0F0F0F0F0F0),
    ABC_CONST(0xFF00FF00FF00FF00),
    ABC_CONST(0xFFFF0000FFFF0000),
    ABC_CONST(0xFFFFFFFF00000000)
};

Alan Mishchenko committed
39 40 41 42 43 44
////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////

/**Function*************************************************************

Alan Mishchenko committed
45 46 47 48 49 50 51 52 53
  Synopsis    [Converts a window into a SAT solver.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
54
int Sfm_NtkWindowToSolver( Sfm_Ntk_t * p )
Alan Mishchenko committed
55
{
Alan Mishchenko committed
56 57 58 59
    // p->vOrder contains all variables in the window in a good order
    // p->vDivs is a subset of nodes in p->vOrder used as divisor candidates
    // p->vTfo contains TFO of the node (does not include node)
    // p->vRoots contains roots of the TFO of the node (may include node)
Alan Mishchenko committed
60
    Vec_Int_t * vClause;
Alan Mishchenko committed
61
    int RetValue, iNode = -1, iFanin, i, k;
62
    abctime clk = Abc_Clock();
Alan Mishchenko committed
63 64 65
//    if ( p->pSat )
//        printf( "%d  ", p->pSat->stats.learnts );
    sat_solver_restart( p->pSat );
Alan Mishchenko committed
66
    sat_solver_setnvars( p->pSat, 1 + Vec_IntSize(p->vOrder) + Vec_IntSize(p->vTfo) + Vec_IntSize(p->vRoots) + 10 );
Alan Mishchenko committed
67
    // create SAT variables
Alan Mishchenko committed
68
    Sfm_NtkCleanVars( p );
Alan Mishchenko committed
69
    p->nSatVars = 1;
Alan Mishchenko committed
70
    Vec_IntForEachEntry( p->vOrder, iNode, i )
Alan Mishchenko committed
71
        Sfm_ObjSetSatVar( p, iNode, p->nSatVars++ );
Alan Mishchenko committed
72
    // collect divisor variables
Alan Mishchenko committed
73 74 75
    Vec_IntClear( p->vDivVars );
    Vec_IntForEachEntry( p->vDivs, iNode, i )
        Vec_IntPush( p->vDivVars, Sfm_ObjSatVar(p, iNode) );
Alan Mishchenko committed
76 77
    // add CNF clauses for the TFI
    Vec_IntForEachEntry( p->vOrder, iNode, i )
Alan Mishchenko committed
78
    {
Alan Mishchenko committed
79 80
        if ( Sfm_ObjIsPi(p, iNode) )
            continue;
Alan Mishchenko committed
81 82 83 84 85 86
        // collect fanin variables
        Vec_IntClear( p->vFaninMap );
        Sfm_ObjForEachFanin( p, iNode, iFanin, k )
            Vec_IntPush( p->vFaninMap, Sfm_ObjSatVar(p, iFanin) );
        Vec_IntPush( p->vFaninMap, Sfm_ObjSatVar(p, iNode) );
        // generate CNF 
Alan Mishchenko committed
87
        Sfm_TranslateCnf( p->vClauses, (Vec_Str_t *)Vec_WecEntry(p->vCnfs, iNode), p->vFaninMap, -1 );
Alan Mishchenko committed
88 89
        // add clauses
        Vec_WecForEachLevel( p->vClauses, vClause, k )
Alan Mishchenko committed
90
        {
Alan Mishchenko committed
91 92
            if ( Vec_IntSize(vClause) == 0 )
                break;
Alan Mishchenko committed
93
            RetValue = sat_solver_addclause( p->pSat, Vec_IntArray(vClause), Vec_IntArray(vClause) + Vec_IntSize(vClause) );
94 95
            if ( RetValue == 0 )
                return 0;
Alan Mishchenko committed
96 97
        }
    }
Alan Mishchenko committed
98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129
    if ( Vec_IntSize(p->vTfo) > 0 )
    {
        assert( p->pPars->nTfoLevMax > 0 );
        assert( Vec_IntSize(p->vRoots) > 0 );
        assert( Vec_IntEntry(p->vTfo, 0) != p->iPivotNode );
        // collect variables of root nodes
        Vec_IntClear( p->vLits );
        Vec_IntForEachEntry( p->vRoots, iNode, i )
            Vec_IntPush( p->vLits, Sfm_ObjSatVar(p, iNode) );
        // assign new variables to the TFO nodes
        Vec_IntForEachEntry( p->vTfo, iNode, i )
        {
            Sfm_ObjCleanSatVar( p, Sfm_ObjSatVar(p, iNode) );
            Sfm_ObjSetSatVar( p, iNode, p->nSatVars++ );
        }
        // add CNF clauses for the TFO
        Vec_IntForEachEntry( p->vTfo, iNode, i )
        {
            assert( Sfm_ObjIsNode(p, iNode) );
            // collect fanin variables
            Vec_IntClear( p->vFaninMap );
            Sfm_ObjForEachFanin( p, iNode, iFanin, k )
                Vec_IntPush( p->vFaninMap, Sfm_ObjSatVar(p, iFanin) );
            Vec_IntPush( p->vFaninMap, Sfm_ObjSatVar(p, iNode) );
            // generate CNF 
            Sfm_TranslateCnf( p->vClauses, (Vec_Str_t *)Vec_WecEntry(p->vCnfs, iNode), p->vFaninMap, Sfm_ObjSatVar(p, p->iPivotNode) );
            // add clauses
            Vec_WecForEachLevel( p->vClauses, vClause, k )
            {
                if ( Vec_IntSize(vClause) == 0 )
                    break;
                RetValue = sat_solver_addclause( p->pSat, Vec_IntArray(vClause), Vec_IntArray(vClause) + Vec_IntSize(vClause) );
130 131
                if ( RetValue == 0 )
                    return 0;
Alan Mishchenko committed
132 133 134 135 136 137 138 139 140 141
            }
        }
        // create XOR clauses for the roots
        Vec_IntForEachEntry( p->vRoots, iNode, i )
        {
            sat_solver_add_xor( p->pSat, Vec_IntEntry(p->vLits, i), Sfm_ObjSatVar(p, iNode), p->nSatVars++, 0 );
            Vec_IntWriteEntry( p->vLits, i, Abc_Var2Lit(p->nSatVars-1, 0) );
        }
        // make OR clause for the last nRoots variables
        RetValue = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntArray(p->vLits) + Vec_IntSize(p->vLits) );
Alan Mishchenko committed
142 143
        if ( RetValue == 0 )
            return 0;
Alan Mishchenko committed
144
    }
Alan Mishchenko committed
145
    // finalize
Alan Mishchenko committed
146
    RetValue = sat_solver_simplify( p->pSat );
147
    p->timeCnf += Abc_Clock() - clk;
148
    return RetValue;
Alan Mishchenko committed
149
} 
Alan Mishchenko committed
150 151 152

/**Function*************************************************************

Alan Mishchenko committed
153
  Synopsis    [Takes SAT solver and returns interpolant.]
Alan Mishchenko committed
154

Alan Mishchenko committed
155
  Description [If interpolant does not exist, records difference variables.]
Alan Mishchenko committed
156 157 158 159 160 161
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
162
word Sfm_ComputeInterpolant( Sfm_Ntk_t * p )
Alan Mishchenko committed
163
{
Alan Mishchenko committed
164
    word * pSign, uCube, uTruth = 0;
Alan Mishchenko committed
165
    int status, i, Div, iVar, nFinal, * pFinal, nIter = 0;
Alan Mishchenko committed
166 167
    int pLits[2], nVars = sat_solver_nvars( p->pSat );
    sat_solver_setnvars( p->pSat, nVars + 1 );
Alan Mishchenko committed
168
    pLits[0] = Abc_Var2Lit( Sfm_ObjSatVar(p, p->iPivotNode), 0 ); // F = 1
Alan Mishchenko committed
169
    pLits[1] = Abc_Var2Lit( nVars, 0 ); // iNewLit
Alan Mishchenko committed
170 171 172
    while ( 1 ) 
    {
        // find onset minterm
Alan Mishchenko committed
173
        p->nSatCalls++;
Alan Mishchenko committed
174
        status = sat_solver_solve( p->pSat, pLits, pLits + 2, p->pPars->nBTLimit, 0, 0, 0 );
Alan Mishchenko committed
175 176 177 178 179
        if ( status == l_Undef )
            return SFM_SAT_UNDEC;
        if ( status == l_False )
            return uTruth;
        assert( status == l_True );
Alan Mishchenko committed
180 181 182 183
        // remember variable values
        Vec_IntClear( p->vValues );
        Vec_IntForEachEntry( p->vDivVars, iVar, i )
            Vec_IntPush( p->vValues, sat_solver_var_value(p->pSat, iVar) );
Alan Mishchenko committed
184 185
        // collect divisor literals
        Vec_IntClear( p->vLits );
Alan Mishchenko committed
186
        Vec_IntPush( p->vLits, Abc_LitNot(pLits[0]) ); // F = 0
Alan Mishchenko committed
187
        Vec_IntForEachEntry( p->vDivIds, Div, i )
Alan Mishchenko committed
188
            Vec_IntPush( p->vLits, sat_solver_var_literal(p->pSat, Div) );
Alan Mishchenko committed
189
        // check against offset
Alan Mishchenko committed
190
        p->nSatCalls++;
Alan Mishchenko committed
191
        status = sat_solver_solve( p->pSat, Vec_IntArray(p->vLits), Vec_IntArray(p->vLits) + Vec_IntSize(p->vLits), p->pPars->nBTLimit, 0, 0, 0 );
Alan Mishchenko committed
192 193 194
        if ( status == l_Undef )
            return SFM_SAT_UNDEC;
        if ( status == l_True )
Alan Mishchenko committed
195
            break;
Alan Mishchenko committed
196 197
        assert( status == l_False );
        // compute cube and add clause
Alan Mishchenko committed
198
        nFinal = sat_solver_final( p->pSat, &pFinal );
Alan Mishchenko committed
199
        uCube = ~(word)0;
Alan Mishchenko committed
200
        Vec_IntClear( p->vLits );
Alan Mishchenko committed
201
        Vec_IntPush( p->vLits, Abc_LitNot(pLits[1]) ); // NOT(iNewLit)
Alan Mishchenko committed
202 203
        for ( i = 0; i < nFinal; i++ )
        {
Alan Mishchenko committed
204 205
            if ( pFinal[i] == pLits[0] )
                continue;
Alan Mishchenko committed
206 207
            Vec_IntPush( p->vLits, pFinal[i] );
            iVar = Vec_IntFind( p->vDivIds, Abc_Lit2Var(pFinal[i]) );   assert( iVar >= 0 );
Alan Mishchenko committed
208 209 210
            uCube &= Abc_LitIsCompl(pFinal[i]) ? s_Truths6[iVar] : ~s_Truths6[iVar];
        }
        uTruth |= uCube;
Alan Mishchenko committed
211
        status = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntArray(p->vLits) + Vec_IntSize(p->vLits) );
Alan Mishchenko committed
212
        assert( status );
Alan Mishchenko committed
213
        nIter++;
Alan Mishchenko committed
214
    }
Alan Mishchenko committed
215 216 217
    assert( status == l_True );
    // store the counter-example
    Vec_IntForEachEntry( p->vDivVars, iVar, i )
Alan Mishchenko committed
218
        if ( Vec_IntEntry(p->vValues, i) ^ sat_solver_var_value(p->pSat, iVar) ) // insert 1
Alan Mishchenko committed
219 220 221 222 223 224 225
        {
            pSign = Vec_WrdEntryP( p->vDivCexes, i );
            assert( !Abc_InfoHasBit( (unsigned *)pSign, p->nCexes) );
            Abc_InfoXorBit( (unsigned *)pSign, p->nCexes );
        }
    p->nCexes++;
    return SFM_SAT_SAT;
Alan Mishchenko committed
226 227
}

Alan Mishchenko committed
228 229 230 231 232 233 234 235 236 237 238 239 240 241
/**Function*************************************************************

  Synopsis    [Checks resubstitution.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Sfm_ComputeInterpolantCheck( Sfm_Ntk_t * p )
{
    int iNode = 3;
Alan Mishchenko committed
242 243
    int iDiv0 = 6;
    int iDiv1 = 7;
Alan Mishchenko committed
244 245 246 247
    word uTruth;
//    int i;
//    Sfm_NtkForEachNode( p, i )
    {
Alan Mishchenko committed
248 249
        Sfm_NtkCreateWindow( p, iNode, 1 );
        Sfm_NtkWindowToSolver( p );
Alan Mishchenko committed
250 251 252 253 254 255

        // collect SAT variables of divisors
        Vec_IntClear( p->vDivIds );
        Vec_IntPush( p->vDivIds, Sfm_ObjSatVar(p, iDiv0) );
        Vec_IntPush( p->vDivIds, Sfm_ObjSatVar(p, iDiv1) );

Alan Mishchenko committed
256
        uTruth = Sfm_ComputeInterpolant( p );
Alan Mishchenko committed
257 258 259 260 261 262 263 264 265 266

        if ( uTruth == SFM_SAT_SAT )
            printf( "The problem is SAT.\n" );
        else if ( uTruth == SFM_SAT_UNDEC )
            printf( "The problem is UNDEC.\n" );
        else
            Kit_DsdPrintFromTruth( (unsigned *)&uTruth, 2 ); printf( "\n" );
    }
}

Alan Mishchenko committed
267 268 269 270 271 272 273
////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////


ABC_NAMESPACE_IMPL_END