GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/prop/bvminisat/simp/SimpSolver.h Lines: 17 19 89.5 %
Date: 2021-03-22 Branches: 16 34 47.1 %

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 BVMinisat_SimpSolver_h
22
#define BVMinisat_SimpSolver_h
23
24
#include "base/check.h"
25
#include "proof/clause_id.h"
26
#include "prop/bvminisat/core/Solver.h"
27
#include "prop/bvminisat/mtl/Queue.h"
28
29
namespace CVC4 {
30
31
namespace context {
32
class Context;
33
}
34
35
namespace BVMinisat {
36
37
//=================================================================================================
38
39
40
class SimpSolver : public Solver {
41
 public:
42
    // Constructor/Destructor:
43
    //
44
  SimpSolver(CVC4::context::Context* context);
45
  ~SimpSolver();
46
47
  // Problem specification:
48
  //
49
  Var newVar(bool polarity = true, bool dvar = true, bool freeze = false);
50
  bool addClause(const vec<Lit>& ps, ClauseId& id);
51
  bool addEmptyClause();                // Add the empty clause to the solver.
52
  bool addClause(Lit p, ClauseId& id);  // Add a unit clause to the solver.
53
  bool addClause(Lit p,
54
                 Lit q,
55
                 ClauseId& id);  // Add a binary clause to the solver.
56
  bool addClause(Lit p,
57
                 Lit q,
58
                 Lit r,
59
                 ClauseId& id);  // Add a ternary clause to the solver.
60
  bool addClause_(vec<Lit>& ps, ClauseId& id);
61
  bool substitute(Var v, Lit x);  // Replace all occurrences of v with x (may
62
                                  // cause a contradiction).
63
64
  // Variable mode:
65
  //
66
  void setFrozen(Var v,
67
                 bool b);  // If a variable is frozen it will not be eliminated.
68
  bool isEliminated(Var v) const;
69
70
  // Solving:
71
  //
72
  lbool solve(const vec<Lit>& assumps,
73
              bool do_simp = true,
74
              bool turn_off_simp = false);
75
  lbool solveLimited(const vec<Lit>& assumps,
76
                     bool do_simp = true,
77
                     bool turn_off_simp = false);
78
  lbool solveLimited(bool do_simp = true, bool turn_off_simp = false);
79
  lbool solve(bool do_simp = true, bool turn_off_simp = false);
80
  lbool solve(Lit p, bool do_simp = true, bool turn_off_simp = false);
81
  lbool solve(Lit p, Lit q, bool do_simp = true, bool turn_off_simp = false);
82
  lbool solve(
83
      Lit p, Lit q, Lit r, bool do_simp = true, bool turn_off_simp = false);
84
  bool eliminate(bool turn_off_elim = false);  // Perform variable elimination
85
                                               // based simplification.
86
87
  // Memory managment:
88
  //
89
  void garbageCollect() override;
90
91
  // Generate a (possibly simplified) DIMACS file:
92
  //
93
#if 0
94
    void    toDimacs  (const char* file, const vec<Lit>& assumps);
95
    void    toDimacs  (const char* file);
96
    void    toDimacs  (const char* file, Lit p);
97
    void    toDimacs  (const char* file, Lit p, Lit q);
98
    void    toDimacs  (const char* file, Lit p, Lit q, Lit r);
99
#endif
100
101
    // Mode of operation:
102
    //
103
    int     grow;              // Allow a variable elimination step to grow by a number of clauses (default to zero).
104
    int     clause_lim;        // Variables are not eliminated if it produces a resolvent with a length above this limit.
105
                               // -1 means no limit.
106
    int     subsumption_lim;   // Do not check if subsumption against a clause larger than this. -1 means no limit.
107
    double  simp_garbage_frac; // A different limit for when to issue a GC during simplification (Also see 'garbage_frac').
108
109
    bool    use_asymm;         // Shrink clauses by asymmetric branching.
110
    bool    use_rcheck;        // Check if a clause is already implied. Prett costly, and subsumes subsumptions :)
111
    bool    use_elim;          // Perform variable elimination.
112
113
    // Statistics:
114
    //
115
    int     merges;
116
    int     asymm_lits;
117
    int     eliminated_vars;
118
  //    CVC4::TimerStat total_eliminate_time;
119
120
 protected:
121
122
    // Helper structures:
123
    //
124
    struct ElimLt {
125
        const vec<int>& n_occ;
126
8975
        explicit ElimLt(const vec<int>& no) : n_occ(no) {}
127
128
        // TODO: are 64-bit operations here noticably bad on 32-bit platforms? Could use a saturating
129
        // 32-bit implementation instead then, but this will have to do for now.
130
175278422
        uint64_t cost  (Var x)        const { return (uint64_t)n_occ[toInt(mkLit(x))] * (uint64_t)n_occ[toInt(~mkLit(x))]; }
131
87639211
        bool operator()(Var x, Var y) const { return cost(x) < cost(y); }
132
133
        // TODO: investigate this order alternative more.
134
        // bool operator()(Var x, Var y) const {
135
        //     int c_x = cost(x);
136
        //     int c_y = cost(y);
137
        //     return c_x < c_y || c_x == c_y && x < y; }
138
    };
139
140
    struct ClauseDeleted {
141
        const ClauseAllocator& ca;
142
8975
        explicit ClauseDeleted(const ClauseAllocator& _ca) : ca(_ca) {}
143
1752604
        bool operator()(const CRef& cr) const { return ca[cr].mark() == 1; } };
144
145
    // Solver state:
146
    //
147
    int                 elimorder;
148
    bool                use_simplification;
149
    vec<uint32_t>       elimclauses;
150
    vec<char>           touched;
151
    OccLists<Var, vec<CRef>, ClauseDeleted>
152
                        occurs;
153
    vec<int>            n_occ;
154
    Heap<ElimLt>        elim_heap;
155
    Queue<CRef>         subsumption_queue;
156
    vec<char>           frozen;
157
    vec<char>           eliminated;
158
    int                 bwdsub_assigns;
159
    int                 n_touched;
160
161
    // Temporaries:
162
    //
163
    CRef                bwdsub_tmpunit;
164
165
    // Main internal methods:
166
    //
167
    lbool         solve_                   (bool do_simp = true, bool turn_off_simp = false);
168
    bool          asymm                    (Var v, CRef cr);
169
    bool          asymmVar                 (Var v);
170
    void          updateElimHeap           (Var v);
171
    void          gatherTouchedClauses     ();
172
    bool          merge                    (const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& out_clause);
173
    bool          merge                    (const Clause& _ps, const Clause& _qs, Var v, int& size);
174
    bool          backwardSubsumptionCheck (bool verbose = false);
175
    bool          eliminateVar             (Var v);
176
    void          extendModel              ();
177
178
    void          removeClause             (CRef cr);
179
    bool          strengthenClause         (CRef cr, Lit l);
180
    void          cleanUpClauses           ();
181
    bool          implied                  (const vec<Lit>& c);
182
    void          relocAll                 (ClauseAllocator& to);
183
};
184
185
186
//=================================================================================================
187
// Implementation of inline methods:
188
189
190
21345917
inline bool SimpSolver::isEliminated (Var v) const { return eliminated[v]; }
191
193148
inline void SimpSolver::updateElimHeap(Var v) {
192
193148
  Assert(use_simplification);
193
  // if (!frozen[v] && !isEliminated(v) && value(v) == l_Undef)
194
386296
  if (elim_heap.inHeap(v)
195
193148
      || (!frozen[v] && !isEliminated(v) && value(v) == l_Undef))
196
165789
    elim_heap.update(v);
197
193148
}
198
199
6976466
inline bool SimpSolver::addClause    (const vec<Lit>& ps, ClauseId& id)    { ps.copyTo(add_tmp); return addClause_(add_tmp, id); }
200
inline bool SimpSolver::addEmptyClause()                     { add_tmp.clear(); ClauseId id; return addClause_(add_tmp, id); }
201
inline bool SimpSolver::addClause    (Lit p, ClauseId& id)                 { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, id); }
202
inline bool SimpSolver::addClause    (Lit p, Lit q, ClauseId& id)          { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, id); }
203
inline bool SimpSolver::addClause    (Lit p, Lit q, Lit r, ClauseId& id)   { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, id); }
204
320398
inline void SimpSolver::setFrozen    (Var v, bool b) { frozen[v] = (char)b; if (use_simplification && !b) { updateElimHeap(v); } }
205
206
9172
inline lbool SimpSolver::solve        (                     bool do_simp, bool turn_off_simp)  {
207
9172
  budgetOff();
208
9172
  return solve_(do_simp, turn_off_simp);
209
 }
