diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-04-11 21:06:42 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-04-11 21:06:42 -0700 |
| commit | 79584f5e201e7388e30df39e6f8fc9b50f34b834 (patch) | |
| tree | fda0c4dc03cad3179d87427f6b7baf64b27f1d0f /src/proof/cec/cecSynth.c | |
| parent | 0d53eece0a8243995215f7fefc39371d07c8d959 (diff) | |
| download | abc-79584f5e201e7388e30df39e6f8fc9b50f34b834.tar.gz abc-79584f5e201e7388e30df39e6f8fc9b50f34b834.tar.bz2 abc-79584f5e201e7388e30df39e6f8fc9b50f34b834.zip | |
Experiments with SAT sweeping.
Diffstat (limited to 'src/proof/cec/cecSynth.c')
| -rw-r--r-- | src/proof/cec/cecSynth.c | 52 |
1 files changed, 52 insertions, 0 deletions
diff --git a/src/proof/cec/cecSynth.c b/src/proof/cec/cecSynth.c index c00723bc..6e5fd221 100644 --- a/src/proof/cec/cecSynth.c +++ b/src/proof/cec/cecSynth.c @@ -372,6 +372,58 @@ int Cec_SequentialSynthesisPart( Gia_Man_t * p, Cec_ParSeq_t * pPars ) return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Gia_ManTestOnePair_rec( sat_solver * pSat, Gia_Man_t * p, int iObj, Vec_Int_t * vSatVar ) +{ + Gia_Obj_t * pObj; + int iVar, iVar0, iVar1; + if ( Vec_IntEntry(vSatVar, iObj) >= 0 ) + return Vec_IntEntry(vSatVar, iObj); + iVar = sat_solver_addvar(pSat); + Vec_IntWriteEntry( vSatVar, iObj, iVar ); + pObj = Gia_ManObj( p, iObj ); + if ( Gia_ObjIsAnd(pObj) ) + { + iVar0 = Gia_ManTestOnePair_rec( pSat, p, Gia_ObjFaninId0(pObj, iObj), vSatVar ); + iVar1 = Gia_ManTestOnePair_rec( pSat, p, Gia_ObjFaninId1(pObj, iObj), vSatVar ); + sat_solver_add_and( pSat, iVar, iVar0, iVar1, Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 ); + } + return iVar; +} +int Gia_ManTestOnePair( Gia_Man_t * p, int iObj1, int iObj2, int fPhase ) +{ + int Lits[2] = {1}, status; + sat_solver * pSat = sat_solver_new(); + Vec_Int_t * vSatVar = Vec_IntStartFull( Gia_ManObjNum(p) ); + Vec_IntWriteEntry( vSatVar, 0, sat_solver_addvar(pSat) ); + sat_solver_addclause( pSat, Lits, Lits + 1 ); + Gia_ManTestOnePair_rec( pSat, p, iObj1, vSatVar ); + Gia_ManTestOnePair_rec( pSat, p, iObj2, vSatVar ); + Lits[0] = Abc_Var2Lit( Vec_IntEntry(vSatVar, iObj1), 1 ); + Lits[1] = Abc_Var2Lit( Vec_IntEntry(vSatVar, iObj2), fPhase ); + status = sat_solver_solve( pSat, Lits, Lits + 2, 0, 0, 0, 0 ); + if ( status == l_False ) + { + Lits[0] = Abc_LitNot( Lits[0] ); + Lits[1] = Abc_LitNot( Lits[1] ); + status = sat_solver_solve( pSat, Lits, Lits + 2, 0, 0, 0, 0 ); + } + Vec_IntFree( vSatVar ); + sat_solver_delete( pSat ); + return status; +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// |