Bug fix related to not properly resizing SAT solver's model array.

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*************************************************************