Skip to content

A
abc
Switch branch/tag
Find file
Normal viewHistoryPermalink
msat.h 9.08 KB
Newer Older
Version abc50729
888e5bed
 
Alan Mishchenko committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 
/**CFile****************************************************************

  FileName    [msat.h]

  PackageName [A C version of SAT solver MINISAT, originally developed 
  in C++ by Niklas Een and Niklas Sorensson, Chalmers University of 
  Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.]

  Synopsis    [External definitions of the solver.]

  Author      [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - January 1, 2004.]

  Revision    [$Id: msat.h,v 1.6 2004/05/12 06:30:20 satrajit Exp $]

***********************************************************************/
Major restructuring of the code.
8014f25f
 
Alan Mishchenko committed
21 22 
#ifndef ABC__sat__msat__msat_h
#define ABC__sat__msat__msat_h
Version abc50729
888e5bed
 
Alan Mishchenko committed
23
initial commit of public abc
6130e39b
 
Alan Mishchenko committed
24
Version abc50729
888e5bed
 
Alan Mishchenko committed
25 26 27 28 29 30 31 32 
////////////////////////////////////////////////////////////////////////
///                          INCLUDES                                ///
////////////////////////////////////////////////////////////////////////

////////////////////////////////////////////////////////////////////////
///                         PARAMETERS                               ///
////////////////////////////////////////////////////////////////////////
initial commit of public abc
6130e39b
 
Alan Mishchenko committed
33 34 35 36 


ABC_NAMESPACE_HEADER_START
Version abc90215
0871bffa
 
Alan Mishchenko committed
37
Version abc50729
888e5bed
 
Alan Mishchenko committed
38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 
////////////////////////////////////////////////////////////////////////
///                    STRUCTURE DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////

typedef struct Msat_Solver_t_      Msat_Solver_t;

// the vector of intergers and of clauses
typedef struct Msat_IntVec_t_      Msat_IntVec_t;
typedef struct Msat_ClauseVec_t_   Msat_ClauseVec_t;
typedef struct Msat_VarHeap_t_     Msat_VarHeap_t;

// the return value of the solver
typedef enum { MSAT_FALSE = -1, MSAT_UNKNOWN = 0, MSAT_TRUE = 1 } Msat_Type_t;

// representation of variables and literals
// the literal (l) is the variable (v) and the sign (s)
// s = 0 the variable is positive
// s = 1 the variable is negative
#define MSAT_VAR2LIT(v,s) (2*(v)+(s)) 
#define MSAT_LITNOT(l)    ((l)^1)
#define MSAT_LITSIGN(l)   ((l)&1)     
#define MSAT_LIT2VAR(l)   ((l)>>1)

////////////////////////////////////////////////////////////////////////
///                       GLOBAL VARIABLES                           ///
////////////////////////////////////////////////////////////////////////

////////////////////////////////////////////////////////////////////////
Version abc80130_2
0c6505a2
 
Alan Mishchenko committed
66 
///                       MACRO DEFINITIONS                          ///
Version abc50729
888e5bed
 
Alan Mishchenko committed
67 68 69 70 71 72 73 
////////////////////////////////////////////////////////////////////////

////////////////////////////////////////////////////////////////////////
///                     FUNCTION DECLARATIONS                        ///
////////////////////////////////////////////////////////////////////////

/*=== satRead.c ============================================================*/
initial commit of public abc
6130e39b
 
Alan Mishchenko committed
74 
extern int              Msat_SolverParseDimacs( FILE * pFile, Msat_Solver_t ** p, int fVerbose );
Version abc50729
888e5bed
 
Alan Mishchenko committed
75 76 
/*=== satSolver.c ===========================================================*/
// adding vars, clauses, simplifying the database, and solving
initial commit of public abc
6130e39b
 
Alan Mishchenko committed
77 78 79 80 
extern int              Msat_SolverAddVar( Msat_Solver_t * p, int Level );
extern int              Msat_SolverAddClause( Msat_Solver_t * p, Msat_IntVec_t * pLits );
extern int              Msat_SolverSimplifyDB( Msat_Solver_t * p );
extern int              Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * pVecAssumps, int nBackTrackLimit, int nTimeLimit );
Version abc50729
888e5bed
 
