From 5a6924060bffb688101f54711f967305fc3fa480 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Thu, 7 Feb 2008 08:01:00 -0800
Subject: Version abc80207

---
 src/aig/fra/fra.h      | 2 +-
 src/aig/fra/fraClaus.c | 6 ++++--
 src/aig/fra/fraHot.c   | 2 +-
 src/aig/fra/fraInd.c   | 6 ++++--
 4 files changed, 10 insertions(+), 6 deletions(-)

(limited to 'src/aig/fra')

diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index 339fd810..64268358 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -39,7 +39,7 @@ extern "C" {
 #include "aig.h"
 #include "dar.h"
 #include "satSolver.h"
-//#include "bar.h"
+#include "ioa.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
diff --git a/src/aig/fra/fraClaus.c b/src/aig/fra/fraClaus.c
index a35e1169..8e3a03e1 100644
--- a/src/aig/fra/fraClaus.c
+++ b/src/aig/fra/fraClaus.c
@@ -1530,7 +1530,7 @@ void Fra_ClausWriteIndClauses( Clu_Man_t * p )
     extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
     Aig_Man_t * pNew;
     Aig_Obj_t * pClause, * pLiteral;
-    char Buffer[500];
+    char Buffer[500], * pName;
     int * pStart, * pVar2Id; 
     int Beg, End, i, k;
     // create mapping from SAT vars to node IDs
@@ -1561,7 +1561,9 @@ void Fra_ClausWriteIndClauses( Clu_Man_t * p )
     free( pVar2Id );
     Aig_ManCleanup( pNew );
     // write the manager into a file
-    sprintf( Buffer, "%s_care.aig", p->pAig->pName );
+    pName = Ioa_FileNameGeneric(p->pAig->pName);
+    sprintf( Buffer, "%s_care.aig", pName );
+    free( pName );
     printf( "Care clauses are written into file \"%s\".\n", Buffer );
     Ioa_WriteAiger( pNew, Buffer, 0, 1 );
     Aig_ManStop( pNew );
diff --git a/src/aig/fra/fraHot.c b/src/aig/fra/fraHot.c
index 4a3f9b03..8796f827 100644
--- a/src/aig/fra/fraHot.c
+++ b/src/aig/fra/fraHot.c
@@ -130,7 +130,7 @@ int Fra_OneHotNodesAreClause( Fra_Sml_t * pSeq, Aig_Obj_t * pObj1, Aig_Obj_t * p
 ***********************************************************************/
 Vec_Int_t * Fra_OneHotCompute( Fra_Man_t * p, Fra_Sml_t * pSim )
 {
-    int fSkipConstEqu = 1;
+    int fSkipConstEqu = 0;
     Vec_Int_t * vOneHots;
     Aig_Obj_t * pObj1, * pObj2;
     int i, k;
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index 07044b52..ea17706c 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -471,12 +471,14 @@ clk2 = clock();
     if ( p->pPars->fWriteImps && p->vOneHots && Fra_OneHotCount(p, p->vOneHots) )
     {
         extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
-        char Buffer[500];
+        char Buffer[500], * pStart;
         Aig_Man_t * pNew;
         pManAigNew = Aig_ManDup( pManAig, 1 );
 //        pManAigNew->pManExdc = Fra_OneHotCreateExdc( p, p->vOneHots );
         pNew = Fra_OneHotCreateExdc( p, p->vOneHots );
-        sprintf( Buffer, "%s_care.aig", p->pManAig->pName );
+        pStart = Ioa_FileNameGeneric(p->pManAig->pName);
+        sprintf( Buffer, "%s_care.aig", pStart );
+        free( pStart );
         printf( "Care one-hotness clauses are written into file \"%s\".\n", Buffer );
         Ioa_WriteAiger( pNew, Buffer, 0, 1 );
         Aig_ManStop( pNew );
-- 
cgit v1.2.3