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
satcheck_cadicalt::set_assignment
void set_assignment(literalt a, bool value) override
hardness_collector.h
Capability to collect the statistics of the complexity of individual solver queries.
satcheck_cadicalt::with_solver_hardness
void with_solver_hardness(std::function< void(solver_hardnesst &)> handler) override
Definition: satcheck_cadical.h:46
bvt
std::vector< literalt > bvt
Definition: literal.h:201
satcheck_cadicalt::is_in_conflict
bool is_in_conflict(literalt a) const override
Returns true if an assumption is in the final conflict.
CaDiCaL
Definition: satcheck_cadical.h:18
satcheck_cadicalt::solver
CaDiCaL::Solver * solver
Definition: satcheck_cadical.h:63
satcheck_cadicalt::set_assumptions
void set_assumptions(const bvt &_assumptions) override
satcheck_cadicalt::has_is_in_conflict
bool has_is_in_conflict() const override
Definition: satcheck_cadical.h:39
satcheck_cadicalt::satcheck_cadicalt
satcheck_cadicalt(message_handlert &message_handler)
cnf_solvert
Definition: cnf.h:73
satcheck_cadicalt::~satcheck_cadicalt
virtual ~satcheck_cadicalt()
satcheck_cadicalt::do_prop_solve
resultt do_prop_solve() override
satcheck_cadicalt::lcnf
void lcnf(const bvt &bv) override
satcheck_cadicalt::solver_hardness
optionalt< solver_hardnesst > solver_hardness
Definition: satcheck_cadical.h:67
message_handlert
Definition: message.h:28
propt::resultt
resultt
Definition: prop.h:99
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
satcheck_cadicalt::l_get
tvt l_get(literalt a) const override
tvt
Definition: threeval.h:20
solver_hardnesst
A structure that facilitates collecting the complexity statistics from a decision procedure.
Definition: solver_hardness.h:45
satcheck_cadicalt::enable_hardness_collection
void enable_hardness_collection() override
Definition: satcheck_cadical.h:54
literalt
Definition: literal.h:26
hardness_collectort
Definition: hardness_collector.h:23
satcheck_cadicalt::has_set_assumptions
bool has_set_assumptions() const override
Definition: satcheck_cadical.h:35
cnf.h
CNF Generation, via Tseitin.
satcheck_cadicalt::assumptions
bvt assumptions
Definition: satcheck_cadical.h:65
satcheck_cadicalt::solver_text
const std::string solver_text() override
satcheck_cadicalt
Definition: satcheck_cadical.h:23