summaryrefslogtreecommitdiffstats
path: root/src/sat/fraig
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2005-12-22 08:01:00 -0800
committerAlan Mishchenko <alanmi@berkeley.edu>2005-12-22 08:01:00 -0800
commit457e243e588e7ed5f39251784335e254a0c9e711 (patch)
tree751d7b416e66e416983760d0b95d79bb24371309 /src/sat/fraig
parent37f19d8dfb17605abab38110beec5fc17413e635 (diff)
downloadabc-457e243e588e7ed5f39251784335e254a0c9e711.tar.gz
abc-457e243e588e7ed5f39251784335e254a0c9e711.tar.bz2
abc-457e243e588e7ed5f39251784335e254a0c9e711.zip
Version abc51222
Diffstat (limited to 'src/sat/fraig')
-rw-r--r--src/sat/fraig/fraigMan.c3
-rw-r--r--src/sat/fraig/fraigSat.c20
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 );
}