summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--abc.rc6
-rw-r--r--src/base/abc/abcDfs.c2
-rw-r--r--src/opt/lpk/lpkCore.c2
-rw-r--r--src/opt/mfs/mfsInter.c11
-rw-r--r--src/opt/mfs/mfsResub.c19
-rw-r--r--src/sat/bsat/satInter.c26
-rw-r--r--src/sat/bsat/satStore.h1
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 );
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-03 09:07:51 +0000