summaryrefslogtreecommitdiffstats
path: root/src/sat/bsat
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2008-02-08 08:01:00 -0800
committerAlan Mishchenko <alanmi@berkeley.edu>2008-02-08 08:01:00 -0800
commitf2d4f6c26eb610cf4843004fc6955a1548aa9f8f (patch)
tree089ca0bde7ecc2bb0acec04aeb28c52ecc18139f /src/sat/bsat
parent5a6924060bffb688101f54711f967305fc3fa480 (diff)
downloadabc-f2d4f6c26eb610cf4843004fc6955a1548aa9f8f.tar.gz
abc-f2d4f6c26eb610cf4843004fc6955a1548aa9f8f.tar.bz2
abc-f2d4f6c26eb610cf4843004fc6955a1548aa9f8f.zip
Version abc80208
Diffstat (limited to 'src/sat/bsat')
-rw-r--r--src/sat/bsat/satInter.c26
-rw-r--r--src/sat/bsat/satStore.h1
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 );