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/aig/gia | |
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/aig/gia')
-rw-r--r-- | src/aig/gia/giaSatoko.c | 3 | ||||
-rw-r--r-- | src/aig/gia/giaSupp.c | 7 |
2 files changed, 4 insertions, 6 deletions
diff --git a/src/aig/gia/giaSatoko.c b/src/aig/gia/giaSatoko.c index 5e04502d..aaf9daaa 100644 --- a/src/aig/gia/giaSatoko.c +++ b/src/aig/gia/giaSatoko.c @@ -21,7 +21,6 @@ #include "gia.h" #include "sat/cnf/cnf.h" #include "sat/satoko/satoko.h" -#include "sat/satoko/solver.h" ABC_NAMESPACE_IMPL_START @@ -133,7 +132,7 @@ int Gia_ManSatokoCallOne( Gia_Man_t * p, satoko_opts_t * opts, int iOutput ) if ( pSat ) { status = satoko_solve( pSat ); - Cost = (unsigned)pSat->stats.n_conflicts; + Cost = satoko_stats(pSat)->n_conflicts; satoko_destroy( pSat ); } else diff --git a/src/aig/gia/giaSupp.c b/src/aig/gia/giaSupp.c index 589084f9..272c94c6 100644 --- a/src/aig/gia/giaSupp.c +++ b/src/aig/gia/giaSupp.c @@ -20,7 +20,6 @@ #include "gia.h" #include "sat/satoko/satoko.h" -#include "sat/satoko/solver.h" #ifdef ABC_USE_CUDD #include "bdd/extrab/extraBdd.h" @@ -389,7 +388,7 @@ Gia_Man2Min_t * Gia_Man2SuppStart( Gia_Man_t * pGia ) p->vFanins = Vec_PtrAlloc( 100 ); p->vSatVars = Vec_IntAlloc( 100 ); p->iPattern = 1; - p->pSat->opts.learnt_ratio = 0; // prevent garbage collection + satoko_options(p->pSat)->learnt_ratio = 0; // prevent garbage collection return p; } void Gia_Man2SuppStop( Gia_Man2Min_t * p ) @@ -725,7 +724,7 @@ int Gia_Min2ManSolve( Gia_Man2Min_t * p ) // assert( iTemp == -1 ); Vec_IntFillExtra( &p->pGia->vCopies, Gia_ManObjNum(p->pGia), -1 ); Vec_IntClear( p->vSatVars ); - assert( solver_varnum(p->pSat) == 0 ); + assert( satoko_varnum(p->pSat) == 0 ); iVar0 = Gia_Min2ObjGetCnfVar( p, iObj0 ); iVar1 = Gia_Min2ObjGetCnfVar( p, iObj1 ); satoko_assump_push( p->pSat, Abc_Var2Lit(iVar0, Abc_LitIsCompl(p->iLits[0])) ); @@ -739,7 +738,7 @@ int Gia_Min2ManSolve( Gia_Man2Min_t * p ) assert( Gia_Min2ManSimulate(p) == 1 ); for ( n = 0; n < 2; n++ ) Vec_IntForEachEntry( p->vCis[n], iTemp, i ) - Gia_Min2SimSetInputBit( p, iTemp, var_polarity(p->pSat, Gia_Min2ObjSatId(p->pGia, Gia_ManObj(p->pGia, iTemp))) == LIT_TRUE, p->iPattern ); + Gia_Min2SimSetInputBit( p, iTemp, satoko_var_polarity(p->pSat, Gia_Min2ObjSatId(p->pGia, Gia_ManObj(p->pGia, iTemp))) == SATOKO_LIT_TRUE, p->iPattern ); //assert( Gia_Min2ManSimulate(p) == 0 ); p->iPattern = p->iPattern == 63 ? 1 : p->iPattern + 1; p->nSatSat++; |