cprover
satcheck_ipasir.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Norbert Manthey, nmanthey@amazon.com
6 
7 See \ref compilation-and-development-subsection-sat-solver for build
8 instructions.
9 
10 \*******************************************************************/
11 
12 #ifndef CPROVER_SOLVERS_SAT_SATCHECK_IPASIR_H
13 #define CPROVER_SOLVERS_SAT_SATCHECK_IPASIR_H
14 
15 #include "cnf.h"
16 
18 
21 {
22 public:
24  virtual ~satcheck_ipasirt() override;
25 
27  const std::string solver_text() override;
28 
30  tvt l_get(literalt a) const override final;
31 
32  void lcnf(const bvt &bv) override final;
33 
34  /* This method is not supported, and currently not called anywhere in CBMC */
35  void set_assignment(literalt a, bool value) override;
36 
37  void set_assumptions(const bvt &_assumptions) override;
38 
39  bool is_in_conflict(literalt a) const override;
40  bool has_set_assumptions() const override final
41  {
42  return true;
43  }
44  bool has_is_in_conflict() const override final
45  {
46  return true;
47  }
48 
49  void
50  with_solver_hardness(std::function<void(solver_hardnesst &)> handler) override
51  {
52  if(solver_hardness.has_value())
53  {
54  handler(solver_hardness.value());
55  }
56  }
57 
59  {
61  }
62 
63 protected:
64  resultt do_prop_solve() override;
65 
66  void *solver;
67 
69 
71 };
72 
73 #endif // CPROVER_SOLVERS_SAT_SATCHECK_IPASIR_H
resultt
Definition: prop.h:97
Interface for generic SAT solver interface IPASIR.
bool has_set_assumptions() const override final
void set_assumptions(const bvt &_assumptions) override
tvt l_get(literalt a) const override final
This method returns the truth value for a literal of the current SAT model.
resultt do_prop_solve() override
optionalt< solver_hardnesst > solver_hardness
bool has_is_in_conflict() const override final
virtual ~satcheck_ipasirt() override
satcheck_ipasirt(message_handlert &message_handler)
void enable_hardness_collection() override
void lcnf(const bvt &bv) override final
void set_assignment(literalt a, bool value) override
bool is_in_conflict(literalt a) const override
Returns true if an assumption is in the final conflict.
void with_solver_hardness(std::function< void(solver_hardnesst &)> handler) override
const std::string solver_text() override
This method returns the description produced by the linked SAT solver.
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.