diff options
author | Bruno Schmitt <bruno@oschmitt.com> | 2017-08-29 09:40:51 +0200 |
---|---|---|
committer | Bruno Schmitt <bruno@oschmitt.com> | 2017-08-29 09:40:51 +0200 |
commit | ba8112ff3a64d527cf6c8a6c0d9385ca27b52c27 (patch) | |
tree | b8575b157b1019275f5f1da040b18d3c36fd6e11 /src/sat/bmc/bmcMesh.c | |
parent | d0f81fcf2952b8a46548c0dd74f95fa1cd0a504f (diff) | |
download | abc-ba8112ff3a64d527cf6c8a6c0d9385ca27b52c27.tar.gz abc-ba8112ff3a64d527cf6c8a6c0d9385ca27b52c27.tar.bz2 abc-ba8112ff3a64d527cf6c8a6c0d9385ca27b52c27.zip |
Fixing bronken C++ build; Satoko internal header, solver.h, should not be used in other packages
Diffstat (limited to 'src/sat/bmc/bmcMesh.c')
-rw-r--r-- | src/sat/bmc/bmcMesh.c | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/src/sat/bmc/bmcMesh.c b/src/sat/bmc/bmcMesh.c index 6da70a1c..ee27496f 100644 --- a/src/sat/bmc/bmcMesh.c +++ b/src/sat/bmc/bmcMesh.c @@ -20,7 +20,6 @@ #include "bmc.h" #include "sat/satoko/satoko.h" -#include "sat/satoko/solver.h" ABC_NAMESPACE_IMPL_START @@ -53,9 +52,9 @@ static inline int Bmc_MeshUVar( int Me[102][102], int x, int y ) { return Me[x][ ***********************************************************************/ static inline int Bmc_MeshVarValue( satoko_t * p, int v ) { -// int value = var_value(p, v) != VAR_UNASSING ? var_value(p, v) : var_polarity(p, v); -// return value == LIT_TRUE; - return var_polarity(p, v) == LIT_TRUE; +// int value = var_value(p, v) != SATOKO_VAR_UNASSING ? var_value(p, v) : satoko_var_polarity(p, v); +// return value == SATOKO_LIT_TRUE; + return satoko_var_polarity(p, v) == SATOKO_LIT_TRUE; } /**Function************************************************************* @@ -360,7 +359,7 @@ void Bmc_MeshTest( Gia_Man_t * p, int X, int Y, int T, int fVerbose ) } printf( "Satisfying solution found. " ); /* - iVar = solver_varnum(pSat); + iVar = satoko_varnum(pSat); for ( i = 0; i < iVar; i++ ) if ( Bmc_MeshVarValue(pSat, i) ) printf( "%d ", i ); |