summaryrefslogtreecommitdiffstats
path: root/src/sat
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2017-12-28 23:05:36 -0800
committerAlan Mishchenko <alanmi@berkeley.edu>2017-12-28 23:05:36 -0800
commit75d334a0df1431e8a5a57a83096dcee9661fd0a6 (patch)
treeca537311c87658d0524402f0303e26bd245f1251 /src/sat
parent7d7ce3ecd03059602f70f26612aabd4a2ec49422 (diff)
downloadabc-75d334a0df1431e8a5a57a83096dcee9661fd0a6.tar.gz
abc-75d334a0df1431e8a5a57a83096dcee9661fd0a6.tar.bz2
abc-75d334a0df1431e8a5a57a83096dcee9661fd0a6.zip
New exact synthesis command 'allexact'.
Diffstat (limited to 'src/sat')
-rw-r--r--src/sat/bmc/bmcMaj3.c2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/sat/bmc/bmcMaj3.c b/src/sat/bmc/bmcMaj3.c
index e35b2e87..8a5b3d16 100644
--- a/src/sat/bmc/bmcMaj3.c
+++ b/src/sat/bmc/bmcMaj3.c
@@ -948,10 +948,12 @@ static void Zyx_ManPrintSolution( Zyx_Man_t * p, int fCompl )
printf( "(" );
for ( k = 0; k < i; k++ )
if ( bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_TopoVar(p, i, k)) )
+ {
if ( k >= 0 && k < p->pPars->nVars )
printf( " %c", 'a'+k );
else
printf( " %02d", k );
+ }
printf( " )\n" );
}
}