src/opt/res/resSat.c File Reference

#include "abc.h"
#include "resInt.h"
#include "hop.h"
#include "satSolver.h"
Include dependency graph for resSat.c:

Go to the source code of this file.

Functions

int Res_SatAddConst1 (sat_solver *pSat, int iVar, int fCompl)
int Res_SatAddEqual (sat_solver *pSat, int iVar0, int iVar1, int fCompl)
int Res_SatAddAnd (sat_solver *pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1)
void * Res_SatProveUnsat (Abc_Ntk_t *pAig, Vec_Ptr_t *vFanins)
void * Res_SatSimulateConstr (Abc_Ntk_t *pAig, int fOnSet)
int Res_SatSimulate (Res_Sim_t *p, int nPatsLimit, int fOnSet)

Function Documentation

int Res_SatAddAnd ( sat_solver *  pSat,
int  iVar,
int  iVar0,
int  iVar1,
int  fCompl0,
int  fCompl1 
)

Function*************************************************************

Synopsis [Adds constraints for the two-input AND-gate.]

Description []

SideEffects []

SeeAlso []

Definition at line 380 of file resSat.c.

00381 {
00382     lit Lits[3];
00383 
00384     Lits[0] = toLitCond( iVar, 1 );
00385     Lits[1] = toLitCond( iVar0, fCompl0 );
00386     if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
00387         return 0;
00388 
00389     Lits[0] = toLitCond( iVar, 1 );
00390     Lits[1] = toLitCond( iVar1, fCompl1 );
00391     if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
00392         return 0;
00393 
00394     Lits[0] = toLitCond( iVar, 0 );
00395     Lits[1] = toLitCond( iVar0, !fCompl0 );
00396     Lits[2] = toLitCond( iVar1, !fCompl1 );
00397     if ( !sat_solver_addclause( pSat, Lits, Lits + 3 ) )
00398         return 0;
00399 
00400     return 1;
00401 }

int Res_SatAddConst1 ( sat_solver *  pSat,
int  iVar,
int  fCompl 
)

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

FileName [resSat.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Resynthesis package.]

Synopsis [Interface with the SAT solver.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - January 15, 2007.]

Revision [

Id
resSat.c,v 1.00 2007/01/15 00:00:00 alanmi Exp

] DECLARATIONS ///

Function*************************************************************

Synopsis [Asserts equality of the variable to a constant.]

Description []

SideEffects []

SeeAlso []

Definition at line 333 of file resSat.c.

00334 {
00335     lit Lit = toLitCond( iVar, fCompl );
00336     if ( !sat_solver_addclause( pSat, &Lit, &Lit + 1 ) )
00337         return 0;
00338     return 1;
00339 }

int Res_SatAddEqual ( sat_solver *  pSat,
int  iVar0,
int  iVar1,
int  fCompl 
)

Function*************************************************************

