16 #include <cadical.hpp> 41 return std::string(
"CaDiCaL ") +
solver->version();
46 for(
const auto &lit : bv)
50 else if(!lit.is_false())
54 for(
const auto &lit : bv)
93 throw "solving inside CaDiCaL SAT solver has been interrupted";
104 INVARIANT(
false,
"method not supported");
120 INVARIANT(
false,
"method not supported");
125 INVARIANT(
false,
"method not supported");
virtual void set_assumptions(const bvt &_assumptions) override
virtual ~satcheck_cadicalt()
virtual const std::string solver_text() override
static mstreamt & eom(mstreamt &m)
virtual resultt prop_solve() override
#define INVARIANT(CONDITION, REASON)
virtual void lcnf(const bvt &bv) override
int solver(std::istream &in)
virtual tvt l_get(literalt a) const override
mstreamt & result() const
mstreamt & status() const
virtual void set_assignment(literalt a, bool value) override
virtual bool is_in_conflict(literalt a) const override
virtual size_t no_variables() const override
std::vector< literalt > bvt