Version abc80717

src/sat/bsat/module.make

@@ -1,6 +1,7 @@
 SRC +=  src/sat/bsat/satMem.c \
     src/sat/bsat/satInter.c \
     src/sat/bsat/satInterA.c \
+    src/sat/bsat/satInterB.c \
     src/sat/bsat/satInterP.c \
     src/sat/bsat/satSolver.c \
     src/sat/bsat/satStore.c \

src/sat/bsat/satInterA.c

@@ -965,6 +965,51 @@ p->timeTotal += clock() - clkTotal;
     
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Inta_ManDeriveClauses( Inta_Man_t * pMan, Sto_Man_t * pCnf, int fClausesA )
+{
+    Aig_Man_t * p;
+    Aig_Obj_t * pMiter, * pSum, * pLit;
+    Sto_Cls_t * pClause;
+    int Var, VarAB, v;
+    p = Aig_ManStart( 10000 );
+    pMiter = Aig_ManConst1(p);
+    Sto_ManForEachClauseRoot( pCnf, pClause )
+    {
+        if ( fClausesA ^ pClause->fA ) // clause of B
+            continue;
+        // clause of A
+        pSum = Aig_ManConst0(p);
+        for ( v = 0; v < (int)pClause->nLits; v++ )
+        {
+            Var = lit_var(pClause->pLits[v]);
+            if ( pMan->pVarTypes[Var] < 0 ) // global var
+            {
+                VarAB = -pMan->pVarTypes[Var]-1;
+                assert( VarAB >= 0 && VarAB < Vec_IntSize(pMan->vVarsAB) );
+                pLit = Aig_NotCond( Aig_IthVar(p, VarAB), lit_sign(pClause->pLits[v]) );
+            }
+            else
+                pLit = Aig_NotCond( Aig_IthVar(p, Vec_IntSize(pMan->vVarsAB)+1+Var), lit_sign(pClause->pLits[v]) );
+            pSum = Aig_Or( p, pSum, pLit );
+        }
+        pMiter = Aig_And( p, pMiter, pSum );
+    }
+    Aig_ObjCreatePo( p, pMiter );
+    return p;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/sat/bsat/satMem.h

@@ -23,7 +23,6 @@
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
 
-//#include "leaks.h"       
 #include <stdio.h>
 #include <stdlib.h>
 #include <string.h>

src/sat/bsat/satStore.h

@@ -135,6 +135,12 @@ extern Inta_Man_t * Inta_ManAlloc();
 extern void         Inta_ManFree( Inta_Man_t * p );
 extern void *       Inta_ManInterpolate( Inta_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, int fVerbose );
 
+/*=== satInterB.c ==========================================================*/
+typedef struct Intb_Man_t_ Intb_Man_t;
+extern Intb_Man_t * Intb_ManAlloc();
+extern void         Intb_ManFree( Intb_Man_t * p );
+extern void *       Intb_ManInterpolate( Intb_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, int fVerbose );
+
 /*=== satInterP.c ==========================================================*/
 typedef struct Intp_Man_t_ Intp_Man_t;
 extern Intp_Man_t * Intp_ManAlloc();

src/sat/fraig/fraigInt.h

@@ -23,7 +23,6 @@
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
 
-//#include "leaks.h"       
 #include <stdio.h>
 #include <stdlib.h>
 #include <string.h>

src/sat/msat/msatInt.h

@@ -25,7 +25,6 @@
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
 
-//#include "leaks.h"       
 #include <stdio.h>
 #include <stdlib.h>
 #include <string.h>