GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/prop/minisat/simp/SimpSolver.h Lines: 21 25 84.0 %
Date: 2021-03-22 Branches: 20 40 50.0 %

Line Exec Source
1
/************************************************************************************[SimpSolver.h]
2
Copyright (c) 2006,      Niklas Een, Niklas Sorensson
3
Copyright (c) 2007-2010, Niklas Sorensson
4
5
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
6
associated documentation files (the "Software"), to deal in the Software without restriction,
7
including without limitation the rights to use, copy, modify, merge, publish, distribute,
8
sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
9
furnished to do so, subject to the following conditions:
10
11
The above copyright notice and this permission notice shall be included in all copies or
12
substantial portions of the Software.
13
14
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
15
NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
16
NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
17
DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
18
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
19
**************************************************************************************************/
20
21
#ifndef Minisat_SimpSolver_h
22
#define Minisat_SimpSolver_h
23
24
#include "base/check.h"
25
#include "cvc4_private.h"
26
#include "proof/clause_id.h"
27
#include "prop/minisat/core/Solver.h"
28
#include "prop/minisat/mtl/Queue.h"
29
30
namespace CVC4 {
31
namespace prop {
32
  class TheoryProxy;
33
}
34
}
35
36
namespace CVC4 {
37
namespace Minisat {
38
39
//=================================================================================================
40
41
class SimpSolver : public Solver {
42
 public:
43
    // Constructor/Destructor:
44
    //
45
  SimpSolver(CVC4::prop::TheoryProxy* proxy,
46
             CVC4::context::Context* context,
47
             CVC4::context::UserContext* userContext,
48
             ProofNodeManager* pnm,
49
             bool enableIncremental = false);
50
  ~SimpSolver();
51
52
  // Problem specification:
53
  //
54
  Var newVar(bool polarity = true,
55
             bool dvar = true,
56
             bool isTheoryAtom = false,
57
             bool preRegister = false,
58
             bool canErase = true);
59
  bool addClause(const vec<Lit>& ps, bool removable, ClauseId& id);
60
  bool addEmptyClause(bool removable);  // Add the empty clause to the solver.
61
  bool addClause(Lit p,
62
                 bool removable,
63
                 ClauseId& id);  // Add a unit clause to the solver.
64
  bool addClause(Lit p,
65
                 Lit q,
66
                 bool removable,
67
                 ClauseId& id);  // Add a binary clause to the solver.
68
  bool addClause(Lit p,
69
                 Lit q,
70
                 Lit r,
71
                 bool removable,
72
                 ClauseId& id);  // Add a ternary clause to the solver.
73
  bool addClause_(vec<Lit>& ps, bool removable, ClauseId& id);
74
  bool substitute(Var v, Lit x);  // Replace all occurrences of v with x (may
75
                                  // cause a contradiction).
76
77
  // Variable mode:
78
  //
79
  void setFrozen(Var v,
80
                 bool b);  // If a variable is frozen it will not be eliminated.
81
  bool isEliminated(Var v) const;
82
83
  // Solving:
84
  //
85
  lbool solve(const vec<Lit>& assumps,
86
              bool do_simp = true,
87
              bool turn_off_simp = false);
88
  lbool solveLimited(const vec<Lit>& assumps,
89
                     bool do_simp = true,
90
                     bool turn_off_simp = false);
91
  lbool solve(bool do_simp = true, bool turn_off_simp = false);
92
  lbool solve(Lit p, bool do_simp = true, bool turn_off_simp = false);
93
  lbool solve(Lit p, Lit q, bool do_simp = true, bool turn_off_simp = false);
94
  lbool solve(
95
      Lit p, Lit q, Lit r, bool do_simp = true, bool turn_off_simp = false);
96
  bool eliminate(bool turn_off_elim = false);  // Perform variable elimination
97
                                               // based simplification.
98
99
  // Memory managment:
100
  //
101
  void garbageCollect() override;
102
103
  // Generate a (possibly simplified) DIMACS file:
104
  //
105
#if 0
106
    void    toDimacs  (const char* file, const vec<Lit>& assumps);
107
    void    toDimacs  (const char* file);
108
    void    toDimacs  (const char* file, Lit p);
109
    void    toDimacs  (const char* file, Lit p, Lit q);
110
    void    toDimacs  (const char* file, Lit p, Lit q, Lit r);
111
#endif
112
113
    // Mode of operation:
114
    //
115
    int     grow;              // Allow a variable elimination step to grow by a number of clauses (default to zero).
116
    int     clause_lim;        // Variables are not eliminated if it produces a resolvent with a length above this limit.
117
                               // -1 means no limit.
118
    int     subsumption_lim;   // Do not check if subsumption against a clause larger than this. -1 means no limit.
119
    double  simp_garbage_frac; // A different limit for when to issue a GC during simplification (Also see 'garbage_frac').
120
121
    bool    use_asymm;         // Shrink clauses by asymmetric branching.
122
    bool    use_rcheck;        // Check if a clause is already implied. Prett costly, and subsumes subsumptions :)
123
    bool    use_elim;          // Perform variable elimination.
124
125
    // Statistics:
126
    //
127
    int     merges;
128
    int     asymm_lits;
129
    int     eliminated_vars;
130
131
 protected:
132
133
    // Helper structures:
134
    //
135
    struct ElimLt {
136
        const vec<int>& n_occ;
137
9027
        explicit ElimLt(const vec<int>& no) : n_occ(no) {}
138
139
        // TODO: are 64-bit operations here noticably bad on 32-bit platforms? Could use a saturating
140
        // 32-bit implementation instead then, but this will have to do for now.
141
13548382
        uint64_t cost  (Var x)        const { return (uint64_t)n_occ[toInt(mkLit(x))] * (uint64_t)n_occ[toInt(~mkLit(x))]; }
142
143
        // old ordering function
144
        // bool operator()(Var x, Var y) const { return cost(x) < cost(y); }
145
146
6774191
        bool operator()(Var x, Var y) const
147
        {
148
6774191
          int c_x = cost(x);
149
6774191
          int c_y = cost(y);
150
6774191
          return c_x < c_y || (c_x == c_y && x < y);
151
        }
152
    };
153
154
    struct ClauseDeleted {
155
        const ClauseAllocator& ca;
156
9027
        explicit ClauseDeleted(const ClauseAllocator& _ca) : ca(_ca) {}
157
2428050
        bool operator()(const CRef& cr) const { return ca[cr].mark() == 1; } };
158
159
    // Solver state:
160
    //
161
    int                 elimorder;
162
    bool                use_simplification;
163
    vec<uint32_t>       elimclauses;
164
    vec<char>           touched;
165
    OccLists<Var, vec<CRef>, ClauseDeleted>
166
                        occurs;
167
    vec<int>            n_occ;
168
    Heap<ElimLt>        elim_heap;
169
    Queue<CRef>         subsumption_queue;
170
    vec<char>           frozen;
171
    vec<char>           eliminated;
172
    int                 bwdsub_assigns;
173
    int                 n_touched;
174
175
    // Temporaries:
176
    //
177
    CRef                bwdsub_tmpunit;
178
179
    // Main internal methods:
180
    //
181
    lbool         solve_                   (bool do_simp = true, bool turn_off_simp = false);
182
    bool          asymm                    (Var v, CRef cr);
183
    bool          asymmVar                 (Var v);
184
    void          updateElimHeap           (Var v);
185
    void          gatherTouchedClauses     ();
186
    bool          merge                    (const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& out_clause);
187
    bool          merge                    (const Clause& _ps, const Clause& _qs, Var v, int& size);
188
    bool          backwardSubsumptionCheck (bool verbose = false);
189
    bool          eliminateVar             (Var v);
190
    void          extendModel              ();
191
192
    void          removeClause             (CRef cr);
193
    bool          strengthenClause         (CRef cr, Lit l);
194
    void          cleanUpClauses           ();
195
    bool          implied                  (const vec<Lit>& c);
196
    void          relocAll                 (ClauseAllocator& to);
197
};
198
199
200
//=================================================================================================
201
// Implementation of inline methods:
202
203
204
2589316
inline bool SimpSolver::isEliminated (Var v) const { return eliminated[v]; }
205
811836
inline void SimpSolver::updateElimHeap(Var v) {
206
811836
  Assert(use_simplification);
207
  // if (!frozen[v] && !isEliminated(v) && value(v) == l_Undef)
208
1623672
  if (elim_heap.inHeap(v)
209
811836
      || (!frozen[v] && !isEliminated(v) && value(v) == l_Undef))
210
691938
    elim_heap.update(v);
211
811836
}
212
213
2031535
inline bool SimpSolver::addClause(const vec<Lit>& ps, bool removable, ClauseId& id)
214
2031535
{ ps.copyTo(add_tmp); return addClause_(add_tmp, removable, id); }
215
inline bool SimpSolver::addEmptyClause(bool removable)    { add_tmp.clear(); ClauseId id=-1; return addClause_(add_tmp, removable, id); }
216
inline bool SimpSolver::addClause    (Lit p, bool removable, ClauseId& id)
217
                                                                             { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, removable, id); }
218
inline bool SimpSolver::addClause    (Lit p, Lit q, bool removable, ClauseId& id)
219
                                                                             { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, removable, id); }
