43 return std::string(
"CaDiCaL ") +
solver->version();
48 for(
const auto &lit : bv)
52 else if(!lit.is_false())
56 for(
const auto &lit : bv)
74 static size_t cnf_clause_index = 0;
82 bv, cnf, cnf_clause_index, !clause_removed);
100 log.
status() <<
"got FALSE as assumption: instance is UNSATISFIABLE"
108 solver->assume(a.dimacs());
120 log.
status() <<
"SAT checker: solving returned without solution"
123 "solving inside CaDiCaL SAT solver has been interrupted");
133 INVARIANT(
false,
"method not supported");
151 for(
const auto &assumption : bv)
153 if(!assumption.is_true())
Thrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an erro...
bool process_clause(const bvt &bv, bvt &dest) const
filter 'true' from clause, eliminate duplicates, recognise trivially satisfied clauses
virtual size_t no_variables() const override
std::unique_ptr< clause_hardness_collectort > solver_hardness
mstreamt & statistics() const
mstreamt & status() const
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
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.
std::vector< literalt > bvt
int solver(std::istream &in)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.