fraCnf.c 8.94 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
/**CFile****************************************************************

  FileName    [fraCnf.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [New FRAIG package.]

  Synopsis    []

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - June 30, 2007.]

  Revision    [$Id: fraCnf.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]

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

#include "fra.h"

23 24 25
ABC_NAMESPACE_IMPL_START


Alan Mishchenko committed
26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45
////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////


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

  Synopsis    [Addes clauses to the solver.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
46
void Fra_AddClausesMux( Fra_Man_t * p, Aig_Obj_t * pNode )
Alan Mishchenko committed
47
{
Alan Mishchenko committed
48
    Aig_Obj_t * pNodeI, * pNodeT, * pNodeE;
Alan Mishchenko committed
49 50
    int pLits[4], RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE;

Alan Mishchenko committed
51 52
    assert( !Aig_IsComplement( pNode ) );
    assert( Aig_ObjIsMuxType( pNode ) );
Alan Mishchenko committed
53
    // get nodes (I = if, T = then, E = else)
Alan Mishchenko committed
54
    pNodeI = Aig_ObjRecognizeMux( pNode, &pNodeT, &pNodeE );
Alan Mishchenko committed
55 56 57
    // get the variable numbers
    VarF = Fra_ObjSatNum(pNode);
    VarI = Fra_ObjSatNum(pNodeI);
Alan Mishchenko committed
58 59
    VarT = Fra_ObjSatNum(Aig_Regular(pNodeT));
    VarE = Fra_ObjSatNum(Aig_Regular(pNodeE));
Alan Mishchenko committed
60
    // get the complementation flags
Alan Mishchenko committed
61 62
    fCompT = Aig_IsComplement(pNodeT);
    fCompE = Aig_IsComplement(pNodeE);
Alan Mishchenko committed
63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 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

    // f = ITE(i, t, e)

    // i' + t' + f
    // i' + t  + f'
    // i  + e' + f
    // i  + e  + f'

    // create four clauses
    pLits[0] = toLitCond(VarI, 1);
    pLits[1] = toLitCond(VarT, 1^fCompT);
    pLits[2] = toLitCond(VarF, 0);
    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
    assert( RetValue );
    pLits[0] = toLitCond(VarI, 1);
    pLits[1] = toLitCond(VarT, 0^fCompT);
    pLits[2] = toLitCond(VarF, 1);
    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
    assert( RetValue );
    pLits[0] = toLitCond(VarI, 0);
    pLits[1] = toLitCond(VarE, 1^fCompE);
    pLits[2] = toLitCond(VarF, 0);
    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
    assert( RetValue );
    pLits[0] = toLitCond(VarI, 0);
    pLits[1] = toLitCond(VarE, 0^fCompE);
    pLits[2] = toLitCond(VarF, 1);
    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
    assert( RetValue );

    // two additional clauses
    // t' & e' -> f'
    // t  & e  -> f 

    // t  + e   + f'
    // t' + e'  + f 

    if ( VarT == VarE )
    {
//        assert( fCompT == !fCompE );
        return;
    }

    pLits[0] = toLitCond(VarT, 0^fCompT);
    pLits[1] = toLitCond(VarE, 0^fCompE);
    pLits[2] = toLitCond(VarF, 1);
    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
    assert( RetValue );
    pLits[0] = toLitCond(VarT, 1^fCompT);
    pLits[1] = toLitCond(VarE, 1^fCompE);
    pLits[2] = toLitCond(VarF, 0);
    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
    assert( RetValue );
}

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

  Synopsis    [Addes clauses to the solver.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
129
void Fra_AddClausesSuper( Fra_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper )
Alan Mishchenko committed
130
{
Alan Mishchenko committed
131
    Aig_Obj_t * pFanin;
Alan Mishchenko committed
132
    int * pLits, nLits, RetValue, i;
Alan Mishchenko committed
133 134
    assert( !Aig_IsComplement(pNode) );
    assert( Aig_ObjIsNode( pNode ) );
Alan Mishchenko committed
135 136
    // create storage for literals
    nLits = Vec_PtrSize(vSuper) + 1;
Alan Mishchenko committed
137
    pLits = ABC_ALLOC( int, nLits );
Alan Mishchenko committed
138 139
    // suppose AND-gate is A & B = C
    // add !A => !C   or   A + !C
140
    Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pFanin, i )
Alan Mishchenko committed
141
    {
Alan Mishchenko committed
142
        pLits[0] = toLitCond(Fra_ObjSatNum(Aig_Regular(pFanin)), Aig_IsComplement(pFanin));
Alan Mishchenko committed
143 144 145 146 147
        pLits[1] = toLitCond(Fra_ObjSatNum(pNode), 1);
        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
        assert( RetValue );
    }
    // add A & B => C   or   !A + !B + C
148
    Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pFanin, i )
Alan Mishchenko committed
149
        pLits[i] = toLitCond(Fra_ObjSatNum(Aig_Regular(pFanin)), !Aig_IsComplement(pFanin));
Alan Mishchenko committed
150 151 152
    pLits[nLits-1] = toLitCond(Fra_ObjSatNum(pNode), 0);
    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + nLits );
    assert( RetValue );
Alan Mishchenko committed
153
    ABC_FREE( pLits );
Alan Mishchenko committed
154 155 156 157 158 159 160 161 162 163 164 165 166
}

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

  Synopsis    [Collects the supergate.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
167
void Fra_CollectSuper_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes )
Alan Mishchenko committed
168 169
{
    // if the new node is complemented or a PI, another gate begins
Alan Mishchenko committed
170 171
    if ( Aig_IsComplement(pObj) || Aig_ObjIsPi(pObj) || (!fFirst && Aig_ObjRefs(pObj) > 1) || 
         (fUseMuxes && Aig_ObjIsMuxType(pObj)) )
Alan Mishchenko committed
172 173 174 175 176
    {
        Vec_PtrPushUnique( vSuper, pObj );
        return;
    }
    // go through the branches
Alan Mishchenko committed
177 178
    Fra_CollectSuper_rec( Aig_ObjChild0(pObj), vSuper, 0, fUseMuxes );
    Fra_CollectSuper_rec( Aig_ObjChild1(pObj), vSuper, 0, fUseMuxes );
Alan Mishchenko committed
179 180 181 182 183 184 185 186 187 188 189 190 191
}

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

  Synopsis    [Collects the supergate.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
192
Vec_Ptr_t * Fra_CollectSuper( Aig_Obj_t * pObj, int fUseMuxes )
Alan Mishchenko committed
193 194
{
    Vec_Ptr_t * vSuper;
Alan Mishchenko committed
195 196
    assert( !Aig_IsComplement(pObj) );
    assert( !Aig_ObjIsPi(pObj) );
Alan Mishchenko committed
197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212
    vSuper = Vec_PtrAlloc( 4 );
    Fra_CollectSuper_rec( pObj, vSuper, 1, fUseMuxes );
    return vSuper;
}

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

  Synopsis    [Updates the solver clause database.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
213
void Fra_ObjAddToFrontier( Fra_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vFrontier )
Alan Mishchenko committed
214
{
Alan Mishchenko committed
215
    assert( !Aig_IsComplement(pObj) );
Alan Mishchenko committed
216 217 218 219
    if ( Fra_ObjSatNum(pObj) )
        return;
    assert( Fra_ObjSatNum(pObj) == 0 );
    assert( Fra_ObjFaninVec(pObj) == NULL );
Alan Mishchenko committed
220
    if ( Aig_ObjIsConst1(pObj) )
Alan Mishchenko committed
221 222
        return;
    Fra_ObjSetSatNum( pObj, p->nSatVars++ );
Alan Mishchenko committed
223
    if ( Aig_ObjIsNode(pObj) )
Alan Mishchenko committed
224 225 226 227 228 229 230 231 232 233 234 235 236 237
        Vec_PtrPush( vFrontier, pObj );
}

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

  Synopsis    [Updates the solver clause database.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
238
void Fra_CnfNodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
Alan Mishchenko committed
239 240
{ 
    Vec_Ptr_t * vFrontier, * vFanins;
Alan Mishchenko committed
241
    Aig_Obj_t * pNode, * pFanin;
Alan Mishchenko committed
242 243 244 245 246 247 248 249 250 251
    int i, k, fUseMuxes = 1;
    assert( pOld || pNew );
    // quit if CNF is ready
    if ( (!pOld || Fra_ObjFaninVec(pOld)) && (!pNew || Fra_ObjFaninVec(pNew)) )
        return;
    // start the frontier
    vFrontier = Vec_PtrAlloc( 100 );
    if ( pOld ) Fra_ObjAddToFrontier( p, pOld, vFrontier );
    if ( pNew ) Fra_ObjAddToFrontier( p, pNew, vFrontier );
    // explore nodes in the frontier
252
    Vec_PtrForEachEntry( Aig_Obj_t *, vFrontier, pNode, i )
Alan Mishchenko committed
253 254 255 256
    {
        // create the supergate
        assert( Fra_ObjSatNum(pNode) );
        assert( Fra_ObjFaninVec(pNode) == NULL );
Alan Mishchenko committed
257
        if ( fUseMuxes && Aig_ObjIsMuxType(pNode) )
Alan Mishchenko committed
258 259
        {
            vFanins = Vec_PtrAlloc( 4 );
Alan Mishchenko committed
260 261 262 263
            Vec_PtrPushUnique( vFanins, Aig_ObjFanin0( Aig_ObjFanin0(pNode) ) );
            Vec_PtrPushUnique( vFanins, Aig_ObjFanin0( Aig_ObjFanin1(pNode) ) );
            Vec_PtrPushUnique( vFanins, Aig_ObjFanin1( Aig_ObjFanin0(pNode) ) );
            Vec_PtrPushUnique( vFanins, Aig_ObjFanin1( Aig_ObjFanin1(pNode) ) );
264
            Vec_PtrForEachEntry( Aig_Obj_t *, vFanins, pFanin, k )
Alan Mishchenko committed
265
                Fra_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier );
Alan Mishchenko committed
266 267 268 269 270
            Fra_AddClausesMux( p, pNode );
        }
        else
        {
            vFanins = Fra_CollectSuper( pNode, fUseMuxes );
271
            Vec_PtrForEachEntry( Aig_Obj_t *, vFanins, pFanin, k )
Alan Mishchenko committed
272
                Fra_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier );
Alan Mishchenko committed
273 274 275 276 277 278 279 280 281 282 283 284 285 286 287
            Fra_AddClausesSuper( p, pNode, vFanins );
        }
        assert( Vec_PtrSize(vFanins) > 1 );
        Fra_ObjSetFaninVec( pNode, vFanins );
    }
    Vec_PtrFree( vFrontier );
}



////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////


288 289
ABC_NAMESPACE_IMPL_END