Version abc80208

7 files changed, 50 insertions, 17 deletions

diff --git a/abc.rc b/abc.rc
index bbde24c2..22c0a0b7 100644
--- a/abc.rc
+++ b/abc.rc
@@ -24,12 +24,16 @@ set gnuplotunix gnuplot
 alias b balance
 alias cl cleanup
 alias clp collapse
+alias cs care_set
+alias dc2 dcompress2
 alias esd ext_seq_dcs
 alias f fraig
 alias fs fraig_sweep
 alias fsto fraig_store
 alias fres fraig_restore
+alias fr fretime
 alias ft fraig_trust
+alias ic indcut
 alias lp lutpack
 alias pd print_dsd
 alias pex print_exdc -d
@@ -123,6 +127,8 @@ alias trec     "rec_start; r c.blif; st; rec_add; rec_use"
 alias trec4    "rec_start -K 4; r i10.blif; st; rec_add; rec_use"
 alias bmc2     "frames -i -F 10; orpos; iprove"
 
+alias pjsolve  "scl; dc2; fr; dc2; ic; ic -t; if -a; cs tacas/005_care.aig; mfs; lp; st; ic"
+
 alias t0       "r test/mc1.blif; st; test"
 alias t1       "r s27mc2.blif; st; test"
 alias t2       "r i/intel_001.aig; ps; indcut -v"
diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c
index c882672b..fd3b9253 100644
--- a/src/base/abc/abcDfs.c
+++ b/src/base/abc/abcDfs.c
@@ -677,7 +677,7 @@ void Abc_NtkNodeSupport_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
     // mark the node as visited
     Abc_NodeSetTravIdCurrent( pNode );
     // collect the CI
-    if ( Abc_ObjIsCi(pNode) )//|| Abc_ObjFaninNum(pNode) == 0 )
+    if ( Abc_ObjIsCi(pNode) || (Abc_NtkIsStrash(pNode->pNtk) && Abc_ObjFaninNum(pNode) == 0) )
     {
         Vec_PtrPush( vNodes, pNode );
         return;
diff --git a/src/opt/lpk/lpkCore.c b/src/opt/lpk/lpkCore.c
index e819a7fb..34911c20 100644
--- a/src/opt/lpk/lpkCore.c
+++ b/src/opt/lpk/lpkCore.c
@@ -340,7 +340,7 @@ void Lpk_ComputeSupports( Lpk_Man_t * p, Lpk_Cut_t * pCut, unsigned * pTruth )
     pTruthInv = Lpk_CutTruth( p, pCut, 1 );
     RetValue1 = Kit_CreateCloudFromTruth( p->pDsdMan->dd, pTruth, pCut->nLeaves, p->vBddDir );
     RetValue2 = Kit_CreateCloudFromTruth( p->pDsdMan->dd, pTruthInv, pCut->nLeaves, p->vBddInv );
-    if ( RetValue1 && RetValue2 )
+    if ( RetValue1 && RetValue2 && Vec_IntSize(p->vBddDir) > 1 && Vec_IntSize(p->vBddInv) > 1 )
         Kit_TruthCofSupports( p->vBddDir, p->vBddInv, pCut->nLeaves, p->vMemory, p->puSupps ); 
     else
         p->puSupps[0] = p->puSupps[1] = 0;
diff --git a/src/opt/mfs/mfsInter.c b/src/opt/mfs/mfsInter.c
index 16db5061..65acd4eb 100644
--- a/src/opt/mfs/mfsInter.c
+++ b/src/opt/mfs/mfsInter.c
@@ -220,6 +220,7 @@ Hop_Obj_t * Abc_NtkMfsInterplate( Mfs_Man_t * p, int * pCands, int nCands )
     Kit_Graph_t * pGraph;
     Hop_Obj_t * pFunc;
     int nFanins, status;
+    int c, i, * pGloVars;
 
     // derive the SAT solver for interpolation
     pSat = Abc_MfsCreateSolverResub( p, pCands, nCands );
@@ -235,6 +236,16 @@ Hop_Obj_t * Abc_NtkMfsInterplate( Mfs_Man_t * p, int * pCands, int nCands )
     pCnf = sat_solver_store_release( pSat );
     sat_solver_delete( pSat );
 
+    // set the global variables
+    pGloVars = Int_ManSetGlobalVars( p->pMan, nCands );
+    for ( c = 0; c < nCands; c++ )
+    {
+        // get the variable number of this divisor
+        i = lit_var( pCands[c] ) - 2 * p->pCnf->nVars;
+        // get the corresponding SAT variable
+        pGloVars[c] = Vec_IntEntry( p->vProjVars, i );
+    }
+
     // derive the interpolant
     nFanins = Int_ManInterpolate( p->pMan, pCnf, 0, &puTruth );
     Sto_ManFree( pCnf );
diff --git a/src/opt/mfs/mfsResub.c b/src/opt/mfs/mfsResub.c
index 1e9da4d2..4171c111 100644
--- a/src/opt/mfs/mfsResub.c
+++ b/src/opt/mfs/mfsResub.c
@@ -235,12 +235,8 @@ p->timeInt += clock() - clk;
 clk = clock();
             // derive the function
             pFunc = Abc_NtkMfsInterplate( p, pCands, nCands+1 );
-            // shift fanins by 1
-            for ( i = Vec_PtrSize(p->vFanins); i > 0; i-- )
-                p->vFanins->pArray[i] = p->vFanins->pArray[i-1];
-            p->vFanins->nSize++;
-            Vec_PtrWriteEntry( p->vFanins, 0, Vec_PtrEntry(p->vDivs, iVar) );
             // update the network
+            Vec_PtrPush( p->vFanins, Vec_PtrEntry(p->vDivs, iVar) );
             Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc );
 p->timeInt += clock() - clk;
             return 1;
