15#include "booleforce.h"
20 booleforce_set_trace(
false);
25 booleforce_set_trace(
true);
46 int r=booleforce_deref(v);
63 return std::string(
"Booleforce version ")+booleforce_version();
73 for(
unsigned j=0; j<tmp.size(); j++)
74 booleforce_add(tmp[j].dimacs());
86 int result=booleforce_sat();
93 case BOOLEFORCE_UNSATISFIABLE:
94 msg=
"SAT checker: instance is UNSATISFIABLE";
97 case BOOLEFORCE_SATISFIABLE:
98 msg=
"SAT checker: instance is SATISFIABLE";
102 msg=
"SAT checker failed: unknown result";
109 if(result==BOOLEFORCE_UNSATISFIABLE)
115 if(result==BOOLEFORCE_SATISFIABLE)
128 return booleforce_var_in_core(l.
var_no());
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
mstreamt & status() const
virtual ~satcheck_booleforce_baset()
void lcnf(const bvt &bv) override
tvt l_get(literalt a) const override
resultt do_prop_solve() override
const std::string solver_text() override
bool is_in_core(literalt l) const
satcheck_booleforce_coret()
std::vector< literalt > bvt
#define CHECK_RETURN(CONDITION)
#define PRECONDITION(CONDITION)