summaryrefslogtreecommitdiffstats
path: root/src/aig/fra
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/fra')
-rw-r--r--src/aig/fra/fraCec.c2
-rw-r--r--src/aig/fra/fraInd.c2
-rw-r--r--src/aig/fra/fraSec.c4
3 files changed, 4 insertions, 4 deletions
diff --git a/src/aig/fra/fraCec.c b/src/aig/fra/fraCec.c
index e5940992..9046d574 100644
--- a/src/aig/fra/fraCec.c
+++ b/src/aig/fra/fraCec.c
@@ -55,7 +55,7 @@ int Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fFl
// pCnf = Cnf_DeriveSimple( pMan, Aig_ManPoNum(pMan) );
if ( fFlipBits )
- Cnf_DataTranformPolarity( pCnf );
+ Cnf_DataTranformPolarity( pCnf, 0 );
// convert into SAT solver
pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index 1935bb7f..41f3ac59 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -530,7 +530,7 @@ p->timeTrav += clock() - clk2;
pCnf = Cnf_DeriveSimple( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
else
pCnf = Cnf_Derive( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
-// Cnf_DataTranformPolarity( pCnf );
+// Cnf_DataTranformPolarity( pCnf, 0 );
//Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 );
p->pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 3aafeb18..04adb7e3 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -389,11 +389,11 @@ PRT( "Time", clock() - clkTotal );
clk = clock();
if ( pParSec->fInterpolation && RetValue == -1 && Aig_ManRegNum(pNew) > 0 && Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew) == 1 )
{
- extern int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUseIp, int fCheckInd, int fCheckKstep, int fVerbose, int * pDepth );
+ extern int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fUseOther, int fUseMiniSat, int fCheckInd, int fCheckKstep, int fVerbose, int * pDepth );
int Depth;
pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew);
pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew);
- RetValue = Saig_Interpolate( pNew, 5000, 40, 0, 1, 0, 1, 1, pParSec->fVeryVerbose, &Depth );
+ RetValue = Saig_Interpolate( pNew, 5000, 40, 0, 1, 0, 0, 0, 1, 1, pParSec->fVeryVerbose, &Depth );
if ( pParSec->fVerbose )
{
if ( RetValue == 1 )