diff options
Diffstat (limited to 'src/opt/res/resSat.c')
| -rw-r--r-- | src/opt/res/resSat.c | 150 |
1 files changed, 146 insertions, 4 deletions
diff --git a/src/opt/res/resSat.c b/src/opt/res/resSat.c index 39ca9ad6..770152cf 100644 --- a/src/opt/res/resSat.c +++ b/src/opt/res/resSat.c @@ -21,19 +21,116 @@ #include "abc.h" #include "res.h" #include "hop.h" -//#include "bf.h" +#include "satSolver.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +extern int Res_SatAddConst1( sat_solver * pSat, int iVar ); +extern int Res_SatAddEqual( sat_solver * pSat, int iVar0, int iVar1, int fCompl ); +extern int Res_SatAddAnd( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1 ); + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* - Synopsis [] + Synopsis [Loads AIG into the SAT solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void * Res_SatProveUnsat( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins ) +{ + void * pCnf; + sat_solver * pSat; + Vec_Ptr_t * vNodes; + Abc_Obj_t * pObj; + int i, nNodes, status; + + // make sure the constant node is not involved + assert( Abc_ObjFanoutNum(Abc_AigConst1(pAig)) == 0 ); + + // collect reachable nodes + vNodes = Abc_NtkDfsNodes( pAig, (Abc_Obj_t **)vFanins->pArray, vFanins->nSize ); + // assign unique numbers to each node + nNodes = 0; + Abc_NtkForEachPi( pAig, pObj, i ) + pObj->pCopy = (void *)nNodes++; + Vec_PtrForEachEntry( vNodes, pObj, i ) + pObj->pCopy = (void *)nNodes++; + Vec_PtrForEachEntry( vFanins, pObj, i ) + pObj->pCopy = (void *)nNodes++; + + // start the solver + pSat = sat_solver_new(); + sat_solver_store_alloc( pSat ); + + // add clause for AND gates + Vec_PtrForEachEntry( vNodes, pObj, i ) + Res_SatAddAnd( pSat, (int)pObj->pCopy, + (int)Abc_ObjFanin0(pObj)->pCopy, (int)Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) ); + // add clauses for the POs + Vec_PtrForEachEntry( vFanins, pObj, i ) + Res_SatAddEqual( pSat, (int)pObj->pCopy, + (int)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) ); + // add trivial clauses + pObj = Vec_PtrEntry(vFanins, 0); + Res_SatAddConst1( pSat, (int)pObj->pCopy ); + pObj = Vec_PtrEntry(vFanins, 1); + Res_SatAddConst1( pSat, (int)pObj->pCopy ); + // bookmark the clauses of A + sat_solver_store_mark_clauses_a( pSat ); + // duplicate the clauses + pObj = Vec_PtrEntry(vFanins, 1); + Sat_SolverDoubleClauses( pSat, (int)pObj->pCopy ); + // add the equality clauses + Vec_PtrForEachEntryStart( vFanins, pObj, i, 2 ) + Res_SatAddEqual( pSat, (int)pObj->pCopy, ((int)pObj->pCopy) + nNodes, 0 ); + // bookmark the roots + sat_solver_store_mark_roots( pSat ); + Vec_PtrFree( vNodes ); + + // solve the problem + status = sat_solver_solve( pSat, NULL, NULL, (sint64)10000, (sint64)0, (sint64)0, (sint64)0 ); + if ( status == l_False ) + pCnf = sat_solver_store_release( pSat ); + else if ( status == l_True ) + pCnf = NULL; + else + pCnf = NULL; + sat_solver_delete( pSat ); + return pCnf; +} + +/**Function************************************************************* + + Synopsis [Loads two-input AND-gate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Res_SatAddConst1( sat_solver * pSat, int iVar ) +{ + lit Lit = lit_var(iVar); + if ( !sat_solver_addclause( pSat, &Lit, &Lit + 1 ) ) + return 0; + return 1; +} + +/**Function************************************************************* + + Synopsis [Loads two-input AND-gate.] Description [] @@ -42,11 +139,56 @@ SeeAlso [] ***********************************************************************/ -Hop_Obj_t * Res_SatFindFunction( Hop_Man_t * pMan, Res_Win_t * pWin, Vec_Ptr_t * vFanins, Abc_Ntk_t * pAig ) +int Res_SatAddEqual( sat_solver * pSat, int iVar0, int iVar1, int fCompl ) { - return NULL; + lit Lits[2]; + + Lits[0] = toLitCond( iVar0, 0 ); + Lits[1] = toLitCond( iVar1, !fCompl ); + if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) ) + return 0; + + Lits[0] = toLitCond( iVar0, 1 ); + Lits[1] = toLitCond( iVar1, fCompl ); + if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) ) + return 0; + + return 1; } +/**Function************************************************************* + + Synopsis [Loads two-input AND-gate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Res_SatAddAnd( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1 ) +{ + lit Lits[3]; + + Lits[0] = toLitCond( iVar, 1 ); + Lits[1] = toLitCond( iVar0, fCompl0 ); + if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) ) + return 0; + + Lits[0] = toLitCond( iVar, 1 ); + Lits[1] = toLitCond( iVar1, fCompl1 ); + if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) ) + return 0; + + Lits[0] = toLitCond( iVar, 0 ); + Lits[1] = toLitCond( iVar0, !fCompl0 ); + Lits[2] = toLitCond( iVar1, !fCompl1 ); + if ( !sat_solver_addclause( pSat, Lits, Lits + 3 ) ) + return 0; + + return 1; +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// |