diff options
Diffstat (limited to 'src/sat')
| -rw-r--r-- | src/sat/asat/added.c | 5 | ||||
| -rw-r--r-- | src/sat/csat/csat_apis.c | 2 | ||||
| -rw-r--r-- | src/sat/fraig/fraigMan.c | 3 | ||||
| -rw-r--r-- | src/sat/fraig/fraigSat.c | 20 | ||||
| -rw-r--r-- | src/sat/msat/msatSolverCore.c | 2 |
5 files changed, 29 insertions, 3 deletions
diff --git a/src/sat/asat/added.c b/src/sat/asat/added.c index 99f1fafe..497087fb 100644 --- a/src/sat/asat/added.c +++ b/src/sat/asat/added.c @@ -71,6 +71,11 @@ void Asat_SolverWriteDimacs( solver * p, char * pFileName, lit* assumptionsBegin // start the file pFile = fopen( pFileName, "wb" ); + if ( pFile == NULL ) + { + printf( "Asat_SolverWriteDimacs(): Cannot open the ouput file.\n" ); + return; + } fprintf( pFile, "c CNF generated by ABC on %s\n", Extra_TimeStamp() ); fprintf( pFile, "p cnf %d %d\n", p->size, nClauses ); diff --git a/src/sat/csat/csat_apis.c b/src/sat/csat/csat_apis.c index efc183a3..74503a2b 100644 --- a/src/sat/csat/csat_apis.c +++ b/src/sat/csat/csat_apis.c @@ -188,7 +188,7 @@ int CSAT_AddGate( CSAT_Manager mng, enum GateType type, char * name, int nofi, c case CSAT_BAND: if ( nofi < 1 ) { printf( "CSAT_AddGate: The AND gate \"%s\" no fanins.\n", name ); return 0; } - pSop = Abc_SopCreateAnd( mng->pNtk->pManFunc, nofi ); + pSop = Abc_SopCreateAnd( mng->pNtk->pManFunc, nofi, NULL ); break; case CSAT_BNAND: if ( nofi < 1 ) diff --git a/src/sat/fraig/fraigMan.c b/src/sat/fraig/fraigMan.c index 4801e340..673fcad7 100644 --- a/src/sat/fraig/fraigMan.c +++ b/src/sat/fraig/fraigMan.c @@ -104,7 +104,8 @@ Fraig_Man_t * Fraig_ManCreate( Fraig_Params_t * pParams ) Fraig_Man_t * p; // set the random seed for simulation - srand( 0xFEEDDEAF ); +// srand( 0xFEEDDEAF ); + srand( 0xDEADCAFE ); // set parameters for equivalence checking if ( pParams == NULL ) diff --git a/src/sat/fraig/fraigSat.c b/src/sat/fraig/fraigSat.c index e585e8ab..bc60e4e9 100644 --- a/src/sat/fraig/fraigSat.c +++ b/src/sat/fraig/fraigSat.c @@ -1049,6 +1049,26 @@ void Fraig_SupergateAddClausesMux( Fraig_Man_t * p, Fraig_Node_t * pNode ) Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarF, 1) ); RetValue = Msat_SolverAddClause( p->pSat, p->vProj ); assert( RetValue ); + + // two additional clauses + // t' & e' -> f' + // t & e -> f + + // t + e + f' + // t' + e' + f + + Msat_IntVecClear( p->vProj ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarT, 0^fCompT) ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarE, 0^fCompE) ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarF, 1) ); + RetValue = Msat_SolverAddClause( p->pSat, p->vProj ); + assert( RetValue ); + Msat_IntVecClear( p->vProj ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarT, 1^fCompT) ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarE, 1^fCompE) ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarF, 0) ); + RetValue = Msat_SolverAddClause( p->pSat, p->vProj ); + assert( RetValue ); } diff --git a/src/sat/msat/msatSolverCore.c b/src/sat/msat/msatSolverCore.c index 92311e48..ed228b33 100644 --- a/src/sat/msat/msatSolverCore.c +++ b/src/sat/msat/msatSolverCore.c @@ -176,7 +176,7 @@ bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTra if ( nBackTrackLimit > 0 ) break; // if the runtime limit is exceeded, quit the restart loop - if ( clock() - timeStart >= nTimeLimit * CLOCKS_PER_SEC ) + if ( nTimeLimit > 0 && clock() - timeStart >= nTimeLimit * CLOCKS_PER_SEC ) break; } Msat_SolverCancelUntil( p, 0 ); |