summaryrefslogtreecommitdiffstats
path: root/src/base/abci/abcProve.c
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2015-08-24 19:49:18 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2015-08-24 19:49:18 -0700
commit77d64787e07638ac9e44ee892e4d4db5b52686e1 (patch)
tree18c1b7d3eea9e38c875afc80980352c43baef9e4 /src/base/abci/abcProve.c
parent1fffe8f6f3274e03289a67a0abf9c7aa4028f823 (diff)
downloadabc-77d64787e07638ac9e44ee892e4d4db5b52686e1.tar.gz
abc-77d64787e07638ac9e44ee892e4d4db5b52686e1.tar.bz2
abc-77d64787e07638ac9e44ee892e4d4db5b52686e1.zip
Changes to be able to compile ABC without CUDD.
Diffstat (limited to 'src/base/abci/abcProve.c')
-rw-r--r--src/base/abci/abcProve.c5
1 files changed, 5 insertions, 0 deletions
diff --git a/src/base/abci/abcProve.c b/src/base/abci/abcProve.c
index 909cc46b..4be3a398 100644
--- a/src/base/abci/abcProve.c
+++ b/src/base/abci/abcProve.c
@@ -22,7 +22,10 @@
#include "base/abc/abc.h"
#include "proof/fraig/fraig.h"
+
+#ifdef ABC_USE_CUDD
#include "misc/extra/extraBdd.h"
+#endif
ABC_NAMESPACE_IMPL_START
@@ -189,6 +192,7 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars )
}
// try to prove it using brute force SAT
+#ifdef ABC_USE_CUDD
if ( RetValue < 0 && pParams->fUseBdds )
{
if ( pParams->fVerbose )
@@ -207,6 +211,7 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars )
pNtk = pNtkTemp;
Abc_NtkMiterPrint( pNtk, "BDD building", clk, pParams->fVerbose );
}
+#endif
if ( RetValue < 0 )
{