sswSat.c 9.22 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    [sswSat.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Inductive prover with constraints.]

  Synopsis    [Calls to the SAT solver.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - September 1, 2008.]

  Revision    [$Id: sswSat.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]

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

#include "sswInt.h"

23 24 25
ABC_NAMESPACE_IMPL_START


Alan Mishchenko committed
26 27 28 29 30 31 32 33 34 35 36 37
////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

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

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

  Synopsis    [Runs equivalence test for the two nodes.]

Alan Mishchenko committed
38
  Description [Both nodes should be regular and different from each other.]
Alan Mishchenko committed
39 40 41 42 43 44 45 46 47
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
{
    int nBTLimit = p->pPars->nBTLimit;
48
    int pLits[3], nLits, RetValue, RetValue1;
49
    abctime clk;//, status;
Alan Mishchenko committed
50
    p->nSatCalls++;
Alan Mishchenko committed
51
    p->pMSat->nSolverCalls++;
Alan Mishchenko committed
52 53 54

    // sanity checks
    assert( !Aig_IsComplement(pOld) );
Alan Mishchenko committed
55 56
    assert( !Aig_IsComplement(pNew) );
    assert( pOld != pNew );
Alan Mishchenko committed
57
    assert( p->pMSat != NULL );
Alan Mishchenko committed
58 59

    // if the nodes do not have SAT variables, allocate them
Alan Mishchenko committed
60 61
    Ssw_CnfNodeAddToSolver( p->pMSat, pOld );
    Ssw_CnfNodeAddToSolver( p->pMSat, pNew );
Alan Mishchenko committed
62 63 64

    // solve under assumptions
    // A = 1; B = 0     OR     A = 1; B = 1 
Alan Mishchenko committed
65
    nLits = 2;
Alan Mishchenko committed
66 67
    pLits[0] = toLitCond( Ssw_ObjSatNum(p->pMSat,pOld), 0 );
    pLits[1] = toLitCond( Ssw_ObjSatNum(p->pMSat,pNew), pOld->fPhase == pNew->fPhase );
Alan Mishchenko committed
68 69
    if ( p->iOutputLit > -1 )
        pLits[nLits++] = p->iOutputLit;
Alan Mishchenko committed
70 71 72 73 74 75
    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 );
Alan Mishchenko committed
76

Alan Mishchenko committed
77
    if ( p->pMSat->pSat->qtail != p->pMSat->pSat->qhead )
Alan Mishchenko committed
78
    {
Alan Mishchenko committed
79
        RetValue = sat_solver_simplify(p->pMSat->pSat);
Alan Mishchenko committed
80 81
        assert( RetValue != 0 );
    }
Alan Mishchenko committed
82

