Go to the documentation of this file.
17 #include <cadical.hpp>
42 return std::string(
"CaDiCaL ") +
solver->version();
47 for(
const auto &lit : bv)
51 else if(!lit.is_false())
55 for(
const auto &lit : bv)
77 log.
status() <<
"SAT checker inconsistent: instance is UNSATISFIABLE"
89 log.
status() <<
"SAT checker: instance is UNSATISFIABLE"
93 log.
status() <<
"SAT checker: solving returned without solution"
96 "solving inside CaDiCaL SAT solver has been interrupted");
107 INVARIANT(
false,
"method not supported");
123 INVARIANT(
false,
"method not supported");
128 INVARIANT(
false,
"method not supported");
void set_assignment(literalt a, bool value) override
std::vector< literalt > bvt
mstreamt & status() const
bool is_in_conflict(literalt a) const override
Returns true if an assumption is in the final conflict.
void set_assumptions(const bvt &_assumptions) override
virtual ~satcheck_cadicalt()
resultt do_prop_solve() override
void lcnf(const bvt &bv) override
tvt l_get(literalt a) const override
int solver(std::istream &in)
virtual size_t no_variables() const override
const std::string solver_text() override
mstreamt & statistics() const
Thrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an erro...