Version abc71001

1 files changed, 137 insertions, 0 deletions

diff --git a/src/sat/bsat/satStore.h b/src/sat/bsat/satStore.h
new file mode 100644
index 00000000..346b59df
--- /dev/null
+++ b/src/sat/bsat/satStore.h
@@ -0,0 +1,137 @@
+/**CFile****************************************************************
+
+  FileName    [pr.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Proof recording.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: pr.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __PR_H__
+#define __PR_H__
+
+/*
+    The trace of SAT solving contains the original clause of the problem
+    along with the learned clauses derived during SAT solving.
+    The first line of the resulting file contains 3 numbers instead of 2:
+    c <num_vars> <num_all_clauses> <num_root_clauses>
+*/
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+#ifdef _WIN32
+#define inline __inline // compatible with MS VS 6.0
+#endif
+
+#ifndef PRT
+#define PRT(a,t)  printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC))
+#endif
+
+#define STO_MAX(a,b)  ((a) > (b) ? (a) : (b))
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef unsigned lit;
+
+typedef struct Sto_Cls_t_ Sto_Cls_t;
+struct Sto_Cls_t_
+{
+    Sto_Cls_t *     pNext;        // the next clause
+    Sto_Cls_t *     pNext0;       // the next 0-watch
+    Sto_Cls_t *     pNext1;       // the next 0-watch
+    int             Id;           // the clause ID
+    unsigned        fA     :  1;  // belongs to A
+    unsigned        fRoot  :  1;  // original clause
+    unsigned        fVisit :  1;  // visited clause
+    unsigned        nLits  : 24;  // the number of literals
+    lit             pLits[0];     // literals of this clause
+};
+
+typedef struct Sto_Man_t_ Sto_Man_t;
+struct Sto_Man_t_
+{
+    // general data
+    int             nVars;        // the number of variables
+    int             nRoots;       // the number of root clauses
+    int             nClauses;     // the number of all clauses
+    int             nClausesA;    // the number of clauses of A 
+    Sto_Cls_t *     pHead;        // the head clause
+    Sto_Cls_t *     pTail;        // the tail clause
+    Sto_Cls_t *     pEmpty;       // the empty clause
+    // memory management
+    int             nChunkSize;   // the number of bytes in a chunk
+    int             nChunkUsed;   // the number of bytes used in the last chunk
+    char *          pChunkLast;   // the last memory chunk
+};
+
+// variable/literal conversions (taken from MiniSat)
+static inline lit   toLit    (int v)        { return v + v;  }
+static inline lit   toLitCond(int v, int c) { return v + v + (c != 0); }
+static inline lit   lit_neg  (lit l)        { return l ^ 1;  }
+static inline int   lit_var  (lit l)        { return l >> 1; }
+static inline int   lit_sign (lit l)        { return l & 1;  }
+static inline int   lit_print(lit l)        { return lit_sign(l)? -lit_var(l)-1 : lit_var(l)+1; }
+static inline lit   lit_read (int s)        { return s > 0 ? toLit(s-1) : lit_neg(toLit(-s-1)); }
+static inline int   lit_check(lit l, int n) { return l >= 0 && lit_var(l) < n;                  }
+
+// iterators through the clauses
+#define Sto_ManForEachClause( p, pCls )      for( pCls = p->pHead; pCls; pCls = pCls->pNext )
+#define Sto_ManForEachClauseRoot( p, pCls )  for( pCls = p->pHead; pCls && pCls->fRoot; pCls = pCls->pNext )
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== satStore.c ==========================================================*/
+extern Sto_Man_t *  Sto_ManAlloc();
+extern void         Sto_ManFree( Sto_Man_t * p );
+extern int          Sto_ManAddClause( Sto_Man_t * p, lit * pBeg, lit * pEnd );
+extern int          Sto_ManMemoryReport( Sto_Man_t * p );
+extern void         Sto_ManMarkRoots( Sto_Man_t * p );
+extern void         Sto_ManMarkClausesA( Sto_Man_t * p );
+extern void         Sto_ManDumpClauses( Sto_Man_t * p, char * pFileName );
+extern Sto_Man_t *  Sto_ManLoadClauses( char * pFileName );
+
+/*=== satInter.c ==========================================================*/
+typedef struct Int_Man_t_ Int_Man_t;
+extern Int_Man_t *  Int_ManAlloc( int nVarsAlloc );
+extern void         Int_ManFree( Int_Man_t * p );
+extern int          Int_ManInterpolate( Int_Man_t * p, Sto_Man_t * pCnf, int fVerbose, unsigned ** ppResult );
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+