Version abc80208

2 files changed, 27 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 )
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 );