cprover
satcheck_cadical.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Michael Tautschnig
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_SOLVERS_SAT_SATCHECK_CADICAL_H
11 #define CPROVER_SOLVERS_SAT_SATCHECK_CADICAL_H
12 
13 #include "cnf.h"
14 
16 
17 namespace CaDiCaL // NOLINT(readability/namespace)
18 {
19  class Solver; // NOLINT(readability/identifiers)
20 }
21 
23 {
24 public:
25  explicit satcheck_cadicalt(message_handlert &message_handler);
26  virtual ~satcheck_cadicalt();
27 
28  const std::string solver_text() override;
29  tvt l_get(literalt a) const override;
30 
31  void lcnf(const bvt &bv) override;
32  void set_assignment(literalt a, bool value) override;
33 
34  void set_assumptions(const bvt &_assumptions) override;
35  bool has_set_assumptions() const override
36  {
37  return true;
38  }
39  bool has_is_in_conflict() const override
40  {
41  return true;
42  }
43  bool is_in_conflict(literalt a) const override;
44 
45  void
46  with_solver_hardness(std::function<void(solver_hardnesst &)> handler) override
47  {
48  if(solver_hardness.has_value())
49  {
50  handler(solver_hardness.value());
51  }
52  }
53 
55  {
57  }
58 
59 protected:
60  resultt do_prop_solve() override;
61 
62  // NOLINTNEXTLINE(readability/identifiers)
63  CaDiCaL::Solver * solver;
64 
66 
68 };
69 
70 #endif // CPROVER_SOLVERS_SAT_SATCHECK_CADICAL_H
resultt
Definition: prop.h:99
bool has_set_assumptions() const override
void set_assumptions(const bvt &_assumptions) override
virtual ~satcheck_cadicalt()
optionalt< solver_hardnesst > solver_hardness
const std::string solver_text() override
resultt do_prop_solve() override
void set_assignment(literalt a, bool value) override
void enable_hardness_collection() override
CaDiCaL::Solver * solver
void lcnf(const bvt &bv) override
satcheck_cadicalt(message_handlert &message_handler)
tvt l_get(literalt a) const override
void with_solver_hardness(std::function< void(solver_hardnesst &)> handler) override
bool is_in_conflict(literalt a) const override
Returns true if an assumption is in the final conflict.
bool has_is_in_conflict() const override
Definition: threeval.h:20
CNF Generation, via Tseitin.
Capability to collect the statistics of the complexity of individual solver queries.
std::vector< literalt > bvt
Definition: literal.h:201
nonstd::optional< T > optionalt
Definition: optional.h:35
A structure that facilitates collecting the complexity statistics from a decision procedure.