diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2008-02-08 08:01:00 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2008-02-08 08:01:00 -0800 |
commit | f2d4f6c26eb610cf4843004fc6955a1548aa9f8f (patch) | |
tree | 089ca0bde7ecc2bb0acec04aeb28c52ecc18139f /src/sat/bsat/satInter.c | |
parent | 5a6924060bffb688101f54711f967305fc3fa480 (diff) | |
download | abc-f2d4f6c26eb610cf4843004fc6955a1548aa9f8f.tar.gz abc-f2d4f6c26eb610cf4843004fc6955a1548aa9f8f.tar.bz2 abc-f2d4f6c26eb610cf4843004fc6955a1548aa9f8f.zip |
Version abc80208
Diffstat (limited to 'src/sat/bsat/satInter.c')
-rw-r--r-- | src/sat/bsat/satInter.c | 26 |
1 files changed, 26 insertions, 0 deletions
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 ) |