diff options
Diffstat (limited to 'src/sat/fraig')
| -rw-r--r-- | src/sat/fraig/fraigMan.c | 3 | ||||
| -rw-r--r-- | src/sat/fraig/fraigSat.c | 20 |
2 files changed, 22 insertions, 1 deletions
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 ); } |