GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/prop/sat_solver_types.h Lines: 29 33 87.9 %
Date: 2021-03-23 Branches: 5 16 31.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file sat_solver_types.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Dejan Jovanovic, Alex Ozdemir, Liana Hadarean
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief This class transforms a sequence of formulas into clauses.
13
 **
14
 ** This class takes a sequence of formulas.
15
 ** It outputs a stream of clauses that is propositionally
16
 ** equi-satisfiable with the conjunction of the formulas.
17
 ** This stream is maintained in an online fashion.
18
 **
19
 ** Unlike other parts of the system it is aware of the PropEngine's
20
 ** internals such as the representation and translation of [??? -Chris]
21
 **/
22
23
#pragma once
24
25
#include "cvc4_private.h"
26
27
#include <sstream>
28
#include <string>
29
#include <unordered_set>
30
#include <vector>
31
32
namespace CVC4 {
33
namespace prop {
34
35
/**
36
 * Boolean values of the SAT solver.
37
 */
38
enum SatValue {
39
  SAT_VALUE_UNKNOWN,
40
  SAT_VALUE_TRUE,
41
  SAT_VALUE_FALSE
42
};
43
44
/** Helper function for inverting a SatValue */
45
11871876
inline SatValue invertValue(SatValue v)
46
{
47
11871876
  if(v == SAT_VALUE_UNKNOWN) return SAT_VALUE_UNKNOWN;
48
11871876
  else if(v == SAT_VALUE_TRUE) return SAT_VALUE_FALSE;
49
2198036
  else return SAT_VALUE_TRUE;
50
}
51
52
53
/**
54
 * A variable of the SAT solver.
55
 */
56
typedef uint64_t SatVariable;
57
58
/**
59
 * Undefined SAT solver variable.
60
 */
61
const SatVariable undefSatVariable = SatVariable(-1);
62
63
/**
64
 * A SAT literal is a variable or an negated variable.
65
 */
66
class SatLiteral {
67
68
  /**
69
   * The value holds the variable and a bit noting if the variable is negated.
70
   */
71
  uint64_t d_value;
72
73
public:
74
75
  /**
76
   * Construct an undefined SAT literal.
77
   */
78
44982079
  SatLiteral()
79
44982079
  : d_value(undefSatVariable)
80
44982079
  {}
81
82
  /**
83
   * Construct a literal given a possible negated variable.
84
   */
85
61833474
  SatLiteral(SatVariable var, bool negated = false) {
86
61833474
    d_value = var + var + (int)negated;
87
61833474
  }
88
89
  /**
90
   * Returns the variable of the literal.
91
   */
92
123123368
  SatVariable getSatVariable() const {
93
123123368
    return d_value >> 1;
94
  }
95
96
  /**
97
   * Returns true if the literal is a negated variable.
98
   */
99
116458490
  bool isNegated() const {
100
116458490
    return d_value & 1;
101
  }
102
103
  /**
104
   * Negate the given literal.
105
   */
106
26844782
  SatLiteral operator ~ () const {
107
26844782
    return SatLiteral(getSatVariable(), !isNegated());
108
  }
109
110
  /**
111
   * Compare two literals for equality.
112
   */
113
164660797
  bool operator == (const SatLiteral& other) const {
114
164660797
    return d_value == other.d_value;
115
  }
116
117
  /**
118
   * Compare two literals for dis-equality.
119
   */
120
9331541
  bool operator != (const SatLiteral& other) const {
121
9331541
    return !(*this == other);
122
  }
123
124
  /**
125
   * Compare two literals
126
   */
127
2078622
  bool operator<(const SatLiteral& other) const
128
  {
129
2078622
    return getSatVariable() == other.getSatVariable()
130
3969896
               ? isNegated() < other.isNegated()
131
3969896
               : getSatVariable() < other.getSatVariable();
132
  }
133
134
  /**
135
   * Returns a string representation of the literal.
136
   */
137
  std::string toString() const {
138
    std::ostringstream os;
139
    os << (isNegated() ? "~" : "") << getSatVariable();
140
    return os.str();
141
  }
142
143
  /**
144
   * Returns the hash value of a literal.
145
   */
146
68386361
  size_t hash() const {
147
68386361
    return (size_t)d_value;
148
  }
149
150
  uint64_t toInt() const {
151
    return d_value;
152
  }
153
154
  /**
155
   * Returns true if the literal is undefined.
156
   */
157
  bool isNull() const {
158
    return getSatVariable() == undefSatVariable;
159
  }
160
};
161
162
/**
163
 * A constant representing a undefined literal.
164
 */
165
302445
const SatLiteral undefSatLiteral = SatLiteral(undefSatVariable);
166
167
/**
168
 * Helper for hashing the literals.
169
 */
170
struct SatLiteralHashFunction {
171
68386361
  inline size_t operator() (const SatLiteral& literal) const {
172
68386361
    return literal.hash();
173
  }
174
};
175
176
/**
177
 * A SAT clause is a vector of literals.
178
 */
179
typedef std::vector<SatLiteral> SatClause;
180
181
struct SatClauseSetHashFunction
182
{
183
  inline size_t operator()(
184
      const std::unordered_set<SatLiteral, SatLiteralHashFunction>& clause)
185
      const
186
  {
187
    size_t acc = 0;
188
    for (const auto& l : clause)
189
    {
190
      acc ^= l.hash();
191
    }
192
    return acc;
193
  }
194
};
195
196
struct SatClauseLessThan
197
{
198
  bool operator()(const SatClause& l, const SatClause& r) const;
199
};
200
201
/**
202
 * Each object in the SAT solver, such as as variables and clauses, can be assigned a life span,
203
 * so that the SAT solver can (or should) remove them when the lifespan is over.
204
 */
205
enum SatSolverLifespan
206
{
207
  /**
208
   * The object should stay forever and never be removed
209
   */
210
  SAT_LIFESPAN_PERMANENT,
211
  /**
212
   * The object can be removed at any point when it becomes unnecessary.
213
   */
214
  SAT_LIFESPAN_REMOVABLE,
215
  /**
216
   * The object must be removed as soon as the SAT solver exits the search context
217
   * where the object got introduced.
218
   */
219
  SAT_LIFESPAN_SEARCH_CONTEXT_STRICT,
220
  /**
221
   * The object can be removed when SAT solver exits the search context where the object
222
   * got introduced, but can be kept at the solver discretion.
223
   */
224
  SAT_LIFESPAN_SEARCH_CONTEXT_LENIENT,
225
  /**
226
   * The object must be removed as soon as the SAT solver exits the user-level context where
227
   * the object got introduced.
228
   */
229
  SAT_LIFESPAN_USER_CONTEXT_STRICT,
230
  /**
231
   * The object can be removed when the SAT solver exits the user-level context where
232
   * the object got introduced.
233
   */
234
  SAT_LIFESPAN_USER_CONTEXT_LENIENT
235
};
236
237
}
238
}