Alan Mishchenko committed
81 82 83 84 85 86 87 
// printing stats, assignments, and clauses
extern void             Msat_SolverPrintStats( Msat_Solver_t * p );
extern void             Msat_SolverPrintAssignment( Msat_Solver_t * p );
extern void             Msat_SolverPrintClauses( Msat_Solver_t * p );
extern void             Msat_SolverWriteDimacs( Msat_Solver_t * p, char * pFileName );
// access to the solver internal data
extern int              Msat_SolverReadVarNum( Msat_Solver_t * p );
Version abc80130_2
0c6505a2
 
Alan Mishchenko committed
88 
extern int              Msat_SolverReadClauseNum( Msat_Solver_t * p );
Version abc50729
888e5bed
 
Alan Mishchenko committed
89 90 91 92 93 
extern int              Msat_SolverReadVarAllocNum( Msat_Solver_t * p );
extern int *            Msat_SolverReadAssignsArray( Msat_Solver_t * p );
extern int *            Msat_SolverReadModelArray( Msat_Solver_t * p );
extern unsigned         Msat_SolverReadTruth( Msat_Solver_t * p );
extern int              Msat_SolverReadBackTracks( Msat_Solver_t * p );
Version abc80130_2
0c6505a2
 
Alan Mishchenko committed
94 
extern int              Msat_SolverReadInspects( Msat_Solver_t * p );
Version abc50729
888e5bed
 
Alan Mishchenko committed
95 96 97 98 99 100 
extern void             Msat_SolverSetVerbosity( Msat_Solver_t * p, int fVerbose );
extern void             Msat_SolverSetProofWriting( Msat_Solver_t * p, int fProof );
extern void             Msat_SolverSetVarTypeA( Msat_Solver_t * p, int Var );
extern void             Msat_SolverSetVarMap( Msat_Solver_t * p, Msat_IntVec_t * vVarMap );
extern void             Msat_SolverMarkLastClauseTypeA( Msat_Solver_t * p );
extern void             Msat_SolverMarkClausesStart( Msat_Solver_t * p );
Version abc80130_2
0c6505a2
 
Alan Mishchenko committed
101 
extern float *          Msat_SolverReadFactors( Msat_Solver_t * p );
Version abc50729
888e5bed
 
Alan Mishchenko committed
102 103 104 105 106 107 108 109 110 111 112 
// returns the solution after incremental solving
extern int              Msat_SolverReadSolutions( Msat_Solver_t * p );
extern int *            Msat_SolverReadSolutionsArray( Msat_Solver_t * p );
extern Msat_ClauseVec_t *  Msat_SolverReadAdjacents( Msat_Solver_t * p );
extern Msat_IntVec_t *  Msat_SolverReadConeVars( Msat_Solver_t * p );
extern Msat_IntVec_t *  Msat_SolverReadVarsUsed( Msat_Solver_t * p );
/*=== satSolverSearch.c ===========================================================*/
extern void             Msat_SolverRemoveLearned( Msat_Solver_t * p );
extern void             Msat_SolverRemoveMarked( Msat_Solver_t * p );
/*=== satSolverApi.c ===========================================================*/
// allocation, cleaning, and freeing the solver
initial commit of public abc
6130e39b
 
Alan Mishchenko committed
113 
extern Msat_Solver_t *  Msat_SolverAlloc( int nVars, double dClaInc, double dClaDecay, double dVarInc, double dVarDecay, int fVerbose );
Version abc50729
888e5bed
 
