From 298ec14efa83fcb435971c2b987afa84f1a9f767 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 17 Oct 2017 14:09:41 +0900 Subject: Integrating Glucose into &qbf. --- src/aig/gia/giaQbf.c | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'src/aig/gia') 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 ); } -- cgit v1.2.3