cprover
Loading...
Searching...
No Matches
satcheck_cadical.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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
17namespace CaDiCaL // NOLINT(readability/namespace)
18{
19 class Solver; // NOLINT(readability/identifiers)
20}
21
23{
24public:
25 explicit satcheck_cadicalt(message_handlert &message_handler);
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
45protected:
47
48 // NOLINTNEXTLINE(readability/identifiers)
49 CaDiCaL::Solver * solver;
50
52};
53
54#endif // CPROVER_SOLVERS_SAT_SATCHECK_CADICAL_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
resultt
Definition prop.h:98
bool has_set_assumptions() const override
void set_assumptions(const bvt &_assumptions) override
virtual ~satcheck_cadicalt()
const std::string solver_text() override
resultt do_prop_solve() override
void set_assignment(literalt a, bool value) override
CaDiCaL::Solver * solver
void lcnf(const bvt &bv) override
satcheck_cadicalt(message_handlert &message_handler)
tvt l_get(literalt a) const 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