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/bmcBmcS.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/bmcBmcS.c')
| -rw-r--r-- | src/sat/bmc/bmcBmcS.c | 15 |
1 files changed, 7 insertions, 8 deletions
diff --git a/src/sat/bmc/bmcBmcS.c b/src/sat/bmc/bmcBmcS.c index 1bfcd9d0..ea8ec2f6 100644 --- a/src/sat/bmc/bmcBmcS.c +++ b/src/sat/bmc/bmcBmcS.c @@ -21,7 +21,6 @@ #include "bmc.h" #include "sat/cnf/cnf.h" #include "sat/satoko/satoko.h" -#include "sat/satoko/solver.h" //#define ABC_USE_EXT_SOLVERS 1 @@ -41,8 +40,8 @@ #define bmc_sat_solver_addclause satoko_add_clause #define bmc_sat_solver_addvar(s) satoko_add_variable(s, 0) #define bmc_sat_solver_solve satoko_solve_assumptions - #define bmc_sat_solver_read_cex_varvalue solver_read_cex_varvalue - #define bmc_sat_solver_setstop solver_set_stop + #define bmc_sat_solver_read_cex_varvalue satoko_read_cex_varvalue + #define bmc_sat_solver_setstop satoko_set_stop #endif @@ -546,7 +545,7 @@ Cnf_Dat_t * Bmcs_ManAddNewCnf( Bmcs_Man_t * p, int f, int nFramesAdd ) if ( pNew == NULL ) return NULL; clk = Abc_Clock(); - pCnf = Mf_ManGenerateCnf( pNew, 8, 1, 0, 0, 0 ); + pCnf = (Cnf_Dat_t *) Mf_ManGenerateCnf( pNew, 8, 1, 0, 0, 0 ); pMap = ABC_FALLOC( int, Gia_ManObjNum(pNew) ); pMap[0] = 0; Gia_ManForEachObj1( pNew, pObj, i ) @@ -584,10 +583,10 @@ void Bmcs_ManPrintFrame( Bmcs_Man_t * p, int f, int nClauses, int Solver, abctim return; Abc_Print( 1, "%4d %s : ", f, fUnfinished ? "-" : "+" ); #ifndef ABC_USE_EXT_SOLVERS - Abc_Print( 1, "Var =%8.0f. ", (double)solver_varnum(p->pSats[0]) ); - Abc_Print( 1, "Cla =%9.0f. ", (double)solver_clausenum(p->pSats[0]) ); - Abc_Print( 1, "Learn =%9.0f. ",(double)solver_learntnum(p->pSats[0]) ); - Abc_Print( 1, "Conf =%9.0f. ", (double)solver_conflictnum(p->pSats[0]) ); + Abc_Print( 1, "Var =%8.0f. ", (double)satoko_varnum(p->pSats[0]) ); + Abc_Print( 1, "Cla =%9.0f. ", (double)satoko_clausenum(p->pSats[0]) ); + Abc_Print( 1, "Learn =%9.0f. ",(double)satoko_learntnum(p->pSats[0]) ); + Abc_Print( 1, "Conf =%9.0f. ", (double)satoko_conflictnum(p->pSats[0]) ); #else Abc_Print( 1, "Var =%8.0f. ", (double)p->nSatVars ); Abc_Print( 1, "Cla =%9.0f. ", (double)nClauses ); |