summaryrefslogtreecommitdiffstats
path: root/src/base/abci/abcMiter.c
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2013-09-02 15:14:49 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2013-09-02 15:14:49 -0700
commit9914c1686802ee507f52856943a22380c1b5d8c8 (patch)
treefaa1995e7d236681d15a204d9251ed243ab5d6ee /src/base/abci/abcMiter.c
parent57b9a9fe130351f609bac0f63b57b7dbcbbc03c8 (diff)
downloadabc-9914c1686802ee507f52856943a22380c1b5d8c8.tar.gz
abc-9914c1686802ee507f52856943a22380c1b5d8c8.tar.bz2
abc-9914c1686802ee507f52856943a22380c1b5d8c8.zip
Adding interpolant computation sat_solver2.
Diffstat (limited to 'src/base/abci/abcMiter.c')
-rw-r--r--src/base/abci/abcMiter.c4
1 files changed, 3 insertions, 1 deletions
diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c
index 8c5a4a83..747fe263 100644
--- a/src/base/abci/abcMiter.c
+++ b/src/base/abci/abcMiter.c
@@ -1148,7 +1148,7 @@ int Abc_NtkDemiter( Abc_Ntk_t * pNtk )
SeeAlso []
***********************************************************************/
-int Abc_NtkCombinePos( Abc_Ntk_t * pNtk, int fAnd )
+int Abc_NtkCombinePos( Abc_Ntk_t * pNtk, int fAnd, int fXor )
{
Abc_Obj_t * pNode, * pMiter;
int i;
@@ -1165,6 +1165,8 @@ int Abc_NtkCombinePos( Abc_Ntk_t * pNtk, int fAnd )
Abc_NtkForEachPo( pNtk, pNode, i )
if ( fAnd )
pMiter = Abc_AigAnd( (Abc_Aig_t *)pNtk->pManFunc, pMiter, Abc_ObjChild0(pNode) );
+ else if ( fXor )
+ pMiter = Abc_AigXor( (Abc_Aig_t *)pNtk->pManFunc, pMiter, Abc_ObjChild0(pNode) );
else
pMiter = Abc_AigOr( (Abc_Aig_t *)pNtk->pManFunc, pMiter, Abc_ObjChild0(pNode) );
// remove the POs and their names