sswSat.c 9.17 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;
Alan Mishchenko committed
48
    int pLits[3], nLits, RetValue, RetValue1, clk;//, status;
Alan Mishchenko committed
49
    p->nSatCalls++;
Alan Mishchenko committed
50
    p->pMSat->nSolverCalls++;
Alan Mishchenko committed
51 52 53

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

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

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

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

Alan Mishchenko committed
82
clk = clock();
Alan Mishchenko committed
83
    RetValue1 = sat_solver_solve( p->pMSat->pSat, pLits, pLits + nLits, 
Alan Mishchenko committed
84
        (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
Alan Mishchenko committed
85 86 87 88
p->timeSat += clock() - clk;
    if ( RetValue1 == l_False )
    {
p->timeSatUnsat += clock() - clk;
Alan Mishchenko committed
89 90 91 92
        if ( nLits == 2 )
        {
            pLits[0] = lit_neg( pLits[0] );
            pLits[1] = lit_neg( pLits[1] );
Alan Mishchenko committed
93
            RetValue = sat_solver_addclause( p->pMSat->pSat, pLits, pLits + 2 );
Alan Mishchenko committed
94
            assert( RetValue );
Alan Mishchenko committed
95 96 97 98 99 100 101
/*
            if ( p->pMSat->pSat->qtail != p->pMSat->pSat->qhead )
            {
                RetValue = sat_solver_simplify(p->pMSat->pSat);
                assert( RetValue != 0 );
            }
*/
Alan Mishchenko committed
102
        }
Alan Mishchenko committed
103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126
        p->nSatCallsUnsat++;
    }
    else if ( RetValue1 == l_True )
    {
p->timeSatSat += clock() - clk;
        p->nSatCallsSat++;
        return 0;
    }
    else // if ( RetValue1 == l_Undef )
    {
p->timeSatUndec += clock() - clk;
        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
127
    nLits = 2;
Alan Mishchenko committed
128 129
    pLits[0] = toLitCond( Ssw_ObjSatNum(p->pMSat,pOld), 1 );
    pLits[1] = toLitCond( Ssw_ObjSatNum(p->pMSat,pNew), pOld->fPhase ^ pNew->fPhase );
Alan Mishchenko committed
130 131
    if ( p->iOutputLit > -1 )
        pLits[nLits++] = p->iOutputLit;
Alan Mishchenko committed
132 133 134 135 136
    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
137

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

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

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

Alan Mishchenko committed
204 205 206 207 208 209 210 211 212 213 214 215 216 217 218
    // 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
219
    assert( p->pMSat != NULL );
Alan Mishchenko committed
220 221

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

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

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

        // (A v !B)
Alan Mishchenko committed
246 247
        pLits[0] = toLitCond( Ssw_ObjSatNum(p->pMSat,pOld), 0 );
        pLits[1] = toLitCond( Ssw_ObjSatNum(p->pMSat,pNew), !fComplNew );
Alan Mishchenko committed
248 249 250 251 252 253 254
        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
255
        RetValue = sat_solver_addclause( p->pMSat->pSat, pLits, pLits + 2 );
Alan Mishchenko committed
256 257
        assert( RetValue );

Alan Mishchenko committed
258
        // (!A v B)
Alan Mishchenko committed
259 260
        pLits[0] = toLitCond( Ssw_ObjSatNum(p->pMSat,pOld), 1 );
        pLits[1] = toLitCond( Ssw_ObjSatNum(p->pMSat,pNew), fComplNew);
Alan Mishchenko committed
261 262 263 264 265 266 267
        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
268
        RetValue = sat_solver_addclause( p->pMSat->pSat, pLits, pLits + 2 );
Alan Mishchenko committed
269 270 271 272 273
        assert( RetValue );
    }
    return 1;
}

274 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
/**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
300 301 302 303 304
////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////


305 306
ABC_NAMESPACE_IMPL_END