From 457e243e588e7ed5f39251784335e254a0c9e711 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 22 Dec 2005 08:01:00 -0800 Subject: Version abc51222 --- src/sat/fraig/fraigMan.c | 3 ++- src/sat/fraig/fraigSat.c | 20 ++++++++++++++++++++ 2 files changed, 22 insertions(+), 1 deletion(-) (limited to 'src/sat/fraig') 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 ); } -- cgit v1.2.3