Alan Mishchenko committed
114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 
extern void             Msat_SolverResize( Msat_Solver_t * pMan, int nVarsAlloc );
extern void             Msat_SolverClean( Msat_Solver_t * p, int nVars );
extern void             Msat_SolverPrepare( Msat_Solver_t * pSat, Msat_IntVec_t * vVars );
extern void             Msat_SolverFree( Msat_Solver_t * p );
/*=== satVec.c ===========================================================*/
extern Msat_IntVec_t *  Msat_IntVecAlloc( int nCap );
extern Msat_IntVec_t *  Msat_IntVecAllocArray( int * pArray, int nSize );
extern Msat_IntVec_t *  Msat_IntVecAllocArrayCopy( int * pArray, int nSize );
extern Msat_IntVec_t *  Msat_IntVecDup( Msat_IntVec_t * pVec );
extern Msat_IntVec_t *  Msat_IntVecDupArray( Msat_IntVec_t * pVec );
extern void             Msat_IntVecFree( Msat_IntVec_t * p );
extern void             Msat_IntVecFill( Msat_IntVec_t * p, int nSize, int Entry );
extern int *            Msat_IntVecReleaseArray( Msat_IntVec_t * p );
extern int *            Msat_IntVecReadArray( Msat_IntVec_t * p );
extern int              Msat_IntVecReadSize( Msat_IntVec_t * p );
extern int              Msat_IntVecReadEntry( Msat_IntVec_t * p, int i );
extern int              Msat_IntVecReadEntryLast( Msat_IntVec_t * p );
extern void             Msat_IntVecWriteEntry( Msat_IntVec_t * p, int i, int Entry );
extern void             Msat_IntVecGrow( Msat_IntVec_t * p, int nCapMin );
extern void             Msat_IntVecShrink( Msat_IntVec_t * p, int nSizeNew );
extern void             Msat_IntVecClear( Msat_IntVec_t * p );
extern void             Msat_IntVecPush( Msat_IntVec_t * p, int Entry );
extern int              Msat_IntVecPushUnique( Msat_IntVec_t * p, int Entry );
extern void             Msat_IntVecPushUniqueOrder( Msat_IntVec_t * p, int Entry, int fIncrease );
extern int              Msat_IntVecPop( Msat_IntVec_t * p );
extern void             Msat_IntVecSort( Msat_IntVec_t * p, int fReverse );
/*=== satHeap.c ===========================================================*/
extern Msat_VarHeap_t * Msat_VarHeapAlloc();
extern void             Msat_VarHeapSetActivity( Msat_VarHeap_t * p, double * pActivity );
extern void             Msat_VarHeapStart( Msat_VarHeap_t * p, int * pVars, int nVars, int nVarsAlloc );
extern void             Msat_VarHeapGrow( Msat_VarHeap_t * p, int nSize );
extern void             Msat_VarHeapStop( Msat_VarHeap_t * p );
extern void             Msat_VarHeapPrint( FILE * pFile, Msat_VarHeap_t * p );
extern void             Msat_VarHeapCheck( Msat_VarHeap_t * p );
extern void             Msat_VarHeapCheckOne( Msat_VarHeap_t * p, int iVar );
extern int              Msat_VarHeapContainsVar( Msat_VarHeap_t * p, int iVar );
extern void             Msat_VarHeapInsert( Msat_VarHeap_t * p, int iVar );  
extern void             Msat_VarHeapUpdate( Msat_VarHeap_t * p, int iVar );  
extern void             Msat_VarHeapDelete( Msat_VarHeap_t * p, int iVar );  
extern double           Msat_VarHeapReadMaxWeight( Msat_VarHeap_t * p );
extern int              Msat_VarHeapCountNodes( Msat_VarHeap_t * p, double WeightLimit );  
extern int              Msat_VarHeapReadMax( Msat_VarHeap_t * p );  
extern int              Msat_VarHeapGetMax( Msat_VarHeap_t * p );
Version abc80130_2
0c6505a2
 
Alan Mishchenko committed
157
initial commit of public abc
6130e39b
 
Alan Mishchenko committed
158 159 160 161 162 


ABC_NAMESPACE_HEADER_END
Version abc80130_2
0c6505a2
 
Alan Mishchenko committed
163 164 

#endif
Version abc50729
888e5bed
 
Alan Mishchenko committed
165 166 167 168 

////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////