GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/prop/sat_solver.h Lines: 6 38 15.8 %
Date: 2021-03-22 Branches: 0 30 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file sat_solver.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Dejan Jovanovic, Liana Hadarean, Mathias Preiner
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 SAT Solver.
13
 **
14
 ** SAT Solver.
15
 **/
16
17
#include "cvc4_private.h"
18
19
#ifndef CVC4__PROP__SAT_SOLVER_H
20
#define CVC4__PROP__SAT_SOLVER_H
21
22
#include <string>
23
24
#include "context/cdlist.h"
25
#include "context/context.h"
26
#include "expr/node.h"
27
#include "expr/proof_node_manager.h"
28
#include "proof/clause_id.h"
29
#include "prop/bv_sat_solver_notify.h"
30
#include "prop/sat_solver_types.h"
31
#include "util/statistics_registry.h"
32
33
namespace CVC4 {
34
35
namespace prop {
36
37
class TheoryProxy;
38
39
18034
class SatSolver {
40
41
public:
42
43
  /** Virtual destructor */
44
18028
  virtual ~SatSolver() { }
45
46
  /** Assert a clause in the solver. */
47
  virtual ClauseId addClause(SatClause& clause,
48
                             bool removable) = 0;
49
50
  /** Return true if the solver supports native xor resoning */
51
  virtual bool nativeXor() { return false; }
52
53
  /** Add a clause corresponding to rhs = l1 xor .. xor ln  */
54
  virtual ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) = 0;
55
56
  /**
57
   * Create a new boolean variable in the solver.
58
   * @param isTheoryAtom is this a theory atom that needs to be asserted to theory
59
   * @param preRegister whether to preregister the atom with the theory
60
   * @param canErase whether the sat solver can safely eliminate this variable
61
   *
62
   */
63
  virtual SatVariable newVar(bool isTheoryAtom, bool preRegister, bool canErase) = 0;
64
65
  /** Create a new (or return an existing) boolean variable representing the constant true */
66
  virtual SatVariable trueVar() = 0;
67
68
  /** Create a new (or return an existing) boolean variable representing the constant false */
69
  virtual SatVariable falseVar() = 0;
70
71
  /** Check the satisfiability of the added clauses */
72
  virtual SatValue solve() = 0;
73
74
  /** Check the satisfiability of the added clauses */
75
  virtual SatValue solve(long unsigned int&) = 0;
76
77
  /** Check satisfiability under assumptions */
78
  virtual SatValue solve(const std::vector<SatLiteral>& assumptions)
79
  {
80
    Unimplemented() << "Solving under assumptions not implemented";
81
    return SAT_VALUE_UNKNOWN;
82
  };
83
84
  /**
85
   * Tell SAT solver to only do propagation on next solve().
86
   *
87
   * @return true if feature is supported, otherwise false.
88
   */
89
  virtual bool setPropagateOnly() { return false; }
90
91
  /** Interrupt the solver */
92
  virtual void interrupt() = 0;
93
94
  /** Call value() during the search.*/
95
  virtual SatValue value(SatLiteral l) = 0;
96
97
  /** Call modelValue() when the search is done.*/
98
  virtual SatValue modelValue(SatLiteral l) = 0;
99
100
  /** Get the current assertion level */
101
  virtual unsigned getAssertionLevel() const = 0;
102
103
  /** Check if the solver is in an inconsistent state */
104
  virtual bool ok() const = 0;
105
106
  /**
107
   * Get list of unsatisfiable assumptions.
108
   *
109
   * The returned assumptions are a subset of the assumptions provided to
110
   * the solve method.
111
   * Can only be called if satisfiability check under assumptions was used and
112
   * if it returned SAT_VALUE_FALSE.
113
   */
114
  virtual void getUnsatAssumptions(std::vector<SatLiteral>& unsat_assumptions)
115
  {
116
    Unimplemented() << "getUnsatAssumptions not implemented";
117
  }
118
119
};/* class SatSolver */
120
121
122
8975
class BVSatSolverInterface: public SatSolver {
123
public:
124
125
8972
  virtual ~BVSatSolverInterface() {}
126
  /** Interface for notifications */
127
128
  virtual void setNotify(BVSatSolverNotify* notify) = 0;
129
130
  virtual void markUnremovable(SatLiteral lit) = 0;
131
132
  virtual void getUnsatCore(SatClause& unsatCore) = 0;
133
134
  virtual void addMarkerLiteral(SatLiteral lit) = 0;
135
136
  virtual SatValue propagate() = 0;
137
138
  virtual void explain(SatLiteral lit, std::vector<SatLiteral>& explanation) = 0;
139
140
  virtual SatValue assertAssumption(SatLiteral lit, bool propagate = false) = 0;
141
142
  virtual void popAssumption() = 0;
143
144
};/* class BVSatSolverInterface */
145
146
9027
class CDCLTSatSolverInterface : public SatSolver
147
{
148
 public:
149
9024
  virtual ~CDCLTSatSolverInterface(){};
150
151
  virtual void initialize(context::Context* context,
152
                          prop::TheoryProxy* theoryProxy,
153
                          CVC4::context::UserContext* userContext,
154
                          ProofNodeManager* pnm) = 0;
155
156
  virtual void push() = 0;
157
158
  virtual void pop() = 0;
159
160
  /*
161
   * Reset the decisions in the DPLL(T) SAT solver at the current assertion
162
   * level.
163
   */
164
  virtual void resetTrail() = 0;
165
166
  virtual bool properExplanation(SatLiteral lit, SatLiteral expl) const = 0;
167
168
  virtual void requirePhase(SatLiteral lit) = 0;
169
170
  virtual bool isDecision(SatVariable decn) const = 0;
171
172
  virtual std::shared_ptr<ProofNode> getProof() = 0;
173
174
}; /* class CDCLTSatSolverInterface */
175
176
inline std::ostream& operator <<(std::ostream& out, prop::SatLiteral lit) {
177
  out << lit.toString();
178
  return out;
179
}
180
181
inline std::ostream& operator <<(std::ostream& out, const prop::SatClause& clause) {
182
  out << "clause:";
183
  for(unsigned i = 0; i < clause.size(); ++i) {
184
    out << " " << clause[i];
185
  }
186
  out << ";";
187
  return out;
188
}
189
190
inline std::ostream& operator <<(std::ostream& out, prop::SatValue val) {
191
  std::string str;
192
  switch(val) {
193
  case prop::SAT_VALUE_UNKNOWN:
194
    str = "_";
195
    break;
196
  case prop::SAT_VALUE_TRUE:
197
    str = "1";
198
    break;
199
  case prop::SAT_VALUE_FALSE:
200
    str = "0";
201
    break;
202
  default:
203
    str = "Error";
204
    break;
205
  }
206
207
  out << str;
208
  return out;
209
}
210
211
}/* CVC4::prop namespace */
212
}/* CVC4 namespace */
213
214
#endif /* CVC4__PROP__SAT_MODULE_H */