220
inline bool SimpSolver::addClause    (Lit p, Lit q, Lit r, bool removable, ClauseId& id)
221
                                                                             { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, removable, id); }
222
inline void SimpSolver::setFrozen    (Var v, bool b) { frozen[v] = (char)b; if (use_simplification && !b) { updateElimHeap(v); } }
223
224
// the solver can always return unknown due to resource limiting
225
12417
inline lbool SimpSolver::solve        (                     bool do_simp, bool turn_off_simp)  {
226
12417
  budgetOff();
227
12417
  assumptions.clear();
228
12417
  return solve_(do_simp, turn_off_simp);
229
 }
230
231
inline lbool SimpSolver::solve        (Lit p       ,        bool do_simp, bool turn_off_simp)  {
232
  budgetOff();
233
  assumptions.clear();
234
  assumptions.push(p);
235
  return solve_(do_simp, turn_off_simp);
236
 }
237
238
inline lbool SimpSolver::solve        (Lit p, Lit q,        bool do_simp, bool turn_off_simp)  {
239
  budgetOff();
240
  assumptions.clear();
241
  assumptions.push(p);
242
  assumptions.push(q);
243
  return solve_(do_simp, turn_off_simp);
244
 }
245
246
inline lbool SimpSolver::solve        (Lit p, Lit q, Lit r, bool do_simp, bool turn_off_simp)  {
247
  budgetOff();
248
  assumptions.clear();
249
  assumptions.push(p);
250
  assumptions.push(q);
251
  assumptions.push(r);
252
  return solve_(do_simp, turn_off_simp);
253
 }
254
255
 inline lbool SimpSolver::solve(const vec<Lit>& assumps,
256
                                bool do_simp,
257
                                bool turn_off_simp)
258
 {
259
   budgetOff();
260
    assumps.copyTo(assumptions);
261
    return solve_(do_simp, turn_off_simp);
262
 }
263
264
 inline lbool SimpSolver::solveLimited(const vec<Lit>& assumps,
265
                                       bool do_simp,
266
                                       bool turn_off_simp)
267
 {
268
   assumps.copyTo(assumptions);
269
   return solve_(do_simp, turn_off_simp);
270
 }
271
272
 //=================================================================================================
273
} /* CVC4::Minisat namespace */
274
} /* CVC4 namespace */
275
276
#endif