@@ -372,17 +368,10 @@ p->timeInt += clock() - clk;
 clk = clock();
             // derive the function
             pFunc = Abc_NtkMfsInterplate( p, pCands, nCands+2 );
-            // shift fanins by 1
-            for ( i = Vec_PtrSize(p->vFanins); i > 0; i-- )
-                p->vFanins->pArray[i] = p->vFanins->pArray[i-1];
-            p->vFanins->nSize++;
-            // shift fanins by 1
-            for ( i = Vec_PtrSize(p->vFanins); i > 0; i-- )
-                p->vFanins->pArray[i] = p->vFanins->pArray[i-1];
-            p->vFanins->nSize++;
-            Vec_PtrWriteEntry( p->vFanins, 0, Vec_PtrEntry(p->vDivs, iVar2) );
-            Vec_PtrWriteEntry( p->vFanins, 1, Vec_PtrEntry(p->vDivs, iVar) );
             // update the network
+            Vec_PtrPush( p->vFanins, Vec_PtrEntry(p->vDivs, iVar2) );
+            Vec_PtrPush( p->vFanins, Vec_PtrEntry(p->vDivs, iVar) );
+            assert( Vec_PtrSize(p->vFanins) == nCands + 2 );
             Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc );
 p->timeInt += clock() - clk;
             return 1;
diff --git a/src/sat/bsat/satInter.c b/src/sat/bsat/satInter.c
index 8e07e9f6..6dc6db0c 100644
--- a/src/sat/bsat/satInter.c
+++ b/src/sat/bsat/satInter.c
@@ -37,6 +37,8 @@ struct Int_Man_t_
 {
     // clauses of the problems
     Sto_Man_t *     pCnf;         // the set of CNF clauses for A and B
+    int             pGloVars[16]; // global variables
+    int             nGloVars;     // the number of global variables
     // various parameters
     int             fVerbose;     // verbosiness flag
     int             fProofVerif;  // verifies the proof
@@ -116,6 +118,23 @@ Int_Man_t * Int_ManAlloc()
 
 /**Function*************************************************************
 
+  Synopsis    [Allocate proof manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int * Int_ManSetGlobalVars( Int_Man_t * p, int nGloVars )
+{
+    p->nGloVars = nGloVars;
+    return p->pGloVars;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Count common variables in the clauses of A and B.]
 
   Description []
@@ -139,6 +158,13 @@ int Int_ManGlobalVars( Int_Man_t * p )
             p->pVarTypes[lit_var(pClause->pLits[v])] = 1;
     }
 
+    if ( p->nGloVars )
+    {
+        for ( v = 0; v < p->nGloVars; v++ )
+            p->pVarTypes[ p->pGloVars[v] ] = - v - 1;
+        return p->nGloVars;
+    }
+
     // check variables that appear in clauses of B
     nVarsAB = 0;
     Sto_ManForEachClauseRoot( p->pCnf, pClause )
diff --git a/src/sat/bsat/satStore.h b/src/sat/bsat/satStore.h
index b66abc8f..bbd7b28b 100644
--- a/src/sat/bsat/satStore.h
+++ b/src/sat/bsat/satStore.h
@@ -125,6 +125,7 @@ extern Sto_Man_t *  Sto_ManLoadClauses( char * pFileName );
 /*=== satInter.c ==========================================================*/
 typedef struct Int_Man_t_ Int_Man_t;
 extern Int_Man_t *  Int_ManAlloc();
+extern int *        Int_ManSetGlobalVars( Int_Man_t * p, int nGloVars );
 extern void         Int_ManFree( Int_Man_t * p );
 extern int          Int_ManInterpolate( Int_Man_t * p, Sto_Man_t * pCnf, int fVerbose, unsigned ** ppResult );