diff options
Diffstat (limited to 'src/aig/cnf/cnfMan.c')
| -rw-r--r-- | src/aig/cnf/cnfMan.c | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/src/aig/cnf/cnfMan.c b/src/aig/cnf/cnfMan.c index 2ee66916..934aab1c 100644 --- a/src/aig/cnf/cnfMan.c +++ b/src/aig/cnf/cnfMan.c @@ -326,6 +326,30 @@ void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit ) return pSat; } +/**Function************************************************************* + + Synopsis [Adds the OR-clause.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cnf_DataWriteOrClause( void * p, Cnf_Dat_t * pCnf ) +{ + sat_solver * pSat = p; + Aig_Obj_t * pObj; + int i, * pLits; + pLits = ALLOC( int, Aig_ManPoNum(pCnf->pMan) ); + Aig_ManForEachPo( pCnf->pMan, pObj, i ) + pLits[i] = toLitCond( pCnf->pVarNums[pObj->Id], 0 ); + if ( !sat_solver_addclause( pSat, pLits, pLits + Aig_ManPoNum(pCnf->pMan) ) ) + assert( 0 ); + free( pLits ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// |