diff options
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 ) |