Synopsis [Asserts equality of two variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 352 of file resSat.c.

00353 {
00354     lit Lits[2];
00355 
00356     Lits[0] = toLitCond( iVar0, 0 );
00357     Lits[1] = toLitCond( iVar1, !fCompl );
00358     if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
00359         return 0;
00360 
00361     Lits[0] = toLitCond( iVar0, 1 );
00362     Lits[1] = toLitCond( iVar1, fCompl );
00363     if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
00364         return 0;
00365 
00366     return 1;
00367 }

void* Res_SatProveUnsat ( Abc_Ntk_t *  pAig,
Vec_Ptr_t *  vFanins 
)

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

Synopsis [Loads AIG into the SAT solver for checking resubstitution.]

Description []

SideEffects []

SeeAlso []

Definition at line 49 of file resSat.c.

00050 {
00051     void * pCnf = NULL;
00052     sat_solver * pSat;
00053     Vec_Ptr_t * vNodes;
00054     Abc_Obj_t * pObj;
00055     int i, nNodes, status;
00056 
00057     // make sure fanins contain POs of the AIG
00058     pObj = Vec_PtrEntry( vFanins, 0 );
00059     assert( pObj->pNtk == pAig && Abc_ObjIsPo(pObj) );
00060 
00061     // collect reachable nodes
00062     vNodes = Abc_NtkDfsNodes( pAig, (Abc_Obj_t **)vFanins->pArray, vFanins->nSize );
00063 
00064     // assign unique numbers to each node
00065     nNodes = 0;
00066     Abc_AigConst1(pAig)->pCopy = (void *)nNodes++;
00067     Abc_NtkForEachPi( pAig, pObj, i )
00068         pObj->pCopy = (void *)nNodes++;
00069     Vec_PtrForEachEntry( vNodes, pObj, i )
00070         pObj->pCopy = (void *)nNodes++;
00071     Vec_PtrForEachEntry( vFanins, pObj, i ) // useful POs
00072         pObj->pCopy = (void *)nNodes++;
00073 
00074     // start the solver
00075     pSat = sat_solver_new();
00076     sat_solver_store_alloc( pSat );
00077 
00078     // add clause for the constant node
00079     Res_SatAddConst1( pSat, (int)Abc_AigConst1(pAig)->pCopy, 0 );
00080     // add clauses for AND gates
00081     Vec_PtrForEachEntry( vNodes, pObj, i )
00082         Res_SatAddAnd( pSat, (int)pObj->pCopy, 
00083             (int)Abc_ObjFanin0(pObj)->pCopy, (int)Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
00084     Vec_PtrFree( vNodes );
00085     // add clauses for POs
00086     Vec_PtrForEachEntry( vFanins, pObj, i )
00087         Res_SatAddEqual( pSat, (int)pObj->pCopy, 
00088             (int)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );
00089     // add trivial clauses
00090     pObj = Vec_PtrEntry(vFanins, 0);
00091     Res_SatAddConst1( pSat, (int)pObj->pCopy, 0 ); // care-set
00092     pObj = Vec_PtrEntry(vFanins, 1);
00093     Res_SatAddConst1( pSat, (int)pObj->pCopy, 0 ); // on-set
00094 
00095     // bookmark the clauses of A
00096     sat_solver_store_mark_clauses_a( pSat );
00097 
00098     // duplicate the clauses
00099     pObj = Vec_PtrEntry(vFanins, 1);
00100     Sat_SolverDoubleClauses( pSat, (int)pObj->pCopy );
00101     // add the equality constraints
00102     Vec_PtrForEachEntryStart( vFanins, pObj, i, 2 )
00103         Res_SatAddEqual( pSat, (int)pObj->pCopy, ((int)pObj->pCopy) + nNodes, 0 );
00104 
00105     // bookmark the roots
00106     sat_solver_store_mark_roots( pSat );
00107 
00108     // solve the problem
00109     status = sat_solver_solve( pSat, NULL, NULL, (sint64)10000, (sint64)0, (sint64)0, (sint64)0 );
00110     if ( status == l_False )
00111     {
00112         pCnf = sat_solver_store_release( pSat );
00113 //        printf( "unsat\n" );
00114     }
00115     else if ( status == l_True )
00116     {
00117 //        printf( "sat\n" );
00118     }
00119     else
00120     {
00121 //        printf( "undef\n" );
00122     }
00123     sat_solver_delete( pSat );
00124     return pCnf;
00125 }

int Res_SatSimulate ( Res_Sim_t *  p,
int  nPatsLimit,
int  fOnSet 
)

Function*************************************************************

Synopsis [Loads AIG into the SAT solver for constrained simulation.]

Description [Returns 1 if the required number of patterns are found. Returns 0 if the solver ran out of time or proved a constant. In the latter, case one of the flags, fConst0 or fConst1, are set to 1.]

SideEffects []

SeeAlso []

Definition at line 209 of file resSat.c.

00210 {
00211     Vec_Int_t * vLits;
00212     Vec_Ptr_t * vPats;
00213     sat_solver * pSat;
00214     int RetValue, i, k, value, status, Lit, Var, iPat;
00215     int clk = clock();
00216 
00217 //printf( "Looking for %s:  ", fOnSet? "onset " : "offset" );
00218 
00219     // decide what problem should be solved
00220     Lit = toLitCond( (int)Abc_NtkPo(p->pAig,1)->pCopy, !fOnSet );
00221     if ( fOnSet )
00222     {
00223         iPat = p->nPats1;
00224         vPats = p->vPats1;
00225     }
00226     else
00227     {
00228         iPat = p->nPats0;
00229         vPats = p->vPats0;
00230     }
00231     assert( iPat < nPatsLimit );
00232 
00233     // derive the SAT solver
00234     pSat = Res_SatSimulateConstr( p->pAig, fOnSet );
00235     pSat->fSkipSimplify = 1;
00236     status = sat_solver_simplify( pSat );
00237     if ( status == 0 )
00238     {
00239         if ( iPat == 0 )
00240         {
00241 //            if ( fOnSet )
00242 //                p->fConst0 = 1;
00243 //            else
00244 //                p->fConst1 = 1;
00245             RetValue = 0;
00246         }
00247         goto finish;
00248     }
00249  
00250     // enumerate through the SAT assignments
00251     RetValue = 1;
00252     vLits = Vec_IntAlloc( 32 );
00253     for ( k = iPat; k < nPatsLimit; k++ )
00254     {
00255         // solve with the assumption
00256 //        status = sat_solver_solve( pSat, &Lit, &Lit + 1, (sint64)10000, (sint64)0, (sint64)0, (sint64)0 );
00257         status = sat_solver_solve( pSat, NULL, NULL, (sint64)10000, (sint64)0, (sint64)0, (sint64)0 );
00258         if ( status == l_False )
00259         {
00260 //printf( "Const %d\n", !fOnSet );
00261             if ( k == 0 )
00262             {
00263                 if ( fOnSet )
00264                     p->fConst0 = 1;
00265                 else
00266                     p->fConst1 = 1;
00267                 RetValue = 0;
00268             }
00269             break;
00270         }
00271         else if ( status == l_True )
00272         {
00273             // save the pattern
00274             Vec_IntClear( vLits );
00275             for ( i = 0; i < p->nTruePis; i++ )
00276             {
00277                 Var = (int)Abc_NtkPi(p->pAig,i)->pCopy;
00278                 value = (int)(pSat->model.ptr[Var] == l_True);
00279                 if ( value )
00280                     Abc_InfoSetBit( Vec_PtrEntry(vPats, i), k );
00281                 Lit = toLitCond( Var, value );
00282                 Vec_IntPush( vLits, Lit );
00283 //                printf( "%d", value );
00284             }
00285 //            printf( "\n" );
00286 
00287             status = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
00288             if ( status == 0 )
00289             {
00290                 k++;
00291                 RetValue = 1; 
00292                 break;
00293             }
00294         }
00295         else
00296         {
00297 //printf( "Undecided\n" );
00298             if ( k == 0 )
00299                 RetValue = 0;
00300             else
00301                 RetValue = 1; 
00302             break;
00303         }
00304     }
00305     Vec_IntFree( vLits );
00306 //printf( "Found %d patterns\n", k - iPat );
00307 
00308     // set the new number of patterns
00309     if ( fOnSet )
00310         p->nPats1 = k;
00311     else
00312         p->nPats0 = k;
00313 
00314 finish:
00315 
00316     sat_solver_delete( pSat );
00317 p->timeSat += clock() - clk;
00318     return RetValue;
00319 }

void* Res_SatSimulateConstr ( Abc_Ntk_t *  pAig,
int  fOnSet 
)

Function*************************************************************

Synopsis [Loads AIG into the SAT solver for constrained simulation.]

Description []

SideEffects []

SeeAlso []

Definition at line 138 of file resSat.c.

00139 {
00140     sat_solver * pSat;
00141     Vec_Ptr_t * vFanins;
00142     Vec_Ptr_t * vNodes;
00143     Abc_Obj_t * pObj;
00144     int i, nNodes;
00145 
00146     // start the array
00147     vFanins = Vec_PtrAlloc( 2 );
00148     pObj = Abc_NtkPo( pAig, 0 );
00149     Vec_PtrPush( vFanins, pObj );
00150     pObj = Abc_NtkPo( pAig, 1 );
00151     Vec_PtrPush( vFanins, pObj );
00152 
00153     // collect reachable nodes
00154     vNodes = Abc_NtkDfsNodes( pAig, (Abc_Obj_t **)vFanins->pArray, vFanins->nSize );
00155 
00156     // assign unique numbers to each node
00157     nNodes = 0;
00158     Abc_AigConst1(pAig)->pCopy = (void *)nNodes++;
00159     Abc_NtkForEachPi( pAig, pObj, i )
00160         pObj->pCopy = (void *)nNodes++;
00161     Vec_PtrForEachEntry( vNodes, pObj, i )
00162         pObj->pCopy = (void *)nNodes++;
00163     Vec_PtrForEachEntry( vFanins, pObj, i ) // useful POs
00164         pObj->pCopy = (void *)nNodes++;
00165 
00166     // start the solver
00167     pSat = sat_solver_new();
00168 
00169     // add clause for the constant node
00170     Res_SatAddConst1( pSat, (int)Abc_AigConst1(pAig)->pCopy, 0 );
00171     // add clauses for AND gates
00172     Vec_PtrForEachEntry( vNodes, pObj, i )
00173         Res_SatAddAnd( pSat, (int)pObj->pCopy, 
00174             (int)Abc_ObjFanin0(pObj)->pCopy, (int)Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
00175     Vec_PtrFree( vNodes );
00176     // add clauses for the first PO
00177     pObj = Abc_NtkPo( pAig, 0 );
00178     Res_SatAddEqual( pSat, (int)pObj->pCopy, 
00179         (int)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );
00180     // add clauses for the second PO
00181     pObj = Abc_NtkPo( pAig, 1 );
00182     Res_SatAddEqual( pSat, (int)pObj->pCopy, 
00183         (int)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );
00184 
00185     // add trivial clauses
00186     pObj = Abc_NtkPo( pAig, 0 );
00187     Res_SatAddConst1( pSat, (int)pObj->pCopy, 0 ); // care-set
00188 
00189     pObj = Abc_NtkPo( pAig, 1 );
00190     Res_SatAddConst1( pSat, (int)pObj->pCopy, !fOnSet ); // on-set
00191 
00192     Vec_PtrFree( vFanins );
00193     return pSat;
00194 }

Generated on Tue Jan 5 12:19:31 2010 for abc70930 by  doxygen 1.6.1