Experiments with SAT sweeping.

1 files changed, 117 insertions, 0 deletions

diff --git a/src/aig/gia/giaCSatP.h b/src/aig/gia/giaCSatP.h
new file mode 100644
index 00000000..4182cd14
--- /dev/null
+++ b/src/aig/gia/giaCSatP.h
@@ -0,0 +1,117 @@
+#ifndef ABC__aig__gia__giaCSatP_h
+#define ABC__aig__gia__giaCSatP_h
+
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include "gia.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_HEADER_START
+
+
+typedef struct CbsP_Par_t_ CbsP_Par_t;
+struct CbsP_Par_t_
+{
+    // conflict limits
+    int           nBTLimit;     // limit on the number of conflicts
+    int           nJustLimit;   // limit on the size of justification queue
+    // current parameters
+    int           nBTThis;      // number of conflicts
+    int           nBTThisNc;    // number of conflicts
+    int           nJustThis;    // max size of the frontier
+    int           nBTTotal;     // total number of conflicts
+    int           nJustTotal;   // total size of the frontier
+    // decision heuristics
+    int           fUseHighest;  // use node with the highest ID
+    int           fUseLowest;   // use node with the highest ID
+    int           fUseMaxFF;    // use node with the largest fanin fanout
+    // other
+    int           fVerbose;
+    int           fUseProved;
+
+    // statistics 
+    int           nJscanThis;
+    int           nRscanThis;
+    int           nPropThis;
+    int           maxJscanUndec;
+    int           maxRscanUndec;
+    int           maxPropUndec;
+    int           maxJscanSolved;
+    int           maxRscanSolved;
+    int           maxPropSolved;
+    int nSat, nUnsat, nUndec;
+    long          accJscanSat;
+    long          accJscanUnsat;
+    long          accJscanUndec;
+    long          accRscanSat;
+    long          accRscanUnsat;
+    long          accRscanUndec;
+    long          accPropSat;
+    long          accPropUnsat;
+    long          accPropUndec;
+
+    // other limits 
+    int           nJscanLimit;
+    int           nRscanLimit;
+    int           nPropLimit;
+};
+
+typedef struct CbsP_Que_t_ CbsP_Que_t;
+struct CbsP_Que_t_
+{
+    int           iHead;        // beginning of the queue
+    int           iTail;        // end of the queue
+    int           nSize;        // allocated size
+    Gia_Obj_t **  pData;        // nodes stored in the queue
+};
+ 
+typedef struct CbsP_Man_t_ CbsP_Man_t;
+struct CbsP_Man_t_
+{
+    CbsP_Par_t     Pars;         // parameters
+    Gia_Man_t *   pAig;         // AIG manager
+    CbsP_Que_t     pProp;        // propagation queue
+    CbsP_Que_t     pJust;        // justification queue
+    CbsP_Que_t     pClauses;     // clause queue
+    Gia_Obj_t **  pIter;        // iterator through clause vars
+    Vec_Int_t *   vLevReas;     // levels and decisions
+    Vec_Int_t *   vValue;
+    Vec_Int_t *   vModel;       // satisfying assignment
+    Vec_Ptr_t *   vTemp;        // temporary storage
+    // SAT calls statistics
+    int           nSatUnsat;    // the number of proofs
+    int           nSatSat;      // the number of failure
+    int           nSatUndec;    // the number of timeouts
+    int           nSatTotal;    // the number of calls
+    // conflicts
+    int           nConfUnsat;   // conflicts in unsat problems
+    int           nConfSat;     // conflicts in sat problems
+    int           nConfUndec;   // conflicts in undec problems
+    // runtime stats
+    abctime       timeSatUnsat; // unsat
+    abctime       timeSatSat;   // sat
+    abctime       timeSatUndec; // undecided
+    abctime       timeTotal;    // total runtime
+};
+
+CbsP_Man_t * CbsP_ManAlloc( Gia_Man_t * pGia );
+void CbsP_ManStop( CbsP_Man_t * p );
+void CbsP_ManSatPrintStats( CbsP_Man_t * p );
+void CbsP_PrintRecord( CbsP_Par_t * pPars );
+int CbsP_ManSolve2( CbsP_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 );
+
+#define CBS_UNSAT  1
+#define CBS_SAT    0
+#define CBS_UNDEC -1
+
+ABC_NAMESPACE_HEADER_END
+
+
+#endif