diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-10-17 14:09:41 +0900 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-10-17 14:09:41 +0900 |
| commit | 298ec14efa83fcb435971c2b987afa84f1a9f767 (patch) | |
| tree | 5499b03d641dc4d4a2233fe5ac56eae90564b611 /src | |
| parent | c1b4b79e99a5338eb6aaf895711b37c4e69414a6 (diff) | |
| download | abc-298ec14efa83fcb435971c2b987afa84f1a9f767.tar.gz abc-298ec14efa83fcb435971c2b987afa84f1a9f767.tar.bz2 abc-298ec14efa83fcb435971c2b987afa84f1a9f767.zip | |
Integrating Glucose into &qbf.
Diffstat (limited to 'src')
| -rw-r--r-- | src/aig/gia/giaQbf.c | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/aig/gia/giaQbf.c b/src/aig/gia/giaQbf.c index 5917a3ef..247c3dad 100644 --- a/src/aig/gia/giaQbf.c +++ b/src/aig/gia/giaQbf.c @@ -525,9 +525,9 @@ void Gia_QbfPrint( Qbf_Man_t * p, Vec_Int_t * vValues, int Iter ) printf( "%5d : ", Iter ); assert( Vec_IntSize(vValues) == p->nVars ); Vec_IntPrintBinary( vValues ); printf( " " ); - printf( "Var = %6d ", p->pSatSynG ? bmcg_sat_solver_varnum(p->pSatSynG) : sat_solver_nvars(p->pSatSyn) ); - printf( "Cla = %6d ", p->pSatSynG ? bmcg_sat_solver_clausenum(p->pSatSynG) : sat_solver_nclauses(p->pSatSyn) ); - printf( "Conf = %6d ", p->pSatSynG ? bmcg_sat_solver_conflictnum(p->pSatSynG) : sat_solver_nconflicts(p->pSatSyn) ); + printf( "Var =%7d ", p->pSatSynG ? bmcg_sat_solver_varnum(p->pSatSynG) : sat_solver_nvars(p->pSatSyn) ); + printf( "Cla =%7d ", p->pSatSynG ? bmcg_sat_solver_clausenum(p->pSatSynG) : sat_solver_nclauses(p->pSatSyn) ); + printf( "Conf =%9d ", p->pSatSynG ? bmcg_sat_solver_conflictnum(p->pSatSynG) : sat_solver_nconflicts(p->pSatSyn) ); Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart ); } |