15 #include "booleforce.h" 20 booleforce_set_trace(
false);
25 booleforce_set_trace(
true);
47 int r=booleforce_deref(v);
64 return std::string(
"Booleforce version ")+booleforce_version();
74 for(
unsigned j=0; j<tmp.size(); j++)
75 booleforce_add(tmp[j].dimacs());
87 int result=booleforce_sat();
94 case BOOLEFORCE_UNSATISFIABLE:
95 msg=
"SAT checker: instance is UNSATISFIABLE";
98 case BOOLEFORCE_SATISFIABLE:
99 msg=
"SAT checker: instance is SATISFIABLE";
103 msg=
"SAT checker failed: unknown result";
110 if(
result==BOOLEFORCE_UNSATISFIABLE)
113 return P_UNSATISFIABLE;
116 if(
result==BOOLEFORCE_SATISFIABLE)
119 return P_SATISFIABLE;
129 return booleforce_var_in_core(l.
var_no());
bool is_in_core(literalt l) const
bool process_clause(const bvt &bv, bvt &dest)
filter 'true' from clause, eliminate duplicates, recognise trivially satisfied clauses ...
static mstreamt & eom(mstreamt &m)
virtual void lcnf(const bvt &bv)
virtual const std::string solver_text()
satcheck_booleforce_coret()
virtual tvt l_get(literalt a) const
mstreamt & result() const
mstreamt & status() const
virtual ~satcheck_booleforce_baset()
virtual size_t no_variables() const override
virtual resultt prop_solve()
std::vector< literalt > bvt