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/bmcMesh2.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/bmcMesh2.c')
| -rw-r--r-- | src/sat/bmc/bmcMesh2.c | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/src/sat/bmc/bmcMesh2.c b/src/sat/bmc/bmcMesh2.c index e6662d7c..1553e5bb 100644 --- a/src/sat/bmc/bmcMesh2.c +++ b/src/sat/bmc/bmcMesh2.c @@ -20,7 +20,6 @@ #include "bmc.h" //#include "sat/satoko/satoko.h" -//#include "sat/satoko/solver.h" #include "sat/bsat/satSolver.h" ABC_NAMESPACE_IMPL_START @@ -56,8 +55,8 @@ static inline int Bmc_MeshUVar( int Me[102][102], int x, int y ) { return Me[x][ ***********************************************************************/ static inline int Bmc_MeshVarValue2( sat_solver * p, int v ) { -// int value = var_value(p, v) != VAR_UNASSING ? var_value(p, v) : var_polarity(p, v); -// return value == 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 sat_solver_var_value( p, v ); } @@ -370,7 +369,7 @@ void Bmc_MeshTest2( Gia_Man_t * p, int X, int Y, int T, int fVerbose ) } printf( "Satisfying solution found. " ); /* -// iVar = solver_varnum(pSat); +// iVar = satoko_varnum(pSat); iVar = sat_solver_nvars(pSat); for ( i = 0; i < iVar; i++ ) if ( Bmc_MeshVarValue2(pSat, i) ) |