diff options
Diffstat (limited to 'src/aig/gia')
-rw-r--r-- | src/aig/gia/giaAbsVta.c | 112 |
1 files changed, 0 insertions, 112 deletions
diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c index 48e09ae9..7cc00556 100644 --- a/src/aig/gia/giaAbsVta.c +++ b/src/aig/gia/giaAbsVta.c @@ -83,118 +83,6 @@ extern Vec_Int_t * Gia_VtaCollect( Gia_Man_t * p, Vec_Int_t ** pvFraLims, Vec_In /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// -static inline int sat_solver2_add_const( sat_solver2 * pSat, int iVar, int fCompl, int fMark ) -{ - lit Lits[1]; - int Cid; - assert( iVar >= 0 ); - - Lits[0] = toLitCond( iVar, fCompl ); - Cid = sat_solver2_addclause( pSat, Lits, Lits + 1 ); - if ( fMark ) - clause_set_partA( pSat, Cid, 1 ); - return 1; -} -static inline int sat_solver2_add_buffer( sat_solver2 * pSat, int iVarA, int iVarB, int fCompl, int fMark ) -{ - lit Lits[2]; - int Cid; - assert( iVarA >= 0 && iVarB >= 0 ); - - Lits[0] = toLitCond( iVarA, 0 ); - Lits[1] = toLitCond( iVarB, !fCompl ); - Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 ); - if ( fMark ) - clause_set_partA( pSat, Cid, 1 ); - - Lits[0] = toLitCond( iVarA, 1 ); - Lits[1] = toLitCond( iVarB, fCompl ); - Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 ); - if ( fMark ) - clause_set_partA( pSat, Cid, 1 ); - return 2; -} -static inline int sat_solver2_add_and( sat_solver2 * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1, int fMark ) -{ - lit Lits[3]; - int Cid; - - Lits[0] = toLitCond( iVar, 1 ); - Lits[1] = toLitCond( iVar0, fCompl0 ); - Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 ); - if ( fMark ) - clause_set_partA( pSat, Cid, 1 ); - - Lits[0] = toLitCond( iVar, 1 ); - Lits[1] = toLitCond( iVar1, fCompl1 ); - Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 ); - if ( fMark ) - clause_set_partA( pSat, Cid, 1 ); - - Lits[0] = toLitCond( iVar, 0 ); - Lits[1] = toLitCond( iVar0, !fCompl0 ); - Lits[2] = toLitCond( iVar1, !fCompl1 ); - Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 ); - if ( fMark ) - clause_set_partA( pSat, Cid, 1 ); - return 3; -} -static inline int sat_solver2_add_xor( sat_solver2 * pSat, int iVarA, int iVarB, int iVarC, int fCompl, int fMark ) -{ - lit Lits[3]; - int Cid; - assert( iVarA >= 0 && iVarB >= 0 && iVarC >= 0 ); - - Lits[0] = toLitCond( iVarA, !fCompl ); - Lits[1] = toLitCond( iVarB, 1 ); - Lits[2] = toLitCond( iVarC, 1 ); - Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 ); - if ( fMark ) - clause_set_partA( pSat, Cid, 1 ); - - Lits[0] = toLitCond( iVarA, !fCompl ); - Lits[1] = toLitCond( iVarB, 0 ); - Lits[2] = toLitCond( iVarC, 0 ); - Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 ); - if ( fMark ) - clause_set_partA( pSat, Cid, 1 ); - - Lits[0] = toLitCond( iVarA, fCompl ); - Lits[1] = toLitCond( iVarB, 1 ); - Lits[2] = toLitCond( iVarC, 0 ); - Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 ); - if ( fMark ) - clause_set_partA( pSat, Cid, 1 ); - - Lits[0] = toLitCond( iVarA, fCompl ); - Lits[1] = toLitCond( iVarB, 0 ); - Lits[2] = toLitCond( iVarC, 1 ); - Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 ); - if ( fMark ) - clause_set_partA( pSat, Cid, 1 ); - return 4; -} -static inline int sat_solver2_add_constraint( sat_solver2 * pSat, int iVar, int fCompl, int fMark ) -{ - lit Lits[2]; - int Cid; - assert( iVar >= 0 ); - - Lits[0] = toLitCond( iVar, fCompl ); - Lits[1] = toLitCond( iVar+1, 0 ); - Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 ); - if ( fMark ) - clause_set_partA( pSat, Cid, 1 ); - - Lits[0] = toLitCond( iVar, fCompl ); - Lits[1] = toLitCond( iVar+1, 1 ); - Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 ); - if ( fMark ) - clause_set_partA( pSat, Cid, 1 ); - return 2; -} - - /**Function************************************************************* |