diff options
Diffstat (limited to 'src/sat/bsat/satInterA.c')
| -rw-r--r-- | src/sat/bsat/satInterA.c | 45 |
1 files changed, 45 insertions, 0 deletions
diff --git a/src/sat/bsat/satInterA.c b/src/sat/bsat/satInterA.c index dd884b3c..cc780580 100644 --- a/src/sat/bsat/satInterA.c +++ b/src/sat/bsat/satInterA.c @@ -965,6 +965,51 @@ p->timeTotal += clock() - clkTotal; } + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Inta_ManDeriveClauses( Inta_Man_t * pMan, Sto_Man_t * pCnf, int fClausesA ) +{ + Aig_Man_t * p; + Aig_Obj_t * pMiter, * pSum, * pLit; + Sto_Cls_t * pClause; + int Var, VarAB, v; + p = Aig_ManStart( 10000 ); + pMiter = Aig_ManConst1(p); + Sto_ManForEachClauseRoot( pCnf, pClause ) + { + if ( fClausesA ^ pClause->fA ) // clause of B + continue; + // clause of A + pSum = Aig_ManConst0(p); + for ( v = 0; v < (int)pClause->nLits; v++ ) + { + Var = lit_var(pClause->pLits[v]); + if ( pMan->pVarTypes[Var] < 0 ) // global var + { + VarAB = -pMan->pVarTypes[Var]-1; + assert( VarAB >= 0 && VarAB < Vec_IntSize(pMan->vVarsAB) ); + pLit = Aig_NotCond( Aig_IthVar(p, VarAB), lit_sign(pClause->pLits[v]) ); + } + else + pLit = Aig_NotCond( Aig_IthVar(p, Vec_IntSize(pMan->vVarsAB)+1+Var), lit_sign(pClause->pLits[v]) ); + pSum = Aig_Or( p, pSum, pLit ); + } + pMiter = Aig_And( p, pMiter, pSum ); + } + Aig_ObjCreatePo( p, pMiter ); + return p; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// |