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 std::string solver_text() const 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 bool has_assumptions() const override
35 {
36 return true;
37 }
38 bool has_is_in_conflict() const override
39 {
40 return true;
41 }
42 bool is_in_conflict(literalt a) const override;
43
44protected:
45 resultt do_prop_solve(const bvt &assumptions) override;
46
47 // NOLINTNEXTLINE(readability/identifiers)
48 CaDiCaL::Solver *solver;
49};
50
51#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:563
resultt
Definition prop.h:101
virtual ~satcheck_cadicalt()
void set_assignment(literalt a, bool value) override
CaDiCaL::Solver * solver
bool has_assumptions() const override
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.
resultt do_prop_solve(const bvt &assumptions) override
std::string solver_text() const override
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