83
clk = Abc_Clock();
Alan Mishchenko committed
84
    RetValue1 = sat_solver_solve( p->pMSat->pSat, pLits, pLits + nLits, 
Alan Mishchenko committed
85
        (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
86
p->timeSat += Abc_Clock() - clk;
Alan Mishchenko committed
87 88
    if ( RetValue1 == l_False )
    {
89
p->timeSatUnsat += Abc_Clock() - clk;
Alan Mishchenko committed
90 91 92 93
        if ( nLits == 2 )
        {
            pLits[0] = lit_neg( pLits[0] );
            pLits[1] = lit_neg( pLits[1] );
Alan Mishchenko committed
94
            RetValue = sat_solver_addclause( p->pMSat->pSat, pLits, pLits + 2 );
Alan Mishchenko committed
95
            assert( RetValue );
Alan Mishchenko committed
96 97 98 99 100 101 102
/*
            if ( p->pMSat->pSat->qtail != p->pMSat->pSat->qhead )
            {
                RetValue = sat_solver_simplify(p->pMSat->pSat);
                assert( RetValue != 0 );
            }
*/
Alan Mishchenko committed
103
        }
Alan Mishchenko committed
104 105 106 107
        p->nSatCallsUnsat++;
    }
    else if ( RetValue1 == l_True )
    {
108
p->timeSatSat += Abc_Clock() - clk;
Alan Mishchenko committed
109 110 111 112 113
        p->nSatCallsSat++;
        return 0;
    }
    else // if ( RetValue1 == l_Undef )
    {
114
p->timeSatUndec += Abc_Clock() - clk;
Alan Mishchenko committed
115 116 117 118 119 120 121 122 123 124 125 126 127
        p->nSatFailsReal++;
        return -1;
    }

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

    // solve under assumptions
    // A = 0; B = 1     OR     A = 0; B = 0 
Alan Mishchenko committed
128
    nLits = 2;
Alan Mishchenko committed
129 130
    pLits[0] = toLitCond( Ssw_ObjSatNum(p->pMSat,pOld), 1 );
    pLits[1] = toLitCond( Ssw_ObjSatNum(p->pMSat,pNew), pOld->fPhase ^ pNew->fPhase );
Alan Mishchenko committed
131 132
    if ( p->iOutputLit > -1 )
        pLits[nLits++] = p->iOutputLit;
Alan Mishchenko committed
133 134 135 136 137
    if ( p->pPars->fPolarFlip )
    {
        if ( pOld->fPhase )  pLits[0] = lit_neg( pLits[0] );
        if ( pNew->fPhase )  pLits[1] = lit_neg( pLits[1] );
    }
Alan Mishchenko committed
138

Alan Mishchenko committed
139
    if ( p->pMSat->pSat->qtail != p->pMSat->pSat->qhead )
Alan Mishchenko committed
140
    {
Alan Mishchenko committed
141
        RetValue = sat_solver_simplify(p->pMSat->pSat);
Alan Mishchenko committed
142 143
        assert( RetValue != 0 );
    }
Alan Mishchenko committed
144

145
clk = Abc_Clock();
Alan Mishchenko committed
146
    RetValue1 = sat_solver_solve( p->pMSat->pSat, pLits, pLits + nLits, 
Alan Mishchenko committed
147
        (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
148
p->timeSat += Abc_Clock() - clk;
Alan Mishchenko committed
149 150
    if ( RetValue1 == l_False )
    {
151
p->timeSatUnsat += Abc_Clock() - clk;
Alan Mishchenko committed
152 153 154 155
        if ( nLits == 2 )
        {
            pLits[0] = lit_neg( pLits[0] );
            pLits[1] = lit_neg( pLits[1] );
Alan Mishchenko committed
156
            RetValue = sat_solver_addclause( p->pMSat->pSat, pLits, pLits + 2 );
Alan Mishchenko committed
157
            assert( RetValue );
Alan Mishchenko committed
158 159 160 161 162 163 164
/*
            if ( p->pMSat->pSat->qtail != p->pMSat->pSat->qhead )
            {
                RetValue = sat_solver_simplify(p->pMSat->pSat);
                assert( RetValue != 0 );
            }
*/
Alan Mishchenko committed
165
        }
Alan Mishchenko committed
166 167 168 169
        p->nSatCallsUnsat++;
    }
    else if ( RetValue1 == l_True )
    {
170
p->timeSatSat += Abc_Clock() - clk;
Alan Mishchenko committed
171 172 173 174 175
        p->nSatCallsSat++;
        return 0;
    }
    else // if ( RetValue1 == l_Undef )
    {
176
p->timeSatUndec += Abc_Clock() - clk;
Alan Mishchenko committed
177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197
        p->nSatFailsReal++;
        return -1;
    }
    // return SAT proof
    p->nSatProof++;
    return 1;
}

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

  Synopsis    [Constrains two nodes to be equivalent in the SAT solver.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
{
Alan Mishchenko committed
198 199
    int pLits[2], RetValue, fComplNew;
    Aig_Obj_t * pTemp;
Alan Mishchenko committed
200 201

    // sanity checks
Alan Mishchenko committed
202
    assert( Aig_Regular(pOld) != Aig_Regular(pNew) );
203
    assert( p->pPars->fConstrs || Aig_ObjPhaseReal(pOld) == Aig_ObjPhaseReal(pNew) );
Alan Mishchenko committed
204

Alan Mishchenko committed
205 206 207 208 209 210 211 212 213 214 215 216 217 218 219
    // move constant to the old node
    if ( Aig_Regular(pNew) == Aig_ManConst1(p->pFrames) )
    {
        assert( Aig_Regular(pOld) != Aig_ManConst1(p->pFrames) );
        pTemp = pOld;
        pOld  = pNew;
        pNew  = pTemp;
    }

    // move complement to the new node
    if ( Aig_IsComplement(pOld) )
    {
        pOld = Aig_Regular(pOld);
        pNew = Aig_Not(pNew);
    }
Alan Mishchenko committed
220
    assert( p->pMSat != NULL );
Alan Mishchenko committed
221 222

    // if the nodes do not have SAT variables, allocate them
Alan Mishchenko committed
223 224
    Ssw_CnfNodeAddToSolver( p->pMSat, pOld );
    Ssw_CnfNodeAddToSolver( p->pMSat, Aig_Regular(pNew) );
Alan Mishchenko committed
225 226 227 228

    // transform the new node
    fComplNew = Aig_IsComplement( pNew );
    pNew = Aig_Regular( pNew );
Alan Mishchenko committed
229

Alan Mishchenko committed
230
    // consider the constant 1 case
Alan Mishchenko committed
231 232
    if ( pOld == Aig_ManConst1(p->pFrames) )
    {
Alan Mishchenko committed
233
        // add constraint A = 1  ---->  A
Alan Mishchenko committed
234
        pLits[0] = toLitCond( Ssw_ObjSatNum(p->pMSat,pNew), fComplNew );
Alan Mishchenko committed
235 236 237 238
        if ( p->pPars->fPolarFlip )
        {
            if ( pNew->fPhase )  pLits[0] = lit_neg( pLits[0] );
        }
Alan Mishchenko committed
239
        RetValue = sat_solver_addclause( p->pMSat->pSat, pLits, pLits + 1 );
Alan Mishchenko committed
240 241 242 243
        assert( RetValue );
    }
    else
    {
Alan Mishchenko committed
244
        // add constraint A = B  ---->  (A v !B)(!A v B)
Alan Mishchenko committed
245 246

        // (A v !B)
Alan Mishchenko committed
247 248
        pLits[0] = toLitCond( Ssw_ObjSatNum(p->pMSat,pOld), 0 );
        pLits[1] = toLitCond( Ssw_ObjSatNum(p->pMSat,pNew), !fComplNew );
Alan Mishchenko committed
249 250 251 252 253 254 255
        if ( p->pPars->fPolarFlip )
        {
            if ( pOld->fPhase )  pLits[0] = lit_neg( pLits[0] );
            if ( pNew->fPhase )  pLits[1] = lit_neg( pLits[1] );
        }
        pLits[0] = lit_neg( pLits[0] );
        pLits[1] = lit_neg( pLits[1] );
Alan Mishchenko committed
256
        RetValue = sat_solver_addclause( p->pMSat->pSat, pLits, pLits + 2 );
Alan Mishchenko committed
257 258
        assert( RetValue );

Alan Mishchenko committed
259
        // (!A v B)
Alan Mishchenko committed
260 261
        pLits[0] = toLitCond( Ssw_ObjSatNum(p->pMSat,pOld), 1 );
        pLits[1] = toLitCond( Ssw_ObjSatNum(p->pMSat,pNew), fComplNew);
Alan Mishchenko committed
262 263 264 265 266 267 268
        if ( p->pPars->fPolarFlip )
        {
            if ( pOld->fPhase )  pLits[0] = lit_neg( pLits[0] );
            if ( pNew->fPhase )  pLits[1] = lit_neg( pLits[1] );
        }
        pLits[0] = lit_neg( pLits[0] );
        pLits[1] = lit_neg( pLits[1] );
Alan Mishchenko committed
269
        RetValue = sat_solver_addclause( p->pMSat->pSat, pLits, pLits + 2 );
Alan Mishchenko committed
270 271 272 273 274
        assert( RetValue );
    }
    return 1;
}

275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300
/**Function*************************************************************

  Synopsis    [Constrains one node in the SAT solver.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Ssw_NodeIsConstrained( Ssw_Man_t * p, Aig_Obj_t * pPoObj )
{
    int RetValue, Lit;
    Ssw_CnfNodeAddToSolver( p->pMSat, Aig_ObjFanin0(pPoObj) );
    // add constraint A = 1  ---->  A
    Lit = toLitCond( Ssw_ObjSatNum(p->pMSat,Aig_ObjFanin0(pPoObj)), !Aig_ObjFaninC0(pPoObj) );
    if ( p->pPars->fPolarFlip )
    {
        if ( Aig_ObjFanin0(pPoObj)->fPhase )  Lit = lit_neg( Lit );
    }
    RetValue = sat_solver_addclause( p->pMSat->pSat, &Lit, &Lit + 1 );
    assert( RetValue );
    return 1;
}

Alan Mishchenko committed
301 302 303 304 305
////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////


306 307
ABC_NAMESPACE_IMPL_END