210
inline lbool SimpSolver::solve        (Lit p       ,        bool do_simp, bool turn_off_simp)  {
211
  budgetOff();
212
  assumptions.push(p);
213
  return solve_(do_simp, turn_off_simp);
214
 }
215
inline lbool SimpSolver::solve        (Lit p, Lit q,        bool do_simp, bool turn_off_simp)  {
216
  budgetOff();
217
  assumptions.push(p);
218
  assumptions.push(q);
219
  return solve_(do_simp, turn_off_simp);
220
 }
221
inline lbool SimpSolver::solve        (Lit p, Lit q, Lit r, bool do_simp, bool turn_off_simp)  {
222
  budgetOff();
223
  assumptions.push(p);
224
  assumptions.push(q);
225
  assumptions.push(r);
226
  return solve_(do_simp, turn_off_simp);
227
 }
228
inline lbool SimpSolver::solve        (const vec<Lit>& assumps, bool do_simp, bool turn_off_simp){
229
  budgetOff(); assumps.copyTo(assumptions);
230
  return solve_(do_simp, turn_off_simp);
231
}
232
233
inline lbool SimpSolver::solveLimited (const vec<Lit>& assumps, bool do_simp, bool turn_off_simp){
234
    assumps.copyTo(assumptions); return solve_(do_simp, turn_off_simp); }
235
236
inline lbool SimpSolver::solveLimited (bool do_simp, bool turn_off_simp){
237
    return solve_(do_simp, turn_off_simp); }
238
239
//=================================================================================================
240
} /* CVC4::BVMinisat namespace */
241
} /* CVC4 namespace */
242
243
244
#endif