summaryrefslogtreecommitdiffstats
path: root/src/sat/bsat/satSolver2.h
blob: 2725c92bab2b10f78c730608966d369e3bf0c916 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
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
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
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
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
/**************************************************************************************************
MiniSat -- Copyright (c) 2005, Niklas Sorensson
http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/

Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
associated documentation files (the "Software"), to deal in the Software without restriction,
including without limitation the rights to use, copy, modify, merge, publish, distribute,
sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:

The above copyright notice and this permission notice shall be included in all copies or
substantial portions of the Software.

THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
**************************************************************************************************/
// Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko

#ifndef satSolver2_h
#define satSolver2_h


#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>

#include "satVec.h"

ABC_NAMESPACE_HEADER_START



//=================================================================================================
// Public interface:

struct sat_solver2_t;
typedef struct sat_solver2_t sat_solver2;

extern sat_solver2* sat_solver2_new(void);
extern void        sat_solver2_delete(sat_solver2* s);

extern int         sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end);
extern int         sat_solver2_simplify(sat_solver2* s);
extern int         sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal);

extern int         sat_solver2_nvars(sat_solver2* s);
extern int         sat_solver2_nclauses(sat_solver2* s);
extern int         sat_solver2_nconflicts(sat_solver2* s);

extern void        sat_solver2_setnvars(sat_solver2* s,int n);

extern void        Sat_Solver2WriteDimacs( sat_solver2 * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars );
extern void        Sat_Solver2PrintStats( FILE * pFile, sat_solver2 * p );
extern int *       Sat_Solver2GetModel( sat_solver2 * p, int * pVars, int nVars );
extern void        Sat_Solver2DoubleClauses( sat_solver2 * p, int iVar );

// trace recording
extern void        sat_solver2TraceStart( sat_solver2 * pSat, char * pName );
extern void        sat_solver2TraceStop( sat_solver2 * pSat );
extern void        sat_solver2TraceWrite( sat_solver2 * pSat, int * pBeg, int * pEnd, int fRoot );

// clause storage
extern void        sat_solver2_store_alloc( sat_solver2 * s );
extern void        sat_solver2_store_write( sat_solver2 * s, char * pFileName );
extern void        sat_solver2_store_free( sat_solver2 * s );
extern void        sat_solver2_store_mark_roots( sat_solver2 * s );
extern void        sat_solver2_store_mark_clauses_a( sat_solver2 * s );
extern void *      sat_solver2_store_release( sat_solver2 * s ); 

//=================================================================================================
// Solver representation:

//struct clause_t;
//typedef struct clause_t clause;

struct varinfo_t;
typedef struct varinfo_t varinfo;

struct sat_solver2_t
{
    int           size;          // nof variables
    int           cap;           // size of varmaps
    int           qhead;         // Head index of queue.
    int           qtail;         // Tail index of queue.

    int           root_level;    // Level of first proper decision.
    int           simpdb_assigns;// Number of top-level assignments at last 'simplifyDB()'.
    int           simpdb_props;  // Number of propagations before next 'simplifyDB()'.
    double        random_seed;
    double        progress_estimate;
    int           verbosity;     // Verbosity level. 0=silent, 1=some progress report, 2=everything
    int           fNotUseRandom; // do not allow random decisions with a fixed probability
//    int           fSkipSimplify; // set to one to skip simplification of the clause database

    // clauses
    int           iLearnt;       // the first learnt clause 
    int           iLast;         // the last learnt clause 
    veci*         wlists;        // watcher lists (for each literal)
    cla*          pWatches;      // watcher lists (for each literal)

    // clause memory
    int *         pMemArray;
    int           nMemAlloc;
    int           nMemSize;

    // activities
    int           var_inc;       // Amount to bump next variable with.
    int           cla_inc;       // Amount to bump next clause with.
    unsigned*     activity;      // A heuristic measurement of the activity of a variable.

    // internal state
    varinfo *     vi;            // variable information
    cla*          reasons;       
    lit*          trail;
    int*          orderpos;      // Index in variable order.

    veci          tagged;        // (contains: var)
    veci          stack;         // (contains: var)
    veci          order;         // Variable order. (heap) (contains: var)
    veci          trail_lim;     // Separator indices for different decision levels in 'trail'. (contains: int)
    veci          temp_clause;   // temporary storage for a CNF clause
    veci          model;         // If problem is solved, this vector contains the model (contains: lbool).
    veci          conf_final;    // If problem is unsatisfiable (possibly under assumptions),
                                 // this vector represent the final conflict clause expressed in the assumptions.
    // statistics
    stats_t       stats;
    ABC_INT64_T   nConfLimit;    // external limit on the number of conflicts
    ABC_INT64_T   nInsLimit;     // external limit on the number of implications
    int           nRuntimeLimit; // external limit on runtime

};

static int sat_solver2_var_value( sat_solver2* s, int v ) 
{
    assert( s->model.ptr != NULL && v < s->size );
    return (int)(s->model.ptr[v] == l_True);
}
static int sat_solver2_var_literal( sat_solver2* s, int v ) 
{
    assert( s->model.ptr != NULL && v < s->size );
    return toLitCond( v, s->model.ptr[v] != l_True );
}
static void sat_solver2_act_var_clear(sat_solver2* s) 
{
    int i;
    for (i = 0; i < s->size; i++)
        s->activity[i] = 0;//.0;
    s->var_inc = 1.0;
}
static void sat_solver2_compress(sat_solver2* s) 
{
    if ( s->qtail != s->qhead )
    {
        int RetValue = sat_solver2_simplify(s);
        assert( RetValue != 0 );
    }
}

static int sat_solver2_final(sat_solver2* s, int ** ppArray)
{
    *ppArray = s->conf_final.ptr;
    return s->conf_final.size;
}

static int sat_solver2_set_runtime_limit(sat_solver2* s, int Limit)
{
    int nRuntimeLimit = s->nRuntimeLimit;
    s->nRuntimeLimit = Limit;
    return nRuntimeLimit;
}

static int sat_solver2_set_random(sat_solver2* s, int fNotUseRandom)
{
    int fNotUseRandomOld = s->fNotUseRandom;
    s->fNotUseRandom = fNotUseRandom;
    return fNotUseRandomOld;
}

ABC_NAMESPACE_HEADER_END

#endif